[e-acsl] rename ExtLogicLabel.from to ExtLogicLabel.get

[e-acsl] fixing comments

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

@@ -93,9 +93,11 @@ module Pred_or_term =
 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
+  val get: kinstr -> logic_label -> logic_label * stmt option
   (** @return an extended logic label from a [kinstr] and a [logic_label]. *)
+
 end = struct
+
   include Datatype.Pair_with_collections
       (Logic_label)
       (Datatype.Option_with_collections
@@ -105,8 +107,8 @@ end = struct
          end))
       (struct let module_name = "E_ACSL.Labels.Ext_logic_label" end)
 
-  (* Override [pretty] to print a more compact representation of [Ext_logic_label]
-     for debugging purposes. *)
+  (* 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
     | Some from_stmt ->
@@ -118,7 +120,7 @@ end = struct
       Format.fprintf fmt "%a"
         Logic_label.pretty label
 
-  let from kinstr label =
+  let get kinstr label =
     let from_stmt_opt =
       match kinstr, label with
       | Kglobal, _
@@ -135,6 +137,7 @@ end = struct
       | Kstmt s, BuiltinLabel (Old | Post) -> Some s
     in
     label, from_stmt_opt
+
 end
 
 (** Basic printer for a [kinstr]. Contrary to [Cil_datatype.Kinstr.pretty], the
@@ -219,29 +222,29 @@ module At_data = struct
             else cmp
           in
           if cmp = 0 then
-            let extlabel1 = Ext_logic_label.from kinstr1 label1 in
-            let extlabel2 = Ext_logic_label.from kinstr2 label2 in
-            Ext_logic_label.compare extlabel1 extlabel2
+            let elabel1 = Ext_logic_label.get kinstr1 label1 in
+            let elabel2 = Ext_logic_label.get kinstr2 label2 in
+            Ext_logic_label.compare elabel1 elabel2
           else cmp
 
         let equal = Datatype.from_compare
 
         let hash { kf; kinstr; lscope; pot; label } =
-          let extlabel = Ext_logic_label.from kinstr label in
+          let elabel = Ext_logic_label.get kinstr label in
           Hashtbl.hash
             (Kf.hash kf,
              basic_kinstr_hash kinstr,
              Lscope.D.hash lscope,
              Pred_or_term.hash pot,
-             Ext_logic_label.hash extlabel)
+             Ext_logic_label.hash elabel)
 
         let pretty fmt { kf; kinstr; lscope; pot; label } =
-          let extlabel = Ext_logic_label.from kinstr label in
+          let elabel = Ext_logic_label.get kinstr label in
           Format.fprintf fmt "@[(%a, %a, %a, %a, %a)@]"
             Kf.pretty kf
             basic_pp_kinstr kinstr
             Lscope.D.pretty lscope
             Pred_or_term.pretty pot
-            Ext_logic_label.pretty extlabel
+            Ext_logic_label.pretty elabel
       end)
 end

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

@@ -232,20 +232,23 @@ class visitor cat
       | None -> None
 
     (* see documentation in e_acsl_visitor.mli *)
-    method visit: 'a 'b. ?vcode_annot:bool -> ?vspec:bool -> (Visitor.frama_c_visitor -> 'a -> 'b) -> 'a -> 'b =
-      fun ?vcode_annot ?vspec visit_func item ->
-      let old_run_from_visitor = self#set_run_from_visitor true in
-      let old_vcode_annot = self#set_do_visit_code_annot vcode_annot in
-      let old_vfunspec = self#set_do_visit_funspec vspec in
-      let finally () =
-        ignore @@ self#set_do_visit_code_annot old_vcode_annot;
-        ignore @@ self#set_do_visit_funspec old_vfunspec;
-        ignore @@ self#set_run_from_visitor old_run_from_visitor
-      in
-      Extlib.try_finally
-        ~finally
-        (fun item -> visit_func (self :> Visitor.frama_c_inplace) item)
-        item
+    method visit
+      : 'a 'b. ?vcode_annot:bool -> ?vspec:bool
+        -> (Visitor.frama_c_visitor -> 'a -> 'b)
+        -> 'a -> 'b
+      = fun ?vcode_annot ?vspec visit_func item ->
+        let old_run_from_visitor = self#set_run_from_visitor true in
+        let old_vcode_annot = self#set_do_visit_code_annot vcode_annot in
+        let old_vfunspec = self#set_do_visit_funspec vspec in
+        let finally () =
+          ignore @@ self#set_do_visit_code_annot old_vcode_annot;
+          ignore @@ self#set_do_visit_funspec old_vfunspec;
+          ignore @@ self#set_run_from_visitor old_run_from_visitor
+        in
+        Extlib.try_finally
+          ~finally
+          (fun item -> visit_func (self :> Visitor.frama_c_inplace) item)
+          item
 
     (** see documentation in e_acsl_visitor.mli *)
     method visit_file file =
@@ -310,7 +313,7 @@ class visitor cat
 
     (** [do_with ?not_yet ?akind ~f arg] changes the visit error to [not_yet]
         and changes the annotation kind to [akind] if provided, then execute
-        [f arg]. Finally, it restore the visit error and annotation kind to
+        [f arg]. Finally, it restores the visit error and annotation kind to
         their old values and returns the result of [f arg]. *)
     method private do_with: 'a 'b.
       ?not_yet:string ->
@@ -356,10 +359,10 @@ class visitor cat
                         self#visit_id_predicate requires))
              bhv.b_requires;
            (* The links between the [identified_property]s and the [assigns] or
-              [allocates] clauses are not clear. For now store a [not_yet] error
-              for every term of the clauses. Update the code to add the relevant
-              [must_translate] calls once the [assigns] or [allocates] clauses
-              translation are supported. *)
+              [allocates] clauses are not clear. For now, store a [not_yet]
+              error for every term of the clauses. Update the code to add the
+              relevant [must_translate] calls once the [assigns] or [allocates]
+              clauses translation are supported. *)
            self#do_with
              ~akind:Postcondition
              ~not_yet:"assigns clause in behavior"
@@ -433,7 +436,7 @@ class visitor cat
       let kf = Option.get self#current_kf in
 
       if Kernel_function.is_first_stmt kf stmt then begin
-        (* Analyse the specification on the function on the first statement *)
+        (* Analyze the funspec before visiting the first statement *)
         if Annotations.has_funspec kf then begin
           let old_kinstr_stmts = self#set_global_kinstr () in
           self#process_spec (Annotations.funspec kf);
@@ -441,7 +444,7 @@ class visitor cat
         end
       end;
 
-      (* Analyse the specification on the current statement *)
+      (* Analyze the code annotation of the current statement *)
       Annotations.iter_code_annot
         (fun _ annot ->
            (* Reset the visit error before starting to analyze an annotation. *)

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

@@ -57,20 +57,19 @@ val case_globals :
     [new visitor cat] creates a visitor with [cat] as the category to use for
     the [Error] module in the visitor.
 
-    For the root of the AST, no the globals level, only visit the cases that are
-    relevant to E-ACSL. Each case is handled by a method of the visitor. The
+    For the root of the AST, not the global level, only visit the cases that
+    are relevant to E-ACSL. Each case is handled by a method of the visitor. The
     cases are similar, and similarly named as the ones of the function
     [case_globals].
 
-    For the rest of the AST, the kind of annotation visited is recorded and
-    accessible through the method [get_akind]. While visiting annotations
+    For the rest of the AST, the kind of the visited annotation is recorded and
+    accessed through the method [get_akind]. While visiting annotations
     currently not supported by E-ACSL, the [get_visit_error] returns a [not_yet]
-    exception detailing the error. The actual visitor inheriting from
-    [E_acsl_visitor.visitor] can then continue its processing or not as it sees
-    fit.
+    exception. Any visitor that inherits from [E_acsl_visitor.visitor] can
+    decide wether continue its processing or not as it sees fit.
 
     As a result of the custom visit of the AST, the methods [vcode_annot] and
-    [vspec] skip their children since they are already visited by [vstmt_aux].
+    [vspec] skip their children, since they are already visited by [vstmt_aux].
     Be sure to use the method [visit] (and associated methods) if you need to
     visit the children of those nodes.
 
@@ -137,3 +136,9 @@ class visitor :
 val must_translate_ppt_ref: (Property.t -> bool) ref
 
 val must_translate_ppt_opt_ref: (Property.t option -> bool) ref
+
+(*
+Local Variables:
+compile-command: "make -C ../../../../.."
+End:
+*)