From 8d82ee5f02e19514f7cee6c048b97bd06325c65e Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 4 Aug 2014 15:22:18 +0200
Subject: [PATCH] changelog + few comments + coding style
---
src/plugins/e-acsl/doc/Changelog | 2 ++
src/plugins/e-acsl/visit.ml | 10 ++++++++--
2 files changed, 10 insertions(+), 2 deletions(-)
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 7734389a2c9..b1513262cd7 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,8 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
+-* E-ACSL [2014/07/08] Fix bug about using some part of the
+ (Frama-C) libc which prevents linking of the generated C code.
-* E-ACSL [2014/07/19] Fix bug #1836 about one-off error when
computing the block which a pointer points to.
-* E-ACSL [2014/07/08] Fix bug about using some part of the
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 12755400d94..2486578f1fc 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -76,7 +76,12 @@ class e_acsl_visitor prj generate = object (self)
(if generate then Cil.copy_visit prj else Cil.inplace_visit ())
val mutable main_fct = None
+ (* fundec of the main entry point, in the new project [prj].
+ [None] while the global corresponding to this fundec has not been
+ visited *)
+
val mutable keep_initializer = None
+
val global_vars: init option Varinfo.Hashtbl.t = Varinfo.Hashtbl.create 7
(* keys belong to the original project while values belong to the new one *)
@@ -224,10 +229,11 @@ class e_acsl_visitor prj generate = object (self)
let build_args_initializer () =
let main = Extlib.the main_fct in
let loc = Location.unknown in
- let args = (List.map Cil.evar main.sformals) in
+ let args = List.map Cil.evar main.sformals in
let call = Misc.mk_call loc "__init_args" args in
main.sbody.bstmts <- call :: main.sbody.bstmts;
- in Project.on prj build_args_initializer ();
+ in
+ Project.on prj build_args_initializer ()
end;
(* reset copied states at the end to be observationally
equivalent to a standard visitor. *)
--
GitLab