diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 6a230a5b505ffc5ca0c25afa8b1a8517f386bded..1b595764bf03ef02f94a6901f87658e97ab5b21d 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -9997,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 (Visitor_behavior.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_services/analysis/exn_flow.ml b/src/kernel_services/analysis/exn_flow.ml index ee42ce089bdae6c5ddee9ac08bd71a642b262a47..8a1904e4b5bf025af481464ee7e0f8c0bc2c4ded 100644 --- a/src/kernel_services/analysis/exn_flow.ml +++ b/src/kernel_services/analysis/exn_flow.ml @@ -693,9 +693,9 @@ object(self) method private clean_catch_clause (bind,b as handler) acc = let remove_local v = let f = - Visitor_behavior.get_fundec self#behavior (Extlib.the self#current_func) + Visitor_behavior.Get.fundec self#behavior (Extlib.the self#current_func) in - let v = Visitor_behavior.get_varinfo self#behavior v 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 470fced61f35914ee8535c6f043cfd731a5fe1ad..1a2466fb8455701a27969258ef45691994692a44 100644 --- a/src/kernel_services/ast_queries/cil.ml +++ b/src/kernel_services/ast_queries/cil.ml @@ -55,7 +55,6 @@ open Logic_const open Format open Cil_datatype open Cil_types -module VisBhv = Visitor_behavior (* ************************************************************************* *) (* Reporting messages *) @@ -737,7 +736,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: VisBhv.t + method behavior: Visitor_behavior.t method project: Project.t option @@ -918,7 +917,7 @@ class internal_genericCilVisitor current_func behavior queue: cilVisitor = object(self) method behavior = behavior - method project = VisBhv.get_project behavior + method project = Visitor_behavior.get_project behavior method plain_copy_visitor = let obj = @@ -1054,7 +1053,7 @@ class genericCilVisitor bhv = internal_genericCilVisitor current_func bhv queue class nopCilVisitor = object - inherit genericCilVisitor (VisBhv.inplace_visit ()) + inherit genericCilVisitor (Visitor_behavior.inplace ()) end let apply_on_project ?selection vis f arg = @@ -1276,14 +1275,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' = VisBhv.get_enumitem vis#behavior 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' = VisBhv.get_enumitem vis#behavior ei in + let ei' = Visitor_behavior.Get.enumitem vis#behavior ei in if ei' != ei then LEnum ei' else c | _ -> c @@ -1436,12 +1435,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 := VisBhv.get_stmt vis#behavior !s; l + StmtLabel s -> s := Visitor_behavior.Get.stmt vis#behavior !s; l | FormalLabel _ | BuiltinLabel _ -> l and visitCilTermLval vis tl = @@ -1474,21 +1473,21 @@ and childrenTermOffset vis toff = TNoOffset -> toff | TField (fi, t) -> let t' = vOffset t in - let fi' = VisBhv.get_fieldinfo vis#behavior 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' = VisBhv.get_model_info vis#behavior 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 (VisBhv.get_logic_info vis#behavior) + doVisitCil vis (Visitor_behavior.Get.logic_info vis#behavior) vis#vlogic_info_use alphabetabeta li in new_li.l_var_info <- new_v; @@ -1501,7 +1500,7 @@ and visitCilLogicInfo vis li = let new_v = visitCilLogicVarDecl vis li.l_var_info in let res = doVisitCil - vis (VisBhv.memo_logic_info vis#behavior) + vis (Visitor_behavior.Memo.logic_info vis#behavior) vis#vlogic_info_decl childrenLogicInfo li in res.l_var_info <- new_v; res @@ -1536,7 +1535,7 @@ and childrenLogicInfo vis li = li and visitCilLogicTypeInfo vis lt = - doVisitCil vis (VisBhv.memo_logic_type_info vis#behavior) + doVisitCil vis (Visitor_behavior.Memo.logic_type_info vis#behavior) vis#vlogic_type_info_decl childrenLogicTypeInfo lt and childrenLogicTypeInfo vis lt = @@ -1557,7 +1556,7 @@ and childrenLogicTypeDef vis def = and visitCilLogicCtorInfoAddTable vis ctor = let ctor' = visitCilLogicCtorInfo vis ctor in - if VisBhv.is_copy vis#behavior then + if Visitor_behavior.is_copy vis#behavior then Queue.add (fun () -> Logic_env.add_logic_ctor ctor'.ctor_name ctor') @@ -1568,7 +1567,7 @@ and visitCilLogicCtorInfo vis ctor = doVisitCil vis id vis#vlogic_ctor_info_decl childrenLogicCtorInfo ctor and childrenLogicCtorInfo vis ctor = - let ctor_type = doVisitCil vis (VisBhv.get_logic_type_info vis#behavior) + 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 @@ -1587,7 +1586,7 @@ and childrenLogicType vis ty = if t != t' then Ctype t' else ty | Linteger | Lreal -> ty | Ltype (s,l) -> - let s' = doVisitCil vis (VisBhv.get_logic_type_info vis#behavior) + 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 @@ -1602,7 +1601,7 @@ and visitCilLogicVarDecl vis lv = (match lv.lv_origin with None -> () | Some cv -> lv.lv_name <- cv.vname); - doVisitCil vis (VisBhv.memo_logic_var vis#behavior) vis#vlogic_var_decl + doVisitCil vis (Visitor_behavior.Memo.logic_var vis#behavior) vis#vlogic_var_decl childrenLogicVarDecl lv and childrenLogicVarDecl vis lv = @@ -1612,7 +1611,7 @@ and childrenLogicVarDecl vis lv = lv and visitCilLogicVarUse vis lv = - if VisBhv.is_copy vis#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. @@ -1640,7 +1639,7 @@ and visitCilLogicVarUse vis lv = end) vis#get_filling_actions; end; - doVisitCil vis (VisBhv.get_logic_var vis#behavior) vis#vlogic_var_use + doVisitCil vis (Visitor_behavior.Get.logic_var vis#behavior) vis#vlogic_var_use childrenLogicVarUse lv and childrenLogicVarUse vis lv = @@ -1653,7 +1652,7 @@ and visitCilQuantifiers vis lv = and visitCilIdPredicate vis ip = doVisitCil vis - (VisBhv.cidentified_predicate vis#behavior) + (Visitor_behavior.cidentified_predicate vis#behavior) vis#videntified_predicate childrenIdentified_predicate ip @@ -1793,7 +1792,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 (VisBhv.cidentified_term vis#behavior) 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 @@ -1842,7 +1841,7 @@ and childrenDeps vis d = if l !=l' then From l' else d and visitCilBehavior vis b = - doVisitCil vis (VisBhv.cfunbehavior vis#behavior) + doVisitCil vis (Visitor_behavior.cfunbehavior vis#behavior) vis#vbehavior childrenBehavior b and childrenBehavior vis b = @@ -1864,7 +1863,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'} @@ -1884,7 +1883,7 @@ and visitCilPredicates vis ps = mapNoCopy (visitCilIdPredicate vis) ps and visitCilBehaviors vis bs = mapNoCopy (visitCilBehavior vis) bs and visitCilFunspec vis s = - doVisitCil vis (VisBhv.cfunspec vis#behavior) 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; @@ -1947,13 +1946,13 @@ and visitCilModelInfo vis m = CurrentLoc.set m.mi_decl; let m' = doVisitCil - vis (VisBhv.memo_model_info vis#behavior) 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. *) - VisBhv.set_model_info vis#behavior m m'; - VisBhv.set_orig_model_info vis#behavior m' m; + Visitor_behavior.Set.model_info vis#behavior m m'; + Visitor_behavior.Set_orig.model_info vis#behavior m' m; end; m' @@ -1968,7 +1967,7 @@ and childrenAnnotation vis a = match a with | Dfun_or_pred (li,loc) -> let li' = visitCilLogicInfo vis li in - if VisBhv.is_copy vis#behavior then + if Visitor_behavior.is_copy vis#behavior then Queue.add (fun () -> Logic_env.add_logic_function_gen alphabetafalse li') @@ -1976,7 +1975,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 VisBhv.is_copy vis#behavior then + if Visitor_behavior.is_copy vis#behavior then Queue.add (fun () -> Logic_env.add_logic_type ti'.lt_name ti') @@ -1990,21 +1989,21 @@ and childrenAnnotation vis a = else a | Dinvariant (p,loc) -> let p' = visitCilLogicInfo vis p in - if VisBhv.is_copy vis#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 VisBhv.is_copy vis#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 VisBhv.is_copy vis#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 @@ -2033,7 +2032,7 @@ and childrenAnnotation vis a = and visitCilCodeAnnotation vis ca = doVisitCil - vis (VisBhv.ccode_annotation vis#behavior) 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 @@ -2078,7 +2077,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 (VisBhv.cexpr vis#behavior) 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 = @@ -2180,7 +2179,7 @@ and childrenOffset (vis: cilVisitor) (off: offset) : offset = match off with Field (f, o) -> let o' = vOff o in - let f' = VisBhv.get_fieldinfo vis#behavior 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 @@ -2261,8 +2260,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 VisBhv.is_copy vis#behavior then - List.map (fun s -> ref (VisBhv.memo_stmt vis#behavior !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 @@ -2286,7 +2285,7 @@ and visitCilStmt (vis:cilVisitor) (s: stmt) : stmt = let toPrepend : instr list ref = ref [] in (* childrenStmt may add to this *) let res = doVisitCil vis - (VisBhv.memo_stmt vis#behavior) 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 (); @@ -2330,9 +2329,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 VisBhv.is_copy vis#behavior then + if Visitor_behavior.is_copy vis#behavior then (* we need new references anyway, no need for mapNoCopy *) - List.map (fun x -> ref (VisBhv.memo_stmt vis#behavior !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 || @@ -2344,8 +2343,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 VisBhv.is_copy vis#behavior then - Goto(ref (VisBhv.memo_stmt vis#behavior !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 @@ -2368,7 +2367,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 (VisBhv.get_stmt vis#behavior) 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 @@ -2450,8 +2449,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' = VisBhv.cblock vis#behavior b in - if VisBhv.is_copy vis#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 @@ -2459,7 +2458,7 @@ and visitCilBlock (vis: cilVisitor) (b: block) : block = *) match vis#current_func with | Some fd when fd.sbody == b -> - (VisBhv.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' @@ -2469,8 +2468,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 (VisBhv.get_varinfo vis#behavior) b.blocals in - let statics' = mapNoCopy (VisBhv.get_varinfo vis#behavior) 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 @@ -2501,7 +2500,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' = VisBhv.get_compinfo vis#behavior 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 @@ -2522,11 +2521,11 @@ and childrenType (vis : cilVisitor) (t : typ) : typ = | TNamed(t1, a) -> let a' = fAttr a in - let t1' = VisBhv.get_typeinfo vis#behavior 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' = VisBhv.get_enuminfo vis#behavior 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. *) @@ -2540,7 +2539,7 @@ and visitCilVarDecl (vis : cilVisitor) (v : varinfo) : varinfo = let oldloc = CurrentLoc.get () in CurrentLoc.set v.vdecl; let res = - doVisitCil vis (VisBhv.memo_varinfo vis#behavior) + doVisitCil vis (Visitor_behavior.Memo.varinfo vis#behavior) vis#vvdec childrenVarDecl v in CurrentLoc.set oldloc; res @@ -2548,7 +2547,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 = VisBhv.get_original_logic_var vis#behavior lv in + let o = Visitor_behavior.Get_orig.logic_var vis#behavior lv in visitCilLogicVarDecl vis o in v.vtype <- visitCilType vis v.vtype; @@ -2557,7 +2556,7 @@ and childrenVarDecl (vis : cilVisitor) (v : varinfo) : varinfo = v and visitCilVarUse vis v = - doVisitCil vis (VisBhv.get_varinfo vis#behavior) 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' = @@ -2631,19 +2630,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 (VisBhv.get_stmt b) stmt.succs; - stmt.preds <- mapNoCopy (VisBhv.get_stmt b) 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 (VisBhv.get_stmt b) 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 (VisBhv.get_stmt b) stmt1 in - let stmt2' = optMapNoCopy (VisBhv.get_stmt b) 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,_) -> @@ -2659,7 +2658,7 @@ let rec visitCilFunction (vis : cilVisitor) (f : fundec) : fundec = assertEmptyQueue vis; vis#set_current_func f; (* update fundec tables *) - let f = VisBhv.memo_fundec vis#behavior 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 @@ -2668,10 +2667,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 VisBhv.is_copy vis#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 (VisBhv.get_stmt vis#behavior) f.sallstmts) + List.rev (List.rev_map (Visitor_behavior.Get.stmt vis#behavior) f.sallstmts) end; vis#reset_current_func (); f @@ -2680,7 +2679,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 = VisBhv.get_original_varinfo vis#behavior 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 @@ -2694,7 +2693,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 VisBhv.is_copy vis#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 @@ -2716,8 +2715,8 @@ let childrenFieldInfo vis fi = fi let visitCilFieldInfo vis f = - let f = VisBhv.get_original_fieldinfo vis#behavior f in - doVisitCil vis (VisBhv.memo_fieldinfo vis#behavior) 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; @@ -2725,15 +2724,15 @@ let childrenCompInfo vis comp = comp let visitCilCompInfo vis c = - doVisitCil vis (VisBhv.memo_compinfo vis#behavior) 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 <- VisBhv.get_enuminfo vis#behavior e.eihost; + e.eihost <- Visitor_behavior.Get.enuminfo vis#behavior e.eihost; e let visitCilEnumItem vis e = - doVisitCil vis (VisBhv.memo_enumitem vis#behavior) 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; @@ -2741,7 +2740,7 @@ let childrenEnumInfo vis e = e let visitCilEnumInfo vis e = - doVisitCil vis (VisBhv.memo_enuminfo vis#behavior) 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 @@ -2756,15 +2755,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' = VisBhv.memo_typeinfo vis#behavior 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' = VisBhv.memo_enuminfo vis#behavior 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' = VisBhv.memo_compinfo vis#behavior 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 @@ -2783,7 +2782,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 VisBhv.is_copy 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 @@ -2794,7 +2793,7 @@ and childrenGlobal (vis: cilVisitor) (g: global) : global = begin (match form' with | Some formals - when VisBhv.is_copy vis#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 @@ -2804,7 +2803,7 @@ and childrenGlobal (vis: cilVisitor) (g: global) : global = else g | GVar (v, inito, l) -> let v' = visitCilVarDecl vis v in - let inito' = VisBhv.cinitinfo vis#behavior 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 @@ -5384,7 +5383,7 @@ let removeOffsetLval ((b, off): lval) : lval * offset = (b, off'), last class copyVisitExpr = object - inherit genericCilVisitor (VisBhv.copy_visit (Project.current ())) + inherit genericCilVisitor (Visitor_behavior.copy (Project.current ())) method! vexpr e = ChangeDoChildrenPost ({e with eid = Eid.next ()}, fun x -> x) end @@ -5493,11 +5492,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 VisBhv.is_copy vis#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 (VisBhv.cfile vis#behavior) (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 @@ -5516,13 +5515,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 VisBhv.is_copy vis#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 (VisBhv.cfile vis#behavior) (post_file vis) childrenFileCopy f + doVisitCil vis (Visitor_behavior.cfile vis#behavior) (post_file vis) childrenFileCopy f let visitCilFile vis f = - if VisBhv.is_copy vis#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) @@ -6989,7 +6988,7 @@ let () = dependency_on_ast Switch_cases.self let separate_switch_succs = Switch_cases.memo separate_switch_succs class dropAttributes ?select () = object - inherit genericCilVisitor (VisBhv.copy_visit (Project.current ())) + inherit genericCilVisitor (Visitor_behavior.copy (Project.current ())) method! vattr a = match select with | None -> ChangeTo [] @@ -7026,154 +7025,154 @@ let typeHasAttributeDeep t = (* Visitor behavior compatibility *) -type visitor_behavior = VisBhv.t - -let refresh_visit = VisBhv.refresh_visit -let copy_visit = VisBhv.copy_visit -let inplace_visit = VisBhv.inplace_visit - -let is_copy_behavior = VisBhv.is_copy -let is_fresh_behavior = VisBhv.is_fresh - -let memo_varinfo = VisBhv.memo_varinfo -let memo_compinfo = VisBhv.memo_compinfo -let memo_fieldinfo = VisBhv.memo_fieldinfo -let memo_model_info = VisBhv.memo_model_info -let memo_enuminfo = VisBhv.memo_enuminfo -let memo_enumitem = VisBhv.memo_enumitem -let memo_stmt = VisBhv.memo_stmt -let memo_typeinfo = VisBhv.memo_typeinfo -let memo_logic_info = VisBhv.memo_logic_info -let memo_logic_type_info = VisBhv.memo_logic_type_info -let memo_logic_var = VisBhv.memo_logic_var -let memo_kernel_function = VisBhv.memo_kernel_function -let memo_fundec = VisBhv.memo_fundec - -let reset_behavior_varinfo = VisBhv.reset_varinfo -let reset_behavior_compinfo = VisBhv.reset_compinfo -let reset_behavior_enuminfo = VisBhv.reset_enuminfo -let reset_behavior_enumitem = VisBhv.reset_enumitem -let reset_behavior_typeinfo = VisBhv.reset_typeinfo -let reset_behavior_logic_info = VisBhv.reset_logic_info -let reset_behavior_logic_type_info = VisBhv.reset_logic_type_info -let reset_behavior_fieldinfo = VisBhv.reset_fieldinfo -let reset_behavior_model_info = VisBhv.reset_model_info -let reset_behavior_stmt = VisBhv.reset_stmt -let reset_logic_var = VisBhv.reset_logic_var -let reset_behavior_kernel_function = VisBhv.reset_kernel_function -let reset_behavior_fundec = VisBhv.reset_fundec - -let get_varinfo = VisBhv.get_varinfo -let get_compinfo = VisBhv.get_compinfo -let get_fieldinfo = VisBhv.get_fieldinfo -let get_model_info = VisBhv.get_model_info -let get_enuminfo = VisBhv.get_enuminfo -let get_enumitem = VisBhv.get_enumitem -let get_stmt = VisBhv.get_stmt -let get_typeinfo = VisBhv.get_typeinfo -let get_logic_info = VisBhv.get_logic_info -let get_logic_type_info = VisBhv.get_logic_type_info -let get_logic_var = VisBhv.get_logic_var -let get_kernel_function = VisBhv.get_kernel_function -let get_fundec = VisBhv.get_fundec - -let get_original_varinfo = VisBhv.get_original_varinfo -let get_original_compinfo = VisBhv.get_original_compinfo -let get_original_fieldinfo = VisBhv.get_original_fieldinfo -let get_original_model_info = VisBhv.get_original_model_info -let get_original_enuminfo = VisBhv.get_original_enuminfo -let get_original_enumitem = VisBhv.get_original_enumitem -let get_original_stmt = VisBhv.get_original_stmt -let get_original_typeinfo = VisBhv.get_original_typeinfo -let get_original_logic_info = VisBhv.get_original_logic_info -let get_original_logic_type_info = VisBhv.get_original_logic_type_info -let get_original_logic_var = VisBhv.get_original_logic_var -let get_original_kernel_function = VisBhv.get_original_kernel_function -let get_original_fundec = VisBhv.get_original_fundec - -let set_varinfo = VisBhv.set_varinfo -let set_compinfo = VisBhv.set_compinfo -let set_fieldinfo = VisBhv.set_fieldinfo -let set_model_info = VisBhv.set_model_info -let set_enuminfo = VisBhv.set_enuminfo -let set_enumitem = VisBhv.set_enumitem -let set_stmt = VisBhv.set_stmt -let set_typeinfo = VisBhv.set_typeinfo -let set_logic_info = VisBhv.set_logic_info -let set_logic_type_info = VisBhv.set_logic_type_info -let set_logic_var = VisBhv.set_logic_var -let set_kernel_function = VisBhv.set_kernel_function -let set_fundec = VisBhv.set_fundec - -let set_orig_varinfo = VisBhv.set_orig_varinfo -let set_orig_compinfo = VisBhv.set_orig_compinfo -let set_orig_fieldinfo = VisBhv.set_orig_fieldinfo -let set_orig_model_info = VisBhv.set_model_info -let set_orig_enuminfo = VisBhv.set_orig_enuminfo -let set_orig_enumitem = VisBhv.set_orig_enumitem -let set_orig_stmt = VisBhv.set_orig_stmt -let set_orig_typeinfo = VisBhv.set_orig_typeinfo -let set_orig_logic_info = VisBhv.set_orig_logic_info -let set_orig_logic_type_info = VisBhv.set_orig_logic_type_info -let set_orig_logic_var = VisBhv.set_orig_logic_var -let set_orig_kernel_function= VisBhv.set_orig_kernel_function -let set_orig_fundec = VisBhv.set_orig_fundec - -let unset_varinfo = VisBhv.unset_varinfo -let unset_compinfo = VisBhv.unset_compinfo -let unset_fieldinfo = VisBhv.unset_fieldinfo -let unset_model_info = VisBhv.unset_model_info -let unset_enuminfo = VisBhv.unset_enuminfo -let unset_enumitem = VisBhv.unset_enumitem -let unset_stmt = VisBhv.unset_stmt -let unset_typeinfo = VisBhv.unset_typeinfo -let unset_logic_info = VisBhv.unset_logic_info -let unset_logic_type_info = VisBhv.unset_logic_type_info -let unset_logic_var = VisBhv.unset_logic_var -let unset_kernel_function = VisBhv.unset_kernel_function -let unset_fundec = VisBhv.unset_fundec - -let unset_orig_varinfo = VisBhv.unset_orig_varinfo -let unset_orig_compinfo = VisBhv.unset_orig_compinfo -let unset_orig_fieldinfo = VisBhv.unset_orig_fieldinfo -let unset_orig_model_info = VisBhv.unset_model_info -let unset_orig_enuminfo = VisBhv.unset_orig_enuminfo -let unset_orig_enumitem = VisBhv.unset_orig_enumitem -let unset_orig_stmt = VisBhv.unset_orig_stmt -let unset_orig_typeinfo = VisBhv.unset_orig_typeinfo -let unset_orig_logic_info = VisBhv.unset_orig_logic_info -let unset_orig_logic_type_info = VisBhv.unset_orig_logic_type_info -let unset_orig_logic_var = VisBhv.unset_orig_logic_var -let unset_orig_kernel_function= VisBhv.unset_orig_kernel_function -let unset_orig_fundec = VisBhv.unset_orig_fundec - -let iter_visitor_varinfo = VisBhv.iter_visitor_varinfo -let iter_visitor_compinfo = VisBhv.iter_visitor_compinfo -let iter_visitor_enuminfo = VisBhv.iter_visitor_enuminfo -let iter_visitor_enumitem = VisBhv.iter_visitor_enumitem -let iter_visitor_typeinfo = VisBhv.iter_visitor_typeinfo -let iter_visitor_stmt = VisBhv.iter_visitor_stmt -let iter_visitor_logic_info= VisBhv.iter_visitor_logic_info -let iter_visitor_logic_type_info = VisBhv.iter_visitor_logic_type_info -let iter_visitor_fieldinfo = VisBhv.iter_visitor_fieldinfo -let iter_visitor_model_info = VisBhv.iter_visitor_model_info -let iter_visitor_logic_var = VisBhv.iter_visitor_logic_var -let iter_visitor_kernel_function = VisBhv.iter_visitor_kernel_function -let iter_visitor_fundec = VisBhv.iter_visitor_fundec - -let fold_visitor_varinfo = VisBhv.fold_visitor_varinfo -let fold_visitor_compinfo = VisBhv.fold_visitor_compinfo -let fold_visitor_enuminfo = VisBhv.fold_visitor_enuminfo -let fold_visitor_enumitem = VisBhv.fold_visitor_enumitem -let fold_visitor_typeinfo = VisBhv.fold_visitor_typeinfo -let fold_visitor_stmt = VisBhv.fold_visitor_stmt -let fold_visitor_logic_info = VisBhv.fold_visitor_logic_info -let fold_visitor_logic_type_info = VisBhv.fold_visitor_logic_type_info -let fold_visitor_fieldinfo = VisBhv.fold_visitor_fieldinfo -let fold_visitor_model_info = VisBhv.fold_visitor_model_info -let fold_visitor_logic_var = VisBhv.fold_visitor_logic_var -let fold_visitor_kernel_function = VisBhv.fold_visitor_kernel_function -let fold_visitor_fundec = VisBhv.fold_visitor_fundec +type visitor_behavior = Visitor_behavior.t + +let refresh_visit = Visitor_behavior.refresh +let copy_visit = Visitor_behavior.copy +let inplace_visit = Visitor_behavior.inplace + +let is_copy_behavior = Visitor_behavior.is_copy +let is_fresh_behavior = Visitor_behavior.is_fresh + +let memo_varinfo = Visitor_behavior.Memo.varinfo +let memo_compinfo = Visitor_behavior.Memo.compinfo +let memo_fieldinfo = Visitor_behavior.Memo.fieldinfo +let memo_model_info = Visitor_behavior.Memo.model_info +let memo_enuminfo = Visitor_behavior.Memo.enuminfo +let memo_enumitem = Visitor_behavior.Memo.enumitem +let memo_stmt = Visitor_behavior.Memo.stmt +let memo_typeinfo = Visitor_behavior.Memo.typeinfo +let memo_logic_info = Visitor_behavior.Memo.logic_info +let memo_logic_type_info = Visitor_behavior.Memo.logic_type_info +let memo_logic_var = Visitor_behavior.Memo.logic_var +let memo_kernel_function = Visitor_behavior.Memo.kernel_function +let memo_fundec = Visitor_behavior.Memo.fundec + +let reset_behavior_varinfo = Visitor_behavior.Reset.varinfo +let reset_behavior_compinfo = Visitor_behavior.Reset.compinfo +let reset_behavior_enuminfo = Visitor_behavior.Reset.enuminfo +let reset_behavior_enumitem = Visitor_behavior.Reset.enumitem +let reset_behavior_typeinfo = Visitor_behavior.Reset.typeinfo +let reset_behavior_logic_info = Visitor_behavior.Reset.logic_info +let reset_behavior_logic_type_info = Visitor_behavior.Reset.logic_type_info +let reset_behavior_fieldinfo = Visitor_behavior.Reset.fieldinfo +let reset_behavior_model_info = Visitor_behavior.Reset.model_info +let reset_behavior_stmt = Visitor_behavior.Reset.stmt +let reset_logic_var = Visitor_behavior.Reset.logic_var +let reset_behavior_kernel_function = Visitor_behavior.Reset.kernel_function +let reset_behavior_fundec = Visitor_behavior.Reset.fundec + +let get_varinfo = Visitor_behavior.Get.varinfo +let get_compinfo = Visitor_behavior.Get.compinfo +let get_fieldinfo = Visitor_behavior.Get.fieldinfo +let get_model_info = Visitor_behavior.Get.model_info +let get_enuminfo = Visitor_behavior.Get.enuminfo +let get_enumitem = Visitor_behavior.Get.enumitem +let get_stmt = Visitor_behavior.Get.stmt +let get_typeinfo = Visitor_behavior.Get.typeinfo +let get_logic_info = Visitor_behavior.Get.logic_info +let get_logic_type_info = Visitor_behavior.Get.logic_type_info +let get_logic_var = Visitor_behavior.Get.logic_var +let get_kernel_function = Visitor_behavior.Get.kernel_function +let get_fundec = Visitor_behavior.Get.fundec + +let get_original_varinfo = Visitor_behavior.Get_orig.varinfo +let get_original_compinfo = Visitor_behavior.Get_orig.compinfo +let get_original_fieldinfo = Visitor_behavior.Get_orig.fieldinfo +let get_original_model_info = Visitor_behavior.Get_orig.model_info +let get_original_enuminfo = Visitor_behavior.Get_orig.enuminfo +let get_original_enumitem = Visitor_behavior.Get_orig.enumitem +let get_original_stmt = Visitor_behavior.Get_orig.stmt +let get_original_typeinfo = Visitor_behavior.Get_orig.typeinfo +let get_original_logic_info = Visitor_behavior.Get_orig.logic_info +let get_original_logic_type_info = Visitor_behavior.Get_orig.logic_type_info +let get_original_logic_var = Visitor_behavior.Get_orig.logic_var +let get_original_kernel_function = Visitor_behavior.Get_orig.kernel_function +let get_original_fundec = Visitor_behavior.Get_orig.fundec + +let set_varinfo = Visitor_behavior.Set.varinfo +let set_compinfo = Visitor_behavior.Set.compinfo +let set_fieldinfo = Visitor_behavior.Set.fieldinfo +let set_model_info = Visitor_behavior.Set.model_info +let set_enuminfo = Visitor_behavior.Set.enuminfo +let set_enumitem = Visitor_behavior.Set.enumitem +let set_stmt = Visitor_behavior.Set.stmt +let set_typeinfo = Visitor_behavior.Set.typeinfo +let set_logic_info = Visitor_behavior.Set.logic_info +let set_logic_type_info = Visitor_behavior.Set.logic_type_info +let set_logic_var = Visitor_behavior.Set.logic_var +let set_kernel_function = Visitor_behavior.Set.kernel_function +let set_fundec = Visitor_behavior.Set.fundec + +let set_orig_varinfo = Visitor_behavior.Set_orig.varinfo +let set_orig_compinfo = Visitor_behavior.Set_orig.compinfo +let set_orig_fieldinfo = Visitor_behavior.Set_orig.fieldinfo +let set_orig_model_info = Visitor_behavior.Set_orig.model_info +let set_orig_enuminfo = Visitor_behavior.Set_orig.enuminfo +let set_orig_enumitem = Visitor_behavior.Set_orig.enumitem +let set_orig_stmt = Visitor_behavior.Set_orig.stmt +let set_orig_typeinfo = Visitor_behavior.Set_orig.typeinfo +let set_orig_logic_info = Visitor_behavior.Set_orig.logic_info +let set_orig_logic_type_info = Visitor_behavior.Set_orig.logic_type_info +let set_orig_logic_var = Visitor_behavior.Set_orig.logic_var +let set_orig_kernel_function= Visitor_behavior.Set_orig.kernel_function +let set_orig_fundec = Visitor_behavior.Set_orig.fundec + +let unset_varinfo = Visitor_behavior.Unset.varinfo +let unset_compinfo = Visitor_behavior.Unset.compinfo +let unset_fieldinfo = Visitor_behavior.Unset.fieldinfo +let unset_model_info = Visitor_behavior.Unset.model_info +let unset_enuminfo = Visitor_behavior.Unset.enuminfo +let unset_enumitem = Visitor_behavior.Unset.enumitem +let unset_stmt = Visitor_behavior.Unset.stmt +let unset_typeinfo = Visitor_behavior.Unset.typeinfo +let unset_logic_info = Visitor_behavior.Unset.logic_info +let unset_logic_type_info = Visitor_behavior.Unset.logic_type_info +let unset_logic_var = Visitor_behavior.Unset.logic_var +let unset_kernel_function = Visitor_behavior.Unset.kernel_function +let unset_fundec = Visitor_behavior.Unset.fundec + +let unset_orig_varinfo = Visitor_behavior.Unset_orig.varinfo +let unset_orig_compinfo = Visitor_behavior.Unset_orig.compinfo +let unset_orig_fieldinfo = Visitor_behavior.Unset_orig.fieldinfo +let unset_orig_model_info = Visitor_behavior.Unset_orig.model_info +let unset_orig_enuminfo = Visitor_behavior.Unset_orig.enuminfo +let unset_orig_enumitem = Visitor_behavior.Unset_orig.enumitem +let unset_orig_stmt = Visitor_behavior.Unset_orig.stmt +let unset_orig_typeinfo = Visitor_behavior.Unset_orig.typeinfo +let unset_orig_logic_info = Visitor_behavior.Unset_orig.logic_info +let unset_orig_logic_type_info = Visitor_behavior.Unset_orig.logic_type_info +let unset_orig_logic_var = Visitor_behavior.Unset_orig.logic_var +let unset_orig_kernel_function= Visitor_behavior.Unset_orig.kernel_function +let unset_orig_fundec = Visitor_behavior.Unset_orig.fundec + +let iter_visitor_varinfo = Visitor_behavior.Iter.varinfo +let iter_visitor_compinfo = Visitor_behavior.Iter.compinfo +let iter_visitor_enuminfo = Visitor_behavior.Iter.enuminfo +let iter_visitor_enumitem = Visitor_behavior.Iter.enumitem +let iter_visitor_typeinfo = Visitor_behavior.Iter.typeinfo +let iter_visitor_stmt = Visitor_behavior.Iter.stmt +let iter_visitor_logic_info= Visitor_behavior.Iter.logic_info +let iter_visitor_logic_type_info = Visitor_behavior.Iter.logic_type_info +let iter_visitor_fieldinfo = Visitor_behavior.Iter.fieldinfo +let iter_visitor_model_info = Visitor_behavior.Iter.model_info +let iter_visitor_logic_var = Visitor_behavior.Iter.logic_var +let iter_visitor_kernel_function = Visitor_behavior.Iter.kernel_function +let iter_visitor_fundec = Visitor_behavior.Iter.fundec + +let fold_visitor_varinfo = Visitor_behavior.Fold.varinfo +let fold_visitor_compinfo = Visitor_behavior.Fold.compinfo +let fold_visitor_enuminfo = Visitor_behavior.Fold.enuminfo +let fold_visitor_enumitem = Visitor_behavior.Fold.enumitem +let fold_visitor_typeinfo = Visitor_behavior.Fold.typeinfo +let fold_visitor_stmt = Visitor_behavior.Fold.stmt +let fold_visitor_logic_info = Visitor_behavior.Fold.logic_info +let fold_visitor_logic_type_info = Visitor_behavior.Fold.logic_type_info +let fold_visitor_fieldinfo = Visitor_behavior.Fold.fieldinfo +let fold_visitor_model_info = Visitor_behavior.Fold.model_info +let fold_visitor_logic_var = Visitor_behavior.Fold.logic_var +let fold_visitor_kernel_function = Visitor_behavior.Fold.kernel_function +let fold_visitor_fundec = Visitor_behavior.Fold.fundec (* Local Variables: diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli index 07aacfacf5a1c91a3bcbbb510fe6c5b8da632740..10aebb0a17a9d77271a68f30b1b9b08a49779bca 100644 --- a/src/kernel_services/ast_queries/cil.mli +++ b/src/kernel_services/ast_queries/cil.mli @@ -1493,12 +1493,12 @@ type visitor_behavior = Visitor_behavior.t @plugin development guide *) val inplace_visit: unit -> Visitor_behavior.t -[@@ ocaml.deprecated "Use Visitor_behavior.inplace_visit"] +[@@ ocaml.deprecated "Use Visitor_behavior.inplace"] (** In-place modification. Behavior of the original cil visitor. @plugin development guide *) val copy_visit: Project.t -> Visitor_behavior.t -[@@ ocaml.deprecated "Use Visitor_behavior.copy_visit"] +[@@ ocaml.deprecated "Use Visitor_behavior.copy"] (** Makes fresh copies of the mutable structures. - preserves sharing for varinfo. - makes fresh copy of varinfo only for declarations. Variables that are @@ -1510,7 +1510,7 @@ val copy_visit: Project.t -> Visitor_behavior.t @plugin development guide *) val refresh_visit: Project.t -> Visitor_behavior.t -[@@ ocaml.deprecated "Use Visitor_behavior.refresh_visit"] +[@@ ocaml.deprecated "Use Visitor_behavior.refresh"] (** 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 @@ -1534,367 +1534,366 @@ val is_copy_behavior: Visitor_behavior.t -> bool [@@ ocaml.deprecated "Use Visitor_behavior.is_copy"] val reset_behavior_varinfo: Visitor_behavior.t -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.reset_varinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Reset.varinfo"] (** resets the internal tables used by the given Visitor_behavior.t. 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. - @deprecated Potassium-19.0+dev. Use {!Visitor_behavior.reset_behavior_varinfo}. + @deprecated Potassium-19.0+dev. Use {!Visitor_behavior.Reset.varinfo}. @plugin development guide *) val reset_behavior_compinfo: Visitor_behavior.t -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.reset_compinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Reset.compinfo"] val reset_behavior_enuminfo: Visitor_behavior.t -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.reset_enuminfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Reset.enuminfo"] val reset_behavior_enumitem: Visitor_behavior.t -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.reset_enumitem"] +[@@ ocaml.deprecated "Use Visitor_behavior.Reset.enumitem"] val reset_behavior_typeinfo: Visitor_behavior.t -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.reset_typeinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Reset.typeinfo"] val reset_behavior_stmt: Visitor_behavior.t -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.reset_stmt"] +[@@ ocaml.deprecated "Use Visitor_behavior.Reset.stmt"] val reset_behavior_logic_info: Visitor_behavior.t -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.reset_logic_info"] +[@@ ocaml.deprecated "Use Visitor_behavior.Reset.logic_info"] val reset_behavior_logic_type_info: Visitor_behavior.t -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.reset_logic_type_info"] +[@@ ocaml.deprecated "Use Visitor_behavior.Reset.logic_type_info"] val reset_behavior_fieldinfo: Visitor_behavior.t -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.reset_fieldinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Reset.fieldinfo"] val reset_behavior_model_info: Visitor_behavior.t -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.reset_model_info"] +[@@ ocaml.deprecated "Use Visitor_behavior.Reset.model_info"] val reset_logic_var: Visitor_behavior.t -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.reset_logic_var"] +[@@ ocaml.deprecated "Use Visitor_behavior.Reset.logic_var"] val reset_behavior_kernel_function: Visitor_behavior.t -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.reset_kernel_function"] +[@@ ocaml.deprecated "Use Visitor_behavior.Reset.kernel_function"] val reset_behavior_fundec: Visitor_behavior.t -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.reset_fundec"] +[@@ ocaml.deprecated "Use Visitor_behavior.Reset.fundec"] val get_varinfo: Visitor_behavior.t -> varinfo -> varinfo -[@@ ocaml.deprecated "Use Visitor_behavior.get_varinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Get.varinfo"] (** retrieve the representative of a given varinfo in the current state of the visitor - @deprecated Potassium-19.0+dev. Use {!Visitor_behavior.get_varinfo}. + @deprecated Potassium-19.0+dev. Use {!Visitor_behavior.Get.varinfo}. @plugin development guide *) val get_compinfo: Visitor_behavior.t -> compinfo -> compinfo -[@@ ocaml.deprecated "Use Visitor_behavior.get_compinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Get.compinfo"] val get_enuminfo: Visitor_behavior.t -> enuminfo -> enuminfo -[@@ ocaml.deprecated "Use Visitor_behavior.get_enuminfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Get.enuminfo"] val get_enumitem: Visitor_behavior.t -> enumitem -> enumitem -[@@ ocaml.deprecated "Use Visitor_behavior.get_enumitem"] +[@@ ocaml.deprecated "Use Visitor_behavior.Get.enumitem"] val get_typeinfo: Visitor_behavior.t -> typeinfo -> typeinfo -[@@ ocaml.deprecated "Use Visitor_behavior.get_typeinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Get.typeinfo"] val get_stmt: Visitor_behavior.t -> stmt -> stmt -[@@ ocaml.deprecated "Use Visitor_behavior.get_stmt"] +[@@ ocaml.deprecated "Use Visitor_behavior.Get.stmt"] (** @plugin development guide *) val get_logic_info: Visitor_behavior.t -> logic_info -> logic_info -[@@ ocaml.deprecated "Use Visitor_behavior.get_logic_info"] +[@@ ocaml.deprecated "Use Visitor_behavior.Get.logic_info"] val get_logic_type_info: Visitor_behavior.t -> logic_type_info -> logic_type_info -[@@ ocaml.deprecated "Use Visitor_behavior.get_logic_type_info"] +[@@ ocaml.deprecated "Use Visitor_behavior.Get.logic_type_info"] val get_fieldinfo: Visitor_behavior.t -> fieldinfo -> fieldinfo -[@@ ocaml.deprecated "Use Visitor_behavior.get_fieldinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Get.fieldinfo"] val get_model_info: Visitor_behavior.t -> model_info -> model_info -[@@ ocaml.deprecated "Use Visitor_behavior.get_model_info"] +[@@ ocaml.deprecated "Use Visitor_behavior.Get.model_info"] val get_logic_var: Visitor_behavior.t -> logic_var -> logic_var -[@@ ocaml.deprecated "Use Visitor_behavior.get_logic_var"] +[@@ ocaml.deprecated "Use Visitor_behavior.Get.logic_var"] val get_kernel_function: Visitor_behavior.t -> kernel_function -> kernel_function -[@@ ocaml.deprecated "Use Visitor_behavior.get_kernel_function"] +[@@ ocaml.deprecated "Use Visitor_behavior.Get.kernel_function"] (** @plugin development guide *) - val get_fundec: Visitor_behavior.t -> fundec -> fundec -[@@ ocaml.deprecated "Use Visitor_behavior.get_fundec"] +[@@ ocaml.deprecated "Use Visitor_behavior.Get.fundec"] val get_original_varinfo: Visitor_behavior.t -> varinfo -> varinfo -[@@ ocaml.deprecated "Use Visitor_behavior.get_original_varinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Get_orig.varinfo"] (** retrieve the original representative of a given copy of a varinfo in the current state of the visitor. - @deprecated Potassium-19.0+dev. Use {!Visitor_behavior.get_original_varinfo}. + @deprecated Potassium-19.0+dev. Use {!Visitor_behavior.Get_orig.varinfo}. @plugin development guide *) val get_original_compinfo: Visitor_behavior.t -> compinfo -> compinfo -[@@ ocaml.deprecated "Use Visitor_behavior.get_original_compinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Get_orig.compinfo"] val get_original_enuminfo: Visitor_behavior.t -> enuminfo -> enuminfo -[@@ ocaml.deprecated "Use Visitor_behavior.get_original_enuminfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Get_orig.enuminfo"] val get_original_enumitem: Visitor_behavior.t -> enumitem -> enumitem -[@@ ocaml.deprecated "Use Visitor_behavior.get_original_enumitem"] +[@@ ocaml.deprecated "Use Visitor_behavior.Get_orig.enumitem"] val get_original_typeinfo: Visitor_behavior.t -> typeinfo -> typeinfo -[@@ ocaml.deprecated "Use Visitor_behavior.get_original_typeinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Get_orig.typeinfo"] val get_original_stmt: Visitor_behavior.t -> stmt -> stmt -[@@ ocaml.deprecated "Use Visitor_behavior.get_original_stmt"] +[@@ ocaml.deprecated "Use Visitor_behavior.Get_orig.stmt"] val get_original_logic_info: Visitor_behavior.t -> logic_info -> logic_info -[@@ ocaml.deprecated "Use Visitor_behavior.get_original_logic_info"] +[@@ ocaml.deprecated "Use Visitor_behavior.Get_orig.logic_info"] val get_original_logic_type_info: Visitor_behavior.t -> logic_type_info -> logic_type_info -[@@ ocaml.deprecated "Use Visitor_behavior.get_original_logic_type_info"] +[@@ ocaml.deprecated "Use Visitor_behavior.Get_orig.logic_type_info"] val get_original_fieldinfo: Visitor_behavior.t -> fieldinfo -> fieldinfo -[@@ ocaml.deprecated "Use Visitor_behavior.get_original_fieldinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Get_orig.fieldinfo"] val get_original_model_info: Visitor_behavior.t -> model_info -> model_info -[@@ ocaml.deprecated "Use Visitor_behavior.get_original_model_info"] +[@@ ocaml.deprecated "Use Visitor_behavior.Get_orig.model_info"] val get_original_logic_var: Visitor_behavior.t -> logic_var -> logic_var -[@@ ocaml.deprecated "Use Visitor_behavior.get_original_logic_var"] +[@@ ocaml.deprecated "Use Visitor_behavior.Get_orig.logic_var"] val get_original_kernel_function: Visitor_behavior.t -> kernel_function -> kernel_function -[@@ ocaml.deprecated "Use Visitor_behavior.get_original_kernel_function"] +[@@ ocaml.deprecated "Use Visitor_behavior.Get_orig.kernel_function"] val get_original_fundec: Visitor_behavior.t -> fundec -> fundec -[@@ ocaml.deprecated "Use Visitor_behavior.get_original_fundec"] +[@@ ocaml.deprecated "Use Visitor_behavior.Get_orig.fundec"] val set_varinfo: Visitor_behavior.t -> varinfo -> varinfo -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.set_varinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Set.varinfo"] (** 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. - @deprecated Potassium-19.0+dev. Use {!Visitor_behavior.set_varinfo}. + @deprecated Potassium-19.0+dev. Use {!Visitor_behavior.Set.varinfo}. @plugin development guide *) val set_compinfo: Visitor_behavior.t -> compinfo -> compinfo -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.set_compinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Set.compinfo"] val set_enuminfo: Visitor_behavior.t -> enuminfo -> enuminfo -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.set_enuminfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Set.enuminfo"] val set_enumitem: Visitor_behavior.t -> enumitem -> enumitem -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.set_enumitem"] +[@@ ocaml.deprecated "Use Visitor_behavior.Set.enumitem"] val set_typeinfo: Visitor_behavior.t -> typeinfo -> typeinfo -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.set_typeinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Set.typeinfo"] val set_stmt: Visitor_behavior.t -> stmt -> stmt -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.set_stmt"] +[@@ ocaml.deprecated "Use Visitor_behavior.Set.stmt"] val set_logic_info: Visitor_behavior.t -> logic_info -> logic_info -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.set_logic_info"] +[@@ ocaml.deprecated "Use Visitor_behavior.Set.logic_info"] val set_logic_type_info: Visitor_behavior.t -> logic_type_info -> logic_type_info -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.set_logic_type_info"] +[@@ ocaml.deprecated "Use Visitor_behavior.Set.logic_type_info"] val set_fieldinfo: Visitor_behavior.t -> fieldinfo -> fieldinfo -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.set_fieldinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Set.fieldinfo"] val set_model_info: Visitor_behavior.t -> model_info -> model_info -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.set_model_info"] +[@@ ocaml.deprecated "Use Visitor_behavior.Set.model_info"] val set_logic_var: Visitor_behavior.t -> logic_var -> logic_var -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.set_logic_var"] +[@@ ocaml.deprecated "Use Visitor_behavior.Set.logic_var"] val set_kernel_function: Visitor_behavior.t -> kernel_function -> kernel_function -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.set_kernel_function"] +[@@ ocaml.deprecated "Use Visitor_behavior.Set.kernel_function"] val set_fundec: Visitor_behavior.t -> fundec -> fundec -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.set_fundec"] +[@@ ocaml.deprecated "Use Visitor_behavior.Set.fundec"] val set_orig_varinfo: Visitor_behavior.t -> varinfo -> varinfo -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.set_orig_varinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Set_orig.varinfo"] (** change the reference of a given new varinfo in the current state of the visitor. Use with care - @deprecated Potassium-19.0+dev. Use {!Visitor_behavior.set_orig_varinfo}. + @deprecated Potassium-19.0+dev. Use {!Visitor_behavior.Set_orig.varinfo}. *) val set_orig_compinfo: Visitor_behavior.t -> compinfo -> compinfo -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.set_orig_compinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Set_orig.compinfo"] val set_orig_enuminfo: Visitor_behavior.t -> enuminfo -> enuminfo -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.set_orig_enuminfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Set_orig.enuminfo"] val set_orig_enumitem: Visitor_behavior.t -> enumitem -> enumitem -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.set_orig_enumitem"] +[@@ ocaml.deprecated "Use Visitor_behavior.Set_orig.enumitem"] val set_orig_typeinfo: Visitor_behavior.t -> typeinfo -> typeinfo -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.set_orig_typeinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Set_orig.typeinfo"] val set_orig_stmt: Visitor_behavior.t -> stmt -> stmt -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.set_orig_stmt"] +[@@ ocaml.deprecated "Use Visitor_behavior.Set_orig.stmt"] val set_orig_logic_info: Visitor_behavior.t -> logic_info -> logic_info -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.set_orig_logic_info"] +[@@ ocaml.deprecated "Use Visitor_behavior.Set_orig.logic_info"] val set_orig_logic_type_info: Visitor_behavior.t -> logic_type_info -> logic_type_info -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.set_orig_logic_type_info"] +[@@ ocaml.deprecated "Use Visitor_behavior.Set_orig.logic_type_info"] val set_orig_fieldinfo: Visitor_behavior.t -> fieldinfo -> fieldinfo -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.set_orig_fieldinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Set_orig.fieldinfo"] val set_orig_model_info: Visitor_behavior.t -> model_info -> model_info -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.set_orig_model_info"] +[@@ ocaml.deprecated "Use Visitor_behavior.Set_orig.model_info"] val set_orig_logic_var: Visitor_behavior.t -> logic_var -> logic_var -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.set_orig_logic_var"] -val set_orig_kernel_function: +[@@ ocaml.deprecated "Use Visitor_behavior.Set_orig.logic_var"] +val set_orig_kernel_function: Visitor_behavior.t -> kernel_function -> kernel_function -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.set_orig_kernel_function"] +[@@ ocaml.deprecated "Use Visitor_behavior.Set_orig.kernel_function"] val set_orig_fundec: Visitor_behavior.t -> fundec -> fundec -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.set_orig_fundec"] +[@@ ocaml.deprecated "Use Visitor_behavior.Set_orig.fundec"] val unset_varinfo: Visitor_behavior.t -> varinfo -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.unset_varinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Unset.varinfo"] (** 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). - @deprecated Potassium-19.0+dev. Use {!Visitor_behavior.unset_varinfo}. + @deprecated Potassium-19.0+dev. Use {!Visitor_behavior.Unset.varinfo}. @plugin development guide *) val unset_compinfo: Visitor_behavior.t -> compinfo -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.unset_compinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Unset.compinfo"] val unset_enuminfo: Visitor_behavior.t -> enuminfo -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.unset_enuminfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Unset.enuminfo"] val unset_enumitem: Visitor_behavior.t -> enumitem -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.unset_enumitem"] +[@@ ocaml.deprecated "Use Visitor_behavior.Unset.enumitem"] val unset_typeinfo: Visitor_behavior.t -> typeinfo -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.unset_typeinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Unset.typeinfo"] val unset_stmt: Visitor_behavior.t -> stmt -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.unset_stmt"] +[@@ ocaml.deprecated "Use Visitor_behavior.Unset.stmt"] val unset_logic_info: Visitor_behavior.t -> logic_info -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.unset_logic_info"] +[@@ ocaml.deprecated "Use Visitor_behavior.Unset.logic_info"] val unset_logic_type_info: Visitor_behavior.t -> logic_type_info -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.unset_logic_type_info"] +[@@ ocaml.deprecated "Use Visitor_behavior.Unset.logic_type_info"] val unset_fieldinfo: Visitor_behavior.t -> fieldinfo -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.unset_fieldinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Unset.fieldinfo"] val unset_model_info: Visitor_behavior.t -> model_info -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.unset_model_info"] +[@@ ocaml.deprecated "Use Visitor_behavior.Unset.model_info"] val unset_logic_var: Visitor_behavior.t -> logic_var -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.unset_logic_var"] +[@@ ocaml.deprecated "Use Visitor_behavior.Unset.logic_var"] val unset_kernel_function: Visitor_behavior.t -> kernel_function -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.unset_kernel_function"] +[@@ ocaml.deprecated "Use Visitor_behavior.Unset.kernel_function"] val unset_fundec: Visitor_behavior.t -> fundec -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.unset_fundec"] +[@@ ocaml.deprecated "Use Visitor_behavior.Unset.fundec"] val unset_orig_varinfo: Visitor_behavior.t -> varinfo -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.unset_orig_varinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Unset_orig.varinfo"] (** remove the entry associated with the given new varinfo in the current state of the visitor. Use with care - @deprecated Potassium-19.0+dev. Use {!Visitor_behavior.unset_orig_varinfo}. + @deprecated Potassium-19.0+dev. Use {!Visitor_behavior.Unset_orig.varinfo}. *) val unset_orig_compinfo: Visitor_behavior.t -> compinfo -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.unset_orig_compinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Unset_orig.compinfo"] val unset_orig_enuminfo: Visitor_behavior.t -> enuminfo -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.unset_orig_enuminfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Unset_orig.enuminfo"] val unset_orig_enumitem: Visitor_behavior.t -> enumitem -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.unset_orig_enumitem"] +[@@ ocaml.deprecated "Use Visitor_behavior.Unset_orig.enumitem"] val unset_orig_typeinfo: Visitor_behavior.t -> typeinfo -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.unset_orig_typeinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Unset_orig.typeinfo"] val unset_orig_stmt: Visitor_behavior.t -> stmt -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.unset_orig_stmt"] +[@@ ocaml.deprecated "Use Visitor_behavior.Unset_orig.stmt"] val unset_orig_logic_info: Visitor_behavior.t -> logic_info -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.unset_orig_logic_info"] +[@@ ocaml.deprecated "Use Visitor_behavior.Unset_orig.logic_info"] val unset_orig_logic_type_info: Visitor_behavior.t -> logic_type_info -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.unset_orig_logic_type_info"] +[@@ ocaml.deprecated "Use Visitor_behavior.Unset_orig.logic_type_info"] val unset_orig_fieldinfo: Visitor_behavior.t -> fieldinfo -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.unset_orig_fieldinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Unset_orig.fieldinfo"] val unset_orig_model_info: Visitor_behavior.t -> model_info -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.unset_orig_model_info"] +[@@ ocaml.deprecated "Use Visitor_behavior.Unset_orig.model_info"] val unset_orig_logic_var: Visitor_behavior.t -> logic_var -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.unset_orig_logic_var"] +[@@ ocaml.deprecated "Use Visitor_behavior.Unset_orig.logic_var"] val unset_orig_kernel_function: Visitor_behavior.t -> kernel_function -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.unset_orig_kernel_function"] +[@@ ocaml.deprecated "Use Visitor_behavior.Unset_orig.kernel_function"] val unset_orig_fundec: Visitor_behavior.t -> fundec -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.unset_orig_fundec"] +[@@ ocaml.deprecated "Use Visitor_behavior.Unset_orig.fundec"] val memo_varinfo: Visitor_behavior.t -> varinfo -> varinfo -[@@ ocaml.deprecated "Use Visitor_behavior.memo_varinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Memo.varinfo"] (** finds a binding in new project for the given varinfo, creating one - if it does not already exists. - @deprecated Potassium-19.0+dev. Use {!Visitor_behavior.memo_varinfo}. + if it does not already exists. + @deprecated Potassium-19.0+dev. Use {!Visitor_behavior.Memo.varinfo}. *) val memo_compinfo: Visitor_behavior.t -> compinfo -> compinfo -[@@ ocaml.deprecated "Use Visitor_behavior.memo_compinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Memo.compinfo"] val memo_enuminfo: Visitor_behavior.t -> enuminfo -> enuminfo -[@@ ocaml.deprecated "Use Visitor_behavior.memo_enuminfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Memo.enuminfo"] val memo_enumitem: Visitor_behavior.t -> enumitem -> enumitem -[@@ ocaml.deprecated "Use Visitor_behavior.memo_enumitem"] +[@@ ocaml.deprecated "Use Visitor_behavior.Memo.enumitem"] val memo_typeinfo: Visitor_behavior.t -> typeinfo -> typeinfo -[@@ ocaml.deprecated "Use Visitor_behavior.memo_typeinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Memo.typeinfo"] val memo_stmt: Visitor_behavior.t -> stmt -> stmt -[@@ ocaml.deprecated "Use Visitor_behavior.memo_stmt"] +[@@ ocaml.deprecated "Use Visitor_behavior.Memo.stmt"] val memo_logic_info: Visitor_behavior.t -> logic_info -> logic_info -[@@ ocaml.deprecated "Use Visitor_behavior.memo_logic_info"] +[@@ ocaml.deprecated "Use Visitor_behavior.Memo.logic_info"] val memo_logic_type_info: Visitor_behavior.t -> logic_type_info -> logic_type_info -[@@ ocaml.deprecated "Use Visitor_behavior.memo_logic_type_info"] +[@@ ocaml.deprecated "Use Visitor_behavior.Memo.logic_type_info"] val memo_fieldinfo: Visitor_behavior.t -> fieldinfo -> fieldinfo -[@@ ocaml.deprecated "Use Visitor_behavior.memo_fieldinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Memo.fieldinfo"] val memo_model_info: Visitor_behavior.t -> model_info -> model_info -[@@ ocaml.deprecated "Use Visitor_behavior.memo_model_info"] +[@@ ocaml.deprecated "Use Visitor_behavior.Memo.model_info"] val memo_logic_var: Visitor_behavior.t -> logic_var -> logic_var -[@@ ocaml.deprecated "Use Visitor_behavior.memo_logic_var"] +[@@ ocaml.deprecated "Use Visitor_behavior.Memo.logic_var"] val memo_kernel_function: Visitor_behavior.t -> kernel_function -> kernel_function -[@@ ocaml.deprecated "Use Visitor_behavior.memo_kernel_function"] +[@@ ocaml.deprecated "Use Visitor_behavior.Memo.kernel_function"] val memo_fundec: Visitor_behavior.t -> fundec -> fundec -[@@ ocaml.deprecated "Use Visitor_behavior.memo_fundec"] +[@@ ocaml.deprecated "Use Visitor_behavior.Memo.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 - @deprecated Potassium-19.0+dev. Use {!Visitor_behavior.iter_visitor_varinfo}. + @deprecated Potassium-19.0+dev. Use {!Visitor_behavior.Iter.varinfo}. *) val iter_visitor_varinfo: Visitor_behavior.t -> (varinfo -> varinfo -> unit) -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.iter_visitor_varinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Iter.varinfo"] val iter_visitor_compinfo: Visitor_behavior.t -> (compinfo -> compinfo -> unit) -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.iter_visitor_compinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Iter.compinfo"] val iter_visitor_enuminfo: Visitor_behavior.t -> (enuminfo -> enuminfo -> unit) -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.iter_visitor_enuminfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Iter.enuminfo"] val iter_visitor_enumitem: Visitor_behavior.t -> (enumitem -> enumitem -> unit) -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.iter_visitor_enumitem"] +[@@ ocaml.deprecated "Use Visitor_behavior.Iter.enumitem"] val iter_visitor_typeinfo: Visitor_behavior.t -> (typeinfo -> typeinfo -> unit) -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.iter_visitor_typeinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Iter.typeinfo"] val iter_visitor_stmt: Visitor_behavior.t -> (stmt -> stmt -> unit) -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.iter_visitor_stmt"] +[@@ ocaml.deprecated "Use Visitor_behavior.Iter.stmt"] val iter_visitor_logic_info: Visitor_behavior.t -> (logic_info -> logic_info -> unit) -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.iter_visitor_logic_info"] +[@@ ocaml.deprecated "Use Visitor_behavior.Iter.logic_info"] val iter_visitor_logic_type_info: Visitor_behavior.t -> (logic_type_info -> logic_type_info -> unit) -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.iter_visitor_logic_type_info"] +[@@ ocaml.deprecated "Use Visitor_behavior.Iter.logic_type_info"] val iter_visitor_fieldinfo: Visitor_behavior.t -> (fieldinfo -> fieldinfo -> unit) -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.iter_visitor_fieldinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Iter.fieldinfo"] val iter_visitor_model_info: Visitor_behavior.t -> (model_info -> model_info -> unit) -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.iter_visitor_model_info"] +[@@ ocaml.deprecated "Use Visitor_behavior.Iter.model_info"] val iter_visitor_logic_var: Visitor_behavior.t -> (logic_var -> logic_var -> unit) -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.iter_visitor_logic_var"] +[@@ ocaml.deprecated "Use Visitor_behavior.Iter.logic_var"] val iter_visitor_kernel_function: Visitor_behavior.t -> (kernel_function -> kernel_function -> unit) -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.iter_visitor_kernel_function"] +[@@ ocaml.deprecated "Use Visitor_behavior.Iter.kernel_function"] val iter_visitor_fundec: Visitor_behavior.t -> (fundec -> fundec -> unit) -> unit -[@@ ocaml.deprecated "Use Visitor_behavior.iter_visitor_fundec"] +[@@ ocaml.deprecated "Use Visitor_behavior.Iter.fundec"] (** [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 - @deprecated Potassium-19.0+dev. Use {!Visitor_behavior.fold_visitor_varinfo}. + @deprecated Potassium-19.0+dev. Use {!Visitor_behavior.Fold.varinfo}. *) val fold_visitor_varinfo: Visitor_behavior.t -> (varinfo -> varinfo -> 'a -> 'a) -> 'a -> 'a -[@@ ocaml.deprecated "Use Visitor_behavior.fold_visitor_varinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Fold.varinfo"] val fold_visitor_compinfo: Visitor_behavior.t -> (compinfo -> compinfo -> 'a -> 'a) -> 'a -> 'a -[@@ ocaml.deprecated "Use Visitor_behavior.fold_visitor_compinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Fold.compinfo"] val fold_visitor_enuminfo: Visitor_behavior.t -> (enuminfo -> enuminfo -> 'a -> 'a) -> 'a -> 'a -[@@ ocaml.deprecated "Use Visitor_behavior.fold_visitor_enuminfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Fold.enuminfo"] val fold_visitor_enumitem: Visitor_behavior.t -> (enumitem -> enumitem -> 'a -> 'a) -> 'a -> 'a -[@@ ocaml.deprecated "Use Visitor_behavior.fold_visitor_enumitem"] +[@@ ocaml.deprecated "Use Visitor_behavior.Fold.enumitem"] val fold_visitor_typeinfo: Visitor_behavior.t -> (typeinfo -> typeinfo -> 'a -> 'a) -> 'a -> 'a -[@@ ocaml.deprecated "Use Visitor_behavior.fold_visitor_typeinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Fold.typeinfo"] val fold_visitor_stmt: Visitor_behavior.t -> (stmt -> stmt -> 'a -> 'a) -> 'a -> 'a -[@@ ocaml.deprecated "Use Visitor_behavior.fold_visitor_stmt"] +[@@ ocaml.deprecated "Use Visitor_behavior.Fold.stmt"] val fold_visitor_logic_info: Visitor_behavior.t -> (logic_info -> logic_info -> 'a -> 'a) -> 'a -> 'a -[@@ ocaml.deprecated "Use Visitor_behavior.fold_visitor_logic_info"] +[@@ ocaml.deprecated "Use Visitor_behavior.Fold.logic_info"] val fold_visitor_logic_type_info: Visitor_behavior.t -> (logic_type_info -> logic_type_info -> 'a -> 'a) -> 'a -> 'a -[@@ ocaml.deprecated "Use Visitor_behavior.fold_visitor_logic_type_info"] +[@@ ocaml.deprecated "Use Visitor_behavior.Fold.logic_type_info"] val fold_visitor_fieldinfo: Visitor_behavior.t -> (fieldinfo -> fieldinfo -> 'a -> 'a) -> 'a -> 'a -[@@ ocaml.deprecated "Use Visitor_behavior.fold_visitor_fieldinfo"] +[@@ ocaml.deprecated "Use Visitor_behavior.Fold.fieldinfo"] val fold_visitor_model_info: Visitor_behavior.t -> (model_info -> model_info -> 'a -> 'a) -> 'a -> 'a -[@@ ocaml.deprecated "Use Visitor_behavior.fold_visitor_model_info"] +[@@ ocaml.deprecated "Use Visitor_behavior.Fold.model_info"] val fold_visitor_logic_var: Visitor_behavior.t -> (logic_var -> logic_var -> 'a -> 'a) -> 'a -> 'a -[@@ ocaml.deprecated "Use Visitor_behavior.fold_visitor_logic_var"] +[@@ ocaml.deprecated "Use Visitor_behavior.Fold.logic_var"] val fold_visitor_kernel_function: Visitor_behavior.t -> (kernel_function -> kernel_function -> 'a -> 'a) -> 'a -> 'a -[@@ ocaml.deprecated "Use Visitor_behavior.fold_visitor_kernel_function"] +[@@ ocaml.deprecated "Use Visitor_behavior.Fold.kernel_function"] val fold_visitor_fundec: Visitor_behavior.t -> (fundec -> fundec -> 'a -> 'a) -> 'a -> 'a -[@@ ocaml.deprecated "Use Visitor_behavior.fold_visitor_fundec"] +[@@ ocaml.deprecated "Use Visitor_behavior.Fold.fundec"] (** {3 Visitor class} *) diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml index 968ecbe40a8233b7e5707c58228efafc9f17e042..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 (Visitor_behavior.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 b606c8acfb899d4f24822581bd485444a9824c09..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 (Visitor_behavior.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 - Visitor_behavior.set_varinfo self#behavior v v'; - Visitor_behavior.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' -> - Visitor_behavior.set_logic_var self#behavior lv lv'; - Visitor_behavior.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 - Visitor_behavior.set_varinfo self#behavior var var'; - Visitor_behavior.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' -> - Visitor_behavior.set_logic_var self#behavior lv lv'; - Visitor_behavior.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,7 @@ end = struct method! vcode_annot v = Extlib.may Cil.CurrentLoc.set (Cil_datatype.Code_annotation.loc v); let stmt = - Visitor_behavior.get_original_stmt + Visitor_behavior.Get_orig.stmt self#behavior (Extlib.the self#current_stmt) in debug "[annotation] stmt %d : %a @." @@ -517,14 +517,14 @@ end = struct Cil.ChangeDoChildrenPost (b, optim) method private change_sid s = - let orig = Visitor_behavior.get_original_stmt self#behavior s in - assert (Visitor_behavior.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_const.Sid.next (); - Visitor_behavior.set_stmt self#behavior orig s; - Visitor_behavior.set_orig_stmt self#behavior s orig; + 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 @@ -540,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 = Visitor_behavior.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. *) @@ -562,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' = Visitor_behavior.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) @@ -585,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 = Visitor_behavior.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 = @@ -613,7 +613,7 @@ end = struct self#change_sid s'; (match s'.skind with | If (cond,bthen,belse,loc) -> - let s_orig = Visitor_behavior.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 @@ -704,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. *) - Visitor_behavior.reset_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 @@ -823,14 +823,14 @@ end = struct new_var.vtype <- mytype; List.iter2 (fun x y -> - Visitor_behavior.set_varinfo self#behavior x y; - Visitor_behavior.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 - Visitor_behavior.set_logic_var self#behavior lv lv'; - Visitor_behavior.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 *) @@ -857,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 (Visitor_behavior.get_varinfo self#behavior orig_var) == orig_var then - Visitor_behavior.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. *) - 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; + 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 @@ -903,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. *) - 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; + 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 49f61fa5d2178686cbc38819beccbb4646854bcd..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 (Visitor_behavior.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 9f3e0dee81e433d1f619bdde321e542393f29b47..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 = Visitor_behavior.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 @@ -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 = Visitor_behavior.get_kernel_function self#behavior kf in + let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in Queue.add (fun () -> List.iter @@ -178,7 +178,7 @@ object(self) else b in let res = self#vbehavior b' in - let new_kf = Visitor_behavior.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 = Visitor_behavior.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 = Visitor_behavior.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 = Visitor_behavior.memo_kernel_function self#behavior kf in + 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 = Visitor_behavior.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,7 +644,7 @@ object(self) v.vname Project.pretty (Project.current ()) in - let new_kf = Visitor_behavior.memo_kernel_function self#behavior kf in + 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; @@ -689,7 +689,7 @@ object(self) | GFunDecl(_,v,l) -> (match self#current_kf with | Some kf -> - let new_kf = Visitor_behavior.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 = Visitor_behavior.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 @@ -837,13 +837,13 @@ class generic_frama_c_visitor bhv = internal_generic_frama_c_visitor current_fundec queue current_kf bhv class frama_c_copy prj = - generic_frama_c_visitor (Visitor_behavior.copy_visit prj) + generic_frama_c_visitor (Visitor_behavior.copy prj) class frama_c_refresh prj = - generic_frama_c_visitor (Visitor_behavior.refresh_visit prj) + generic_frama_c_visitor (Visitor_behavior.refresh prj) class frama_c_inplace = - generic_frama_c_visitor (Visitor_behavior.inplace_visit()) + generic_frama_c_visitor (Visitor_behavior.inplace()) let visitFramacFileCopy vis f = visitCilFileCopy (vis:>cilVisitor) f @@ -857,7 +857,7 @@ let visitFramacGlobal vis g = vis#fill_global_tables; g' let visitFramacFunction vis f = - let orig_var = Visitor_behavior.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 @@ -872,7 +872,7 @@ let visitFramacKf vis kf = | None -> kf | Some prj -> let vi = Kernel_function.get_vi kf in - let vi' = Visitor_behavior.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_behavior.ml b/src/kernel_services/visitors/visitor_behavior.ml index 50587caf5b235b75e2e6a3f624ade98b8fec2aed..9bff52e7fb21295bd5ae4a623297cd35e781088a 100644 --- a/src/kernel_services/visitors/visitor_behavior.ml +++ b/src/kernel_services/visitors/visitor_behavior.ml @@ -197,7 +197,7 @@ let alphabetabeta _ x = x let unitunit: unit -> unit = id let alphaunit _ = () -let inplace_visit () = +let inplace () = { cfile = id; get_compinfo = id; get_fieldinfo = id; @@ -915,8 +915,8 @@ let copy_visit_gen fresh prj = Cil_datatype.Varinfo.Hashtbl.fold f fundecs i); } -let copy_visit = copy_visit_gen false -let refresh_visit = copy_visit_gen true +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 @@ -933,142 +933,214 @@ let cblock b = b.cblock let cinitinfo b = b.cinitinfo let cfile b = b.cfile -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 +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 -let reset_varinfo b = b.reset_behavior_varinfo () -let reset_compinfo b = b.reset_behavior_compinfo () -let reset_enuminfo b = b.reset_behavior_enuminfo () -let reset_enumitem b = b.reset_behavior_enumitem () -let reset_typeinfo b = b.reset_behavior_typeinfo () -let reset_logic_info b = b.reset_behavior_logic_info () -let reset_logic_type_info b = b.reset_behavior_logic_type_info () -let reset_fieldinfo b = b.reset_behavior_fieldinfo () -let reset_model_info b = b.reset_behavior_model_info () -let reset_stmt b = b.reset_behavior_stmt () -let reset_logic_var b = b.reset_logic_var () -let reset_kernel_function b = b.reset_behavior_kernel_function () -let reset_fundec b = b.reset_behavior_fundec () +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 -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 +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 -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 +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 -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 +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 -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 +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 -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 + 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 -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 +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 -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 +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 -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 +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 index a59a2658017fdde6e5a619ae069a15bc1654f550..f448e0a69c9840d598a1f8242925b8476507ab52 100644 --- a/src/kernel_services/visitors/visitor_behavior.mli +++ b/src/kernel_services/visitors/visitor_behavior.mli @@ -22,6 +22,10 @@ (* *) (**************************************************************************) +(** Operations on visitor behaviors. + @since Potassium-19.0+dev. +*) + open Cil_types type t @@ -30,11 +34,11 @@ type t Use one of the two values below in your classes. @plugin development guide *) -val inplace_visit: unit -> t +val inplace: unit -> t (** In-place modification. Behavior of the original cil visitor. @plugin development guide *) -val copy_visit: Project.t -> t +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 @@ -44,7 +48,7 @@ val copy_visit: Project.t -> t globals in the function's body. @plugin development guide *) -val refresh_visit: Project.t -> t +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 @@ -61,226 +65,255 @@ val is_copy: t -> bool val get_project: t -> Project.t option -val reset_varinfo: t -> unit -(** resets the internal tables used by the given t. 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. +(** 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 -val reset_compinfo: t -> unit -val reset_enuminfo: t -> unit -val reset_enumitem: t -> unit -val reset_typeinfo: t -> unit -val reset_stmt: t -> unit -val reset_logic_info: t -> unit -val reset_logic_type_info: t -> unit -val reset_fieldinfo: t -> unit -val reset_model_info: t -> unit -val reset_logic_var: t -> unit -val reset_kernel_function: t -> unit -val reset_fundec: t -> unit - -val get_varinfo: t -> varinfo -> varinfo -(** retrieve the representative of a given varinfo in the current - state of the visitor +(** 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. -val get_compinfo: t -> compinfo -> compinfo -val get_enuminfo: t -> enuminfo -> enuminfo -val get_enumitem: t -> enumitem -> enumitem -val get_typeinfo: t -> typeinfo -> typeinfo -val get_stmt: t -> stmt -> stmt -(** @plugin development guide *) - -val get_logic_info: t -> logic_info -> logic_info -val get_logic_type_info: t -> logic_type_info -> logic_type_info -val get_fieldinfo: t -> fieldinfo -> fieldinfo -val get_model_info: t -> model_info -> model_info -val get_logic_var: t -> logic_var -> logic_var -val get_kernel_function: t -> kernel_function -> kernel_function -(** @plugin development guide *) - -val get_fundec: t -> fundec -> fundec - -val get_original_varinfo: t -> varinfo -> varinfo -(** retrieve the original representative of a given copy of a varinfo - in the current 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. -val get_original_compinfo: t -> compinfo -> compinfo -val get_original_enuminfo: t -> enuminfo -> enuminfo -val get_original_enumitem: t -> enumitem -> enumitem -val get_original_typeinfo: t -> typeinfo -> typeinfo -val get_original_stmt: t -> stmt -> stmt -val get_original_logic_info: t -> logic_info -> logic_info -val get_original_logic_type_info: - t -> logic_type_info -> logic_type_info -val get_original_fieldinfo: t -> fieldinfo -> fieldinfo -val get_original_model_info: t -> model_info -> model_info -val get_original_logic_var: t -> logic_var -> logic_var -val get_original_kernel_function: - t -> kernel_function -> kernel_function -val get_original_fundec: t -> fundec -> fundec - -val set_varinfo: t -> 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. + [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 *) -val set_compinfo: t -> compinfo -> compinfo -> unit -val set_enuminfo: t -> enuminfo -> enuminfo -> unit -val set_enumitem: t -> enumitem -> enumitem -> unit -val set_typeinfo: t -> typeinfo -> typeinfo -> unit -val set_stmt: t -> stmt -> stmt -> unit -val set_logic_info: t -> logic_info -> logic_info -> unit -val set_logic_type_info: - t -> logic_type_info -> logic_type_info -> unit -val set_fieldinfo: t -> fieldinfo -> fieldinfo -> unit -val set_model_info: t -> model_info -> model_info -> unit -val set_logic_var: t -> logic_var -> logic_var -> unit -val set_kernel_function: - t -> kernel_function -> kernel_function -> unit -val set_fundec: t -> fundec -> fundec -> unit - -val set_orig_varinfo: t -> 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: t -> compinfo -> compinfo -> unit -val set_orig_enuminfo: t -> enuminfo -> enuminfo -> unit -val set_orig_enumitem: t -> enumitem -> enumitem -> unit -val set_orig_typeinfo: t -> typeinfo -> typeinfo -> unit -val set_orig_stmt: t -> stmt -> stmt -> unit -val set_orig_logic_info: t -> logic_info -> logic_info -> unit -val set_orig_logic_type_info: - t -> logic_type_info -> logic_type_info -> unit -val set_orig_fieldinfo: t -> fieldinfo -> fieldinfo -> unit -val set_orig_model_info: t -> model_info -> model_info -> unit -val set_orig_logic_var: t -> logic_var -> logic_var -> unit -val set_orig_kernel_function: - t -> kernel_function -> kernel_function -> unit -val set_orig_fundec: t -> fundec -> fundec -> unit - -val unset_varinfo: t -> 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). +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 *) -val unset_compinfo: t -> compinfo -> unit -val unset_enuminfo: t -> enuminfo -> unit -val unset_enumitem: t -> enumitem -> unit -val unset_typeinfo: t -> typeinfo -> unit -val unset_stmt: t -> stmt -> unit -val unset_logic_info: t -> logic_info -> unit -val unset_logic_type_info: t -> logic_type_info -> unit -val unset_fieldinfo: t -> fieldinfo -> unit -val unset_model_info: t -> model_info -> unit -val unset_logic_var: t -> logic_var -> unit -val unset_kernel_function: t -> kernel_function -> unit -val unset_fundec: t -> fundec -> unit - -val unset_orig_varinfo: t -> varinfo -> unit -(** remove the entry associated with the given new varinfo in the current - state of the visitor. Use with care +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 *) -val unset_orig_compinfo: t -> compinfo -> unit -val unset_orig_enuminfo: t -> enuminfo -> unit -val unset_orig_enumitem: t -> enumitem -> unit -val unset_orig_typeinfo: t -> typeinfo -> unit -val unset_orig_stmt: t -> stmt -> unit -val unset_orig_logic_info: t -> logic_info -> unit -val unset_orig_logic_type_info: t -> logic_type_info -> unit -val unset_orig_fieldinfo: t -> fieldinfo -> unit -val unset_orig_model_info: t -> model_info -> unit -val unset_orig_logic_var: t -> logic_var -> unit -val unset_orig_kernel_function: t -> kernel_function -> unit -val unset_orig_fundec: t -> fundec -> unit - -val memo_varinfo: t -> varinfo -> varinfo -(** finds a binding in new project for the given varinfo, creating one - if it does not already exists. *) -val memo_compinfo: t -> compinfo -> compinfo -val memo_enuminfo: t -> enuminfo -> enuminfo -val memo_enumitem: t -> enumitem -> enumitem -val memo_typeinfo: t -> typeinfo -> typeinfo -val memo_stmt: t -> stmt -> stmt -val memo_logic_info: t -> logic_info -> logic_info -val memo_logic_type_info: t -> logic_type_info -> logic_type_info -val memo_fieldinfo: t -> fieldinfo -> fieldinfo -val memo_model_info: t -> model_info -> model_info -val memo_logic_var: t -> logic_var -> logic_var -val memo_kernel_function: - t -> kernel_function -> kernel_function -val memo_fundec: t -> 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. +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 *) -val iter_visitor_varinfo: - t -> (varinfo -> varinfo -> unit) -> unit -val iter_visitor_compinfo: - t -> (compinfo -> compinfo -> unit) -> unit -val iter_visitor_enuminfo: - t -> (enuminfo -> enuminfo -> unit) -> unit -val iter_visitor_enumitem: - t -> (enumitem -> enumitem -> unit) -> unit -val iter_visitor_typeinfo: - t -> (typeinfo -> typeinfo -> unit) -> unit -val iter_visitor_stmt: - t -> (stmt -> stmt -> unit) -> unit -val iter_visitor_logic_info: - t -> (logic_info -> logic_info -> unit) -> unit -val iter_visitor_logic_type_info: - t -> (logic_type_info -> logic_type_info -> unit) -> unit -val iter_visitor_fieldinfo: - t -> (fieldinfo -> fieldinfo -> unit) -> unit -val iter_visitor_model_info: - t -> (model_info -> model_info -> unit) -> unit -val iter_visitor_logic_var: - t -> (logic_var -> logic_var -> unit) -> unit -val iter_visitor_kernel_function: - t -> (kernel_function -> kernel_function -> unit) -> unit -val iter_visitor_fundec: - t -> (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. +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 *) -val fold_visitor_varinfo: - t -> (varinfo -> varinfo -> 'a -> 'a) -> 'a -> 'a -val fold_visitor_compinfo: - t -> (compinfo -> compinfo -> 'a -> 'a) -> 'a -> 'a -val fold_visitor_enuminfo: - t -> (enuminfo -> enuminfo -> 'a -> 'a) -> 'a -> 'a -val fold_visitor_enumitem: - t -> (enumitem -> enumitem -> 'a -> 'a) -> 'a -> 'a -val fold_visitor_typeinfo: - t -> (typeinfo -> typeinfo -> 'a -> 'a) -> 'a -> 'a -val fold_visitor_stmt: - t -> (stmt -> stmt -> 'a -> 'a) -> 'a -> 'a -val fold_visitor_logic_info: - t -> (logic_info -> logic_info -> 'a -> 'a) -> 'a -> 'a -val fold_visitor_logic_type_info: - t -> - (logic_type_info -> logic_type_info -> 'a -> 'a) -> 'a -> 'a -val fold_visitor_fieldinfo: - t -> (fieldinfo -> fieldinfo -> 'a -> 'a) -> 'a -> 'a -val fold_visitor_model_info: - t -> (model_info -> model_info -> 'a -> 'a) -> 'a -> 'a -val fold_visitor_logic_var: - t -> (logic_var -> logic_var -> 'a -> 'a) -> 'a -> 'a -val fold_visitor_kernel_function: - t -> - (kernel_function -> kernel_function -> 'a -> 'a) -> 'a -> 'a -val fold_visitor_fundec: - t -> (fundec -> fundec -> 'a -> 'a) -> 'a -> 'a +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 diff --git a/src/plugins/constant_propagation/api.ml b/src/plugins/constant_propagation/api.ml index 30a1c050aeb4edf1ff3dd5f14c53db9f86ce048e..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 = Visitor_behavior.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 446ce77c734b8c164ca797dab7b4f97ca1f457a2..2428d248fd935bbd304d08b1ff0d3a298e7753da 100644 --- a/src/plugins/scope/datascope.ml +++ b/src/plugins/scope/datascope.ml @@ -571,7 +571,7 @@ class check_annot_visitor = object(self) method! vcode_annot annot = let kf = Extlib.the self#current_kf in let stmt = - Visitor_behavior.get_original_stmt + Visitor_behavior.Get_orig.stmt self#behavior (Extlib.the self#current_stmt) in begin match annot.annot_content with diff --git a/src/plugins/sparecode/globs.ml b/src/plugins/sparecode/globs.ml index 8e32c76c2bf714a1700e9b4c8217c42cfed91e9b..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 (Visitor_behavior.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 0ac548e41ec3b09816b66e4311a7fa5a630f978e..8a01575729702dc47de5c17c51f41cf9f03c8f4f 100644 --- a/src/plugins/wp/normAtLabels.ml +++ b/src/plugins/wp/normAtLabels.ml @@ -34,7 +34,7 @@ type label_mapping = Cil_types.logic_label -> Clabels.c_label class norm_at (mapping : label_mapping) = object(self) inherit Visitor.generic_frama_c_visitor - (Visitor_behavior.copy_visit (Project.current ())) + (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 b1b43a481cf376281d6a3b5ed4347ca13d4ee18a..b46478f7925e914d25506a3200d3d9e87b55885f 100644 --- a/tests/misc/bug_0209.ml +++ b/tests/misc/bug_0209.ml @@ -4,7 +4,7 @@ let main () = ignore (File.create_project_from_visitor "foo" (fun p -> - new Visitor.generic_frama_c_visitor (Visitor_behavior.copy_visit 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/property_test.ml b/tests/spec/property_test.ml index 9659559edb133082b6d41fabe058511fc488ad3e..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 = Visitor_behavior.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 5b76e99370d507ebbfae0ad4abdaa09bc6e06855..9a82d0fd6b4635681d12e70869a6769a7fa6283e 100644 --- a/tests/syntax/Refresh_visitor.ml +++ b/tests/syntax/Refresh_visitor.ml @@ -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 756704f38e840192c258550776e60aaf722b902c..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 = Visitor_behavior.get_original_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 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 9198cdf670cb5b5eab7a2bc29c6bd4ad2872fcf2..0938b72d74627597f86fd7fe7c6070c363e36bac 100644 --- a/tests/syntax/transient_block.ml +++ b/tests/syntax/transient_block.ml @@ -9,7 +9,7 @@ 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 = Visitor_behavior.get_fundec + 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; @@ -32,7 +32,7 @@ class vis prj = object(self) with Log.AbortFatal _ -> Kernel.feedback "transient_block fatal error on %a as expected" Printer.pp_instr instr; - let f = Visitor_behavior.get_fundec + let f = Visitor_behavior.Get.fundec self#behavior (Extlib.the self#current_func) in let y = Extlib.the my_var in f.slocals <-