From 6cb5e8c8e2838faaabc6e7b391c858f8ccd7dedb Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@cea.fr>
Date: Wed, 13 Oct 2021 10:43:46 +0200
Subject: [PATCH] [e-acsl] rename file
---
src/plugins/e-acsl/Makefile.in | 2 +-
src/plugins/e-acsl/headers/header_spec.txt | 4 ++--
src/plugins/e-acsl/src/analyses/bound_variables.ml | 2 +-
.../{predicate_normalizer.ml => logic_normalizer.ml} | 0
.../{predicate_normalizer.mli => logic_normalizer.mli} | 0
src/plugins/e-acsl/src/analyses/typing.ml | 8 ++++----
src/plugins/e-acsl/src/code_generator/injector.ml | 4 ++--
src/plugins/e-acsl/src/code_generator/translate.ml | 4 ++--
8 files changed, 12 insertions(+), 12 deletions(-)
rename src/plugins/e-acsl/src/analyses/{predicate_normalizer.ml => logic_normalizer.ml} (100%)
rename src/plugins/e-acsl/src/analyses/{predicate_normalizer.mli => logic_normalizer.mli} (100%)
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 621b258f44d..dfb8d49cd2d 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 9f014a0a1ab..b8d2e280542 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 7e450eb7158..9ca2a162568 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 f7159b31556..95c9189b0e6 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 23e1965ce62..5964cedbcf0 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 618d4751d6a..b0c3d6a1339 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
--
GitLab