Skip to content
Snippets Groups Projects
Commit 147c0a38 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[eva] don't reduce check-only loop invariants

parent 0bcdf987
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/value/engine/transfer_logic.ml
+ 1
− 1
View file @ 147c0a38
...@@ -691,7 +691,7 @@ module Make ...@@ -691,7 +691,7 @@ module Make
| AAssert (behav, p) -> | AAssert (behav, p) ->
aux ~reduce:(not p.tp_only_check) code_annot behav p.tp_statement aux ~reduce:(not p.tp_only_check) code_annot behav p.tp_statement
| AInvariant (behav, true, p) -> | 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 _ | APragma _
| AInvariant (_, false, _) | AInvariant (_, false, _)
| AVariant _ | AAssigns _ | AAllocation _ | AExtended _ | AVariant _ | AAssigns _ | AAllocation _ | AExtended _
......
tests/spec/generalized_check.i
+ 8
− 3
View file @ 147c0a38
/* run.config /* 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 OPT: -eva -eva-use-spec f
*/ */
/*@ check lemma easy_proof: \false; */ // should not be put in any environment /*@ check lemma easy_proof: \false; */ // should not be put in any environment
...@@ -13,6 +13,8 @@ void f(int* x) { ...@@ -13,6 +13,8 @@ void f(int* x) {
*x = 0; *x = 0;
} }
void loop(void);
int main() { int main() {
int a = 4; int a = 4;
volatile int c; volatile int c;
...@@ -21,12 +23,15 @@ int main() { ...@@ -21,12 +23,15 @@ int main() {
f(p); f(p);
/*@ check main_valid_ko: \valid(p); */ /*@ check main_valid_ko: \valid(p); */
/*@ check main_p_content_ko: *p == 0; */ /*@ check main_p_content_ko: *p == 0; */
loop();
} }
void loop () { void loop () {
/*@ check loop invariant \true; */
for (int i = 0; i< 10; i++);
int j = 0; int j = 0;
/*@ check loop invariant j == 10;
loop assigns i;
*/
for (int i = 0; i< 10; i++);
l: /*@ check invariant \true; */ ; l: /*@ check invariant \true; */ ;
if (j >= 10) goto l1; if (j >= 10) goto l1;
j++; j++;
......
tests/spec/oracle/generalized_check.0.res.oracle
+ 142
− 9
View file @ 147c0a38
...@@ -5,7 +5,55 @@ ...@@ -5,7 +5,55 @@
[wp:strategy] take f_assigns *x; [wp:strategy] take f_assigns *x;
[wp:strategy] [add_node_annots] on <stmt-1> [wp:strategy] [add_node_annots] on <stmt-1>
[wp:strategy] [add_node_annots] on <stmt-2> [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] 'main' is the main entry point
[wp:strategy] [add_node_annots] on <stmt-5> [wp:strategy] [add_node_annots] on <stmt-5>
[wp:strategy] [add_node_annots] on <stmt-6> [wp:strategy] [add_node_annots] on <stmt-6>
...@@ -16,8 +64,10 @@ ...@@ -16,8 +64,10 @@
[wp:strategy] [add_node_annots] on <callIn-11> [wp:strategy] [add_node_annots] on <callIn-11>
[wp:strategy] [add_node_annots] on <stmt-12> [wp:strategy] [add_node_annots] on <stmt-12>
[wp:strategy] [add_node_annots] on <stmt-13> [wp:strategy] [add_node_annots] on <stmt-13>
[wp:strategy] [add_node_annots] on <stmt-14> [wp:strategy] [add_node_annots] on <callIn-14>
[wp:strategy] [add_node_annots] on <stmt-38> [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] Warning: Missing RTE guards
[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] 'f' is NOT the main entry point
...@@ -43,6 +93,78 @@ ...@@ -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] '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 [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 @@ ...@@ -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: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] [Qed] Goal typed_f_assigns : Valid
[wp] [Failed] Goal typed_f_check_f_valid_ko [wp] [Failed] Goal typed_f_check_f_valid_ko
[wp] [Qed] Goal typed_f_ensures_f_init_x : Valid [wp] [Qed] Goal typed_f_ensures_f_init_x : Valid
[wp] [Failed] Goal typed_lemma_easy_proof [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_call_f_requires_f_valid_x
[wp] [Failed] Goal typed_main_check_main_p_content_ko [wp] [Failed] Goal typed_main_check_main_p_content_ko
[wp] [Failed] Goal typed_main_check_main_valid_ko [wp] Proved goals: 4 / 10
[wp] Proved goals: 2 / 7 Qed: 4
Qed: 2
[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] '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 [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) ...@@ -158,6 +287,8 @@ void f(int *x)
return; return;
} }
void loop(void);
int main(void) int main(void)
{ {
int __retres; int __retres;
...@@ -168,18 +299,20 @@ int main(void) ...@@ -168,18 +299,20 @@ int main(void)
f(p); f(p);
/*@ check main_valid_ko: \valid(p); */ ; /*@ check main_valid_ko: \valid(p); */ ;
/*@ check main_p_content_ko: *p ≡ 0; */ ; /*@ check main_p_content_ko: *p ≡ 0; */ ;
loop();
__retres = 0; __retres = 0;
return __retres; return __retres;
} }
void loop(void) void loop(void)
{ {
int j = 0;
{ {
int i = 0; int i = 0;
/*@ check loop invariant \true; */ /*@ check loop invariant j ≡ 10;
loop assigns i; */
while (i < 10) i ++; while (i < 10) i ++;
} }
int j = 0;
l: /*@ check invariant \true; */ ; l: /*@ check invariant \true; */ ;
if (j >= 10) goto l1; if (j >= 10) goto l1;
j ++; j ++;
......
tests/spec/oracle/generalized_check.1.res.oracle
+ 12
− 7
View file @ 147c0a38
...@@ -4,27 +4,32 @@ ...@@ -4,27 +4,32 @@
[eva] Initial state computed [eva] Initial state computed
[eva:initial-state] Values of globals at initialization [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); accessing uninitialized left-value. assert \initialized(&c);
[eva] using specification for function f [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. function f: precondition 'f_valid_x' got status unknown.
[eva] tests/spec/generalized_check.i:8: Warning: [eva] tests/spec/generalized_check.i:8: Warning:
no \from part for clause 'assigns *x;' 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. 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. 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] done for function main
[eva] ====== VALUES COMPUTED ====== [eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function loop:
j ∈ {10}
[eva:final-states] Values at end of function main: [eva:final-states] Values at end of function main:
a ∈ [--..--] a ∈ [--..--]
p ∈ {{ NULL ; &a }} p ∈ {{ NULL ; &a }}
__retres ∈ {0} __retres ∈ {0}
[eva:summary] ====== ANALYSIS SUMMARY ====== [eva:summary] ====== ANALYSIS SUMMARY ======
---------------------------------------------------------------------------- ----------------------------------------------------------------------------
2 functions analyzed (out of 3): 66% coverage. 3 functions analyzed (out of 3): 100% coverage.
In these functions, 9 statements reached (out of 12): 75% coverage. In these functions, 24 statements reached (out of 27): 88% coverage.
---------------------------------------------------------------------------- ----------------------------------------------------------------------------
Some errors and warnings have been raised during the analysis: Some errors and warnings have been raised during the analysis:
by the Eva analyzer: 0 errors 1 warning by the Eva analyzer: 0 errors 1 warning
...@@ -34,7 +39,7 @@ ...@@ -34,7 +39,7 @@
1 access to uninitialized left-values 1 access to uninitialized left-values
---------------------------------------------------------------------------- ----------------------------------------------------------------------------
Evaluation of the logical properties reached by the analysis: 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 Preconditions 0 valid 1 unknown 0 invalid 1 total
0% of the logical properties reached have been proven. 0% of the logical properties reached have been proven.
---------------------------------------------------------------------------- ----------------------------------------------------------------------------
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment