diff --git a/src/plugins/value/engine/transfer_logic.ml b/src/plugins/value/engine/transfer_logic.ml
index a615747430c06dea473a8fdaa67825ac54dc74da..e251024a6cc92ccf7e664b96dc9f98e4beb616db 100644
--- a/src/plugins/value/engine/transfer_logic.ml
+++ b/src/plugins/value/engine/transfer_logic.ml
@@ -691,7 +691,7 @@ module Make
| AAssert (behav, p) ->
aux ~reduce:(not p.tp_only_check) code_annot behav p.tp_statement
| AInvariant (behav, true, p) ->
- aux ~reduce:true code_annot behav p.tp_statement
+ aux ~reduce:(not p.tp_only_check) code_annot behav p.tp_statement
| APragma _
| AInvariant (_, false, _)
| AVariant _ | AAssigns _ | AAllocation _ | AExtended _
diff --git a/tests/spec/generalized_check.i b/tests/spec/generalized_check.i
index 5fbfd04972974ca3565db3de297ace71fa29b051..8231d53c2876f3c832c25634f076ab9d9fe6cdc6 100644
--- a/tests/spec/generalized_check.i
+++ b/tests/spec/generalized_check.i
@@ -1,5 +1,5 @@
/* run.config
-OPT: -wp-fct f,main -wp -wp-prover qed -wp-msg-key strategy,no-time-info -print
+OPT: -wp -wp-prover qed -wp-msg-key strategy,no-time-info -print
OPT: -eva -eva-use-spec f
*/
/*@ check lemma easy_proof: \false; */ // should not be put in any environment
@@ -13,6 +13,8 @@ void f(int* x) {
*x = 0;
}
+void loop(void);
+
int main() {
int a = 4;
volatile int c;
@@ -21,12 +23,15 @@ int main() {
f(p);
/*@ check main_valid_ko: \valid(p); */
/*@ check main_p_content_ko: *p == 0; */
+ loop();
}
void loop () {
- /*@ check loop invariant \true; */
- for (int i = 0; i< 10; i++);
int j = 0;
+ /*@ check loop invariant j == 10;
+ loop assigns i;
+ */
+ for (int i = 0; i< 10; i++);
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 b51e566532cc803f6d8a03cf4130678aa9ccd0c0..753b2499bdd1dfb153e619953b918eea3e36579c 100644
--- a/tests/spec/oracle/generalized_check.0.res.oracle
+++ b/tests/spec/oracle/generalized_check.0.res.oracle
@@ -5,7 +5,55 @@
[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-36>
+[wp:strategy] [add_node_annots] on <stmt-37>
+[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] 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-33>
+[wp:strategy] [add_node_annots] on <stmt-34>
+[wp:strategy] [add_node_annots] on <stmt-41>
+[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
+[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] take loop_loop_assigns i;
+[wp:strategy] take loop_loop_assigns i;
+[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
+[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] 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] 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_node_annots] on <blkIn-stmt:18>
[wp:strategy] 'main' is the main entry point
[wp:strategy] [add_node_annots] on <stmt-5>
[wp:strategy] [add_node_annots] on <stmt-6>
@@ -16,8 +64,10 @@
[wp:strategy] [add_node_annots] on <callIn-11>
[wp:strategy] [add_node_annots] on <stmt-12>
[wp:strategy] [add_node_annots] on <stmt-13>
-[wp:strategy] [add_node_annots] on <stmt-14>
-[wp:strategy] [add_node_annots] on <stmt-38>
+[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] Warning: Missing RTE guards
[wp:strategy] 'f' is NOT the main entry point
[wp:strategy] 'f' is NOT the main entry point
@@ -43,6 +93,78 @@
[wp:strategy] 'f' is NOT the main entry point
[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
+[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] '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] '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] '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] '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] '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] 'loop' is NOT the main entry point
+[wp:strategy] 'loop' is NOT the main entry point
+[wp] tests/spec/generalized_check.i:35: 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
+[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] '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] '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] '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] '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] '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] '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] '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] '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] '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] '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
@@ -127,18 +249,25 @@
[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] 7 goals scheduled
+[wp:strategy] 'main' is the main entry point
+[wp] 10 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_main_call_f_requires_f_valid_x
[wp] [Failed] Goal typed_main_check_main_p_content_ko
-[wp] [Failed] Goal typed_main_check_main_valid_ko
-[wp] Proved goals: 2 / 7
- Qed: 2
+[wp] Proved goals: 4 / 10
+ Qed: 4
[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
+[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
@@ -158,6 +287,8 @@ void f(int *x)
return;
}
+void loop(void);
+
int main(void)
{
int __retres;
@@ -168,18 +299,20 @@ int main(void)
f(p);
/*@ check main_valid_ko: \valid(p); */ ;
/*@ check main_p_content_ko: *p ≡ 0; */ ;
+ loop();
__retres = 0;
return __retres;
}
void loop(void)
{
+ int j = 0;
{
int i = 0;
- /*@ check loop invariant \true; */
+ /*@ check loop invariant j ≡ 10;
+ loop assigns i; */
while (i < 10) i ++;
}
- int j = 0;
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 4c0df089fdc7a7e7e8363d3c06e83bbaa5dd953c..fc45924ecaf584159ac7c85fbc79eb6c46348711 100644
--- a/tests/spec/oracle/generalized_check.1.res.oracle
+++ b/tests/spec/oracle/generalized_check.1.res.oracle
@@ -4,27 +4,32 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva:alarm] tests/spec/generalized_check.i:20: Warning:
+[eva:alarm] tests/spec/generalized_check.i:22: Warning:
accessing uninitialized left-value. assert \initialized(&c);
[eva] using specification for function f
-[eva:alarm] tests/spec/generalized_check.i:21: Warning:
+[eva:alarm] tests/spec/generalized_check.i:23: Warning:
function f: precondition 'f_valid_x' got status unknown.
[eva] tests/spec/generalized_check.i:8: Warning:
no \from part for clause 'assigns *x;'
-[eva:alarm] tests/spec/generalized_check.i:22: Warning:
+[eva:alarm] tests/spec/generalized_check.i:24: Warning:
check 'main_valid_ko' got status unknown.
-[eva:alarm] tests/spec/generalized_check.i:23: Warning:
+[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.
+[eva] tests/spec/generalized_check.i:34: starting to merge loop iterations
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function loop:
+ j ∈ {10}
[eva:final-states] Values at end of function main:
a ∈ [--..--]
p ∈ {{ NULL ; &a }}
__retres ∈ {0}
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 2 functions analyzed (out of 3): 66% coverage.
- In these functions, 9 statements reached (out of 12): 75% coverage.
+ 3 functions analyzed (out of 3): 100% coverage.
+ In these functions, 24 statements reached (out of 27): 88% coverage.
----------------------------------------------------------------------------
Some errors and warnings have been raised during the analysis:
by the Eva analyzer: 0 errors 1 warning
@@ -34,7 +39,7 @@
1 access to uninitialized left-values
----------------------------------------------------------------------------
Evaluation of the logical properties reached by the analysis:
- Assertions 0 valid 2 unknown 0 invalid 2 total
+ Assertions 0 valid 2 unknown 1 invalid 3 total
Preconditions 0 valid 1 unknown 0 invalid 1 total
0% of the logical properties reached have been proven.
----------------------------------------------------------------------------