Skip to content
Snippets Groups Projects
Commit 32698b11 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

Update tests: WP now populates terminates and exits

parent 52880073
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 248 additions and 53 deletions
tests/meta-deduce/oracle/consequence.res.oracle
+ 33
− 7
View file @ 32698b11
......@@ -7,21 +7,35 @@
[meta] Warning: false_wit2 : FAILURE
[meta] Successful translation
[wp] Running WP plugin...
[wp] [Valid] Goal f1_exits (Cfg) (Unreachable)
[wp] [Valid] Goal f1_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[wp] 11 goals scheduled
[wp] [Valid] Goal f2_exits (Cfg) (Unreachable)
[wp] [Valid] Goal f2_terminates (Cfg) (Trivial)
[wp] [Valid] Goal f3_exits (Cfg) (Unreachable)
[wp] [Valid] Goal f3_terminates (Cfg) (Trivial)
[wp] [Valid] Goal f5_exits (Cfg) (Unreachable)
[wp] [Valid] Goal f5_terminates (Cfg) (Trivial)
[wp] 15 goals scheduled
[wp] [Valid] typed_f1_ensures_inv_big_meta (Qed)
[wp] [Valid] typed_f1_assigns (Qed)
[wp] [Valid] typed_f2_ensures_inv_big_meta (Qed)
[wp] [Valid] typed_f2_assigns (Qed)
[wp] [Valid] typed_f3_assigns (Qed)
[wp] [Valid] typed_f5_assigns (Qed)
[wp] [Valid] typed_f4_terminates (Qed)
[wp] [Valid] typed_f4_exits (Qed)
[wp] [Valid] typed_f4_assigns_exit (Qed)
[wp] [Valid] typed_f4_assigns_normal (Qed)
[wp] [Unsuccess] typed_f4_call_f2_requires_inv_big_meta (Alt-Ergo) (Cached)
[wp] [Valid] typed_f6_terminates (Qed)
[wp] [Valid] typed_f6_exits (Qed)
[wp] [Valid] typed_f6_assigns_exit (Qed)
[wp] [Valid] typed_f6_assigns_normal (Qed)
[wp] Proved goals: 10 / 11
Qed: 10
[wp] Proved goals: 22 / 23
Terminating: 4
Unreachable: 4
Qed: 14
Unsuccess: 1
/* Generated by Frama-C */
int A;
......@@ -29,7 +43,9 @@ int B;
int C;
int D;
/*@ requires inv_big: meta: A ≡ B;
terminates \true;
ensures inv_big: meta: A ≡ B;
exits \false;
assigns A, B;
*/
void f1(int v)
......@@ -40,7 +56,9 @@ void f1(int v)
}
/*@ requires inv_big: meta: A ≡ B;
terminates \true;
ensures inv_big: meta: A ≡ B;
exits \false;
assigns A;
*/
void f2(void)
......@@ -49,21 +67,27 @@ void f2(void)
return;
}
/*@ assigns C; */
/*@ terminates \true;
exits \false;
assigns C; */
void f3(void)
{
C = 42;
return;
}
/*@ assigns A; */
/*@ terminates \true;
exits \false;
assigns A; */
void f5(void)
{
A = 42;
return;
}
/*@ assigns D, A; */
/*@ terminates \true;
exits \false;
assigns D, A; */
void f4(void)
{
D = 24;
......@@ -71,7 +95,9 @@ void f4(void)
return;
}
/*@ assigns D, A; */
/*@ terminates \true;
exits \false;
assigns D, A; */
void f6(void)
{
f4();
......
tests/meta-deduce/oracle/negative_assigns.res.oracle
+ 31
− 10
View file @ 32698b11
......@@ -6,30 +6,46 @@
[meta] Successful translation
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 8 goals scheduled
[wp] [Valid] Goal f3_exits (Cfg) (Unreachable)
[wp] [Valid] Goal f3_terminates (Cfg) (Trivial)
[wp] 14 goals scheduled
[wp] [Valid] typed_f3_assigns (Qed)
[wp] [Valid] typed_f2_terminates (Qed)
[wp] [Valid] typed_f2_exits (Qed)
[wp] [Valid] typed_f2_assigns_exit (Qed)
[wp] [Valid] typed_f2_assigns_normal (Qed)
[wp] [Valid] typed_f1_terminates (Qed)
[wp] [Valid] typed_f1_exits (Qed)
[wp] [Valid] typed_f1_assigns_exit (Qed)
[wp] [Valid] typed_f1_assigns_normal (Qed)
[wp] [Valid] typed_f0_terminates (Qed)
[wp] [Valid] typed_f0_exits (Qed)
[wp] [Valid] typed_f0_assert (Qed)
[wp] [Valid] typed_f0_assigns_exit (Qed)
[wp] [Valid] typed_f0_assigns_normal (Qed)
[wp] Proved goals: 8 / 8
Qed: 8
[wp] Proved goals: 16 / 16
Terminating: 1
Unreachable: 1
Qed: 14
/* Generated by Frama-C */
int A;
int B;
/*@ ensures nega_correct: meta: A ≡ \old(A);
assigns B; */
/*@ terminates \true;
ensures nega_correct: meta: A ≡ \old(A);
exits \false;
assigns B;
*/
void f3(void)
{
B = 42;
return;
}
/*@ ensures nega_correct: meta: A ≡ \old(A);
assigns B; */
/*@ terminates \true;
ensures nega_correct: meta: A ≡ \old(A);
exits \false;
assigns B;
*/
void f2(void)
{
B = 12;
......@@ -37,8 +53,11 @@ void f2(void)
return;
}
/*@ ensures nega_correct: meta: A ≡ \old(A);
assigns B; */
/*@ terminates \true;
ensures nega_correct: meta: A ≡ \old(A);
exits \false;
assigns B;
*/
void f1(void)
{
B = 0;
......@@ -47,7 +66,9 @@ void f1(void)
return;
}
/*@ assigns A, B; */
/*@ terminates \true;
exits \false;
assigns A, B; */
void f0(void)
{
A = 42;
......
tests/meta-wp/oracle/assert_type_of.res.oracle
+ 18
− 4
View file @ 32698b11
......@@ -3,7 +3,13 @@
[meta] Will process 3 properties
[meta] Successful translation
[wp] Running WP plugin...
[wp] [Valid] Goal f1_exits (Cfg) (Unreachable)
[wp] [Valid] Goal f1_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[wp] [Valid] Goal f2_exits (Cfg) (Unreachable)
[wp] [Valid] Goal f2_terminates (Cfg) (Trivial)
[wp] [Valid] Goal f3_exits (Cfg) (Unreachable)
[wp] [Valid] Goal f3_terminates (Cfg) (Trivial)
[wp] 9 goals scheduled
[wp] [Valid] typed_f1_assert_m1_meta (Qed)
[wp] [Valid] typed_f1_assert_m2_meta (Qed)
......@@ -14,7 +20,9 @@
[wp] [Valid] typed_f3_assert_m3_meta (Qed)
[wp] [Unsuccess] typed_f3_assert_m3_meta_2 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f3_assigns (Qed)
[wp] Proved goals: 7 / 9
[wp] Proved goals: 13 / 15
Terminating: 3
Unreachable: 3
Qed: 7
Unsuccess: 2
/* Generated by Frama-C */
......@@ -28,7 +36,9 @@ int i2;
float d;
float e;
enum Foo f = ONE;
/*@ assigns i1; */
/*@ terminates \true;
exits \false;
assigns i1; */
void f1(void)
{
meta_pre_0: i1 = 42;
......@@ -37,7 +47,9 @@ void f1(void)
return;
}
/*@ assigns d, f, i2; */
/*@ terminates \true;
exits \false;
assigns d, f, i2; */
void f2(void)
{
d = (float)42.0;
......@@ -53,7 +65,9 @@ void f2(void)
return;
}
/*@ assigns f; */
/*@ terminates \true;
exits \false;
assigns f; */
void f3(void)
{
meta_pre_3: f = THREE;
......
tests/meta-wp/oracle/axiomatic_requires.res.oracle
+ 20
− 5
View file @ 32698b11
......@@ -3,17 +3,28 @@
[meta] Will process 1 properties
[meta] Successful translation
[wp] Running WP plugin...
[kernel:annot:missing-spec] axiomatic_requires.c:13: Warning:
Neither code nor explicit exits and terminates for function f0,
generating default clauses. See -generated-spec-* options for more info
[wp] [Valid] Goal f1_exits (Cfg) (Unreachable)
[wp] [Valid] Goal f1_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
[wp] 6 goals scheduled
[wp] [Valid] typed_f1_assigns (Qed)
[wp] [Valid] typed_main_terminates (Qed)
[wp] [Valid] typed_main_exits (Qed)
[wp] [Valid] typed_main_assert (Qed)
[wp] [Valid] typed_main_assigns_exit (Qed)
[wp] [Valid] typed_main_assigns_normal (Qed)
[wp] Proved goals: 4 / 4
Qed: 4
[wp] Proved goals: 8 / 8
Terminating: 1
Unreachable: 1
Qed: 6
/* Generated by Frama-C */
int A = 42;
/*@ requires axiomatic_requires: meta: A ≡ 42;
terminates \true;
exits \false;
ensures axiomatic_requires: meta: A ≡ 42;
assigns A;
*/
......@@ -23,10 +34,14 @@ void f1(void)
return;
}
/*@ assigns A; */
/*@ terminates \true;
exits \false;
assigns A; */
int f0(void);
/*@ assigns A; */
/*@ terminates \true;
exits \false;
assigns A; */
int main(void)
{
A = f0();
......
tests/meta-wp/oracle/dummy.res.oracle
+ 17
− 3
View file @ 32698b11
......@@ -3,8 +3,12 @@
[meta] Will process 6 properties
[meta] Successful translation
[wp] Running WP plugin...
[wp] [Valid] Goal RW_exits (Cfg) (Unreachable)
[wp] [Valid] Goal RW_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[wp] 39 goals scheduled
[wp] [Valid] Goal compute_exits (Cfg) (Unreachable)
[wp] [Valid] Goal compute_terminates (Cfg) (Trivial)
[wp] 41 goals scheduled
[wp] [Valid] typed_RW_ensures_strong_invariant_5_meta (Qed)
[wp] [Valid] typed_RW_assert_reading_2_meta (Qed)
[wp] [Valid] typed_RW_assert_writing_4_meta (Qed)
......@@ -23,8 +27,10 @@
[wp] [Valid] typed_compute_assigns_part4 (Qed)
[wp] [Valid] typed_compute_assigns_part5 (Alt-Ergo) (Cached)
[wp] [Valid] typed_compute_assigns_part6 (Qed)
[wp] [Valid] typed_main_terminates (Qed)
[wp] [Valid] typed_main_requires_strong_invariant_5_meta (Qed)
[wp] [Valid] typed_main_ensures_strong_invariant_5_meta (Qed)
[wp] [Valid] typed_main_exits (Qed)
[wp] [Valid] typed_main_assert_writing_3_meta (Qed)
[wp] [Valid] typed_main_assert_writing_4_meta (Qed)
[wp] [Valid] typed_main_assert_writing_6_meta (Qed)
......@@ -44,8 +50,10 @@
[wp] [Valid] typed_main_call_RW_requires_strong_invariant_5_meta (Qed)
[wp] [Valid] typed_main_call_compute_requires (Qed)
[wp] [Valid] typed_main_call_compute_requires_strong_invariant_5_meta (Qed)
[wp] Proved goals: 39 / 39
Qed: 38
[wp] Proved goals: 45 / 45
Terminating: 2
Unreachable: 2
Qed: 40
Alt-Ergo: 1
[wp] dummy.c:22: Warning:
Memory model hypotheses for function 'RW':
......@@ -73,6 +81,8 @@ struct SemiHidden STATE;
/*@ requires strong_invariant_5: meta: checkSum ≡ 1;
requires \valid(a);
requires \valid(b);
terminates \true;
exits \false;
ensures strong_invariant_5: meta: checkSum ≡ 1;
assigns *a;
*/
......@@ -87,6 +97,8 @@ void RW(int *a, int *b)
/*@ requires strong_invariant_5: meta: checkSum ≡ 1;
requires \valid(a);
terminates \true;
exits \false;
ensures strong_invariant_5: meta: checkSum ≡ 1;
assigns ROOT_BYTE;
*/
......@@ -111,6 +123,8 @@ int compute(int *a)
}
/*@ requires strong_invariant_5: meta: checkSum ≡ 1;
terminates \true;
exits \false;
ensures strong_invariant_5: meta: checkSum ≡ 1;
assigns INSTALL_BYTE, STATE.HIDDEN, ROOT_BYTE, checkSum;
*/
......
tests/meta-wp/oracle/forbidden.res.oracle
+ 8
− 2
View file @ 32698b11
......@@ -3,6 +3,8 @@
[meta] Will process 1 properties
[meta] Successful translation
[wp] Running WP plugin...
[wp] [Valid] Goal main_exits (Cfg) (Unreachable)
[wp] [Valid] Goal main_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
[wp] [Unsuccess] typed_main_assert_writing_1_meta (Alt-Ergo) (Cached)
......@@ -11,14 +13,18 @@
[wp] [Valid] typed_main_assert_writing_1_meta_4 (Alt-Ergo) (Cached)
[wp] [Valid] typed_main_assigns_part1 (Qed)
[wp] [Valid] typed_main_assigns_part2 (Qed)
[wp] Proved goals: 5 / 6
[wp] Proved goals: 7 / 8
Terminating: 1
Unreachable: 1
Qed: 2
Alt-Ergo: 3
Unsuccess: 1
/* Generated by Frama-C */
int a = 42;
int forbidden[2] = {42, 2713};
/*@ assigns a; */
/*@ terminates \true;
exits \false;
assigns a; */
int main(void)
{
int __retres;
......
tests/meta-wp/oracle/invariant.res.oracle
+ 34
− 5
View file @ 32698b11
......@@ -3,23 +3,38 @@
[meta] Will process 4 properties
[meta] Successful translation
[wp] Running WP plugin...
[kernel:annot:missing-spec] FRAMAC_SHARE/libc/assert.h:34: Warning:
Neither code nor explicit exits and terminates for function __FC_assert,
generating default clauses. See -generated-spec-* options for more info
[wp] [Valid] Goal breaksInv_exits (Cfg) (Unreachable)
[wp] [Valid] Goal breaksInv_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[wp] 27 goals scheduled
[wp] [Valid] Goal cond_exits (Cfg) (Unreachable)
[wp] [Valid] Goal cond_terminates (Cfg) (Trivial)
[wp] [Valid] Goal useless_exits (Cfg) (Unreachable)
[wp] [Valid] Goal useless_terminates (Cfg) (Trivial)
[wp] 33 goals scheduled
[wp] [Valid] typed_requiresInv_terminates (Qed)
[wp] [Valid] typed_requiresInv_ensures_invariant_2_meta (Qed)
[wp] [Valid] typed_requiresInv_exits (Qed)
[wp] [Valid] typed_requiresInv_assigns_exit (Qed)
[wp] [Valid] typed_requiresInv_assigns_normal (Qed)
[wp] [Valid] typed_requiresInv_call___FC_assert_FC_assert_requires_nonnull_c (Qed)
[wp] [Unsuccess] typed_breaksInv_ensures_invariant_2_meta (Alt-Ergo) (Cached)
[wp] [Valid] typed_breaksInv_assigns (Qed)
[wp] [Valid] typed_useless_assigns (Qed)
[wp] [Valid] typed_maintainsInv_terminates (Qed)
[wp] [Valid] typed_maintainsInv_ensures_invariant_2_meta (Alt-Ergo) (Cached)
[wp] [Valid] typed_maintainsInv_exits (Qed)
[wp] [Valid] typed_maintainsInv_assigns_exit (Qed)
[wp] [Valid] typed_maintainsInv_assigns_normal (Qed)
[wp] [Unsuccess] typed_cond_conditional_false_ensures_conditional_false_meta (Alt-Ergo) (Cached)
[wp] [Valid] typed_cond_assigns (Qed)
[wp] [Valid] typed_cond_conditional_true_ensures_conditional_true_meta (Qed)
[wp] [Valid] typed_main_terminates (Qed)
[wp] [Valid] typed_main_requires_strong_invariant_1_meta (Qed)
[wp] [Valid] typed_main_ensures_strong_invariant_1_meta (Qed)
[wp] [Valid] typed_main_exits (Qed)
[wp] [Valid] typed_main_assert_strong_invariant_1_meta (Qed)
[wp] [Valid] typed_main_assert_strong_invariant_1_meta_2 (Qed)
[wp] [Valid] typed_main_assert_strong_invariant_1_meta_3 (Qed)
......@@ -32,8 +47,10 @@
[wp] [Valid] typed_main_call_requiresInv_requires_invariant_2_meta (Qed)
[wp] [Valid] typed_main_call_breaksInv_requires_invariant_2_meta (Qed)
[wp] [Valid] typed_main_call_requiresInv_2_requires_invariant_2_meta (Qed)
[wp] Proved goals: 25 / 27
Qed: 23
[wp] Proved goals: 37 / 39
Terminating: 3
Unreachable: 3
Qed: 29
Alt-Ergo: 2
Unsuccess: 2
/* Generated by Frama-C */
......@@ -41,7 +58,9 @@
unsigned int A = (unsigned int)2;
unsigned int B;
/*@ requires invariant_2: meta: A % 2 ≡ 0;
terminates \true;
ensures invariant_2: meta: A % 2 ≡ 0;
exits \false;
assigns \nothing;
*/
void requiresInv(void)
......@@ -52,7 +71,9 @@ void requiresInv(void)
}
/*@ requires invariant_2: meta: A % 2 ≡ 0;
terminates \true;
ensures invariant_2: meta: A % 2 ≡ 0;
exits \false;
assigns A;
*/
void breaksInv(void)
......@@ -61,14 +82,18 @@ void breaksInv(void)
return;
}
/*@ assigns \nothing; */
/*@ terminates \true;
exits \false;
assigns \nothing; */
void useless(void)
{
return;
}
/*@ requires invariant_2: meta: A % 2 ≡ 0;
terminates \true;
ensures invariant_2: meta: A % 2 ≡ 0;
exits \false;
assigns A;
*/
void maintainsInv(void)
......@@ -78,7 +103,9 @@ void maintainsInv(void)
return;
}
/*@ assigns B;
/*@ terminates \true;
exits \false;
assigns B;
behavior conditional_false:
assumes conditional_false: meta: B ≡ 43;
......@@ -95,7 +122,9 @@ void cond(void)
}
/*@ requires strong_invariant_1: meta: A % 2 ≡ 0;
terminates \true;
ensures strong_invariant_1: meta: A % 2 ≡ 0;
exits \false;
assigns A, B;
*/
void main(void)
......
tests/meta-wp/oracle/loop_invariant.res.oracle
+ 14
− 5
View file @ 32698b11
......@@ -3,24 +3,31 @@
[meta] Will process 1 properties
[meta] Successful translation
[wp] Running WP plugin...
[wp] [Valid] Goal f_exits (Cfg) (Unreachable)
[wp] Warning: Missing RTE guards
[wp] 10 goals scheduled
[wp] 13 goals scheduled
[wp] [Unsuccess] typed_f_terminates (Alt-Ergo) (Cached)
[wp] [Valid] typed_f_ensures_strong_invariant_1_meta (Qed)
[wp] [Valid] typed_f_loop_invariant_strong_invariant_1_preserved (Qed)
[wp] [Valid] typed_f_loop_invariant_strong_invariant_1_established (Qed)
[wp] [Valid] typed_f_assert_strong_invariant_1_meta (Qed)
[wp] [Valid] typed_f_loop_assigns (Qed)
[wp] [Valid] typed_f_assigns (Qed)
[wp] [Valid] typed_main_terminates (Qed)
[wp] [Valid] typed_main_exits (Qed)
[wp] [Valid] typed_main_assigns_exit (Qed)
[wp] [Valid] typed_main_assigns_normal_part1 (Qed)
[wp] [Valid] typed_main_assigns_normal_part2 (Qed)
[wp] [Unsuccess] typed_main_call_f_requires_strong_invariant_1_meta (Alt-Ergo) (Cached)
[wp] Proved goals: 9 / 10
Qed: 9
Unsuccess: 1
[wp] Proved goals: 12 / 14
Unreachable: 1
Qed: 11
Unsuccess: 2
/* Generated by Frama-C */
int foo = 1;
/*@ requires strong_invariant_1: meta: foo > 0;
terminates \true;
exits \false;
ensures strong_invariant_1: meta: foo > 0;
assigns foo;
*/
......@@ -43,7 +50,9 @@ int f(void)
return foo;
}
/*@ assigns foo; */
/*@ terminates \true;
exits \false;
assigns foo; */
int main(void)
{
int __retres;
......
tests/meta-wp/oracle/monotony.res.oracle
+ 8
− 2
View file @ 32698b11
......@@ -3,6 +3,8 @@
[meta] Will process 1 properties
[meta] Successful translation
[wp] Running WP plugin...
[wp] [Valid] Goal main_exits (Cfg) (Unreachable)
[wp] [Valid] Goal main_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
[wp] [Valid] typed_main_assert_writing_1_meta (Qed)
......@@ -11,12 +13,16 @@
[wp] [Valid] typed_main_assert_writing_1_meta_4 (Qed)
[wp] [Valid] typed_main_assigns_part1 (Qed)
[wp] [Valid] typed_main_assigns_part2 (Qed)
[wp] Proved goals: 5 / 6
[wp] Proved goals: 7 / 8
Terminating: 1
Unreachable: 1
Qed: 5
Unsuccess: 1
/* Generated by Frama-C */
int a = 0;
/*@ assigns a; */
/*@ terminates \true;
exits \false;
assigns a; */
int main(void)
{
int __retres;
......
tests/meta-wp/oracle/options.0.res.oracle
+ 19
− 1
View file @ 32698b11
......@@ -3,7 +3,15 @@
[meta] Will process 5 properties
[meta] Successful translation
[wp] Running WP plugin...
[wp] [Valid] Goal f1_exits (Cfg) (Unreachable)
[wp] [Valid] Goal f1_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[wp] [Valid] Goal f2_exits (Cfg) (Unreachable)
[wp] [Valid] Goal f2_terminates (Cfg) (Trivial)
[wp] [Valid] Goal f3_exits (Cfg) (Unreachable)
[wp] [Valid] Goal f3_terminates (Cfg) (Trivial)
[wp] [Valid] Goal f4_exits (Cfg) (Unreachable)
[wp] [Valid] Goal f4_terminates (Cfg) (Trivial)
[wp] 13 goals scheduled
[wp] [Valid] typed_f1_ensures_test2_meta (Qed)
[wp] [Valid] typed_f1_assert_test2_meta (Qed)
......@@ -18,7 +26,9 @@
[wp] [Valid] typed_f4_assert_always_assert_meta (Qed)
[wp] [Unsuccess] typed_f4_assert_test2_meta (Alt-Ergo) (Cached)
[wp] [Valid] typed_f4_assigns (Qed)
[wp] Proved goals: 11 / 13
[wp] Proved goals: 19 / 21
Terminating: 4
Unreachable: 4
Qed: 11
Unsuccess: 2
/* Generated by Frama-C */
......@@ -30,8 +40,10 @@ int C;
int D;
/*@ requires test2: meta: C ≡ D;
requires test: meta: A ≡ B;
terminates \true;
ensures test2: meta: C ≡ D;
ensures test: meta: A ≡ B;
exits \false;
assigns A, B, C, D;
*/
void f1(void)
......@@ -55,8 +67,10 @@ void f1(void)
/*@ requires test2: meta: C ≡ D;
requires test: meta: A ≡ B;
terminates \true;
ensures test2: meta: C ≡ D;
ensures test: meta: A ≡ B;
exits \false;
assigns \nothing;
*/
void f2(void)
......@@ -66,8 +80,10 @@ void f2(void)
/*@ requires test2: meta: C ≡ D;
requires test: meta: A ≡ B;
terminates \true;
ensures test2: meta: C ≡ D;
ensures test: meta: A ≡ B;
exits \false;
assigns A;
*/
void f3(void)
......@@ -80,8 +96,10 @@ void f3(void)
/*@ requires test2: meta: C ≡ D;
requires test: meta: A ≡ B;
terminates \true;
ensures test2: meta: C ≡ D;
ensures test: meta: A ≡ B;
exits \false;
assigns C;
*/
void f4(void)
......
tests/meta-wp/oracle/options.1.res.oracle
+ 19
− 1
View file @ 32698b11
......@@ -3,7 +3,15 @@
[meta] Will process 5 properties
[meta] Successful translation
[wp] Running WP plugin...
[wp] [Valid] Goal f1_exits (Cfg) (Unreachable)
[wp] [Valid] Goal f1_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[wp] [Valid] Goal f2_exits (Cfg) (Unreachable)
[wp] [Valid] Goal f2_terminates (Cfg) (Trivial)
[wp] [Valid] Goal f3_exits (Cfg) (Unreachable)
[wp] [Valid] Goal f3_terminates (Cfg) (Trivial)
[wp] [Valid] Goal f4_exits (Cfg) (Unreachable)
[wp] [Valid] Goal f4_terminates (Cfg) (Trivial)
[wp] 13 goals scheduled
[wp] [Unsuccess] typed_f1_check_ensures_test2_meta (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_f1_check_test2_meta (Alt-Ergo) (Cached)
......@@ -18,7 +26,9 @@
[wp] [Unsuccess] typed_f4_assert_always_assert_meta (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_f4_check_test2_meta (Alt-Ergo) (Cached)
[wp] [Valid] typed_f4_assigns (Qed)
[wp] Proved goals: 4 / 13
[wp] Proved goals: 12 / 21
Terminating: 4
Unreachable: 4
Qed: 4
Unsuccess: 9
/* Generated by Frama-C */
......@@ -30,8 +40,10 @@ int C;
int D;
/*@ check requires test2: meta: C ≡ D;
check requires test: meta: A ≡ B;
terminates \true;
check ensures test2: meta: C ≡ D;
check ensures test: meta: A ≡ B;
exits \false;
assigns A, B, C, D;
*/
void f1(void)
......@@ -55,8 +67,10 @@ void f1(void)
/*@ check requires test2: meta: C ≡ D;
check requires test: meta: A ≡ B;
terminates \true;
check ensures test2: meta: C ≡ D;
check ensures test: meta: A ≡ B;
exits \false;
assigns \nothing;
*/
void f2(void)
......@@ -66,8 +80,10 @@ void f2(void)
/*@ check requires test2: meta: C ≡ D;
check requires test: meta: A ≡ B;
terminates \true;
check ensures test2: meta: C ≡ D;
check ensures test: meta: A ≡ B;
exits \false;
assigns A;
*/
void f3(void)
......@@ -80,8 +96,10 @@ void f3(void)
/*@ check requires test2: meta: C ≡ D;
check requires test: meta: A ≡ B;
terminates \true;
check ensures test2: meta: C ≡ D;
check ensures test: meta: A ≡ B;
exits \false;
assigns C;
*/
void f4(void)
......
tests/meta-wp/oracle/pre_label.res.oracle
+ 20
− 6
View file @ 32698b11
......@@ -4,26 +4,38 @@
[meta] Successful translation
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 7 goals scheduled
[wp] [Valid] Goal foo_exits (Cfg) (Unreachable)
[wp] [Valid] Goal foo_terminates (Cfg) (Trivial)
[wp] 11 goals scheduled
[wp] [Valid] typed_foo_assigns (Qed)
[wp] [Valid] typed_bar_terminates (Qed)
[wp] [Valid] typed_bar_exits (Qed)
[wp] [Valid] typed_bar_assert_calling_1_meta (Qed)
[wp] [Unsuccess] typed_bar_assert_calling_1_meta_2 (Alt-Ergo) (Cached)
[wp] [Valid] typed_bar_assigns_exit (Qed)
[wp] [Valid] typed_bar_assigns_normal (Qed)
[wp] [Valid] typed_main_terminates (Qed)
[wp] [Valid] typed_main_exits (Qed)
[wp] [Valid] typed_main_assigns_exit (Qed)
[wp] [Valid] typed_main_assigns_normal (Qed)
[wp] Proved goals: 6 / 7
Qed: 6
[wp] Proved goals: 12 / 13
Terminating: 1
Unreachable: 1
Qed: 10
Unsuccess: 1
/* Generated by Frama-C */
int x;
/*@ assigns \nothing; */
/*@ terminates \true;
exits \false;
assigns \nothing; */
void foo(void)
{
return;
}
/*@ assigns x; */
/*@ terminates \true;
exits \false;
assigns x; */
void bar(void)
{
if (x == 0)
......@@ -37,7 +49,9 @@ void bar(void)
return;
}
/*@ assigns x; */
/*@ terminates \true;
exits \false;
assigns x; */
void main(int a)
{
x = a;
......
tests/meta-wp/oracle/typing.res.oracle
+ 5
− 1
View file @ 32698b11
......@@ -3,11 +3,15 @@
[meta] Will process 1 properties
[meta] Successful translation
[wp] Running WP plugin...
[wp] [Valid] Goal f_exits (Cfg) (Unreachable)
[wp] [Valid] Goal f_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Valid] typed_f_assert_test_meta (Qed)
[wp] [Valid] typed_f_assigns (Qed)
[wp] Proved goals: 2 / 2
[wp] Proved goals: 4 / 4
Terminating: 1
Unreachable: 1
Qed: 2
------------------------------------------------------------
Function f
......
tests/meta-wp/uncalled.c
+ 1
− 1
View file @ 32698b11
/* run.config
OPT: @META@ @WP@ -wp-warn-key pedantic-assigns=inactive -then-last -eva -print
OPT: @META@ @WP@ -wp-warn-key pedantic-assigns=inactive -generated-spec-custom exits:skip,terminates:skip -then-last -eva -print
*/
void called() {
......
tests/wp-cache/cache/2201e41d911b00594c42d9e055fab137.json 0 → 100644
+ 1
− 0
View file @ 32698b11
{ "prover": "Alt-Ergo:2.4.2", "verdict": "timeout", "time": 1. }
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