diff --git a/Changelog b/Changelog
index fdd6af530d7a908fe316ff318a6de3e8daf87ddf..fdeab1fa81a4f63f4457c77819a04b02671bb6a4 100644
--- a/Changelog
+++ b/Changelog
@@ -17,6 +17,9 @@
Open Source Release <next-release>
##################################
+o! Kernel [2019/08/02] Functions over visitor's behaviors have been moved
+ from Cil into a new module Visitor_behavior. Apply the migration
+ script potassium2calcium.sh to update your plug-ins automatically.
o! Sparecode [2019/07/26] Removed from Db. Use proper Sparecode API instead.
-! Kernel [2019/07/24] OCaml version greater than or equal to 4.05.0 required.
- Kernel [2019/07/24] Improve placeholders handling in -cpp-command
diff --git a/Makefile b/Makefile
index 66a68df323552efd31deb99e5602b262207800c7..72f0a63b88a1e0a40be8e93f25d1a163cb87cfe6 100644
--- a/Makefile
+++ b/Makefile
@@ -520,6 +520,7 @@ KERNEL_CMO=\
src/kernel_services/ast_queries/cil_const.cmo \
src/kernel_services/ast_queries/logic_env.cmo \
src/kernel_services/ast_queries/logic_const.cmo \
+ src/kernel_services/visitors/visitor_behavior.cmo \
src/kernel_services/ast_queries/cil.cmo \
src/kernel_internals/parsing/errorloc.cmo \
src/kernel_services/ast_printing/cil_printer.cmo \
diff --git a/bin/migration_scripts/potassium2calcium.sh b/bin/migration_scripts/potassium2calcium.sh
index b927f2094eee56786f785f1bdd81bae323ab9dfe..73f36e65462cd9623e8db919ce109821d868c871 100755
--- a/bin/migration_scripts/potassium2calcium.sh
+++ b/bin/migration_scripts/potassium2calcium.sh
@@ -84,6 +84,26 @@ process_file ()
-e "s/Transitioning\.List\./List./g" \
-e "s/Transitioning\.Stack\./Stack./g" \
-e "s/Transitioning\.String\./String./g" \
+ -e "s/Cil\.Eid/Cil_const\.Eid/g" \
+ -e "s/Cil\.Sid/Cil_const\.Sid/g" \
+ -e "s/Cil\.mkCompInfo/Cil_const\.mkCompInfo/g" \
+ -e "s/Cil\.copyCompInfo/Cil_const\.copyCompInfo/g" \
+ -e "s/Cil\.visitor_behavior/Visitor_behavior\.t/g" \
+ -e "s/Cil\.inplace_visit/Visitor_behavior\.inplace/g" \
+ -e "s/Cil\.copy_visit/Visitor_behavior\.copy/g" \
+ -e "s/Cil\.refresh_visit/Visitor_behavior\.refresh/g" \
+ -e "s/Cil\.is_fresh_behavior/Visitor_behavior\.is_fresh/g" \
+ -e "s/Cil\.is_copy_behavior/Visitor_behavior\.is_copy/g" \
+ -e "s/Cil\.reset_behavior_/Visitor_behavior\.Reset\./g" \
+ -e "s/Cil\.get_original_/Visitor_behavior\.Get_orig\./g" \
+ -e "s/Cil\.get_/Visitor_behavior\.Get\./g" \
+ -e "s/Cil\.set_orig_/Visitor_behavior\.Set_orig\./g" \
+ -e "s/Cil\.set_/Visitor_behavior\.Set\./g" \
+ -e "s/Cil\.unset_orig_/Visitor_behavior\.Unset_orig\./g" \
+ -e "s/Cil\.unset_/Visitor_behavior\.Unset\./g" \
+ -e "s/Cil\.memo_/Visitor_behavior\.Memo\./g" \
+ -e "s/Cil\.iter_visitor_/Visitor_behavior\.Iter\./g" \
+ -e "s/Cil\.fold_visitor_/Visitor_behavior\.Fold\./g" \
$file
}
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 08eb5d8ee17919e849c7b5888e070d46e69029a5..2d3abcb762ac7e9a419a2be8c515b764ab150861 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -586,6 +586,8 @@ src/kernel_services/visitors/cabsvisit.ml: CIL
src/kernel_services/visitors/cabsvisit.mli: CIL
src/kernel_services/visitors/visitor.ml: CEA_LGPL
src/kernel_services/visitors/visitor.mli: CEA_LGPL
+src/kernel_services/visitors/visitor_behavior.ml: CEA_INRIA_LGPL
+src/kernel_services/visitors/visitor_behavior.mli: CEA_INRIA_LGPL
src/libraries/README.md: .ignore
src/libraries/datatype/README.md: .ignore
src/libraries/datatype/datatype.ml: CEA_LGPL
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index cd3d07b4f50795b3aff774f4ed95c472a900abf0..1b595764bf03ef02f94a6901f87658e97ab5b21d 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -1222,7 +1222,9 @@ let createCompInfo (iss: bool) (n: string) ~(norig: string) : compinfo * bool =
H.find compInfoNameEnv key, false (* Only if not already in *)
with Not_found -> begin
(* Create a compinfo. This will have "cdefined" false. *)
- let res = mkCompInfo iss n ~norig (fun _ ->[]) (fc_stdlib_attribute []) in
+ let res =
+ Cil_const.mkCompInfo iss n ~norig (fun _ ->[]) (fc_stdlib_attribute [])
+ in
H.add compInfoNameEnv key res;
res, true
end
@@ -9995,7 +9997,7 @@ and doStatement local_env (s : A.statement) : chunk =
let copy_spec (old_f,new_f) formals_map spec =
let obj = object
- inherit Cil.genericCilVisitor (Cil.refresh_visit (Project.current()))
+ inherit Cil.genericCilVisitor (Visitor_behavior.refresh (Project.current()))
method! vlogic_var_use lv =
match lv.lv_origin with
| None -> DoChildren
diff --git a/src/kernel_internals/typing/cfg.ml b/src/kernel_internals/typing/cfg.ml
index 2d52020ae408c3d0f22febebc4d5ce80263f006e..21e648adf5c318f6dd538eadb1f81ac982d868d4 100644
--- a/src/kernel_internals/typing/cfg.ml
+++ b/src/kernel_internals/typing/cfg.ml
@@ -127,7 +127,7 @@ let make_break_stmt loc env next =
let rec cfgFun (fd : fundec) =
nodeList := [];
cfgBlock (init_env fd.sbody) fd.sbody None None None;
- fd.smaxstmtid <- Some(Cil.Sid.next ());
+ fd.smaxstmtid <- Some(Cil_const.Sid.next ());
fd.sallstmts <- List.rev !nodeList;
nodeList := []
@@ -161,7 +161,7 @@ and cfgBlock env (blk: block) next break cont =
(* Fill in the CFG info for a stmt
Meaning of next, break, cont should be clear from earlier comment *)
and cfgStmt env (s: stmt) next break cont =
- if s.sid = -1 then s.sid <- Cil.Sid.next ();
+ if s.sid = -1 then s.sid <- Cil_const.Sid.next ();
nodeList := s :: !nodeList;
if s.succs <> [] then
Kernel.fatal
diff --git a/src/kernel_internals/typing/unroll_loops.ml b/src/kernel_internals/typing/unroll_loops.ml
index c85d9b2aa7178af7dff2298349b53fb2639bff72..697409bca64ca11bc4872bc36262516489d8c9a3 100644
--- a/src/kernel_internals/typing/unroll_loops.ml
+++ b/src/kernel_internals/typing/unroll_loops.ml
@@ -318,7 +318,7 @@ let copy_block kf switch_label_action break_continue_must_change bl =
labelled_stmt_tbl calls_tbl stmt =
let result =
{ labels = [];
- sid = Sid.next ();
+ sid = Cil_const.Sid.next ();
succs = [];
preds = [];
skind = stmt.skind;
@@ -627,14 +627,14 @@ class do_it global_find_init ((force:bool),(times:int)) = object(self)
let break_label = fresh_label () in
let break_lbl_stmt = mkEmptyStmt () in
break_lbl_stmt.labels <- [break_label];
- break_lbl_stmt.sid <- Cil.Sid.next ();
+ break_lbl_stmt.sid <- Cil_const.Sid.next ();
break_lbl_stmt
in
let mk_continue () =
let continue_label = fresh_label () in
let continue_lbl_stmt = mkEmptyStmt () in
continue_lbl_stmt.labels <- [continue_label] ;
- continue_lbl_stmt.sid <- Cil.Sid.next ();
+ continue_lbl_stmt.sid <- Cil_const.Sid.next ();
continue_lbl_stmt
in
let current_continue = ref (mk_continue ()) in
diff --git a/src/kernel_services/analysis/exn_flow.ml b/src/kernel_services/analysis/exn_flow.ml
index ce65a50c9f099f06ec8bc4ac732d950928634387..8a1904e4b5bf025af481464ee7e0f8c0bc2c4ded 100644
--- a/src/kernel_services/analysis/exn_flow.ml
+++ b/src/kernel_services/analysis/exn_flow.ml
@@ -350,7 +350,8 @@ let generate_exn_union e exns =
in
let union_name = "__fc_exn_union" in
let exn_kind_union =
- Cil.mkCompInfo false union_name ~norig:union_name create_union_fields []
+ Cil_const.mkCompInfo
+ false union_name ~norig:union_name create_union_fields []
in
let create_struct_fields _ =
let uncaught = (exn_uncaught_name, Cil.intType, None, [], loc) in
@@ -363,7 +364,8 @@ let generate_exn_union e exns =
in
let struct_name = "__fc_exn_struct" in
let exn_struct =
- Cil.mkCompInfo true struct_name ~norig:struct_name create_struct_fields []
+ Cil_const.mkCompInfo
+ true struct_name ~norig:struct_name create_struct_fields []
in
exn_kind_union, exn_struct
@@ -690,8 +692,10 @@ object(self)
method private clean_catch_clause (bind,b as handler) acc =
let remove_local v =
- let f = Cil.get_fundec self#behavior (Extlib.the self#current_func) in
- let v = Cil.get_varinfo self#behavior v in
+ let f =
+ Visitor_behavior.Get.fundec self#behavior (Extlib.the self#current_func)
+ in
+ let v = Visitor_behavior.Get.varinfo self#behavior v in
f.slocals <- List.filter (fun v' -> v!=v') f.slocals;
in
match bind with
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 0184c5caff71b00d91d7d5c9aa952a5d17c30bff..6b8f9d91e8e15bd13ef38dd1457acf7619bc17eb 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -210,12 +210,7 @@ let selfMachine_is_computed = TheMachine.is_computed
let debugConstFold = false
-(* TODO: migrate that to Cil_const as well *)
-module Sid = State_builder.SharedCounter(struct let name = "sid" end)
-
-module Eid = State_builder.SharedCounter(struct let name = "eid" end)
-
-let new_exp ~loc e = { eloc = loc; eid = Eid.next (); enode = e }
+let new_exp ~loc e = { eloc = loc; eid = Cil_const.Eid.next (); enode = e }
let dummy_exp e = { eid = -1; enode = e; eloc = Cil_datatype.Location.unknown }
@@ -291,7 +286,7 @@ let mkStmt ?(ghost=false) ?(valid_sid=false) ?(sattr=[]) (sk: stmtkind) : stmt =
safely be used in tables. I only do it when performing Jessie
analysis, as other plugins rely on specific sid values for their tests
(e.g. slicing). *)
- sid = if valid_sid then Sid.next () else -1;
+ sid = if valid_sid then Cil_const.Sid.next () else -1;
succs = []; preds = [];
ghost = ghost;
sattr = sattr;}
@@ -685,74 +680,12 @@ let is_empty_behavior b =
b.b_assumes = [] && b.b_requires = [] && b.b_post_cond = [] &&
b.b_assigns = WritesAny && b.b_allocation = FreeAllocAny && b.b_extended = []
+let missingFieldName = "" (* "___missing_field_name"*)
+
(** Get the full name of a comp *)
let compFullName comp =
(if comp.cstruct then "struct " else "union ") ^ comp.cname
-
-let missingFieldName = "" (* "___missing_field_name"*)
-
-(* The next compindo identifier to use. Counts up. *)
-let nextCompinfoKey =
- let module M =
- State_builder.SharedCounter(struct let name = "compinfokey" end)
- in
- M.next
-
-(** Creates a (potentially recursive) composite type. Make sure you add a
- * GTag for it to the file! **)
-let mkCompInfo
- (isstruct: bool)
- (n: string)
- ?(norig=n)
- (* fspec is a function that when given a forward
- * representation of the structure type constructs the type of
- * the fields. The function can ignore this argument if not
- * constructing a recursive type. *)
- (mkfspec: compinfo -> (string * typ * int option * attribute list *
- location) list)
- (a: attribute list) : compinfo =
-
- (* make a new name for anonymous structs *)
- if n = "" then Kernel.fatal "mkCompInfo: missing structure name\n" ;
- (* Make a new self cell and a forward reference *)
- let comp =
- { cstruct = isstruct;
- corig_name = norig;
- cname = n;
- ckey = nextCompinfoKey ();
- cfields = []; (* fields will be added afterwards. *)
- cattr = a;
- creferenced = false;
- (* Make this compinfo undefined by default *)
- cdefined = false; }
- in
- let flds =
- List.map (fun (fn, ft, fb, fa, fl) ->
- { fcomp = comp;
- ftype = ft;
- forig_name = fn;
- fname = fn;
- fbitfield = fb;
- fattr = fa;
- floc = fl;
- faddrof = false;
- fsize_in_bits = None;
- foffset_in_bits = None;
- fpadding_in_bits = None;
- }) (mkfspec comp) in
- comp.cfields <- flds;
- if flds <> [] then comp.cdefined <- true;
- comp
-
-(** Make a copy of a compinfo, changing the name and the key *)
-let copyCompInfo ?(fresh=true) ci cname =
- let ckey = if fresh then nextCompinfoKey () else ci.ckey in
- let ci' = { ci with cname; ckey } in
- (* Copy the fields and set the new pointers to parents *)
- ci'.cfields <- List.map (fun f -> {f with fcomp = ci'}) ci'.cfields;
- ci'
-
(** Different visiting actions. 'a will be instantiated with [exp], [instr],
etc.
@see Plugin Development Guide *)
@@ -778,1046 +711,11 @@ type 'a visitAction =
has changed and then apply the
function on the node *)
-type visitor_behavior =
- { (* copy mutable structure which are not shared across the AST*)
- cfile: file -> file;
- cinitinfo: initinfo -> initinfo;
- cblock: block -> block;
- cfunspec: funspec -> funspec;
- cfunbehavior: funbehavior -> funbehavior;
- cidentified_term: identified_term -> identified_term;
- cidentified_predicate: identified_predicate -> identified_predicate;
- cexpr: exp -> exp;
- ccode_annotation: code_annotation -> code_annotation;
- (* get the copy of a shared value *)
- get_stmt: stmt -> stmt;
- get_compinfo: compinfo -> compinfo;
- get_fieldinfo: fieldinfo -> fieldinfo;
- get_model_info: model_info -> model_info;
- get_enuminfo: enuminfo -> enuminfo;
- get_enumitem: enumitem -> enumitem;
- get_typeinfo: typeinfo -> typeinfo;
- get_varinfo: varinfo -> varinfo;
- get_logic_info: logic_info -> logic_info;
- get_logic_type_info: logic_type_info -> logic_type_info;
- get_logic_var: logic_var -> logic_var;
- get_kernel_function: kernel_function -> kernel_function;
- get_fundec: fundec -> fundec;
- (* get the original value tied to a copy *)
- get_original_stmt: stmt -> stmt;
- get_original_compinfo: compinfo -> compinfo;
- get_original_fieldinfo: fieldinfo -> fieldinfo;
- get_original_model_info: model_info -> model_info;
- get_original_enuminfo: enuminfo -> enuminfo;
- get_original_enumitem: enumitem -> enumitem;
- get_original_typeinfo: typeinfo -> typeinfo;
- get_original_varinfo: varinfo -> varinfo;
- get_original_logic_info: logic_info -> logic_info;
- get_original_logic_type_info: logic_type_info -> logic_type_info;
- get_original_logic_var: logic_var -> logic_var;
- get_original_kernel_function: kernel_function -> kernel_function;
- get_original_fundec: fundec -> fundec;
- (* change a binding... use with care *)
- set_stmt: stmt -> stmt -> unit;
- set_compinfo: compinfo -> compinfo -> unit;
- set_fieldinfo: fieldinfo -> fieldinfo -> unit;
- set_model_info: model_info -> model_info -> unit;
- set_enuminfo: enuminfo -> enuminfo -> unit;
- set_enumitem: enumitem -> enumitem -> unit;
- set_typeinfo: typeinfo -> typeinfo -> unit;
- set_varinfo: varinfo -> varinfo -> unit;
- set_logic_info: logic_info -> logic_info -> unit;
- set_logic_type_info: logic_type_info -> logic_type_info -> unit;
- set_logic_var: logic_var -> logic_var -> unit;
- set_kernel_function: kernel_function -> kernel_function -> unit;
- set_fundec: fundec -> fundec -> unit;
- (* change a reference... use with care *)
- set_orig_stmt: stmt -> stmt -> unit;
- set_orig_compinfo: compinfo -> compinfo -> unit;
- set_orig_fieldinfo: fieldinfo -> fieldinfo -> unit;
- set_orig_model_info: model_info -> model_info -> unit;
- set_orig_enuminfo: enuminfo -> enuminfo -> unit;
- set_orig_enumitem: enumitem -> enumitem -> unit;
- set_orig_typeinfo: typeinfo -> typeinfo -> unit;
- set_orig_varinfo: varinfo -> varinfo -> unit;
- set_orig_logic_info: logic_info -> logic_info -> unit;
- set_orig_logic_type_info: logic_type_info -> logic_type_info -> unit;
- set_orig_logic_var: logic_var -> logic_var -> unit;
- set_orig_kernel_function: kernel_function -> kernel_function -> unit;
- set_orig_fundec: fundec -> fundec -> unit;
-
- unset_varinfo: varinfo -> unit;
- unset_compinfo: compinfo -> unit;
- unset_enuminfo: enuminfo -> unit;
- unset_enumitem: enumitem -> unit;
- unset_typeinfo: typeinfo -> unit;
- unset_stmt: stmt -> unit;
- unset_logic_info: logic_info -> unit;
- unset_logic_type_info: logic_type_info -> unit;
- unset_fieldinfo: fieldinfo -> unit;
- unset_model_info: model_info -> unit;
- unset_logic_var: logic_var -> unit;
- unset_kernel_function: kernel_function -> unit;
- unset_fundec: fundec -> unit;
-
- unset_orig_varinfo: varinfo -> unit;
- unset_orig_compinfo: compinfo -> unit;
- unset_orig_enuminfo: enuminfo -> unit;
- unset_orig_enumitem: enumitem -> unit;
- unset_orig_typeinfo: typeinfo -> unit;
- unset_orig_stmt: stmt -> unit;
- unset_orig_logic_info: logic_info -> unit;
- unset_orig_logic_type_info: logic_type_info -> unit;
- unset_orig_fieldinfo: fieldinfo -> unit;
- unset_orig_model_info: model_info -> unit;
- unset_orig_logic_var: logic_var -> unit;
- unset_orig_kernel_function: kernel_function -> unit;
- unset_orig_fundec: fundec -> unit;
-
- (* copy fields that can referenced in other places of the AST*)
- memo_stmt: stmt -> stmt;
- memo_varinfo: varinfo -> varinfo;
- memo_compinfo: compinfo -> compinfo;
- memo_model_info: model_info -> model_info;
- memo_enuminfo: enuminfo -> enuminfo;
- memo_enumitem: enumitem -> enumitem;
- memo_typeinfo: typeinfo -> typeinfo;
- memo_logic_info: logic_info -> logic_info;
- memo_logic_type_info: logic_type_info -> logic_type_info;
- memo_fieldinfo: fieldinfo -> fieldinfo;
- memo_logic_var: logic_var -> logic_var;
- memo_kernel_function: kernel_function -> kernel_function;
- memo_fundec: fundec -> fundec;
- (* is the behavior a copy behavior *)
- is_copy_behavior: bool;
- is_fresh_behavior: bool;
- project: Project.t option;
- (* reset memoizing tables *)
- reset_behavior_varinfo: unit -> unit;
- reset_behavior_compinfo: unit -> unit;
- reset_behavior_enuminfo: unit -> unit;
- reset_behavior_enumitem: unit -> unit;
- reset_behavior_typeinfo: unit -> unit;
- reset_behavior_logic_info: unit -> unit;
- reset_behavior_logic_type_info: unit -> unit;
- reset_behavior_fieldinfo: unit -> unit;
- reset_behavior_model_info: unit -> unit;
- reset_behavior_stmt: unit -> unit;
- reset_logic_var: unit -> unit;
- reset_behavior_kernel_function: unit -> unit;
- reset_behavior_fundec: unit -> unit;
- (* iterates over tables *)
- iter_visitor_varinfo: (varinfo -> varinfo -> unit) -> unit;
- iter_visitor_compinfo: (compinfo -> compinfo -> unit) -> unit;
- iter_visitor_enuminfo: (enuminfo -> enuminfo -> unit) -> unit;
- iter_visitor_enumitem: (enumitem -> enumitem -> unit) -> unit;
- iter_visitor_typeinfo: (typeinfo -> typeinfo -> unit) -> unit;
- iter_visitor_stmt: (stmt -> stmt -> unit) -> unit;
- iter_visitor_logic_info: (logic_info -> logic_info -> unit) -> unit;
- iter_visitor_logic_type_info:
- (logic_type_info -> logic_type_info -> unit) -> unit;
- iter_visitor_fieldinfo: (fieldinfo -> fieldinfo -> unit) -> unit;
- iter_visitor_model_info: (model_info -> model_info -> unit) -> unit;
- iter_visitor_logic_var: (logic_var -> logic_var -> unit) -> unit;
- iter_visitor_kernel_function:
- (kernel_function -> kernel_function -> unit) -> unit;
- iter_visitor_fundec: (fundec -> fundec -> unit) -> unit;
- (* folds over tables *)
- fold_visitor_varinfo: 'a.(varinfo -> varinfo -> 'a -> 'a) -> 'a -> 'a;
- fold_visitor_compinfo: 'a.(compinfo -> compinfo -> 'a -> 'a) -> 'a -> 'a;
- fold_visitor_enuminfo: 'a.(enuminfo -> enuminfo -> 'a -> 'a) -> 'a -> 'a;
- fold_visitor_enumitem: 'a.(enumitem -> enumitem -> 'a -> 'a) -> 'a -> 'a;
- fold_visitor_typeinfo: 'a.(typeinfo -> typeinfo -> 'a -> 'a) -> 'a -> 'a;
- fold_visitor_stmt: 'a.(stmt -> stmt -> 'a -> 'a) -> 'a -> 'a;
- fold_visitor_logic_info:
- 'a. (logic_info -> logic_info -> 'a -> 'a) -> 'a -> 'a;
- fold_visitor_logic_type_info:
- 'a.(logic_type_info -> logic_type_info -> 'a -> 'a) -> 'a -> 'a;
- fold_visitor_fieldinfo:
- 'a.(fieldinfo -> fieldinfo -> 'a -> 'a) -> 'a -> 'a;
- fold_visitor_model_info:
- 'a. (model_info -> model_info -> 'a -> 'a) -> 'a -> 'a;
- fold_visitor_logic_var:
- 'a.(logic_var -> logic_var -> 'a -> 'a) -> 'a -> 'a;
- fold_visitor_kernel_function:
- 'a.(kernel_function -> kernel_function -> 'a -> 'a) -> 'a -> 'a;
- fold_visitor_fundec:
- 'a.(fundec -> fundec -> 'a -> 'a) -> 'a -> 'a;
- }
-
-let is_copy_behavior b = b.is_copy_behavior
-
-let is_fresh_behavior b = b.is_fresh_behavior
-
-let memo_varinfo b = b.memo_varinfo
-let memo_compinfo b = b.memo_compinfo
-let memo_fieldinfo b = b.memo_fieldinfo
-let memo_model_info b = b.memo_model_info
-let memo_enuminfo b = b.memo_enuminfo
-let memo_enumitem b = b.memo_enumitem
-let memo_stmt b = b.memo_stmt
-let memo_typeinfo b = b.memo_typeinfo
-let memo_logic_info b = b.memo_logic_info
-let memo_logic_type_info b = b.memo_logic_type_info
-let memo_logic_var b = b.memo_logic_var
-let memo_kernel_function b = b.memo_kernel_function
-let memo_fundec b = b.memo_fundec
-
-let reset_behavior_varinfo b = b.reset_behavior_varinfo ()
-let reset_behavior_compinfo b = b.reset_behavior_compinfo ()
-let reset_behavior_enuminfo b = b.reset_behavior_enuminfo ()
-let reset_behavior_enumitem b = b.reset_behavior_enumitem ()
-let reset_behavior_typeinfo b = b.reset_behavior_typeinfo ()
-let reset_behavior_logic_info b = b.reset_behavior_logic_info ()
-let reset_behavior_logic_type_info b = b.reset_behavior_logic_type_info ()
-let reset_behavior_fieldinfo b = b.reset_behavior_fieldinfo ()
-let reset_behavior_model_info b = b.reset_behavior_model_info ()
-let reset_behavior_stmt b = b.reset_behavior_stmt ()
-let reset_logic_var b = b.reset_logic_var ()
-let reset_behavior_kernel_function b = b.reset_behavior_kernel_function ()
-let reset_behavior_fundec b = b.reset_behavior_fundec ()
-
-let get_varinfo b = b.get_varinfo
-let get_compinfo b = b.get_compinfo
-let get_fieldinfo b = b.get_fieldinfo
-let get_model_info b = b.get_model_info
-let get_enuminfo b = b.get_enuminfo
-let get_enumitem b = b.get_enumitem
-let get_stmt b = b.get_stmt
-let get_typeinfo b = b.get_typeinfo
-let get_logic_info b = b.get_logic_info
-let get_logic_type_info b = b.get_logic_type_info
-let get_logic_var b = b.get_logic_var
-let get_kernel_function b = b.get_kernel_function
-let get_fundec b = b.get_fundec
-
-let get_original_varinfo b = b.get_original_varinfo
-let get_original_compinfo b = b.get_original_compinfo
-let get_original_fieldinfo b = b.get_original_fieldinfo
-let get_original_model_info b = b.get_original_model_info
-let get_original_enuminfo b = b.get_original_enuminfo
-let get_original_enumitem b = b.get_original_enumitem
-let get_original_stmt b = b.get_original_stmt
-let get_original_typeinfo b = b.get_original_typeinfo
-let get_original_logic_info b = b.get_original_logic_info
-let get_original_logic_type_info b = b.get_original_logic_type_info
-let get_original_logic_var b = b.get_original_logic_var
-let get_original_kernel_function b = b.get_original_kernel_function
-let get_original_fundec b = b.get_original_fundec
-
-let set_varinfo b = b.set_varinfo
-let set_compinfo b = b.set_compinfo
-let set_fieldinfo b = b.set_fieldinfo
-let set_model_info b = b.set_model_info
-let set_enuminfo b = b.set_enuminfo
-let set_enumitem b = b.set_enumitem
-let set_stmt b = b.set_stmt
-let set_typeinfo b = b.set_typeinfo
-let set_logic_info b = b.set_logic_info
-let set_logic_type_info b = b.set_logic_type_info
-let set_logic_var b = b.set_logic_var
-let set_kernel_function b = b.set_kernel_function
-let set_fundec b = b.set_fundec
-
-let set_orig_varinfo b = b.set_orig_varinfo
-let set_orig_compinfo b = b.set_orig_compinfo
-let set_orig_fieldinfo b = b.set_orig_fieldinfo
-let set_orig_model_info b = b.set_model_info
-let set_orig_enuminfo b = b.set_orig_enuminfo
-let set_orig_enumitem b = b.set_orig_enumitem
-let set_orig_stmt b = b.set_orig_stmt
-let set_orig_typeinfo b = b.set_orig_typeinfo
-let set_orig_logic_info b = b.set_orig_logic_info
-let set_orig_logic_type_info b = b.set_orig_logic_type_info
-let set_orig_logic_var b = b.set_orig_logic_var
-let set_orig_kernel_function b= b.set_orig_kernel_function
-let set_orig_fundec b = b.set_orig_fundec
-
-let unset_varinfo b = b.unset_varinfo
-let unset_compinfo b = b.unset_compinfo
-let unset_fieldinfo b = b.unset_fieldinfo
-let unset_model_info b = b.unset_model_info
-let unset_enuminfo b = b.unset_enuminfo
-let unset_enumitem b = b.unset_enumitem
-let unset_stmt b = b.unset_stmt
-let unset_typeinfo b = b.unset_typeinfo
-let unset_logic_info b = b.unset_logic_info
-let unset_logic_type_info b = b.unset_logic_type_info
-let unset_logic_var b = b.unset_logic_var
-let unset_kernel_function b = b.unset_kernel_function
-let unset_fundec b = b.unset_fundec
-
-let unset_orig_varinfo b = b.unset_orig_varinfo
-let unset_orig_compinfo b = b.unset_orig_compinfo
-let unset_orig_fieldinfo b = b.unset_orig_fieldinfo
-let unset_orig_model_info b = b.unset_model_info
-let unset_orig_enuminfo b = b.unset_orig_enuminfo
-let unset_orig_enumitem b = b.unset_orig_enumitem
-let unset_orig_stmt b = b.unset_orig_stmt
-let unset_orig_typeinfo b = b.unset_orig_typeinfo
-let unset_orig_logic_info b = b.unset_orig_logic_info
-let unset_orig_logic_type_info b = b.unset_orig_logic_type_info
-let unset_orig_logic_var b = b.unset_orig_logic_var
-let unset_orig_kernel_function b= b.unset_orig_kernel_function
-let unset_orig_fundec b = b.unset_orig_fundec
-
-let iter_visitor_varinfo b = b.iter_visitor_varinfo
-let iter_visitor_compinfo b = b.iter_visitor_compinfo
-let iter_visitor_enuminfo b = b.iter_visitor_enuminfo
-let iter_visitor_enumitem b = b.iter_visitor_enumitem
-let iter_visitor_typeinfo b = b.iter_visitor_typeinfo
-let iter_visitor_stmt b = b.iter_visitor_stmt
-let iter_visitor_logic_info b= b.iter_visitor_logic_info
-let iter_visitor_logic_type_info b = b .iter_visitor_logic_type_info
-let iter_visitor_fieldinfo b = b.iter_visitor_fieldinfo
-let iter_visitor_model_info b = b.iter_visitor_model_info
-let iter_visitor_logic_var b = b.iter_visitor_logic_var
-let iter_visitor_kernel_function b = b.iter_visitor_kernel_function
-let iter_visitor_fundec b = b.iter_visitor_fundec
-
-let fold_visitor_varinfo b = b.fold_visitor_varinfo
-let fold_visitor_compinfo b = b.fold_visitor_compinfo
-let fold_visitor_enuminfo b = b.fold_visitor_enuminfo
-let fold_visitor_enumitem b = b.fold_visitor_enumitem
-let fold_visitor_typeinfo b = b.fold_visitor_typeinfo
-let fold_visitor_stmt b = b.fold_visitor_stmt
-let fold_visitor_logic_info b = b.fold_visitor_logic_info
-let fold_visitor_logic_type_info b = b.fold_visitor_logic_type_info
-let fold_visitor_fieldinfo b = b.fold_visitor_fieldinfo
-let fold_visitor_model_info b = b.fold_visitor_model_info
-let fold_visitor_logic_var b = b.fold_visitor_logic_var
-let fold_visitor_kernel_function b = b.fold_visitor_kernel_function
-let fold_visitor_fundec b = b.fold_visitor_fundec
let id = Extlib.id
-let alphabetaunit _ _ = ()
let alphabetabeta _ x = x
let alphabetafalse _ _ = false
-let unitunit: unit -> unit = id
let alphatrue _ = true
-let alphaunit _ = ()
-
-let inplace_visit () =
- { cfile = id;
- get_compinfo = id;
- get_fieldinfo = id;
- get_model_info = id;
- get_enuminfo = id;
- get_enumitem = id;
- get_typeinfo = id;
- get_varinfo = id;
- get_logic_var = id;
- get_stmt = id;
- get_logic_info = id;
- get_logic_type_info = id;
- get_kernel_function = id;
- get_fundec = id;
- get_original_compinfo = id;
- get_original_fieldinfo = id;
- get_original_model_info = id;
- get_original_enuminfo = id;
- get_original_enumitem = id;
- get_original_typeinfo = id;
- get_original_varinfo = id;
- get_original_logic_var = id;
- get_original_stmt = id;
- get_original_logic_info = id;
- get_original_logic_type_info = id;
- get_original_kernel_function = id;
- get_original_fundec = id;
- cinitinfo = id;
- cblock = id;
- cfunspec = id;
- cfunbehavior = id;
- cidentified_term = id;
- cidentified_predicate = id;
- ccode_annotation = id;
- cexpr = id;
- is_copy_behavior = false;
- is_fresh_behavior = false;
- project = None;
- memo_varinfo = id;
- memo_compinfo = id;
- memo_enuminfo = id;
- memo_enumitem = id;
- memo_typeinfo = id;
- memo_logic_info = id;
- memo_logic_type_info = id;
- memo_stmt = id;
- memo_fieldinfo = id;
- memo_model_info = id;
- memo_logic_var = id;
- memo_kernel_function = id;
- memo_fundec = id;
- set_varinfo = alphabetaunit;
- set_compinfo = alphabetaunit;
- set_enuminfo = alphabetaunit;
- set_enumitem = alphabetaunit;
- set_typeinfo = alphabetaunit;
- set_logic_info = alphabetaunit;
- set_logic_type_info = alphabetaunit;
- set_stmt = alphabetaunit;
- set_fieldinfo = alphabetaunit;
- set_model_info = alphabetaunit;
- set_logic_var = alphabetaunit;
- set_kernel_function = alphabetaunit;
- set_fundec = alphabetaunit;
- set_orig_varinfo = alphabetaunit;
- set_orig_compinfo = alphabetaunit;
- set_orig_enuminfo = alphabetaunit;
- set_orig_enumitem = alphabetaunit;
- set_orig_typeinfo = alphabetaunit;
- set_orig_logic_info = alphabetaunit;
- set_orig_logic_type_info = alphabetaunit;
- set_orig_stmt = alphabetaunit;
- set_orig_fieldinfo = alphabetaunit;
- set_orig_model_info = alphabetaunit;
- set_orig_logic_var = alphabetaunit;
- set_orig_kernel_function = alphabetaunit;
- set_orig_fundec = alphabetaunit;
- unset_varinfo = alphaunit;
- unset_compinfo = alphaunit;
- unset_enuminfo = alphaunit;
- unset_enumitem = alphaunit;
- unset_typeinfo = alphaunit;
- unset_logic_info = alphaunit;
- unset_logic_type_info = alphaunit;
- unset_stmt = alphaunit;
- unset_fieldinfo = alphaunit;
- unset_model_info = alphaunit;
- unset_logic_var = alphaunit;
- unset_kernel_function = alphaunit;
- unset_fundec = alphaunit;
- unset_orig_varinfo = alphaunit;
- unset_orig_compinfo = alphaunit;
- unset_orig_enuminfo = alphaunit;
- unset_orig_enumitem = alphaunit;
- unset_orig_typeinfo = alphaunit;
- unset_orig_logic_info = alphaunit;
- unset_orig_logic_type_info = alphaunit;
- unset_orig_stmt = alphaunit;
- unset_orig_fieldinfo = alphaunit;
- unset_orig_model_info = alphaunit;
- unset_orig_logic_var = alphaunit;
- unset_orig_kernel_function = alphaunit;
- unset_orig_fundec = alphaunit;
- reset_behavior_varinfo = unitunit;
- reset_behavior_compinfo = unitunit;
- reset_behavior_enuminfo = unitunit;
- reset_behavior_enumitem = unitunit;
- reset_behavior_typeinfo = unitunit;
- reset_behavior_logic_info = unitunit;
- reset_behavior_logic_type_info = unitunit;
- reset_behavior_fieldinfo = unitunit;
- reset_behavior_model_info = unitunit;
- reset_behavior_stmt = unitunit;
- reset_logic_var = unitunit;
- reset_behavior_kernel_function = unitunit;
- reset_behavior_fundec = unitunit;
- iter_visitor_varinfo = alphaunit;
- iter_visitor_compinfo = alphaunit;
- iter_visitor_enuminfo = alphaunit;
- iter_visitor_enumitem = alphaunit;
- iter_visitor_typeinfo = alphaunit;
- iter_visitor_stmt = alphaunit;
- iter_visitor_logic_info = alphaunit;
- iter_visitor_logic_type_info = alphaunit;
- iter_visitor_fieldinfo = alphaunit;
- iter_visitor_model_info = alphaunit;
- iter_visitor_logic_var = alphaunit;
- iter_visitor_kernel_function = alphaunit;
- iter_visitor_fundec = alphaunit;
- fold_visitor_varinfo = alphabetabeta;
- fold_visitor_compinfo = alphabetabeta;
- fold_visitor_enuminfo = alphabetabeta;
- fold_visitor_enumitem = alphabetabeta;
- fold_visitor_typeinfo = alphabetabeta;
- fold_visitor_stmt = alphabetabeta;
- fold_visitor_logic_info = alphabetabeta;
- fold_visitor_logic_type_info = alphabetabeta;
- fold_visitor_fieldinfo = alphabetabeta;
- fold_visitor_model_info = alphabetabeta;
- fold_visitor_logic_var = alphabetabeta;
- fold_visitor_kernel_function = alphabetabeta;
- fold_visitor_fundec = alphabetabeta;
- }
-
-let copy_visit_gen fresh prj =
- let varinfos = Cil_datatype.Varinfo.Hashtbl.create 103 in
- let compinfos = Cil_datatype.Compinfo.Hashtbl.create 17 in
- let enuminfos = Cil_datatype.Enuminfo.Hashtbl.create 17 in
- let enumitems = Cil_datatype.Enumitem.Hashtbl.create 17 in
- let typeinfos = Cil_datatype.Typeinfo.Hashtbl.create 17 in
- let logic_infos = Cil_datatype.Logic_info.Hashtbl.create 17 in
- let logic_type_infos = Cil_datatype.Logic_type_info.Hashtbl.create 17 in
- let fieldinfos = Cil_datatype.Fieldinfo.Hashtbl.create 17 in
- let model_infos = Cil_datatype.Model_info.Hashtbl.create 17 in
- let stmts = Cil_datatype.Stmt.Hashtbl.create 103 in
- let logic_vars = Cil_datatype.Logic_var.Hashtbl.create 17 in
- let kernel_functions = Cil_datatype.Kf.Hashtbl.create 17 in
- let fundecs = Cil_datatype.Varinfo.Hashtbl.create 17 in
- let orig_varinfos = Cil_datatype.Varinfo.Hashtbl.create 103 in
- let orig_compinfos = Cil_datatype.Compinfo.Hashtbl.create 17 in
- let orig_enuminfos = Cil_datatype.Enuminfo.Hashtbl.create 17 in
- let orig_enumitems = Cil_datatype.Enumitem.Hashtbl.create 17 in
- let orig_typeinfos = Cil_datatype.Typeinfo.Hashtbl.create 17 in
- let orig_logic_infos = Cil_datatype.Logic_info.Hashtbl.create 17 in
- let orig_logic_type_infos = Cil_datatype.Logic_type_info.Hashtbl.create 17 in
- let orig_fieldinfos = Cil_datatype.Fieldinfo.Hashtbl.create 17 in
- let orig_model_infos = Cil_datatype.Model_info.Hashtbl.create 17 in
- let orig_stmts = Cil_datatype.Stmt.Hashtbl.create 103 in
- let orig_logic_vars = Cil_datatype.Logic_var.Hashtbl.create 17 in
- let orig_kernel_functions = Cil_datatype.Kf.Hashtbl.create 17 in
- let orig_fundecs = Cil_datatype.Varinfo.Hashtbl.create 17 in
- let temp_set_logic_var x new_x =
- Cil_datatype.Logic_var.Hashtbl.add logic_vars x new_x
- in
- let temp_set_orig_logic_var new_x x =
- Cil_datatype.Logic_var.Hashtbl.add orig_logic_vars new_x x
- in
- let temp_unset_logic_var x =
- Cil_datatype.Logic_var.Hashtbl.remove logic_vars x
- in
- let temp_unset_orig_logic_var new_x =
- Cil_datatype.Logic_var.Hashtbl.remove orig_logic_vars new_x
- in
- let temp_memo_logic_var x =
- (* Format.printf "search for %s#%d@." x.lv_name x.lv_id;*)
- let res =
- try Cil_datatype.Logic_var.Hashtbl.find logic_vars x
- with Not_found ->
- (* Format.printf "Not found@.";*)
- let id = if fresh then Cil_const.new_raw_id () else x.lv_id in
- let new_x = { x with lv_id = id } in
- temp_set_logic_var x new_x; temp_set_orig_logic_var new_x x; new_x
- in
- (* Format.printf "res is %s#%d@." res.lv_name res.lv_id;*)
- res
- in
- let temp_set_varinfo x new_x =
- Cil_datatype.Varinfo.Hashtbl.add varinfos x new_x;
- match x.vlogic_var_assoc, new_x.vlogic_var_assoc with
- | None, _ | _, None -> ()
- | Some lx, Some new_lx ->
- Cil_datatype.Logic_var.Hashtbl.add logic_vars lx new_lx
- in
- let temp_set_orig_varinfo new_x x =
- Cil_datatype.Varinfo.Hashtbl.add orig_varinfos new_x x;
- match new_x.vlogic_var_assoc, x.vlogic_var_assoc with
- | None, _ | _, None -> ()
- | Some new_lx, Some lx ->
- Cil_datatype.Logic_var.Hashtbl.add orig_logic_vars new_lx lx
- in
- let temp_unset_varinfo x =
- Cil_datatype.Varinfo.Hashtbl.remove varinfos x;
- match x.vlogic_var_assoc with
- | None -> ()
- | Some lx -> Cil_datatype.Logic_var.Hashtbl.remove logic_vars lx
- in
- let temp_unset_orig_varinfo new_x =
- Cil_datatype.Varinfo.Hashtbl.remove orig_varinfos new_x;
- match new_x.vlogic_var_assoc with
- | None -> ()
- | Some new_lx ->
- Cil_datatype.Logic_var.Hashtbl.remove orig_logic_vars new_lx
- in
- let temp_memo_varinfo x =
- try Cil_datatype.Varinfo.Hashtbl.find varinfos x
- with Not_found ->
- let new_x =
- if fresh then Cil_const.copy_with_new_vid x else begin
- let new_x = { x with vid = x.vid } in
- (match x.vlogic_var_assoc with
- | None -> ()
- | Some lv ->
- let new_lv = { lv with lv_origin = Some new_x } in
- new_x.vlogic_var_assoc <- Some new_lv);
- new_x
- end
- in
- temp_set_varinfo x new_x; temp_set_orig_varinfo new_x x; new_x
- in
- let temp_set_fundec f new_f =
- Cil_datatype.Varinfo.Hashtbl.add fundecs f.svar new_f
- in
- let temp_set_orig_fundec new_f f =
- Cil_datatype.Varinfo.Hashtbl.add orig_fundecs new_f.svar f
- in
- let temp_unset_fundec f =
- Cil_datatype.Varinfo.Hashtbl.remove fundecs f.svar
- in
- let temp_unset_orig_fundec new_f =
- Cil_datatype.Varinfo.Hashtbl.remove orig_fundecs new_f.svar
- in
- let temp_memo_fundec f =
- try Cil_datatype.Varinfo.Hashtbl.find fundecs f.svar
- with Not_found ->
- let v = temp_memo_varinfo f.svar in
- let new_f = { f with svar = v } in
- temp_set_fundec f new_f; temp_set_orig_fundec new_f f; new_f
- in
- let temp_set_kernel_function kf new_kf =
- Cil_datatype.Kf.Hashtbl.replace kernel_functions kf new_kf;
- match kf.fundec, new_kf.fundec with
- | Declaration(_,vi,_,_), Declaration(_,new_vi,_,_)
- | Declaration(_,vi,_,_), Definition({ svar = new_vi }, _)
- | Definition({svar = vi},_), Declaration(_,new_vi,_,_) ->
- temp_set_varinfo vi new_vi
- | Definition (fundec,_), Definition(new_fundec,_) ->
- temp_set_fundec fundec new_fundec
- in
- let temp_set_orig_kernel_function new_kf kf =
- Cil_datatype.Kf.Hashtbl.replace orig_kernel_functions new_kf kf;
- match new_kf.fundec, kf.fundec with
- | Declaration(_,new_vi,_,_), Declaration(_,vi,_,_)
- | Declaration(_,new_vi,_,_), Definition({ svar = vi }, _)
- | Definition({svar = new_vi},_), Declaration(_,vi,_,_) ->
- temp_set_orig_varinfo new_vi vi
- | Definition (new_fundec,_), Definition(fundec,_) ->
- temp_set_orig_fundec new_fundec fundec
- in
- let temp_unset_kernel_function kf =
- Cil_datatype.Kf.Hashtbl.remove kernel_functions kf;
- match kf.fundec with
- | Declaration(_,vi,_,_) -> temp_unset_varinfo vi
- | Definition (fundec,_) -> temp_unset_fundec fundec
- in
- let temp_unset_orig_kernel_function new_kf =
- Cil_datatype.Kf.Hashtbl.remove orig_kernel_functions new_kf;
- match new_kf.fundec with
- | Declaration(_,new_vi,_,_) -> temp_unset_orig_varinfo new_vi
- | Definition (new_fundec,_) -> temp_unset_orig_fundec new_fundec
- in
- let temp_memo_kernel_function kf =
- try Cil_datatype.Kf.Hashtbl.find kernel_functions kf
- with Not_found ->
- let new_kf =
- match kf.fundec with
- | Declaration (spec,vi,prms,loc) ->
- let new_vi = temp_memo_varinfo vi in
- { kf with fundec = Declaration(spec,new_vi,prms,loc) }
- | Definition(f,loc) ->
- let new_f = temp_memo_fundec f in
- { kf with fundec = Definition(new_f,loc) }
- in
- temp_set_kernel_function kf new_kf;
- temp_set_orig_kernel_function new_kf kf;
- new_kf
- in
- let temp_set_compinfo c new_c =
- Cil_datatype.Compinfo.Hashtbl.add compinfos c new_c;
- List.iter2
- (fun f new_f -> Cil_datatype.Fieldinfo.Hashtbl.add fieldinfos f new_f)
- c.cfields new_c.cfields
- in
- let temp_set_orig_compinfo new_c c =
- Cil_datatype.Compinfo.Hashtbl.add orig_compinfos new_c c;
- List.iter2
- (fun new_f f ->
- Cil_datatype.Fieldinfo.Hashtbl.add orig_fieldinfos new_f f)
- new_c.cfields c.cfields
- in
- let temp_unset_compinfo c =
- Cil_datatype.Compinfo.Hashtbl.remove compinfos c;
- List.iter
- (fun f -> Cil_datatype.Fieldinfo.Hashtbl.remove fieldinfos f) c.cfields
- in
- let temp_unset_orig_compinfo new_c =
- Cil_datatype.Compinfo.Hashtbl.remove orig_compinfos new_c;
- List.iter
- (fun new_f ->
- Cil_datatype.Fieldinfo.Hashtbl.remove orig_fieldinfos new_f)
- new_c.cfields
- in
- let temp_memo_compinfo c =
- try Cil_datatype.Compinfo.Hashtbl.find compinfos c
- with Not_found ->
- let new_c =
- copyCompInfo ~fresh c c.cname
- in
- temp_set_compinfo c new_c; temp_set_orig_compinfo new_c c; new_c
- in
- { cfile = (fun x -> { x with fileName = x.fileName });
- get_compinfo =
- (fun x ->
- try Cil_datatype.Compinfo.Hashtbl.find compinfos x with Not_found -> x);
- get_fieldinfo =
- (fun x ->
- try Cil_datatype.Fieldinfo.Hashtbl.find fieldinfos x
- with Not_found -> x);
- get_model_info =
- (fun x ->
- try Cil_datatype.Model_info.Hashtbl.find model_infos x
- with Not_found -> x);
- get_enuminfo =
- (fun x ->
- try Cil_datatype.Enuminfo.Hashtbl.find enuminfos x with Not_found -> x);
- get_enumitem =
- (fun x ->
- try Cil_datatype.Enumitem.Hashtbl.find enumitems x with Not_found -> x);
- get_typeinfo =
- (fun x ->
- try Cil_datatype.Typeinfo.Hashtbl.find typeinfos x with Not_found -> x);
- get_varinfo =
- (fun x ->
- try Cil_datatype.Varinfo.Hashtbl.find varinfos x with Not_found -> x);
- get_stmt =
- (fun x -> try Cil_datatype.Stmt.Hashtbl.find stmts x with Not_found -> x);
- get_logic_info =
- (fun x ->
- try Cil_datatype.Logic_info.Hashtbl.find logic_infos x
- with Not_found -> x);
- get_logic_type_info =
- (fun x ->
- try Cil_datatype.Logic_type_info.Hashtbl.find logic_type_infos x
- with Not_found -> x);
- get_logic_var =
- (fun x ->
- try Cil_datatype.Logic_var.Hashtbl.find logic_vars x
- with Not_found -> x);
- get_kernel_function =
- (fun x ->
- try Cil_datatype.Kf.Hashtbl.find kernel_functions x
- with Not_found -> x);
- get_fundec =
- (fun x ->
- try Cil_datatype.Varinfo.Hashtbl.find fundecs x.svar
- with Not_found -> x);
- get_original_compinfo =
- (fun x ->
- try Cil_datatype.Compinfo.Hashtbl.find orig_compinfos x
- with Not_found -> x);
- get_original_fieldinfo =
- (fun x ->
- try Cil_datatype.Fieldinfo.Hashtbl.find orig_fieldinfos x
- with Not_found -> x);
- get_original_model_info =
- (fun x ->
- try Cil_datatype.Model_info.Hashtbl.find orig_model_infos x
- with Not_found -> x);
- get_original_enuminfo =
- (fun x ->
- try Cil_datatype.Enuminfo.Hashtbl.find orig_enuminfos x
- with Not_found -> x);
- get_original_enumitem =
- (fun x ->
- try Cil_datatype.Enumitem.Hashtbl.find orig_enumitems x
- with Not_found -> x);
- get_original_typeinfo =
- (fun x ->
- try Cil_datatype.Typeinfo.Hashtbl.find orig_typeinfos x
- with Not_found -> x);
- get_original_varinfo =
- (fun x ->
- try Cil_datatype.Varinfo.Hashtbl.find orig_varinfos x
- with Not_found -> x);
- get_original_stmt =
- (fun x ->
- try Cil_datatype.Stmt.Hashtbl.find orig_stmts x with Not_found -> x);
- get_original_logic_var =
- (fun x ->
- try Cil_datatype.Logic_var.Hashtbl.find orig_logic_vars x
- with Not_found -> x);
- get_original_logic_info =
- (fun x ->
- try Cil_datatype.Logic_info.Hashtbl.find orig_logic_infos x
- with Not_found -> x);
- get_original_logic_type_info =
- (fun x ->
- try Cil_datatype.Logic_type_info.Hashtbl.find orig_logic_type_infos x
- with Not_found -> x);
- get_original_kernel_function =
- (fun x ->
- try Cil_datatype.Kf.Hashtbl.find orig_kernel_functions x
- with Not_found -> x);
- get_original_fundec =
- (fun x ->
- try Cil_datatype.Varinfo.Hashtbl.find orig_fundecs x.svar
- with Not_found -> x);
- cinitinfo = (fun x -> { init = x.init });
- cblock = (fun x -> { x with battrs = x.battrs });
- cfunspec = (fun x -> { x with spec_behavior = x.spec_behavior});
- cfunbehavior = (fun x -> { x with b_name = x.b_name});
- ccode_annotation =
- if fresh then Logic_const.refresh_code_annotation
- else (fun x -> { x with annot_id = x.annot_id });
- cidentified_predicate =
- if fresh then Logic_const.refresh_predicate
- else (fun x -> { x with ip_id = x.ip_id });
- cidentified_term =
- if fresh then Logic_const.refresh_identified_term
- else (fun x -> { x with it_id = x.it_id});
- cexpr =
- (fun x ->
- let id = if fresh then Eid.next () else x.eid in { x with eid = id });
- is_copy_behavior = true;
- is_fresh_behavior = fresh;
- project = Some prj;
- reset_behavior_varinfo =
- (fun () ->
- Cil_datatype.Varinfo.Hashtbl.clear varinfos;
- Cil_datatype.Varinfo.Hashtbl.clear orig_varinfos);
- reset_behavior_compinfo =
- (fun () ->
- Cil_datatype.Compinfo.Hashtbl.clear compinfos;
- Cil_datatype.Compinfo.Hashtbl.clear orig_compinfos);
- reset_behavior_enuminfo =
- (fun () ->
- Cil_datatype.Enuminfo.Hashtbl.clear enuminfos;
- Cil_datatype.Enuminfo.Hashtbl.clear orig_enuminfos);
- reset_behavior_enumitem =
- (fun () ->
- Cil_datatype.Enumitem.Hashtbl.clear enumitems;
- Cil_datatype.Enumitem.Hashtbl.clear orig_enumitems);
- reset_behavior_typeinfo =
- (fun () ->
- Cil_datatype.Typeinfo.Hashtbl.clear typeinfos;
- Cil_datatype.Typeinfo.Hashtbl.clear orig_typeinfos);
- reset_behavior_logic_info =
- (fun () ->
- Cil_datatype.Logic_info.Hashtbl.clear logic_infos;
- Cil_datatype.Logic_info.Hashtbl.clear orig_logic_infos);
- reset_behavior_logic_type_info =
- (fun () ->
- Cil_datatype.Logic_type_info.Hashtbl.clear logic_type_infos;
- Cil_datatype.Logic_type_info.Hashtbl.clear orig_logic_type_infos);
- reset_behavior_fieldinfo =
- (fun () ->
- Cil_datatype.Fieldinfo.Hashtbl.clear fieldinfos;
- Cil_datatype.Fieldinfo.Hashtbl.clear orig_fieldinfos);
- reset_behavior_model_info =
- (fun () ->
- Cil_datatype.Model_info.Hashtbl.clear model_infos;
- Cil_datatype.Model_info.Hashtbl.clear orig_model_infos);
- reset_behavior_stmt =
- (fun () ->
- Cil_datatype.Stmt.Hashtbl.clear stmts;
- Cil_datatype.Stmt.Hashtbl.clear orig_stmts);
- reset_logic_var =
- (fun () ->
- Cil_datatype.Logic_var.Hashtbl.clear logic_vars;
- Cil_datatype.Logic_var.Hashtbl.clear orig_logic_vars);
- reset_behavior_kernel_function =
- (fun () ->
- Cil_datatype.Kf.Hashtbl.clear kernel_functions;
- Cil_datatype.Kf.Hashtbl.clear orig_kernel_functions);
- reset_behavior_fundec =
- (fun () ->
- Cil_datatype.Varinfo.Hashtbl.clear fundecs;
- Cil_datatype.Varinfo.Hashtbl.clear orig_fundecs);
- memo_varinfo = temp_memo_varinfo;
- memo_compinfo = temp_memo_compinfo;
- memo_enuminfo =
- (fun x ->
- try Cil_datatype.Enuminfo.Hashtbl.find enuminfos x
- with Not_found ->
- let new_x = { x with ename = x.ename } in
- Cil_datatype.Enuminfo.Hashtbl.add enuminfos x new_x;
- Cil_datatype.Enuminfo.Hashtbl.add orig_enuminfos new_x x;
- new_x);
- memo_enumitem =
- (fun x ->
- try Cil_datatype.Enumitem.Hashtbl.find enumitems x
- with Not_found ->
- let new_x = { x with einame = x.einame } in
- Cil_datatype.Enumitem.Hashtbl.add enumitems x new_x;
- Cil_datatype.Enumitem.Hashtbl.add orig_enumitems new_x x;
- new_x);
- memo_typeinfo =
- (fun x ->
- try Cil_datatype.Typeinfo.Hashtbl.find typeinfos x
- with Not_found ->
- let new_x = { x with tname = x.tname } in
- Cil_datatype.Typeinfo.Hashtbl.add typeinfos x new_x;
- Cil_datatype.Typeinfo.Hashtbl.add orig_typeinfos new_x x;
- new_x);
- memo_logic_info =
- (fun x ->
- try Cil_datatype.Logic_info.Hashtbl.find logic_infos x
- with Not_found ->
- let new_v = temp_memo_logic_var x.l_var_info in
- let new_x = { x with l_var_info = new_v } in
- Cil_datatype.Logic_info.Hashtbl.add logic_infos x new_x;
- Cil_datatype.Logic_info.Hashtbl.add orig_logic_infos new_x x;
- new_x);
- memo_logic_type_info =
- (fun x ->
- try Cil_datatype.Logic_type_info.Hashtbl.find logic_type_infos x
- with Not_found ->
- let new_x = { x with lt_name = x.lt_name } in
- Cil_datatype.Logic_type_info.Hashtbl.add logic_type_infos x new_x;
- Cil_datatype.Logic_type_info.Hashtbl.add
- orig_logic_type_infos new_x x;
- new_x);
- memo_stmt =
- (fun x ->
- try Cil_datatype.Stmt.Hashtbl.find stmts x
- with Not_found ->
- let sid = if fresh then Sid.next () else x.sid in
- let new_x = { x with sid = sid } in
- Cil_datatype.Stmt.Hashtbl.add stmts x new_x;
- Cil_datatype.Stmt.Hashtbl.add orig_stmts new_x x;
- new_x);
- memo_fieldinfo =
- (fun x ->
- try Cil_datatype.Fieldinfo.Hashtbl.find fieldinfos x
- with Not_found ->
- let _ = temp_memo_compinfo x.fcomp in
- (* memo_compinfo fills the field correspondence table as well *)
- let new_x = Cil_datatype.Fieldinfo.Hashtbl.find fieldinfos x in
- Cil_datatype.Fieldinfo.Hashtbl.add fieldinfos x new_x;
- Cil_datatype.Fieldinfo.Hashtbl.add orig_fieldinfos new_x x;
- new_x);
- memo_model_info =
- (fun x ->
- try Cil_datatype.Model_info.Hashtbl.find model_infos x
- with Not_found ->
- let new_x = { x with mi_name = x.mi_name } in
- Cil_datatype.Model_info.Hashtbl.add model_infos x new_x;
- Cil_datatype.Model_info.Hashtbl.add orig_model_infos new_x x;
- new_x
- );
- memo_logic_var = temp_memo_logic_var;
- memo_kernel_function = temp_memo_kernel_function;
- memo_fundec = temp_memo_fundec;
- set_varinfo = temp_set_varinfo;
- set_compinfo = temp_set_compinfo;
- set_enuminfo = Cil_datatype.Enuminfo.Hashtbl.replace enuminfos;
- set_enumitem = Cil_datatype.Enumitem.Hashtbl.replace enumitems;
- set_typeinfo = Cil_datatype.Typeinfo.Hashtbl.replace typeinfos;
- set_logic_info = Cil_datatype.Logic_info.Hashtbl.replace logic_infos;
- set_logic_type_info =
- Cil_datatype.Logic_type_info.Hashtbl.replace logic_type_infos;
- set_stmt = Cil_datatype.Stmt.Hashtbl.replace stmts;
- set_fieldinfo = Cil_datatype.Fieldinfo.Hashtbl.replace fieldinfos;
- set_model_info = Cil_datatype.Model_info.Hashtbl.replace model_infos;
- set_logic_var = temp_set_logic_var;
- set_kernel_function = temp_set_kernel_function;
- set_fundec = temp_set_fundec;
- set_orig_varinfo = temp_set_orig_varinfo;
- set_orig_compinfo = temp_set_orig_compinfo;
- set_orig_enuminfo = Cil_datatype.Enuminfo.Hashtbl.replace orig_enuminfos;
- set_orig_enumitem = Cil_datatype.Enumitem.Hashtbl.replace orig_enumitems;
- set_orig_typeinfo = Cil_datatype.Typeinfo.Hashtbl.replace orig_typeinfos;
- set_orig_logic_info =
- Cil_datatype.Logic_info.Hashtbl.replace orig_logic_infos;
- set_orig_logic_type_info =
- Cil_datatype.Logic_type_info.Hashtbl.replace orig_logic_type_infos;
- set_orig_stmt = Cil_datatype.Stmt.Hashtbl.replace orig_stmts;
- set_orig_fieldinfo =
- Cil_datatype.Fieldinfo.Hashtbl.replace orig_fieldinfos;
- set_orig_model_info =
- Cil_datatype.Model_info.Hashtbl.replace orig_model_infos;
- set_orig_logic_var = temp_set_orig_logic_var;
- set_orig_kernel_function = temp_set_orig_kernel_function;
- set_orig_fundec = temp_set_orig_fundec;
-
- unset_varinfo = temp_unset_varinfo;
- unset_compinfo = temp_unset_compinfo;
- unset_enuminfo = Cil_datatype.Enuminfo.Hashtbl.remove enuminfos;
- unset_enumitem = Cil_datatype.Enumitem.Hashtbl.remove enumitems;
- unset_typeinfo = Cil_datatype.Typeinfo.Hashtbl.remove typeinfos;
- unset_logic_info = Cil_datatype.Logic_info.Hashtbl.remove logic_infos;
- unset_logic_type_info =
- Cil_datatype.Logic_type_info.Hashtbl.remove logic_type_infos;
- unset_stmt = Cil_datatype.Stmt.Hashtbl.remove stmts;
- unset_fieldinfo = Cil_datatype.Fieldinfo.Hashtbl.remove fieldinfos;
- unset_model_info = Cil_datatype.Model_info.Hashtbl.remove model_infos;
- unset_logic_var = temp_unset_logic_var;
- unset_kernel_function = temp_unset_kernel_function;
- unset_fundec = temp_unset_fundec;
-
- unset_orig_varinfo = temp_unset_orig_varinfo;
- unset_orig_compinfo = temp_unset_orig_compinfo;
- unset_orig_enuminfo = Cil_datatype.Enuminfo.Hashtbl.remove orig_enuminfos;
- unset_orig_enumitem = Cil_datatype.Enumitem.Hashtbl.remove orig_enumitems;
- unset_orig_typeinfo = Cil_datatype.Typeinfo.Hashtbl.remove orig_typeinfos;
- unset_orig_logic_info =
- Cil_datatype.Logic_info.Hashtbl.remove orig_logic_infos;
- unset_orig_logic_type_info =
- Cil_datatype.Logic_type_info.Hashtbl.remove orig_logic_type_infos;
- unset_orig_stmt = Cil_datatype.Stmt.Hashtbl.remove orig_stmts;
- unset_orig_fieldinfo =
- Cil_datatype.Fieldinfo.Hashtbl.remove orig_fieldinfos;
- unset_orig_model_info =
- Cil_datatype.Model_info.Hashtbl.remove orig_model_infos;
- unset_orig_logic_var = temp_unset_orig_logic_var;
- unset_orig_kernel_function = temp_unset_orig_kernel_function;
- unset_orig_fundec = temp_unset_orig_fundec;
-
- iter_visitor_varinfo =
- (fun f -> Cil_datatype.Varinfo.Hashtbl.iter f varinfos);
- iter_visitor_compinfo =
- (fun f -> Cil_datatype.Compinfo.Hashtbl.iter f compinfos);
- iter_visitor_enuminfo =
- (fun f -> Cil_datatype.Enuminfo.Hashtbl.iter f enuminfos);
- iter_visitor_enumitem =
- (fun f -> Cil_datatype.Enumitem.Hashtbl.iter f enumitems);
- iter_visitor_typeinfo =
- (fun f -> Cil_datatype.Typeinfo.Hashtbl.iter f typeinfos);
- iter_visitor_stmt =
- (fun f -> Cil_datatype.Stmt.Hashtbl.iter f stmts);
- iter_visitor_logic_info =
- (fun f -> Cil_datatype.Logic_info.Hashtbl.iter f logic_infos);
- iter_visitor_logic_type_info =
- (fun f -> Cil_datatype.Logic_type_info.Hashtbl.iter f logic_type_infos);
- iter_visitor_fieldinfo =
- (fun f -> Cil_datatype.Fieldinfo.Hashtbl.iter f fieldinfos);
- iter_visitor_model_info =
- (fun f -> Cil_datatype.Model_info.Hashtbl.iter f model_infos);
- iter_visitor_logic_var =
- (fun f -> Cil_datatype.Logic_var.Hashtbl.iter f logic_vars);
- iter_visitor_kernel_function =
- (fun f -> Cil_datatype.Kf.Hashtbl.iter f kernel_functions);
- iter_visitor_fundec =
- (fun f ->
- let f _ new_fundec =
- let old_fundec =
- Cil_datatype.Varinfo.Hashtbl.find orig_fundecs new_fundec.svar
- in
- f old_fundec new_fundec
- in
- Cil_datatype.Varinfo.Hashtbl.iter f fundecs);
- fold_visitor_varinfo =
- (fun f i -> Cil_datatype.Varinfo.Hashtbl.fold f varinfos i);
- fold_visitor_compinfo =
- (fun f i -> Cil_datatype.Compinfo.Hashtbl.fold f compinfos i);
- fold_visitor_enuminfo =
- (fun f i -> Cil_datatype.Enuminfo.Hashtbl.fold f enuminfos i);
- fold_visitor_enumitem =
- (fun f i -> Cil_datatype.Enumitem.Hashtbl.fold f enumitems i);
- fold_visitor_typeinfo =
- (fun f i -> Cil_datatype.Typeinfo.Hashtbl.fold f typeinfos i);
- fold_visitor_stmt =
- (fun f i -> Cil_datatype.Stmt.Hashtbl.fold f stmts i);
- fold_visitor_logic_info =
- (fun f i -> Cil_datatype.Logic_info.Hashtbl.fold f logic_infos i);
- fold_visitor_logic_type_info =
- (fun f i ->
- Cil_datatype.Logic_type_info.Hashtbl.fold f logic_type_infos i);
- fold_visitor_fieldinfo =
- (fun f i -> Cil_datatype.Fieldinfo.Hashtbl.fold f fieldinfos i);
- fold_visitor_model_info =
- (fun f i -> Cil_datatype.Model_info.Hashtbl.fold f model_infos i);
- fold_visitor_logic_var =
- (fun f i -> Cil_datatype.Logic_var.Hashtbl.fold f logic_vars i);
- fold_visitor_kernel_function =
- (fun f i ->
- Cil_datatype.Kf.Hashtbl.fold f kernel_functions i);
- fold_visitor_fundec =
- (fun f i ->
- let f _ new_fundec acc =
- let old_fundec =
- Cil_datatype.Varinfo.Hashtbl.find orig_fundecs new_fundec.svar
- in
- f old_fundec new_fundec acc
- in
- Cil_datatype.Varinfo.Hashtbl.fold f fundecs i);
- }
-
-let copy_visit = copy_visit_gen false
-
-let refresh_visit = copy_visit_gen true
let visitor_tbl = Hashtbl.create 5
@@ -1831,8 +729,7 @@ let register_behavior_extension name ext = Hashtbl.add visitor_tbl name ext
(** A visitor interface for traversing CIL trees. Create instantiations of
* this type by specializing the class {!Cil.nopCilVisitor}. *)
class type cilVisitor = object
-
- method behavior: visitor_behavior
+ method behavior: Visitor_behavior.t
method project: Project.t option
@@ -2013,7 +910,7 @@ class internal_genericCilVisitor current_func behavior queue: cilVisitor =
object(self)
method behavior = behavior
- method project = behavior.project;
+ method project = Visitor_behavior.get_project behavior
method plain_copy_visitor =
let obj =
@@ -2149,7 +1046,7 @@ class genericCilVisitor bhv =
internal_genericCilVisitor current_func bhv queue
class nopCilVisitor = object
- inherit genericCilVisitor (inplace_visit ())
+ inherit genericCilVisitor (Visitor_behavior.inplace ())
end
let apply_on_project ?selection vis f arg =
@@ -2371,14 +1268,14 @@ let debugVisit = false
let visitCilConst vis c =
match c with
| CEnum ei -> (* In case of deep copy, we must change the enumitem*)
- let ei' = vis#behavior.get_enumitem ei in
+ let ei' = Visitor_behavior.Get.enumitem vis#behavior ei in
if ei' != ei then CEnum ei' else c
| _ -> c
let visitCilLConst vis c =
match c with
| LEnum ei -> (* In case of deep copy, we must change the enumitem*)
- let ei' = vis#behavior.get_enumitem ei in
+ let ei' = Visitor_behavior.Get.enumitem vis#behavior ei in
if ei' != ei then LEnum ei' else c
| _ -> c
@@ -2531,12 +1428,12 @@ and childrenTermNode vis tn =
and visitCilLogicLabel vis l =
doVisitCil vis
- (copy_logic_label vis#behavior.is_copy_behavior)
+ (copy_logic_label (Visitor_behavior.is_copy vis#behavior))
vis#vlogic_label childrenLogicLabel l
and childrenLogicLabel vis l =
match l with
- StmtLabel s -> s := vis#behavior.get_stmt !s; l
+ StmtLabel s -> s := Visitor_behavior.Get.stmt vis#behavior !s; l
| FormalLabel _ | BuiltinLabel _ -> l
and visitCilTermLval vis tl =
@@ -2569,21 +1466,21 @@ and childrenTermOffset vis toff =
TNoOffset -> toff
| TField (fi, t) ->
let t' = vOffset t in
- let fi' = vis#behavior.get_fieldinfo fi in
+ let fi' = Visitor_behavior.Get.fieldinfo vis#behavior fi in
if t' != t || fi != fi' then TField(fi',t') else toff
| TIndex(t,o) ->
let t' = vTerm t in let o' = vOffset o in
if t' != t || o' != o then TIndex(t',o') else toff
| TModel (mi,t) ->
let t' = vOffset t in
- let mi' = vis#behavior.get_model_info mi in
+ let mi' = Visitor_behavior.Get.model_info vis#behavior mi in
if t' != t || mi != mi' then TModel(mi', t') else toff
and visitCilLogicInfoUse vis li =
(* First, visit the underlying varinfo to fill the copy tables if needed. *)
let new_v = visitCilLogicVarUse vis li.l_var_info in
let new_li =
- doVisitCil vis vis#behavior.get_logic_info
+ doVisitCil vis (Visitor_behavior.Get.logic_info vis#behavior)
vis#vlogic_info_use alphabetabeta li
in
new_li.l_var_info <- new_v;
@@ -2596,7 +1493,7 @@ and visitCilLogicInfo vis li =
let new_v = visitCilLogicVarDecl vis li.l_var_info in
let res =
doVisitCil
- vis vis#behavior.memo_logic_info
+ vis (Visitor_behavior.Memo.logic_info vis#behavior)
vis#vlogic_info_decl childrenLogicInfo li
in res.l_var_info <- new_v; res
@@ -2631,7 +1528,7 @@ and childrenLogicInfo vis li =
li
and visitCilLogicTypeInfo vis lt =
- doVisitCil vis vis#behavior.memo_logic_type_info
+ doVisitCil vis (Visitor_behavior.Memo.logic_type_info vis#behavior)
vis#vlogic_type_info_decl childrenLogicTypeInfo lt
and childrenLogicTypeInfo vis lt =
@@ -2652,7 +1549,7 @@ and childrenLogicTypeDef vis def =
and visitCilLogicCtorInfoAddTable vis ctor =
let ctor' = visitCilLogicCtorInfo vis ctor in
- if is_copy_behavior vis#behavior then
+ if Visitor_behavior.is_copy vis#behavior then
Queue.add
(fun () ->
Logic_env.add_logic_ctor ctor'.ctor_name ctor')
@@ -2663,7 +1560,7 @@ and visitCilLogicCtorInfo vis ctor =
doVisitCil vis id vis#vlogic_ctor_info_decl childrenLogicCtorInfo ctor
and childrenLogicCtorInfo vis ctor =
- let ctor_type = doVisitCil vis vis#behavior.get_logic_type_info
+ let ctor_type = doVisitCil vis (Visitor_behavior.Get.logic_type_info vis#behavior)
vis#vlogic_type_info_use alphabetabeta ctor.ctor_type
in
let ctor_params = ctor.ctor_params in
@@ -2682,7 +1579,7 @@ and childrenLogicType vis ty =
if t != t' then Ctype t' else ty
| Linteger | Lreal -> ty
| Ltype (s,l) ->
- let s' = doVisitCil vis vis#behavior.get_logic_type_info
+ let s' = doVisitCil vis (Visitor_behavior.Get.logic_type_info vis#behavior)
vis#vlogic_type_info_use alphabetabeta s in
let l' = mapNoCopy (visitCilLogicType vis) l in
if s' != s || l' != l then Ltype (s',l') else ty
@@ -2697,7 +1594,7 @@ and visitCilLogicVarDecl vis lv =
(match lv.lv_origin with
None -> ()
| Some cv -> lv.lv_name <- cv.vname);
- doVisitCil vis vis#behavior.memo_logic_var vis#vlogic_var_decl
+ doVisitCil vis (Visitor_behavior.Memo.logic_var vis#behavior) vis#vlogic_var_decl
childrenLogicVarDecl lv
and childrenLogicVarDecl vis lv =
@@ -2707,7 +1604,7 @@ and childrenLogicVarDecl vis lv =
lv
and visitCilLogicVarUse vis lv =
- if vis#behavior.is_copy_behavior &&
+ if Visitor_behavior.is_copy vis#behavior &&
(* In a copy visitor, there's always a project. Furthermore, if
we target the current project, builtins are by definition already
tied to logic_infos and should not be copied.
@@ -2735,7 +1632,7 @@ and visitCilLogicVarUse vis lv =
end)
vis#get_filling_actions;
end;
- doVisitCil vis vis#behavior.get_logic_var vis#vlogic_var_use
+ doVisitCil vis (Visitor_behavior.Get.logic_var vis#behavior) vis#vlogic_var_use
childrenLogicVarUse lv
and childrenLogicVarUse vis lv =
@@ -2748,7 +1645,7 @@ and visitCilQuantifiers vis lv =
and visitCilIdPredicate vis ip =
doVisitCil
vis
- vis#behavior.cidentified_predicate
+ (Visitor_behavior.cidentified_predicate vis#behavior)
vis#videntified_predicate
childrenIdentified_predicate
ip
@@ -2888,7 +1785,7 @@ and childrenPredicateNode vis p =
if t' != t || n' != n || s1 != s1' || s2 != s2' then Pfresh (s1',s2',t',n') else p
and visitCilIdTerm vis loc =
- doVisitCil vis vis#behavior.cidentified_term vis#videntified_term
+ doVisitCil vis (Visitor_behavior.cidentified_term vis#behavior) vis#videntified_term
childrenIdentified_term loc
and childrenIdentified_term vis loc =
let loc' = visitCilTerm vis loc.it_content in
@@ -2937,7 +1834,7 @@ and childrenDeps vis d =
if l !=l' then From l' else d
and visitCilBehavior vis b =
- doVisitCil vis vis#behavior.cfunbehavior
+ doVisitCil vis (Visitor_behavior.cfunbehavior vis#behavior)
vis#vbehavior childrenBehavior b
and childrenBehavior vis b =
@@ -2959,7 +1856,7 @@ and visitCilExtended vis orig =
with Not_found -> (fun _ _ -> DoChildren)
in
let e' = doVisitCil vis id (visit vis) childrenCilExtended orig.ext_kind in
- if is_fresh_behavior vis#behavior then
+ if Visitor_behavior.is_fresh vis#behavior then
Logic_const.new_acsl_extension orig.ext_name orig.ext_loc
orig.ext_has_status e'
else if orig.ext_kind == e' then orig else {orig with ext_kind = e'}
@@ -2979,7 +1876,7 @@ and visitCilPredicates vis ps = mapNoCopy (visitCilIdPredicate vis) ps
and visitCilBehaviors vis bs = mapNoCopy (visitCilBehavior vis) bs
and visitCilFunspec vis s =
- doVisitCil vis vis#behavior.cfunspec vis#vspec childrenSpec s
+ doVisitCil vis (Visitor_behavior.cfunspec vis#behavior) vis#vspec childrenSpec s
and childrenSpec vis s =
s.spec_behavior <- visitCilBehaviors vis s.spec_behavior;
@@ -3042,13 +1939,13 @@ and visitCilModelInfo vis m =
CurrentLoc.set m.mi_decl;
let m' =
doVisitCil
- vis vis#behavior.memo_model_info vis#vmodel_info childrenModelInfo m
+ vis (Visitor_behavior.Memo.model_info vis#behavior) vis#vmodel_info childrenModelInfo m
in
CurrentLoc.set oldloc;
if m' != m then begin
(* reflect changes in the behavior tables for copy visitor. *)
- vis#behavior.set_model_info m m';
- vis#behavior.set_orig_model_info m' m;
+ Visitor_behavior.Set.model_info vis#behavior m m';
+ Visitor_behavior.Set_orig.model_info vis#behavior m' m;
end;
m'
@@ -3063,7 +1960,7 @@ and childrenAnnotation vis a =
match a with
| Dfun_or_pred (li,loc) ->
let li' = visitCilLogicInfo vis li in
- if vis#behavior.is_copy_behavior then
+ if Visitor_behavior.is_copy vis#behavior then
Queue.add
(fun () ->
Logic_env.add_logic_function_gen alphabetafalse li')
@@ -3071,7 +1968,7 @@ and childrenAnnotation vis a =
if li' != li then Dfun_or_pred (li',loc) else a
| Dtype (ti,loc) ->
let ti' = visitCilLogicTypeInfo vis ti in
- if vis#behavior.is_copy_behavior then
+ if Visitor_behavior.is_copy vis#behavior then
Queue.add
(fun () ->
Logic_env.add_logic_type ti'.lt_name ti')
@@ -3085,21 +1982,21 @@ and childrenAnnotation vis a =
else a
| Dinvariant (p,loc) ->
let p' = visitCilLogicInfo vis p in
- if vis#behavior.is_copy_behavior then
+ if Visitor_behavior.is_copy vis#behavior then
Queue.add
(fun () -> Logic_env.add_logic_function_gen alphabetafalse p')
vis#get_filling_actions;
if p' != p then Dinvariant (p',loc) else a
| Dtype_annot (ta,loc) ->
let ta' = visitCilLogicInfo vis ta in
- if vis#behavior.is_copy_behavior then
+ if Visitor_behavior.is_copy vis#behavior then
Queue.add
(fun () -> Logic_env.add_logic_function_gen alphabetafalse ta')
vis#get_filling_actions;
if ta' != ta then Dtype_annot (ta',loc) else a
| Dmodel_annot (mfi,loc) ->
let mfi' = visitCilModelInfo vis mfi in
- if vis#behavior.is_copy_behavior then
+ if Visitor_behavior.is_copy vis#behavior then
Queue.add (fun () -> Logic_env.add_model_field mfi')
vis#get_filling_actions;
if mfi' != mfi then Dmodel_annot (mfi',loc) else a
@@ -3128,7 +2025,7 @@ and childrenAnnotation vis a =
and visitCilCodeAnnotation vis ca =
doVisitCil
- vis vis#behavior.ccode_annotation vis#vcode_annot childrenCodeAnnot ca
+ vis (Visitor_behavior.ccode_annotation vis#behavior) vis#vcode_annot childrenCodeAnnot ca
and childrenCodeAnnot vis ca =
let vPred p = visitCilPredicate vis p in
@@ -3173,7 +2070,7 @@ and childrenCodeAnnot vis ca =
and visitCilExpr (vis: cilVisitor) (e: exp) : exp =
let oldLoc = CurrentLoc.get () in
CurrentLoc.set e.eloc;
- let res = doVisitCil vis vis#behavior.cexpr vis#vexpr childrenExp e in
+ let res = doVisitCil vis (Visitor_behavior.cexpr vis#behavior) vis#vexpr childrenExp e in
CurrentLoc.set oldLoc; res
and childrenExp (vis: cilVisitor) (e: exp) : exp =
@@ -3275,7 +2172,7 @@ and childrenOffset (vis: cilVisitor) (off: offset) : offset =
match off with
Field (f, o) ->
let o' = vOff o in
- let f' = vis#behavior.get_fieldinfo f in
+ let f' = Visitor_behavior.Get.fieldinfo vis#behavior f in
if o' != o || f' != f then Field (f', o') else off
| Index (e, o) ->
let e' = visitCilExpr vis e in
@@ -3356,8 +2253,8 @@ and childrenInstr (vis: cilVisitor) (i: instr) : instr =
if e' != e then (id,s,e') else pair) asm_inputs_pre
in
let asm_gotos =
- if vis#behavior.is_copy_behavior then
- List.map (fun s -> ref (vis#behavior.memo_stmt !s)) ext.asm_gotos
+ if Visitor_behavior.is_copy vis#behavior then
+ List.map (fun s -> ref (Visitor_behavior.Memo.stmt vis#behavior !s)) ext.asm_gotos
else ext.asm_gotos
in
if asm_outputs != asm_outputs_pre
@@ -3381,7 +2278,7 @@ and visitCilStmt (vis:cilVisitor) (s: stmt) : stmt =
let toPrepend : instr list ref = ref [] in (* childrenStmt may add to this *)
let res =
doVisitCil vis
- vis#behavior.memo_stmt vis#vstmt (childrenStmt toPrepend) s in
+ (Visitor_behavior.Memo.stmt vis#behavior) vis#vstmt (childrenStmt toPrepend) s in
let ghost = res.ghost in
(* Now see if we have saved some instructions *)
toPrepend := !toPrepend @ vis#unqueueInstr ();
@@ -3425,9 +2322,9 @@ and childrenStmt (toPrepend: instr list ref) (vis:cilVisitor) (s:stmt): stmt =
let writes' = mapNoCopy (visitCilLval vis) writes in
let reads' = mapNoCopy (visitCilLval vis) reads in
let calls' =
- if vis#behavior.is_copy_behavior then
+ if Visitor_behavior.is_copy vis#behavior then
(* we need new references anyway, no need for mapNoCopy *)
- List.map (fun x -> ref (vis#behavior.memo_stmt !x)) calls
+ List.map (fun x -> ref (Visitor_behavior.Memo.stmt vis#behavior !x)) calls
else calls
in
if stmt' != stmt || writes' != writes || reads' != reads ||
@@ -3439,8 +2336,8 @@ and childrenStmt (toPrepend: instr list ref) (vis:cilVisitor) (s:stmt): stmt =
in
if seq' != seq then UnspecifiedSequence seq' else s.skind
| Goto (sr,l) ->
- if vis#behavior.is_copy_behavior then
- Goto(ref (vis#behavior.memo_stmt !sr),l)
+ if Visitor_behavior.is_copy vis#behavior then
+ Goto(ref (Visitor_behavior.Memo.stmt vis#behavior !sr),l)
else s.skind
| Return (Some e, l) ->
let e' = fExp e in
@@ -3463,7 +2360,7 @@ and childrenStmt (toPrepend: instr list ref) (vis:cilVisitor) (s:stmt): stmt =
let e' = fExp e in
toPrepend := vis#unqueueInstr (); (* insert these before the switch *)
let b' = fBlock b in
- let stmts' = mapNoCopy (vis#behavior.get_stmt) stmts in
+ let stmts' = mapNoCopy (Visitor_behavior.Get.stmt vis#behavior) stmts in
(* the stmts in b should have cleaned up after themselves.*)
assertEmptyQueue vis;
if e' != e || b' != b || stmts' != stmts then
@@ -3545,8 +2442,8 @@ and visitCilCatch_binder vis cb =
if v != v' || l != l' then Catch_exn(v',l') else cb
| Catch_all -> cb
and visitCilBlock (vis: cilVisitor) (b: block) : block =
- let b' = vis#behavior.cblock b in
- if vis#behavior.is_copy_behavior then begin
+ let b' = Visitor_behavior.cblock vis#behavior b in
+ if Visitor_behavior.is_copy vis#behavior then begin
(* in case we are the main block of the current function,
update immediately the sbody, so that makeLocalVar can be used
seamlessly by the underlying visitor and associate the
@@ -3554,7 +2451,7 @@ and visitCilBlock (vis: cilVisitor) (b: block) : block =
*)
match vis#current_func with
| Some fd when fd.sbody == b ->
- (get_fundec vis#behavior fd).sbody <- b'
+ (Visitor_behavior.Get.fundec vis#behavior fd).sbody <- b'
| Some _ | None -> ()
end;
doVisitCil vis id vis#vblock childrenBlock b'
@@ -3564,8 +2461,8 @@ and childrenBlock (vis: cilVisitor) (b: block) : block =
that wish to create a local into the innermost scope can simply append
it to the current block.
*)
- let locals' = mapNoCopy (vis#behavior.get_varinfo) b.blocals in
- let statics' = mapNoCopy (vis#behavior.get_varinfo) b.bstatics in
+ let locals' = mapNoCopy (Visitor_behavior.Get.varinfo vis#behavior) b.blocals in
+ let statics' = mapNoCopy (Visitor_behavior.Get.varinfo vis#behavior) b.bstatics in
b.blocals <- locals';
b.bstatics <- statics';
let stmts' = mapNoCopy fStmt b.bstmts in
@@ -3596,7 +2493,7 @@ and childrenType (vis : cilVisitor) (t : typ) : typ =
(* DON'T recurse into the compinfo, this is done in visitCilGlobal.
User can iterate over cinfo.cfields manually, if desired.*)
| TComp(cinfo, _, a) ->
- let cinfo' = vis#behavior.get_compinfo cinfo in
+ let cinfo' = Visitor_behavior.Get.compinfo vis#behavior cinfo in
let a' = fAttr a in
if a != a' || cinfo' != cinfo then TComp(cinfo',empty_size_cache (), a') else t
@@ -3617,11 +2514,11 @@ and childrenType (vis : cilVisitor) (t : typ) : typ =
| TNamed(t1, a) ->
let a' = fAttr a in
- let t1' = vis#behavior.get_typeinfo t1 in
+ let t1' = Visitor_behavior.Get.typeinfo vis#behavior t1 in
if a' != a || t1' != t1 then TNamed (t1', a') else t
| TEnum(enum,a) ->
let a' = fAttr a in
- let enum' = vis#behavior.get_enuminfo enum in
+ let enum' = Visitor_behavior.Get.enuminfo vis#behavior enum in
if a' != a || enum' != enum then TEnum(enum',a') else t
| TVoid _ | TInt _ | TFloat _ | TBuiltin_va_list _ ->
(* no nested type. visit only the attributes. *)
@@ -3635,7 +2532,7 @@ and visitCilVarDecl (vis : cilVisitor) (v : varinfo) : varinfo =
let oldloc = CurrentLoc.get () in
CurrentLoc.set v.vdecl;
let res =
- doVisitCil vis vis#behavior.memo_varinfo
+ doVisitCil vis (Visitor_behavior.Memo.varinfo vis#behavior)
vis#vvdec childrenVarDecl v
in CurrentLoc.set oldloc; res
@@ -3643,7 +2540,7 @@ and childrenVarDecl (vis : cilVisitor) (v : varinfo) : varinfo =
(* in case of refresh visitor, the associated new logic var has a different
id. We must visit the original logic var associated to it. *)
let visit_orig_var_assoc lv =
- let o = vis#behavior.get_original_logic_var lv in
+ let o = Visitor_behavior.Get_orig.logic_var vis#behavior lv in
visitCilLogicVarDecl vis o
in
v.vtype <- visitCilType vis v.vtype;
@@ -3652,7 +2549,7 @@ and childrenVarDecl (vis : cilVisitor) (v : varinfo) : varinfo =
v
and visitCilVarUse vis v =
- doVisitCil vis vis#behavior.get_varinfo vis#vvrbl alphabetabeta v
+ doVisitCil vis (Visitor_behavior.Get.varinfo vis#behavior) vis#vvrbl alphabetabeta v
and visitCilAttributes (vis: cilVisitor) (al: attribute list) : attribute list=
let al' =
@@ -3726,19 +2623,19 @@ and childrenAttrparam (vis: cilVisitor) (aa: attrparam) : attrparam =
let rec fix_succs_preds_block b block =
List.iter (fix_succs_preds b) block.bstmts
and fix_succs_preds b stmt =
- stmt.succs <- mapNoCopy b.get_stmt stmt.succs;
- stmt.preds <- mapNoCopy b.get_stmt stmt.preds;
+ stmt.succs <- mapNoCopy (Visitor_behavior.Get.stmt b) stmt.succs;
+ stmt.preds <- mapNoCopy (Visitor_behavior.Get.stmt b) stmt.preds;
match stmt.skind with
If(_,bthen,belse,_) ->
fix_succs_preds_block b bthen;
fix_succs_preds_block b belse
| Switch(e,cases,stmts,l) ->
fix_succs_preds_block b cases;
- stmt.skind <- Switch(e,cases,List.map b.get_stmt stmts,l)
+ stmt.skind <- Switch(e,cases,List.map (Visitor_behavior.Get.stmt b) stmts,l)
| Loop(annot,block,loc,stmt1,stmt2) ->
fix_succs_preds_block b block;
- let stmt1' = optMapNoCopy b.get_stmt stmt1 in
- let stmt2' = optMapNoCopy b.get_stmt stmt2 in
+ let stmt1' = optMapNoCopy (Visitor_behavior.Get.stmt b) stmt1 in
+ let stmt2' = optMapNoCopy (Visitor_behavior.Get.stmt b) stmt2 in
stmt.skind <- Loop(annot,block,loc,stmt1',stmt2')
| Block block -> fix_succs_preds_block b block
| TryFinally(block1,block2,_) ->
@@ -3754,7 +2651,7 @@ let rec visitCilFunction (vis : cilVisitor) (f : fundec) : fundec =
assertEmptyQueue vis;
vis#set_current_func f;
(* update fundec tables *)
- let f = vis#behavior.memo_fundec f in
+ let f = Visitor_behavior.Memo.fundec vis#behavior f in
let f =
doVisitCil vis id (* copy has already been done *)
vis#vfunc childrenFunction f
@@ -3763,10 +2660,10 @@ let rec visitCilFunction (vis : cilVisitor) (f : fundec) : fundec =
if toPrepend <> [] then
f.sbody.bstmts <-
(List.map (fun i -> mkStmt (Instr i)) toPrepend) @ f.sbody.bstmts;
- if vis#behavior.is_copy_behavior then begin
+ if Visitor_behavior.is_copy vis#behavior then begin
fix_succs_preds_block vis#behavior f.sbody;
f.sallstmts <-
- List.rev (List.rev_map vis#behavior.get_stmt f.sallstmts)
+ List.rev (List.rev_map (Visitor_behavior.Get.stmt vis#behavior) f.sallstmts)
end;
vis#reset_current_func ();
f
@@ -3775,7 +2672,7 @@ and childrenFunction (vis : cilVisitor) (f : fundec) : fundec =
(* we have already made a copy of the svar, but not visited it.
Use the original variable as argument of visitCilVarDecl,
update fundec table in case the vid gets changed. *)
- let v = vis#behavior.get_original_varinfo f.svar in
+ let v = Visitor_behavior.Get_orig.varinfo vis#behavior f.svar in
let nv = visitCilVarDecl vis v in
if not (Cil_datatype.Varinfo.equal nv f.svar) then begin
Kernel.fatal
@@ -3789,7 +2686,7 @@ and childrenFunction (vis : cilVisitor) (f : fundec) : fundec =
f.slocals <- mapNoCopy (visitCilVarDecl vis) f.slocals;
(* Make sure the type reflects the formals *)
let selection = State_selection.singleton FormalsDecl.self in
- if vis#behavior.is_copy_behavior || newformals != f.sformals then begin
+ if Visitor_behavior.is_copy vis#behavior || newformals != f.sformals then begin
apply_on_project ~selection vis (setFormals f) newformals;
end;
(* Remember any new instructions that were generated while visiting
@@ -3811,8 +2708,8 @@ let childrenFieldInfo vis fi =
fi
let visitCilFieldInfo vis f =
- let f = vis#behavior.get_original_fieldinfo f in
- doVisitCil vis vis#behavior.memo_fieldinfo vis#vfieldinfo childrenFieldInfo f
+ let f = Visitor_behavior.Get_orig.fieldinfo vis#behavior f in
+ doVisitCil vis (Visitor_behavior.Memo.fieldinfo vis#behavior) vis#vfieldinfo childrenFieldInfo f
let childrenCompInfo vis comp =
comp.cfields <- mapNoCopy (visitCilFieldInfo vis) comp.cfields;
@@ -3820,15 +2717,15 @@ let childrenCompInfo vis comp =
comp
let visitCilCompInfo vis c =
- doVisitCil vis vis#behavior.memo_compinfo vis#vcompinfo childrenCompInfo c
+ doVisitCil vis (Visitor_behavior.Memo.compinfo vis#behavior) vis#vcompinfo childrenCompInfo c
let childrenEnumItem vis e =
e.eival <- visitCilExpr vis e.eival;
- e.eihost <- vis#behavior.get_enuminfo e.eihost;
+ e.eihost <- Visitor_behavior.Get.enuminfo vis#behavior e.eihost;
e
let visitCilEnumItem vis e =
- doVisitCil vis vis#behavior.memo_enumitem vis#venumitem childrenEnumItem e
+ doVisitCil vis (Visitor_behavior.Memo.enumitem vis#behavior) vis#venumitem childrenEnumItem e
let childrenEnumInfo vis e =
e.eitems <- mapNoCopy (visitCilEnumItem vis) e.eitems;
@@ -3836,7 +2733,7 @@ let childrenEnumInfo vis e =
e
let visitCilEnumInfo vis e =
- doVisitCil vis vis#behavior.memo_enuminfo vis#venuminfo childrenEnumInfo e
+ doVisitCil vis (Visitor_behavior.Memo.enuminfo vis#behavior) vis#venuminfo childrenEnumInfo e
let rec visitCilGlobal (vis: cilVisitor) (g: global) : global list =
let oldloc = CurrentLoc.get () in
@@ -3851,15 +2748,15 @@ and childrenGlobal (vis: cilVisitor) (g: global) : global =
let f' = visitCilFunction vis f in
if f' != f then GFun (f', l) else g
| GType(t, l) ->
- let t' = vis#behavior.memo_typeinfo t in
+ let t' = Visitor_behavior.Memo.typeinfo vis#behavior t in
t'.ttype <- visitCilType vis t'.ttype;
if t' != t then GType(t',l) else g
| GEnumTagDecl (enum,l) ->
- let enum' = vis#behavior.memo_enuminfo enum in
+ let enum' = Visitor_behavior.Memo.enuminfo vis#behavior enum in
if enum != enum' then GEnumTagDecl(enum',l) else g
(* real visit'll be done in the definition *)
| GCompTagDecl (comp,l) ->
- let comp' = vis#behavior.memo_compinfo comp in
+ let comp' = Visitor_behavior.Memo.compinfo vis#behavior comp in
if comp != comp' then GCompTagDecl(comp',l) else g
| GEnumTag (enum, l) ->
let enum' = visitCilEnumInfo vis enum in
@@ -3878,7 +2775,7 @@ and childrenGlobal (vis: cilVisitor) (g: global) : global =
let form' = optMapNoCopy (mapNoCopy (visitCilVarDecl vis)) form in
let spec' =
if is_empty_funspec spec then begin
- if is_copy_behavior vis#behavior then
+ if Visitor_behavior.is_copy vis#behavior then
empty_funspec ()
else spec (* do not need to change it if it's not a copy visitor. *)
end else begin
@@ -3889,7 +2786,7 @@ and childrenGlobal (vis: cilVisitor) (g: global) : global =
begin
(match form' with
| Some formals
- when vis#behavior.is_copy_behavior || form != form' ->
+ when Visitor_behavior.is_copy vis#behavior || form != form' ->
let selection = State_selection.singleton FormalsDecl.self in
apply_on_project
~selection vis (unsafeSetFormalsDecl v') formals
@@ -3899,7 +2796,7 @@ and childrenGlobal (vis: cilVisitor) (g: global) : global =
else g
| GVar (v, inito, l) ->
let v' = visitCilVarDecl vis v in
- let inito' = vis#behavior.cinitinfo inito in
+ let inito' = Visitor_behavior.cinitinfo vis#behavior inito in
(match inito'.init with
None -> ()
| Some i -> let i' = visitCilInit vis v NoOffset i in
@@ -4242,7 +3139,7 @@ let mkStmtCfg ~before ~(new_stmtkind:stmtkind) ~(ref_stmt:stmt) : stmt =
labels = [];
sid = -1; succs = []; preds = []; ghost = false; sattr = [] }
in
- new_.sid <- Sid.next ();
+ new_.sid <- Cil_const.Sid.next ();
if before then begin
new_.succs <- [ref_stmt];
let old_preds = ref_stmt.preds in
@@ -4271,7 +3168,7 @@ let mkStmtCfg ~before ~(new_stmtkind:stmtkind) ~(ref_stmt:stmt) : stmt =
new_
let mkStmtCfgBlock sl =
- let sid = Sid.next () in
+ let sid = Cil_const.Sid.next () in
let n = mkStmt (Block (mkBlock sl)) in
n.sid <- sid;
match sl with
@@ -6479,9 +5376,9 @@ let removeOffsetLval ((b, off): lval) : lval * offset =
(b, off'), last
class copyVisitExpr = object
- inherit genericCilVisitor (copy_visit (Project.current ()))
+ inherit genericCilVisitor (Visitor_behavior.copy (Project.current ()))
method! vexpr e =
- ChangeDoChildrenPost ({e with eid = Eid.next ()}, fun x -> x)
+ ChangeDoChildrenPost ({e with eid = Cil_const.Eid.next ()}, fun x -> x)
end
let copy_exp e = visitCilExpr (new copyVisitExpr) e
@@ -6588,11 +5485,11 @@ let post_file vis f =
(* A visitor for the whole file that does not change the globals *)
let visitCilFileSameGlobals (vis : cilVisitor) (f : file) : unit =
- if vis#behavior.is_copy_behavior then
+ if Visitor_behavior.is_copy vis#behavior then
Kernel.fatal ~current:true "You used visitCilFileSameGlobals with a copy visitor. Nothing is done"
else
ignore
- (doVisitCil vis vis#behavior.cfile (post_file vis) childrenFileSameGlobals f)
+ (doVisitCil vis (Visitor_behavior.cfile vis#behavior) (post_file vis) childrenFileSameGlobals f)
let childrenFileCopy vis f =
let fGlob g = visitCilGlobal vis g in
@@ -6611,13 +5508,13 @@ let childrenFileCopy vis f =
(* Be careful with visiting the whole file because it might be huge. *)
let visitCilFileCopy (vis : cilVisitor) (f : file) : file =
- if vis#behavior.is_copy_behavior then begin
+ if Visitor_behavior.is_copy vis#behavior then begin
Queue.add Logic_env.prepare_tables vis#get_filling_actions;
end;
- doVisitCil vis vis#behavior.cfile (post_file vis) childrenFileCopy f
+ doVisitCil vis (Visitor_behavior.cfile vis#behavior) (post_file vis) childrenFileCopy f
let visitCilFile vis f =
- if vis#behavior.is_copy_behavior then
+ if Visitor_behavior.is_copy vis#behavior then
Kernel.fatal ~current:true "You used visitCilFile with a copy visitor. Nothing is done"
else ignore (visitCilFileCopy vis f)
@@ -8084,7 +6981,7 @@ let () = dependency_on_ast Switch_cases.self
let separate_switch_succs = Switch_cases.memo separate_switch_succs
class dropAttributes ?select () = object
- inherit genericCilVisitor (copy_visit (Project.current ()))
+ inherit genericCilVisitor (Visitor_behavior.copy (Project.current ()))
method! vattr a =
match select with
| None -> ChangeTo []
@@ -8118,6 +7015,7 @@ let typeHasAttributeDeep t =
Kernel.deprecated "Cil.typeHasAttributeDeep"
~now:"Cil.typeHasAttributeMemoryBlock"
typeHasAttributeMemoryBlock t
+
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index a2ae37a764d25eea95f19f5bb8db657a711baef7..2c60334fc5ed4d032a1d2c3e885049b7ae99a9d2 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -234,14 +234,6 @@ val mapGlobals: file -> (global -> global) -> unit
* refer to any struct or union types in the function type.*)
val findOrCreateFunc: file -> string -> typ -> varinfo
-module Sid: sig
- val next: unit -> int
-end
-
-module Eid: sig
- val next: unit -> int
-end
-
(** creates an expression with a fresh id *)
val new_exp: loc:location -> exp_node -> exp
@@ -421,34 +413,6 @@ val isSignedInteger: typ -> bool
@since Oxygen-20120901 *)
val isUnsignedInteger: typ -> bool
-
-(** Creates a (potentially recursive) composite type. The arguments are:
- * (1) a boolean indicating whether it is a struct or a union, (2) the name
- * (always non-empty), (3) a function that when given a representation of the
- * structure type constructs the type of the fields recursive type (the first
- * argument is only useful when some fields need to refer to the type of the
- * structure itself), and (4) a list of attributes to be associated with the
- * composite type. The resulting compinfo has the field "cdefined" only if
- * the list of fields is non-empty. *)
-val mkCompInfo: bool -> (* whether it is a struct or a union *)
- string -> (* name of the composite type; cannot be empty *)
- ?norig:string -> (* original name of the composite type, empty when anonymous *)
- (compinfo ->
- (string * typ * int option * attributes * location) list) ->
- (* a function that when given a forward
- representation of the structure type constructs the type of
- the fields. The function can ignore this argument if not
- constructing a recursive type. *)
- attributes -> compinfo
-
-(** Makes a shallow copy of a {!Cil_types.compinfo} changing the name. It also
- copies the fields, and makes sure that the copied field points back to the
- copied compinfo.
- If [fresh] is [true] (the default), it will also give a fresh id to the
- copy.
-*)
-val copyCompInfo: ?fresh:bool -> compinfo -> string -> compinfo
-
(** This is a constant used as the name of an unnamed bitfield. These fields
do not participate in initialization and their name is not printed. *)
val missingFieldName: string
@@ -1474,266 +1438,6 @@ val find_default_requires: behavior list -> identified_predicate list
(** {2 Visitor mechanism} *)
(* ************************************************************************* *)
-(** {3 Visitor behavior} *)
-type visitor_behavior
- (** How the visitor should behave in front of mutable fields: in
- place modification or copy of the structure. This type is abstract.
- Use one of the two values below in your classes.
- @plugin development guide *)
-
-val inplace_visit: unit -> visitor_behavior
- (** In-place modification. Behavior of the original cil visitor.
- @plugin development guide *)
-
-val copy_visit: Project.t -> visitor_behavior
- (** Makes fresh copies of the mutable structures.
- - preserves sharing for varinfo.
- - makes fresh copy of varinfo only for declarations. Variables that are
- only used in the visited AST are thus still shared with the original
- AST. This allows for instance to copy a function with its
- formals and local variables, and to keep the references to other
- globals in the function's body.
- @plugin development guide *)
-
-val refresh_visit: Project.t -> visitor_behavior
- (** Makes fresh copies of the mutable structures and provides fresh id
- for the structures that have ids. Note that as for {!copy_visit}, only
- varinfo that are declared in the scope of the visit will be copied and
- provided with a new id.
- @since Sodium-20150201
- *)
-
-(** true iff the behavior provides fresh id for copied structs with id.
- Always [false] for an inplace visitor.
- @since Sodium-20150201
-*)
-val is_fresh_behavior: visitor_behavior -> bool
-
-(** true iff the behavior is a copy behavior. *)
-val is_copy_behavior: visitor_behavior -> bool
-
-val reset_behavior_varinfo: visitor_behavior -> unit
-(** resets the internal tables used by the given visitor_behavior. If you use
- fresh instances of visitor for each round of transformation, this should
- not be needed. In place modifications do not need that at all.
- @plugin development guide
- *)
-
-val reset_behavior_compinfo: visitor_behavior -> unit
-val reset_behavior_enuminfo: visitor_behavior -> unit
-val reset_behavior_enumitem: visitor_behavior -> unit
-val reset_behavior_typeinfo: visitor_behavior -> unit
-val reset_behavior_stmt: visitor_behavior -> unit
-val reset_behavior_logic_info: visitor_behavior -> unit
-val reset_behavior_logic_type_info: visitor_behavior -> unit
-val reset_behavior_fieldinfo: visitor_behavior -> unit
-val reset_behavior_model_info: visitor_behavior -> unit
-val reset_logic_var: visitor_behavior -> unit
-val reset_behavior_kernel_function: visitor_behavior -> unit
-val reset_behavior_fundec: visitor_behavior -> unit
-
-val get_varinfo: visitor_behavior -> varinfo -> varinfo
-(** retrieve the representative of a given varinfo in the current
- state of the visitor
- @plugin development guide
- *)
-
-val get_compinfo: visitor_behavior -> compinfo -> compinfo
-val get_enuminfo: visitor_behavior -> enuminfo -> enuminfo
-val get_enumitem: visitor_behavior -> enumitem -> enumitem
-val get_typeinfo: visitor_behavior -> typeinfo -> typeinfo
-val get_stmt: visitor_behavior -> stmt -> stmt
-(** @plugin development guide *)
-
-val get_logic_info: visitor_behavior -> logic_info -> logic_info
-val get_logic_type_info: visitor_behavior -> logic_type_info -> logic_type_info
-val get_fieldinfo: visitor_behavior -> fieldinfo -> fieldinfo
-val get_model_info: visitor_behavior -> model_info -> model_info
-val get_logic_var: visitor_behavior -> logic_var -> logic_var
-val get_kernel_function: visitor_behavior -> kernel_function -> kernel_function
-(** @plugin development guide *)
-
-val get_fundec: visitor_behavior -> fundec -> fundec
-
-val get_original_varinfo: visitor_behavior -> varinfo -> varinfo
- (** retrieve the original representative of a given copy of a varinfo
- in the current state of the visitor.
- @plugin development guide
- *)
-
-val get_original_compinfo: visitor_behavior -> compinfo -> compinfo
-val get_original_enuminfo: visitor_behavior -> enuminfo -> enuminfo
-val get_original_enumitem: visitor_behavior -> enumitem -> enumitem
-val get_original_typeinfo: visitor_behavior -> typeinfo -> typeinfo
-val get_original_stmt: visitor_behavior -> stmt -> stmt
-val get_original_logic_info: visitor_behavior -> logic_info -> logic_info
-val get_original_logic_type_info:
- visitor_behavior -> logic_type_info -> logic_type_info
-val get_original_fieldinfo: visitor_behavior -> fieldinfo -> fieldinfo
-val get_original_model_info: visitor_behavior -> model_info -> model_info
-val get_original_logic_var: visitor_behavior -> logic_var -> logic_var
-val get_original_kernel_function:
- visitor_behavior -> kernel_function -> kernel_function
-val get_original_fundec: visitor_behavior -> fundec -> fundec
-
-val set_varinfo: visitor_behavior -> varinfo -> varinfo -> unit
- (** change the representative of a given varinfo in the current
- state of the visitor. Use with care (i.e. makes sure that the old one
- is not referenced anywhere in the AST, or sharing will be lost.
- @plugin development guide
- *)
-val set_compinfo: visitor_behavior -> compinfo -> compinfo -> unit
-val set_enuminfo: visitor_behavior -> enuminfo -> enuminfo -> unit
-val set_enumitem: visitor_behavior -> enumitem -> enumitem -> unit
-val set_typeinfo: visitor_behavior -> typeinfo -> typeinfo -> unit
-val set_stmt: visitor_behavior -> stmt -> stmt -> unit
-val set_logic_info: visitor_behavior -> logic_info -> logic_info -> unit
-val set_logic_type_info:
- visitor_behavior -> logic_type_info -> logic_type_info -> unit
-val set_fieldinfo: visitor_behavior -> fieldinfo -> fieldinfo -> unit
-val set_model_info: visitor_behavior -> model_info -> model_info -> unit
-val set_logic_var: visitor_behavior -> logic_var -> logic_var -> unit
-val set_kernel_function:
- visitor_behavior -> kernel_function -> kernel_function -> unit
-val set_fundec: visitor_behavior -> fundec -> fundec -> unit
-
-val set_orig_varinfo: visitor_behavior -> varinfo -> varinfo -> unit
- (** change the reference of a given new varinfo in the current
- state of the visitor. Use with care
- *)
-val set_orig_compinfo: visitor_behavior -> compinfo -> compinfo -> unit
-val set_orig_enuminfo: visitor_behavior -> enuminfo -> enuminfo -> unit
-val set_orig_enumitem: visitor_behavior -> enumitem -> enumitem -> unit
-val set_orig_typeinfo: visitor_behavior -> typeinfo -> typeinfo -> unit
-val set_orig_stmt: visitor_behavior -> stmt -> stmt -> unit
-val set_orig_logic_info: visitor_behavior -> logic_info -> logic_info -> unit
-val set_orig_logic_type_info:
- visitor_behavior -> logic_type_info -> logic_type_info -> unit
-val set_orig_fieldinfo: visitor_behavior -> fieldinfo -> fieldinfo -> unit
-val set_orig_model_info: visitor_behavior -> model_info -> model_info -> unit
-val set_orig_logic_var: visitor_behavior -> logic_var -> logic_var -> unit
-val set_orig_kernel_function:
- visitor_behavior -> kernel_function -> kernel_function -> unit
-val set_orig_fundec: visitor_behavior -> fundec -> fundec -> unit
-
-val unset_varinfo: visitor_behavior -> varinfo -> unit
- (** remove the entry associated to the given varinfo in the current
- state of the visitor. Use with care (i.e. make sure that you will never
- visit again this varinfo in the same visiting context).
- @plugin development guide
- *)
-val unset_compinfo: visitor_behavior -> compinfo -> unit
-val unset_enuminfo: visitor_behavior -> enuminfo -> unit
-val unset_enumitem: visitor_behavior -> enumitem -> unit
-val unset_typeinfo: visitor_behavior -> typeinfo -> unit
-val unset_stmt: visitor_behavior -> stmt -> unit
-val unset_logic_info: visitor_behavior -> logic_info -> unit
-val unset_logic_type_info: visitor_behavior -> logic_type_info -> unit
-val unset_fieldinfo: visitor_behavior -> fieldinfo -> unit
-val unset_model_info: visitor_behavior -> model_info -> unit
-val unset_logic_var: visitor_behavior -> logic_var -> unit
-val unset_kernel_function: visitor_behavior -> kernel_function -> unit
-val unset_fundec: visitor_behavior -> fundec -> unit
-
-val unset_orig_varinfo: visitor_behavior -> varinfo -> unit
- (** remove the entry associated with the given new varinfo in the current
- state of the visitor. Use with care
- *)
-val unset_orig_compinfo: visitor_behavior -> compinfo -> unit
-val unset_orig_enuminfo: visitor_behavior -> enuminfo -> unit
-val unset_orig_enumitem: visitor_behavior -> enumitem -> unit
-val unset_orig_typeinfo: visitor_behavior -> typeinfo -> unit
-val unset_orig_stmt: visitor_behavior -> stmt -> unit
-val unset_orig_logic_info: visitor_behavior -> logic_info -> unit
-val unset_orig_logic_type_info: visitor_behavior -> logic_type_info -> unit
-val unset_orig_fieldinfo: visitor_behavior -> fieldinfo -> unit
-val unset_orig_model_info: visitor_behavior -> model_info -> unit
-val unset_orig_logic_var: visitor_behavior -> logic_var -> unit
-val unset_orig_kernel_function: visitor_behavior -> kernel_function -> unit
-val unset_orig_fundec: visitor_behavior -> fundec -> unit
-
-val memo_varinfo: visitor_behavior -> varinfo -> varinfo
- (** finds a binding in new project for the given varinfo, creating one
- if it does not already exists. *)
-val memo_compinfo: visitor_behavior -> compinfo -> compinfo
-val memo_enuminfo: visitor_behavior -> enuminfo -> enuminfo
-val memo_enumitem: visitor_behavior -> enumitem -> enumitem
-val memo_typeinfo: visitor_behavior -> typeinfo -> typeinfo
-val memo_stmt: visitor_behavior -> stmt -> stmt
-val memo_logic_info: visitor_behavior -> logic_info -> logic_info
-val memo_logic_type_info: visitor_behavior -> logic_type_info -> logic_type_info
-val memo_fieldinfo: visitor_behavior -> fieldinfo -> fieldinfo
-val memo_model_info: visitor_behavior -> model_info -> model_info
-val memo_logic_var: visitor_behavior -> logic_var -> logic_var
-val memo_kernel_function:
- visitor_behavior -> kernel_function -> kernel_function
-val memo_fundec: visitor_behavior -> fundec -> fundec
-
-(** [iter_visitor_varinfo vis f] iterates [f] over each pair of
- varinfo registered in [vis]. Varinfo for the old AST is presented
- to [f] first.
- @since Oxygen-20120901
-*)
-val iter_visitor_varinfo:
- visitor_behavior -> (varinfo -> varinfo -> unit) -> unit
-val iter_visitor_compinfo:
- visitor_behavior -> (compinfo -> compinfo -> unit) -> unit
-val iter_visitor_enuminfo:
- visitor_behavior -> (enuminfo -> enuminfo -> unit) -> unit
-val iter_visitor_enumitem:
- visitor_behavior -> (enumitem -> enumitem -> unit) -> unit
-val iter_visitor_typeinfo:
- visitor_behavior -> (typeinfo -> typeinfo -> unit) -> unit
-val iter_visitor_stmt:
- visitor_behavior -> (stmt -> stmt -> unit) -> unit
-val iter_visitor_logic_info:
- visitor_behavior -> (logic_info -> logic_info -> unit) -> unit
-val iter_visitor_logic_type_info:
- visitor_behavior -> (logic_type_info -> logic_type_info -> unit) -> unit
-val iter_visitor_fieldinfo:
- visitor_behavior -> (fieldinfo -> fieldinfo -> unit) -> unit
-val iter_visitor_model_info:
- visitor_behavior -> (model_info -> model_info -> unit) -> unit
-val iter_visitor_logic_var:
- visitor_behavior -> (logic_var -> logic_var -> unit) -> unit
-val iter_visitor_kernel_function:
- visitor_behavior -> (kernel_function -> kernel_function -> unit) -> unit
-val iter_visitor_fundec:
- visitor_behavior -> (fundec -> fundec -> unit) -> unit
-
-(** [fold_visitor_varinfo vis f] folds [f] over each pair of varinfo registered
- in [vis]. Varinfo for the old AST is presented to [f] first.
- @since Oxygen-20120901
-*)
-val fold_visitor_varinfo:
- visitor_behavior -> (varinfo -> varinfo -> 'a -> 'a) -> 'a -> 'a
-val fold_visitor_compinfo:
- visitor_behavior -> (compinfo -> compinfo -> 'a -> 'a) -> 'a -> 'a
-val fold_visitor_enuminfo:
- visitor_behavior -> (enuminfo -> enuminfo -> 'a -> 'a) -> 'a -> 'a
-val fold_visitor_enumitem:
- visitor_behavior -> (enumitem -> enumitem -> 'a -> 'a) -> 'a -> 'a
-val fold_visitor_typeinfo:
- visitor_behavior -> (typeinfo -> typeinfo -> 'a -> 'a) -> 'a -> 'a
-val fold_visitor_stmt:
- visitor_behavior -> (stmt -> stmt -> 'a -> 'a) -> 'a -> 'a
-val fold_visitor_logic_info:
- visitor_behavior -> (logic_info -> logic_info -> 'a -> 'a) -> 'a -> 'a
-val fold_visitor_logic_type_info:
- visitor_behavior ->
- (logic_type_info -> logic_type_info -> 'a -> 'a) -> 'a -> 'a
-val fold_visitor_fieldinfo:
- visitor_behavior -> (fieldinfo -> fieldinfo -> 'a -> 'a) -> 'a -> 'a
-val fold_visitor_model_info:
- visitor_behavior -> (model_info -> model_info -> 'a -> 'a) -> 'a -> 'a
-val fold_visitor_logic_var:
- visitor_behavior -> (logic_var -> logic_var -> 'a -> 'a) -> 'a -> 'a
-val fold_visitor_kernel_function:
- visitor_behavior ->
- (kernel_function -> kernel_function -> 'a -> 'a) -> 'a -> 'a
-val fold_visitor_fundec:
- visitor_behavior -> (fundec -> fundec -> 'a -> 'a) -> 'a -> 'a
-
(** {3 Visitor class} *)
(** A visitor interface for traversing CIL trees. Create instantiations of
@@ -1750,7 +1454,7 @@ val fold_visitor_fundec:
@plugin development guide *)
class type cilVisitor = object
- method behavior: visitor_behavior
+ method behavior: Visitor_behavior.t
(** the kind of behavior expected for the behavior.
@plugin development guide *)
@@ -1978,12 +1682,12 @@ val register_behavior_extension:
(**/**)
class internal_genericCilVisitor:
- fundec option ref -> visitor_behavior -> (unit->unit) Queue.t -> cilVisitor
+ fundec option ref -> Visitor_behavior.t -> (unit->unit) Queue.t -> cilVisitor
(**/**)
(** generic visitor, parameterized by its copying behavior.
Traverses the CIL tree without modifying anything *)
-class genericCilVisitor: visitor_behavior -> cilVisitor
+class genericCilVisitor: Visitor_behavior.t -> cilVisitor
(** Default in place visitor doing nothing and operating on current project. *)
class nopCilVisitor: cilVisitor
diff --git a/src/kernel_services/ast_queries/cil_const.ml b/src/kernel_services/ast_queries/cil_const.ml
index da948c8edd1beb07616fb34b7328f73b7d6b65e9..f11f85dbf1f6ca987cf761d5cc257e3b0a1806f3 100644
--- a/src/kernel_services/ast_queries/cil_const.ml
+++ b/src/kernel_services/ast_queries/cil_const.ml
@@ -55,6 +55,8 @@ module CurrentLoc =
let voidType = TVoid([])
module Vid = State_builder.SharedCounter(struct let name = "vid_counter" end)
+module Sid = State_builder.SharedCounter(struct let name = "sid" end)
+module Eid = State_builder.SharedCounter(struct let name = "eid" end)
let set_vid v =
let n = Vid.next () in
@@ -79,6 +81,68 @@ let change_varinfo_name vi name =
let new_raw_id = Vid.next
+(* The next compindo identifier to use. Counts up. *)
+ let nextCompinfoKey =
+ let module M =
+ State_builder.SharedCounter(struct let name = "compinfokey" end)
+ in
+ M.next
+
+(** Creates a (potentially recursive) composite type. Make sure you add a
+ * GTag for it to the file! **)
+let mkCompInfo
+ (isstruct: bool)
+ (n: string)
+ ?(norig=n)
+ (* fspec is a function that when given a forward
+ * representation of the structure type constructs the type of
+ * the fields. The function can ignore this argument if not
+ * constructing a recursive type. *)
+ (mkfspec: compinfo -> (string * typ * int option * attribute list *
+ location) list)
+ (a: attribute list) : compinfo =
+
+ (* make a new name for anonymous structs *)
+ if n = "" then Kernel.fatal "mkCompInfo: missing structure name\n" ;
+ (* Make a new self cell and a forward reference *)
+ let comp =
+ { cstruct = isstruct;
+ corig_name = norig;
+ cname = n;
+ ckey = nextCompinfoKey ();
+ cfields = []; (* fields will be added afterwards. *)
+ cattr = a;
+ creferenced = false;
+ (* Make this compinfo undefined by default *)
+ cdefined = false; }
+ in
+ let flds =
+ List.map (fun (fn, ft, fb, fa, fl) ->
+ { fcomp = comp;
+ ftype = ft;
+ forig_name = fn;
+ fname = fn;
+ fbitfield = fb;
+ fattr = fa;
+ floc = fl;
+ faddrof = false;
+ fsize_in_bits = None;
+ foffset_in_bits = None;
+ fpadding_in_bits = None;
+ }) (mkfspec comp) in
+ comp.cfields <- flds;
+ if flds <> [] then comp.cdefined <- true;
+ comp
+
+(** Make a copy of a compinfo, changing the name and the key *)
+let copyCompInfo ?(fresh=true) ci cname =
+ let ckey = if fresh then nextCompinfoKey () else ci.ckey in
+ let ci' = { ci with cname; ckey } in
+ (* Copy the fields and set the new pointers to parents *)
+ ci'.cfields <- List.map (fun f -> {f with fcomp = ci'}) ci'.cfields;
+ ci'
+
+
let make_logic_var_kind x kind typ =
{lv_name = x; lv_id = new_raw_id(); lv_type = typ; lv_kind = kind;
lv_origin = None; lv_attr = [] }
diff --git a/src/kernel_services/ast_queries/cil_const.mli b/src/kernel_services/ast_queries/cil_const.mli
index 0fdc1c5fc996e9a56375763da6953268db13ff0f..58178291430fce395a9cefe0f39f2fa696ba4956 100644
--- a/src/kernel_services/ast_queries/cil_const.mli
+++ b/src/kernel_services/ast_queries/cil_const.mli
@@ -50,6 +50,8 @@ val voidType: typ
module CurrentLoc: State_builder.Ref with type data = location
module Vid: sig val next: unit -> int end
+module Sid: sig val next: unit -> int end
+module Eid: sig val next: unit -> int end
(** set the vid to a fresh number. *)
val set_vid: varinfo -> unit
@@ -72,6 +74,34 @@ val new_raw_id: unit -> int
that is generated by {!Cil.makeLocalVar} and friends.
Must not be used for setting vid: use {!set_vid} instead. *)
+(** Creates a (potentially recursive) composite type. The arguments are:
+ * (1) a boolean indicating whether it is a struct or a union, (2) the name
+ * (always non-empty), (3) a function that when given a representation of the
+ * structure type constructs the type of the fields recursive type (the first
+ * argument is only useful when some fields need to refer to the type of the
+ * structure itself), and (4) a list of attributes to be associated with the
+ * composite type. The resulting compinfo has the field "cdefined" only if
+ * the list of fields is non-empty. *)
+val mkCompInfo: bool -> (* whether it is a struct or a union *)
+ string -> (* name of the composite type; cannot be empty *)
+ ?norig:string -> (* original name of the composite type, empty when anonymous *)
+ (compinfo ->
+ (string * typ * int option * attributes * location) list) ->
+ (* a function that when given a forward
+ representation of the structure type constructs the type of
+ the fields. The function can ignore this argument if not
+ constructing a recursive type. *)
+ attributes -> compinfo
+
+(** Makes a shallow copy of a {!Cil_types.compinfo} changing the name. It also
+ copies the fields, and makes sure that the copied field points back to the
+ copied compinfo.
+ If [fresh] is [true] (the default), it will also give a fresh id to the
+ copy.
+*)
+val copyCompInfo: ?fresh:bool -> compinfo -> string -> compinfo
+
+
(** Create a fresh logical variable giving its name, type and origin.
@since Fluorine-20130401
*)
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 9fd8da5e14f15e9d52bee6b56c65cc7952b1058a..60ee0168a457e35ea8e96e1e344080082729d802 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -1567,7 +1567,7 @@ let prepare_from_c_files () =
let init_project_from_visitor ?(reorder=false) prj
(vis:Visitor.frama_c_visitor) =
- if not (Cil.is_copy_behavior vis#behavior)
+ if not (Visitor_behavior.is_copy vis#behavior)
|| not (Project.equal prj (Extlib.the vis#project))
then
Kernel.fatal
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 7b34794252919a949b016b77e9ce38241abc86a9..fb00eb02fa931eef53384306ea221720419d599f 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -2513,7 +2513,7 @@ let eval_term_lval global_find_init (lhost, loff) =
| _ -> None
class simplify_const_lval global_find_init = object (self)
- inherit Cil.genericCilVisitor (Cil.copy_visit (Project.current ()))
+ inherit Cil.genericCilVisitor (Visitor_behavior.copy (Project.current ()))
method! vterm t =
match t.term_node with
diff --git a/src/kernel_services/ast_transformations/filter.ml b/src/kernel_services/ast_transformations/filter.ml
index 53907e6dc53d71f21bd0f3866f0a5e6b5a6f39b6..0a24be8541627b5368278c60906916b4780171e4 100644
--- a/src/kernel_services/ast_transformations/filter.ml
+++ b/src/kernel_services/ast_transformations/filter.ml
@@ -327,7 +327,7 @@ end = struct
* *)
class filter_visitor pinfo prj = object(self)
- inherit Visitor.generic_frama_c_visitor (Cil.copy_visit prj)
+ inherit Visitor.generic_frama_c_visitor (Visitor_behavior.copy prj)
val mutable keep_stmts = Stmt.Set.empty
val mutable fi = None
@@ -396,13 +396,13 @@ end = struct
(fun v ->
Varinfo.Hashtbl.add local_visible v ();
let v' = Cil.copyVarinfo v v.vname in
- Cil.set_varinfo self#behavior v v';
- Cil.set_orig_varinfo self#behavior v' v;
+ Visitor_behavior.Set.varinfo self#behavior v v';
+ Visitor_behavior.Set_orig.varinfo self#behavior v' v;
(match v.vlogic_var_assoc, v'.vlogic_var_assoc with
None, None -> ()
| Some lv, Some lv' ->
- Cil.set_logic_var self#behavior lv lv';
- Cil.set_orig_logic_var self#behavior lv' lv
+ Visitor_behavior.Set.logic_var self#behavior lv lv';
+ Visitor_behavior.Set_orig.logic_var self#behavior lv' lv
| _ -> assert false (* copy should be faithful *));
v')
formals
@@ -418,13 +418,13 @@ end = struct
then begin
Varinfo.Hashtbl.add local_visible var ();
let var' = Cil.copyVarinfo var var.vname in
- Cil.set_varinfo self#behavior var var';
- Cil.set_orig_varinfo self#behavior var' var;
+ Visitor_behavior.Set.varinfo self#behavior var var';
+ Visitor_behavior.Set_orig.varinfo self#behavior var' var;
(match var.vlogic_var_assoc, var'.vlogic_var_assoc with
None, None -> ()
| Some lv, Some lv' ->
- Cil.set_logic_var self#behavior lv lv';
- Cil.set_orig_logic_var self#behavior lv' lv
+ Visitor_behavior.Set.logic_var self#behavior lv lv';
+ Visitor_behavior.Set_orig.logic_var self#behavior lv' lv
| _ -> assert false (* copy should be faithful *));
var' :: (filter locals)
end else filter locals
@@ -434,7 +434,8 @@ end = struct
method! vcode_annot v =
Extlib.may Cil.CurrentLoc.set (Cil_datatype.Code_annotation.loc v);
let stmt =
- Cil.get_original_stmt self#behavior (Extlib.the self#current_stmt)
+ Visitor_behavior.Get_orig.stmt
+ self#behavior (Extlib.the self#current_stmt)
in
debug "[annotation] stmt %d : %a @."
stmt.sid Printer.pp_code_annotation v;
@@ -516,14 +517,14 @@ end = struct
Cil.ChangeDoChildrenPost (b, optim)
method private change_sid s =
- let orig = Cil.get_original_stmt self#behavior s in
- assert (Cil.get_stmt self#behavior orig == s);
+ let orig = Visitor_behavior.Get_orig.stmt self#behavior s in
+ assert (Visitor_behavior.Get.stmt self#behavior orig == s);
let old = s.sid in
let keep = Stmt.Set.mem s keep_stmts in
keep_stmts <- Stmt.Set.remove s keep_stmts;
- s.sid <- Cil.Sid.next ();
- Cil.set_stmt self#behavior orig s;
- Cil.set_orig_stmt self#behavior s orig;
+ s.sid <- Cil_const.Sid.next ();
+ Visitor_behavior.Set.stmt self#behavior orig s;
+ Visitor_behavior.Set_orig.stmt self#behavior s orig;
if keep then self#add_stmt_keep s;
debug "@[finalize sid:%d->sid:%d@]@\n@." old s.sid
@@ -539,7 +540,7 @@ end = struct
| If (_,bthen,belse,loc) ->
let bthen = Cil.visitCilBlock (self:>Cil.cilVisitor) bthen in
let belse = Cil.visitCilBlock (self:>Cil.cilVisitor) belse in
- let s_orig = Cil.get_original_stmt self#behavior s in
+ let s_orig = Visitor_behavior.Get_orig.stmt self#behavior s in
optim_if finfo keep_stmts s_orig s None bthen belse loc
| Switch (_exp, body, _, loc) ->
(* the switch is invisible : it can be translated into a block. *)
@@ -561,7 +562,7 @@ end = struct
anything to do: it will not appear at all in the function.
*)
if Info.loc_var_visible (self#get_finfo()) v then begin
- let v' = Cil.get_varinfo self#behavior v in
+ let v' = Visitor_behavior.Get.varinfo self#behavior v in
v'.vdefined <- false;
end;
mk_new_stmt s (mk_stmt_skip s)
@@ -584,7 +585,7 @@ end = struct
we would have multiple syntactic scope for the same variable).
*)
method private remove_local_static_attr v =
- let new_v = Cil.get_varinfo self#behavior v in
+ let new_v = Visitor_behavior.Get.varinfo self#behavior v in
new_v.vattr <- Cil.dropAttribute Cabs2cil.fc_local_static new_v.vattr
method private process_visible_stmt s =
@@ -612,7 +613,7 @@ end = struct
self#change_sid s';
(match s'.skind with
| If (cond,bthen,belse,loc) ->
- let s_orig = Cil.get_original_stmt self#behavior s' in
+ let s_orig = Visitor_behavior.Get_orig.stmt self#behavior s' in
optim_if finfo keep_stmts s_orig s' (Some cond) bthen belse loc
| Switch (e,b,c,l) ->
let c' = List.filter (not $ (can_skip keep_stmts)) c in
@@ -703,7 +704,7 @@ end = struct
(fun () -> Cil.setFormals f new_formals) self#get_filling_actions;
(* clean up the environment if we have more than one copy of the
function in the sliced code. *)
- Cil.reset_behavior_stmt self#behavior;
+ Visitor_behavior.Reset.stmt self#behavior;
keep_stmts <- Stmt.Set.empty;
Varinfo.Hashtbl.clear local_visible;
Varinfo.Hashtbl.add spec_table f.svar
@@ -822,14 +823,14 @@ end = struct
new_var.vtype <- mytype;
List.iter2
(fun x y ->
- Cil.set_varinfo self#behavior x y;
- Cil.set_orig_varinfo self#behavior y x;
+ Visitor_behavior.Set.varinfo self#behavior x y;
+ Visitor_behavior.Set_orig.varinfo self#behavior y x;
match x.vlogic_var_assoc with
None -> ();
| Some lv ->
let lv' = Cil.cvar_to_lvar y in
- Cil.set_logic_var self#behavior lv lv';
- Cil.set_orig_logic_var self#behavior lv' lv)
+ Visitor_behavior.Set.logic_var self#behavior lv lv';
+ Visitor_behavior.Set_orig.logic_var self#behavior lv' lv)
old_formals
new_formals;
(* adds the new parameters to the formals decl table *)
@@ -856,15 +857,15 @@ end = struct
let orig_var = Ast_info.Function.get_vi kf.fundec in
(* The first copy is also the default one for varinfo that are not handled
by ff_var but directly by the visitor *)
- if (Cil.get_varinfo self#behavior orig_var) == orig_var then
- Cil.set_varinfo self#behavior orig_var new_var;
+ if (Visitor_behavior.Get.varinfo self#behavior orig_var) == orig_var then
+ Visitor_behavior.Set.varinfo self#behavior orig_var new_var;
(* Set the new_var as an already known one, coming from the vi associated
to the current kf.
*)
- Cil.set_varinfo self#behavior new_var new_var;
- Cil.set_orig_varinfo self#behavior new_var orig_var;
- Cil.set_kernel_function self#behavior kf new_kf;
- Cil.set_orig_kernel_function self#behavior new_kf kf;
+ Visitor_behavior.Set.varinfo self#behavior new_var new_var;
+ Visitor_behavior.Set_orig.varinfo self#behavior new_var orig_var;
+ Visitor_behavior.Set.kernel_function self#behavior kf new_kf;
+ Visitor_behavior.Set_orig.kernel_function self#behavior new_kf kf;
Queue.add
(fun () -> Globals.Functions.register new_kf) self#get_filling_actions;
GFunDecl (Cil.empty_funspec(), new_var, loc), action
@@ -902,10 +903,10 @@ end = struct
let new_kf = make_new_kf my_kf kf new_fct_var in
(* Set the new_var as an already known one,
* coming from the vi associated to the current kf. *)
- Cil.set_varinfo self#behavior new_fct_var new_fct_var;
- Cil.set_orig_varinfo self#behavior new_fct_var fvar;
- Cil.set_kernel_function self#behavior kf new_kf;
- Cil.set_orig_kernel_function self#behavior new_kf kf;
+ Visitor_behavior.Set.varinfo self#behavior new_fct_var new_fct_var;
+ Visitor_behavior.Set_orig.varinfo self#behavior new_fct_var fvar;
+ Visitor_behavior.Set.kernel_function self#behavior kf new_kf;
+ Visitor_behavior.Set_orig.kernel_function self#behavior new_kf kf;
Queue.add
(fun () -> Globals.Functions.register new_kf)
self#get_filling_actions;
diff --git a/src/kernel_services/ast_transformations/inline.ml b/src/kernel_services/ast_transformations/inline.ml
index cb00a64b313a8dc77930c56db256653944770fa7..600438e672790705bcb21a8956246d3539ef92a7 100644
--- a/src/kernel_services/ast_transformations/inline.ml
+++ b/src/kernel_services/ast_transformations/inline.ml
@@ -90,7 +90,7 @@ let inline_call loc caller callee return args =
method! vvrbl v =
if v.vglob then
- Cil.ChangeTo (Cil.get_original_varinfo self#behavior v)
+ Cil.ChangeTo (Visitor_behavior.Get_orig.varinfo self#behavior v)
else Cil.DoChildren
method! vterm_lval (host,offset) =
diff --git a/src/kernel_services/visitors/visitor.ml b/src/kernel_services/visitors/visitor.ml
index 9e6738a2b39efce81be89b924d4670a5263211d2..01ee6940afea4dd4737b8ffd4b766022dd122065 100644
--- a/src/kernel_services/visitors/visitor.ml
+++ b/src/kernel_services/visitors/visitor.ml
@@ -66,7 +66,7 @@ object(self)
method current_kf = !current_kf
method! private vstmt stmt =
- let orig_stmt = Cil.get_original_stmt self#behavior stmt in
+ let orig_stmt = Visitor_behavior.Get_orig.stmt self#behavior stmt in
let annots =
Annotations.fold_code_annot (fun e a acc -> (e, a) :: acc) orig_stmt []
in
@@ -91,7 +91,7 @@ object(self)
if [x] is already trivial itself. *)
let becomes_trivial = is_trivial y && not (is_trivial x) in
let curr_add, remove_curr =
- if Cil.is_copy_behavior vis#behavior then
+ if Visitor_behavior.is_copy vis#behavior then
(* Copy visitor. We add [y], except if trivial. No sense in
removing [x], since the stmt is a new one. *)
(if not becomes_trivial then [e, y] else []),
@@ -115,7 +115,7 @@ object(self)
let change_stmt stmt (add, remove) =
if (add <> [] || remove <> []) then begin
let kf = Extlib.the self#current_kf in
- let new_kf = Cil.get_kernel_function self#behavior kf in
+ let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
Queue.add
(fun () ->
List.iter
@@ -173,12 +173,12 @@ object(self)
let old_allocates = fold_elt Annotations.fold_allocates in
let old_extended = fold_elt Annotations.fold_extended in
let b' =
- if Cil.is_copy_behavior self#behavior then
+ if Visitor_behavior.is_copy self#behavior then
{ b with b_name = b.b_name }
else b
in
let res = self#vbehavior b' in
- let new_kf = Cil.get_kernel_function self#behavior kf in
+ let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
let add_queue a = Queue.add a self#get_filling_actions in
let visit_clauses vis f =
(* Ensures that we have a table associated to new_kf in Annotations. *)
@@ -385,7 +385,7 @@ object(self)
method private vfunspec_annot () =
let kf = Extlib.the self#current_kf in
- let new_kf = Cil.get_kernel_function self#behavior kf in
+ let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
let old_behaviors =
Annotations.fold_behaviors (fun e b acc -> (e,b)::acc) kf []
in
@@ -625,18 +625,18 @@ object(self)
method! vglob g =
let fundec, has_kf = match g with
| GFunDecl(_,v,_) ->
- let ov = Cil.get_original_varinfo self#behavior v in
+ let ov = Visitor_behavior.Get_orig.varinfo self#behavior v in
let kf = try Globals.Functions.get ov with Not_found ->
Kernel.fatal "No kernel function for %s(%d)" v.vname v.vid
in
(* Just make a copy of current kernel function in case it is needed *)
- let new_kf = Cil.memo_kernel_function self#behavior kf in
- if Cil.is_copy_behavior self#behavior then
+ let new_kf = Visitor_behavior.Memo.kernel_function self#behavior kf in
+ if Visitor_behavior.is_copy self#behavior then
new_kf.spec <- Cil.empty_funspec ();
self#set_current_kf kf;
None, true
| GFun(f,_) ->
- let v = Cil.get_original_varinfo self#behavior f.svar in
+ let v = Visitor_behavior.Get_orig.varinfo self#behavior f.svar in
let kf =
try Globals.Functions.get v
with Not_found ->
@@ -644,8 +644,8 @@ object(self)
v.vname
Project.pretty (Project.current ())
in
- let new_kf = Cil.memo_kernel_function self#behavior kf in
- if Cil.is_copy_behavior self#behavior then
+ let new_kf = Visitor_behavior.Memo.kernel_function self#behavior kf in
+ if Visitor_behavior.is_copy self#behavior then
new_kf.spec <- Cil.empty_funspec ();
self#set_current_kf kf;
Some f, true
@@ -672,7 +672,7 @@ object(self)
| _ -> None
in
let change_glob ng spec =
- let cond = is_copy_behavior self#behavior in
+ let cond = Visitor_behavior.is_copy self#behavior in
match ng with
| GVar(vi,init,_) ->
if cond then
@@ -689,7 +689,7 @@ object(self)
| GFunDecl(_,v,l) ->
(match self#current_kf with
| Some kf ->
- let new_kf = Cil.get_kernel_function self#behavior kf in
+ let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
if cond then begin
Queue.add
(fun () ->
@@ -743,7 +743,7 @@ object(self)
if cond then begin
match self#current_kf with
| Some kf ->
- let new_kf = Cil.get_kernel_function self#behavior kf in
+ let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
Queue.add
(fun () ->
Kernel.debug ~dkey:Kernel.dkey_visitor
@@ -836,11 +836,14 @@ class generic_frama_c_visitor bhv =
let queue = Queue.create () in
internal_generic_frama_c_visitor current_fundec queue current_kf bhv
-class frama_c_copy prj = generic_frama_c_visitor (copy_visit prj)
+class frama_c_copy prj =
+ generic_frama_c_visitor (Visitor_behavior.copy prj)
-class frama_c_refresh prj = generic_frama_c_visitor (refresh_visit prj)
+class frama_c_refresh prj =
+ generic_frama_c_visitor (Visitor_behavior.refresh prj)
-class frama_c_inplace = generic_frama_c_visitor (inplace_visit())
+class frama_c_inplace =
+ generic_frama_c_visitor (Visitor_behavior.inplace())
let visitFramacFileCopy vis f = visitCilFileCopy (vis:>cilVisitor) f
@@ -854,7 +857,7 @@ let visitFramacGlobal vis g =
vis#fill_global_tables; g'
let visitFramacFunction vis f =
- let orig_var = Cil.get_original_varinfo vis#behavior f.svar in
+ let orig_var = Visitor_behavior.Get_orig.varinfo vis#behavior f.svar in
let old_current_kf = vis#current_kf in
vis#set_current_kf (Globals.Functions.get orig_var);
let f' = visitCilFunction (vis:>cilVisitor) f in
@@ -869,7 +872,7 @@ let visitFramacKf vis kf =
| None -> kf
| Some prj ->
let vi = Kernel_function.get_vi kf in
- let vi' = Cil.get_varinfo vis#behavior vi in
+ let vi' = Visitor_behavior.Get.varinfo vis#behavior vi in
Project.on prj Globals.Functions.get vi'
let visitFramacExpr vis e =
diff --git a/src/kernel_services/visitors/visitor.mli b/src/kernel_services/visitors/visitor.mli
index 3fffe6a974c20e101b8ec86108f970214b55c417..faa4d4be3a64ce614003527f3601057cadab68ba 100644
--- a/src/kernel_services/visitors/visitor.mli
+++ b/src/kernel_services/visitors/visitor.mli
@@ -95,7 +95,7 @@ class frama_c_refresh: Project.t -> frama_c_visitor
*)
class generic_frama_c_visitor:
- Cil.visitor_behavior -> frama_c_visitor
+ Visitor_behavior.t -> frama_c_visitor
(** Generic class that abstracts over [frama_c_inplace] and [frama_c_copy].
@plugin development guide *)
diff --git a/src/kernel_services/visitors/visitor_behavior.ml b/src/kernel_services/visitors/visitor_behavior.ml
new file mode 100644
index 0000000000000000000000000000000000000000..9bff52e7fb21295bd5ae4a623297cd35e781088a
--- /dev/null
+++ b/src/kernel_services/visitors/visitor_behavior.ml
@@ -0,0 +1,1146 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* INRIA (Institut National de Recherche en Informatique et en *)
+(* Automatique) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+type t =
+ { (* copy mutable structure which are not shared across the AST*)
+ cfile: file -> file;
+ cinitinfo: initinfo -> initinfo;
+ cblock: block -> block;
+ cfunspec: funspec -> funspec;
+ cfunbehavior: funbehavior -> funbehavior;
+ cidentified_term: identified_term -> identified_term;
+ cidentified_predicate: identified_predicate -> identified_predicate;
+ cexpr: exp -> exp;
+ ccode_annotation: code_annotation -> code_annotation;
+ (* get the copy of a shared value *)
+ get_stmt: stmt -> stmt;
+ get_compinfo: compinfo -> compinfo;
+ get_fieldinfo: fieldinfo -> fieldinfo;
+ get_model_info: model_info -> model_info;
+ get_enuminfo: enuminfo -> enuminfo;
+ get_enumitem: enumitem -> enumitem;
+ get_typeinfo: typeinfo -> typeinfo;
+ get_varinfo: varinfo -> varinfo;
+ get_logic_info: logic_info -> logic_info;
+ get_logic_type_info: logic_type_info -> logic_type_info;
+ get_logic_var: logic_var -> logic_var;
+ get_kernel_function: kernel_function -> kernel_function;
+ get_fundec: fundec -> fundec;
+ (* get the original value tied to a copy *)
+ get_original_stmt: stmt -> stmt;
+ get_original_compinfo: compinfo -> compinfo;
+ get_original_fieldinfo: fieldinfo -> fieldinfo;
+ get_original_model_info: model_info -> model_info;
+ get_original_enuminfo: enuminfo -> enuminfo;
+ get_original_enumitem: enumitem -> enumitem;
+ get_original_typeinfo: typeinfo -> typeinfo;
+ get_original_varinfo: varinfo -> varinfo;
+ get_original_logic_info: logic_info -> logic_info;
+ get_original_logic_type_info: logic_type_info -> logic_type_info;
+ get_original_logic_var: logic_var -> logic_var;
+ get_original_kernel_function: kernel_function -> kernel_function;
+ get_original_fundec: fundec -> fundec;
+ (* change a binding... use with care *)
+ set_stmt: stmt -> stmt -> unit;
+ set_compinfo: compinfo -> compinfo -> unit;
+ set_fieldinfo: fieldinfo -> fieldinfo -> unit;
+ set_model_info: model_info -> model_info -> unit;
+ set_enuminfo: enuminfo -> enuminfo -> unit;
+ set_enumitem: enumitem -> enumitem -> unit;
+ set_typeinfo: typeinfo -> typeinfo -> unit;
+ set_varinfo: varinfo -> varinfo -> unit;
+ set_logic_info: logic_info -> logic_info -> unit;
+ set_logic_type_info: logic_type_info -> logic_type_info -> unit;
+ set_logic_var: logic_var -> logic_var -> unit;
+ set_kernel_function: kernel_function -> kernel_function -> unit;
+ set_fundec: fundec -> fundec -> unit;
+ (* change a reference... use with care *)
+ set_orig_stmt: stmt -> stmt -> unit;
+ set_orig_compinfo: compinfo -> compinfo -> unit;
+ set_orig_fieldinfo: fieldinfo -> fieldinfo -> unit;
+ set_orig_model_info: model_info -> model_info -> unit;
+ set_orig_enuminfo: enuminfo -> enuminfo -> unit;
+ set_orig_enumitem: enumitem -> enumitem -> unit;
+ set_orig_typeinfo: typeinfo -> typeinfo -> unit;
+ set_orig_varinfo: varinfo -> varinfo -> unit;
+ set_orig_logic_info: logic_info -> logic_info -> unit;
+ set_orig_logic_type_info: logic_type_info -> logic_type_info -> unit;
+ set_orig_logic_var: logic_var -> logic_var -> unit;
+ set_orig_kernel_function: kernel_function -> kernel_function -> unit;
+ set_orig_fundec: fundec -> fundec -> unit;
+
+ unset_varinfo: varinfo -> unit;
+ unset_compinfo: compinfo -> unit;
+ unset_enuminfo: enuminfo -> unit;
+ unset_enumitem: enumitem -> unit;
+ unset_typeinfo: typeinfo -> unit;
+ unset_stmt: stmt -> unit;
+ unset_logic_info: logic_info -> unit;
+ unset_logic_type_info: logic_type_info -> unit;
+ unset_fieldinfo: fieldinfo -> unit;
+ unset_model_info: model_info -> unit;
+ unset_logic_var: logic_var -> unit;
+ unset_kernel_function: kernel_function -> unit;
+ unset_fundec: fundec -> unit;
+
+ unset_orig_varinfo: varinfo -> unit;
+ unset_orig_compinfo: compinfo -> unit;
+ unset_orig_enuminfo: enuminfo -> unit;
+ unset_orig_enumitem: enumitem -> unit;
+ unset_orig_typeinfo: typeinfo -> unit;
+ unset_orig_stmt: stmt -> unit;
+ unset_orig_logic_info: logic_info -> unit;
+ unset_orig_logic_type_info: logic_type_info -> unit;
+ unset_orig_fieldinfo: fieldinfo -> unit;
+ unset_orig_model_info: model_info -> unit;
+ unset_orig_logic_var: logic_var -> unit;
+ unset_orig_kernel_function: kernel_function -> unit;
+ unset_orig_fundec: fundec -> unit;
+
+ (* copy fields that can referenced in other places of the AST*)
+ memo_stmt: stmt -> stmt;
+ memo_varinfo: varinfo -> varinfo;
+ memo_compinfo: compinfo -> compinfo;
+ memo_model_info: model_info -> model_info;
+ memo_enuminfo: enuminfo -> enuminfo;
+ memo_enumitem: enumitem -> enumitem;
+ memo_typeinfo: typeinfo -> typeinfo;
+ memo_logic_info: logic_info -> logic_info;
+ memo_logic_type_info: logic_type_info -> logic_type_info;
+ memo_fieldinfo: fieldinfo -> fieldinfo;
+ memo_logic_var: logic_var -> logic_var;
+ memo_kernel_function: kernel_function -> kernel_function;
+ memo_fundec: fundec -> fundec;
+ (* is the behavior a copy behavior *)
+ is_copy_behavior: bool;
+ is_fresh_behavior: bool;
+ project: Project.t option;
+ (* reset memoizing tables *)
+ reset_behavior_varinfo: unit -> unit;
+ reset_behavior_compinfo: unit -> unit;
+ reset_behavior_enuminfo: unit -> unit;
+ reset_behavior_enumitem: unit -> unit;
+ reset_behavior_typeinfo: unit -> unit;
+ reset_behavior_logic_info: unit -> unit;
+ reset_behavior_logic_type_info: unit -> unit;
+ reset_behavior_fieldinfo: unit -> unit;
+ reset_behavior_model_info: unit -> unit;
+ reset_behavior_stmt: unit -> unit;
+ reset_logic_var: unit -> unit;
+ reset_behavior_kernel_function: unit -> unit;
+ reset_behavior_fundec: unit -> unit;
+ (* iterates over tables *)
+ iter_visitor_varinfo: (varinfo -> varinfo -> unit) -> unit;
+ iter_visitor_compinfo: (compinfo -> compinfo -> unit) -> unit;
+ iter_visitor_enuminfo: (enuminfo -> enuminfo -> unit) -> unit;
+ iter_visitor_enumitem: (enumitem -> enumitem -> unit) -> unit;
+ iter_visitor_typeinfo: (typeinfo -> typeinfo -> unit) -> unit;
+ iter_visitor_stmt: (stmt -> stmt -> unit) -> unit;
+ iter_visitor_logic_info: (logic_info -> logic_info -> unit) -> unit;
+ iter_visitor_logic_type_info:
+ (logic_type_info -> logic_type_info -> unit) -> unit;
+ iter_visitor_fieldinfo: (fieldinfo -> fieldinfo -> unit) -> unit;
+ iter_visitor_model_info: (model_info -> model_info -> unit) -> unit;
+ iter_visitor_logic_var: (logic_var -> logic_var -> unit) -> unit;
+ iter_visitor_kernel_function:
+ (kernel_function -> kernel_function -> unit) -> unit;
+ iter_visitor_fundec: (fundec -> fundec -> unit) -> unit;
+ (* folds over tables *)
+ fold_visitor_varinfo: 'a.(varinfo -> varinfo -> 'a -> 'a) -> 'a -> 'a;
+ fold_visitor_compinfo: 'a.(compinfo -> compinfo -> 'a -> 'a) -> 'a -> 'a;
+ fold_visitor_enuminfo: 'a.(enuminfo -> enuminfo -> 'a -> 'a) -> 'a -> 'a;
+ fold_visitor_enumitem: 'a.(enumitem -> enumitem -> 'a -> 'a) -> 'a -> 'a;
+ fold_visitor_typeinfo: 'a.(typeinfo -> typeinfo -> 'a -> 'a) -> 'a -> 'a;
+ fold_visitor_stmt: 'a.(stmt -> stmt -> 'a -> 'a) -> 'a -> 'a;
+ fold_visitor_logic_info:
+ 'a. (logic_info -> logic_info -> 'a -> 'a) -> 'a -> 'a;
+ fold_visitor_logic_type_info:
+ 'a.(logic_type_info -> logic_type_info -> 'a -> 'a) -> 'a -> 'a;
+ fold_visitor_fieldinfo:
+ 'a.(fieldinfo -> fieldinfo -> 'a -> 'a) -> 'a -> 'a;
+ fold_visitor_model_info:
+ 'a. (model_info -> model_info -> 'a -> 'a) -> 'a -> 'a;
+ fold_visitor_logic_var:
+ 'a.(logic_var -> logic_var -> 'a -> 'a) -> 'a -> 'a;
+ fold_visitor_kernel_function:
+ 'a.(kernel_function -> kernel_function -> 'a -> 'a) -> 'a -> 'a;
+ fold_visitor_fundec:
+ 'a.(fundec -> fundec -> 'a -> 'a) -> 'a -> 'a;
+ }
+
+let id = Extlib.id
+let alphabetaunit _ _ = ()
+let alphabetabeta _ x = x
+let unitunit: unit -> unit = id
+let alphaunit _ = ()
+
+let inplace () =
+ { cfile = id;
+ get_compinfo = id;
+ get_fieldinfo = id;
+ get_model_info = id;
+ get_enuminfo = id;
+ get_enumitem = id;
+ get_typeinfo = id;
+ get_varinfo = id;
+ get_logic_var = id;
+ get_stmt = id;
+ get_logic_info = id;
+ get_logic_type_info = id;
+ get_kernel_function = id;
+ get_fundec = id;
+ get_original_compinfo = id;
+ get_original_fieldinfo = id;
+ get_original_model_info = id;
+ get_original_enuminfo = id;
+ get_original_enumitem = id;
+ get_original_typeinfo = id;
+ get_original_varinfo = id;
+ get_original_logic_var = id;
+ get_original_stmt = id;
+ get_original_logic_info = id;
+ get_original_logic_type_info = id;
+ get_original_kernel_function = id;
+ get_original_fundec = id;
+ cinitinfo = id;
+ cblock = id;
+ cfunspec = id;
+ cfunbehavior = id;
+ cidentified_term = id;
+ cidentified_predicate = id;
+ ccode_annotation = id;
+ cexpr = id;
+ is_copy_behavior = false;
+ is_fresh_behavior = false;
+ project = None;
+ memo_varinfo = id;
+ memo_compinfo = id;
+ memo_enuminfo = id;
+ memo_enumitem = id;
+ memo_typeinfo = id;
+ memo_logic_info = id;
+ memo_logic_type_info = id;
+ memo_stmt = id;
+ memo_fieldinfo = id;
+ memo_model_info = id;
+ memo_logic_var = id;
+ memo_kernel_function = id;
+ memo_fundec = id;
+ set_varinfo = alphabetaunit;
+ set_compinfo = alphabetaunit;
+ set_enuminfo = alphabetaunit;
+ set_enumitem = alphabetaunit;
+ set_typeinfo = alphabetaunit;
+ set_logic_info = alphabetaunit;
+ set_logic_type_info = alphabetaunit;
+ set_stmt = alphabetaunit;
+ set_fieldinfo = alphabetaunit;
+ set_model_info = alphabetaunit;
+ set_logic_var = alphabetaunit;
+ set_kernel_function = alphabetaunit;
+ set_fundec = alphabetaunit;
+ set_orig_varinfo = alphabetaunit;
+ set_orig_compinfo = alphabetaunit;
+ set_orig_enuminfo = alphabetaunit;
+ set_orig_enumitem = alphabetaunit;
+ set_orig_typeinfo = alphabetaunit;
+ set_orig_logic_info = alphabetaunit;
+ set_orig_logic_type_info = alphabetaunit;
+ set_orig_stmt = alphabetaunit;
+ set_orig_fieldinfo = alphabetaunit;
+ set_orig_model_info = alphabetaunit;
+ set_orig_logic_var = alphabetaunit;
+ set_orig_kernel_function = alphabetaunit;
+ set_orig_fundec = alphabetaunit;
+ unset_varinfo = alphaunit;
+ unset_compinfo = alphaunit;
+ unset_enuminfo = alphaunit;
+ unset_enumitem = alphaunit;
+ unset_typeinfo = alphaunit;
+ unset_logic_info = alphaunit;
+ unset_logic_type_info = alphaunit;
+ unset_stmt = alphaunit;
+ unset_fieldinfo = alphaunit;
+ unset_model_info = alphaunit;
+ unset_logic_var = alphaunit;
+ unset_kernel_function = alphaunit;
+ unset_fundec = alphaunit;
+ unset_orig_varinfo = alphaunit;
+ unset_orig_compinfo = alphaunit;
+ unset_orig_enuminfo = alphaunit;
+ unset_orig_enumitem = alphaunit;
+ unset_orig_typeinfo = alphaunit;
+ unset_orig_logic_info = alphaunit;
+ unset_orig_logic_type_info = alphaunit;
+ unset_orig_stmt = alphaunit;
+ unset_orig_fieldinfo = alphaunit;
+ unset_orig_model_info = alphaunit;
+ unset_orig_logic_var = alphaunit;
+ unset_orig_kernel_function = alphaunit;
+ unset_orig_fundec = alphaunit;
+ reset_behavior_varinfo = unitunit;
+ reset_behavior_compinfo = unitunit;
+ reset_behavior_enuminfo = unitunit;
+ reset_behavior_enumitem = unitunit;
+ reset_behavior_typeinfo = unitunit;
+ reset_behavior_logic_info = unitunit;
+ reset_behavior_logic_type_info = unitunit;
+ reset_behavior_fieldinfo = unitunit;
+ reset_behavior_model_info = unitunit;
+ reset_behavior_stmt = unitunit;
+ reset_logic_var = unitunit;
+ reset_behavior_kernel_function = unitunit;
+ reset_behavior_fundec = unitunit;
+ iter_visitor_varinfo = alphaunit;
+ iter_visitor_compinfo = alphaunit;
+ iter_visitor_enuminfo = alphaunit;
+ iter_visitor_enumitem = alphaunit;
+ iter_visitor_typeinfo = alphaunit;
+ iter_visitor_stmt = alphaunit;
+ iter_visitor_logic_info = alphaunit;
+ iter_visitor_logic_type_info = alphaunit;
+ iter_visitor_fieldinfo = alphaunit;
+ iter_visitor_model_info = alphaunit;
+ iter_visitor_logic_var = alphaunit;
+ iter_visitor_kernel_function = alphaunit;
+ iter_visitor_fundec = alphaunit;
+ fold_visitor_varinfo = alphabetabeta;
+ fold_visitor_compinfo = alphabetabeta;
+ fold_visitor_enuminfo = alphabetabeta;
+ fold_visitor_enumitem = alphabetabeta;
+ fold_visitor_typeinfo = alphabetabeta;
+ fold_visitor_stmt = alphabetabeta;
+ fold_visitor_logic_info = alphabetabeta;
+ fold_visitor_logic_type_info = alphabetabeta;
+ fold_visitor_fieldinfo = alphabetabeta;
+ fold_visitor_model_info = alphabetabeta;
+ fold_visitor_logic_var = alphabetabeta;
+ fold_visitor_kernel_function = alphabetabeta;
+ fold_visitor_fundec = alphabetabeta;
+ }
+
+let copy_visit_gen fresh prj =
+ let varinfos = Cil_datatype.Varinfo.Hashtbl.create 103 in
+ let compinfos = Cil_datatype.Compinfo.Hashtbl.create 17 in
+ let enuminfos = Cil_datatype.Enuminfo.Hashtbl.create 17 in
+ let enumitems = Cil_datatype.Enumitem.Hashtbl.create 17 in
+ let typeinfos = Cil_datatype.Typeinfo.Hashtbl.create 17 in
+ let logic_infos = Cil_datatype.Logic_info.Hashtbl.create 17 in
+ let logic_type_infos = Cil_datatype.Logic_type_info.Hashtbl.create 17 in
+ let fieldinfos = Cil_datatype.Fieldinfo.Hashtbl.create 17 in
+ let model_infos = Cil_datatype.Model_info.Hashtbl.create 17 in
+ let stmts = Cil_datatype.Stmt.Hashtbl.create 103 in
+ let logic_vars = Cil_datatype.Logic_var.Hashtbl.create 17 in
+ let kernel_functions = Cil_datatype.Kf.Hashtbl.create 17 in
+ let fundecs = Cil_datatype.Varinfo.Hashtbl.create 17 in
+ let orig_varinfos = Cil_datatype.Varinfo.Hashtbl.create 103 in
+ let orig_compinfos = Cil_datatype.Compinfo.Hashtbl.create 17 in
+ let orig_enuminfos = Cil_datatype.Enuminfo.Hashtbl.create 17 in
+ let orig_enumitems = Cil_datatype.Enumitem.Hashtbl.create 17 in
+ let orig_typeinfos = Cil_datatype.Typeinfo.Hashtbl.create 17 in
+ let orig_logic_infos = Cil_datatype.Logic_info.Hashtbl.create 17 in
+ let orig_logic_type_infos = Cil_datatype.Logic_type_info.Hashtbl.create 17 in
+ let orig_fieldinfos = Cil_datatype.Fieldinfo.Hashtbl.create 17 in
+ let orig_model_infos = Cil_datatype.Model_info.Hashtbl.create 17 in
+ let orig_stmts = Cil_datatype.Stmt.Hashtbl.create 103 in
+ let orig_logic_vars = Cil_datatype.Logic_var.Hashtbl.create 17 in
+ let orig_kernel_functions = Cil_datatype.Kf.Hashtbl.create 17 in
+ let orig_fundecs = Cil_datatype.Varinfo.Hashtbl.create 17 in
+ let temp_set_logic_var x new_x =
+ Cil_datatype.Logic_var.Hashtbl.add logic_vars x new_x
+ in
+ let temp_set_orig_logic_var new_x x =
+ Cil_datatype.Logic_var.Hashtbl.add orig_logic_vars new_x x
+ in
+ let temp_unset_logic_var x =
+ Cil_datatype.Logic_var.Hashtbl.remove logic_vars x
+ in
+ let temp_unset_orig_logic_var new_x =
+ Cil_datatype.Logic_var.Hashtbl.remove orig_logic_vars new_x
+ in
+ let temp_memo_logic_var x =
+ (* Format.printf "search for %s#%d@." x.lv_name x.lv_id;*)
+ let res =
+ try Cil_datatype.Logic_var.Hashtbl.find logic_vars x
+ with Not_found ->
+ (* Format.printf "Not found@.";*)
+ let id = if fresh then Cil_const.new_raw_id () else x.lv_id in
+ let new_x = { x with lv_id = id } in
+ temp_set_logic_var x new_x; temp_set_orig_logic_var new_x x; new_x
+ in
+ (* Format.printf "res is %s#%d@." res.lv_name res.lv_id;*)
+ res
+ in
+ let temp_set_varinfo x new_x =
+ Cil_datatype.Varinfo.Hashtbl.add varinfos x new_x;
+ match x.vlogic_var_assoc, new_x.vlogic_var_assoc with
+ | None, _ | _, None -> ()
+ | Some lx, Some new_lx ->
+ Cil_datatype.Logic_var.Hashtbl.add logic_vars lx new_lx
+ in
+ let temp_set_orig_varinfo new_x x =
+ Cil_datatype.Varinfo.Hashtbl.add orig_varinfos new_x x;
+ match new_x.vlogic_var_assoc, x.vlogic_var_assoc with
+ | None, _ | _, None -> ()
+ | Some new_lx, Some lx ->
+ Cil_datatype.Logic_var.Hashtbl.add orig_logic_vars new_lx lx
+ in
+ let temp_unset_varinfo x =
+ Cil_datatype.Varinfo.Hashtbl.remove varinfos x;
+ match x.vlogic_var_assoc with
+ | None -> ()
+ | Some lx -> Cil_datatype.Logic_var.Hashtbl.remove logic_vars lx
+ in
+ let temp_unset_orig_varinfo new_x =
+ Cil_datatype.Varinfo.Hashtbl.remove orig_varinfos new_x;
+ match new_x.vlogic_var_assoc with
+ | None -> ()
+ | Some new_lx ->
+ Cil_datatype.Logic_var.Hashtbl.remove orig_logic_vars new_lx
+ in
+ let temp_memo_varinfo x =
+ try Cil_datatype.Varinfo.Hashtbl.find varinfos x
+ with Not_found ->
+ let new_x =
+ if fresh then Cil_const.copy_with_new_vid x else begin
+ let new_x = { x with vid = x.vid } in
+ (match x.vlogic_var_assoc with
+ | None -> ()
+ | Some lv ->
+ let new_lv = { lv with lv_origin = Some new_x } in
+ new_x.vlogic_var_assoc <- Some new_lv);
+ new_x
+ end
+ in
+ temp_set_varinfo x new_x; temp_set_orig_varinfo new_x x; new_x
+ in
+ let temp_set_fundec f new_f =
+ Cil_datatype.Varinfo.Hashtbl.add fundecs f.svar new_f
+ in
+ let temp_set_orig_fundec new_f f =
+ Cil_datatype.Varinfo.Hashtbl.add orig_fundecs new_f.svar f
+ in
+ let temp_unset_fundec f =
+ Cil_datatype.Varinfo.Hashtbl.remove fundecs f.svar
+ in
+ let temp_unset_orig_fundec new_f =
+ Cil_datatype.Varinfo.Hashtbl.remove orig_fundecs new_f.svar
+ in
+ let temp_memo_fundec f =
+ try Cil_datatype.Varinfo.Hashtbl.find fundecs f.svar
+ with Not_found ->
+ let v = temp_memo_varinfo f.svar in
+ let new_f = { f with svar = v } in
+ temp_set_fundec f new_f; temp_set_orig_fundec new_f f; new_f
+ in
+ let temp_set_kernel_function kf new_kf =
+ Cil_datatype.Kf.Hashtbl.replace kernel_functions kf new_kf;
+ match kf.fundec, new_kf.fundec with
+ | Declaration(_,vi,_,_), Declaration(_,new_vi,_,_)
+ | Declaration(_,vi,_,_), Definition({ svar = new_vi }, _)
+ | Definition({svar = vi},_), Declaration(_,new_vi,_,_) ->
+ temp_set_varinfo vi new_vi
+ | Definition (fundec,_), Definition(new_fundec,_) ->
+ temp_set_fundec fundec new_fundec
+ in
+ let temp_set_orig_kernel_function new_kf kf =
+ Cil_datatype.Kf.Hashtbl.replace orig_kernel_functions new_kf kf;
+ match new_kf.fundec, kf.fundec with
+ | Declaration(_,new_vi,_,_), Declaration(_,vi,_,_)
+ | Declaration(_,new_vi,_,_), Definition({ svar = vi }, _)
+ | Definition({svar = new_vi},_), Declaration(_,vi,_,_) ->
+ temp_set_orig_varinfo new_vi vi
+ | Definition (new_fundec,_), Definition(fundec,_) ->
+ temp_set_orig_fundec new_fundec fundec
+ in
+ let temp_unset_kernel_function kf =
+ Cil_datatype.Kf.Hashtbl.remove kernel_functions kf;
+ match kf.fundec with
+ | Declaration(_,vi,_,_) -> temp_unset_varinfo vi
+ | Definition (fundec,_) -> temp_unset_fundec fundec
+ in
+ let temp_unset_orig_kernel_function new_kf =
+ Cil_datatype.Kf.Hashtbl.remove orig_kernel_functions new_kf;
+ match new_kf.fundec with
+ | Declaration(_,new_vi,_,_) -> temp_unset_orig_varinfo new_vi
+ | Definition (new_fundec,_) -> temp_unset_orig_fundec new_fundec
+ in
+ let temp_memo_kernel_function kf =
+ try Cil_datatype.Kf.Hashtbl.find kernel_functions kf
+ with Not_found ->
+ let new_kf =
+ match kf.fundec with
+ | Declaration (spec,vi,prms,loc) ->
+ let new_vi = temp_memo_varinfo vi in
+ { kf with fundec = Declaration(spec,new_vi,prms,loc) }
+ | Definition(f,loc) ->
+ let new_f = temp_memo_fundec f in
+ { kf with fundec = Definition(new_f,loc) }
+ in
+ temp_set_kernel_function kf new_kf;
+ temp_set_orig_kernel_function new_kf kf;
+ new_kf
+ in
+ let temp_set_compinfo c new_c =
+ Cil_datatype.Compinfo.Hashtbl.add compinfos c new_c;
+ List.iter2
+ (fun f new_f -> Cil_datatype.Fieldinfo.Hashtbl.add fieldinfos f new_f)
+ c.cfields new_c.cfields
+ in
+ let temp_set_orig_compinfo new_c c =
+ Cil_datatype.Compinfo.Hashtbl.add orig_compinfos new_c c;
+ List.iter2
+ (fun new_f f ->
+ Cil_datatype.Fieldinfo.Hashtbl.add orig_fieldinfos new_f f)
+ new_c.cfields c.cfields
+ in
+ let temp_unset_compinfo c =
+ Cil_datatype.Compinfo.Hashtbl.remove compinfos c;
+ List.iter
+ (fun f -> Cil_datatype.Fieldinfo.Hashtbl.remove fieldinfos f) c.cfields
+ in
+ let temp_unset_orig_compinfo new_c =
+ Cil_datatype.Compinfo.Hashtbl.remove orig_compinfos new_c;
+ List.iter
+ (fun new_f ->
+ Cil_datatype.Fieldinfo.Hashtbl.remove orig_fieldinfos new_f)
+ new_c.cfields
+ in
+ let temp_memo_compinfo c =
+ try Cil_datatype.Compinfo.Hashtbl.find compinfos c
+ with Not_found ->
+ let new_c =
+ Cil_const.copyCompInfo ~fresh c c.cname
+ in
+ temp_set_compinfo c new_c; temp_set_orig_compinfo new_c c; new_c
+ in
+ { cfile = (fun x -> { x with fileName = x.fileName });
+ get_compinfo =
+ (fun x ->
+ try Cil_datatype.Compinfo.Hashtbl.find compinfos x with Not_found -> x);
+ get_fieldinfo =
+ (fun x ->
+ try Cil_datatype.Fieldinfo.Hashtbl.find fieldinfos x
+ with Not_found -> x);
+ get_model_info =
+ (fun x ->
+ try Cil_datatype.Model_info.Hashtbl.find model_infos x
+ with Not_found -> x);
+ get_enuminfo =
+ (fun x ->
+ try Cil_datatype.Enuminfo.Hashtbl.find enuminfos x with Not_found -> x);
+ get_enumitem =
+ (fun x ->
+ try Cil_datatype.Enumitem.Hashtbl.find enumitems x with Not_found -> x);
+ get_typeinfo =
+ (fun x ->
+ try Cil_datatype.Typeinfo.Hashtbl.find typeinfos x with Not_found -> x);
+ get_varinfo =
+ (fun x ->
+ try Cil_datatype.Varinfo.Hashtbl.find varinfos x with Not_found -> x);
+ get_stmt =
+ (fun x -> try Cil_datatype.Stmt.Hashtbl.find stmts x with Not_found -> x);
+ get_logic_info =
+ (fun x ->
+ try Cil_datatype.Logic_info.Hashtbl.find logic_infos x
+ with Not_found -> x);
+ get_logic_type_info =
+ (fun x ->
+ try Cil_datatype.Logic_type_info.Hashtbl.find logic_type_infos x
+ with Not_found -> x);
+ get_logic_var =
+ (fun x ->
+ try Cil_datatype.Logic_var.Hashtbl.find logic_vars x
+ with Not_found -> x);
+ get_kernel_function =
+ (fun x ->
+ try Cil_datatype.Kf.Hashtbl.find kernel_functions x
+ with Not_found -> x);
+ get_fundec =
+ (fun x ->
+ try Cil_datatype.Varinfo.Hashtbl.find fundecs x.svar
+ with Not_found -> x);
+ get_original_compinfo =
+ (fun x ->
+ try Cil_datatype.Compinfo.Hashtbl.find orig_compinfos x
+ with Not_found -> x);
+ get_original_fieldinfo =
+ (fun x ->
+ try Cil_datatype.Fieldinfo.Hashtbl.find orig_fieldinfos x
+ with Not_found -> x);
+ get_original_model_info =
+ (fun x ->
+ try Cil_datatype.Model_info.Hashtbl.find orig_model_infos x
+ with Not_found -> x);
+ get_original_enuminfo =
+ (fun x ->
+ try Cil_datatype.Enuminfo.Hashtbl.find orig_enuminfos x
+ with Not_found -> x);
+ get_original_enumitem =
+ (fun x ->
+ try Cil_datatype.Enumitem.Hashtbl.find orig_enumitems x
+ with Not_found -> x);
+ get_original_typeinfo =
+ (fun x ->
+ try Cil_datatype.Typeinfo.Hashtbl.find orig_typeinfos x
+ with Not_found -> x);
+ get_original_varinfo =
+ (fun x ->
+ try Cil_datatype.Varinfo.Hashtbl.find orig_varinfos x
+ with Not_found -> x);
+ get_original_stmt =
+ (fun x ->
+ try Cil_datatype.Stmt.Hashtbl.find orig_stmts x with Not_found -> x);
+ get_original_logic_var =
+ (fun x ->
+ try Cil_datatype.Logic_var.Hashtbl.find orig_logic_vars x
+ with Not_found -> x);
+ get_original_logic_info =
+ (fun x ->
+ try Cil_datatype.Logic_info.Hashtbl.find orig_logic_infos x
+ with Not_found -> x);
+ get_original_logic_type_info =
+ (fun x ->
+ try Cil_datatype.Logic_type_info.Hashtbl.find orig_logic_type_infos x
+ with Not_found -> x);
+ get_original_kernel_function =
+ (fun x ->
+ try Cil_datatype.Kf.Hashtbl.find orig_kernel_functions x
+ with Not_found -> x);
+ get_original_fundec =
+ (fun x ->
+ try Cil_datatype.Varinfo.Hashtbl.find orig_fundecs x.svar
+ with Not_found -> x);
+ cinitinfo = (fun x -> { init = x.init });
+ cblock = (fun x -> { x with battrs = x.battrs });
+ cfunspec = (fun x -> { x with spec_behavior = x.spec_behavior});
+ cfunbehavior = (fun x -> { x with b_name = x.b_name});
+ ccode_annotation =
+ if fresh then Logic_const.refresh_code_annotation
+ else (fun x -> { x with annot_id = x.annot_id });
+ cidentified_predicate =
+ if fresh then Logic_const.refresh_predicate
+ else (fun x -> { x with ip_id = x.ip_id });
+ cidentified_term =
+ if fresh then Logic_const.refresh_identified_term
+ else (fun x -> { x with it_id = x.it_id});
+ cexpr =
+ (fun x ->
+ let id = if fresh then Cil_const.Eid.next () else x.eid in { x with eid = id });
+ is_copy_behavior = true;
+ is_fresh_behavior = fresh;
+ project = Some prj;
+ reset_behavior_varinfo =
+ (fun () ->
+ Cil_datatype.Varinfo.Hashtbl.clear varinfos;
+ Cil_datatype.Varinfo.Hashtbl.clear orig_varinfos);
+ reset_behavior_compinfo =
+ (fun () ->
+ Cil_datatype.Compinfo.Hashtbl.clear compinfos;
+ Cil_datatype.Compinfo.Hashtbl.clear orig_compinfos);
+ reset_behavior_enuminfo =
+ (fun () ->
+ Cil_datatype.Enuminfo.Hashtbl.clear enuminfos;
+ Cil_datatype.Enuminfo.Hashtbl.clear orig_enuminfos);
+ reset_behavior_enumitem =
+ (fun () ->
+ Cil_datatype.Enumitem.Hashtbl.clear enumitems;
+ Cil_datatype.Enumitem.Hashtbl.clear orig_enumitems);
+ reset_behavior_typeinfo =
+ (fun () ->
+ Cil_datatype.Typeinfo.Hashtbl.clear typeinfos;
+ Cil_datatype.Typeinfo.Hashtbl.clear orig_typeinfos);
+ reset_behavior_logic_info =
+ (fun () ->
+ Cil_datatype.Logic_info.Hashtbl.clear logic_infos;
+ Cil_datatype.Logic_info.Hashtbl.clear orig_logic_infos);
+ reset_behavior_logic_type_info =
+ (fun () ->
+ Cil_datatype.Logic_type_info.Hashtbl.clear logic_type_infos;
+ Cil_datatype.Logic_type_info.Hashtbl.clear orig_logic_type_infos);
+ reset_behavior_fieldinfo =
+ (fun () ->
+ Cil_datatype.Fieldinfo.Hashtbl.clear fieldinfos;
+ Cil_datatype.Fieldinfo.Hashtbl.clear orig_fieldinfos);
+ reset_behavior_model_info =
+ (fun () ->
+ Cil_datatype.Model_info.Hashtbl.clear model_infos;
+ Cil_datatype.Model_info.Hashtbl.clear orig_model_infos);
+ reset_behavior_stmt =
+ (fun () ->
+ Cil_datatype.Stmt.Hashtbl.clear stmts;
+ Cil_datatype.Stmt.Hashtbl.clear orig_stmts);
+ reset_logic_var =
+ (fun () ->
+ Cil_datatype.Logic_var.Hashtbl.clear logic_vars;
+ Cil_datatype.Logic_var.Hashtbl.clear orig_logic_vars);
+ reset_behavior_kernel_function =
+ (fun () ->
+ Cil_datatype.Kf.Hashtbl.clear kernel_functions;
+ Cil_datatype.Kf.Hashtbl.clear orig_kernel_functions);
+ reset_behavior_fundec =
+ (fun () ->
+ Cil_datatype.Varinfo.Hashtbl.clear fundecs;
+ Cil_datatype.Varinfo.Hashtbl.clear orig_fundecs);
+ memo_varinfo = temp_memo_varinfo;
+ memo_compinfo = temp_memo_compinfo;
+ memo_enuminfo =
+ (fun x ->
+ try Cil_datatype.Enuminfo.Hashtbl.find enuminfos x
+ with Not_found ->
+ let new_x = { x with ename = x.ename } in
+ Cil_datatype.Enuminfo.Hashtbl.add enuminfos x new_x;
+ Cil_datatype.Enuminfo.Hashtbl.add orig_enuminfos new_x x;
+ new_x);
+ memo_enumitem =
+ (fun x ->
+ try Cil_datatype.Enumitem.Hashtbl.find enumitems x
+ with Not_found ->
+ let new_x = { x with einame = x.einame } in
+ Cil_datatype.Enumitem.Hashtbl.add enumitems x new_x;
+ Cil_datatype.Enumitem.Hashtbl.add orig_enumitems new_x x;
+ new_x);
+ memo_typeinfo =
+ (fun x ->
+ try Cil_datatype.Typeinfo.Hashtbl.find typeinfos x
+ with Not_found ->
+ let new_x = { x with tname = x.tname } in
+ Cil_datatype.Typeinfo.Hashtbl.add typeinfos x new_x;
+ Cil_datatype.Typeinfo.Hashtbl.add orig_typeinfos new_x x;
+ new_x);
+ memo_logic_info =
+ (fun x ->
+ try Cil_datatype.Logic_info.Hashtbl.find logic_infos x
+ with Not_found ->
+ let new_v = temp_memo_logic_var x.l_var_info in
+ let new_x = { x with l_var_info = new_v } in
+ Cil_datatype.Logic_info.Hashtbl.add logic_infos x new_x;
+ Cil_datatype.Logic_info.Hashtbl.add orig_logic_infos new_x x;
+ new_x);
+ memo_logic_type_info =
+ (fun x ->
+ try Cil_datatype.Logic_type_info.Hashtbl.find logic_type_infos x
+ with Not_found ->
+ let new_x = { x with lt_name = x.lt_name } in
+ Cil_datatype.Logic_type_info.Hashtbl.add logic_type_infos x new_x;
+ Cil_datatype.Logic_type_info.Hashtbl.add
+ orig_logic_type_infos new_x x;
+ new_x);
+ memo_stmt =
+ (fun x ->
+ try Cil_datatype.Stmt.Hashtbl.find stmts x
+ with Not_found ->
+ let sid = if fresh then Cil_const.Sid.next () else x.sid in
+ let new_x = { x with sid = sid } in
+ Cil_datatype.Stmt.Hashtbl.add stmts x new_x;
+ Cil_datatype.Stmt.Hashtbl.add orig_stmts new_x x;
+ new_x);
+ memo_fieldinfo =
+ (fun x ->
+ try Cil_datatype.Fieldinfo.Hashtbl.find fieldinfos x
+ with Not_found ->
+ let _ = temp_memo_compinfo x.fcomp in
+ (* memo_compinfo fills the field correspondence table as well *)
+ let new_x = Cil_datatype.Fieldinfo.Hashtbl.find fieldinfos x in
+ Cil_datatype.Fieldinfo.Hashtbl.add fieldinfos x new_x;
+ Cil_datatype.Fieldinfo.Hashtbl.add orig_fieldinfos new_x x;
+ new_x);
+ memo_model_info =
+ (fun x ->
+ try Cil_datatype.Model_info.Hashtbl.find model_infos x
+ with Not_found ->
+ let new_x = { x with mi_name = x.mi_name } in
+ Cil_datatype.Model_info.Hashtbl.add model_infos x new_x;
+ Cil_datatype.Model_info.Hashtbl.add orig_model_infos new_x x;
+ new_x
+ );
+ memo_logic_var = temp_memo_logic_var;
+ memo_kernel_function = temp_memo_kernel_function;
+ memo_fundec = temp_memo_fundec;
+ set_varinfo = temp_set_varinfo;
+ set_compinfo = temp_set_compinfo;
+ set_enuminfo = Cil_datatype.Enuminfo.Hashtbl.replace enuminfos;
+ set_enumitem = Cil_datatype.Enumitem.Hashtbl.replace enumitems;
+ set_typeinfo = Cil_datatype.Typeinfo.Hashtbl.replace typeinfos;
+ set_logic_info = Cil_datatype.Logic_info.Hashtbl.replace logic_infos;
+ set_logic_type_info =
+ Cil_datatype.Logic_type_info.Hashtbl.replace logic_type_infos;
+ set_stmt = Cil_datatype.Stmt.Hashtbl.replace stmts;
+ set_fieldinfo = Cil_datatype.Fieldinfo.Hashtbl.replace fieldinfos;
+ set_model_info = Cil_datatype.Model_info.Hashtbl.replace model_infos;
+ set_logic_var = temp_set_logic_var;
+ set_kernel_function = temp_set_kernel_function;
+ set_fundec = temp_set_fundec;
+ set_orig_varinfo = temp_set_orig_varinfo;
+ set_orig_compinfo = temp_set_orig_compinfo;
+ set_orig_enuminfo = Cil_datatype.Enuminfo.Hashtbl.replace orig_enuminfos;
+ set_orig_enumitem = Cil_datatype.Enumitem.Hashtbl.replace orig_enumitems;
+ set_orig_typeinfo = Cil_datatype.Typeinfo.Hashtbl.replace orig_typeinfos;
+ set_orig_logic_info =
+ Cil_datatype.Logic_info.Hashtbl.replace orig_logic_infos;
+ set_orig_logic_type_info =
+ Cil_datatype.Logic_type_info.Hashtbl.replace orig_logic_type_infos;
+ set_orig_stmt = Cil_datatype.Stmt.Hashtbl.replace orig_stmts;
+ set_orig_fieldinfo =
+ Cil_datatype.Fieldinfo.Hashtbl.replace orig_fieldinfos;
+ set_orig_model_info =
+ Cil_datatype.Model_info.Hashtbl.replace orig_model_infos;
+ set_orig_logic_var = temp_set_orig_logic_var;
+ set_orig_kernel_function = temp_set_orig_kernel_function;
+ set_orig_fundec = temp_set_orig_fundec;
+
+ unset_varinfo = temp_unset_varinfo;
+ unset_compinfo = temp_unset_compinfo;
+ unset_enuminfo = Cil_datatype.Enuminfo.Hashtbl.remove enuminfos;
+ unset_enumitem = Cil_datatype.Enumitem.Hashtbl.remove enumitems;
+ unset_typeinfo = Cil_datatype.Typeinfo.Hashtbl.remove typeinfos;
+ unset_logic_info = Cil_datatype.Logic_info.Hashtbl.remove logic_infos;
+ unset_logic_type_info =
+ Cil_datatype.Logic_type_info.Hashtbl.remove logic_type_infos;
+ unset_stmt = Cil_datatype.Stmt.Hashtbl.remove stmts;
+ unset_fieldinfo = Cil_datatype.Fieldinfo.Hashtbl.remove fieldinfos;
+ unset_model_info = Cil_datatype.Model_info.Hashtbl.remove model_infos;
+ unset_logic_var = temp_unset_logic_var;
+ unset_kernel_function = temp_unset_kernel_function;
+ unset_fundec = temp_unset_fundec;
+
+ unset_orig_varinfo = temp_unset_orig_varinfo;
+ unset_orig_compinfo = temp_unset_orig_compinfo;
+ unset_orig_enuminfo = Cil_datatype.Enuminfo.Hashtbl.remove orig_enuminfos;
+ unset_orig_enumitem = Cil_datatype.Enumitem.Hashtbl.remove orig_enumitems;
+ unset_orig_typeinfo = Cil_datatype.Typeinfo.Hashtbl.remove orig_typeinfos;
+ unset_orig_logic_info =
+ Cil_datatype.Logic_info.Hashtbl.remove orig_logic_infos;
+ unset_orig_logic_type_info =
+ Cil_datatype.Logic_type_info.Hashtbl.remove orig_logic_type_infos;
+ unset_orig_stmt = Cil_datatype.Stmt.Hashtbl.remove orig_stmts;
+ unset_orig_fieldinfo =
+ Cil_datatype.Fieldinfo.Hashtbl.remove orig_fieldinfos;
+ unset_orig_model_info =
+ Cil_datatype.Model_info.Hashtbl.remove orig_model_infos;
+ unset_orig_logic_var = temp_unset_orig_logic_var;
+ unset_orig_kernel_function = temp_unset_orig_kernel_function;
+ unset_orig_fundec = temp_unset_orig_fundec;
+
+ iter_visitor_varinfo =
+ (fun f -> Cil_datatype.Varinfo.Hashtbl.iter f varinfos);
+ iter_visitor_compinfo =
+ (fun f -> Cil_datatype.Compinfo.Hashtbl.iter f compinfos);
+ iter_visitor_enuminfo =
+ (fun f -> Cil_datatype.Enuminfo.Hashtbl.iter f enuminfos);
+ iter_visitor_enumitem =
+ (fun f -> Cil_datatype.Enumitem.Hashtbl.iter f enumitems);
+ iter_visitor_typeinfo =
+ (fun f -> Cil_datatype.Typeinfo.Hashtbl.iter f typeinfos);
+ iter_visitor_stmt =
+ (fun f -> Cil_datatype.Stmt.Hashtbl.iter f stmts);
+ iter_visitor_logic_info =
+ (fun f -> Cil_datatype.Logic_info.Hashtbl.iter f logic_infos);
+ iter_visitor_logic_type_info =
+ (fun f -> Cil_datatype.Logic_type_info.Hashtbl.iter f logic_type_infos);
+ iter_visitor_fieldinfo =
+ (fun f -> Cil_datatype.Fieldinfo.Hashtbl.iter f fieldinfos);
+ iter_visitor_model_info =
+ (fun f -> Cil_datatype.Model_info.Hashtbl.iter f model_infos);
+ iter_visitor_logic_var =
+ (fun f -> Cil_datatype.Logic_var.Hashtbl.iter f logic_vars);
+ iter_visitor_kernel_function =
+ (fun f -> Cil_datatype.Kf.Hashtbl.iter f kernel_functions);
+ iter_visitor_fundec =
+ (fun f ->
+ let f _ new_fundec =
+ let old_fundec =
+ Cil_datatype.Varinfo.Hashtbl.find orig_fundecs new_fundec.svar
+ in
+ f old_fundec new_fundec
+ in
+ Cil_datatype.Varinfo.Hashtbl.iter f fundecs);
+ fold_visitor_varinfo =
+ (fun f i -> Cil_datatype.Varinfo.Hashtbl.fold f varinfos i);
+ fold_visitor_compinfo =
+ (fun f i -> Cil_datatype.Compinfo.Hashtbl.fold f compinfos i);
+ fold_visitor_enuminfo =
+ (fun f i -> Cil_datatype.Enuminfo.Hashtbl.fold f enuminfos i);
+ fold_visitor_enumitem =
+ (fun f i -> Cil_datatype.Enumitem.Hashtbl.fold f enumitems i);
+ fold_visitor_typeinfo =
+ (fun f i -> Cil_datatype.Typeinfo.Hashtbl.fold f typeinfos i);
+ fold_visitor_stmt =
+ (fun f i -> Cil_datatype.Stmt.Hashtbl.fold f stmts i);
+ fold_visitor_logic_info =
+ (fun f i -> Cil_datatype.Logic_info.Hashtbl.fold f logic_infos i);
+ fold_visitor_logic_type_info =
+ (fun f i ->
+ Cil_datatype.Logic_type_info.Hashtbl.fold f logic_type_infos i);
+ fold_visitor_fieldinfo =
+ (fun f i -> Cil_datatype.Fieldinfo.Hashtbl.fold f fieldinfos i);
+ fold_visitor_model_info =
+ (fun f i -> Cil_datatype.Model_info.Hashtbl.fold f model_infos i);
+ fold_visitor_logic_var =
+ (fun f i -> Cil_datatype.Logic_var.Hashtbl.fold f logic_vars i);
+ fold_visitor_kernel_function =
+ (fun f i ->
+ Cil_datatype.Kf.Hashtbl.fold f kernel_functions i);
+ fold_visitor_fundec =
+ (fun f i ->
+ let f _ new_fundec acc =
+ let old_fundec =
+ Cil_datatype.Varinfo.Hashtbl.find orig_fundecs new_fundec.svar
+ in
+ f old_fundec new_fundec acc
+ in
+ Cil_datatype.Varinfo.Hashtbl.fold f fundecs i);
+ }
+
+let copy = copy_visit_gen false
+let refresh = copy_visit_gen true
+
+let is_copy b = b.is_copy_behavior
+let is_fresh b = b.is_fresh_behavior
+
+let get_project b = b.project
+
+let ccode_annotation b = b.ccode_annotation
+let cexpr b = b.cexpr
+let cidentified_predicate b = b.cidentified_predicate
+let cidentified_term b = b.cidentified_term
+let cfunbehavior b = b.cfunbehavior
+let cfunspec b = b.cfunspec
+let cblock b = b.cblock
+let cinitinfo b = b.cinitinfo
+let cfile b = b.cfile
+
+module Memo = struct
+ let varinfo b = b.memo_varinfo
+ let compinfo b = b.memo_compinfo
+ let fieldinfo b = b.memo_fieldinfo
+ let model_info b = b.memo_model_info
+ let enuminfo b = b.memo_enuminfo
+ let enumitem b = b.memo_enumitem
+ let stmt b = b.memo_stmt
+ let typeinfo b = b.memo_typeinfo
+ let logic_info b = b.memo_logic_info
+ let logic_type_info b = b.memo_logic_type_info
+ let logic_var b = b.memo_logic_var
+ let kernel_function b = b.memo_kernel_function
+ let fundec b = b.memo_fundec
+end
+
+module Reset = struct
+ let varinfo b = b.reset_behavior_varinfo ()
+ let compinfo b = b.reset_behavior_compinfo ()
+ let enuminfo b = b.reset_behavior_enuminfo ()
+ let enumitem b = b.reset_behavior_enumitem ()
+ let typeinfo b = b.reset_behavior_typeinfo ()
+ let logic_info b = b.reset_behavior_logic_info ()
+ let logic_type_info b = b.reset_behavior_logic_type_info ()
+ let fieldinfo b = b.reset_behavior_fieldinfo ()
+ let model_info b = b.reset_behavior_model_info ()
+ let stmt b = b.reset_behavior_stmt ()
+ let logic_var b = b.reset_logic_var ()
+ let kernel_function b = b.reset_behavior_kernel_function ()
+ let fundec b = b.reset_behavior_fundec ()
+end
+
+module type Get = sig
+ val varinfo: t -> varinfo -> varinfo
+ val compinfo: t -> compinfo -> compinfo
+ val enuminfo: t -> enuminfo -> enuminfo
+ val enumitem: t -> enumitem -> enumitem
+ val typeinfo: t -> typeinfo -> typeinfo
+ val stmt: t -> stmt -> stmt
+ val logic_info: t -> logic_info -> logic_info
+ val logic_type_info: t -> logic_type_info -> logic_type_info
+ val fieldinfo: t -> fieldinfo -> fieldinfo
+ val model_info: t -> model_info -> model_info
+ val logic_var: t -> logic_var -> logic_var
+ val kernel_function: t -> kernel_function -> kernel_function
+ val fundec: t -> fundec -> fundec
+end
+
+module Get = struct
+ let varinfo b = b.get_varinfo
+ let compinfo b = b.get_compinfo
+ let fieldinfo b = b.get_fieldinfo
+ let model_info b = b.get_model_info
+ let enuminfo b = b.get_enuminfo
+ let enumitem b = b.get_enumitem
+ let stmt b = b.get_stmt
+ let typeinfo b = b.get_typeinfo
+ let logic_info b = b.get_logic_info
+ let logic_type_info b = b.get_logic_type_info
+ let logic_var b = b.get_logic_var
+ let kernel_function b = b.get_kernel_function
+ let fundec b = b.get_fundec
+end
+
+module Get_orig = struct
+ let varinfo b = b.get_original_varinfo
+ let compinfo b = b.get_original_compinfo
+ let fieldinfo b = b.get_original_fieldinfo
+ let model_info b = b.get_original_model_info
+ let enuminfo b = b.get_original_enuminfo
+ let enumitem b = b.get_original_enumitem
+ let stmt b = b.get_original_stmt
+ let typeinfo b = b.get_original_typeinfo
+ let logic_info b = b.get_original_logic_info
+ let logic_type_info b = b.get_original_logic_type_info
+ let logic_var b = b.get_original_logic_var
+ let kernel_function b = b.get_original_kernel_function
+ let fundec b = b.get_original_fundec
+end
+
+module type Set = sig
+ val varinfo: t -> varinfo -> varinfo -> unit
+ val compinfo: t -> compinfo -> compinfo -> unit
+ val enuminfo: t -> enuminfo -> enuminfo -> unit
+ val enumitem: t -> enumitem -> enumitem -> unit
+ val typeinfo: t -> typeinfo -> typeinfo -> unit
+ val stmt: t -> stmt -> stmt -> unit
+
+ val logic_info: t -> logic_info -> logic_info -> unit
+ val logic_type_info:
+ t -> logic_type_info -> logic_type_info -> unit
+ val fieldinfo: t -> fieldinfo -> fieldinfo -> unit
+ val model_info: t -> model_info -> model_info -> unit
+ val logic_var: t -> logic_var -> logic_var -> unit
+ val kernel_function:
+ t -> kernel_function -> kernel_function -> unit
+ val fundec: t -> fundec -> fundec -> unit
+end
+
+module Set = struct
+ let varinfo b = b.set_varinfo
+ let compinfo b = b.set_compinfo
+ let fieldinfo b = b.set_fieldinfo
+ let model_info b = b.set_model_info
+ let enuminfo b = b.set_enuminfo
+ let enumitem b = b.set_enumitem
+ let stmt b = b.set_stmt
+ let typeinfo b = b.set_typeinfo
+ let logic_info b = b.set_logic_info
+ let logic_type_info b = b.set_logic_type_info
+ let logic_var b = b.set_logic_var
+ let kernel_function b = b.set_kernel_function
+ let fundec b = b.set_fundec
+end
+
+module Set_orig = struct
+ let varinfo b = b.set_orig_varinfo
+ let compinfo b = b.set_orig_compinfo
+ let fieldinfo b = b.set_orig_fieldinfo
+ let model_info b = b.set_model_info
+ let enuminfo b = b.set_orig_enuminfo
+ let enumitem b = b.set_orig_enumitem
+ let stmt b = b.set_orig_stmt
+ let typeinfo b = b.set_orig_typeinfo
+ let logic_info b = b.set_orig_logic_info
+ let logic_type_info b = b.set_orig_logic_type_info
+ let logic_var b = b.set_orig_logic_var
+ let kernel_function b = b.set_orig_kernel_function
+ let fundec b = b.set_orig_fundec
+end
+
+module type Unset = sig
+ val varinfo: t -> varinfo -> unit
+ val compinfo: t -> compinfo -> unit
+ val enuminfo: t -> enuminfo -> unit
+ val enumitem: t -> enumitem -> unit
+ val typeinfo: t -> typeinfo -> unit
+ val stmt: t -> stmt -> unit
+
+ val logic_info: t -> logic_info -> unit
+ val logic_type_info: t -> logic_type_info -> unit
+ val fieldinfo: t -> fieldinfo -> unit
+ val model_info: t -> model_info -> unit
+ val logic_var: t -> logic_var -> unit
+ val kernel_function: t -> kernel_function -> unit
+ val fundec: t -> fundec -> unit
+end
+
+module Unset = struct
+ let varinfo b = b.unset_varinfo
+ let compinfo b = b.unset_compinfo
+ let fieldinfo b = b.unset_fieldinfo
+ let model_info b = b.unset_model_info
+ let enuminfo b = b.unset_enuminfo
+ let enumitem b = b.unset_enumitem
+ let stmt b = b.unset_stmt
+ let typeinfo b = b.unset_typeinfo
+ let logic_info b = b.unset_logic_info
+ let logic_type_info b = b.unset_logic_type_info
+ let logic_var b = b.unset_logic_var
+ let kernel_function b = b.unset_kernel_function
+ let fundec b = b.unset_fundec
+end
+
+module Unset_orig = struct
+ let varinfo b = b.unset_orig_varinfo
+ let compinfo b = b.unset_orig_compinfo
+ let fieldinfo b = b.unset_orig_fieldinfo
+ let model_info b = b.unset_model_info
+ let enuminfo b = b.unset_orig_enuminfo
+ let enumitem b = b.unset_orig_enumitem
+ let stmt b = b.unset_orig_stmt
+ let typeinfo b = b.unset_orig_typeinfo
+ let logic_info b = b.unset_orig_logic_info
+ let logic_type_info b = b.unset_orig_logic_type_info
+ let logic_var b = b.unset_orig_logic_var
+ let kernel_function b = b.unset_orig_kernel_function
+ let fundec b = b.unset_orig_fundec
+end
+
+module Iter = struct
+ let varinfo b = b.iter_visitor_varinfo
+ let compinfo b = b.iter_visitor_compinfo
+ let enuminfo b = b.iter_visitor_enuminfo
+ let enumitem b = b.iter_visitor_enumitem
+ let typeinfo b = b.iter_visitor_typeinfo
+ let stmt b = b.iter_visitor_stmt
+ let logic_info b = b.iter_visitor_logic_info
+ let logic_type_info b = b.iter_visitor_logic_type_info
+ let fieldinfo b = b.iter_visitor_fieldinfo
+ let model_info b = b.iter_visitor_model_info
+ let logic_var b = b.iter_visitor_logic_var
+ let kernel_function b = b.iter_visitor_kernel_function
+ let fundec b = b.iter_visitor_fundec
+end
+
+module Fold = struct
+ let varinfo b = b.fold_visitor_varinfo
+ let compinfo b = b.fold_visitor_compinfo
+ let enuminfo b = b.fold_visitor_enuminfo
+ let enumitem b = b.fold_visitor_enumitem
+ let typeinfo b = b.fold_visitor_typeinfo
+ let stmt b = b.fold_visitor_stmt
+ let logic_info b = b.fold_visitor_logic_info
+ let logic_type_info b = b.fold_visitor_logic_type_info
+ let fieldinfo b = b.fold_visitor_fieldinfo
+ let model_info b = b.fold_visitor_model_info
+ let logic_var b = b.fold_visitor_logic_var
+ let kernel_function b = b.fold_visitor_kernel_function
+ let fundec b = b.fold_visitor_fundec
+end
diff --git a/src/kernel_services/visitors/visitor_behavior.mli b/src/kernel_services/visitors/visitor_behavior.mli
new file mode 100644
index 0000000000000000000000000000000000000000..f448e0a69c9840d598a1f8242925b8476507ab52
--- /dev/null
+++ b/src/kernel_services/visitors/visitor_behavior.mli
@@ -0,0 +1,326 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* INRIA (Institut National de Recherche en Informatique et en *)
+(* Automatique) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** Operations on visitor behaviors.
+ @since Potassium-19.0+dev.
+*)
+
+open Cil_types
+
+type t
+(** How the visitor should behave in front of mutable fields: in
+ place modification or copy of the structure. This type is abstract.
+ Use one of the two values below in your classes.
+ @plugin development guide *)
+
+val inplace: unit -> t
+(** In-place modification. Behavior of the original cil visitor.
+ @plugin development guide *)
+
+val copy: Project.t -> t
+(** Makes fresh copies of the mutable structures.
+ - preserves sharing for varinfo.
+ - makes fresh copy of varinfo only for declarations. Variables that are
+ only used in the visited AST are thus still shared with the original
+ AST. This allows for instance to copy a function with its
+ formals and local variables, and to keep the references to other
+ globals in the function's body.
+ @plugin development guide *)
+
+val refresh: Project.t -> t
+(** Makes fresh copies of the mutable structures and provides fresh id
+ for the structures that have ids. Note that as for {!copy_visit}, only
+ varinfo that are declared in the scope of the visit will be copied and
+ provided with a new id.
+*)
+
+(** true iff the behavior provides fresh id for copied structs with id.
+ Always [false] for an inplace visitor.
+*)
+val is_fresh: t -> bool
+
+(** true iff the behavior is a copy behavior. *)
+val is_copy: t -> bool
+
+val get_project: t -> Project.t option
+
+(** Reset operations on behaviors, allows to reset the tables associated to a given
+ kind of AST elements. If you use fresh instances of visitor for each round of
+ transformation, you should not need this module. In place modifications
+ do not need this at all.
+
+ [Reset.ast_element vis] resets the tables associated to the considered type of
+ AST elements in [vis]. For example for {!Cil_types.varinfo}: [Reset.varinfo vis].
+
+ @since Potassium-19.0+dev
+ @plugin development guide
+*)
+module Reset: sig
+ val varinfo: t -> unit
+ val compinfo: t -> unit
+ val enuminfo: t -> unit
+ val enumitem: t -> unit
+ val typeinfo: t -> unit
+ val stmt: t -> unit
+ val logic_info: t -> unit
+ val logic_type_info: t -> unit
+ val fieldinfo: t -> unit
+ val model_info: t -> unit
+ val logic_var: t -> unit
+ val kernel_function: t -> unit
+ val fundec: t -> unit
+end
+
+module type Get = sig
+ val varinfo: t -> varinfo -> varinfo
+ val compinfo: t -> compinfo -> compinfo
+ val enuminfo: t -> enuminfo -> enuminfo
+ val enumitem: t -> enumitem -> enumitem
+ val typeinfo: t -> typeinfo -> typeinfo
+ val stmt: t -> stmt -> stmt
+ val logic_info: t -> logic_info -> logic_info
+ val logic_type_info: t -> logic_type_info -> logic_type_info
+ val fieldinfo: t -> fieldinfo -> fieldinfo
+ val model_info: t -> model_info -> model_info
+ val logic_var: t -> logic_var -> logic_var
+ val kernel_function: t -> kernel_function -> kernel_function
+ val fundec: t -> fundec -> fundec
+end
+
+(** Get operations on behaviors, allows to get the representative of an
+ AST element in the current state of the visitor.
+
+ [Get.ast_element vis e] with [e] of type [ast_element] gets the
+ representative of [e] in [vis]. For example for {!Cil_types.varinfo}:
+ [Get.varinfo vis vi].
+
+ @since Potassium-19.0+dev
+ @plugin development guide
+*)
+module Get: Get
+
+(** Get operations on behaviors, allows to get the original representative of
+ an element of the {b new} AST in the curent state of the visitor.
+
+ [Get_orig.ast_element vis new_e] with [new_e] of type [ast_element] gets the
+ original representative of [new_e] in [vis]. For example for
+ {!Cil_types.varinfo}: [Get_orig.varinfo vis new_vi].
+
+ @since Potassium-19.0+dev
+ @plugin development guide
+*)
+module Get_orig: Get
+
+(** Memo operations on behaviors, allows to get a binding in the new project
+ for the given AST element, creating one if it does not already exists.
+
+ [Memo.ast_element vis e] with [e] of type [ast_element] tries to find a
+ binding to a [e] in the new project created using [vis] in the current
+ state, if it does not exist this binding is created. For example for
+ {!Cil_types.varinfo}: [Memo.varinfo vis vi].
+
+ @since Potassium-19.0+dev
+ @plugin development guide
+*)
+module Memo: Get
+
+module type Set = sig
+ val varinfo: t -> varinfo -> varinfo -> unit
+ val compinfo: t -> compinfo -> compinfo -> unit
+ val enuminfo: t -> enuminfo -> enuminfo -> unit
+ val enumitem: t -> enumitem -> enumitem -> unit
+ val typeinfo: t -> typeinfo -> typeinfo -> unit
+ val stmt: t -> stmt -> stmt -> unit
+
+ val logic_info: t -> logic_info -> logic_info -> unit
+ val logic_type_info:
+ t -> logic_type_info -> logic_type_info -> unit
+ val fieldinfo: t -> fieldinfo -> fieldinfo -> unit
+ val model_info: t -> model_info -> model_info -> unit
+ val logic_var: t -> logic_var -> logic_var -> unit
+ val kernel_function:
+ t -> kernel_function -> kernel_function -> unit
+ val fundec: t -> fundec -> fundec -> unit
+end
+
+(** Set operations on behaviors, allows to change the representative of a
+ given AST element in the current state of the visitor. Use with care
+ (i.e. makes sure that the old one is not referenced anywhere in the
+ AST, or sharing will be lost).
+
+ [Set.ast_element vis e s] with [e] and [s] of type [ast_element] changes
+ the representative of [e] to [s] in [vis]. For example, for
+ {!Cil_types.varinfo}: [Set.varinfo vis vi new_representative].
+
+ @since Potassium-19.0+dev
+ @plugin development guide
+*)
+module Set: Set
+
+(** Set operations on behaviors related to original representatives, allows to
+ change the reference of an element of the {b new} AST in the current state
+ of the visitor. Use with care.
+
+ [Set.ast_element vis e s] with [e] and [s] of type [ast_element] changes
+ the original representative of [e] to [s] in [vis]. For example, for
+ {!Cil_types.varinfo}: [Set_orig.varinfo vis vi new_original_repr].
+
+ @since Potassium-19.0+dev
+*)
+module Set_orig: Set
+
+module type Unset = sig
+ val varinfo: t -> varinfo -> unit
+ val compinfo: t -> compinfo -> unit
+ val enuminfo: t -> enuminfo -> unit
+ val enumitem: t -> enumitem -> unit
+ val typeinfo: t -> typeinfo -> unit
+ val stmt: t -> stmt -> unit
+
+ val logic_info: t -> logic_info -> unit
+ val logic_type_info: t -> logic_type_info -> unit
+ val fieldinfo: t -> fieldinfo -> unit
+ val model_info: t -> model_info -> unit
+ val logic_var: t -> logic_var -> unit
+ val kernel_function: t -> kernel_function -> unit
+ val fundec: t -> fundec -> unit
+end
+
+
+(** Operations to remove the entry associated to a given AST element in the
+ current state of the visitor. Use with care (i.e. make sure that you will
+ never visit again this element in the same visiting context).
+
+ [Unset.ast_element vis e] with [e] of type [ast_element] removes the
+ representative of [e] in the [ast_element] table of [vis]. For example,
+ for {!Cil_types.varinfo}: [Unset.varinfo vis vi].
+
+ @since Potassium-19.0+dev
+*)
+module Unset: Unset
+
+(** Operations to remove the entry associated to a given element of the {b new}
+ AST in the current state of the visitor. Use with care.
+
+ [Unset_orig.ast_element vis e] with [e] of type [ast_element] removes the
+ original representative of [e] in the [ast_element] table of [vis]. For
+ example, for {!Cil_types.varinfo}: [Unset_orig.varinfo vis vi].
+
+ @since Potassium-19.0+dev
+*)
+module Unset_orig: Unset
+
+(** Iter operations on the table of a given type of AST elements.
+
+ [Iter.ast_element vis f], iterates [f] over each pair of [ast_element]
+ registered in [vis]. The [ast_element] in the old AST is presented to [f]
+ first (that is, [f] looks like: [let f old_e new_e = ...]. For example for
+ {!Cil_types.varinfo}: [Iter.varinfo vis (fun old_vi new_vi -> ())].
+
+ @since Potassium-19.0+dev
+*)
+module Iter: sig
+ val varinfo:
+ t -> (varinfo -> varinfo -> unit) -> unit
+ val compinfo:
+ t -> (compinfo -> compinfo -> unit) -> unit
+ val enuminfo:
+ t -> (enuminfo -> enuminfo -> unit) -> unit
+ val enumitem:
+ t -> (enumitem -> enumitem -> unit) -> unit
+ val typeinfo:
+ t -> (typeinfo -> typeinfo -> unit) -> unit
+ val stmt:
+ t -> (stmt -> stmt -> unit) -> unit
+ val logic_info:
+ t -> (logic_info -> logic_info -> unit) -> unit
+ val logic_type_info:
+ t -> (logic_type_info -> logic_type_info -> unit) -> unit
+ val fieldinfo:
+ t -> (fieldinfo -> fieldinfo -> unit) -> unit
+ val model_info:
+ t -> (model_info -> model_info -> unit) -> unit
+ val logic_var:
+ t -> (logic_var -> logic_var -> unit) -> unit
+ val kernel_function:
+ t -> (kernel_function -> kernel_function -> unit) -> unit
+ val fundec:
+ t -> (fundec -> fundec -> unit) -> unit
+end
+
+(** Fold operations on table of a given type of AST elements.
+
+ [Fold.ast_element vis f], folds [f] over each pair of [ast_element]
+ registered in [vis]. The [ast_element] in the old AST is presented to [f]
+ first (that is, [f] looks like: [let f old_e new_e acc = ...]. For example
+ for {!Cil_types.varinfo}:
+ [Fold.varinfo vis (fun old_vi new_vi acc -> ... )].
+
+ @since Potassium-19.0+dev
+*)
+module Fold: sig
+ val varinfo:
+ t -> (varinfo -> varinfo -> 'a -> 'a) -> 'a -> 'a
+ val compinfo:
+ t -> (compinfo -> compinfo -> 'a -> 'a) -> 'a -> 'a
+ val enuminfo:
+ t -> (enuminfo -> enuminfo -> 'a -> 'a) -> 'a -> 'a
+ val enumitem:
+ t -> (enumitem -> enumitem -> 'a -> 'a) -> 'a -> 'a
+ val typeinfo:
+ t -> (typeinfo -> typeinfo -> 'a -> 'a) -> 'a -> 'a
+ val stmt:
+ t -> (stmt -> stmt -> 'a -> 'a) -> 'a -> 'a
+ val logic_info:
+ t -> (logic_info -> logic_info -> 'a -> 'a) -> 'a -> 'a
+ val logic_type_info:
+ t ->
+ (logic_type_info -> logic_type_info -> 'a -> 'a) -> 'a -> 'a
+ val fieldinfo:
+ t -> (fieldinfo -> fieldinfo -> 'a -> 'a) -> 'a -> 'a
+ val model_info:
+ t -> (model_info -> model_info -> 'a -> 'a) -> 'a -> 'a
+ val logic_var:
+ t -> (logic_var -> logic_var -> 'a -> 'a) -> 'a -> 'a
+ val kernel_function:
+ t ->
+ (kernel_function -> kernel_function -> 'a -> 'a) -> 'a -> 'a
+ val fundec:
+ t -> (fundec -> fundec -> 'a -> 'a) -> 'a -> 'a
+end
+
+
+(**/**)
+
+(** For INTERNAL USE only *)
+
+val cfile: t -> file -> file
+val cinitinfo: t -> initinfo -> initinfo
+val cblock: t -> block -> block
+val cfunspec: t -> funspec -> funspec
+val cfunbehavior: t -> funbehavior -> funbehavior
+val cidentified_term: t -> identified_term -> identified_term
+val cidentified_predicate: t -> identified_predicate -> identified_predicate
+val cexpr: t -> exp -> exp
+val ccode_annotation: t -> code_annotation -> code_annotation
diff --git a/src/plugins/aorai/aorai_visitors.ml b/src/plugins/aorai/aorai_visitors.ml
index 68571210062b0840fed735fc4ff2666354155d20..165990df1ce1bf35fe8b81f022bcd9820cd24d98 100644
--- a/src/plugins/aorai/aorai_visitors.ml
+++ b/src/plugins/aorai/aorai_visitors.ml
@@ -978,7 +978,7 @@ object(self)
Cil.mkStmtOneInstr
(Set((Var vi_init,NoOffset), Cil.zero ~loc, loc))
in
- stmt_varset.sid<-(Cil.Sid.next ());
+ stmt_varset.sid<-(Cil_const.Sid.next ());
stmt_varset.ghost<-true;
begin
(* Function adapted from the cil printer *)
diff --git a/src/plugins/constant_propagation/api.ml b/src/plugins/constant_propagation/api.ml
index 58c9aa199a689ab05b50958687f1d4504cd33ed1..88a83bc845c27adf32855a8f2ed694d73200001a 100644
--- a/src/plugins/constant_propagation/api.ml
+++ b/src/plugins/constant_propagation/api.ml
@@ -74,7 +74,7 @@ class propagate project fnames ~cast_intro = object(self)
known_globals <- Varinfo.Set.add vi known_globals;
if Cil.isFunctionType vi.vtype then begin
let kf = Globals.Functions.get vi in
- let new_kf = Cil.memo_kernel_function self#behavior kf in
+ let new_kf = Visitor_behavior.Memo.kernel_function self#behavior kf in
Queue.add (fun () -> Globals.Functions.register new_kf)
self#get_filling_actions;
end
diff --git a/src/plugins/scope/datascope.ml b/src/plugins/scope/datascope.ml
index 007449cd839883d7bc0e23c04090445f2b2be633..2428d248fd935bbd304d08b1ff0d3a298e7753da 100644
--- a/src/plugins/scope/datascope.ml
+++ b/src/plugins/scope/datascope.ml
@@ -571,7 +571,8 @@ class check_annot_visitor = object(self)
method! vcode_annot annot =
let kf = Extlib.the self#current_kf in
let stmt =
- Cil.get_original_stmt self#behavior (Extlib.the self#current_stmt)
+ Visitor_behavior.Get_orig.stmt
+ self#behavior (Extlib.the self#current_stmt)
in
begin match annot.annot_content with
| AAssert _ ->
diff --git a/src/plugins/sparecode/globs.ml b/src/plugins/sparecode/globs.ml
index eb84a71c48abcc51a8426777bde0d3247c18dfec..6021439c1bb1872bed135b5659777adfc9ccf1b1 100644
--- a/src/plugins/sparecode/globs.ml
+++ b/src/plugins/sparecode/globs.ml
@@ -110,7 +110,7 @@ end
class filter_visitor prj = object
- inherit Visitor.generic_frama_c_visitor (Cil.copy_visit prj)
+ inherit Visitor.generic_frama_c_visitor (Visitor_behavior.copy prj)
method! vglob_aux g =
match g with
diff --git a/src/plugins/wp/normAtLabels.ml b/src/plugins/wp/normAtLabels.ml
index c876927da3c546f5a455079e05aba5710743e281..8a01575729702dc47de5c17c51f41cf9f03c8f4f 100644
--- a/src/plugins/wp/normAtLabels.ml
+++ b/src/plugins/wp/normAtLabels.ml
@@ -33,7 +33,8 @@ type label_mapping = Cil_types.logic_label -> Clabels.c_label
* *)
class norm_at (mapping : label_mapping) =
object(self)
- inherit Visitor.generic_frama_c_visitor (Cil.copy_visit (Project.current ()))
+ inherit Visitor.generic_frama_c_visitor
+ (Visitor_behavior.copy (Project.current ()))
val mutable current_label = None
diff --git a/tests/misc/bug_0209.ml b/tests/misc/bug_0209.ml
index 37134ef7eee872aae616f6f82f9faefc609b55ab..b46478f7925e914d25506a3200d3d9e87b55885f 100644
--- a/tests/misc/bug_0209.ml
+++ b/tests/misc/bug_0209.ml
@@ -3,7 +3,8 @@ let main () =
Logic_env.Builtins.apply *)
ignore
(File.create_project_from_visitor "foo"
- (fun p -> new Visitor.generic_frama_c_visitor (Cil.copy_visit p)));
+ (fun p ->
+ new Visitor.generic_frama_c_visitor (Visitor_behavior.copy p)));
let p = Project.create "bar" in
(* Computing the AST first calls File.cil_init, than calls
Logic_env.Builtins.apply. This second call raises an exception because
diff --git a/tests/spec/Extend.ml b/tests/spec/Extend.ml
index 980bcae57360b3ee4084f357dec73b8539d1f77d..eeb9585d6abde841f316f8a96dac43e883765f1a 100644
--- a/tests/spec/Extend.ml
+++ b/tests/spec/Extend.ml
@@ -50,7 +50,7 @@ let visit_bar vis ext =
| Ext_id idx ->
let l = Bar_table.find idx in
let l' = Cil.mapNoCopy (Cil.visitCilPredicate vis) l in
- if Cil.is_copy_behavior vis#behavior then begin
+ if Visitor_behavior.is_copy vis#behavior then begin
let idx' = Count.next () in
Queue.add (fun () -> Bar_table.add idx' l') vis#get_filling_actions;
Cil.ChangeTo(Ext_id idx')
diff --git a/tests/spec/property_test.ml b/tests/spec/property_test.ml
index 1fef091214845c4be83ef7b5bffac13e3ff84d95..443e8cefd62dc590c13935476210378f744f6037 100644
--- a/tests/spec/property_test.ml
+++ b/tests/spec/property_test.ml
@@ -20,7 +20,7 @@ class visit prj =
From [ Logic_const.new_identified_term (Logic_const.tvar x);
Logic_const.new_identified_term (Logic_const.tvar c)]
];
- let nkf = Cil.get_kernel_function self#behavior kf in
+ let nkf = Visitor_behavior.Get.kernel_function self#behavior kf in
let keep_empty = true in
let post b =
Queue.add
diff --git a/tests/syntax/Refresh_visitor.ml b/tests/syntax/Refresh_visitor.ml
index 850219bceb5a5a5aa51e785b951026d946af2f89..9a82d0fd6b4635681d12e70869a6769a7fa6283e 100644
--- a/tests/syntax/Refresh_visitor.ml
+++ b/tests/syntax/Refresh_visitor.ml
@@ -1,5 +1,5 @@
open Cil_types
-open Cil
+open Visitor_behavior
let category = Kernel.register_category "refresh-test"
@@ -31,7 +31,7 @@ let main () =
File.init_project_from_visitor p vis;
Cil_datatype.(
let orig_id, copy_id, shared_id =
- CheckVarinfo.check "varinfo" fold_visitor_varinfo vis#behavior
+ CheckVarinfo.check "varinfo" Fold.varinfo vis#behavior
in
if Kernel.is_debug_key_enabled category then begin
Varinfo.Set.iter
@@ -47,13 +47,13 @@ let main () =
shared_id;
end;
let _ =
- CheckCompinfo.check "compinfo" fold_visitor_compinfo vis#behavior
+ CheckCompinfo.check "compinfo" Fold.compinfo vis#behavior
in
let _ =
- CheckStmt.check "stmt" fold_visitor_stmt vis#behavior;
+ CheckStmt.check "stmt" Fold.stmt vis#behavior;
in
let orig_id, copy_id, shared_id =
- CheckLogic_var.check "logic var" fold_visitor_logic_var vis#behavior
+ CheckLogic_var.check "logic var" Fold.logic_var vis#behavior
in
if Kernel.is_debug_key_enabled category then begin
Logic_var.Set.iter
diff --git a/tests/syntax/copy_visitor_bts_1073.ml b/tests/syntax/copy_visitor_bts_1073.ml
index 52073e68ac26990a41d8d51031ff529fe52d0675..a8bf07b17d614fc3f967f5aebdc594039b47403d 100644
--- a/tests/syntax/copy_visitor_bts_1073.ml
+++ b/tests/syntax/copy_visitor_bts_1073.ml
@@ -11,11 +11,11 @@ object(self)
let f1 = Visitor.visitFramacFunction (self:>Visitor.frama_c_visitor) f
in
let v2 = Cil.copyVarinfo f.svar (f.svar.vname ^ "1") in
- let orig = Cil.get_original_varinfo self#behavior f.svar in
- Cil.set_varinfo self#behavior orig v2;
- Cil.set_orig_varinfo self#behavior v2 orig;
- Cil.reset_behavior_fundec self#behavior;
- Cil.reset_behavior_stmt self#behavior;
+ let orig = Visitor_behavior.Get_orig.varinfo self#behavior f.svar in
+ Visitor_behavior.Set.varinfo self#behavior orig v2;
+ Visitor_behavior.Set_orig.varinfo self#behavior v2 orig;
+ Visitor_behavior.Reset.fundec self#behavior;
+ Visitor_behavior.Reset.stmt self#behavior;
let f2 = Visitor.visitFramacFunction (self:>Visitor.frama_c_visitor) f
in
f2.svar <- v2;
diff --git a/tests/syntax/transient_block.ml b/tests/syntax/transient_block.ml
index 0bf3ce8e4aa34403c82d326a1954c14eb805e4e7..0938b72d74627597f86fd7fe7c6070c363e36bac 100644
--- a/tests/syntax/transient_block.ml
+++ b/tests/syntax/transient_block.ml
@@ -9,7 +9,8 @@ class vis prj = object(self)
let s1 = Cil.mkStmtOneInstr ~valid_sid:true instr in
let b = Cil.mkBlock [s1] in
if create then begin
- let f = Cil.get_fundec self#behavior (Extlib.the self#current_func) in
+ let f = Visitor_behavior.Get.fundec
+ self#behavior (Extlib.the self#current_func) in
let y = Cil.makeLocalVar f ~scope:b "y" (TInt(IInt,[])) in
my_var <- Some y;
let loc = Cil_datatype.Location.unknown in
@@ -31,7 +32,8 @@ class vis prj = object(self)
with Log.AbortFatal _ ->
Kernel.feedback "transient_block fatal error on %a as expected"
Printer.pp_instr instr;
- let f = Cil.get_fundec self#behavior (Extlib.the self#current_func) in
+ let f = Visitor_behavior.Get.fundec
+ self#behavior (Extlib.the self#current_func) in
let y = Extlib.the my_var in
f.slocals <-
List.filter