Merge branch 'fix/wp/assigns-cfg' into 'master'

[wp] fix post-assigns and post-valid VC generation

See merge request frama-c/frama-c!2830

src/plugins/wp/Cache.ml

@@ -136,6 +136,11 @@ module MODE = WpContext.StaticGenerator(Datatype.Unit)
 let get_mode = MODE.get
 let set_mode m = MODE.clear () ; Wp_parameters.Cache.set (mode_name m)
 
+let is_updating () =
+  match MODE.get () with
+  | NoCache | Replay | Offline -> false
+  | Update | Rebuild | Cleanup -> true
+
 let task_hash wpo drv prover task =
   lazy
     begin

src/plugins/wp/Cache.mli

@@ -30,6 +30,8 @@ val get_hits : unit -> int
 val get_miss : unit -> int
 val get_removed : unit -> int
 
+val is_updating : unit -> bool
+
 val cleanup_cache : unit -> unit
 
 type runner =

src/plugins/wp/GuiSequent.ml

@@ -341,7 +341,7 @@ class pcond
     (focus : step_selection)
     (plang : Pcond.state) =
   object(self)
-    inherit Pcond.sequence plang as super
+    inherit Pcond.seqengine plang as super
 
     (* All displayed entries *)
     val mutable domain = Vars.empty

src/plugins/wp/LogicCompiler.ml

@@ -258,6 +258,10 @@ struct
       types = [];
     }
 
+  let has_at_frame frame label =
+    assert (not (Clabels.is_here label));
+    LabelMap.mem label frame.labels
+
   let mem_at_frame frame label =
     assert (not (Clabels.is_here label));
     try LabelMap.find label frame.labels

src/plugins/wp/LogicCompiler.mli

@@ -76,6 +76,7 @@ sig
 
   val guards : frame -> pred list
   val mem_frame : c_label -> sigma
+  val has_at_frame : frame -> c_label -> bool
   val mem_at_frame : frame -> c_label -> sigma
   val set_at_frame : frame -> c_label -> sigma -> unit
 

src/plugins/wp/LogicSemantics.ml

@@ -63,6 +63,7 @@ struct
   let mk_frame = C.mk_frame
   let in_frame = C.in_frame
   let mem_frame = C.mem_frame
+  let has_at_frame = C.has_at_frame
   let mem_at_frame = C.mem_at_frame
   let set_at_frame = C.set_at_frame
   let mem_at = C.mem_at

src/plugins/wp/Pcond.ml

@@ -333,7 +333,7 @@ class engine (lang : #Plang.engine) =
 
 let is_nop = function None -> true | Some(_,upd) -> Bag.is_empty upd
 
-class sequence (lang : #state) =
+class seqengine (lang : #state) =
   object(self)
     inherit engine lang as super
 
@@ -440,7 +440,7 @@ class sequence (lang : #state) =
 
 let engine () =
   if Wp_parameters.has_dkey dkey_state then
-    ( new sequence (new state) :> engine )
+    ( new seqengine (new state) :> engine )
   else
     new engine (new Plang.engine)
 
@@ -449,15 +449,18 @@ let pretty fmt seq =
 
 let () = Conditions.pretty := pretty
 
-let sequence ?(clause="Sequence") fmt seq =
+let dump_sequence ?(clause="Sequence") ?goal fmt seq =
   let plang = new Plang.engine in
   let pcond = new engine plang in
   plang#global
-    (fun () ->
-       Vars.iter (fun x -> ignore (plang#bind x)) (Conditions.vars_hyp seq) ;
-       pcond#pp_sequence ~clause fmt seq)
+    begin fun () ->
+      pcond#pp_block ~clause fmt seq ;
+      match goal with
+      | None -> ()
+      | Some g -> Format.fprintf fmt "@ @[<hov 2>Prove %a@]" plang#pp_pred g
+    end
 
-let bundle ?clause fmt bundle =
-  sequence ?clause fmt (Conditions.bundle bundle)
+let dump_bundle ?clause ?goal fmt bundle =
+  dump_sequence ?clause ?goal fmt (Conditions.bundle bundle)
 
-let dump = bundle ~clause:"Bundle"
+let dump = dump_bundle ?goal:None ~clause:"Bundle"

src/plugins/wp/Pcond.mli

@@ -23,16 +23,18 @@
 open Qed.Plib
 open Conditions
 
+open Lang.F
+
 (** {2 All-in-one printers} *)
 
-val dump : bundle printer
-val bundle : ?clause:string -> bundle printer
-val sequence : ?clause:string -> sequence printer
 val pretty : sequent printer
 
+val dump : bundle printer
+val dump_bundle : ?clause:string -> ?goal:pred -> bundle printer
+val dump_sequence : ?clause:string -> ?goal:pred -> sequence printer
+
 (** {2 Low-level API} *)
 
-open Lang.F
 type env = Plang.Env.t
 
 val alloc_hyp : Plang.pool -> (var -> unit) -> sequence -> unit
@@ -103,7 +105,7 @@ class state :
     method pp_value : Format.formatter -> term -> unit
   end
 
-class sequence : #state ->
+class seqengine : #state ->
   object
     inherit engine
     method set_sequence : Conditions.sequence -> unit

src/plugins/wp/Sigma.ml

@@ -115,15 +115,16 @@ struct
   let mem w c = H.Map.mem c w.map
 
   let join a b =
-    let p = ref Passive.empty in
-    H.Map.iter2
-      (fun chunk x y ->
-         match x,y with
-         | Some x , Some y -> p := Passive.join x y !p
-         | Some x , None -> b.map <- H.Map.add chunk x b.map
-         | None , Some y -> a.map <- H.Map.add chunk y a.map
-         | None , None -> ())
-      a.map b.map ; !p
+    if a == b then Passive.empty else
+      let p = ref Passive.empty in
+      H.Map.iter2
+        (fun chunk x y ->
+           match x,y with
+           | Some x , Some y -> p := Passive.join x y !p
+           | Some x , None -> b.map <- H.Map.add chunk x b.map
+           | None , Some y -> a.map <- H.Map.add chunk y a.map
+           | None , None -> ())
+        a.map b.map ; !p
 
   let assigned ~pre ~post written =
     let p = ref Bag.empty in

src/plugins/wp/Sigs.ml

@@ -658,6 +658,9 @@ sig
   (** Update a frame with a specific environment for the given label. *)
   val set_at_frame : frame -> Clabels.c_label -> sigma -> unit
 
+  (** Chek if a frame already has a specific envioronement for the given label. *)
+  val has_at_frame : frame -> Clabels.c_label -> bool
+
   (** Same as [mem_at_frame] but for the current frame. *)
   val mem_frame : Clabels.c_label -> sigma
 

src/plugins/wp/VCS.ml

@@ -317,31 +317,35 @@ let pp_result fmt r =
   | Stepout -> Format.fprintf fmt "Step limit%a" pp_perf r
   | Timeout -> Format.fprintf fmt "Timeout%a" pp_perf r
 
-let pp_cache_miss fmt st prover r =
-  let qualified =
-    match prover with
-    | Qed | Tactical -> true
-    | NativeAltErgo | NativeCoq -> r.verdict <> Timeout
-    | Why3 _ -> r.cached || r.prover_time < Rformat.epsilon
-  in
-  if not qualified && Wp_parameters.has_dkey dkey_shell then
-    Format.fprintf fmt "%s%a (unqualified)" st pp_perf r
+let is_qualified prover result =
+  match prover with
+  | Qed | Tactical -> true
+  | NativeAltErgo | NativeCoq -> result.verdict <> Timeout
+  | Why3 _ -> result.cached || result.prover_time < Rformat.epsilon
+
+let pp_cache_miss fmt st updating prover result =
+  if not updating
+  && not (is_qualified prover result)
+  && Wp_parameters.has_dkey dkey_shell
+  then
+    Format.fprintf fmt "%s%a (missing cache)" st pp_perf result
   else
-    Format.pp_print_string fmt (if is_valid r then "Valid" else "Unsuccess")
+    Format.pp_print_string fmt @@
+    if is_valid result then "Valid" else "Unsuccess"
 
-let pp_result_qualif prover fmt r =
+let pp_result_qualif ?(updating=true) prover result fmt =
   if Wp_parameters.has_dkey dkey_shell then
-    match r.verdict with
+    match result.verdict with
     | NoResult -> Format.pp_print_string fmt "No Result"
     | Computing _ -> Format.pp_print_string fmt "Computing"
     | Invalid -> Format.pp_print_string fmt "Invalid"
-    | Failed -> Format.fprintf fmt "Failed@ %s" r.prover_errmsg
-    | Valid -> pp_cache_miss fmt "Valid" prover r
-    | Unknown -> pp_cache_miss fmt "Unsuccess" prover r
-    | Timeout -> pp_cache_miss fmt "Timeout" prover r
-    | Stepout -> pp_cache_miss fmt "Stepout" prover r
+    | Failed -> Format.fprintf fmt "Failed@ %s" result.prover_errmsg
+    | Valid -> pp_cache_miss fmt "Valid" updating prover result
+    | Unknown -> pp_cache_miss fmt "Unsuccess" updating prover result
+    | Timeout -> pp_cache_miss fmt "Timeout" updating prover result
+    | Stepout -> pp_cache_miss fmt "Stepout" updating prover result
   else
-    pp_result fmt r
+    pp_result fmt result
 
 let compare p q =
   let rank = function

src/plugins/wp/VCS.mli

@@ -119,7 +119,8 @@ val configure : result -> config
 val autofit : result -> bool (** Result that fits the default configuration *)
 
 val pp_result : Format.formatter -> result -> unit
-val pp_result_qualif : prover -> Format.formatter -> result -> unit
+val pp_result_qualif : ?updating:bool -> prover -> result ->
+  Format.formatter -> unit
 
 val compare : result -> result -> int (* best is minimal *)
 val merge : result -> result -> result

src/plugins/wp/calculus.ml

@@ -495,9 +495,8 @@ module Cfg (W : Mcfg.S) = struct
        | Mcfg.SC_Global -> "global"
        | Mcfg.SC_Block_in -> "block in"
        | Mcfg.SC_Block_out -> "block out"
-       | Mcfg.SC_Function_in -> "function in"
-       | Mcfg.SC_Function_frame -> "function frame"
-       | Mcfg.SC_Function_out -> "function out" )
+       | Mcfg.SC_Frame_in -> "frame in"
+       | Mcfg.SC_Frame_out -> "frame out" )
       (Pretty_utils.pp_list  ~sep:", " Printer.pp_varinfo) vars;
     match scope with
     | Mcfg.(SC_Block_in | SC_Block_out) when vars = [] -> obj
@@ -564,13 +563,12 @@ module Cfg (W : Mcfg.S) = struct
           Wp_error.unsupported "strange CFGs."
       | Cil2cfg.VfctIn ->
           let obj = get_only_succ env cfg v in
-          let obj = wp_scope wenv formals Mcfg.SC_Function_in obj in
           let obj = wp_scope wenv [] Mcfg.SC_Global obj in
           obj
       | Cil2cfg.VblkIn (Cil2cfg.Bfct, b) ->
           let obj = get_only_succ env cfg v in
           let obj = wp_scope wenv b.blocals Mcfg.SC_Block_in obj in
-          let obj = wp_scope wenv formals Mcfg.SC_Function_frame obj in
+          let obj = wp_scope wenv formals Mcfg.SC_Frame_in obj in
           obj
       | Cil2cfg.VblkOut (Cil2cfg.Bfct, b) ->
           let obj = get_only_succ env cfg v in
@@ -601,10 +599,9 @@ module Cfg (W : Mcfg.S) = struct
       | Cil2cfg.Vloop _ | Cil2cfg.Vloop2 _ ->
           let get_loop_head = fun n -> get_only_succ env cfg n in
           wp_loop env v e get_loop_head
-      | Cil2cfg.VfctOut
-      | Cil2cfg.Vexit ->
+      | Cil2cfg.VfctOut | Cil2cfg.VfctErr ->
           let obj = get_only_succ env cfg v (* exitpost / postcondition *) in
-          wp_scope wenv formals Mcfg.SC_Function_out obj
+          wp_scope wenv formals Mcfg.SC_Frame_out obj
       | Cil2cfg.Vend ->
           W.empty
           (* LC : unused entry point...

src/plugins/wp/cfgDump.ml

@@ -121,6 +121,7 @@ struct
   let add_assigns env (pid,_) k =
     let u = node () in
     Format.fprintf !out "  %a [ color=red , label=\"Assigns %a\" ] ;@." pretty u WpPropId.pp_propid pid ;
+    Format.fprintf !out "  %a -> %a [ style=dotted ] ;@." pretty u pretty k ;
     merge env u k
 
   let use_assigns _env _stmt region d k =
@@ -215,7 +216,9 @@ struct
             (fun (_,p) -> Format.fprintf fmt "\n@[<hov 2>Requires %a ;@]"
                 Printer.pp_predicate p) pre
       end ;
-    ignore pre ; merge env u k
+    ignore pre ;
+    Format.fprintf !out "  %a -> %a [ style=dotted ] ;@." pretty u pretty k ;
+    merge env u k
 
   let call env stmt _r kf _es ~pre ~post ~pexit ~assigns ~p_post ~p_exit =
     let u_post = List.fold_right (add_hyp env) post p_post in
@@ -231,9 +234,8 @@ struct
   let pp_scope sc fmt xs =
     let title = match sc with
       | Mcfg.SC_Global -> "Global"
-      | Mcfg.SC_Function_in -> "F-in"
-      | Mcfg.SC_Function_frame -> "F-frame"
-      | Mcfg.SC_Function_out -> "F-out"
+      | Mcfg.SC_Frame_in -> "F-in"
+      | Mcfg.SC_Frame_out -> "F-out"
       | Mcfg.SC_Block_in -> "B-in"
       | Mcfg.SC_Block_out -> "B-out"
     in begin

src/plugins/wp/cfgWP.ml

@@ -101,6 +101,10 @@ struct
   struct
     type t = effect
     let compare e1 e2 = P.compare e1.e_pid e2.e_pid
+    let pretty fmt e =
+      Format.fprintf fmt "@[<hov 2>EFFECT %a:@ %a@]"
+        P.pretty e.e_pid (Cvalues.pp_region M.pretty) e.e_region
+    [@@ warning "-32"]
   end
 
   module G = Qed.Collection.Make(TARGET)
@@ -140,9 +144,8 @@ struct
   (* -------------------------------------------------------------------------- *)
 
   let pp_vc fmt vc =
-    Format.fprintf fmt "%a@ @[<hov 2>Prove %a@]"
-      Pcond.dump vc.hyps
-      F.pp_pred vc.goal
+    Format.fprintf fmt "%a"
+      (Pcond.dump_bundle ~clause:"Context" ~goal:vc.goal) vc.hyps
 
   let pp_vcs fmt vcs =
     let k = ref 0 in
@@ -250,10 +253,6 @@ struct
       (fun vc (warn,hyp) -> assume_vc ?descr ?filter ?init ~warn [hyp] vc)
       vc whs
 
-  let passify_vc pa vc =
-    let hs = Passive.conditions pa (occurs_vc vc) in
-    assume_vc hs vc
-
   (* -------------------------------------------------------------------------- *)
   (* --- Branching                                                          --- *)
   (* -------------------------------------------------------------------------- *)
@@ -362,6 +361,14 @@ struct
       (fun g -> Splitter.merge_all merge_vcs (List.map (goal g) cases))
       targets
 
+  let passify_vc pa vc =
+    let hs = Passive.conditions pa (occurs_vc vc) in
+    assume_vc hs vc
+
+  let passify_vcs pa vcs =
+    if Passive.is_empty pa then vcs
+    else gmap (passify_vc pa) vcs
+
   (* -------------------------------------------------------------------------- *)
   (* --- Merge for Calculus                                                 --- *)
   (* -------------------------------------------------------------------------- *)
@@ -383,8 +390,8 @@ struct
       (fun () ->
          let sigma,pa1,pa2 = merge_sigma wp1.sigma wp2.sigma in
          let effects = Eset.union wp1.effects wp2.effects in
-         let vcs1 = gmap (passify_vc pa1) wp1.vcs in
-         let vcs2 = gmap (passify_vc pa2) wp2.vcs in
+         let vcs1 = passify_vcs pa1 wp1.vcs in
+         let vcs2 = passify_vcs pa2 wp2.vcs in
          let vcs = gmerge vcs1 vcs2 in
          { sigma = sigma ; vcs = vcs ; effects = effects }
       ) ()
@@ -651,15 +658,20 @@ struct
     if Clabels.is_here label then wp else
       in_wenv wenv wp
         (fun env wp ->
+           let frame = L.get_frame () in
            let s_here = L.current env in
-           let s_labl = L.mem_frame label in
-           let pa = Sigma.join s_here s_labl in
+           let s_frame =
+             if L.has_at_frame frame label then
+               L.mem_at_frame frame label
+             else
+               (L.set_at_frame frame label s_here ; s_here) in
+           let pa = Sigma.join s_here s_frame in
            let stop,effects = Eset.partition (is_stopeffect label) wp.effects in
            let vcs = Gmap.filter (not_posteffect stop) wp.vcs in
-           let vcs = gmap (passify_vc pa) vcs in
+           let vcs = passify_vcs pa vcs in
            let vcs = check_nothing stop vcs in
            let vcs = state_vcs stmt s_here vcs in
-           { sigma = Some s_here ; vcs=vcs ; effects=effects })
+           { sigma = Some s_frame ; vcs=vcs ; effects=effects })
 
   (* -------------------------------------------------------------------------- *)
   (* --- WP RULE : assignation                                              --- *)
@@ -806,8 +818,8 @@ struct
                   Some (Splitter.union (merge_vc) s1 s2)
                ) vcs1 vcs2
            else
-             let vcs1 = gmap (passify_vc pa1) wp1.vcs in
-             let vcs2 = gmap (passify_vc pa2) wp2.vcs in
+             let vcs1 = passify_vcs pa1 wp1.vcs in
+             let vcs2 = passify_vcs pa2 wp2.vcs in
              gbranch
                ~left:(assume_vc ~descr:"Then" ~stmt ~warn [cond])
                ~right:(assume_vc ~descr:"Else" ~stmt ~warn [p_not cond])
@@ -1044,6 +1056,7 @@ struct
     let seq_post = cc_havoc dom_call seq_result.pre in
     let seq_exit = cc_havoc dom_call (sigma_at wexit) in
     (* Pre-State *)
+    (* Passive: joined later by call_proper *)
     let sigma_pre, _, _ = Sigma.merge seq_post.pre seq_exit.pre in
     let formals = List.map (C.exp sigma_pre) es in
     let call = L.call kf formals in
@@ -1200,11 +1213,10 @@ struct
             let hs = M.frame (L.current env) in
             let vcs = gmap (assume_vc ~descr:"Heap" ~domain:true hs) wp.vcs in
             { wp with vcs }
-        | Mcfg.SC_Function_in -> wp
-        | Mcfg.SC_Function_frame ->
-            wp_scope env wp ~descr:"Function Frame" Enter xs
-        | Mcfg.SC_Function_out ->
-            wp_scope env wp ~descr:"Function Exit" Leave xs
+        | Mcfg.SC_Frame_in ->
+            wp_scope env wp ~descr:"Frame In" Enter xs
+        | Mcfg.SC_Frame_out ->
+            wp_scope env wp ~descr:"Frame Out" Leave xs
         | Mcfg.SC_Block_in ->
             wp_scope env wp ~descr:"Block In" Enter xs
         | Mcfg.SC_Block_out ->

src/plugins/wp/cil2cfg.ml

@@ -48,8 +48,8 @@ let pp_call_type fmt = function
   | Static kf -> Kernel_function.pretty fmt kf
 
 type node_type =
-  | Vstart | Vend | Vexit
-  | VfctIn | VfctOut (* TODO : not useful anymore -> Bfct *)
+  | Vstart | Vend
+  | VfctIn | VfctOut | VfctErr
   | VblkIn of block_type * block
   | VblkOut of block_type * block
   | Vstmt of stmt
@@ -82,7 +82,7 @@ let node_type_id t : node_id = match t with
   | Vstart -> (0, 0)
   | VfctIn -> (0, 1)
   | VfctOut -> (0, 2)
-  | Vexit -> (0, 3)
+  | VfctErr -> (0, 3)
   | Vend -> (0, 4)
   | Vstmt s | Vtest (true, s, _) | Vswitch (s,_) | Vcall (s, _, _, _) ->
       (1, s.sid)
@@ -113,8 +113,8 @@ let pp_node_type fmt n = match n with
   | Vstart -> Format.fprintf fmt "<start>"
   | VfctIn -> Format.fprintf fmt "<fctIn>"
   | VfctOut -> Format.fprintf fmt "<fctOut>"
+  | VfctErr -> Format.fprintf fmt "<fctErr>"
   | Vend -> Format.fprintf fmt "<end>"
-  | Vexit -> Format.fprintf fmt "<exit>"
   | VblkIn (bk,_) -> Format.fprintf fmt "<blkIn-%a>" pp_bkind bk
   | VblkOut (bk,_) -> Format.fprintf fmt "<blkOut-%a>" pp_bkind bk
   | Vcall (s, _, _, _) -> Format.fprintf fmt "<callIn-%d>" s.sid
@@ -146,7 +146,7 @@ let pp_node fmt v = VL.pretty fmt v
 
 let start_stmt_of_node v = match node_type v with
   | Vstart | Vtest (false, _, _) | VblkOut _
-  | VfctIn | VfctOut | Vend | Vexit | Vloop2 _ -> None
+  | VfctIn | VfctOut | VfctErr | Vend | Vloop2 _ -> None
   | VblkIn (bk, _) -> bkind_stmt bk
   | Vstmt s | Vtest (true, s, _) | Vloop (_, s) | Vswitch (s,_)
   | Vcall (s, _, _, _)
@@ -154,7 +154,7 @@ let start_stmt_of_node v = match node_type v with
 
 let node_stmt_opt v = match node_type v with
   | Vstart | Vtest (false, _, _)
-  | VfctIn | VfctOut | Vend | Vexit | Vloop2 _ -> None
+  | VfctIn | VfctOut | VfctErr | Vend | Vloop2 _ -> None
   | VblkIn (bk, _) | VblkOut (bk, _) -> bkind_stmt bk
   | Vstmt s | Vtest (true, s, _) | Vloop (_, s) | Vswitch (s,_)
   | Vcall (s, _, _, _)
@@ -479,14 +479,14 @@ let get_call_out_edges cfg v =
   in
   let en, ee = match node_type (edge_dst e1) ,
                      node_type (edge_dst e2) with
-  | _,  Vexit -> e1, e2
-  | Vexit, _  -> e2, e1
+  | _,  VfctErr -> e1, e2
+  | VfctErr, _  -> e2, e1
   | _, _ -> assert false
   in en, ee
 
 let get_edge_stmt e =
   match node_type (edge_dst e) with
-  | Vstart | VfctIn | Vexit | VfctOut -> None
+  | Vstart | VfctIn | VfctOut | VfctErr -> None
   | VblkIn (Bstmt s, _) | Vstmt s
   | Vcall (s,_,_,_) | Vtest (true, s, _) | Vswitch (s,_) -> Some s
   | Vloop (_,s) -> if is_back_edge e then None else Some s
@@ -497,7 +497,7 @@ let get_edge_labels e =
   let l = match node_type v_after with
     | Vstart -> assert false
     | VfctIn -> []
-    | Vexit | VfctOut -> [Clabels.post]
+    | VfctErr | VfctOut -> [Clabels.post]
     | VblkIn (Bstmt s, _)
     | Vcall (s,_,_,_) | Vstmt s | Vtest (true, s, _) | Vswitch (s,_) ->
         [Clabels.stmt s]
@@ -556,7 +556,7 @@ let get_exit_edges cfg src =
     let add_exit e acc =
       let dst = edge_dst e in
       match node_type dst with
-      | Vexit ->
+      | VfctErr ->
           debug
             "[get_exit_edges] add %a@." pp_edge e;
           (* (succ_e cfg dst) @ acc *)
@@ -660,12 +660,12 @@ let block_scope_for_edge cfg e =
   | VblkIn(Bstmt _,b) -> { b_opened=[b] ; b_closed=[] }
   | Vcall _
   | VblkIn _ | VblkOut _ | Vtest(false,_,_)
-  | VfctIn | VfctOut | Vstart | Vend | Vexit | Vloop2 _ ->
+  | VfctIn | VfctOut | VfctErr | Vstart | Vend | Vloop2 _ ->
       no_scope
 
 let has_exit cfg =
   try
-    let node = Hashtbl.find cfg.stmt_node (node_type_id Vexit) in
+    let node = Hashtbl.find cfg.stmt_node (node_type_id VfctErr) in
     match pred_e cfg node with
     | [] -> false
     | _ -> true
@@ -758,10 +758,10 @@ let init_cfg spec_only kf =
   let fct_in =  add_node env (VfctIn) in
   let _ = add_edge env start Enone fct_in in
   let fct_out =  add_node env (VfctOut) in
-  let nexit =  add_node env (Vexit) in
+  let fct_err =  add_node env (VfctErr) in
   let nend =  add_node env (Vend) in
   let _ = add_edge env fct_out Enone nend in
-  let _ = add_edge env nexit Enone nend in
+  let _ = add_edge env fct_err Enone nend in
   env, fct_in, fct_out
 
 let get_node env t =
@@ -883,7 +883,7 @@ and cfg_stmt env s next =
       setup_preconditions_proxies f;
       let in_call = get_stmt_node env s in
       add_edge env in_call Enone next;
-      let exit_node = get_node env (Vexit) in
+      let exit_node = get_node env VfctErr in
       add_edge env in_call Enone exit_node;
       in_call
   | Instr (Local_init(_,ConsInit (f, _, _), _)) ->
@@ -891,7 +891,7 @@ and cfg_stmt env s next =
       Statuses_by_call.setup_all_preconditions_proxies kf;
       let in_call = get_stmt_node env s in
       add_edge env in_call Enone next;
-      let exit_node = get_node env Vexit in
+      let exit_node = get_node env VfctErr in
       add_edge env in_call Enone exit_node;
       in_call
   | Instr _  | Return _ ->

src/plugins/wp/cil2cfg.mli

@@ -70,8 +70,8 @@ val pp_call_type : Format.formatter -> call_type -> unit
 val get_call_type : exp -> call_type
 
 type node_type = private
-  | Vstart | Vend | Vexit
-  | VfctIn | VfctOut
+  | Vstart | Vend
+  | VfctIn | VfctOut | VfctErr
   | VblkIn of block_type * block
   | VblkOut of block_type * block
   | Vstmt of stmt

src/plugins/wp/mcfg.ml

@@ -24,9 +24,8 @@ open Cil_types
 
 type scope =
   | SC_Global
-  | SC_Function_in    (* Just before the pre-state *)
-  | SC_Function_frame (* Just after the introduction of formals *)
-  | SC_Function_out   (* Post-state *)
+  | SC_Frame_in
+  | SC_Frame_out
   | SC_Block_in
   | SC_Block_out
 

src/plugins/wp/register.ml

@@ -391,19 +391,21 @@ let results g =
     (Wpo.get_results g)
 
 let do_wpo_failed goal =
+  let updating = Cache.is_updating () in
   match results goal with
   | [p,r] ->
-      Wp_parameters.result "[%a] Goal %s : %a%a"
+      Wp_parameters.result "[%a] Goal %s : %t%a"
         VCS.pp_prover p (Wpo.get_gid goal)
-        (VCS.pp_result_qualif p) r pp_warnings goal
+        (VCS.pp_result_qualif ~updating p r) pp_warnings goal
   | pres ->
       Wp_parameters.result "[Failed] Goal %s%t" (Wpo.get_gid goal)
         begin fun fmt ->
           pp_warnings fmt goal ;
           List.iter
             (fun (p,r) ->
-               Format.fprintf fmt "@\n%8s: @[<hv>%a@]"
-                 (VCS.title_of_prover p) (VCS.pp_result_qualif p) r
+               Format.fprintf fmt "@\n%8s: @[<hv>%t@]"
+                 (VCS.title_of_prover p)
+                 (VCS.pp_result_qualif ~updating p r)
             ) pres ;
         end
 
@@ -416,11 +418,12 @@ let do_wpo_smoke status goal =
     (Wpo.get_gid goal)
     begin fun fmt ->
       pp_warnings fmt goal ;
+      let updating = Cache.is_updating () in
       List.iter
         (fun (p,r) ->
-           Format.fprintf fmt "@\n%8s: @[<hv>%a@]"
+           Format.fprintf fmt "@\n%8s: @[<hv>%t@]"
              (VCS.title_of_prover p)
-             (VCS.pp_result_qualif p) r
+             (VCS.pp_result_qualif ~updating p r)
         ) (results goal) ;
     end
 
@@ -453,10 +456,11 @@ let do_wpo_success goal s =
             VCS.pp_prover script (Wpo.get_gid goal)
       | Some prover ->
           let result = Wpo.get_result goal prover in
+          let updating = Cache.is_updating () in
           Wp_parameters.feedback ~ontty:`Silent
-            "[%a] Goal %s : %a"
+            "[%a] Goal %s : %t"
             VCS.pp_prover prover (Wpo.get_gid goal)
-            (VCS.pp_result_qualif prover) result
+            (VCS.pp_result_qualif ~updating prover result)
     end
 
 let do_report_time fmt s =

src/plugins/wp/tests/wp/oracle_qualif/cfg_loop.res.oracle

 # frama-c -wp [...]
 [kernel] Parsing tests/wp/cfg_loop.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 15 goals scheduled
 [wp] [Qed] Goal typed_loop_continue_loop_invariant_preserved : Valid