diff --git a/src/kernel_services/ast_printing/description.ml b/src/kernel_services/ast_printing/description.ml
index 4dbb21c9455022dfd23d5cc4c152f3210b83bf30..a0a4d8a5f593408da8aff26db007b1dad4f83a4d 100644
--- a/src/kernel_services/ast_printing/description.ml
+++ b/src/kernel_services/ast_printing/description.ml
@@ -33,14 +33,14 @@ let pp_opt doit pp fmt x = if doit then pp fmt x
let goto_stmt stmt =
let rec goto_label = function
| [] -> Printf.sprintf "s%04d" stmt.sid
- | Label(a,_,true)::_ -> a
+ | Label(a,_,true)::_ -> a
| _::labels -> goto_label labels
in goto_label stmt.labels
let rec stmt_labels = function
| Label(a,_,true) :: ls -> a :: stmt_labels ls
| Label _ :: ls -> stmt_labels ls
- | Case(e,_) :: ls ->
+ | Case(e,_) :: ls ->
let cvalue = (Cil.constFold true e) in
Format.asprintf "case %a" Printer.pp_exp cvalue
:: stmt_labels ls
@@ -55,20 +55,20 @@ let pp_labels fmt stmt =
let pp_idpred kloc fmt idpred =
let np = idpred.ip_content in
- if np.pred_name <> []
+ if np.pred_name <> []
then Format.fprintf fmt " '%s'" (String.concat "," np.pred_name)
else pp_kloc kloc fmt np.pred_loc
let pp_allocation kloc fmt (allocation:identified_term list) =
if allocation = [] then Format.fprintf fmt "nothing"
else
- let names =
+ let names =
List.fold_left
(fun names x -> names @ x.it_content.term_name)
[] allocation in
match names with
| [] ->
- if kloc then
+ if kloc then
let x = List.hd allocation in
Format.fprintf fmt "(%a)" pp_loc x.it_content.term_loc
else Format.fprintf fmt "..."
@@ -78,13 +78,13 @@ let pp_allocation kloc fmt (allocation:identified_term list) =
let pp_region kloc fmt (region:from list) =
if region = [] then Format.fprintf fmt "nothing"
else
- let names =
+ let names =
List.fold_left
(fun names (x,_) -> names @ x.it_content.term_name)
[] region in
match names with
| [] ->
- if kloc then
+ if kloc then
let x = fst (List.hd region) in
Format.fprintf fmt "(%a)" pp_loc x.it_content.term_loc
else Format.fprintf fmt "..."
@@ -92,7 +92,7 @@ let pp_region kloc fmt (region:from list) =
Format.fprintf fmt "'%s'" (String.concat "," names)
let pp_bhv fmt bhv =
- if not (Cil.is_default_behavior bhv) then
+ if not (Cil.is_default_behavior bhv) then
Format.fprintf fmt " for '%s'" bhv.b_name
let pp_bhvs fmt = function
@@ -113,7 +113,7 @@ let pp_named fmt nx =
let pp_code_annot fmt ca =
match ca.annot_content with
| AAssert(bs,np) -> Format.fprintf fmt "assertion%a%a" pp_for bs pp_named np
- | AInvariant(bs,_,np) ->
+ | AInvariant(bs,_,np) ->
Format.fprintf fmt "invariant%a%a" pp_for bs pp_named np
| AAssigns(bs,_) -> Format.fprintf fmt "assigns%a" pp_for bs
| AAllocation(bs,_) -> Format.fprintf fmt "allocates_frees%a" pp_for bs
@@ -126,9 +126,9 @@ let pp_stmt kloc fmt stmt =
match stmt.skind with
| Instr (Local_init (v,_,loc)) ->
Format.fprintf fmt "initialization of '%s'%a" v.vname (pp_kloc kloc) loc
- | Instr (Call(_,{enode=Lval(Var v,_)},_,loc)) ->
+ | Instr (Call(_,{enode=Lval(Var v,_)},_,loc)) ->
Format.fprintf fmt "call '%s'%a" v.vname (pp_kloc kloc) loc
- | Instr (Set(_,_,loc)|Call(_,_,_,loc)) ->
+ | Instr (Set(_,_,loc)|Call(_,_,_,loc)) ->
Format.fprintf fmt "instruction%a" (pp_kloc kloc) loc
| Instr (Asm(_,_,_,loc)) ->
Format.fprintf fmt "assembly%a%a" pp_labels stmt (pp_kloc kloc) loc
@@ -146,7 +146,7 @@ let pp_stmt kloc fmt stmt =
| Block _ -> Format.fprintf fmt "block%a" pp_labels stmt
| UnspecifiedSequence _ -> Format.fprintf fmt "instruction%a" pp_labels stmt
| Throw(_,loc) -> Format.fprintf fmt "throw%a" (pp_kloc kloc) loc
- | TryFinally(_,_,loc) | TryExcept(_,_,_,loc) | TryCatch(_,_,loc)->
+ | TryFinally(_,_,loc) | TryExcept(_,_,_,loc) | TryCatch(_,_,loc)->
Format.fprintf fmt "try-catch%a" (pp_kloc kloc) loc
let pp_stmt_loc kloc fmt s = Format.fprintf fmt " at %a" (pp_stmt kloc) s
@@ -155,9 +155,9 @@ let pp_kinstr kloc fmt = function
| Kglobal -> () | Kstmt s -> pp_stmt_loc kloc fmt s
let pp_predicate fmt = function
- | PKRequires bhv ->
+ | PKRequires bhv ->
Format.fprintf fmt "Pre-condition%a" pp_bhv bhv
- | PKAssumes bhv ->
+ | PKAssumes bhv ->
Format.fprintf fmt "Assumption%a" pp_bhv bhv
| PKEnsures(bhv,Normal) ->
Format.fprintf fmt "Post-condition%a" pp_bhv bhv
@@ -206,8 +206,10 @@ let pp_active fmt active =
~pre:" under active behaviors" ~sep:"," Format.pp_print_string fmt
(Datatype.String.Set.elements active)
-let pp_acsl_extension fmt (_,s,_,_) =
- Format.fprintf fmt "%s" s
+let pp_capitalize fmt s =
+ Format.pp_print_string fmt (Transitioning.String.capitalize_ascii s)
+
+let pp_acsl_extension fmt (_,s,_,_) = pp_capitalize fmt s
let rec pp_prop kfopt kiopt kloc fmt = function
| IPAxiom (s,_,_,_,_) -> Format.fprintf fmt "Axiom '%s'" s
@@ -216,16 +218,16 @@ let rec pp_prop kfopt kiopt kloc fmt = function
| IPGlobalInvariant (s,_,_) -> Format.fprintf fmt "Global invariant '%s'" s
| IPAxiomatic (s,_) -> Format.fprintf fmt "Axiomatic '%s'" s
| IPOther(s,le) ->
- Format.fprintf fmt "%s%a" s (pp_other_loc kfopt kiopt kloc) le
+ Format.fprintf fmt "%a%a" pp_capitalize s (pp_other_loc kfopt kiopt kloc) le
| IPPredicate(kind,kf,Kglobal,idpred) ->
- Format.fprintf fmt "%a%a%a"
- pp_predicate kind
- (pp_idpred kloc) idpred
+ Format.fprintf fmt "%a%a%a"
+ pp_predicate kind
+ (pp_idpred kloc) idpred
(pp_context kfopt) (Some kf)
| IPPredicate(kind,_,ki,idpred) ->
- Format.fprintf fmt "%a%a%a"
- pp_predicate kind
- (pp_idpred kloc) idpred
+ Format.fprintf fmt "%a%a%a"
+ pp_predicate kind
+ (pp_idpred kloc) idpred
(pp_kinstr kloc) ki
| IPExtended(le,(_,_,loc,_ as pred)) ->
Format.fprintf fmt "%a%a"
@@ -236,67 +238,67 @@ let rec pp_prop kfopt kiopt kloc fmt = function
Format.fprintf fmt "Default behavior%a%a"
(pp_opt kiopt (pp_kinstr kloc)) ki (pp_opt kiopt pp_active) active
else
- Format.fprintf fmt "Behavior '%s'%a"
+ Format.fprintf fmt "Behavior '%s'%a"
bhv.b_name
(pp_opt kiopt (pp_kinstr kloc)) ki
| IPComplete(_,ki,active, bs) ->
- Format.fprintf fmt "Complete behaviors%a%a%a"
+ Format.fprintf fmt "Complete behaviors%a%a%a"
pp_bhvs bs
(pp_opt kiopt (pp_kinstr kloc)) ki (pp_opt kiopt pp_active) active
| IPDisjoint(_,ki,active, bs) ->
- Format.fprintf fmt "Disjoint behaviors%a%a%a"
+ Format.fprintf fmt "Disjoint behaviors%a%a%a"
pp_bhvs bs
(pp_opt kiopt (pp_kinstr kloc)) ki
(pp_opt kiopt pp_active) active
| IPCodeAnnot(_,_,{annot_content=AAssert(bs,np)}) ->
- Format.fprintf fmt "Assertion%a%a%a"
- pp_for bs
- pp_named np
+ Format.fprintf fmt "Assertion%a%a%a"
+ pp_for bs
+ pp_named np
(pp_kloc kloc) np.pred_loc
| IPCodeAnnot(_,_,{annot_content=AInvariant(bs,_,np)}) ->
- Format.fprintf fmt "Invariant%a%a%a"
- pp_for bs
- pp_named np
+ Format.fprintf fmt "Invariant%a%a%a"
+ pp_for bs
+ pp_named np
(pp_kloc kloc) np.pred_loc
| IPCodeAnnot(_,stmt,_) ->
Format.fprintf fmt "Annotation %a" (pp_stmt kloc) stmt
| IPAllocation(kf,Kglobal,Id_contract (_,bhv),(frees,allocates)) ->
- Format.fprintf fmt "Frees/Allocates%a %a/%a %a"
- pp_bhv bhv
+ Format.fprintf fmt "Frees/Allocates%a %a/%a %a"
+ pp_bhv bhv
(pp_allocation kloc) frees
(pp_allocation kloc) allocates
(pp_context kfopt) (Some kf)
| IPAssigns(kf,Kglobal,Id_contract(_, bhv),region) ->
- Format.fprintf fmt "Assigns%a %a%a"
- pp_bhv bhv
- (pp_region kloc) region
- (pp_context kfopt) (Some kf)
+ Format.fprintf fmt "Assigns%a %a%a"
+ pp_bhv bhv
+ (pp_region kloc) region
+ (pp_context kfopt) (Some kf)
| IPFrom (kf,Kglobal,Id_contract(_,bhv),depend) ->
Format.fprintf fmt "Froms%a %a%a"
- pp_bhv bhv
- (pp_region kloc) [depend]
- (pp_context kfopt) (Some kf)
+ pp_bhv bhv
+ (pp_region kloc) [depend]
+ (pp_context kfopt) (Some kf)
| IPAllocation(_,ki,Id_contract (active,bhv),(frees,allocates)) ->
- Format.fprintf fmt "Frees/Allocates%a %a/%a %a%a"
- pp_bhv bhv
+ Format.fprintf fmt "Frees/Allocates%a %a/%a %a%a"
+ pp_bhv bhv
(pp_allocation kloc) frees
(pp_allocation kloc) allocates
(pp_opt kiopt (pp_kinstr kloc)) ki
(pp_opt kiopt pp_active) active
| IPAssigns(_,ki,Id_contract (active,bhv),region) ->
Format.fprintf fmt "Assigns%a %a%a%a"
- pp_bhv bhv
- (pp_region kloc) region
+ pp_bhv bhv
+ (pp_region kloc) region
(pp_opt kiopt (pp_kinstr kloc)) ki
(pp_opt kiopt pp_active) active
| IPFrom (_,ki,Id_contract (active,bhv),depend) ->
- Format.fprintf fmt "Froms%a %a%a%a"
- pp_bhv bhv
- (pp_region kloc) [depend]
+ Format.fprintf fmt "Froms%a %a%a%a"
+ pp_bhv bhv
+ (pp_region kloc) [depend]
(pp_opt kiopt (pp_kinstr kloc)) ki
(pp_opt kiopt pp_active) active
| IPAllocation(_,_,Id_loop _,(frees,allocates)) ->
- Format.fprintf fmt "Loop frees%a Loop allocates%a"
+ Format.fprintf fmt "Loop frees%a Loop allocates%a"
(pp_allocation kloc) frees
(pp_allocation kloc) allocates
| IPAssigns(_,_,Id_loop _,region) ->
@@ -307,14 +309,14 @@ let rec pp_prop kfopt kiopt kloc fmt = function
Format.fprintf fmt "Recursion variant"
| IPDecrease(_,Kstmt stmt,_,_) ->
Format.fprintf fmt "Loop variant at %a" (pp_stmt kloc) stmt
- | IPReachable (None, Kglobal, Before) ->
+ | IPReachable (None, Kglobal, Before) ->
(* print "Unreachable": it seems that it is what the user want to see *)
Format.fprintf fmt "Unreachable entry point"
| IPReachable (None, Kglobal, After)
| IPReachable (None, Kstmt _, _) -> assert false
| IPReachable (Some _, Kstmt stmt, ba) ->
(* print "Unreachable": it seems that it is what the user want to see *)
- Format.fprintf fmt "Unreachable %a%s"
+ Format.fprintf fmt "Unreachable %a%s"
(pp_stmt kloc) stmt
(match ba with Before -> "" | After -> " (after it)")
| IPReachable (Some kf, Kglobal, _) ->
@@ -447,8 +449,8 @@ let kind_order = function
| PKTerminates -> [I 8]
let named_order xs = List.map (fun x -> S x) xs
-let for_order k = function
- | [] -> [I k]
+let for_order k = function
+ | [] -> [I k]
| bs -> I (succ k) :: named_order bs
let annot_order = function
| {annot_content=AAssert(bs,np)} ->
@@ -459,7 +461,7 @@ let annot_order = function
let loop_order = function
| Id_contract (active,b) -> [B b; A active]
| Id_loop _ -> []
-
+
let rec ip_order = function
| IPAxiomatic(a,_) -> [I 0;S a]
| IPAxiom(a,_,_,_,_) | IPLemma(a,_,_,_,_) -> [I 1;S a]
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index 83d95408e127e211c2446b2bccb844ec58468ac5..b51600c0725802af5fd4ce24b2f660c4a42e6f42 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -220,8 +220,6 @@ struct
| Some s -> S.add s vc.path in
let deps = match hpid with
| None -> [] | Some p -> [WpPropId.property_of_id p] in
- let descr = match hpid with
- | None -> descr | Some _ -> None in
let dset = List.fold_right D.add deps vc.deps in
let wrns = match warn with
| None -> vc.warn
@@ -461,7 +459,6 @@ struct
let add_hyp wenv (hpid,predicate) wp = in_wenv wenv wp
(fun env wp ->
- let descr = Pretty_utils.to_string WpPropId.pretty hpid in
let outcome = Warning.catch
~severe:false ~effect:"Skip hypothesis"
(L.pred `Negative env) predicate in
@@ -469,7 +466,7 @@ struct
| Warning.Result(warn,p) -> warn , [p]
| Warning.Failed warn -> warn , []
in
- let vcs = gmap (assume_vc ~hpid ~descr ~warn hs) wp.vcs in
+ let vcs = gmap (assume_vc ~hpid ~warn hs) wp.vcs in
{ wp with vcs = vcs })
let add_goal wenv (gpid,predicate) wp = in_wenv wenv wp
@@ -857,22 +854,20 @@ struct
(fun env wp ->
let shere = L.current env in
let sinit = L.mem_at env Clabels.init in
- let hyp = C.unchanged shere sinit v in
- let filter = true in
- let init = true in
- let descr = "Global Constant" in
- let vcs = gmap (assume_vc ~filter ~init ~descr [hyp]) wp.vcs in
- { wp with vcs = vcs })
+ let const_vc = assume_vc
+ ~init:true ~filter:true
+ ~descr:"Global Constant"
+ [C.unchanged shere sinit v]
+ in { wp with vcs = gmap const_vc wp.vcs })
let init wenv var init wp = in_wenv wenv wp
(fun env wp ->
let sigma = L.current env in
- let hyps = C.init ~sigma var init in
- let filter = true in
- let init = true in
- let descr = "Initializer" in
- let vcs = gmap (assume_vcs ~filter ~init ~descr hyps) wp.vcs in
- { wp with vcs = vcs })
+ let init_vc = assume_vcs
+ ~init:true ~filter:true
+ ~descr:"Initializer"
+ (C.init ~sigma var init)
+ in { wp with vcs = gmap init_vc wp.vcs })
(* -------------------------------------------------------------------------- *)
(* --- WP RULE : tag --- *)
@@ -885,48 +880,45 @@ struct
(* --- WP RULE : call dynamic --- *)
(* -------------------------------------------------------------------------- *)
- let call_instances sigma gpid fct calls vcs =
+ let call_pointer sigma fct =
let outcome = Warning.catch
~severe:true ~effect:"Degenerated goal"
(C.call sigma) fct in
- let warn,goal = match outcome with
- | Warning.Failed warn -> warn,F.p_false
- | Warning.Result(warn,floc) ->
- warn , F.p_any (C.instance_of floc) calls
+ match outcome with
+ | Warning.Failed warn -> warn,None
+ | Warning.Result(warn,floc) -> warn,Some floc
+
+ let call_instance_of gpid (warn,fopt) calls vcs =
+ let goal = match fopt with
+ | None -> F.p_false
+ | Some floc -> F.p_any (C.instance_of floc) calls
in add_vc (Gprop gpid) ~warn goal vcs
- let call_contract stmt sigma fptr (kf,wp) : vc Splitter.t Gmap.t =
+ let call_contract stmt sigma hpid (warn,fopt) (kf,wp) : vc Splitter.t Gmap.t =
let pa = join_with sigma wp.sigma in
let tag = Splitter.call stmt kf in
- let descr = Printf.sprintf "Instance of '%s'" (Kernel_function.get_name kf) in
- let instance_vc pa fptr vc =
- passify_vc pa
- begin match fptr with
- | None -> vc
- | Some(warn,floc) ->
- let hyp = C.instance_of floc kf in
- assume_vc ~stmt ~warn ~descr [hyp] vc
- end
+ let descr =
+ Printf.sprintf "Instance of '%s'" (Kernel_function.get_name kf) in
+ let instance_of vc =
+ let hyp = match fopt with
+ | None -> F.p_true
+ | Some floc -> C.instance_of floc kf
+ in assume_vc ~stmt ~warn ~descr ~hpid [hyp] vc
in
Gmap.map
(fun s ->
Splitter.map
- (instance_vc pa fptr)
+ (fun vc -> passify_vc pa (instance_of vc))
(Splitter.group tag merge_vcs s)
) wp.vcs
let call_dynamic wenv stmt gpid fct calls = L.in_frame wenv.frame
begin fun () ->
let sigma = Sigma.create () in
- let outcome = Warning.catch
- ~severe:false ~effect:"Ignored function pointer value"
- (C.call sigma) fct in
- let fptr = match outcome with
- | Warning.Failed _warn -> None
- | Warning.Result(warn,floc) -> Some(warn,floc) in
- let vcs_calls = List.map (call_contract stmt sigma fptr) calls in
+ let called = call_pointer sigma fct in
+ let vcs_calls = List.map (call_contract stmt sigma gpid called) calls in
let vcs = merge_all_vcs vcs_calls in
- let vcs = call_instances sigma gpid fct (List.map fst calls) vcs in
+ let vcs = call_instance_of gpid called (List.map fst calls) vcs in
let effects = List.fold_left
(fun es (_,wp) -> Eset.union es wp.effects) Eset.empty calls in
{ sigma = Some sigma ; vcs = vcs ; effects = effects }
diff --git a/src/plugins/wp/dyncall.ml b/src/plugins/wp/dyncall.ml
index 486acc3d15292234737b9ccffdbdb46c1981386c..a13a06ebc5fed8f510ee27d07bc4c8538014e570 100644
--- a/src/plugins/wp/dyncall.ml
+++ b/src/plugins/wp/dyncall.ml
@@ -98,7 +98,7 @@ module CallPoints = State_builder.Hashtbl(Point.Hashtbl)(Calls)(CInfo)
let property ~kf ?bhv ~stmt ~calls =
let fact = match bhv with
| None -> Format.asprintf "@[<hov 2>calls%a@]" pp_calls calls
- | Some b -> Format.asprintf "@[<hov 2>for %s calls%a@]" b pp_calls calls
+ | Some b -> Format.asprintf "@[<hov 2>calls%a for %s@]" pp_calls calls b
in
Property.(ip_other fact (OLStmt (kf,stmt)))
diff --git a/src/plugins/wp/tests/wp_plugin/dynamic.i.0.report.json b/src/plugins/wp/tests/wp_plugin/dynamic.i.0.report.json
index 3fc42db1868cdc9fa34566f975d4b927b940c9fe..928d6afe79ece9ec9233f104866dc3272c72a31d 100644
--- a/src/plugins/wp/tests/wp_plugin/dynamic.i.0.report.json
+++ b/src/plugins/wp/tests/wp_plugin/dynamic.i.0.report.json
@@ -55,7 +55,7 @@
"wp:main": { "total": 5,
"valid": 5,
"rank": 5 } } },
- "behavior": { "behavior_stmt_for_bhv1_calls_h1_h2":
+ "behavior": { "behavior_stmt_calls_h1_h2_for_bhv1":
{ "qed": { "total": 1, "valid": 1 },
"wp:main": { "total": 1, "valid": 1 } },
"behavior_bhv1_assign": { "qed": { "total": 6,
@@ -72,11 +72,11 @@
"valid": 9 },
"wp:main": { "total": 9,
"valid": 9 } } },
- "some_behaviors": { "some_behaviors_stmt_for_bhv1_calls_h1_h2_h0":
+ "some_behaviors": { "some_behaviors_stmt_calls_h1_h2_h0_for_bhv1":
{ "qed": { "total": 1, "valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
- "some_behaviors_stmt_for_bhv0_calls_h1_h2_h0":
+ "some_behaviors_stmt_calls_h1_h2_h0_for_bhv0":
{ "qed": { "total": 1, "valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
index bf4dd0108f3be3b7038c570ea0b70f0009c67574..6b119b905ab053d9892cd64aa530c35f0d460f1b 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
@@ -17,7 +17,7 @@
Function behavior with behavior bhv1
------------------------------------------------------------
-Goal for bhv1 calls h1 h2 in 'behavior' at instruction (file tests/wp_plugin/dynamic.i, line 65):
+Goal Calls h1 h2 for bhv1 in 'behavior' at instruction (file tests/wp_plugin/dynamic.i, line 65):
Prove: true.
------------------------------------------------------------
@@ -75,7 +75,7 @@ Prove: true.
Function call
------------------------------------------------------------
-Goal calls f1 f2 in 'call' at instruction (file tests/wp_plugin/dynamic.i, line 30):
+Goal Calls f1 f2 in 'call' at instruction (file tests/wp_plugin/dynamic.i, line 30):
Let a = Mptr_0[shiftfield_F1_S_f(closure_0)].
Let a_1 = global(G_f2_26).
Let a_2 = global(G_f1_20).
@@ -114,6 +114,7 @@ Assume {
(* Pre-condition *)
Have: abs_int(x) <= 5.
(* Instance of 'f1' *)
+ (* Calls f1 f2 *)
Have: Mptr_0[shiftfield_F1_S_f(closure_0)] = global(G_f1_20).
}
Prove: ((-10) <= x) /\ (x <= 10).
@@ -123,7 +124,7 @@ Prove: ((-10) <= x) /\ (x <= 10).
Function guarded_call
------------------------------------------------------------
-Goal calls g in 'guarded_call' at instruction (file tests/wp_plugin/dynamic.i, line 44):
+Goal Calls g in 'guarded_call' at instruction (file tests/wp_plugin/dynamic.i, line 44):
Prove: true.
------------------------------------------------------------
@@ -162,7 +163,7 @@ Prove: true.
Function no_call
------------------------------------------------------------
-Goal calls unreachable_g in 'no_call' at instruction (file tests/wp_plugin/dynamic.i, line 91):
+Goal Calls unreachable_g in 'no_call' at instruction (file tests/wp_plugin/dynamic.i, line 91):
Prove: true.
------------------------------------------------------------
@@ -188,7 +189,7 @@ Prove: true.
Function some_behaviors with behavior bhv0
------------------------------------------------------------
-Goal for bhv0 calls h1 h2 h0 in 'some_behaviors' at instruction (file tests/wp_plugin/dynamic.i, line 78):
+Goal Calls h1 h2 h0 for bhv0 in 'some_behaviors' at instruction (file tests/wp_plugin/dynamic.i, line 78):
Prove: true.
------------------------------------------------------------
@@ -273,7 +274,7 @@ Prove: true.
Function some_behaviors with behavior bhv1
------------------------------------------------------------
-Goal for bhv1 calls h1 h2 h0 in 'some_behaviors' at instruction (file tests/wp_plugin/dynamic.i, line 78):
+Goal Calls h1 h2 h0 for bhv1 in 'some_behaviors' at instruction (file tests/wp_plugin/dynamic.i, line 78):
Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
index b3976cc55b41db5a9b3dd360f5feb8055a32b281..42d0aad2267dcab09a88aa697aa7a678155906cd 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
@@ -6,7 +6,7 @@
Missigns 'calls' clause dedicated to dynamic calls (see WP manual)
[wp] Warning: Missing RTE guards
[wp] 46 goals scheduled
-[wp] [Qed] Goal typed_behavior_stmt_for_bhv1_calls_h1_h2 : Valid
+[wp] [Qed] Goal typed_behavior_stmt_calls_h1_h2_for_bhv1 : Valid
[wp] [Qed] Goal typed_behavior_bhv1_post_part1 : Valid
[wp] [Qed] Goal typed_behavior_bhv1_post_part2 : Valid
[wp] [Qed] Goal typed_behavior_bhv1_assign_exit_part1 : Valid
@@ -28,7 +28,7 @@
[wp] [Qed] Goal typed_no_call_post_part1 : Valid
[wp] [Qed] Goal typed_no_call_post_part2 : Valid
[wp] [Qed] Goal typed_no_call_call_unreachable_g_pre : Valid
-[wp] [Qed] Goal typed_some_behaviors_stmt_for_bhv0_calls_h1_h2_h0 : Valid
+[wp] [Qed] Goal typed_some_behaviors_stmt_calls_h1_h2_h0_for_bhv0 : Valid
[wp] [Qed] Goal typed_some_behaviors_bhv0_post_part1 : Valid
[wp] [Qed] Goal typed_some_behaviors_bhv0_post_part2 : Valid
[wp] [Qed] Goal typed_some_behaviors_bhv0_post_part3 : Valid
@@ -41,7 +41,7 @@
[wp] [Qed] Goal typed_some_behaviors_bhv0_assign_normal_part4 : Valid
[wp] [Qed] Goal typed_some_behaviors_bhv0_assign_normal_part5 : Valid
[wp] [Qed] Goal typed_some_behaviors_bhv0_assign_normal_part6 : Valid
-[wp] [Qed] Goal typed_some_behaviors_stmt_for_bhv1_calls_h1_h2_h0 : Valid
+[wp] [Qed] Goal typed_some_behaviors_stmt_calls_h1_h2_h0_for_bhv1 : Valid
[wp] [Qed] Goal typed_some_behaviors_bhv1_post_part1 : Valid
[wp] [Qed] Goal typed_some_behaviors_bhv1_post_part2 : Valid
[wp] [Qed] Goal typed_some_behaviors_bhv1_post_part3 : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/string_c.c.0.report.json b/src/plugins/wp/tests/wp_plugin/string_c.c.0.report.json
index 89a03ae6f3db1f3d7f13fdd15da4799ae615ee0d..a4d745460b88f693b10e7b28968614fc8fe5225a 100644
--- a/src/plugins/wp/tests/wp_plugin/string_c.c.0.report.json
+++ b/src/plugins/wp/tests/wp_plugin/string_c.c.0.report.json
@@ -34,12 +34,12 @@
"valid": 1 } },
"memcpy_loop_assign": { "alt-ergo": { "total": 1,
"valid": 1,
- "rank": 43 },
+ "rank": 40 },
"qed": { "total": 2,
"valid": 2 },
"wp:main": { "total": 3,
"valid": 3,
- "rank": 43 } },
+ "rank": 40 } },
"memcpy_post_result_ptr": { "qed": { "total": 1,
"valid": 1 },
"wp:main":