From fd1eb2c75319b958762ba8c046e3a8ece08fa71f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 9 Sep 2020 17:27:41 +0200
Subject: [PATCH] [wp] unit test for checks
---
.../wp/tests/wp_acsl/generalized_checks.i | 66 +++++++++
.../oracle/generalized_checks.res.oracle | 139 ++++++++++++++++++
.../generalized_checks.res.oracle | 34 +++++
3 files changed, 239 insertions(+)
create mode 100644 src/plugins/wp/tests/wp_acsl/generalized_checks.i
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle
diff --git a/src/plugins/wp/tests/wp_acsl/generalized_checks.i b/src/plugins/wp/tests/wp_acsl/generalized_checks.i
new file mode 100644
index 00000000000..3b34ced34e2
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/generalized_checks.i
@@ -0,0 +1,66 @@
+/* run.config_qualif
+ OPT: -wp-timeout 1
+ */
+
+/*@
+ axiomatic Th {
+
+ predicate P(integer p);
+ predicate Q(integer q);
+ predicate R(integer r);
+
+ axiom A: \forall integer x; P(x) ==> Q(x);
+ check lemma C: ko: \forall integer x; Q(x) ==> R(x);
+ lemma L: ko: \forall integer x; P(x) ==> R(x); // C is not used
+
+ }
+ */
+
+/*@
+ axiomatic Cfg {
+ logic integer F(integer x);
+ predicate A(integer x);
+ predicate B(integer x);
+ predicate CA1(integer x);
+ predicate CA2(integer x);
+ predicate CB1(integer x);
+ predicate CB2(integer x);
+
+ axiom AFB: \forall integer x; A(x) ==> B(F(x));
+ axiom ACB1: \forall integer x; A(x) ==> CB1(F(x));
+ axiom CA1B2: \forall integer x; CA1(x) ==> CB2(F(x));
+
+ }
+ */
+
+/*@
+ ensures \result == F(x);
+ assigns \nothing;
+ */
+int f(int x);
+
+/*@
+ requires A: A(x);
+ check requires CA1: CA1(x);
+ check requires CA2: ko: CA2(x);
+ ensures B: B(\result);
+ check ensures CB1: CB1(\result);
+ check ensures CB2: ko: CB2(\result); // CA1 is not used
+ assigns \nothing;
+*/
+int job(int x) {
+ return f(x);
+}
+
+/*@
+ requires A(x);
+ requires CA1(x);
+ ensures R: B(\result);
+ ensures R1: ko: CB1(\result); // CB1 is not used from job
+ ensures R2: ko: CA2(x); // CA2 is not used from job
+ assigns \nothing;
+*/
+int caller(int x)
+{
+ return job(x); // CA2 is not proved
+}
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
new file mode 100644
index 00000000000..6b7463a9cd6
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle
@@ -0,0 +1,139 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/generalized_checks.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Axiomatic 'Th'
+------------------------------------------------------------
+
+Lemma C:
+Assume: 'A'
+Prove: (P_Q x_0) -> (P_R x_0)
+
+------------------------------------------------------------
+
+Lemma L:
+Assume: 'A'
+Prove: (P_P x_0) -> (P_R x_0)
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function caller
+------------------------------------------------------------
+
+Goal Post-condition 'R' in 'caller':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition 'R1,ko' in 'caller':
+Assume {
+ Type: is_sint32(caller_0) /\ is_sint32(x).
+ (* Pre-condition *)
+ Have: P_A(x) /\ P_CA1(x).
+ (* Call 'job' *)
+ Have: P_B(caller_0).
+}
+Prove: P_CB1(caller_0).
+
+------------------------------------------------------------
+
+Goal Post-condition 'R2,ko' in 'caller':
+Assume {
+ Type: is_sint32(caller_0) /\ is_sint32(x).
+ (* Pre-condition *)
+ Have: P_A(x) /\ P_CA1(x).
+ (* Call 'job' *)
+ Have: P_B(caller_0).
+}
+Prove: P_CA2(x).
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'caller':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'caller' (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'caller' (2/2):
+Call Result at line 65
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'A' in 'job'' in 'caller' at call 'job' (file tests/wp_acsl/generalized_checks.i, line 65)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'CA1' in 'job'' in 'caller' at call 'job' (file tests/wp_acsl/generalized_checks.i, line 65)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'CA2,ko' in 'job'' in 'caller' at call 'job' (file tests/wp_acsl/generalized_checks.i, line 65)
+:
+Assume { Type: is_sint32(x). (* Pre-condition *) Have: P_A(x) /\ P_CA1(x). }
+Prove: P_CA2(x).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function job
+------------------------------------------------------------
+
+Goal Post-condition 'B' in 'job':
+Let x_1 = L_F(x).
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1).
+ (* Pre-condition *)
+ Have: P_A(x).
+}
+Prove: P_B(x_1).
+
+------------------------------------------------------------
+
+Goal Post-condition 'CB1' in 'job':
+Let x_1 = L_F(x).
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1).
+ (* Pre-condition *)
+ Have: P_A(x).
+}
+Prove: P_CB1(x_1).
+
+------------------------------------------------------------
+
+Goal Post-condition 'CB2,ko' in 'job':
+Let x_1 = L_F(x).
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1).
+ (* Pre-condition *)
+ Have: P_A(x).
+}
+Prove: P_CB2(x_1).
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'job':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'job' (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'job' (2/2):
+Call Result at line 52
+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
new file mode 100644
index 00000000000..1673f54ff07
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle
@@ -0,0 +1,34 @@
+# frama-c -wp -wp-timeout 1 [...]
+[kernel] Parsing tests/wp_acsl/generalized_checks.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 17 goals scheduled
+[wp] [Alt-Ergo] Goal typed_lemma_C_ko : Unsuccess
+[wp] [Alt-Ergo] Goal typed_lemma_L_ko : Unsuccess
+[wp] [Qed] Goal typed_caller_ensures_R : Valid
+[wp] [Alt-Ergo] Goal typed_caller_ensures_R1_ko : Unsuccess
+[wp] [Alt-Ergo] Goal typed_caller_ensures_R2_ko : Unsuccess
+[wp] [Qed] Goal typed_caller_assigns_exit : Valid
+[wp] [Qed] Goal typed_caller_assigns_normal_part1 : Valid
+[wp] [Qed] Goal typed_caller_assigns_normal_part2 : Valid
+[wp] [Qed] Goal typed_caller_call_job_requires_A : Valid
+[wp] [Qed] Goal typed_caller_call_job_requires_CA1 : Valid
+[wp] [Alt-Ergo] Goal typed_caller_call_job_requires_CA2_ko : Unsuccess
+[wp] [Alt-Ergo] Goal typed_job_ensures_B : Valid
+[wp] [Alt-Ergo] Goal typed_job_ensures_CB1 : Valid
+[wp] [Alt-Ergo] Goal typed_job_ensures_CB2_ko : Unsuccess
+[wp] [Qed] Goal typed_job_assigns_exit : Valid
+[wp] [Qed] Goal typed_job_assigns_normal_part1 : Valid
+[wp] [Qed] Goal typed_job_assigns_normal_part2 : Valid
+[wp] Proved goals: 11 / 17
+ Qed: 9
+ Alt-Ergo: 2 (unsuccess: 6)
+------------------------------------------------------------
+ Axiomatics WP Alt-Ergo Total Success
+ Axiomatic Th - - 2 0.0%
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ job 3 2 6 83.3%
+ caller 6 - 9 66.7%
+------------------------------------------------------------
--
GitLab