diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
index 657067711432e4223399316527bd4e45f89b2cff..3033904e011717b1e46f6946859aa84513c9976f 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
+++ b/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
diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.mli b/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
index 3f891afe738b6d4248bfb92b3c219a7f133769c6..097cd6c01dff9a1362159430168823edee7e681d 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
+++ b/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:
diff --git a/src/plugins/e-acsl/src/analyses/analyses_types.mli b/src/plugins/e-acsl/src/analyses/analyses_types.mli
index aff323023bc6f4bf68d29579450e9d6170c3a34a..357f0dda4d19e382bae81bf1ffb09287f0c46da7 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_types.mli
+++ b/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;
diff --git a/src/plugins/e-acsl/src/analyses/labels.ml b/src/plugins/e-acsl/src/analyses/labels.ml
index e56ddca95f70dafd45d8c175cfa952d2d7723298..8e9575002733461d03eebd7226db631b1fec64b1 100644
--- a/src/plugins/e-acsl/src/analyses/labels.ml
+++ b/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
diff --git a/src/plugins/e-acsl/src/analyses/labels.mli b/src/plugins/e-acsl/src/analyses/labels.mli
index 2c10744d8d863b918e4fa27e2c6573ba1f37de11..d122e68b854fcb5109471335b93267db10a3d76a 100644
--- a/src/plugins/e-acsl/src/analyses/labels.mli
+++ b/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. *)