diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 621b258f44d25e98be761f865c2be7fd0e6dbd39..dfb8d49cd2d416643ce6cd900aabc9db78ca8bcd 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -59,7 +59,7 @@ SRC_PROJECT_INITIALIZER:=\
SRC_ANALYSES:= \
rte \
lscope \
- predicate_normalizer \
+ logic_normalizer \
bound_variables \
interval \
typing \
diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
index 9f014a0a1abe4040f1804d2d5e5caf67ca31ce72..b8d2e280542e4eac9613125cd9c987eed033eb6e 100644
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ b/src/plugins/e-acsl/headers/header_spec.txt
@@ -76,11 +76,11 @@ src/analyses/interval.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/interval.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/literal_strings.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/literal_strings.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/analyses/predicate_normalizer.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/analyses/predicate_normalizer.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/lscope.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/lscope.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/memory_tracking.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/predicate_normalizer.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/predicate_normalizer.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/memory_tracking.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/rte.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/rte.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml
index 7e450eb7158254f94101c07eeae896c709e4f44e..9ca2a162568d089f09e9f94cbfc5eab49fd7eeaf 100644
--- a/src/plugins/e-acsl/src/analyses/bound_variables.ml
+++ b/src/plugins/e-acsl/src/analyses/bound_variables.ml
@@ -731,7 +731,7 @@ end
method !vpredicate p =
let loc = p.pred_loc in
- match Predicate_normalizer.get_pred p with
+ match Logic_normalizer.get_pred p with
| PoT_pred p -> Error.generic_handle (process_quantif ~loc) () p;
Cil.DoChildren
| PoT_term _ -> Cil.DoChildren
diff --git a/src/plugins/e-acsl/src/analyses/predicate_normalizer.ml b/src/plugins/e-acsl/src/analyses/logic_normalizer.ml
similarity index 100%
rename from src/plugins/e-acsl/src/analyses/predicate_normalizer.ml
rename to src/plugins/e-acsl/src/analyses/logic_normalizer.ml
diff --git a/src/plugins/e-acsl/src/analyses/predicate_normalizer.mli b/src/plugins/e-acsl/src/analyses/logic_normalizer.mli
similarity index 100%
rename from src/plugins/e-acsl/src/analyses/predicate_normalizer.mli
rename to src/plugins/e-acsl/src/analyses/logic_normalizer.mli
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index f7159b3155643e61e0cca75a5c33924ed7bfdbb1..95c9189b0e62dc9954a7b1d94137f3f211996b60 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -677,7 +677,7 @@ let rec type_term
| Ttype _
| Tempty_set -> dup Nan
in
- let t = Predicate_normalizer.get_term t in
+ let t = Logic_normalizer.get_term t in
Memo.memo ~lenv
(fun t ->
let ty, op = infer t in
@@ -806,7 +806,7 @@ and type_bound_variables ~loc ~lenv (t1, lv, t2) =
(t1, lv, t2)
and type_predicate ?(lenv=[]) p =
- match Predicate_normalizer.get_pred p with
+ match Logic_normalizer.get_pred p with
| PoT_term t -> type_term ~use_gmp_opt:true ~lenv t
| PoT_pred p ->
Cil.CurrentLoc.set p.pred_loc;
@@ -1016,12 +1016,12 @@ let type_code_annot lenv annot =
ignore (Visitor.visitFramacCodeAnnotation (typer_visitor lenv) annot)
let preprocess_predicate lenv p =
- Predicate_normalizer.preprocess_predicate p;
+ Logic_normalizer.preprocess_predicate p;
Bound_variables.preprocess_predicate p;
ignore (Visitor.visitFramacPredicate (typer_visitor lenv) p)
let preprocess_rte ~lenv rte =
- Predicate_normalizer.preprocess_annot rte;
+ Logic_normalizer.preprocess_annot rte;
Bound_variables.preprocess_annot rte;
type_code_annot lenv rte
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index 23e1965ce624983cfe2fdabf4e2e86afc1d35587..5964cedbcf0f2e4f2bda5df6a81fad34446385c4 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -852,7 +852,7 @@ let reset_all ast =
Literal_strings.reset ();
Global_observer.reset ();
Bound_variables.clear_guards ();
- Predicate_normalizer.clear ();
+ Logic_normalizer.clear ();
Typing.clear ();
(* reset some kernel states: *)
(* reset the CFG that has been heavily modified by the code generation step *)
@@ -869,7 +869,7 @@ let inject () =
Options.feedback ~level:2
"preprocessing annotations in project %a"
Project.pretty current_project;
- Predicate_normalizer.preprocess ast;
+ Logic_normalizer.preprocess ast;
Options.feedback ~level:2
"normalizing quantifiers in project %a"
Project.pretty current_project;
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 618d4751d6a4401ceda25908c0816c71b6e0ff17..b0c3d6a1339d342555305618a54b60683025d3f1 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -853,7 +853,7 @@ and term_to_exp ~adata kf env t =
environment '%a'"
Printer.pp_term t generate_rte Typing.Function_params_ty.pretty
(Env.Local_vars.get env);
- let t = Predicate_normalizer.get_term t in
+ let t = Logic_normalizer.get_term t in
Extlib.flatten
(Env.with_rte_and_result env false
~f:(fun env ->
@@ -1225,7 +1225,7 @@ and predicate_content_to_exp ~adata ?name kf env p =
| Pfresh _ -> Env.not_yet env "\\fresh"
and predicate_to_exp ~adata ?name kf ?rte env p =
- match Predicate_normalizer.get_pred p with
+ match Logic_normalizer.get_pred p with
| PoT_term t -> term_to_exp ~adata kf env t
| PoT_pred p ->
let rte = match rte with None -> Env.generate_rte env | Some b -> b in