From 46068928fd13140036c0d5db6eec5384aaf30ec7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 15 Feb 2021 17:31:37 +0100
Subject: [PATCH] [wp] removed stmt-contract
---
src/plugins/wp/tests/wp_usage/code_spec.i | 28 -------------------
.../wp_usage/oracle/code_spec.res.oracle | 10 ++-----
2 files changed, 2 insertions(+), 36 deletions(-)
diff --git a/src/plugins/wp/tests/wp_usage/code_spec.i b/src/plugins/wp/tests/wp_usage/code_spec.i
index 30c1819dcc1..f3a491fd9be 100644
--- a/src/plugins/wp/tests/wp_usage/code_spec.i
+++ b/src/plugins/wp/tests/wp_usage/code_spec.i
@@ -53,34 +53,6 @@ void by_array_in_code(int *p, int *q, int **qq) {
p1[p2[0]]=*(p3+p4[*(p5+1)]);
}
//-------------------------------------------------------
-void by_value_in_code_annotation(int v, int *p, int*q) {
- //@ assert tab[v-1]==0 && \initialized (&x6);
- /*@ requires (x1?x2:x3)== 0;
- @ assigns x4;
- @*/
- /*@ loop invariant x5<0;
- @ loop variant q-p;
- @*/
- while (1)
- //@ assert 0 == \let term=1+\at(x7,Pre) ; 1+term;
- //@ assert \let pred=(x8==0) ; pred && x9==0;
- ;
-}
-
-//@ behavior no_exit: exits \false;
-void by_reference_in_code_annotation(int*p) {
- //@ for no_exit: assert \valid (p);
- //@ ensures \separated (p1,p2) && \freeable (p3) || \allocable (p5) <==> \initialized (p6);
- ;
- //@ loop invariant *p4<0;
- while (1);
-}
-
-void by_addr_in_code_annotation(void) {
- //@ requires (&x0 != &s0.c) && &tab[5];
- return;
-}
-
void by_array_in_code_annotation(int *p, int *q, int **qq) {
//@ assert *(ptr+1)==0 && *(p+1)==q[0] && p1[p2[0]]==*(p3+p4[*(p5+1)]);
;
diff --git a/src/plugins/wp/tests/wp_usage/oracle/code_spec.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/code_spec.res.oracle
index 253cb2dea90..e4ec1c30595 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/code_spec.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/code_spec.res.oracle
@@ -1,9 +1,9 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_usage/code_spec.i (no preprocessing)
[wp] Running WP plugin...
-[kernel] tests/wp_usage/code_spec.i:154: Warning:
+[kernel] tests/wp_usage/code_spec.i:126: Warning:
No code nor implicit assigns clause for function by_addr_in_spec, generating default assigns from the prototype
-[kernel] tests/wp_usage/code_spec.i:154: Warning:
+[kernel] tests/wp_usage/code_spec.i:126: Warning:
No code nor implicit assigns clause for function by_array_in_spec, generating default assigns from the prototype
.................................................
... Ref Usage
@@ -16,10 +16,6 @@ Function by_value_in_code:
Function by_reference_in_code: { *p1 *p *qq }
Function by_addr_in_code: { &x0 &s0 &tab &v1 &s2 &s3 }
Function by_array_in_code: { p1[] p2[] p3[] p4[] p5[] ptr[] p[] q[] }
-Function by_value_in_code_annotation:
-{ x1 x2 x3 x4 x5 x6 x7 x8 x9 tab v p q }
-Function by_reference_in_code_annotation: { *p1 *p2 *p3 *p4 *p5 *p6 *p }
-Function by_addr_in_code_annotation: { &x0 &s0 &tab }
Function by_array_in_code_annotation:
{ p1[] p2[] p3[] p4[] p5[] ptr[] p[] q[] }
Function by_value_in_spec: { x0 x1 p0 p1 p2 }
@@ -39,7 +35,5 @@ Function calling_spec:
Function cup:
{ val *ref &addr array[] &addr_value val_ref array_ref[] value_array }
.................................................
-[wp] [CFG] Goal by_addr_in_code_annotation_requires : Valid (Unreachable)
-[wp] [CFG] Goal by_reference_in_code_annotation_no_exit_exits : Valid (Unreachable)
[wp] Warning: Missing RTE guards
[wp] No proof obligations
--
GitLab