From 246c9cc5ecd7533936f354826d113f3bbb70df97 Mon Sep 17 00:00:00 2001 From: Allan Blanchard <allan.blanchard@inria.fr> Date: Wed, 27 Feb 2019 09:45:07 +0100 Subject: [PATCH] [Kernel] Replaces deprecated function calls related to new Visitor_behavior module --- src/kernel_internals/typing/cabs2cil.ml | 6 +- src/kernel_internals/typing/cfg.ml | 4 +- src/kernel_internals/typing/unroll_loops.ml | 6 +- src/kernel_services/analysis/exn_flow.ml | 12 ++-- src/kernel_services/ast_queries/file.ml | 2 +- .../ast_queries/logic_utils.ml | 2 +- .../ast_transformations/filter.ml | 69 ++++++++++--------- .../ast_transformations/inline.ml | 2 +- src/kernel_services/visitors/visitor.ml | 43 ++++++------ src/kernel_services/visitors/visitor.mli | 2 +- 10 files changed, 79 insertions(+), 69 deletions(-) diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index cd3d07b4f50..6a230a5b505 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -1222,7 +1222,9 @@ let createCompInfo (iss: bool) (n: string) ~(norig: string) : compinfo * bool = H.find compInfoNameEnv key, false (* Only if not already in *) with Not_found -> begin (* Create a compinfo. This will have "cdefined" false. *) - let res = mkCompInfo iss n ~norig (fun _ ->[]) (fc_stdlib_attribute []) in + let res = + Cil_const.mkCompInfo iss n ~norig (fun _ ->[]) (fc_stdlib_attribute []) + in H.add compInfoNameEnv key res; res, true end @@ -9995,7 +9997,7 @@ and doStatement local_env (s : A.statement) : chunk = let copy_spec (old_f,new_f) formals_map spec = let obj = object - inherit Cil.genericCilVisitor (Cil.refresh_visit (Project.current())) + inherit Cil.genericCilVisitor (Visitor_behavior.refresh_visit (Project.current())) method! vlogic_var_use lv = match lv.lv_origin with | None -> DoChildren diff --git a/src/kernel_internals/typing/cfg.ml b/src/kernel_internals/typing/cfg.ml index 2d52020ae40..21e648adf5c 100644 --- a/src/kernel_internals/typing/cfg.ml +++ b/src/kernel_internals/typing/cfg.ml @@ -127,7 +127,7 @@ let make_break_stmt loc env next = let rec cfgFun (fd : fundec) = nodeList := []; cfgBlock (init_env fd.sbody) fd.sbody None None None; - fd.smaxstmtid <- Some(Cil.Sid.next ()); + fd.smaxstmtid <- Some(Cil_const.Sid.next ()); fd.sallstmts <- List.rev !nodeList; nodeList := [] @@ -161,7 +161,7 @@ and cfgBlock env (blk: block) next break cont = (* Fill in the CFG info for a stmt Meaning of next, break, cont should be clear from earlier comment *) and cfgStmt env (s: stmt) next break cont = - if s.sid = -1 then s.sid <- Cil.Sid.next (); + if s.sid = -1 then s.sid <- Cil_const.Sid.next (); nodeList := s :: !nodeList; if s.succs <> [] then Kernel.fatal diff --git a/src/kernel_internals/typing/unroll_loops.ml b/src/kernel_internals/typing/unroll_loops.ml index c85d9b2aa71..697409bca64 100644 --- a/src/kernel_internals/typing/unroll_loops.ml +++ b/src/kernel_internals/typing/unroll_loops.ml @@ -318,7 +318,7 @@ let copy_block kf switch_label_action break_continue_must_change bl = labelled_stmt_tbl calls_tbl stmt = let result = { labels = []; - sid = Sid.next (); + sid = Cil_const.Sid.next (); succs = []; preds = []; skind = stmt.skind; @@ -627,14 +627,14 @@ class do_it global_find_init ((force:bool),(times:int)) = object(self) let break_label = fresh_label () in let break_lbl_stmt = mkEmptyStmt () in break_lbl_stmt.labels <- [break_label]; - break_lbl_stmt.sid <- Cil.Sid.next (); + break_lbl_stmt.sid <- Cil_const.Sid.next (); break_lbl_stmt in let mk_continue () = let continue_label = fresh_label () in let continue_lbl_stmt = mkEmptyStmt () in continue_lbl_stmt.labels <- [continue_label] ; - continue_lbl_stmt.sid <- Cil.Sid.next (); + continue_lbl_stmt.sid <- Cil_const.Sid.next (); continue_lbl_stmt in let current_continue = ref (mk_continue ()) in diff --git a/src/kernel_services/analysis/exn_flow.ml b/src/kernel_services/analysis/exn_flow.ml index ce65a50c9f0..ee42ce089bd 100644 --- a/src/kernel_services/analysis/exn_flow.ml +++ b/src/kernel_services/analysis/exn_flow.ml @@ -350,7 +350,8 @@ let generate_exn_union e exns = in let union_name = "__fc_exn_union" in let exn_kind_union = - Cil.mkCompInfo false union_name ~norig:union_name create_union_fields [] + Cil_const.mkCompInfo + false union_name ~norig:union_name create_union_fields [] in let create_struct_fields _ = let uncaught = (exn_uncaught_name, Cil.intType, None, [], loc) in @@ -363,7 +364,8 @@ let generate_exn_union e exns = in let struct_name = "__fc_exn_struct" in let exn_struct = - Cil.mkCompInfo true struct_name ~norig:struct_name create_struct_fields [] + Cil_const.mkCompInfo + true struct_name ~norig:struct_name create_struct_fields [] in exn_kind_union, exn_struct @@ -690,8 +692,10 @@ object(self) method private clean_catch_clause (bind,b as handler) acc = let remove_local v = - let f = Cil.get_fundec self#behavior (Extlib.the self#current_func) in - let v = Cil.get_varinfo self#behavior v in + let f = + Visitor_behavior.get_fundec self#behavior (Extlib.the self#current_func) + in + let v = Visitor_behavior.get_varinfo self#behavior v in f.slocals <- List.filter (fun v' -> v!=v') f.slocals; in match bind with diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml index 9fd8da5e14f..60ee0168a45 100644 --- a/src/kernel_services/ast_queries/file.ml +++ b/src/kernel_services/ast_queries/file.ml @@ -1567,7 +1567,7 @@ let prepare_from_c_files () = let init_project_from_visitor ?(reorder=false) prj (vis:Visitor.frama_c_visitor) = - if not (Cil.is_copy_behavior vis#behavior) + if not (Visitor_behavior.is_copy vis#behavior) || not (Project.equal prj (Extlib.the vis#project)) then Kernel.fatal diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml index 7b347942529..968ecbe40a8 100644 --- a/src/kernel_services/ast_queries/logic_utils.ml +++ b/src/kernel_services/ast_queries/logic_utils.ml @@ -2513,7 +2513,7 @@ let eval_term_lval global_find_init (lhost, loff) = | _ -> None class simplify_const_lval global_find_init = object (self) - inherit Cil.genericCilVisitor (Cil.copy_visit (Project.current ())) + inherit Cil.genericCilVisitor (Visitor_behavior.copy_visit (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 53907e6dc53..b606c8acfb8 100644 --- a/src/kernel_services/ast_transformations/filter.ml +++ b/src/kernel_services/ast_transformations/filter.ml @@ -327,7 +327,7 @@ end = struct * *) class filter_visitor pinfo prj = object(self) - inherit Visitor.generic_frama_c_visitor (Cil.copy_visit prj) + inherit Visitor.generic_frama_c_visitor (Visitor_behavior.copy_visit prj) val mutable keep_stmts = Stmt.Set.empty val mutable fi = None @@ -396,13 +396,13 @@ end = struct (fun v -> Varinfo.Hashtbl.add local_visible v (); let v' = Cil.copyVarinfo v v.vname in - Cil.set_varinfo self#behavior v v'; - Cil.set_orig_varinfo self#behavior v' v; + Visitor_behavior.set_varinfo self#behavior v v'; + Visitor_behavior.set_orig_varinfo self#behavior v' v; (match v.vlogic_var_assoc, v'.vlogic_var_assoc with None, None -> () | Some lv, Some lv' -> - Cil.set_logic_var self#behavior lv lv'; - Cil.set_orig_logic_var self#behavior lv' lv + Visitor_behavior.set_logic_var self#behavior lv lv'; + Visitor_behavior.set_orig_logic_var self#behavior lv' lv | _ -> assert false (* copy should be faithful *)); v') formals @@ -418,13 +418,13 @@ end = struct then begin Varinfo.Hashtbl.add local_visible var (); let var' = Cil.copyVarinfo var var.vname in - Cil.set_varinfo self#behavior var var'; - Cil.set_orig_varinfo self#behavior var' var; + Visitor_behavior.set_varinfo self#behavior var var'; + Visitor_behavior.set_orig_varinfo self#behavior var' var; (match var.vlogic_var_assoc, var'.vlogic_var_assoc with None, None -> () | Some lv, Some lv' -> - Cil.set_logic_var self#behavior lv lv'; - Cil.set_orig_logic_var self#behavior lv' lv + Visitor_behavior.set_logic_var self#behavior lv lv'; + Visitor_behavior.set_orig_logic_var self#behavior lv' lv | _ -> assert false (* copy should be faithful *)); var' :: (filter locals) end else filter locals @@ -434,7 +434,8 @@ end = struct method! vcode_annot v = Extlib.may Cil.CurrentLoc.set (Cil_datatype.Code_annotation.loc v); let stmt = - Cil.get_original_stmt self#behavior (Extlib.the self#current_stmt) + Visitor_behavior.get_original_stmt + self#behavior (Extlib.the self#current_stmt) in debug "[annotation] stmt %d : %a @." stmt.sid Printer.pp_code_annotation v; @@ -516,14 +517,14 @@ end = struct Cil.ChangeDoChildrenPost (b, optim) method private change_sid s = - let orig = Cil.get_original_stmt self#behavior s in - assert (Cil.get_stmt self#behavior orig == s); + let orig = Visitor_behavior.get_original_stmt self#behavior s in + assert (Visitor_behavior.get_stmt self#behavior orig == s); let old = s.sid in let keep = Stmt.Set.mem s keep_stmts in keep_stmts <- Stmt.Set.remove s keep_stmts; - s.sid <- Cil.Sid.next (); - Cil.set_stmt self#behavior orig s; - Cil.set_orig_stmt self#behavior s orig; + s.sid <- Cil_const.Sid.next (); + Visitor_behavior.set_stmt self#behavior orig s; + Visitor_behavior.set_orig_stmt self#behavior s orig; if keep then self#add_stmt_keep s; debug "@[finalize sid:%d->sid:%d@]@\n@." old s.sid @@ -539,7 +540,7 @@ end = struct | If (_,bthen,belse,loc) -> let bthen = Cil.visitCilBlock (self:>Cil.cilVisitor) bthen in let belse = Cil.visitCilBlock (self:>Cil.cilVisitor) belse in - let s_orig = Cil.get_original_stmt self#behavior s in + let s_orig = Visitor_behavior.get_original_stmt self#behavior s in optim_if finfo keep_stmts s_orig s None bthen belse loc | Switch (_exp, body, _, loc) -> (* the switch is invisible : it can be translated into a block. *) @@ -561,7 +562,7 @@ end = struct anything to do: it will not appear at all in the function. *) if Info.loc_var_visible (self#get_finfo()) v then begin - let v' = Cil.get_varinfo self#behavior v in + let v' = Visitor_behavior.get_varinfo self#behavior v in v'.vdefined <- false; end; mk_new_stmt s (mk_stmt_skip s) @@ -584,7 +585,7 @@ end = struct we would have multiple syntactic scope for the same variable). *) method private remove_local_static_attr v = - let new_v = Cil.get_varinfo self#behavior v in + let new_v = Visitor_behavior.get_varinfo self#behavior v in new_v.vattr <- Cil.dropAttribute Cabs2cil.fc_local_static new_v.vattr method private process_visible_stmt s = @@ -612,7 +613,7 @@ end = struct self#change_sid s'; (match s'.skind with | If (cond,bthen,belse,loc) -> - let s_orig = Cil.get_original_stmt self#behavior s' in + let s_orig = Visitor_behavior.get_original_stmt self#behavior s' in optim_if finfo keep_stmts s_orig s' (Some cond) bthen belse loc | Switch (e,b,c,l) -> let c' = List.filter (not $ (can_skip keep_stmts)) c in @@ -703,7 +704,7 @@ end = struct (fun () -> Cil.setFormals f new_formals) self#get_filling_actions; (* clean up the environment if we have more than one copy of the function in the sliced code. *) - Cil.reset_behavior_stmt self#behavior; + Visitor_behavior.reset_stmt self#behavior; keep_stmts <- Stmt.Set.empty; Varinfo.Hashtbl.clear local_visible; Varinfo.Hashtbl.add spec_table f.svar @@ -822,14 +823,14 @@ end = struct new_var.vtype <- mytype; List.iter2 (fun x y -> - Cil.set_varinfo self#behavior x y; - Cil.set_orig_varinfo self#behavior y x; + Visitor_behavior.set_varinfo self#behavior x y; + Visitor_behavior.set_orig_varinfo self#behavior y x; match x.vlogic_var_assoc with None -> (); | Some lv -> let lv' = Cil.cvar_to_lvar y in - Cil.set_logic_var self#behavior lv lv'; - Cil.set_orig_logic_var self#behavior lv' lv) + Visitor_behavior.set_logic_var self#behavior lv lv'; + Visitor_behavior.set_orig_logic_var self#behavior lv' lv) old_formals new_formals; (* adds the new parameters to the formals decl table *) @@ -856,15 +857,15 @@ end = struct let orig_var = Ast_info.Function.get_vi kf.fundec in (* The first copy is also the default one for varinfo that are not handled by ff_var but directly by the visitor *) - if (Cil.get_varinfo self#behavior orig_var) == orig_var then - Cil.set_varinfo self#behavior orig_var new_var; + if (Visitor_behavior.get_varinfo self#behavior orig_var) == orig_var then + Visitor_behavior.set_varinfo self#behavior orig_var new_var; (* Set the new_var as an already known one, coming from the vi associated to the current kf. *) - Cil.set_varinfo self#behavior new_var new_var; - Cil.set_orig_varinfo self#behavior new_var orig_var; - Cil.set_kernel_function self#behavior kf new_kf; - Cil.set_orig_kernel_function self#behavior new_kf kf; + Visitor_behavior.set_varinfo self#behavior new_var new_var; + Visitor_behavior.set_orig_varinfo self#behavior new_var orig_var; + Visitor_behavior.set_kernel_function self#behavior kf new_kf; + Visitor_behavior.set_orig_kernel_function self#behavior new_kf kf; Queue.add (fun () -> Globals.Functions.register new_kf) self#get_filling_actions; GFunDecl (Cil.empty_funspec(), new_var, loc), action @@ -902,10 +903,10 @@ end = struct let new_kf = make_new_kf my_kf kf new_fct_var in (* Set the new_var as an already known one, * coming from the vi associated to the current kf. *) - Cil.set_varinfo self#behavior new_fct_var new_fct_var; - Cil.set_orig_varinfo self#behavior new_fct_var fvar; - Cil.set_kernel_function self#behavior kf new_kf; - Cil.set_orig_kernel_function self#behavior new_kf kf; + Visitor_behavior.set_varinfo self#behavior new_fct_var new_fct_var; + Visitor_behavior.set_orig_varinfo self#behavior new_fct_var fvar; + Visitor_behavior.set_kernel_function self#behavior kf new_kf; + Visitor_behavior.set_orig_kernel_function self#behavior new_kf kf; Queue.add (fun () -> Globals.Functions.register new_kf) self#get_filling_actions; diff --git a/src/kernel_services/ast_transformations/inline.ml b/src/kernel_services/ast_transformations/inline.ml index cb00a64b313..49f61fa5d21 100644 --- a/src/kernel_services/ast_transformations/inline.ml +++ b/src/kernel_services/ast_transformations/inline.ml @@ -90,7 +90,7 @@ let inline_call loc caller callee return args = method! vvrbl v = if v.vglob then - Cil.ChangeTo (Cil.get_original_varinfo self#behavior v) + Cil.ChangeTo (Visitor_behavior.get_original_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 9e6738a2b39..9f3e0dee81e 100644 --- a/src/kernel_services/visitors/visitor.ml +++ b/src/kernel_services/visitors/visitor.ml @@ -66,7 +66,7 @@ object(self) method current_kf = !current_kf method! private vstmt stmt = - let orig_stmt = Cil.get_original_stmt self#behavior stmt in + let orig_stmt = Visitor_behavior.get_original_stmt self#behavior stmt in let annots = Annotations.fold_code_annot (fun e a acc -> (e, a) :: acc) orig_stmt [] in @@ -91,7 +91,7 @@ object(self) if [x] is already trivial itself. *) let becomes_trivial = is_trivial y && not (is_trivial x) in let curr_add, remove_curr = - if Cil.is_copy_behavior vis#behavior then + if Visitor_behavior.is_copy vis#behavior then (* Copy visitor. We add [y], except if trivial. No sense in removing [x], since the stmt is a new one. *) (if not becomes_trivial then [e, y] else []), @@ -115,7 +115,7 @@ object(self) let change_stmt stmt (add, remove) = if (add <> [] || remove <> []) then begin let kf = Extlib.the self#current_kf in - let new_kf = Cil.get_kernel_function self#behavior kf in + let new_kf = Visitor_behavior.get_kernel_function self#behavior kf in Queue.add (fun () -> List.iter @@ -173,12 +173,12 @@ object(self) let old_allocates = fold_elt Annotations.fold_allocates in let old_extended = fold_elt Annotations.fold_extended in let b' = - if Cil.is_copy_behavior self#behavior then + if Visitor_behavior.is_copy self#behavior then { b with b_name = b.b_name } else b in let res = self#vbehavior b' in - let new_kf = Cil.get_kernel_function self#behavior kf in + let new_kf = Visitor_behavior.get_kernel_function self#behavior kf in let add_queue a = Queue.add a self#get_filling_actions in let visit_clauses vis f = (* Ensures that we have a table associated to new_kf in Annotations. *) @@ -385,7 +385,7 @@ object(self) method private vfunspec_annot () = let kf = Extlib.the self#current_kf in - let new_kf = Cil.get_kernel_function self#behavior kf in + let new_kf = Visitor_behavior.get_kernel_function self#behavior kf in let old_behaviors = Annotations.fold_behaviors (fun e b acc -> (e,b)::acc) kf [] in @@ -625,18 +625,18 @@ object(self) method! vglob g = let fundec, has_kf = match g with | GFunDecl(_,v,_) -> - let ov = Cil.get_original_varinfo self#behavior v in + let ov = Visitor_behavior.get_original_varinfo self#behavior v in let kf = try Globals.Functions.get ov with Not_found -> Kernel.fatal "No kernel function for %s(%d)" v.vname v.vid in (* Just make a copy of current kernel function in case it is needed *) - let new_kf = Cil.memo_kernel_function self#behavior kf in - if Cil.is_copy_behavior self#behavior then + let new_kf = Visitor_behavior.memo_kernel_function self#behavior kf in + if Visitor_behavior.is_copy self#behavior then new_kf.spec <- Cil.empty_funspec (); self#set_current_kf kf; None, true | GFun(f,_) -> - let v = Cil.get_original_varinfo self#behavior f.svar in + let v = Visitor_behavior.get_original_varinfo self#behavior f.svar in let kf = try Globals.Functions.get v with Not_found -> @@ -644,8 +644,8 @@ object(self) v.vname Project.pretty (Project.current ()) in - let new_kf = Cil.memo_kernel_function self#behavior kf in - if Cil.is_copy_behavior self#behavior then + let new_kf = Visitor_behavior.memo_kernel_function self#behavior kf in + if Visitor_behavior.is_copy self#behavior then new_kf.spec <- Cil.empty_funspec (); self#set_current_kf kf; Some f, true @@ -672,7 +672,7 @@ object(self) | _ -> None in let change_glob ng spec = - let cond = is_copy_behavior self#behavior in + let cond = Visitor_behavior.is_copy self#behavior in match ng with | GVar(vi,init,_) -> if cond then @@ -689,7 +689,7 @@ object(self) | GFunDecl(_,v,l) -> (match self#current_kf with | Some kf -> - let new_kf = Cil.get_kernel_function self#behavior kf in + let new_kf = Visitor_behavior.get_kernel_function self#behavior kf in if cond then begin Queue.add (fun () -> @@ -743,7 +743,7 @@ object(self) if cond then begin match self#current_kf with | Some kf -> - let new_kf = Cil.get_kernel_function self#behavior kf in + let new_kf = Visitor_behavior.get_kernel_function self#behavior kf in Queue.add (fun () -> Kernel.debug ~dkey:Kernel.dkey_visitor @@ -836,11 +836,14 @@ class generic_frama_c_visitor bhv = let queue = Queue.create () in internal_generic_frama_c_visitor current_fundec queue current_kf bhv -class frama_c_copy prj = generic_frama_c_visitor (copy_visit prj) +class frama_c_copy prj = + generic_frama_c_visitor (Visitor_behavior.copy_visit prj) -class frama_c_refresh prj = generic_frama_c_visitor (refresh_visit prj) +class frama_c_refresh prj = + generic_frama_c_visitor (Visitor_behavior.refresh_visit prj) -class frama_c_inplace = generic_frama_c_visitor (inplace_visit()) +class frama_c_inplace = + generic_frama_c_visitor (Visitor_behavior.inplace_visit()) let visitFramacFileCopy vis f = visitCilFileCopy (vis:>cilVisitor) f @@ -854,7 +857,7 @@ let visitFramacGlobal vis g = vis#fill_global_tables; g' let visitFramacFunction vis f = - let orig_var = Cil.get_original_varinfo vis#behavior f.svar in + let orig_var = Visitor_behavior.get_original_varinfo vis#behavior f.svar in let old_current_kf = vis#current_kf in vis#set_current_kf (Globals.Functions.get orig_var); let f' = visitCilFunction (vis:>cilVisitor) f in @@ -869,7 +872,7 @@ let visitFramacKf vis kf = | None -> kf | Some prj -> let vi = Kernel_function.get_vi kf in - let vi' = Cil.get_varinfo vis#behavior vi in + let vi' = Visitor_behavior.get_varinfo vis#behavior vi in Project.on prj Globals.Functions.get vi' let visitFramacExpr vis e = diff --git a/src/kernel_services/visitors/visitor.mli b/src/kernel_services/visitors/visitor.mli index 3fffe6a974c..faa4d4be3a6 100644 --- a/src/kernel_services/visitors/visitor.mli +++ b/src/kernel_services/visitors/visitor.mli @@ -95,7 +95,7 @@ class frama_c_refresh: Project.t -> frama_c_visitor *) class generic_frama_c_visitor: - Cil.visitor_behavior -> frama_c_visitor + Visitor_behavior.t -> frama_c_visitor (** Generic class that abstracts over [frama_c_inplace] and [frama_c_copy]. @plugin development guide *) -- GitLab