From 35055ae7bbd9fae925fd5d4bd7f5b57bc59d71f7 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 13 Oct 2023 17:12:23 +0200
Subject: [PATCH] Update tests: WP now populates exits and terminates
---
tests/bugs/oracle/issue11.res.oracle | 28 ++++++++++---
tests/bugs/oracle/issue23.res.oracle | 8 +++-
tests/bugs/oracle/issue24.res.oracle | 8 +++-
tests/bugs/oracle/issue27-pred.res.oracle | 17 ++++++--
tests/bugs/oracle/logiccast.res.oracle | 12 +++++-
tests/bugs/oracle/term.res.oracle | 39 +++++++++++++------
tests/ppwp/oracle/expand.res.oracle | 10 ++++-
tests/ppwp/oracle/expandf.res.oracle | 10 ++++-
tests/ppwp/oracle/simple.res.oracle | 10 ++++-
tests/ppwp/oracle/z.res.oracle | 10 ++++-
tests/specs/oracle/wp_empty_struct.res.oracle | 6 ++-
11 files changed, 127 insertions(+), 31 deletions(-)
diff --git a/tests/bugs/oracle/issue11.res.oracle b/tests/bugs/oracle/issue11.res.oracle
index 68b823a9..e9a4cddb 100644
--- a/tests/bugs/oracle/issue11.res.oracle
+++ b/tests/bugs/oracle/issue11.res.oracle
@@ -2,12 +2,22 @@
[kernel] Parsing issue11.cpp (external front-end)
Now output intermediate result
[wp] Running WP plugin...
+[wp] [Valid] Goal ZN1a1bIcEEC1v_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal ZN1a1bIcEEC1v_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
-[wp] 2 goals scheduled
+[wp] [Valid] Goal ZN1a1bIvEEC1v_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal ZN1a1bIvEEC1v_terminates (Cfg) (Trivial)
+[wp] 6 goals scheduled
+[wp] [Valid] typed_fc_init_ZN1aE1c_terminates (Qed)
+[wp] [Valid] typed_fc_init_ZN1aE1c_exits (Qed)
[wp] [Valid] typed___fc_init_ZN1aE1c_call__ZN1a1bIvEEC1v_ZN1a1bIvEEC1v_requires (Qed)
+[wp] [Valid] typed_fc_init_ZN1aE1d_terminates (Qed)
+[wp] [Valid] typed_fc_init_ZN1aE1d_exits (Qed)
[wp] [Valid] typed___fc_init_ZN1aE1d_call__ZN1a1bIcEEC1v_ZN1a1bIcEEC1v_requires (Qed)
-[wp] Proved goals: 2 / 2
- Qed: 2
+[wp] Proved goals: 10 / 10
+ Terminating: 2
+ Unreachable: 2
+ Qed: 6
/* Generated by Frama-C */
struct _frama_c_vmt_content {
void (*method_ptr)() ;
@@ -40,7 +50,9 @@ void b<void>::Ctor(struct b<void> const *this);
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
-/*@ requires \valid_read(this); */
+/*@ requires \valid_read(this);
+ terminates \true;
+ exits \false; */
void b<void>::Ctor(struct b<void> const *this)
{
return;
@@ -55,7 +67,9 @@ void b<char>::Ctor(struct b<char> const *this);
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
-/*@ requires \valid_read(this); */
+/*@ requires \valid_read(this);
+ terminates \true;
+ exits \false; */
void b<char>::Ctor(struct b<char> const *this)
{
return;
@@ -67,6 +81,8 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
.number_of_base_classes = 0,
.pvmt = (struct _frama_c_vmt *)0};
struct b<void> c;
+/*@ terminates \true;
+ exits \false; */
void __fc_init_ZN1aE1c(void) __attribute__((__constructor__));
void __fc_init_ZN1aE1c(void)
{
@@ -75,6 +91,8 @@ void __fc_init_ZN1aE1c(void)
}
struct b<char> d;
+/*@ terminates \true;
+ exits \false; */
void __fc_init_ZN1aE1d(void) __attribute__((__constructor__));
void __fc_init_ZN1aE1d(void)
{
diff --git a/tests/bugs/oracle/issue23.res.oracle b/tests/bugs/oracle/issue23.res.oracle
index 7381b557..633ff616 100644
--- a/tests/bugs/oracle/issue23.res.oracle
+++ b/tests/bugs/oracle/issue23.res.oracle
@@ -2,11 +2,15 @@
[kernel] Parsing issue23.cpp (external front-end)
Now output intermediate result
[wp] Running WP plugin...
+[wp] [Valid] Goal Z1m_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal Z1m_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Valid] typed_Z1m_assert (Qed)
[wp] [Valid] typed_Z1m_assert_2 (Qed)
-[wp] Proved goals: 2 / 2
+[wp] Proved goals: 4 / 4
+ Terminating: 1
+ Unreachable: 1
Qed: 2
/* Generated by Frama-C */
struct _frama_c_vmt_content {
@@ -40,6 +44,8 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
.number_of_base_classes = 0,
.pvmt = (struct _frama_c_vmt *)0};
int i;
+/*@ terminates \true;
+ exits \false; */
void m(void)
{
i = 0;
diff --git a/tests/bugs/oracle/issue24.res.oracle b/tests/bugs/oracle/issue24.res.oracle
index c3f8560f..b8936432 100644
--- a/tests/bugs/oracle/issue24.res.oracle
+++ b/tests/bugs/oracle/issue24.res.oracle
@@ -2,6 +2,8 @@
[kernel] Parsing issue24.cpp (external front-end)
Now output intermediate result
[wp] Running WP plugin...
+[wp] [Valid] Goal Z1m_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal Z1m_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
[wp] [Valid] typed_Z1m_assert (Alt-Ergo) (Cached)
@@ -10,7 +12,9 @@ Now output intermediate result
[wp] [Valid] typed_Z1m_assert_4 (Qed)
[wp] [Valid] typed_Z1m_assert_5 (Qed)
[wp] [Valid] typed_Z1m_assert_6 (Alt-Ergo) (Cached)
-[wp] Proved goals: 6 / 6
+[wp] Proved goals: 8 / 8
+ Terminating: 1
+ Unreachable: 1
Qed: 2
Alt-Ergo: 4
/* Generated by Frama-C */
@@ -20,6 +24,8 @@ static int i;
/*@ predicate pos(ℤ k) = k < 0;
*/
int i;
+/*@ terminates \true;
+ exits \false; */
void m(void)
{
i = 0;
diff --git a/tests/bugs/oracle/issue27-pred.res.oracle b/tests/bugs/oracle/issue27-pred.res.oracle
index cb417645..19db6789 100644
--- a/tests/bugs/oracle/issue27-pred.res.oracle
+++ b/tests/bugs/oracle/issue27-pred.res.oracle
@@ -3,17 +3,26 @@
Now output intermediate result
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] 2 goals scheduled
+[wp] [Valid] Goal Z3posi_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal Z3posi_terminates (Cfg) (Trivial)
+[wp] 4 goals scheduled
[wp] [Valid] typed_Z3posi_ensures (Alt-Ergo) (Trivial)
[wp] [Valid] typed_Z3posi_ensures_2 (Alt-Ergo) (Cached)
-[wp] Proved goals: 2 / 2
+[wp] [Valid] typed_Z1mi_terminates (Qed)
+[wp] [Valid] typed_Z1mi_exits (Qed)
+[wp] Proved goals: 6 / 6
+ Terminating: 1
+ Unreachable: 1
+ Qed: 2
Alt-Ergo: 2
/* Generated by Frama-C */
/*@ predicate positive(int i) = i > 0;
*/
/*@ logic _Bool p(int i) = (_Bool)(i > 0? 1: 0);
*/
-/*@ ensures \result ≢ 0 ⇔ positive(\old(k));
+/*@ terminates \true;
+ exits \false;
+ ensures \result ≢ 0 ⇔ positive(\old(k));
ensures \result ≡ p(\old(k));
*/
_Bool pos(int k)
@@ -23,6 +32,8 @@ _Bool pos(int k)
return __retres;
}
+/*@ terminates \true;
+ exits \false; */
_Bool m(int k)
{
_Bool tmp;
diff --git a/tests/bugs/oracle/logiccast.res.oracle b/tests/bugs/oracle/logiccast.res.oracle
index 7e3a1a6c..2dbd5253 100644
--- a/tests/bugs/oracle/logiccast.res.oracle
+++ b/tests/bugs/oracle/logiccast.res.oracle
@@ -2,11 +2,17 @@
[kernel] Parsing logiccast.cpp (external front-end)
Now output intermediate result
[wp] Running WP plugin...
+[wp] [Valid] Goal Z1mPv_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal Z1mPv_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
+[wp] [Valid] Goal Z1nPc_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal Z1nPc_terminates (Cfg) (Trivial)
[wp] 2 goals scheduled
[wp] [Unsuccess] typed_Z1mPv_assert (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_Z1nPc_assert (Alt-Ergo) (Cached)
-[wp] Proved goals: 0 / 2
+[wp] Proved goals: 4 / 6
+ Terminating: 2
+ Unreachable: 2
Unsuccess: 2
[wp] logiccast.cpp:3: Warning:
Memory model hypotheses for function '_Z1mPv':
@@ -20,12 +26,16 @@ Now output intermediate result
void _Z1nPc(char *r);
/* Generated by Frama-C */
char *base;
+/*@ terminates \true;
+ exits \false; */
void m(void *r)
{
/*@ assert \subset(r, (void *)(base + (0 .. 1))); */ ;
return;
}
+/*@ terminates \true;
+ exits \false; */
void n(char *r)
{
/*@ assert \subset(r, (char *)((void *)(base + (0 .. 1)))); */ ;
diff --git a/tests/bugs/oracle/term.res.oracle b/tests/bugs/oracle/term.res.oracle
index f5ad26c0..8168060d 100644
--- a/tests/bugs/oracle/term.res.oracle
+++ b/tests/bugs/oracle/term.res.oracle
@@ -2,21 +2,32 @@
[kernel] Parsing term.cpp (external front-end)
Now output intermediate result
[wp] Running WP plugin...
+[wp] [Valid] Goal Z2m1_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal Z2m1_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
-[wp] [CFG] Goal Z2m2_terminates : Valid (Trivial)
-[wp] [CFG] Goal Z2m3_terminates : Valid (Trivial)
-[wp] [CFG] Goal Z2m4_terminates : Valid (Trivial)
-[wp] [CFG] Goal Z3m3a_terminates : Valid (Trivial)
-[wp] [CFG] Goal Z3m3b_terminates : Valid (Trivial)
+[wp] [Valid] Goal Z2m2_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal Z2m2_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal Z2m3_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal Z2m3_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal Z2m4_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal Z2m4_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal Z3m3a_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal Z3m3a_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal Z3m3b_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal Z3m3b_terminates (Cfg) (Trivial)
[wp] 3 goals scheduled
[wp] [Valid] typed_Z2m2_ensures (Qed)
[wp] [Valid] typed_Z2m3_c_ensures (Qed)
[wp] [Valid] typed_Z3m3a_c_ensures (Qed)
-[wp] Proved goals: 8 / 8
- Terminating: 5
+[wp] Proved goals: 15 / 15
+ Terminating: 6
+ Unreachable: 6
Qed: 3
/* Generated by Frama-C */
-/*@ behavior c:
+/*@ terminates \true;
+ exits \false;
+
+ behavior c:
requires \true; */
void m1(void)
{
@@ -25,6 +36,7 @@ void m1(void)
/*@ requires \true;
terminates \true;
+ exits \false;
ensures \true; */
void m2(void)
{
@@ -32,10 +44,12 @@ void m2(void)
}
/*@ terminates \true;
+ exits \false;
behavior c:
requires \true;
- ensures \true; */
+ ensures \true;
+ */
void m3(void)
{
return;
@@ -43,6 +57,7 @@ void m3(void)
/*@ requires \true;
terminates \true;
+ exits \false;
behavior c:
requires \true;
@@ -53,13 +68,15 @@ void m3a(void)
return;
}
-/*@ terminates \true; */
+/*@ terminates \true;
+ exits \false; */
void m3b(void)
{
return;
}
-/*@ terminates \true; */
+/*@ terminates \true;
+ exits \false; */
void m4(void)
{
return;
diff --git a/tests/ppwp/oracle/expand.res.oracle b/tests/ppwp/oracle/expand.res.oracle
index def23f83..26550523 100644
--- a/tests/ppwp/oracle/expand.res.oracle
+++ b/tests/ppwp/oracle/expand.res.oracle
@@ -2,13 +2,19 @@
[kernel] Parsing expand.cpp (external front-end)
Now output intermediate result
[wp] Running WP plugin...
+[wp] [Valid] Goal Z1m_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal Z1m_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Valid] typed_Z1m_ensures (Qed)
-[wp] Proved goals: 1 / 1
+[wp] Proved goals: 3 / 3
+ Terminating: 1
+ Unreachable: 1
Qed: 1
/* Generated by Frama-C */
-/*@ ensures 45 + 1 ≡ 46; */
+/*@ terminates \true;
+ exits \false;
+ ensures 45 + 1 ≡ 46; */
void m(void)
{
return;
diff --git a/tests/ppwp/oracle/expandf.res.oracle b/tests/ppwp/oracle/expandf.res.oracle
index 0cec7aa5..e54ea3b0 100644
--- a/tests/ppwp/oracle/expandf.res.oracle
+++ b/tests/ppwp/oracle/expandf.res.oracle
@@ -2,13 +2,19 @@
[kernel] Parsing expandf.cpp (external front-end)
Now output intermediate result
[wp] Running WP plugin...
+[wp] [Valid] Goal Z1m_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal Z1m_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Valid] typed_Z1m_ensures (Qed)
-[wp] Proved goals: 1 / 1
+[wp] Proved goals: 3 / 3
+ Terminating: 1
+ Unreachable: 1
Qed: 1
/* Generated by Frama-C */
-/*@ ensures 45 + 1 ≡ 46; */
+/*@ terminates \true;
+ exits \false;
+ ensures 45 + 1 ≡ 46; */
void m(void)
{
return;
diff --git a/tests/ppwp/oracle/simple.res.oracle b/tests/ppwp/oracle/simple.res.oracle
index d372c195..8aca2fdc 100644
--- a/tests/ppwp/oracle/simple.res.oracle
+++ b/tests/ppwp/oracle/simple.res.oracle
@@ -2,13 +2,19 @@
[kernel] Parsing simple.cpp (external front-end)
Now output intermediate result
[wp] Running WP plugin...
+[wp] [Valid] Goal Z1m_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal Z1m_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Valid] typed_Z1m_ensures (Qed)
-[wp] Proved goals: 1 / 1
+[wp] Proved goals: 3 / 3
+ Terminating: 1
+ Unreachable: 1
Qed: 1
/* Generated by Frama-C */
-/*@ ensures 45 + 1 ≡ 46; */
+/*@ terminates \true;
+ exits \false;
+ ensures 45 + 1 ≡ 46; */
void m(void)
{
return;
diff --git a/tests/ppwp/oracle/z.res.oracle b/tests/ppwp/oracle/z.res.oracle
index d8f05008..56620422 100644
--- a/tests/ppwp/oracle/z.res.oracle
+++ b/tests/ppwp/oracle/z.res.oracle
@@ -2,13 +2,19 @@
[kernel] Parsing z.cpp (external front-end)
Now output intermediate result
[wp] Running WP plugin...
+[wp] [Valid] Goal Z1m_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal Z1m_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Valid] typed_Z1m_ensures (Qed)
-[wp] Proved goals: 1 / 1
+[wp] Proved goals: 3 / 3
+ Terminating: 1
+ Unreachable: 1
Qed: 1
/* Generated by Frama-C */
-/*@ ensures ∀ ℤ n; n > 0 ∨ n ≤ 0; */
+/*@ terminates \true;
+ exits \false;
+ ensures ∀ ℤ n; n > 0 ∨ n ≤ 0; */
void m(void)
{
return;
diff --git a/tests/specs/oracle/wp_empty_struct.res.oracle b/tests/specs/oracle/wp_empty_struct.res.oracle
index c4a06f37..40b79e2c 100644
--- a/tests/specs/oracle/wp_empty_struct.res.oracle
+++ b/tests/specs/oracle/wp_empty_struct.res.oracle
@@ -2,9 +2,13 @@
[kernel] Parsing wp_empty_struct.cpp (external front-end)
Now output intermediate result
[wp] Running WP plugin...
+[wp] [Valid] Goal ZN6Point2E3foo_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal ZN6Point2E3foo_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Valid] typed_ZN6Point2E3foo_ensures (Qed)
[wp] [Valid] typed_ZN6Point2E3foo_ensures_2 (Qed)
-[wp] Proved goals: 2 / 2
+[wp] Proved goals: 4 / 4
+ Terminating: 1
+ Unreachable: 1
Qed: 2
--
GitLab