From 8669a7d410c723fda97143093a1f2ebe6cb15c18 Mon Sep 17 00:00:00 2001
From: thibautbenjamin <thibaut.benjamin@polytechnique.edu>
Date: Mon, 19 Jul 2021 14:53:40 +0200
Subject: [PATCH] [e-acsl] creation of a preprocessing phase for typing
---
src/plugins/e-acsl/Makefile.in | 9 +--
.../e-acsl/src/analyses/preprocess_typing.ml | 63 +++++++++++++++++++
.../e-acsl/src/analyses/preprocess_typing.mli | 5 ++
.../e-acsl/src/code_generator/injector.ml | 1 +
4 files changed, 74 insertions(+), 4 deletions(-)
create mode 100644 src/plugins/e-acsl/src/analyses/preprocess_typing.ml
create mode 100644 src/plugins/e-acsl/src/analyses/preprocess_typing.mli
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 5aab9fbc89d..0d9786c27d7 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -58,13 +58,14 @@ SRC_PROJECT_INITIALIZER:=\
# analyses
SRC_ANALYSES:= \
rte \
+ bound_variables \
+ interval \
+ typing \
+ preprocess_typing \
literal_strings \
memory_tracking \
exit_points \
- lscope \
- interval \
- typing \
- bound_variables
+ lscope
SRC_ANALYSES:=$(addprefix src/analyses/, $(SRC_ANALYSES))
# code generator
diff --git a/src/plugins/e-acsl/src/analyses/preprocess_typing.ml b/src/plugins/e-acsl/src/analyses/preprocess_typing.ml
new file mode 100644
index 00000000000..d76bf406d2a
--- /dev/null
+++ b/src/plugins/e-acsl/src/analyses/preprocess_typing.ml
@@ -0,0 +1,63 @@
+let typer_visitor = object
+ inherit Visitor.frama_c_inplace
+
+ (* Nothing to type in global annotations *)
+ method !vannotation _ = Cil.SkipChildren
+
+ (* Only type the globals that do not come from the Rtl *)
+ method !vglob_aux =
+ function
+ (* library functions and built-ins *)
+ | GVarDecl(vi, _) | GVar(vi, _, _)
+ | GFunDecl(_, vi, _) | GFun({ svar = vi }, _) when Builtins.mem vi.vname ->
+ Options.feedback "ignoring builtin";
+ Cil.SkipChildren
+
+ | GVarDecl(vi, _) | GVar(vi, _, _) | GFun({ svar = vi }, _)
+ when Misc.is_fc_or_compiler_builtin vi ->
+ Options.feedback "ignoring fc_or_compiler_builtin %a" Printer.pp_varinfo vi;
+ Cil.SkipChildren
+ | g when Rtl.Symbols.mem_global g ->
+ Options.feedback "ignoring rtl %a" Printer.pp_global g;
+ Cil.SkipChildren
+
+ (* generated function declaration: nothing to do *)
+ | GFunDecl(_, vi, _) when Misc.is_fc_stdlib_generated vi ->
+ Options.feedback "ignoring stdlib generated";
+ Cil.SkipChildren
+
+ (* other globals: nothing to do *)
+ | GType _
+ | GCompTag _
+ | GCompTagDecl _
+ | GEnumTag _
+ | GEnumTagDecl _
+ | GAsm _
+ | GPragma _
+ | GText _
+ -> Cil.SkipChildren
+
+<<<<<<< variant A
+ | _ -> Cil.DoChildren
+>>>>>>> variant B
+ method !vpredicate p =
+ Error.generic_handle (Typing.type_named_predicate ~lenv) () p;
+ Cil.SkipChildren
+
+ method !vspec spec =
+ List.iter (fun b -> (List.iter (fun p -> ignore (Visitor.visitFramacIdPredicate self p)) b.b_assumes)) spec.spec_behavior;
+ List.iter (type_requires self (Option.get self#current_kf) (self#current_kinstr)) spec.spec_behavior;
+ List.iter (type_post_conditions self (Option.get self#current_kf) self#current_kinstr) spec.spec_behavior;
+ Cil.SkipChildren
+======= end
+
+ method !vpredicate p = Typing.type_named_predicate p; Cil.DoChildren
+
+end
+
+
+let type_program ast =
+ Visitor.visitFramacFileSameGlobals typer_visitor ast
+
+let type_code_annot annot =
+ ignore (Visitor.visitFramacCodeAnnotation typer_visitor annot)
diff --git a/src/plugins/e-acsl/src/analyses/preprocess_typing.mli b/src/plugins/e-acsl/src/analyses/preprocess_typing.mli
new file mode 100644
index 00000000000..bea11954655
--- /dev/null
+++ b/src/plugins/e-acsl/src/analyses/preprocess_typing.mli
@@ -0,0 +1,5 @@
+open Cil_types
+
+val type_program : file -> unit
+
+val type_code_annot : code_annotation -> unit
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index d43acb78c5b..275d229ff01 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -864,6 +864,7 @@ let inject () =
Project.pretty (Project.current ());
Gmp_types.init ();
let ast = Ast.get () in
+ Preprocess_typing.type_program ast;
inject_in_file ast;
reset_all ast;
--
GitLab