Skip to content
Snippets Groups Projects
Commit 8d82ee5f authored by Julien Signoles's avatar Julien Signoles
Browse files

changelog + few comments + coding style

parent 07f1261f
No related branches found
No related tags found
No related merge requests found
...@@ -15,6 +15,8 @@ ...@@ -15,6 +15,8 @@
# E-ACSL: the Whole E-ACSL plug-in # 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 -* E-ACSL [2014/07/19] Fix bug #1836 about one-off error when
computing the block which a pointer points to. computing the block which a pointer points to.
-* E-ACSL [2014/07/08] Fix bug about using some part of the -* E-ACSL [2014/07/08] Fix bug about using some part of the
......
...@@ -76,7 +76,12 @@ class e_acsl_visitor prj generate = object (self) ...@@ -76,7 +76,12 @@ class e_acsl_visitor prj generate = object (self)
(if generate then Cil.copy_visit prj else Cil.inplace_visit ()) (if generate then Cil.copy_visit prj else Cil.inplace_visit ())
val mutable main_fct = None 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 mutable keep_initializer = None
val global_vars: init option Varinfo.Hashtbl.t = Varinfo.Hashtbl.create 7 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 *) (* 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) ...@@ -224,10 +229,11 @@ class e_acsl_visitor prj generate = object (self)
let build_args_initializer () = let build_args_initializer () =
let main = Extlib.the main_fct in let main = Extlib.the main_fct in
let loc = Location.unknown 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 let call = Misc.mk_call loc "__init_args" args in
main.sbody.bstmts <- call :: main.sbody.bstmts; main.sbody.bstmts <- call :: main.sbody.bstmts;
in Project.on prj build_args_initializer (); in
Project.on prj build_args_initializer ()
end; end;
(* reset copied states at the end to be observationally (* reset copied states at the end to be observationally
equivalent to a standard visitor. *) equivalent to a standard visitor. *)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment