From 32698b11a42f1714b35fe2e925093c36d882a710 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 13 Oct 2023 17:29:02 +0200
Subject: [PATCH] Update tests: WP now populates terminates and exits
---
.../meta-deduce/oracle/consequence.res.oracle | 40 ++++++++++++++----
.../oracle/negative_assigns.res.oracle | 41 ++++++++++++++-----
.../meta-wp/oracle/assert_type_of.res.oracle | 22 ++++++++--
.../oracle/axiomatic_requires.res.oracle | 25 ++++++++---
tests/meta-wp/oracle/dummy.res.oracle | 20 +++++++--
tests/meta-wp/oracle/forbidden.res.oracle | 10 ++++-
tests/meta-wp/oracle/invariant.res.oracle | 39 +++++++++++++++---
.../meta-wp/oracle/loop_invariant.res.oracle | 19 ++++++---
tests/meta-wp/oracle/monotony.res.oracle | 10 ++++-
tests/meta-wp/oracle/options.0.res.oracle | 20 ++++++++-
tests/meta-wp/oracle/options.1.res.oracle | 20 ++++++++-
tests/meta-wp/oracle/pre_label.res.oracle | 26 +++++++++---
tests/meta-wp/oracle/typing.res.oracle | 6 ++-
tests/meta-wp/uncalled.c | 2 +-
.../2201e41d911b00594c42d9e055fab137.json | 1 +
15 files changed, 248 insertions(+), 53 deletions(-)
create mode 100644 tests/wp-cache/cache/2201e41d911b00594c42d9e055fab137.json
diff --git a/tests/meta-deduce/oracle/consequence.res.oracle b/tests/meta-deduce/oracle/consequence.res.oracle
index 55c9139..a07a7fd 100644
--- a/tests/meta-deduce/oracle/consequence.res.oracle
+++ b/tests/meta-deduce/oracle/consequence.res.oracle
@@ -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();
diff --git a/tests/meta-deduce/oracle/negative_assigns.res.oracle b/tests/meta-deduce/oracle/negative_assigns.res.oracle
index 263b8ed..fe34313 100644
--- a/tests/meta-deduce/oracle/negative_assigns.res.oracle
+++ b/tests/meta-deduce/oracle/negative_assigns.res.oracle
@@ -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;
diff --git a/tests/meta-wp/oracle/assert_type_of.res.oracle b/tests/meta-wp/oracle/assert_type_of.res.oracle
index 56bfe98..1cceb3e 100644
--- a/tests/meta-wp/oracle/assert_type_of.res.oracle
+++ b/tests/meta-wp/oracle/assert_type_of.res.oracle
@@ -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;
diff --git a/tests/meta-wp/oracle/axiomatic_requires.res.oracle b/tests/meta-wp/oracle/axiomatic_requires.res.oracle
index 222c182..95fdc3f 100644
--- a/tests/meta-wp/oracle/axiomatic_requires.res.oracle
+++ b/tests/meta-wp/oracle/axiomatic_requires.res.oracle
@@ -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();
diff --git a/tests/meta-wp/oracle/dummy.res.oracle b/tests/meta-wp/oracle/dummy.res.oracle
index 5a612e8..b75f063 100644
--- a/tests/meta-wp/oracle/dummy.res.oracle
+++ b/tests/meta-wp/oracle/dummy.res.oracle
@@ -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;
*/
diff --git a/tests/meta-wp/oracle/forbidden.res.oracle b/tests/meta-wp/oracle/forbidden.res.oracle
index 86204bf..1b3bb8e 100644
--- a/tests/meta-wp/oracle/forbidden.res.oracle
+++ b/tests/meta-wp/oracle/forbidden.res.oracle
@@ -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;
diff --git a/tests/meta-wp/oracle/invariant.res.oracle b/tests/meta-wp/oracle/invariant.res.oracle
index e9af94d..493ac54 100644
--- a/tests/meta-wp/oracle/invariant.res.oracle
+++ b/tests/meta-wp/oracle/invariant.res.oracle
@@ -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)
diff --git a/tests/meta-wp/oracle/loop_invariant.res.oracle b/tests/meta-wp/oracle/loop_invariant.res.oracle
index fe35cb8..d2934ad 100644
--- a/tests/meta-wp/oracle/loop_invariant.res.oracle
+++ b/tests/meta-wp/oracle/loop_invariant.res.oracle
@@ -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;
diff --git a/tests/meta-wp/oracle/monotony.res.oracle b/tests/meta-wp/oracle/monotony.res.oracle
index 298326e..7efb264 100644
--- a/tests/meta-wp/oracle/monotony.res.oracle
+++ b/tests/meta-wp/oracle/monotony.res.oracle
@@ -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;
diff --git a/tests/meta-wp/oracle/options.0.res.oracle b/tests/meta-wp/oracle/options.0.res.oracle
index c46b295..9155103 100644
--- a/tests/meta-wp/oracle/options.0.res.oracle
+++ b/tests/meta-wp/oracle/options.0.res.oracle
@@ -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)
diff --git a/tests/meta-wp/oracle/options.1.res.oracle b/tests/meta-wp/oracle/options.1.res.oracle
index 545427c..2f05e1b 100644
--- a/tests/meta-wp/oracle/options.1.res.oracle
+++ b/tests/meta-wp/oracle/options.1.res.oracle
@@ -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)
diff --git a/tests/meta-wp/oracle/pre_label.res.oracle b/tests/meta-wp/oracle/pre_label.res.oracle
index 7a42dd6..65d46bd 100644
--- a/tests/meta-wp/oracle/pre_label.res.oracle
+++ b/tests/meta-wp/oracle/pre_label.res.oracle
@@ -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;
diff --git a/tests/meta-wp/oracle/typing.res.oracle b/tests/meta-wp/oracle/typing.res.oracle
index a23a64a..d12269e 100644
--- a/tests/meta-wp/oracle/typing.res.oracle
+++ b/tests/meta-wp/oracle/typing.res.oracle
@@ -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
diff --git a/tests/meta-wp/uncalled.c b/tests/meta-wp/uncalled.c
index 9ab4023..4650922 100644
--- a/tests/meta-wp/uncalled.c
+++ b/tests/meta-wp/uncalled.c
@@ -1,5 +1,5 @@
/* 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() {
diff --git a/tests/wp-cache/cache/2201e41d911b00594c42d9e055fab137.json b/tests/wp-cache/cache/2201e41d911b00594c42d9e055fab137.json
new file mode 100644
index 0000000..0d952f7
--- /dev/null
+++ b/tests/wp-cache/cache/2201e41d911b00594c42d9e055fab137.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.4.2", "verdict": "timeout", "time": 1. }
--
GitLab