feat: configurable warnings (uninit locals, unused unfold)

src/ecCommands.ml

@@ -99,6 +99,8 @@ let gstate_bool_flags = [
   EcGState.pp_showtvi;
   EcGState.circuit_timing;
   EcGState.circuit_debug_smt;
+  EcGState.warn_uninit;
+  EcGState.warn_unused_unfold;
 ]
 
 exception InvalidPragma of string

src/ecGState.ml

@@ -82,6 +82,18 @@ let circuit_debug_smt = "Circuit:debug_smt"
 let get_circuit_debug_smt (g : gstate) : bool =
   getflag ~default:false circuit_debug_smt g
 
+(* -------------------------------------------------------------------- *)
+let warn_uninit = "Warn:uninit"
+
+let get_warn_uninit (g : gstate) : bool =
+  getflag ~default:true warn_uninit g
+
+(* -------------------------------------------------------------------- *)
+let warn_unused_unfold = "Warn:unused_unfold"
+
+let get_warn_unused_unfold (g : gstate) : bool =
+  getflag ~default:true warn_unused_unfold g
+
 (* -------------------------------------------------------------------- *)
 let add_notifier (notifier : loglevel -> string Lazy.t -> unit) (gs : gstate) =
   let notifier = { nt_id = EcUid.unique (); nt_cb = notifier; } in

src/ecGState.mli

@@ -40,6 +40,14 @@ val get_circuit_timing : gstate -> bool
 val circuit_debug_smt : string
 val get_circuit_debug_smt : gstate -> bool
 
+(* --------------------------------------------------------------------- *)
+val warn_uninit : string
+val get_warn_uninit : gstate -> bool
+
+(* --------------------------------------------------------------------- *)
+val warn_unused_unfold : string
+val get_warn_unused_unfold : gstate -> bool
+
 (* --------------------------------------------------------------------- *)
 type nid_t
 type loglevel = [`Debug | `Info | `Warning | `Critical]

src/ecHiGoal.ml

@@ -696,7 +696,8 @@ let process_delta ?target ((s :rwside), o, p) tc =
           EcReduction.delta_h = check_id; } in
     let redform = EcReduction.simplify ri hyps target in
 
-    if EcFol.f_equal target redform then
+    if EcGState.get_warn_unused_unfold (EcEnv.gstate env)
+       && EcFol.f_equal target redform then
       EcEnv.notify env `Warning "unused unfold: /%s" x;
 
     t_change ~ri:{ ri with eta = true; beta = true; } ?target:idtg redform tc

src/ecOptions.ml

@@ -90,6 +90,7 @@ type ini_options = {
   ini_timeout  : int option;
   ini_idirs    : (string option * string) list;
   ini_rdirs    : (string option * string) list;
+  ini_pragmas  : string list;
 }
 
 type ini_context = {
@@ -116,6 +117,8 @@ module Ini : sig
 
   val get_rdirs : ini_context -> (string option * string) list
 
+  val get_pragmas : ini_context -> string list
+
   (* ------------------------------------------------------------------ *)
   val get_all_ppwidth : ini_context list -> int option
 
@@ -132,6 +135,8 @@ module Ini : sig
   val get_all_idirs : ini_context list -> (string option * string) list
 
   val get_all_rdirs : ini_context list -> (string option * string) list
+
+  val get_all_pragmas : ini_context list -> string list
 end = struct
   (* ------------------------------------------------------------------ *)
   let absolute ?(root : string option) (filename : string) =
@@ -174,6 +179,9 @@ end = struct
       (snd_map (absolute ?root:ini.inic_root))
       ini.inic_ini.ini_rdirs
 
+  let get_pragmas (ini : ini_context) =
+    ini.inic_ini.ini_pragmas
+
   (* ------------------------------------------------------------------ *)
   let get_all_ppwidth (ini : ini_context list) =
     List.find_map_opt get_ppwidth ini
@@ -198,6 +206,9 @@ end = struct
 
   let get_all_rdirs (ini : ini_context list) =
     List.flatten (List.map get_rdirs ini)
+
+  let get_all_pragmas (ini : ini_context list) =
+    List.flatten (List.map get_pragmas ini)
 end
 
 (* -------------------------------------------------------------------- *)
@@ -525,7 +536,8 @@ let prv_options_of_values ini values =
         | None -> Ini.get_all_quorum ini
         | Some _ as i -> i
       end;
-      prvo_pragmas   = get_string_list "pragmas" values;
+      prvo_pragmas   =
+        (Ini.get_all_pragmas ini) @ (get_string_list "pragmas" values);
       prvo_ppwidth   = begin
         match get_int "pp-width" values with
         | None -> Ini.get_all_ppwidth ini
@@ -747,7 +759,8 @@ let read_ini_file (filename : string) =
       ini_quorum   = tryint  "quorum"  ;
       ini_timeout  = tryint  "timeout" ;
       ini_idirs    = List.map parse_idir (trylist "idirs");
-      ini_rdirs    = List.map parse_idir (trylist "rdirs"); } in
+      ini_rdirs    = List.map parse_idir (trylist "rdirs");
+      ini_pragmas  = trylist "pragmas"; } in
 
   { ini_ppwidth  = ini.ini_ppwidth;
     ini_why3     = omap expand ini.ini_why3;
@@ -756,4 +769,5 @@ let read_ini_file (filename : string) =
     ini_quorum   = ini.ini_quorum;
     ini_timeout  = ini.ini_timeout;
     ini_idirs    = ini.ini_idirs;
-    ini_rdirs    = ini.ini_rdirs; }
+    ini_rdirs    = ini.ini_rdirs;
+    ini_pragmas  = ini.ini_pragmas; }

src/ecOptions.mli

@@ -86,6 +86,7 @@ type ini_options = {
   ini_timeout  : int option;
   ini_idirs    : (string option * string) list;
   ini_rdirs    : (string option * string) list;
+  ini_pragmas  : string list;
 }
 
 type ini_context = {

src/ecScope.ml

@@ -1761,7 +1761,10 @@ module Mod = struct
     in
 
     let m = TT.transmod (env scope) ~attop:true ptm in
-    let ur = EcModules.get_uninit_read_of_module (path scope) m in
+    let ur =
+      if EcGState.get_warn_uninit (EcEnv.gstate (env scope)) then
+        EcModules.get_uninit_read_of_module (path scope) m
+      else [] in
 
     if not (List.is_empty ur) then begin
       let ppe = EcPrinting.PPEnv.ofenv (env scope) in