diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index cb2cf7d5809d6a538fa36a9ac6422762a6fba412..eaee55511cfafb12924c110f9ab35ad17d8f4b6c 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -833,6 +833,8 @@ let add_variant_annot config s ca var_exp loop_entry loop_back =
in loop_entry, loop_back
let add_loop_invariant_annot config vloop s ca b_list inv acc =
+ let only_check = inv.tp_only_check in
+ let inv = inv.tp_statement in
let assigns, loop_entry, loop_back , loop_core = acc in
(* we have to prove that inv is true for each edge that goes
* in the loop, so we can assume that inv is true for each edge
@@ -846,15 +848,18 @@ let add_loop_invariant_annot config vloop s ca b_list inv acc =
WpStrategy.Agoal s ca inv in
let loop_back = add_prop_loop_inv ~established:false config loop_back
WpStrategy.Agoal s ca inv in
- let loop_core = add_prop_inv_fixpoint config loop_core
- WpStrategy.Ahyp s ca inv in
+ let loop_core =
+ if only_check then loop_core
+ else
+ add_prop_inv_fixpoint config loop_core WpStrategy.Ahyp s ca inv
+ in
assigns, loop_entry , loop_back , loop_core
end
- | TBRhyp ->
+ | TBRhyp when not only_check ->
let kind = WpStrategy.Ahyp in
let loop_core = add_prop_inv_fixpoint config loop_core kind s ca inv
in assigns, loop_entry , loop_back , loop_core
- | TBRno -> acc
+ | TBRhyp | TBRno -> acc
(** Returns the annotations for the three edges of the loop node:
* - loop_entry : goals for the edge entering in the loop
@@ -865,7 +870,7 @@ let get_loop_annots config vloop s =
let do_annot _ a (assigns, loop_entry, loop_back , loop_core as acc) =
match a.annot_content with
| AInvariant (b_list, true, inv) ->
- add_loop_invariant_annot config vloop s a b_list inv.tp_statement acc
+ add_loop_invariant_annot config vloop s a b_list inv acc
| AVariant (var_exp, None) ->
let loop_entry, loop_back =
add_variant_annot config s a var_exp loop_entry loop_back
diff --git a/tests/spec/generalized_check.i b/tests/spec/generalized_check.i
index 8231d53c2876f3c832c25634f076ab9d9fe6cdc6..e65573c02330b3aa9d5d5fd24a82f8e61cf555b2 100644
--- a/tests/spec/generalized_check.i
+++ b/tests/spec/generalized_check.i
@@ -28,10 +28,11 @@ int main() {
void loop () {
int j = 0;
- /*@ check loop invariant j == 10;
+ /*@ check loop invariant false_but_preserved: j == 10;
loop assigns i;
*/
for (int i = 0; i< 10; i++);
+ /*@ check implied_by_false_invariant: j == 10; */
l: /*@ check invariant \true; */ ;
if (j >= 10) goto l1;
j++;
diff --git a/tests/spec/oracle/generalized_check.0.res.oracle b/tests/spec/oracle/generalized_check.0.res.oracle
index 753b2499bdd1dfb153e619953b918eea3e36579c..eca824fbeedb4d37a9498e1516b96a8492cfdfc0 100644
--- a/tests/spec/oracle/generalized_check.0.res.oracle
+++ b/tests/spec/oracle/generalized_check.0.res.oracle
@@ -5,24 +5,25 @@
[wp:strategy] take f_assigns *x;
[wp:strategy] [add_node_annots] on <stmt-1>
[wp:strategy] [add_node_annots] on <stmt-2>
-[wp:strategy] [add_node_annots] on <stmt-37>
+[wp:strategy] [add_node_annots] on <stmt-38>
[wp:strategy] 'loop' is NOT the main entry point
[wp:strategy] [add_node_annots] on <stmt-17>
[wp:strategy] [add_node_annots] on <stmt-19>
[wp:strategy] [add_node_annots] on <testIn-22>
[wp:strategy] [add_node_annots] on <stmt-23>
[wp:strategy] [add_node_annots] on <stmt-25>
+[wp:strategy] [add_node_annots] on <stmt-26>
[wp] tests/spec/generalized_check.i:29: Warning:
Unsupported generalized invariant, use loop invariant instead.
Ignored invariant
check invariant \true;
-[wp:strategy] [add_node_annots] on <stmt-26>
-[wp:strategy] [add_node_annots] on <testIn-29>
-[wp:strategy] [add_node_annots] on <stmt-30>
-[wp:strategy] [add_node_annots] on <stmt-32>
+[wp:strategy] [add_node_annots] on <stmt-27>
+[wp:strategy] [add_node_annots] on <testIn-30>
+[wp:strategy] [add_node_annots] on <stmt-31>
[wp:strategy] [add_node_annots] on <stmt-33>
[wp:strategy] [add_node_annots] on <stmt-34>
-[wp:strategy] [add_node_annots] on <stmt-41>
+[wp:strategy] [add_node_annots] on <stmt-35>
+[wp:strategy] [add_node_annots] on <stmt-42>
[wp:strategy] [add_loop_annots] on <loop-20>
[wp:strategy] [add_loop_annots] 1 edges_to_head
[wp:strategy] [add_loop_annots] 2 edges_to_loop
@@ -39,14 +40,14 @@
[wp:strategy] [add_loop_annots on entry_edges ok]
[wp:strategy] [add_loop_annots on back_edges ok]
[wp:strategy] [add_loop_annots on edges_to_head ok]
-[wp:strategy] [add_loop_annots] on <loop-26>
+[wp:strategy] [add_loop_annots] on <loop-27>
[wp:strategy] [add_loop_annots] 1 edges_to_head
[wp:strategy] [add_loop_annots] 2 edges_to_loop
[wp:strategy] [add_loop_annots] 1 back_edges + 1 entry_edges
[wp:strategy] [add_loop_annots on entry_edges ok]
[wp:strategy] [add_loop_annots on back_edges ok]
[wp:strategy] [add_loop_annots on edges_to_head ok]
-[wp:strategy] [add_loop_annots] on <loop-26>
+[wp:strategy] [add_loop_annots] on <loop-27>
[wp:strategy] [add_loop_annots] 1 edges_to_head
[wp:strategy] [add_loop_annots] 2 edges_to_loop
[wp:strategy] [add_loop_annots] 1 back_edges + 1 entry_edges
@@ -67,7 +68,7 @@
[wp:strategy] [add_node_annots] on <callIn-14>
[wp:strategy] [add_node_annots] on <callIn-14>
[wp:strategy] [add_node_annots] on <stmt-15>
-[wp:strategy] [add_node_annots] on <stmt-39>
+[wp:strategy] [add_node_annots] on <stmt-40>
[wp] Warning: Missing RTE guards
[wp:strategy] 'f' is NOT the main entry point
[wp:strategy] 'f' is NOT the main entry point
@@ -120,7 +121,7 @@
[wp:strategy] 'loop' is NOT the main entry point
[wp:strategy] 'loop' is NOT the main entry point
[wp:strategy] 'loop' is NOT the main entry point
-[wp] tests/spec/generalized_check.i:35: Warning:
+[wp] tests/spec/generalized_check.i:36: Warning:
Missing assigns clause (assigns 'everything' instead)
[wp:strategy] 'loop' is NOT the main entry point
[wp:strategy] 'loop' is NOT the main entry point
@@ -165,6 +166,7 @@
[wp:strategy] 'loop' is NOT the main entry point
[wp:strategy] 'loop' is NOT the main entry point
[wp:strategy] 'loop' is NOT the main entry point
+[wp:strategy] 'loop' is NOT the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
@@ -250,19 +252,20 @@
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
-[wp] 10 goals scheduled
+[wp] 11 goals scheduled
[wp] [Qed] Goal typed_f_assigns : Valid
[wp] [Failed] Goal typed_f_check_f_valid_ko
[wp] [Qed] Goal typed_f_ensures_f_init_x : Valid
[wp] [Failed] Goal typed_lemma_easy_proof
-[wp] [Failed] Goal typed_main_check_main_valid_ko
[wp] [Qed] Goal typed_loop_loop_assigns : Valid
-[wp] [Failed] Goal typed_loop_loop_invariant_established
-[wp] [Qed] Goal typed_loop_loop_invariant_preserved : Valid
+[wp] [Failed] Goal typed_loop_check_implied_by_false_invariant
+[wp] [Failed] Goal typed_loop_loop_invariant_false_but_preserved_established
+[wp] [Failed] Goal typed_loop_loop_invariant_false_but_preserved_preserved
[wp] [Failed] Goal typed_main_call_f_requires_f_valid_x
[wp] [Failed] Goal typed_main_check_main_p_content_ko
-[wp] Proved goals: 4 / 10
- Qed: 4
+[wp] [Failed] Goal typed_main_check_main_valid_ko
+[wp] Proved goals: 3 / 11
+ Qed: 3
[wp:strategy] 'f' is NOT the main entry point
[wp:strategy] 'f' is NOT the main entry point
[wp:strategy] 'loop' is NOT the main entry point
@@ -309,10 +312,11 @@ void loop(void)
int j = 0;
{
int i = 0;
- /*@ check loop invariant j ≡ 10;
+ /*@ check loop invariant false_but_preserved: j ≡ 10;
loop assigns i; */
while (i < 10) i ++;
}
+ /*@ check implied_by_false_invariant: j ≡ 10; */ ;
l: /*@ check invariant \true; */ ;
if (j >= 10) goto l1;
j ++;
diff --git a/tests/spec/oracle/generalized_check.1.res.oracle b/tests/spec/oracle/generalized_check.1.res.oracle
index fc45924ecaf584159ac7c85fbc79eb6c46348711..e160c9b946ffa483177c8693ed53f85b9d7f7e82 100644
--- a/tests/spec/oracle/generalized_check.1.res.oracle
+++ b/tests/spec/oracle/generalized_check.1.res.oracle
@@ -16,8 +16,10 @@
[eva:alarm] tests/spec/generalized_check.i:25: Warning:
check 'main_p_content_ko' got status unknown.
[eva:alarm] tests/spec/generalized_check.i:31: Warning:
- loop invariant got status invalid.
+ loop invariant 'false_but_preserved' got status invalid.
[eva] tests/spec/generalized_check.i:34: starting to merge loop iterations
+[eva:alarm] tests/spec/generalized_check.i:35: Warning:
+ check 'implied_by_false_invariant' got status invalid.
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function loop:
@@ -29,7 +31,7 @@
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
3 functions analyzed (out of 3): 100% coverage.
- In these functions, 24 statements reached (out of 27): 88% coverage.
+ In these functions, 25 statements reached (out of 28): 89% coverage.
----------------------------------------------------------------------------
Some errors and warnings have been raised during the analysis:
by the Eva analyzer: 0 errors 1 warning
@@ -39,7 +41,7 @@
1 access to uninitialized left-values
----------------------------------------------------------------------------
Evaluation of the logical properties reached by the analysis:
- Assertions 0 valid 2 unknown 1 invalid 3 total
+ Assertions 0 valid 2 unknown 2 invalid 4 total
Preconditions 0 valid 1 unknown 0 invalid 1 total
0% of the logical properties reached have been proven.
----------------------------------------------------------------------------