From f456c7b7b3060f8f1c01aa0c26b13d6f8cf4010f Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 22 Sep 2020 14:15:14 +0200
Subject: [PATCH] [wp] More tests on base_offset
---
src/plugins/wp/tests/wp_acsl/base_offset.i | 13 +++++++++++++
.../wp/tests/wp_acsl/oracle/base_offset.res.oracle | 13 +++++++++++++
.../wp_acsl/oracle_qualif/base_offset.res.oracle | 9 ++++++---
3 files changed, 32 insertions(+), 3 deletions(-)
diff --git a/src/plugins/wp/tests/wp_acsl/base_offset.i b/src/plugins/wp/tests/wp_acsl/base_offset.i
index e4e96b65f5c..f38f29df60f 100644
--- a/src/plugins/wp/tests/wp_acsl/base_offset.i
+++ b/src/plugins/wp/tests/wp_acsl/base_offset.i
@@ -16,3 +16,16 @@ struct S* p ;
\offset( &p->a[i] ) <= \offset( &p->a[j] ) ;
*/
void f(void){return;}
+
+struct { int a ; int b ; } x ;
+struct { int a ; int b ; } y ;
+struct { double a ; int b ; } z ;
+
+void g(void){
+ int *xb = &x.b;
+ int *yb = &y.b;
+ int *zb = &z.b;
+
+ //@ check KO: \offset(xb) == \offset(zb) ;
+ //@ check KO: \offset(xb) != \offset(yb) ;
+}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle
index fcc2455baea..3876073ea1f 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle
@@ -29,3 +29,16 @@ Assume {
Prove: base_offset(x_1, 1 + i + x_2) <= base_offset(x_1, 1 + i_1 + x_2).
------------------------------------------------------------
+------------------------------------------------------------
+ Function g
+------------------------------------------------------------
+
+Goal Check 'KO' (file tests/wp_acsl/base_offset.i, line 29):
+Prove: base_offset_table(G_z_33) = base_offset_table(G_x_31).
+
+------------------------------------------------------------
+
+Goal Check 'KO' (file tests/wp_acsl/base_offset.i, line 30):
+Prove: base_offset_table(G_y_32) != base_offset_table(G_x_31).
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle
index 8b29211f4ec..05b7c9c11f2 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle
@@ -2,14 +2,17 @@
[kernel] Parsing tests/wp_acsl/base_offset.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] 3 goals scheduled
+[wp] 5 goals scheduled
[wp] [Qed] Goal typed_f_ensures : Valid
[wp] [Qed] Goal typed_f_ensures_2 : Valid
[wp] [Alt-Ergo] Goal typed_f_ensures_3 : Valid
-[wp] Proved goals: 3 / 3
+[wp] [Alt-Ergo] Goal typed_g_check_KO : Unsuccess
+[wp] [Alt-Ergo] Goal typed_g_check_KO_2 : Unsuccess
+[wp] Proved goals: 3 / 5
Qed: 2
- Alt-Ergo: 1
+ Alt-Ergo: 1 (unsuccess: 2)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
f 2 1 3 100%
+ g - - 2 0.0%
------------------------------------------------------------
--
GitLab