From f5b131fe353566ebb440a220fea97002e8f872b9 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 10 Aug 2020 17:55:12 +0200
Subject: [PATCH] [e-acsl] remove the main visitor in Prepare_ast in order to
propagate property statuses soundly [e-acsl] simplify and document
Prepare_ast a bit more
---
.../src/project_initializer/prepare_ast.ml | 595 ++++++++----------
1 file changed, 274 insertions(+), 321 deletions(-)
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
index 29f4c1df264..2b01ed8d9a8 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
@@ -21,6 +21,7 @@
(**************************************************************************)
open Cil_types
+open Cil_datatype
let dkey = Options.dkey_prepare
@@ -28,81 +29,69 @@ let dkey = Options.dkey_prepare
(* Environment *)
(* ********************************************************************** *)
-let fct_tbl: unit Kernel_function.Hashtbl.t = Kernel_function.Hashtbl.create 7
-
-(* The purpose of [actions] is similar to the Frama-C visitor's
- [get_filling_actions] but we need to fill it outside the visitor. So it is
- our own version. *)
-let actions = Queue.create ()
-
-(* global table for ensuring that logic info are not shared between a function
- definition and its duplicate *)
-module Global: sig
- val add_logic_info: logic_info -> unit
- val mem_logic_info: logic_info -> bool
+module Dup_functions: sig
+ val generate_vi: varinfo -> varinfo (* return the new varinfo *)
+ val mem: varinfo -> bool
+ val find: varinfo -> varinfo
val reset: unit -> unit
end = struct
- let tbl = Cil_datatype.Logic_info.Hashtbl.create 7
- let add_logic_info x = Cil_datatype.Logic_info.Hashtbl.add tbl x ()
- let mem_logic_info x = Cil_datatype.Logic_info.Hashtbl.mem tbl x
- let reset () = Cil_datatype.Logic_info.Hashtbl.clear tbl
+ let tbl: varinfo Varinfo.Hashtbl.t = Varinfo.Hashtbl.create 7
+
+ (* assume [vi] is not already in [tbl] *)
+ let generate_vi vi =
+ let new_name = Functions.RTL.mk_gen_name vi.vname in
+ let new_vi =
+ Cil.makeGlobalVar
+ ~referenced:vi.vreferenced
+ ~loc:vi.vdecl
+ new_name
+ vi.vtype
+ in
+ Varinfo.Hashtbl.add tbl vi new_vi;
+ new_vi
-end
+ let mem = Varinfo.Hashtbl.mem tbl
+ let find = Varinfo.Hashtbl.find tbl
+ let reset () = Varinfo.Hashtbl.clear tbl
-let reset () =
- Kernel_function.Hashtbl.clear fct_tbl;
- Global.reset ();
- Queue.clear actions
+end
(* ********************************************************************** *)
(* Duplicating a function *)
(* ********************************************************************** *)
-(* [tbl] associates the old formals to the new ones *)
-let dup_funspec tbl bhv spec =
+(* [formals] associates the old formals to the new ones in order to
+ substitute them in [spec]. *)
+let dup_funspec formals spec =
(* Options.feedback "DUP SPEC %a" Cil.d_funspec spec;*)
let o = object
- inherit Cil.genericCilVisitor bhv
-
- val already_visited = Cil_datatype.Logic_var.Hashtbl.create 7
-
- method !vlogic_info_use li =
- if Global.mem_logic_info li then
- Cil.ChangeDoChildrenPost
- ({ li with l_var_info = li.l_var_info } (* force a copy *),
- Visitor_behavior.Get.logic_info bhv)
- else
- Cil.JustCopy
+ inherit Visitor.frama_c_refresh (Project.current ())
- method !vterm_offset _ =
- Cil.DoChildrenPost
- (function (* no way to directly visit fieldinfo and model_info uses *)
- | TField(fi, off) ->
- TField(Visitor_behavior.Get.fieldinfo bhv fi, off)
- | TModel(mi, off) ->
- TModel(Visitor_behavior.Get.model_info bhv mi, off)
- | off ->
- off)
+ val already_visited = Logic_var.Hashtbl.create 7
+ (* just substituting in [!vvrbl] (when using a varinfo) does not work
+ because varinfo's occurrences are shared in logic_vars, so modifying the
+ varinfo would modify any logic_var based on it, even if it is not part of
+ this [spec] (e.g., if it is in another annotation of the same
+ function) *)
method !vlogic_var_use orig_lvi =
match orig_lvi.lv_origin with
| None ->
Cil.JustCopy
| Some vi ->
try
- let new_lvi =
- Cil_datatype.Logic_var.Hashtbl.find already_visited orig_lvi
- in
+ let new_lvi = Logic_var.Hashtbl.find already_visited orig_lvi in
+ (* recreate sharing of the logic_var in this [spec] *)
Cil.ChangeTo new_lvi
with Not_found ->
+ (* first time visiting this logic var *)
Cil.ChangeDoChildrenPost
({ orig_lvi with lv_id = orig_lvi.lv_id } (* force a copy *),
fun lvi ->
try
- let new_vi = Cil_datatype.Varinfo.Hashtbl.find tbl vi in
- Cil_datatype.Logic_var.Hashtbl.add
- already_visited orig_lvi lvi;
+ let new_vi = Varinfo.Hashtbl.find formals vi in
+ Logic_var.Hashtbl.add already_visited orig_lvi lvi;
(* [lvi] is the logic counterpart of a formal varinfo that has
been replaced by a new one: propagate this change *)
lvi.lv_id <- new_vi.vid;
@@ -112,20 +101,12 @@ let dup_funspec tbl bhv spec =
lvi
with Not_found ->
assert vi.vglob;
- (* using [Visitor_behavior.Get.logic_var bhv lvi] is correct
- only because the lv_id used to compare the lvi does not
- change between the original one and this copy *)
- Visitor_behavior.Get.logic_var bhv lvi)
-
- method !videntified_term _ =
- Cil.DoChildrenPost Logic_const.refresh_identified_term
+ lvi)
- method !videntified_predicate _ =
- Cil.DoChildrenPost Logic_const.refresh_predicate
end in
- Cil.visitCilFunspec o spec
+ Cil.visitCilFunspec (o :> Cil.cilVisitor) spec
-let dup_fundec loc spec bhv sound_verdict_vi kf vi new_vi =
+let dup_fundec loc spec sound_verdict_vi kf vi new_vi =
new_vi.vdefined <- true;
let formals = Kernel_function.get_formals kf in
let mk_formal vi =
@@ -174,9 +155,9 @@ let dup_fundec loc spec bhv sound_verdict_vi kf vi new_vi =
let locals = match res with None -> [] | Some r -> [ r ] in
let body = Cil.mkBlock stmts in
body.blocals <- locals;
- let tbl = Cil_datatype.Varinfo.Hashtbl.create 7 in
- List.iter2 (Cil_datatype.Varinfo.Hashtbl.add tbl) formals new_formals;
- let new_spec = dup_funspec tbl bhv spec in
+ let tbl = Varinfo.Hashtbl.create 7 in
+ List.iter2 (Varinfo.Hashtbl.add tbl) formals new_formals;
+ let new_spec = dup_funspec tbl spec in
let fundec =
{ svar = new_vi;
sformals = new_formals;
@@ -192,54 +173,69 @@ let dup_fundec loc spec bhv sound_verdict_vi kf vi new_vi =
Cfg.cfgFun fundec;
fundec
-let dup_global loc actions spec bhv sound_verdict_vi kf vi new_vi =
+let dup_global loc spec sound_verdict_vi kf vi new_vi =
let name = vi.vname in
Options.feedback ~dkey ~level:2 "entering in function %s" name;
- let fundec = dup_fundec loc spec bhv sound_verdict_vi kf vi new_vi in
- let fct = Definition(fundec, loc) in
- let new_spec = fundec.sspec in
- let new_kf = { fundec = fct; spec = new_spec } in
- Queue.add
- (fun () ->
- Kernel_function.Hashtbl.add fct_tbl new_kf ();
- Globals.Functions.register new_kf;
- Globals.Functions.replace_by_definition new_spec fundec loc;
- Annotations.register_funspec new_kf;
- if new_vi.vname = "main" then begin
- (* recompute the info about the old main since its name has changed;
- see the corresponding part in the main visitor *)
- Globals.Functions.remove vi;
- Globals.Functions.register kf
- end)
- actions;
- (* remove the specs attached to the previous kf iff it is a definition:
- it is necessary to keep stable the number of annotations in order to get
- [Keep_status] working fine. *)
- let kf = Visitor_behavior.Get.kernel_function bhv kf in
+ let new_fundec = dup_fundec loc spec sound_verdict_vi kf vi new_vi in
+ let new_fct = Definition(new_fundec, loc) in
+ let new_spec = new_fundec.sspec in
+ let new_kf = { fundec = new_fct; spec = new_spec } in
+ Globals.Functions.register new_kf;
+ Globals.Functions.replace_by_definition new_spec new_fundec loc;
+ Annotations.register_funspec new_kf;
+ if Datatype.String.equal new_vi.vname "main" then begin
+ (* recompute kernel's info about the old main since its name has changed;
+ see the corresponding part in the main visitor *)
+ Globals.Functions.remove vi;
+ Globals.Functions.register kf
+ end;
+ (* copy property statuses to the new spec *)
+ let copy old_ip new_ip =
+ let open Property_status in
+ let cp status ep =
+ let e = Emitter.Usable_emitter.get ep.emitter in
+ if ep.logical_consequence
+ then logical_consequence e new_ip ep.properties
+ else emit e new_ip ~hyps:ep.properties status
+ in
+ match get old_ip with
+ | Never_tried ->
+ ()
+ | Best(s, epl) ->
+ List.iter (cp s) epl
+ | Inconsistent icst ->
+ List.iter (cp True) icst.valid;
+ (* either the program is reachable and [False_and_reachable] is
+ fine, or the program point is not reachable and it does not
+ matter for E-ACSL that checks it at runtime. *)
+ List.iter (cp False_and_reachable) icst.invalid
+ in
+ let ips kf s = Property.ip_of_spec kf Kglobal ~active:[] s in
+ List.iter2 copy (ips kf spec) (ips new_kf new_spec);
+ (* remove annotations from the old spec. Yet keep them in functions only
+ declared since, otherwise, the kernel would complain about functions
+ with neither contract nor body *)
if Kernel_function.is_definition kf then begin
- Queue.add
- (fun () ->
- let bhvs =
- Annotations.fold_behaviors (fun e b acc -> (e, b) :: acc) kf []
- in
- List.iter
- (fun (e, b) -> Annotations.remove_behavior ~force:true e kf b)
- bhvs;
- Annotations.iter_decreases
- (fun e _ -> Annotations.remove_decreases e kf)
- kf;
- Annotations.iter_terminates
- (fun e _ -> Annotations.remove_terminates e kf)
- kf;
- Annotations.iter_complete
- (fun e l -> Annotations.remove_complete e kf l)
- kf;
- Annotations.iter_disjoint
- (fun e l -> Annotations.remove_disjoint e kf l)
- kf)
- actions
+ let old_bhvs =
+ Annotations.fold_behaviors (fun e b acc -> (e, b) :: acc) kf []
+ in
+ List.iter
+ (fun (e, b) -> Annotations.remove_behavior ~force:true e kf b)
+ old_bhvs;
+ Annotations.iter_decreases
+ (fun e _ -> Annotations.remove_decreases e kf)
+ kf;
+ Annotations.iter_terminates
+ (fun e _ -> Annotations.remove_terminates e kf)
+ kf;
+ Annotations.iter_complete
+ (fun e l -> Annotations.remove_complete e kf l)
+ kf;
+ Annotations.iter_disjoint
+ (fun e l -> Annotations.remove_disjoint e kf l)
+ kf
end;
- GFun(fundec, loc), GFunDecl(new_spec, new_vi, loc)
+ GFun(new_fundec, loc), GFunDecl(new_spec, new_vi, loc)
(* ********************************************************************** *)
(* Alignment *)
@@ -293,230 +289,187 @@ let require_alignment vi algn =
Cil.bitsSizeOf vi.vtype < algn*8 && not (sufficiently_aligned vi algn)
(* ********************************************************************** *)
-(* Visitor *)
+(* Visiting the globals *)
(* ********************************************************************** *)
-class prepare_visitor = object (self)
- inherit Visitor.frama_c_inplace
-
- val mutable has_new_stmt_in_fundec = false
-
- (* ---------------------------------------------------------------------- *)
- (* visitor's local variable *)
- (* ---------------------------------------------------------------------- *)
-
- val terms = Misc.Id_term.Hashtbl.create 7
- (* table for ensuring absence of term sharing *)
+(* perform a few modifications in the [kf]'s code and annotations that are
+ required by E-ACSL's analyses and transformations *)
+let prepare_fundec kf =
+ let o = object
+ inherit Visitor.frama_c_inplace
+
+ (* table for ensuring absence of term sharing *)
+ val terms = Misc.Id_term.Hashtbl.create 7
+
+ (* substitute function's varinfos by their duplicate in function calls *)
+ method !vvrbl vi =
+ try Cil.ChangeTo (Dup_functions.find vi)
+ with Not_found -> Cil.SkipChildren
+
+ (* temporal analysis requires that attributes are aligned to local
+ variables *)
+ method !vblock _ =
+ if Options.Temporal_validity.get () then
+ Cil.DoChildrenPost
+ (fun blk ->
+ List.iter
+ (fun vi ->
+ (* 4 bytes alignment is required to allow sufficient space for
+ storage of 32-bit timestamps in a 1:1 shadow. *)
+ if require_alignment vi 4 then
+ vi.vattr <-
+ Attr("aligned", [ AInt Integer.four ]) :: vi.vattr)
+ blk.blocals;
+ blk)
+ else
+ Cil.DoChildren
- val unduplicable_functions =
- let white_list =
- [ "__builtin_va_arg";
- "__builtin_va_end";
- "__builtin_va_start";
- "__builtin_va_copy" ]
- in
- List.fold_left
- (fun acc s -> Datatype.String.Set.add s acc)
- Datatype.String.Set.empty
- white_list
-
- val fct_tbl = Cil_datatype.Varinfo.Hashtbl.create 7
- val mutable new_definitions: global list = []
- (* new definitions of the annotated functions which will contain the
- translation of the E-ACSL contract *)
-
- (* the variable [sound_verdict] belongs to the E-ACSL's RTL and indicates
- whether the verdict emitted by E-ACSL is sound. It needs to be visible at
- that point because it is set in all function duplicates
- (see [dup_fundec]). *)
- val mutable sound_verdict_vi =
- let name = Functions.RTL.mk_api_name "sound_verdict" in
- let vi = Cil.makeGlobalVar name Cil.intType in
- vi.vstorage <- Extern;
- vi.vreferenced <- true;
- vi
-
- (* ---------------------------------------------------------------------- *)
- (* visitor's private methods *)
- (* ---------------------------------------------------------------------- *)
-
- method private is_variadic_function vi =
- match Cil.unrollType vi.vtype with
- | TFun(_, _, variadic, _) -> variadic
- | _ -> true
-
- (* ---------------------------------------------------------------------- *)
- (* visitor's method overloading *)
- (* ---------------------------------------------------------------------- *)
-
- method !vlogic_info_decl li =
- Global.add_logic_info li;
- Cil.SkipChildren
-
- method !vvrbl vi =
- try
- let new_vi = Cil_datatype.Varinfo.Hashtbl.find fct_tbl vi in
- (* replace functions at callsite by its duplicated version *)
- Cil.ChangeTo new_vi
- with Not_found ->
- Cil.SkipChildren
-
- method !vterm _t =
- Cil.DoChildrenPost
- (fun t ->
- if Misc.Id_term.Hashtbl.mem terms t then
- (* remove term sharing for soundness of E-ACSL typing
- (see typing.ml) *)
- { t with term_node = t.term_node }
- else begin
- Misc.Id_term.Hashtbl.add terms t ();
- t
- end)
-
- (* Add align attributes to local variables (required by temporal analysis) *)
- method !vblock _ =
- if Options.Temporal_validity.get () then
+ (* remove term sharing introduced by the Frama-C kernel. For instance, an
+ annotation such as [a <= t <= b] is replaced by [a <= t && t <= b] with
+ both occurrences of [t] being shared. Yet, the E-ACSL type system may
+ require to assign them different types. *)
+ method !vterm _ =
Cil.DoChildrenPost
- (fun blk ->
- List.iter
- (fun vi ->
- (* 4 bytes alignment is required to allow sufficient space for
- storage of 32-bit timestamps in a 1:1 shadow. *)
- if require_alignment vi 4 then
- vi.vattr <-
- Attr("aligned", [ AInt Integer.four ]) :: vi.vattr)
- blk.blocals;
- blk)
- else
- Cil.DoChildren
+ (fun t ->
+ if Misc.Id_term.Hashtbl.mem terms t then
+ { t with term_node = t.term_node }
+ else begin
+ Misc.Id_term.Hashtbl.add terms t ();
+ t
+ end)
- method !vfunc fundec =
- Cil.DoChildrenPost
- (fun _ ->
- if has_new_stmt_in_fundec then begin
- has_new_stmt_in_fundec <- false;
- (* recompute the CFG *)
- Cfg.clearCFGinfo ~clear_id:false fundec;
- Cfg.cfgFun fundec;
- end;
- fundec)
-
- method !vglob_aux = function
- | GFunDecl(_, vi, loc) | GFun({ svar = vi }, loc)
- when (* duplicate a function iff: *)
- (* it is not already duplicated *)
- not (Cil_datatype.Varinfo.Hashtbl.mem fct_tbl vi)
- && (* it is duplicable *)
- not (Datatype.String.Set.mem vi.vname unduplicable_functions)
- && (* it is not a variadic function *)
- not (self#is_variadic_function vi)
- && (* it is not a built-in *)
- not (Misc.is_fc_or_compiler_builtin vi)
- &&
- (let kf =
- try Globals.Functions.get vi with Not_found -> assert false
- in
- (* either explicitely listed as to be not instrumented *)
- not (Functions.instrument kf)
- ||
- (* or: *)
- ((* it has a function contract *)
- not (Cil.is_empty_funspec
- (Annotations.funspec ~populate:false
- (Extlib.the self#current_kf)))
- && (* its annotations must be monitored *)
- Functions.check kf))
- && (* it is neither malloc nor free *)
- (* [TODO:] this special case preserves the former behavior.
- Should be generalized latter by considering only preconditions of
- libc functions *)
- vi.vname <> "malloc" && vi.vname <> "calloc" && vi.vname <> "realloc"
- && vi.vname <> "free"
- ->
- let name = Functions.RTL.mk_gen_name vi.vname in
- let new_vi = Cil.makeGlobalVar name vi.vtype in
- Cil_datatype.Varinfo.Hashtbl.add fct_tbl vi new_vi;
- Cil.DoChildrenPost
- (fun l -> match l with
- | [ GFunDecl(_, vi, _) | GFun({ svar = vi }, _) as g ]
- ->
- let kf = Extlib.the self#current_kf in
- (match g with
- | GFunDecl _ ->
- if not (Kernel_function.is_definition kf) then
- Options.warning
- "@[annotating undefined function `%a':@ \
- the generated program may miss memory instrumentation@ \
- if there are memory-related annotations.@]"
- Printer.pp_varinfo vi
- | GFun _ -> ()
- | _ -> assert false);
- let tmp = vi.vname in
- if tmp = "main" then begin
- (* the new function becomes the new main: *)
- (* 1. swap the name of both functions *)
- vi.vname <- new_vi.vname;
- new_vi.vname <- tmp;
- (* 2. force recomputation of the entry point if necessary *)
- if Kernel.MainFunction.get () = tmp then begin
- let selection =
- State_selection.with_dependencies Kernel.MainFunction.self
- in
- Project.clear ~selection ()
- end
- (* 3. recompute what is necessary in [Globals.Functions]:
- done in [dup_global] *)
- end;
- let new_g, new_decl =
- dup_global
- loc
- self#get_filling_actions
- (Annotations.funspec ~populate:false kf)
- self#behavior
- sound_verdict_vi
- kf
- vi
- new_vi
- in
- (* postpone the introduction of the new function definition to the
- end *)
- new_definitions <- new_g :: new_definitions;
- (* put the declaration before the original function in order to
- solve issue with recursive functions *)
- [ new_decl; g ]
- | _ -> assert false)
-
- | _ ->
+ method !videntified_predicate _ =
+ (* when entering a new annotation, clear the context to keep it small:
+ anyway, no sharing is possible between two identified predicates *)
+ Misc.Id_term.Hashtbl.clear terms;
Cil.DoChildren
- method !vfile f =
- Cil.DoChildrenPost
- (fun _ ->
- match new_definitions with
- | [] -> f
- | _ :: _ ->
- (* add the generated definitions of libc at the end of
- [new_definitions]. This way, we are sure that they have access to
- all of it (in particular, the memory model, GMP and the soundness
- variable). Also add the [__e_acsl_sound_verdict] variable at the
- beginning *)
- let new_globals =
- GVarDecl(sound_verdict_vi, Cil_datatype.Location.unknown)
- :: f.globals
- @ new_definitions
- in
- f.globals <- new_globals;
- f)
-
- initializer
- reset ()
-
-end
+ end in
+ ignore (Visitor.visitFramacKf o kf)
+
+(* the variable [sound_verdict] belongs to the E-ACSL's RTL and indicates
+ whether the verdict emitted by E-ACSL is sound. It needs to be visible at
+ that point because it is set in all function duplicates (see
+ [dup_fundec]). *)
+let sound_verdict_vi =
+ lazy
+ (let name = Functions.RTL.mk_api_name "sound_verdict" in
+ let vi = Cil.makeGlobalVar name Cil.intType in
+ vi.vstorage <- Extern;
+ vi.vreferenced <- true;
+ vi)
+
+let is_variadic_function vi = match Cil.unrollType vi.vtype with
+ | TFun(_, _, variadic, _) -> variadic
+ | _ -> false
+
+(* set of functions that must never be duplicated *)
+let unduplicable_functions =
+ let white_list =
+ [ "__builtin_va_arg";
+ "__builtin_va_end";
+ "__builtin_va_start";
+ "__builtin_va_copy";
+ (* *alloc and free should not be duplicated. *)
+ (* [TODO:] it preserves the former behavior. Should be modified latter by
+ checking only preconditions for any libc functions *)
+ "malloc";
+ "calloc";
+ "realloc";
+ "free" ]
+ in
+ List.fold_left
+ (fun acc s -> Datatype.String.Set.add s acc)
+ Datatype.String.Set.empty
+ white_list
+
+let must_duplicate kf vi =
+ (* it is not already duplicated *)
+ not (Dup_functions.mem vi)
+ && (* it is duplicable *)
+ not (Datatype.String.Set.mem vi.vname unduplicable_functions)
+ && (* it is not a variadic function *)
+ not (is_variadic_function vi)
+ && (* it is not a built-in *)
+ not (Misc.is_fc_or_compiler_builtin vi)
+ &&
+ ((* either explicitely listed as to be not instrumented *)
+ not (Functions.instrument kf)
+ ||
+ (* or: *)
+ ((* it has a function contract *)
+ not (Cil.is_empty_funspec (Annotations.funspec ~populate:false kf))
+ && (* its annotations must be monitored *)
+ Functions.check kf))
+
+let prepare_global (globals, new_defs) = function
+ | GFunDecl(_, vi, loc) | GFun({ svar = vi }, loc) as g ->
+ let kf = try Globals.Functions.get vi with Not_found -> assert false in
+ if must_duplicate kf vi then begin
+ let new_vi = Dup_functions.generate_vi vi in
+ if Kernel_function.is_definition kf then
+ prepare_fundec kf
+ else
+ (* TODO: this warning could be more precise if emitted during code
+ generation; see also E-ACSL issue #85 about partial verdicts *)
+ Options.warning
+ "@[annotating undefined function `%a':@ \
+ the generated program may miss memory instrumentation@ \
+ if there are memory-related annotations.@]"
+ Printer.pp_varinfo vi;
+ let tmp = vi.vname in
+ if Datatype.String.equal tmp "main" then begin
+ (* the new function becomes the new main: *)
+ (* 1. swap the name of both functions *)
+ vi.vname <- new_vi.vname;
+ new_vi.vname <- tmp;
+ (* 2. force recomputation of the entry point if necessary *)
+ if Kernel.MainFunction.get () = tmp then begin
+ let selection =
+ State_selection.with_dependencies Kernel.MainFunction.self
+ in
+ Project.clear ~selection ()
+ end
+ end;
+ let new_def, new_decl =
+ dup_global
+ loc
+ (Annotations.funspec ~populate:false kf)
+ (Lazy.force sound_verdict_vi)
+ kf
+ vi
+ new_vi
+ in
+ (* postpone the introduction of the new function definition *)
+ let new_defs = new_def :: new_defs in
+ (* put the declaration before the original function in order to solve
+ issues with recursive functions *)
+ g :: new_decl :: globals, new_defs
+ end else begin (* not duplicated *)
+ prepare_fundec kf;
+ g :: globals, new_defs
+ end
+ | g ->
+ (* nothing to do for globals that are not functions *)
+ g :: globals, new_defs
+
+let prepare_file file =
+ Dup_functions.reset ();
+ let rev_globals, new_defs =
+ List.fold_left prepare_global ([], []) file.globals
+ in
+ match new_defs with
+ | [] -> ()
+ | _ :: _ ->
+ (* insert the new_definitions at the end and reverse back the globals *)
+ let globals = List.fold_left (fun acc g -> g :: acc) new_defs rev_globals in
+ (* insert [__e_acsl_sound_verdict] at the beginning *)
+ let sg = GVarDecl(Lazy.force sound_verdict_vi, Location.unknown) in
+ file.globals <- sg :: globals
let prepare () =
Options.feedback ~level:2 "prepare AST for E-ACSL transformations";
- Visitor.visitFramacFile (new prepare_visitor) (Ast.get ());
- Queue.iter (fun f -> f ()) actions;
+ prepare_file (Ast.get ());
Ast.mark_as_grown ()
(*
--
GitLab