From 5ab440e166ea0021c3278be3895e0093270cc501 Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@cea.fr>
Date: Thu, 19 Aug 2021 17:23:27 +0200
Subject: [PATCH] [e-acsl] Change names of the phase for preprocessing
predicates
---
src/plugins/e-acsl/Makefile.in | 6 +++---
src/plugins/e-acsl/src/analyses/bound_variables.ml | 2 +-
.../{preprocess_predicates.ml => predicate_normalizer.ml} | 2 +-
.../{preprocess_predicates.mli => predicate_normalizer.mli} | 2 +-
src/plugins/e-acsl/src/analyses/preprocess_typing.ml | 4 ++--
src/plugins/e-acsl/src/analyses/typing.ml | 2 +-
src/plugins/e-acsl/src/code_generator/injector.ml | 2 +-
src/plugins/e-acsl/src/code_generator/translate.ml | 2 +-
8 files changed, 11 insertions(+), 11 deletions(-)
rename src/plugins/e-acsl/src/analyses/{preprocess_predicates.ml => predicate_normalizer.ml} (99%)
rename src/plugins/e-acsl/src/analyses/{preprocess_predicates.mli => predicate_normalizer.mli} (97%)
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 9eb2aadfb3e..e3538068d25 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -58,9 +58,9 @@ SRC_PROJECT_INITIALIZER:=\
# analyses
SRC_ANALYSES:= \
rte \
- lscope \
- preprocess_predicates \
- bound_variables \
+ lscope \
+ predicate_normalizer \
+ bound_variables \
interval \
typing \
preprocess_typing \
diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml
index 663b0d3d72b..a978dc8ea11 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 Preprocess_predicates.get_preprocessed_form p with
+ match Predicate_normalizer.get 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/preprocess_predicates.ml b/src/plugins/e-acsl/src/analyses/predicate_normalizer.ml
similarity index 99%
rename from src/plugins/e-acsl/src/analyses/preprocess_predicates.ml
rename to src/plugins/e-acsl/src/analyses/predicate_normalizer.ml
index ae6c7883d38..d502eb22fa4 100644
--- a/src/plugins/e-acsl/src/analyses/preprocess_predicates.ml
+++ b/src/plugins/e-acsl/src/analyses/predicate_normalizer.ml
@@ -156,4 +156,4 @@ let preprocess_annot annot =
let preprocess_predicate p =
ignore (Visitor.visitFramacPredicate preprocessor p)
-let get_preprocessed_form p = Memo.get p
+let get p = Memo.get p
diff --git a/src/plugins/e-acsl/src/analyses/preprocess_predicates.mli b/src/plugins/e-acsl/src/analyses/predicate_normalizer.mli
similarity index 97%
rename from src/plugins/e-acsl/src/analyses/preprocess_predicates.mli
rename to src/plugins/e-acsl/src/analyses/predicate_normalizer.mli
index b42ab2ca379..7e280a6b32f 100644
--- a/src/plugins/e-acsl/src/analyses/preprocess_predicates.mli
+++ b/src/plugins/e-acsl/src/analyses/predicate_normalizer.mli
@@ -41,5 +41,5 @@ val preprocess_annot : code_annotation -> unit
val preprocess_predicate : predicate -> unit
(** Preprocess a predicate and its children and store the results *)
-val get_preprocessed_form : predicate -> Lscope.pred_or_term
+val get : predicate -> Lscope.pred_or_term
(** Retrieve the preprocessed form of a predicate *)
diff --git a/src/plugins/e-acsl/src/analyses/preprocess_typing.ml b/src/plugins/e-acsl/src/analyses/preprocess_typing.ml
index d4292aa3f6b..90ba5ff1f6f 100644
--- a/src/plugins/e-acsl/src/analyses/preprocess_typing.ml
+++ b/src/plugins/e-acsl/src/analyses/preprocess_typing.ml
@@ -187,11 +187,11 @@ let type_code_annot lenv annot =
ignore (Visitor.visitFramacCodeAnnotation (typer_visitor lenv) annot)
let preprocess_predicate lenv p =
- Preprocess_predicates.preprocess_predicate p;
+ Predicate_normalizer.preprocess_predicate p;
Bound_variables.preprocess_predicate p;
ignore (Visitor.visitFramacPredicate (typer_visitor lenv) p)
let preprocess_rte ~lenv rte =
- Preprocess_predicates.preprocess_annot rte;
+ Predicate_normalizer.preprocess_annot rte;
Bound_variables.preprocess_annot rte;
type_code_annot lenv rte
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index 3f14ead29ac..0ceb31ebeff 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -795,7 +795,7 @@ and type_bound_variables ~loc ~lenv (t1, lv, t2) =
and type_predicate ?(lenv=[]) p =
- match Preprocess_predicates.get_preprocessed_form p with
+ match Predicate_normalizer.get p with
| PoT_term t -> type_term ~use_gmp_opt:true ~lenv t
| PoT_pred p ->
Cil.CurrentLoc.set p.pred_loc;
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index 36dc3d86838..af0cc8b0633 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -868,7 +868,7 @@ let inject () =
Options.feedback ~level:2
"preprocessing annotations in project %a"
Project.pretty current_project;
- Preprocess_predicates.preprocess ast;
+ Predicate_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 3297bd317cc..246079281d9 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -1223,7 +1223,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 Preprocess_predicates.get_preprocessed_form p with
+ match Predicate_normalizer.get p with
| PoT_term t -> term_to_exp kf env t
| PoT_pred p ->
let rte = match rte with None -> Env.generate_rte env | Some b -> b in
--
GitLab