fixup! [eacsl] Create an analysis to compute translation location of labeled pred and terms

src/plugins/e-acsl/src/analyses/analyses_datatype.ml

@@ -44,12 +44,12 @@ module Annotation_kind =
         | RTE -> Format.fprintf fmt "RTE"
     end)
 
-module PredOrTerm =
+module Pred_or_term =
   Datatype.Make_with_collections
     (struct
       type t = pred_or_term
 
-      let name = "E_ACSL.PredOrTerm"
+      let name = "E_ACSL.Pred_or_term"
 
       let reprs =
         let reprs =
@@ -85,13 +85,12 @@ module PredOrTerm =
       let varname _ = "pred_or_term"
     end)
 
-(** Extended logic label module to associate a statement to a label when
-    necessary. For instance, the label `Old` is associated with its contract
-    statement to be able to distinguish two `Old` annotations in the same
-    function. On the contrary the `Pre` label does not have an associated
-    statement because this label designate the same location for all contracts
-    in the same function. *)
-module ExtLogicLabel: sig
+(** [Ext_logic_label] associates a statement to a label when necessary. For
+    instance, the label `Old` is associated with its contract statement to
+    distinguish two `Old` annotations in the same function. On the contrary, the
+    `Pre` label does not have an associated statement because this label
+    represents the same location for all contracts in the same function. *)
+module Ext_logic_label: sig
   include Datatype.S_with_collections with type t = logic_label * stmt option
 
   val from: kinstr -> logic_label -> logic_label * stmt option
@@ -102,11 +101,11 @@ end = struct
       (Datatype.Option_with_collections
          (Stmt)
          (struct
-           let module_name = "E_ACSL.Labels.ExtLogicLabel.StmtOption"
+           let module_name = "E_ACSL.Labels.Ext_logic_label.StmtOption"
          end))
-      (struct let module_name = "E_ACSL.Labels.ExtLogicLabel" end)
+      (struct let module_name = "E_ACSL.Labels.Ext_logic_label" end)
 
-  (* Override [pretty] to print a more compact representation of [ExtLogicLabel]
+  (* Override [pretty] to print a more compact representation of [Ext_logic_label]
      for debugging purposes. *)
   let pretty fmt (label, from_stmt_opt) =
     match from_stmt_opt with
@@ -163,14 +162,14 @@ let basic_kinstr_hash kinstr =
   | Kglobal -> 1 lsl 29
   | Kstmt _ -> 1 lsl 31
 
-module AtData = struct
+module At_data = struct
   let create ?error kf kinstr lscope pot label =
     { kf; kinstr; lscope; pot; label; error }
 
   include Datatype.Make_with_collections
       (struct
         type t = at_data
-        let name = "E_ACSL.AtData"
+        let name = "E_ACSL.At_data"
 
         let reprs =
           List.fold_left
@@ -185,7 +184,7 @@ module AtData = struct
                            acc
                            Logic_label.reprs)
                       acc
-                      PredOrTerm.reprs)
+                      Pred_or_term.reprs)
                  acc
                  Kinstr.reprs)
             []
@@ -216,33 +215,33 @@ module AtData = struct
             else cmp
           in
           let cmp =
-            if cmp = 0 then PredOrTerm.compare pot1 pot2
+            if cmp = 0 then Pred_or_term.compare pot1 pot2
             else cmp
           in
           if cmp = 0 then
-            let extlabel1 = ExtLogicLabel.from kinstr1 label1 in
-            let extlabel2 = ExtLogicLabel.from kinstr2 label2 in
-            ExtLogicLabel.compare extlabel1 extlabel2
+            let extlabel1 = Ext_logic_label.from kinstr1 label1 in
+            let extlabel2 = Ext_logic_label.from kinstr2 label2 in
+            Ext_logic_label.compare extlabel1 extlabel2
           else cmp
 
         let equal = Datatype.from_compare
 
         let hash { kf; kinstr; lscope; pot; label } =
-          let extlabel = ExtLogicLabel.from kinstr label in
+          let extlabel = Ext_logic_label.from kinstr label in
           Hashtbl.hash
             (Kf.hash kf,
              basic_kinstr_hash kinstr,
              Lscope.D.hash lscope,
-             PredOrTerm.hash pot,
-             ExtLogicLabel.hash extlabel)
+             Pred_or_term.hash pot,
+             Ext_logic_label.hash extlabel)
 
         let pretty fmt { kf; kinstr; lscope; pot; label } =
-          let extlabel = ExtLogicLabel.from kinstr label in
+          let extlabel = Ext_logic_label.from kinstr label in
           Format.fprintf fmt "@[(%a, %a, %a, %a, %a)@]"
             Kf.pretty kf
             basic_pp_kinstr kinstr
             Lscope.D.pretty lscope
-            PredOrTerm.pretty pot
-            ExtLogicLabel.pretty extlabel
+            Pred_or_term.pretty pot
+            Ext_logic_label.pretty extlabel
       end)
 end

src/plugins/e-acsl/src/analyses/analyses_datatype.mli

@@ -27,9 +27,9 @@ open Analyses_types
 
 module Annotation_kind: Datatype.S with type t = annotation_kind
 
-module PredOrTerm: Datatype.S_with_collections with type t = pred_or_term
+module Pred_or_term: Datatype.S_with_collections with type t = pred_or_term
 
-module AtData: sig
+module At_data: sig
   include Datatype.S_with_collections with type t = at_data
 
   val create:

src/plugins/e-acsl/src/analyses/analyses_types.mli

@@ -37,7 +37,7 @@ type pred_or_term =
   | PoT_term of term
 
 (** Type uniquely representing a [predicate] or [term] with an associated
-    [label], and all the information necessary for its translation. *)
+    [label], and the necessary information for its translation. *)
 type at_data = {
   (** [kernel_function] englobing the [pred_or_term]. *)
   kf: kernel_function;

src/plugins/e-acsl/src/analyses/labels.ml

@@ -58,7 +58,7 @@ let preprocess_done = ref false
 
 (** Associate a statement with the [at_data] that need to be translated on
     this statement. *)
-let at_data_for_stmts: AtData.Set.t ref Stmt.Hashtbl.t =
+let at_data_for_stmts: At_data.Set.t ref Stmt.Hashtbl.t =
   Stmt.Hashtbl.create 17
 
 (** Add [data] to the list of [at_data] that must be translated on the
@@ -69,23 +69,23 @@ let add_at_for_stmt data stmt =
     try
       Stmt.Hashtbl.find at_data_for_stmts stmt
     with Not_found ->
-      let ats_ref = ref AtData.Set.empty in
+      let ats_ref = ref At_data.Set.empty in
       Stmt.Hashtbl.add at_data_for_stmts stmt ats_ref;
       ats_ref
   in
   let old_data =
     try
-      AtData.Set.find data !ats_ref
+      At_data.Set.find data !ats_ref
     with Not_found ->
-      ats_ref := AtData.Set.add data !ats_ref;
+      ats_ref := At_data.Set.add data !ats_ref;
       data
   in
   match old_data.error, data.error with
   | Some _, None ->
     (* Replace the old data that has an error with the new data that do not
        have one. *)
-    ats_ref := AtData.Set.remove old_data !ats_ref;
-    ats_ref := AtData.Set.add data !ats_ref
+    ats_ref := At_data.Set.remove old_data !ats_ref;
+    ats_ref := At_data.Set.add data !ats_ref
   | Some _, Some _
   | None, Some _
   | None, None ->
@@ -97,7 +97,7 @@ let add_at_for_stmt data stmt =
 let at_for_stmt stmt =
   if !preprocess_done then
     let ats_ref =
-      Stmt.Hashtbl.find_def at_data_for_stmts stmt (ref AtData.Set.empty)
+      Stmt.Hashtbl.find_def at_data_for_stmts stmt (ref At_data.Set.empty)
     in
     Result.Ok !ats_ref
   else
@@ -126,10 +126,10 @@ module Process: sig
   end
 
   val term: ?error:exn -> Env.t -> term -> unit
-  (** Traverse the given term to analyse labeled predicates and terms. *)
+  (** Traverse the given term to analyze its labeled predicates and terms. *)
 
   val predicate: ?error:exn -> Env.t -> predicate -> unit
-  (** Traverse the given predicate to analyse the labeled predicates and
+  (** Traverse the given predicate to analyze its labeled predicates and
       terms. *)
 
 end = struct
@@ -177,7 +177,7 @@ end = struct
   (** Analyse the predicate or term [pot] and the label [label] to decide where
       the predicate or term must be translated. *)
   let process ?error env pot label =
-    Env.( (* locally open Env to be able to access the fields of Env.t *)
+    Env.( (* locally open Env to access to the fields of Env.t *)
       let msg s =
         Format.asprintf
           "%s '%a' within %s annotation '%a' in '%a'"
@@ -187,7 +187,7 @@ end = struct
            | Kglobal -> "function"
            | Kstmt _ -> "statement")
           Annotation_kind.pretty env.akind
-          PredOrTerm.pretty pot
+          Pred_or_term.pretty pot
       in
       let error, dest_stmt_opt =
         match env.kinstr, env.akind, label with
@@ -199,7 +199,7 @@ end = struct
           Options.fatal "%s" (msg "invalid use of C label")
 
         (* Assertions *)
-        (* - Pre label corresponds to the first statement of the function *)
+        (* - Pre label corresponding to the first statement of the function *)
         | Kstmt _, Assertion, BuiltinLabel Pre ->
           error, Some (Kernel_function.find_first_stmt env.kf)
         (* - In-place translation for label Here *)
@@ -296,7 +296,7 @@ end = struct
           (* Register the current labeled pred_or_term to the destination
              statement for a later translation *)
           let at =
-            AtData.create ?error env.kf env.kinstr env.lscope pot label
+            At_data.create ?error env.kf env.kinstr env.lscope pot label
           in
           add_at_for_stmt at dest_stmt;
         | None ->
@@ -439,7 +439,7 @@ end = struct
           else begin
             (* We want to process the bounds and the predicate with the same
                environment as the translation (done in [Quantif.convert]). As a
-               result the [lscope] is first built with a [fold_right] on the
+               result, the [lscope] is first built with a [fold_right] on the
                [bound_vars], then once the [lscope] is entirely built, the terms
                of the bounds and the predicate of the goal are analyzed. *)
             let env =
@@ -493,8 +493,8 @@ end = struct
          arguments *)
       let error = do_term ?error env t in
       (* Since we do not know how the labels are used with the arguments,
-         for each argument, register a not_yet error with each label of the
-         function so that each possible combination gracefully raise an error
+         for each argument, register a [Not_yet] error with each label of the
+         function so that each possible combination gracefully raises an error
          to the user. *)
       List.fold_left
         (fun error label -> process ?error env (PoT_term t) label)
@@ -555,10 +555,10 @@ let _debug () =
        Options.feedback ~level:2 "| - stmt %d at %a"
          stmt.sid
          Printer.pp_location (Stmt.loc stmt);
-       AtData.Set.iter
+       At_data.Set.iter
          (fun at ->
             Options.feedback ~level:2 "|    - at %a"
-              AtData.pretty at)
+              At_data.pretty at)
          !ats_ref
     )
     at_data_for_stmts

src/plugins/e-acsl/src/analyses/labels.mli

@@ -35,7 +35,7 @@ val get_first_inner_stmt: stmt -> stmt
 (** If the given statement has a label, return the first statement of the block.
     Otherwise return the given statement. *)
 
-val at_for_stmt: stmt -> AtData.Set.t Error.result
+val at_for_stmt: stmt -> At_data.Set.t Error.result
 (** @return the set of labeled predicates and terms to be translated on the
     given statement.
     @raise Not_memoized if the labels pre-analysis was not run. *)