From da2e73dff7c29e9c202c6ca87b36e54be8c47168 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 9 Sep 2020 15:26:44 +0200
Subject: [PATCH] [spec] separate wp objectives from kernel ones in check test
---
tests/spec/generalized_check.i | 3 +-
.../oracle/generalized_check.0.res.oracle | 54 +------------------
.../oracle/generalized_check.1.res.oracle | 16 +++---
.../oracle/generalized_check.2.res.oracle | 51 ++++++++++++++++++
4 files changed, 63 insertions(+), 61 deletions(-)
create mode 100644 tests/spec/oracle/generalized_check.2.res.oracle
diff --git a/tests/spec/generalized_check.i b/tests/spec/generalized_check.i
index a343867864c..7f7c9748c53 100644
--- a/tests/spec/generalized_check.i
+++ b/tests/spec/generalized_check.i
@@ -1,6 +1,7 @@
/* run.config
-OPT: -wp -wp-prover qed -wp-msg-key no-cache-info,no-time-info -print
+OPT: -wp -wp-prover qed -wp-msg-key no-cache-info,no-time-info
OPT: -eva -eva-use-spec f
+OPT: -print
*/
/*@ check lemma easy_proof: \false; */ // should not be put in any environment
diff --git a/tests/spec/oracle/generalized_check.0.res.oracle b/tests/spec/oracle/generalized_check.0.res.oracle
index 96bfee08bea..a9fee931026 100644
--- a/tests/spec/oracle/generalized_check.0.res.oracle
+++ b/tests/spec/oracle/generalized_check.0.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing tests/spec/generalized_check.i (no preprocessing)
[wp] Running WP plugin...
-[wp] tests/spec/generalized_check.i:29: Warning:
+[wp] tests/spec/generalized_check.i:30: Warning:
Unsupported generalized invariant, use loop invariant instead.
Ignored invariant
check invariant \true;
[wp] Warning: Missing RTE guards
-[wp] tests/spec/generalized_check.i:36: Warning:
+[wp] tests/spec/generalized_check.i:37: Warning:
Missing assigns clause (assigns 'everything' instead)
[wp] 11 goals scheduled
[wp] [Qed] Goal typed_f_assigns : Valid
@@ -21,53 +21,3 @@
[wp] [Failed] Goal typed_main_check_main_valid_ko
[wp] Proved goals: 3 / 11
Qed: 3
-/* Generated by Frama-C */
-/*@ check lemma easy_proof: \false;
- */
-/*@ check requires f_valid_x: \valid(x);
- check ensures f_init_x: *\old(x) ≡ 0;
- assigns *x;
- */
-void f(int *x)
-{
- /*@ check f_valid_ko: \valid(x); */ ;
- *x = 0;
- return;
-}
-
-void loop(void);
-
-int main(void)
-{
- int __retres;
- int volatile c;
- int a = 4;
- int *p = (int *)0;
- if (c) p = & a;
- f(p);
- /*@ check main_valid_ko: \valid(p); */ ;
- /*@ check main_p_content_ko: *p ≡ 0; */ ;
- loop();
- __retres = 0;
- return __retres;
-}
-
-void loop(void)
-{
- int j = 0;
- {
- int i = 0;
- /*@ check loop invariant false_but_preserved: j ≡ 10;
- loop assigns i; */
- while (i < 10) i ++;
- }
- /*@ check implied_by_false_invariant: j ≡ 10; */ ;
- l: /*@ check invariant \true; */ ;
- if (j >= 10) goto l1;
- j ++;
- goto l;
- l1: ;
- return;
-}
-
-
diff --git a/tests/spec/oracle/generalized_check.1.res.oracle b/tests/spec/oracle/generalized_check.1.res.oracle
index e160c9b946f..f93e7228b40 100644
--- a/tests/spec/oracle/generalized_check.1.res.oracle
+++ b/tests/spec/oracle/generalized_check.1.res.oracle
@@ -4,21 +4,21 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva:alarm] tests/spec/generalized_check.i:22: Warning:
+[eva:alarm] tests/spec/generalized_check.i:23: Warning:
accessing uninitialized left-value. assert \initialized(&c);
[eva] using specification for function f
-[eva:alarm] tests/spec/generalized_check.i:23: Warning:
+[eva:alarm] tests/spec/generalized_check.i:24: Warning:
function f: precondition 'f_valid_x' got status unknown.
-[eva] tests/spec/generalized_check.i:8: Warning:
+[eva] tests/spec/generalized_check.i:9: Warning:
no \from part for clause 'assigns *x;'
-[eva:alarm] tests/spec/generalized_check.i:24: Warning:
- check 'main_valid_ko' got status unknown.
[eva:alarm] tests/spec/generalized_check.i:25: Warning:
+ check 'main_valid_ko' got status unknown.
+[eva:alarm] tests/spec/generalized_check.i:26: Warning:
check 'main_p_content_ko' got status unknown.
-[eva:alarm] tests/spec/generalized_check.i:31: Warning:
+[eva:alarm] tests/spec/generalized_check.i:32: Warning:
loop invariant 'false_but_preserved' got status invalid.
-[eva] tests/spec/generalized_check.i:34: starting to merge loop iterations
-[eva:alarm] tests/spec/generalized_check.i:35: Warning:
+[eva] tests/spec/generalized_check.i:35: starting to merge loop iterations
+[eva:alarm] tests/spec/generalized_check.i:36: Warning:
check 'implied_by_false_invariant' got status invalid.
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/spec/oracle/generalized_check.2.res.oracle b/tests/spec/oracle/generalized_check.2.res.oracle
new file mode 100644
index 00000000000..dd870d5dc00
--- /dev/null
+++ b/tests/spec/oracle/generalized_check.2.res.oracle
@@ -0,0 +1,51 @@
+[kernel] Parsing tests/spec/generalized_check.i (no preprocessing)
+/* Generated by Frama-C */
+/*@ check lemma easy_proof: \false;
+ */
+/*@ check requires f_valid_x: \valid(x);
+ check ensures f_init_x: *\old(x) ≡ 0;
+ assigns *x;
+ */
+void f(int *x)
+{
+ /*@ check f_valid_ko: \valid(x); */ ;
+ *x = 0;
+ return;
+}
+
+void loop(void);
+
+int main(void)
+{
+ int __retres;
+ int volatile c;
+ int a = 4;
+ int *p = (int *)0;
+ if (c) p = & a;
+ f(p);
+ /*@ check main_valid_ko: \valid(p); */ ;
+ /*@ check main_p_content_ko: *p ≡ 0; */ ;
+ loop();
+ __retres = 0;
+ return __retres;
+}
+
+void loop(void)
+{
+ int j = 0;
+ {
+ int i = 0;
+ /*@ check loop invariant false_but_preserved: j ≡ 10;
+ loop assigns i; */
+ while (i < 10) i ++;
+ }
+ /*@ check implied_by_false_invariant: j ≡ 10; */ ;
+ l: /*@ check invariant \true; */ ;
+ if (j >= 10) goto l1;
+ j ++;
+ goto l;
+ l1: ;
+ return;
+}
+
+
--
GitLab