From 8ee9cc4d4b7ce5ccd4243fa732ee52bed653638c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 18 Feb 2021 09:58:57 +0100
Subject: [PATCH] [wp] removed stmt-contract
---
.../wp/tests/wp_bts/nupw-bcl-bts1120.i | 45 +------------------
.../wp_bts/oracle/nupw-bcl-bts1120.res.oracle | 45 +------------------
.../oracle_qualif/nupw-bcl-bts1120.res.oracle | 15 ++-----
3 files changed, 6 insertions(+), 99 deletions(-)
diff --git a/src/plugins/wp/tests/wp_bts/nupw-bcl-bts1120.i b/src/plugins/wp/tests/wp_bts/nupw-bcl-bts1120.i
index fff780f8692..a10cc5ea417 100644
--- a/src/plugins/wp/tests/wp_bts/nupw-bcl-bts1120.i
+++ b/src/plugins/wp/tests/wp_bts/nupw-bcl-bts1120.i
@@ -1,21 +1,12 @@
/* run.config_qualif
- OPT: -wp -wp-par 1 -wp-fct "g,unreachable_smt_with_contract"
+ OPT: -wp-fct "g"
*/
/*@ axiomatic ax {
@ predicate ExitF(integer x);
@ predicate ExitP(integer x);
- @ predicate Exit1(integer x);
-
@ predicate PostF(integer x);
- @ predicate PostP(integer x);
- @ predicate Post1(integer x);
-
- @ predicate P(integer x);
- @ predicate PreF(integer x);
- @ predicate Pre(integer x);
- @ predicate Pre1(integer x);
} */
//@ assigns \nothing; ensures PostF(x); exits ExitF(x) ;
@@ -30,37 +21,3 @@ void g (int max) {
tmp ++;
}
}
-
-//@ requires ok: x > 0 ; assigns \nothing;
-extern int f_with_precond (int x);
-
-// corrected.
-//@ requires PostP(max); ensures ok: PostP(max);
-void unreachable_smt_with_contract (int max) {
- int tmp = f_with_precond(1);
- goto L;
- //@ requires ok: Pre1(max); assigns ok: tmp; ensures ok: Post1(max); exits ok: Exit1(max);
- tmp = f_with_precond(-2);
- //@ assert ok: P(tmp);
- tmp=3;
- L:;
-}
-
-//@ assigns \nothing; exits never: \false;
-int f_no_exit(int) ;
-
-// corrected in stronger the PO (e1 is forgotten and is not provable *)
-//@ exits e:ExitP(0);
-int cfg_domination_problem (int max) {
- int tmp=1;
- if (max) {
- tmp=f_no_exit(tmp);
- goto L;
- }
- //@ assigns tmp; exits e1:ExitP(max);
- {
- tmp=f(max);
- L: tmp=3;
- }
- return tmp;
-}
diff --git a/src/plugins/wp/tests/wp_bts/oracle/nupw-bcl-bts1120.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/nupw-bcl-bts1120.res.oracle
index 60c6a834f15..eff9406479d 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/nupw-bcl-bts1120.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/nupw-bcl-bts1120.res.oracle
@@ -1,34 +1,7 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/nupw-bcl-bts1120.i (no preprocessing)
[wp] Running WP plugin...
-[wp] tests/wp_bts/nupw-bcl-bts1120.i:54: Warning:
- [cfg] Forget exits clause of node <blkIn-stmt:26>
-[wp] tests/wp_bts/nupw-bcl-bts1120.i:54: Warning:
- [cfg] Forget exits clause of node <blkIn-stmt:26>
-[wp] [CFG] Goal unreachable_smt_with_contract_assigns : Valid (Unreachable)
-[wp] [CFG] Goal unreachable_smt_with_contract_exits_ok : Valid (Unreachable)
-[wp] [CFG] Goal unreachable_smt_with_contract_ensures_ok : Valid (Unreachable)
-[wp] [CFG] Goal unreachable_smt_with_contract_requires_ok : Valid (Unreachable)
-[wp] [CFG] Goal unreachable_smt_with_contract_assert_ok : Valid (Unreachable)
-[wp] [CFG] Goal unreachable_smt_with_contract_call_f_with_precond_requires_ok : Valid (Unreachable)
[wp] Warning: Missing RTE guards
-------------------------------------------------------------
- Function cfg_domination_problem
-------------------------------------------------------------
-
-Goal Exit-condition 'e' in 'cfg_domination_problem':
-Assume { (* Exit 'f' *) Have: P_ExitF(0). }
-Prove: P_ExitP(0).
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function cfg_domination_problem with behavior default_for_stmt_26
-------------------------------------------------------------
-
-Goal Assigns (file tests/wp_bts/nupw-bcl-bts1120.i, line 60) at block:
-Prove: true.
-
-------------------------------------------------------------
------------------------------------------------------------
Function g
------------------------------------------------------------
@@ -54,27 +27,13 @@ Prove: true.
------------------------------------------------------------
Goal Assigns nothing in 'g' (2/3):
-Call Result at line 27
+Call Result at line 18
Prove: true.
------------------------------------------------------------
Goal Assigns nothing in 'g' (3/3):
-Effect at line 29
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function unreachable_smt_with_contract
-------------------------------------------------------------
-
-Goal Post-condition 'ok' in 'unreachable_smt_with_contract':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Instance of 'Pre-condition 'ok' in 'f_with_precond'' in 'unreachable_smt_with_contract' at initialization of 'tmp' (file tests/wp_bts/nupw-bcl-bts1120.i, line 40)
-:
+Effect at line 20
Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle
index b7eb301f118..5b44fe269a0 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle
@@ -1,26 +1,17 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/nupw-bcl-bts1120.i (no preprocessing)
[wp] Running WP plugin...
-[wp] [CFG] Goal unreachable_smt_with_contract_assigns : Valid (Unreachable)
-[wp] [CFG] Goal unreachable_smt_with_contract_exits_ok : Valid (Unreachable)
-[wp] [CFG] Goal unreachable_smt_with_contract_ensures_ok : Valid (Unreachable)
-[wp] [CFG] Goal unreachable_smt_with_contract_requires_ok : Valid (Unreachable)
-[wp] [CFG] Goal unreachable_smt_with_contract_assert_ok : Valid (Unreachable)
-[wp] [CFG] Goal unreachable_smt_with_contract_call_f_with_precond_requires_ok : Valid (Unreachable)
[wp] Warning: Missing RTE guards
-[wp] 8 goals scheduled
+[wp] 6 goals scheduled
[wp] [Qed] Goal typed_g_exits_ok : Valid
[wp] [Qed] Goal typed_g_loop_assigns : Valid
[wp] [Qed] Goal typed_g_assigns_exit : Valid
[wp] [Qed] Goal typed_g_assigns_normal_part1 : Valid
[wp] [Qed] Goal typed_g_assigns_normal_part2 : Valid
[wp] [Qed] Goal typed_g_assigns_normal_part3 : Valid
-[wp] [Qed] Goal typed_unreachable_smt_with_contract_ensures_ok_2 : Valid
-[wp] [Qed] Goal typed_unreachable_smt_with_contract_call_f_with_precond_2_requires_ok : Valid
-[wp] Proved goals: 14 / 14
- Qed: 8
+[wp] Proved goals: 6 / 6
+ Qed: 6
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
g 6 - 6 100%
- unreachable_smt_with_contract 2 - 2 100%
------------------------------------------------------------
--
GitLab