From 84cfb470f7c5a4aae58c076fb0587aaa484744ce Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 17 Nov 2020 11:48:26 +0100
Subject: [PATCH] [wp] Moves a test from kernel to WP
---
.../wp/tests/wp_acsl/generalized_checks.i | 14 +++
.../oracle/generalized_checks.res.oracle | 31 ++++++
.../generalized_checks.res.oracle | 19 +++-
tests/spec/generalized_check.i | 2 +-
.../oracle/generalized_check.0.res.oracle | 69 ++++++++-----
.../oracle/generalized_check.1.res.oracle | 96 ++++++++++---------
.../oracle/generalized_check.2.res.oracle | 51 ----------
7 files changed, 157 insertions(+), 125 deletions(-)
delete mode 100644 tests/spec/oracle/generalized_check.2.res.oracle
diff --git a/src/plugins/wp/tests/wp_acsl/generalized_checks.i b/src/plugins/wp/tests/wp_acsl/generalized_checks.i
index 3b34ced34e2..88b32e9f49a 100644
--- a/src/plugins/wp/tests/wp_acsl/generalized_checks.i
+++ b/src/plugins/wp/tests/wp_acsl/generalized_checks.i
@@ -64,3 +64,17 @@ int caller(int x)
{
return job(x); // CA2 is not proved
}
+
+void loop () {
+ int j = 0;
+ /*@ check loop invariant false_but_preserved: j == 10;
+ loop assigns i;
+ */
+ for (int i = 0; i< 10; i++);
+ /*@ check implied_by_false_invariant: j == 10; */
+ l: /*@ check invariant \true; */ ;
+ if (j >= 10) goto l1;
+ j++;
+ goto l;
+ l1 : ;
+}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle
index 233aa076c4f..d3f8259be9d 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle
@@ -1,7 +1,13 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/generalized_checks.i (no preprocessing)
[wp] Running WP plugin...
+[wp] tests/wp_acsl/generalized_checks.i:68: Warning:
+ Unsupported generalized invariant, use loop invariant instead.
+ Ignored invariant
+ check invariant \true;
[wp] Warning: Missing RTE guards
+[wp] tests/wp_acsl/generalized_checks.i:75: Warning:
+ Missing assigns clause (assigns 'everything' instead)
------------------------------------------------------------
Axiomatic 'Th'
------------------------------------------------------------
@@ -136,3 +142,28 @@ Call Result at line 52
Prove: true.
------------------------------------------------------------
+------------------------------------------------------------
+ Function loop
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'false_but_preserved' (file tests/wp_acsl/generalized_checks.i, line 70):
+Assume { Type: is_sint32(i). (* Then *) Have: i <= 9. }
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'false_but_preserved' (file tests/wp_acsl/generalized_checks.i, line 70):
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Check 'implied_by_false_invariant' (file tests/wp_acsl/generalized_checks.i, line 74):
+Assume { Type: is_sint32(i). (* Else *) Have: 10 <= i. }
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/generalized_checks.i, line 71):
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle
index ee38ba79727..5ab67d884fd 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle
@@ -1,8 +1,14 @@
# frama-c -wp -wp-timeout 1 [...]
[kernel] Parsing tests/wp_acsl/generalized_checks.i (no preprocessing)
[wp] Running WP plugin...
+[wp] tests/wp_acsl/generalized_checks.i:68: Warning:
+ Unsupported generalized invariant, use loop invariant instead.
+ Ignored invariant
+ check invariant \true;
[wp] Warning: Missing RTE guards
-[wp] 17 goals scheduled
+[wp] tests/wp_acsl/generalized_checks.i:75: Warning:
+ Missing assigns clause (assigns 'everything' instead)
+[wp] 21 goals scheduled
[wp] [Alt-Ergo] Goal typed_check_lemma_C_ko : Unsuccess
[wp] [Alt-Ergo] Goal typed_lemma_L_ko : Unsuccess
[wp] [Alt-Ergo] Goal typed_job_ensures_B : Valid
@@ -20,9 +26,13 @@
[wp] [Qed] Goal typed_caller_call_job_requires_A : Valid
[wp] [Qed] Goal typed_caller_call_job_check_requires_CA1 : Valid
[wp] [Alt-Ergo] Goal typed_caller_call_job_check_requires_CA2_ko : Unsuccess
-[wp] Proved goals: 11 / 17
- Qed: 9
- Alt-Ergo: 2 (unsuccess: 6)
+[wp] [Alt-Ergo] Goal typed_loop_check_loop_invariant_false_but_preserved_preserved : Unsuccess
+[wp] [Alt-Ergo] Goal typed_loop_check_loop_invariant_false_but_preserved_established : Unsuccess
+[wp] [Alt-Ergo] Goal typed_loop_check_implied_by_false_invariant : Unsuccess
+[wp] [Qed] Goal typed_loop_loop_assigns : Valid
+[wp] Proved goals: 12 / 21
+ Qed: 10
+ Alt-Ergo: 2 (unsuccess: 9)
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Axiomatic Th - - 2 0.0%
@@ -30,4 +40,5 @@
Functions WP Alt-Ergo Total Success
job 3 2 6 83.3%
caller 6 - 9 66.7%
+ loop 1 - 4 25.0%
------------------------------------------------------------
diff --git a/tests/spec/generalized_check.i b/tests/spec/generalized_check.i
index baf66eaa6b7..06f74139cfb 100644
--- a/tests/spec/generalized_check.i
+++ b/tests/spec/generalized_check.i
@@ -1,8 +1,8 @@
/* run.config
-OPT: -wp -wp-prover qed -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive
OPT: -eva -eva-use-spec f
OPT: -print
*/
+
/*@ check lemma easy_proof: \false; */ // should not be put in any environment
/*@ check requires f_valid_x: \valid(x);
diff --git a/tests/spec/oracle/generalized_check.0.res.oracle b/tests/spec/oracle/generalized_check.0.res.oracle
index 391634ac903..f93e7228b40 100644
--- a/tests/spec/oracle/generalized_check.0.res.oracle
+++ b/tests/spec/oracle/generalized_check.0.res.oracle
@@ -1,24 +1,47 @@
-# frama-c -wp [...]
[kernel] Parsing tests/spec/generalized_check.i (no preprocessing)
-[wp] Running WP plugin...
-[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:37: Warning:
- Missing assigns clause (assigns 'everything' instead)
-[wp] 11 goals scheduled
-[wp] [Qed] Goal typed_f_assigns : Valid
-[wp] [Failed] Goal typed_f_check_f_valid_ko
-[wp] [Qed] Goal typed_f_check_ensures_f_init_x : Valid
-[wp] [Failed] Goal typed_check_lemma_easy_proof
-[wp] [Qed] Goal typed_loop_loop_assigns : Valid
-[wp] [Failed] Goal typed_loop_check_implied_by_false_invariant
-[wp] [Failed] Goal typed_loop_check_loop_invariant_false_but_preserved_established
-[wp] [Failed] Goal typed_loop_check_loop_invariant_false_but_preserved_preserved
-[wp] [Failed] Goal typed_main_call_f_check_requires_f_valid_x
-[wp] [Failed] Goal typed_main_check_main_p_content_ko
-[wp] [Failed] Goal typed_main_check_main_valid_ko
-[wp] Proved goals: 3 / 11
- Qed: 3
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+
+[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:24: Warning:
+ function f: precondition 'f_valid_x' got status unknown.
+[eva] tests/spec/generalized_check.i:9: Warning:
+ no \from part for clause 'assigns *x;'
+[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:32: Warning:
+ loop invariant 'false_but_preserved' got status invalid.
+[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 ======
+[eva:final-states] Values at end of function loop:
+ j ∈ {10}
+[eva:final-states] Values at end of function main:
+ a ∈ [--..--]
+ p ∈ {{ NULL ; &a }}
+ __retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 3 functions analyzed (out of 3): 100% coverage.
+ In these functions, 25 statements reached (out of 28): 89% coverage.
+ ----------------------------------------------------------------------------
+ Some errors and warnings have been raised during the analysis:
+ by the Eva analyzer: 0 errors 1 warning
+ by the Frama-C kernel: 0 errors 0 warnings
+ ----------------------------------------------------------------------------
+ 1 alarm generated by the analysis:
+ 1 access to uninitialized left-values
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 0 valid 2 unknown 2 invalid 4 total
+ Preconditions 0 valid 1 unknown 0 invalid 1 total
+ 0% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------
diff --git a/tests/spec/oracle/generalized_check.1.res.oracle b/tests/spec/oracle/generalized_check.1.res.oracle
index f93e7228b40..dd870d5dc00 100644
--- a/tests/spec/oracle/generalized_check.1.res.oracle
+++ b/tests/spec/oracle/generalized_check.1.res.oracle
@@ -1,47 +1,51 @@
[kernel] Parsing tests/spec/generalized_check.i (no preprocessing)
-[eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
-
-[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:24: Warning:
- function f: precondition 'f_valid_x' got status unknown.
-[eva] tests/spec/generalized_check.i:9: Warning:
- no \from part for clause 'assigns *x;'
-[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:32: Warning:
- loop invariant 'false_but_preserved' got status invalid.
-[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 ======
-[eva:final-states] Values at end of function loop:
- j ∈ {10}
-[eva:final-states] Values at end of function main:
- a ∈ [--..--]
- p ∈ {{ NULL ; &a }}
- __retres ∈ {0}
-[eva:summary] ====== ANALYSIS SUMMARY ======
- ----------------------------------------------------------------------------
- 3 functions analyzed (out of 3): 100% coverage.
- In these functions, 25 statements reached (out of 28): 89% coverage.
- ----------------------------------------------------------------------------
- Some errors and warnings have been raised during the analysis:
- by the Eva analyzer: 0 errors 1 warning
- by the Frama-C kernel: 0 errors 0 warnings
- ----------------------------------------------------------------------------
- 1 alarm generated by the analysis:
- 1 access to uninitialized left-values
- ----------------------------------------------------------------------------
- Evaluation of the logical properties reached by the analysis:
- Assertions 0 valid 2 unknown 2 invalid 4 total
- Preconditions 0 valid 1 unknown 0 invalid 1 total
- 0% of the logical properties reached have been proven.
- ----------------------------------------------------------------------------
+/* 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.2.res.oracle b/tests/spec/oracle/generalized_check.2.res.oracle
deleted file mode 100644
index dd870d5dc00..00000000000
--- a/tests/spec/oracle/generalized_check.2.res.oracle
+++ /dev/null
@@ -1,51 +0,0 @@
-[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