Source file meta_annotate.ml

(**************************************************************************)
(*                                                                        *)
(*  This file is part of the Frama-C's MetACSL plug-in.                   *)
(*                                                                        *)
(*  Copyright (C) 2018-2024                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file LICENSE)                       *)
(*                                                                        *)
(**************************************************************************)

open Meta_utils
open Meta_options
open Meta_parse
open Meta_dispatch
open Cil_types

let after_present p =
  let vis = object (_)
    inherit Visitor.frama_c_inplace
    val mutable found = false
    method get () = found
    method! vlogic_label = function
      | FormalLabel "After" -> found <- true; Cil.DoChildren
      | _ -> Cil.DoChildren
  end in
  ignore (Visitor.visitFramacPredicate (vis :> Visitor.frama_c_visitor) p);
  vis # get ()

let replace_after_before is_after stmt pred =
  let vis = object (_)
    inherit Visitor.frama_c_inplace
    method! vlogic_label = function
      | FormalLabel "After" when is_after ->
        Cil.ChangeTo (BuiltinLabel Here)
      | FormalLabel "Before" when is_after ->
        Cil.ChangeTo (StmtLabel (ref stmt))
      | FormalLabel "Before" ->
        Cil.ChangeTo (BuiltinLabel Here)
      | _ -> Cil.DoChildren
  end in
  Visitor.visitFramacPredicate vis pred

(*
 * Add an unique C label to a statement if it does not have one already
 *)
let label_counter = ref 0
let add_label stmt =
  let loc = Cil.CurrentLoc.get () in
  let label_name = "meta_pre_" ^ (string_of_int !label_counter) in
  if stmt.labels = [] then (
    stmt.labels <- (Label (label_name, loc, false)) :: stmt.labels ;
    label_counter := !label_counter + 1
  )

let delayed_instances = Stmt_Hashtbl.create 256
let delayed_contracts = Fundec_Hashtbl.create 256
let cfg_recomputation = ref Fundec_Set.empty

(* Common class for contexts *)
class context_visitor flags all_mp table = object(self)
  inherit Visitor.frama_c_inplace
  val mutable mp_todo = []
  val skip_to_add = Stmt_Hashtbl.create 50

  (* Fill mp_todo with MPs to process for the given function name *)
  method fill_todo fn =
    let todo = find_hash_list Str_Hashtbl.find_opt table fn in
    mp_todo <- List.map (Hashtbl.find all_mp) todo

  (* Determine is the current function is a target for some of the properties
   * in the current context *)
  method! vfunc f =
    self # fill_todo f.svar.vname;
    if mp_todo = [] then Cil.SkipChildren
    else (
      Stmt_Hashtbl.clear skip_to_add;
      Cil.DoChildren
    )

  method private curr_func_cfg_recompute () =
    let f = Option.get self#current_func in
    cfg_recomputation := Fundec_Set.add f !cfg_recomputation

  (* Remember that we must add a SKIP after the statement for an annotation to
   * be put *)
  method private create_next_stmt stmt =
    self#curr_func_cfg_recompute ();
    let loc = Cil.CurrentLoc.get () in
    let new_stmt = Cil.mkStmtOneInstr ~valid_sid:true (Skip loc) in
    add_to_hash_list Stmt_Hashtbl.(find_opt, replace) skip_to_add stmt new_stmt;
    new_stmt

  (* Insert registered SKIPs in corresponding blocks *)
  method! vblock _ = Cil.DoChildrenPost (fun block ->
      let rec aux = function
        | [] -> []
        | s :: t ->
          s :: (find_hash_list Stmt_Hashtbl.find_opt skip_to_add s) @ (aux t)
      in block.bstmts <- aux block.bstmts;
      block
    )

  (* Common method used by the subclasses to instantiate an ump *)
  method instantiate ?(post=None) ?(force_after=false) stmt assoc_list ump =
    let loc = Property.location ump.ump_ip in
    let kf = Option.get self # current_kf in
    let vf = Kernel_function.get_vi kf in
    let func_ptr = Cil_builder.Exp.(cil_term ~loc (addr (var vf))) in
    let func_assoc = "\\func", RepVariable func_ptr in
    let assoc_list = func_assoc :: assoc_list in
    (* Do not instantiate anything on ghost statements *)
    if not stmt.ghost then
      let pred = ump.ump_property kf ~stmt assoc_list in
      (* Apply potential post transformation *)
      let post_pred = match post with
        | None -> pred
        | Some f -> f pred
      in
      (* Simplify *)
      (* Discard if trivially true *)
      if not @@ Logic_utils.is_trivially_true post_pred then
        (* Check if the annotation should be inserted before of after the
         * current statement *)
        let after_pres = after_present post_pred in
        let will_be_after = force_after || after_pres in
        (* Only add a pre C label when there is a legitimate reason *)
        if after_pres then add_label stmt;
        (* Create a SKIP after the stmt to attach the annot to *)
        let annot_stmt = if will_be_after then
            self # create_next_stmt stmt else stmt
        in
        (* Replace After/Before by correct actual labels *)
        let labelled = replace_after_before will_be_after stmt post_pred in
        let finalize () =
          let named = Meta_dispatch.name_mp_pred flags labelled ump.ump_counter in
          let kind = if ump.ump_assert then Assert else Check in
          let annot =
            Logic_const.(
              new_code_annotation
                (AAssert ([], toplevel_predicate ~kind named)))
          in
          Annotations.add_code_annot ump.ump_emitter ~kf annot_stmt annot;
          let ips = Property.ip_of_code_annot kf annot_stmt annot in
          Meta_dispatch.add_dependency ump ips
        in
        (* Delay actual instanciation for correct numbering *)
        add_to_hash_list Stmt_Hashtbl.(find_opt, replace) delayed_instances
          stmt finalize
end

let get_callsites_ips kf rips =
  let calls = Kernel_function.find_syntactic_callsites kf in
  match calls with
    (* if the function is never called (e.g. it is the entry point), then
       do not set up a proxy over a vacuous set of properties. *)
    | [] -> []
    | _ ->
      let segmented =
        List.map
          (fun rip ->
             Statuses_by_call.setup_precondition_proxy kf rip;
             List.map
               (fun (_, stmt) ->
                  Statuses_by_call.precondition_at_call kf rip stmt)
               calls)
          rips
      in
      List.concat segmented

(* Simply modifies a function contract to ensures that pred is a weak invariant *)
class weak_inv_visitor flags full_table table (pre, post) = object (self)
  inherit context_visitor flags full_table table

  (* Given a kf and a UMP, add it as requires/ensures to the kf *)
  method add_to_contract ump =
    let kf = Option.get self # current_kf in
    let pred = ump.ump_property kf [] in
    let finalize () =
      let pred' = Meta_dispatch.name_mp_pred flags pred ump.ump_counter in
      let pred_name = (Emitter.get_name ump.ump_emitter) :: pred'.pred_name in
      let pred'' = {pred' with pred_name} in
      let kind = if ump.ump_assert then Assert else Check in
      let deps = ref [] in
      if pre then (
        let ip_requires = Logic_const.new_predicate ~kind pred'' in
        Annotations.add_requires ump.ump_emitter kf [ip_requires];
        let defb = Option.get (Cil.find_default_behavior (Annotations.funspec kf)) in
        let rips = Property.ip_of_requires kf Kglobal defb ip_requires :: !deps in
        let callsites_ip = get_callsites_ips kf rips in
        deps := rips @ callsites_ip @ !deps
      );
      begin match post with
        | `None -> ()
        | `Strict ->
          let ip_ensures = Logic_const.new_predicate ~kind pred'' in
          Annotations.add_ensures ump.ump_emitter kf [(Normal, ip_ensures)];
          let defb = Option.get (Cil.find_default_behavior (Annotations.funspec kf)) in
          let eip = Property.ip_of_ensures kf Kglobal defb (Normal, ip_ensures) in
          deps := eip :: !deps
        | `Conditional ->
          let ip_assumes = Logic_const.new_predicate ~kind pred'' in
          let ip_ensures = Logic_const.new_predicate ~kind pred'' in
          let bh = {b_name = List.hd pred_name; b_requires = [];
                    b_assumes = [ip_assumes]; b_post_cond = [(Normal, ip_ensures)];
                    b_assigns = WritesAny; b_allocation = FreeAllocAny;
                    b_extended = []} in
          Annotations.add_behaviors ump.ump_emitter kf [bh];
      end;
      Meta_dispatch.add_dependency ump !deps
    in
    (* Delay actual instanciation for correct numbering *)
    let fundec = Kernel_function.get_definition kf in
    add_to_hash_list Fundec_Hashtbl.(find_opt, replace) delayed_contracts
      fundec finalize

  method! vfunc f =
    self # fill_todo f.svar.vname;
    List.iter (self # add_to_contract) mp_todo;
    Cil.SkipChildren
end

(* Given a tlval, return the term taking its address *)
let addr_of_tlval tlval =
  let typ = Cil.typeOfTermLval tlval in
  Logic_utils.mk_logic_AddrOf tlval typ

let addr_of_tlhost (h,_) = addr_of_tlval (h, TNoOffset)

(* Instantiate properties at any call site, replacing \called by
 * the called function. *)
class calling_visitor flags all_mp table = object (self)
  inherit context_visitor flags all_mp table

  method calling_instance stmt called called_kf args =
    let addr_term = addr_of_tlval called in
    let main_assoc = ("\\called", RepVariable addr_term) in
    let assoc_list = match called_kf with
      | None ->
        Self.warning ~once:true
          "\\called_arg cannot be used with indirect calls" ;
        [main_assoc]
      | Some kf ->
        let formals = Kernel_function.get_formals kf in
        try
          let param_assocs = List.map2 (fun formal given ->
              let given_term = Logic_utils.expr_to_term given in
              (formal.vorig_name, given_term)
            ) formals args
          in [main_assoc; ("\\called_arg", RepApp param_assocs)]
        with Invalid_argument _ ->
          Self.warning ~once:true "\\called_arg cannot be used with variadic \
                                   functions. Please use the Instantiate plugin" ;
          [main_assoc]
    in
    List.iter (self # instantiate stmt assoc_list) mp_todo

  method! vinst = function
    | Call (_, fexpr, args, _) ->
      let lv = match fexpr.enode with Lval lv -> lv | _ -> assert false in
      let stmt = Option.get self # current_stmt in
      let called_kf = Kernel_function.get_called fexpr in
      let tlval = Logic_utils.lval_to_term_lval lv in
      self#calling_instance stmt tlval called_kf args ;
      Cil.DoChildren
    | _ -> Cil.SkipChildren
end


(*
 * Retrieve the specification from a kf, replace every instance of its formal
 * parameters by the actual arguments passed, extract "assigns" clauses and pass
 * them to "process"
 *)
let inspect_contract process stmt ckf args =
  let vis = object (_)
    inherit Visitor.frama_c_inplace

    val fargs =
      let h = Hashtbl.create (List.length args) in
      let _, oargs, _, _ = Cil.splitFunctionType
          (Kernel_function.get_type ckf) in
      if (List.length args) != 0 then
        List.iter2 (fun (a, _, _) b -> Hashtbl.add h a b)
          (Option.get oargs) args ;
      h

    method! vterm _ =
      Cil.DoChildrenPost (fun term -> match term.term_node with
          | TLval (host, _) | TAddrOf (host, _) | TStartOf (host, _) ->
            begin match host with
              | TVar lovar ->
                if Hashtbl.mem fargs lovar.lv_name then
                  Logic_utils.expr_to_term @@
                  Hashtbl.find fargs lovar.lv_name
                else term
              | _ -> term
            end
          | _ -> term
        )
  end in
  let bhvs = Annotations.behaviors ckf in
  let f b =
    let ass =
      Annotations.fold_assumes
        (fun _ p old ->
           (Visitor.visitFramacPredicate vis
              (Logic_const.pred_of_id_pred p))
           ::old)
        ckf b.b_name []
    in
    match b.b_assigns with
      | WritesAny ->
        Self.warning "Cannot analyze footprint of function %a: no assigns \
                      clause. Assuming meta-properties with reading/writing contexts are \
                      valid in this function." Kernel_function.pretty ckf
      | Writes l -> process ckf stmt vis l ass
  in
  List.iter f bhvs

(* Instantiate properties at any point where a modification can happen, that is:
 * - common assignments (including the result of a function)
 * - calls to an external function (if the flag is set)
*)
class writing_visitor flags all_mp table = object(self)
  inherit context_visitor flags all_mp table

  (* Instantiates the property while replacing \written terms *)
  method writing_instance ?post stmt = function
    | TVar lv, _ when flags.simpl && Meta_simplify.is_not_orig_variable lv -> ()
    | written ->
      let addr_term = addr_of_tlval written in
      let base_addr_term = addr_of_tlhost written in
      let assoc_list =
        [ "\\written", RepVariable addr_term;
          "\\lhost_written", RepVariable base_addr_term
        ]
      in
      List.iter (self # instantiate ~post stmt assoc_list) mp_todo

  (* Inspect function specs to see what it assigns and instantiate the
   * annotation for each assigns clause (with the precond leading to it) *)
  method private external_assigns _ stmt vis l preconds =
    List.iter (fun (it, _) ->
        let term = it.it_content in
        let propag = Visitor.visitFramacTerm vis term in
        if not @@ Logic_utils.contains_result propag then
          match propag.term_node with
            | TLval t ->
              let post prop =
                List.fold_left (fun prop prec ->
                    Logic_const.pimplies (prec, prop)
                  ) prop preconds
              in
              self#writing_instance ~post stmt t ;
            | _ -> assert false
      ) l

  (* Instantiate an annotation for each affectation (potentially resulting
   * from a call) and each call to an undefined function *)
  method! vstmt_aux stmt =
    if not stmt.ghost then (
      match stmt.skind with
        | Instr Set (lval, _, _) ->
          (* x = y, \written -> &x *)
          let tl = Logic_utils.lval_to_term_lval lval in
          self # writing_instance stmt tl ;
          Cil.SkipChildren
        | Instr Call (lval, fexp, args, (source,_)) ->
          if Option.is_some lval then (
            (* x = f(y), \written -> &x *)
            let tl = Logic_utils.lval_to_term_lval
                (Option.get lval) in
            self#writing_instance stmt tl
          ) ;
          (match Kernel_function.get_called fexp with
            | Some kf ->
              let caller = Option.get self#current_kf in
              let callee_def = Kernel_function.has_definition kf in
              let is_check_assigns f =
                Kernel_function.Set.mem f flags.check_callee_assigns
              in
              if (not callee_def && flags.check_external) ||
                 is_check_assigns kf && not (is_check_assigns caller)
              then
                inspect_contract self#external_assigns stmt kf args
            | None ->
              Self.warning ~source
                "Indirect call '%a': assuming no 'writing' context-related \
                 assertions are needed"
                Printer.pp_exp fexp;
          ); Cil.SkipChildren
        | _ -> Cil.DoChildren
    ) else Cil.SkipChildren
end

module TLvalSet = Cil_datatype.Term_lval.Set
module StmtHashtbl = Cil_datatype.Stmt.Hashtbl
class reading_visitor flags all_mp table = object (self)
  inherit context_visitor flags all_mp table

  (* Instantiates the property while replacing \read terms *)
  method reading_instance ?post stmt read =
    let addr_term = addr_of_tlval read in
    let base_addr_term = addr_of_tlhost read in
    let assoc_list =
      ["\\read", RepVariable addr_term;
       "\\lhost_read", RepVariable base_addr_term ]
    in
    List.iter (self#instantiate ~post stmt assoc_list) mp_todo

  (* Hashtable : stmt -> set of tlvals used in it. Used to avoid duplicate
   * annotations *)
  val lvals_by_stmt = StmtHashtbl.create 20
  val mutable in_exp = false (* Visitor currently in an expression *)

  (* Allow detecting if we are currently in an expression *)
  method! vexpr e =
    in_exp <- true ;
    match e.enode with
      | SizeOfE _ | AlignOfE _ ->
        (* we're not evaluating the expression itself, merely its type. *)
        in_exp <- false; Cil.SkipChildren
      | AddrOf (_,o) | StartOf(_,o) ->
        (* the toplevel lval is not read. However, we might read some lvals
           when evaluating the offset. The host is always a Var in this
           context, thus we don't need to visit it further. *)
        ignore (Visitor.visitFramacOffset (self:>Visitor.frama_c_visitor) o);
        in_exp <- false;
        Cil.SkipChildren
      | _ ->
        Cil.DoChildrenPost (fun e -> in_exp <- false ; e)

  (* When encoutering an lval in an expression, add it to the statement set *)
  method! vlval lval =
    let typ = Cil.typeOfLval lval in
    (* Exclude functions names *)
    if in_exp && not (Cil.isFunctionType typ) then begin
      if Option.is_some (self # current_stmt) then
        let stmt = Option.get (self # current_stmt) in
        begin match stmt.skind with
          | UnspecifiedSequence _ -> () (* ignore attributes from US node *)
          | _ ->
            let tl = Logic_utils.lval_to_term_lval lval in
            let old_set =
              match StmtHashtbl.find_opt lvals_by_stmt stmt with
                | Some s -> s
                | None -> TLvalSet.empty
            in
            StmtHashtbl.add lvals_by_stmt stmt @@ TLvalSet.add tl old_set
        end
    end ; Cil.DoChildren

  (* Inspect function specs to see what it reads and instantiate the
   * annotation for each \from clause (with the precond leading to it) *)
  method passthrough_from kf stmt vis l preconds =
    List.iter (fun (_, deps) -> match deps with
        | FromAny ->
          Self.warning ~once:true
            "Cannot fully analyze read footprint of function %a: no \\from \
             part in some assigns clauses."
            Kernel_function.pretty kf
        | From itl -> List.iter (fun it ->
            let term = it.it_content in
            let propag = Visitor.visitFramacTerm vis term in
            match propag.term_node with
              | TCastE (_, {term_node = TLval t})
              | TLval t ->
                let post property =
                  List.fold_left (fun prop prec ->
                      Logic_const.pimplies (prec, prop)
                    ) property preconds
                in
                self#reading_instance ~post stmt t
              | _ -> ()
          ) itl
      ) l

  method passthrough_process stmt kf args =
    let cond =
      (not (Kernel_function.has_definition kf) && flags.check_external) ||
      Kernel_function.Set.(
        mem kf flags.check_callee_assigns &&
        not (mem (Option.get self#current_kf) flags.check_callee_assigns))
    in
    if cond then
      inspect_contract self # passthrough_from stmt kf args

  method! vstmt_aux stmt =
    if not stmt.ghost then (
      (* If the statement is a call to an undefined function, use its spec to
       * generate \read *)
      begin match stmt.skind with
        | Instr Local_init (_, ConsInit (f, args, Plain_func), _) ->
          let kf = Globals.Functions.get f in
          self#passthrough_process stmt kf args
        | Instr Call (_, fexp, args, (source,_)) -> begin match
            Kernel_function.get_called fexp with
            | Some ckf -> self#passthrough_process stmt ckf args
            | None ->
              Self.warning ~source
                "Indirect call '%a': assuming no 'reading' context related \
                 assertion are needed"
                Printer.pp_exp fexp
          end
        | _ -> ()
      end ;
      let after s =
        let set = StmtHashtbl.find_opt lvals_by_stmt s in
        if Option.is_some set then
          TLvalSet.iter (self#reading_instance s) @@ Option.get set
      ; s
      in
      (* Visit every sub-expression to populate the tlval set then for each
       * lval, instantiate the property. *)
      Cil.DoChildrenPost after
    ) else Cil.DoChildren
end

(* Return the set of used lvals in a given predicate *)
let lvals_of_predicate pred =
  let s = ref (Some TLvalSet.empty) in
  let vis = object(self)
    inherit Visitor.frama_c_inplace

    method! vterm_lval tlval =
      s := Option.map (TLvalSet.add tlval) !s ; Cil.DoChildren

    method! vpredicate_node = function
      | Papp (li, _, _) -> begin match li.l_body with
          | LBnone -> ()
          | LBinductive _
          | LBreads _ -> s := None
          | LBpred p -> ignore (Visitor.visitFramacPredicate
                                  (self :> Visitor.frama_c_visitor) p)
          | LBterm t -> ignore (Visitor.visitFramacTerm
                                  (self :> Visitor.frama_c_visitor) t)
        end ; Cil.DoChildren
      | _ -> Cil.DoChildren
  end in
  ignore (Visitor.visitFramacPredicate vis pred) ; !s

(*
 * Modifies the function contract and add asserts to ensures that pred is a weak invariant
 * AND that each assignment maintains the invariant
 * A block of instructions can be left unchecked using `//@meta lenient` but this block must
 * maintain the invariant at the end
 *)
class strong_inv_visitor flags all_mp table = object (self)
  inherit weak_inv_visitor flags all_mp table (true, `Strict)
  val mutable lenient = false

  (* Given a lval which is to be modified, check if its modification
   * can interfere with the truth of the invariant (only rejects obvious non-interferences)
  *)
  method possible_interference lval ump =
    let tlval = Logic_utils.lval_to_term_lval lval in
    let kf = Option.get (self # current_kf) in
    let pred = ump.ump_property kf [] in
    let pvars = lvals_of_predicate pred in
    match pvars with
      | Some set -> not (
          TLvalSet.fold (fun pvar ->
              (&&) (Meta_simplify.neq_lval pvar tlval)
            ) set true
        )
      (* Could not determine what variables are used in the predicate *)
      | None -> true

  (* Check the statement contract of a statement to check if a lenient is present *)
  method check_annots stmt =
    let aux _ a = match a.annot_content with
      | AExtended (_, _, e) -> begin match e with
          | {ext_name = "imeta";
             ext_kind = Ext_terms [{term_node = TConst (LStr "lenient")}]} ->
            lenient <- true
          | _ -> () end
      | _ -> ()
    in
    Annotations.iter_code_annot aux stmt

  method! vstmt_aux stmt =
    self#check_annots stmt ;
    let non_loop modif ump =
      (* If a lenient was found, automatically instantiate the predicate
       * since we are not sure the invariant will be maintained inside the
       * statement. Else do it only if interference with the invariant is
       * possible (ie the statement may modify a variable used in the
       * invariant *)
      let can_interfere =
        not flags.simpl || match modif with
          | None -> false
          | Some m -> self # possible_interference m ump
      in
      if lenient || can_interfere then
        self#instantiate ~force_after:true stmt [] ump
    in
    begin match stmt.skind with
      | Loop _ ->
        let kf = Option.get (self # current_kf) in
        List.iter (fun ump ->
            let prop = ump.ump_property kf ~stmt [] in
            let kind = if ump.ump_assert then Assert else Check in
            let annot =
              Logic_const.(
                new_code_annotation
                  (AInvariant ([], true, toplevel_predicate ~kind prop)))
            in
            Annotations.add_code_annot ump.ump_emitter ~kf stmt annot
          ) mp_todo
      | Instr Set (lval, _, _) -> List.iter (non_loop (Some lval)) mp_todo
      | Instr Call _ -> List.iter (self#instantiate ~force_after:true stmt []) mp_todo
      | _ -> List.iter (non_loop None) mp_todo
    end ;
    if lenient then (
      lenient <- false ;
      Cil.SkipChildren
    ) else Cil.DoChildren

  method! vfunc f =
    self # fill_todo f.svar.vname;
    List.iter (self # add_to_contract) mp_todo;
    if mp_todo = [] then Cil.SkipChildren
    else Cil.DoChildren
end

(* Make one copy-pass for each context, typing and instanciating MPs on the fly *)
let annotate flags all_mp by_context =
  let get_vis table = function
    | Weak_invariant ->
      (new weak_inv_visitor flags all_mp table (true, `Strict) :> Visitor.frama_c_visitor)
    | Calling ->
      (new calling_visitor flags all_mp table :> Visitor.frama_c_visitor)
    | Writing ->
      (new writing_visitor flags all_mp table :> Visitor.frama_c_visitor)
    | Reading ->
      (new reading_visitor flags all_mp table :> Visitor.frama_c_visitor)
    | Strong_invariant ->
      (new strong_inv_visitor flags all_mp table :> Visitor.frama_c_visitor)
    | Precond ->
      (new weak_inv_visitor flags all_mp table (true, `None) :> Visitor.frama_c_visitor)
    | Postcond ->
      (new weak_inv_visitor flags all_mp table (false, `Strict) :> Visitor.frama_c_visitor)
    | Conditional_invariant ->
      (new weak_inv_visitor flags all_mp table (false, `Conditional) :> Visitor.frama_c_visitor)
  in
  List.iter (fun (ctx, table) ->
      let vis = get_vis table ctx in
      Visitor.visitFramacFileSameGlobals vis (Ast.get ())
    ) by_context;
  (* Finally, actually instanciate all annotations in the correct order *)
  let final_vis = object (_)
    inherit Visitor.frama_c_inplace

    method! vfunc f =
      (* Reset assertion numbers *)
      Hashtbl.iter (fun _ ump -> ump.ump_counter := 0) all_mp;
      (* Instantiate delayed contracts *)
      let todo = find_hash_list Fundec_Hashtbl.find_opt delayed_contracts f in
      List.iter (fun f -> f ()) (List.rev todo);
      Cil.DoChildren

    method! vstmt_aux stmt =
      (* Instantiate delayed annotations *)
      let todo = find_hash_list Stmt_Hashtbl.find_opt delayed_instances stmt in
      List.iter (fun f -> f ()) (List.rev todo);
      Cil.DoChildren

  end in
  Visitor.visitFramacFileSameGlobals final_vis (Ast.get ());
  let update_cfg f =
    Cfg.clearCFGinfo ~clear_id:false f;
    Cfg.cfgFun f
  in
  Fundec_Set.iter update_cfg !cfg_recomputation;
  if Fundec_Set.is_empty !cfg_recomputation then
    (* slight overapproximation: if we don't generate any annotation, then
       the AST is unchanged. *)
    Ast.mark_as_grown ()
  else
    Ast.mark_as_changed ()