From d0a573906fcc96fb91f448b958c9f75b2b8921ff Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?C=C3=A9cile=20RUET-CROS?= <cecile.ruet-cros@cea.fr>
Date: Tue, 8 Oct 2024 16:31:09 +0200
Subject: [PATCH] [wp/region] test record + bug fixes range
---
src/plugins/region/ranges.ml | 4 +-
.../tests/region/oracle/fb_SORT.res.oracle | 23 ++-
.../tests/wp_region/oracle/record.res.oracle | 183 ++++++++++++++++++
.../wp_region/oracle_qualif/record.res.oracle | 128 ++++++++++++
src/plugins/wp/tests/wp_region/record.c | 24 +++
5 files changed, 353 insertions(+), 9 deletions(-)
create mode 100644 src/plugins/wp/tests/wp_region/oracle/record.res.oracle
create mode 100644 src/plugins/wp/tests/wp_region/oracle_qualif/record.res.oracle
create mode 100644 src/plugins/wp/tests/wp_region/record.c
diff --git a/src/plugins/region/ranges.ml b/src/plugins/region/ranges.ml
index 54e7cc2c43f..3e9dbed60ea 100644
--- a/src/plugins/region/ranges.ml
+++ b/src/plugins/region/ranges.ml
@@ -57,7 +57,7 @@ let range ?(offset=0) ?(length=1) data = singleton { offset ; length ; data }
let rec find (k: int) = function
| [] -> raise Not_found
| ({ offset ; length } as r) :: rs ->
- if offset <= k && k <= offset + length then r else find k rs
+ if offset <= k && k < offset + length then r else find k rs
let find k (R rs) = find k rs
@@ -70,7 +70,7 @@ let rec merge f ra rb =
if a' <= b.offset then
a :: merge f wa rb
else
- if b' < a.offset then
+ if b' <= a.offset then
b :: merge f ra wb
else
let offset = min a.offset b.offset in
diff --git a/src/plugins/region/tests/region/oracle/fb_SORT.res.oracle b/src/plugins/region/tests/region/oracle/fb_SORT.res.oracle
index 4de3c9517db..586a487686d 100644
--- a/src/plugins/region/tests/region/oracle/fb_SORT.res.oracle
+++ b/src/plugins/region/tests/region/oracle/fb_SORT.res.oracle
@@ -4,14 +4,19 @@
R0003: R-- fb (FB *) 64b (*R0005) ;
R0005: --- 704b
{
- .prm.inp1: R0007[2];
+ .prm: R002e;
+ .inp1: R0007;
#128b;
.out1: R000f;
.out2: R006a;
- .out3.idx1: R0017[2];
+ .out3: R0074;
+ .idx1: R0017;
#128b;
.sum: R0057;
} ;
+ R002e: R-- (struct N *) 64b (*R0031) ;
+ R0031: --- 128b { .v: R0033; #64b; } ;
+ R0033: R-- (double) 64b ;
R0007: R-- (struct N *) 64b (*R0027) ;
R0027: --- 128b { .v: R0029; .s: R0049; #32b; } ;
R0029: R-- (double) 64b ;
@@ -23,13 +28,17 @@
R006a: R-- (struct N *) 64b (*R006d) ;
R006d: --- 128b { .v: R006f; #64b; } ;
R006f: R-- (double) 64b ;
- R0017: R-- (struct N *) (struct L *) 64b (*R0041) ;
- R0041: --- 64b { .v.s: R0043[2]; } ;
- R0043: RW- (int) (double) 32b ;
+ R0074: R-- (struct N *) 64b (*R0077) ;
+ R0077: --- 128b { .v: R0079; #64b; } ;
+ R0079: R-- (double) 64b ;
+ R0017: R-- (struct L *) 64b (*R0041) ;
+ R0041: --- 64b { .v: R0043; .s: R0052; } ;
+ R0043: -W- (int) 32b ;
+ R0052: -W- (int) 32b ;
R0057: R-- (struct N *) 64b (*R005a) ;
- R005a: --- 128b { .v: R005c; .s: R0083; #32b; } ;
+ R005a: --- 128b { .v: R005c; .s: R0084; #32b; } ;
R005c: -W- (double) 64b ;
- R0083: -W- (int) 32b ;
+ R0084: -W- (int) 32b ;
R0001: RWA inp (SN *) 64b (*R0007) ;
R000b: RWA out (SN *) 64b (*R000f) ;
R0013: RWA idx (SL *) 64b (*R0017) ;
diff --git a/src/plugins/wp/tests/wp_region/oracle/record.res.oracle b/src/plugins/wp/tests/wp_region/oracle/record.res.oracle
new file mode 100644
index 00000000000..7ba53f1df82
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/oracle/record.res.oracle
@@ -0,0 +1,183 @@
+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing record.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal f_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal f_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+------------------------------------------------------------
+ Function f
+------------------------------------------------------------
+
+Goal Post-condition (file record.c, line 12) in 'f':
+Let a = shiftfield_F1_S_g(q).
+Let a_1 = shiftfield_F1_S_f(p).
+Let x = Msint32_0[a_1].
+Let x_1 = 1 + x.
+Let m = Msint32_0[a_1 <- x_1].
+Let a_2 = shiftfield_F1_S_f(q).
+Let x_2 = m[a_2].
+Let x_3 = m[a_2 <- x_2 - 1][a_1].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_2) /\ is_sint32(x_3).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ (region(q.base) <= 0) /\ framed(mem_0) /\
+ sconst(mem_0).
+ (* Goal *)
+ When: q != p.
+ (* Pre-condition *)
+ Have: P_pointed(p, q).
+ (* Assertion *)
+ Have: read_sint32(write_sint16(write_sint16(mem_0, shift_sint16(a, 0), -1),
+ shift_sint16(a, 1), -1), a) = (-1).
+}
+Prove: x_3 = x_1.
+
+------------------------------------------------------------
+
+Goal Post-condition (file record.c, line 13) in 'f':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition (file record.c, line 14) in 'f':
+Let a = shiftfield_F1_S_g(q).
+Let m = write_sint16(write_sint16(mem_0, shift_sint16(a, 0), -1),
+ shift_sint16(a, 1), -1).
+Let x = read_sint32(write_sint32(m, a, 0), a).
+Assume {
+ Type: is_sint32(x).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ (region(q.base) <= 0) /\ framed(mem_0) /\
+ sconst(mem_0).
+ (* Pre-condition *)
+ Have: P_pointed(p, q).
+ (* Assertion *)
+ Have: read_sint32(m, a) = (-1).
+}
+Prove: x = 0.
+
+------------------------------------------------------------
+
+Goal Assertion (file record.c, line 22):
+Let a = shiftfield_F1_S_g(q).
+Let x = read_sint32(write_sint16(write_sint16(mem_0, shift_sint16(a, 0), -1),
+ shift_sint16(a, 1), -1), a).
+Assume {
+ Type: is_sint32(x).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ (region(q.base) <= 0) /\ framed(mem_0) /\
+ sconst(mem_0).
+ (* Pre-condition *)
+ Have: P_pointed(p, q).
+}
+Prove: x = (-1).
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/record.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/record.res.oracle
new file mode 100644
index 00000000000..cc8d40d8228
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/record.res.oracle
@@ -0,0 +1,128 @@
+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing record.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal f_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal f_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[region] record.c:22: Warning: Annotations not analyzed
+[wp] 4 goals scheduled
+[wp] [Valid] region_f_ensures (Alt-Ergo) (Cached)
+[wp] [Valid] region_f_ensures_2 (Qed)
+[wp] [Valid] region_f_ensures_3 (Alt-Ergo) (Cached)
+[wp] [Valid] region_f_assert (Alt-Ergo) (Cached)
+[wp] Proved goals: 6 / 6
+ Terminating: 1
+ Unreachable: 1
+ Qed: 1
+ Alt-Ergo: 3
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ f 1 3 4 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/record.c b/src/plugins/wp/tests/wp_region/record.c
new file mode 100644
index 00000000000..10da25acbd0
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/record.c
@@ -0,0 +1,24 @@
+struct S {
+ int f;
+ int g;
+};
+
+/*@ predicate pointed(struct S *p, struct S * q) = p==q || \separated(p,q);
+*/
+
+
+/*@ requires pointed(p,q);
+ region PQf: p->f, q->f;
+ ensures p != q ==> p->f == \old(p->f) + 1;
+ ensures p == q ==> p->f == \old(p->f);
+ ensures q->g == 0;
+@*/
+void f (struct S *p, struct S *q) {
+ (p->f)++;
+ (q->f)--;
+ short *r = &(q->g);
+ r[0] = -1;
+ r[1] = -1;
+ //@ assert q->g == -1;
+ (q->g)++;
+}
--
GitLab