From f3f0e2eaa3b5a37c186e3eeb3b932f82b42d7939 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 19 Feb 2021 10:49:01 +0100
Subject: [PATCH] [wp] removed stmt-contract
---
.../wp/tests/wp_plugin/oracle/stmt.res.oracle | 141 ------------------
.../wp/tests/wp_plugin/oracle_qualif/stmt.log | 22 ---
.../wp_plugin/oracle_qualif/stmt.res.oracle | 114 --------------
src/plugins/wp/tests/wp_plugin/stmt.c | 55 -------
4 files changed, 332 deletions(-)
delete mode 100644 src/plugins/wp/tests/wp_plugin/oracle/stmt.res.oracle
delete mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log
delete mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle
delete mode 100644 src/plugins/wp/tests/wp_plugin/stmt.c
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/stmt.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/stmt.res.oracle
deleted file mode 100644
index 124de2a508d..00000000000
--- a/src/plugins/wp/tests/wp_plugin/oracle/stmt.res.oracle
+++ /dev/null
@@ -1,141 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/stmt.c (with preprocessing)
-[wp] Running WP plugin...
-[wp] [CFG] Goal f_exits : Valid (Unreachable)
-[wp] [CFG] Goal g_exits : Valid (Unreachable)
-[wp] [CFG] Goal g_assigns : Valid (Unreachable)
-[wp] [CFG] Goal g_ensures : Valid (Unreachable)
-[wp] [CFG] Goal g_exits : Valid (Unreachable)
-[wp] [CFG] Goal h_exits : Valid (Unreachable)
-[wp] [CFG] Goal h_assigns : Valid (Unreachable)
-[wp] [CFG] Goal h_ensures : Valid (Unreachable)
-[wp] [CFG] Goal h_exits : Valid (Unreachable)
-[wp] Warning: Missing RTE guards
-------------------------------------------------------------
- Function f
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_plugin/stmt.c, line 10) in 'f':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_plugin/stmt.c, line 11) in 'f':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assertion (file tests/wp_plugin/stmt.c, line 16):
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function f with behavior default_for_stmt_2
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_plugin/stmt.c, line 17) at block:
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file tests/wp_plugin/stmt.c, line 21) at block:
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function g
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_plugin/stmt.c, line 27) in 'g':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assertion (file tests/wp_plugin/stmt.c, line 32):
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function h
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_plugin/stmt.c, line 40) in 'h':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assertion (generated):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assertion (generated):
-Prove: true.
-
-------------------------------------------------------------
-[report] Computing properties status...
-
---------------------------------------------------------------------------------
---- Properties of Function 'f'
---------------------------------------------------------------------------------
-
-[ Valid ] Exit-condition (file tests/wp_plugin/stmt.c, line 15) at block
- by Unreachable Annotations.
-[ Partial ] Return-condition (file tests/wp_plugin/stmt.c, line 16) at block
- By Frama-C kernel, with pending:
- - Assertion (file tests/wp_plugin/stmt.c, line 16)
-[ - ] Default behavior at block
- tried with Frama-C kernel.
-
---------------------------------------------------------------------------------
---- Properties of Function 'g'
---------------------------------------------------------------------------------
-
-[ Valid ] Exit-condition (file tests/wp_plugin/stmt.c, line 31) at block
- by Unreachable Annotations.
-[ Valid ] Return-condition (file tests/wp_plugin/stmt.c, line 32) at block
- by Unreachable Annotations.
-[ Valid ] Post-condition (file tests/wp_plugin/stmt.c, line 33) at block
- by Unreachable Annotations.
-[ Valid ] Assigns (file tests/wp_plugin/stmt.c, line 36) at block
- by Unreachable Annotations.
-[ Valid ] Default behavior at block
- by Frama-C kernel.
-
---------------------------------------------------------------------------------
---- Properties of Function 'h'
---------------------------------------------------------------------------------
-
-[ Valid ] Exit-condition (file tests/wp_plugin/stmt.c, line 43) at block
- by Unreachable Annotations.
-[ Valid ] Post-condition (file tests/wp_plugin/stmt.c, line 44) at block
- by Unreachable Annotations.
-[ Partial ] Return-condition for 'POS' (file tests/wp_plugin/stmt.c, line 48) at block
- By Frama-C kernel, with pending:
- - Assertion (generated)
- - Assertion (generated)
-[ Partial ] Return-condition for 'NEG' (file tests/wp_plugin/stmt.c, line 51) at block
- By Frama-C kernel, with pending:
- - Assertion (generated)
- - Assertion (generated)
-[ Valid ] Assigns (file tests/wp_plugin/stmt.c, line 53) at block
- by Unreachable Annotations.
-[ Partial ] Behavior 'NEG' at block
- By Frama-C kernel, with pending:
- - Assertion (generated)
- - Assertion (generated)
-[ Partial ] Behavior 'POS' at block
- By Frama-C kernel, with pending:
- - Assertion (generated)
- - Assertion (generated)
-[ Valid ] Default behavior at block
- by Frama-C kernel.
-
---------------------------------------------------------------------------------
---- Status Report Summary
---------------------------------------------------------------------------------
- 10 Completely validated
- 5 Locally validated
- 1 To be validated
- 16 Total
---------------------------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log b/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log
deleted file mode 100644
index fc376ede27e..00000000000
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log
+++ /dev/null
@@ -1,22 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/stmt.c (with preprocessing)
-[wp] Running WP plugin...
-[wp] [CFG] Goal f_exits : Valid (Unreachable)
-[wp] [CFG] Goal g_exits : Valid (Unreachable)
-[wp] [CFG] Goal g_assigns : Valid (Unreachable)
-[wp] [CFG] Goal g_ensures : Valid (Unreachable)
-[wp] [CFG] Goal g_exits : Valid (Unreachable)
-[wp] [CFG] Goal h_exits : Valid (Unreachable)
-[wp] [CFG] Goal h_assigns : Valid (Unreachable)
-[wp] [CFG] Goal h_ensures : Valid (Unreachable)
-[wp] [CFG] Goal h_exits : Valid (Unreachable)
-[wp] CFG h -> h
-[wp] CFG h -> h_NEG_stmt_15
-[wp] CFG h -> h_POS_stmt_15
-[wp] CFG h -> h_default_for_stmt_15
-[wp] CFG g -> g
-[wp] CFG g -> g_default_for_stmt_11
-[wp] CFG f -> f
-[wp] CFG f -> f_default_for_stmt_2
-[wp] Warning: No goal generated
-[wp] Proved goals: 9 / 9
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle
deleted file mode 100644
index 0d904ff5c08..00000000000
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle
+++ /dev/null
@@ -1,114 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/stmt.c (with preprocessing)
-[wp] Running WP plugin...
-[wp] [CFG] Goal f_exits : Valid (Unreachable)
-[wp] [CFG] Goal g_exits : Valid (Unreachable)
-[wp] [CFG] Goal g_assigns : Valid (Unreachable)
-[wp] [CFG] Goal g_ensures : Valid (Unreachable)
-[wp] [CFG] Goal g_exits : Valid (Unreachable)
-[wp] [CFG] Goal h_exits : Valid (Unreachable)
-[wp] [CFG] Goal h_assigns : Valid (Unreachable)
-[wp] [CFG] Goal h_ensures : Valid (Unreachable)
-[wp] [CFG] Goal h_exits : Valid (Unreachable)
-[wp] Warning: Missing RTE guards
-[wp] 10 goals scheduled
-[wp] [Qed] Goal typed_f_ensures : Valid
-[wp] [Qed] Goal typed_f_assigns : Valid
-[wp] [Qed] Goal typed_f_ensures_2 : Valid
-[wp] [Qed] Goal typed_f_ensures_3 : Valid
-[wp] [Qed] Goal typed_f_assert : Valid
-[wp] [Qed] Goal typed_g_ensures_2 : Valid
-[wp] [Qed] Goal typed_g_assert : Valid
-[wp] [Qed] Goal typed_h_ensures_2 : Valid
-[wp] [Qed] Goal typed_h_assert : Valid
-[wp] [Qed] Goal typed_h_assert_2 : Valid
-[wp] Proved goals: 19 / 19
- Qed: 10
-------------------------------------------------------------
- Functions WP Alt-Ergo Total Success
- f 5 - 5 100%
- g 2 - 2 100%
- h 3 - 3 100%
-------------------------------------------------------------
-[report] Computing properties status...
-
---------------------------------------------------------------------------------
---- Properties of Function 'f'
---------------------------------------------------------------------------------
-
-[ Valid ] Post-condition (file tests/wp_plugin/stmt.c, line 10)
- by Wp.typed.
-[ Valid ] Post-condition (file tests/wp_plugin/stmt.c, line 11)
- by Wp.typed.
-[ Valid ] Exit-condition (file tests/wp_plugin/stmt.c, line 15) at block
- by Unreachable Annotations.
-[ Valid ] Return-condition (file tests/wp_plugin/stmt.c, line 16) at block
- by Frama-C kernel.
-[ Valid ] Post-condition (file tests/wp_plugin/stmt.c, line 17) at block
- by Wp.typed.
-[ Valid ] Assigns (file tests/wp_plugin/stmt.c, line 21) at block
- by Wp.typed.
-[ Valid ] Assertion (file tests/wp_plugin/stmt.c, line 16)
- by Wp.typed.
-[ Valid ] Default behavior at block
- by Frama-C kernel.
-[ Valid ] Default behavior
- by Frama-C kernel.
-
---------------------------------------------------------------------------------
---- Properties of Function 'g'
---------------------------------------------------------------------------------
-
-[ Valid ] Post-condition (file tests/wp_plugin/stmt.c, line 27)
- by Wp.typed.
-[ Valid ] Exit-condition (file tests/wp_plugin/stmt.c, line 31) at block
- by Unreachable Annotations.
-[ Valid ] Return-condition (file tests/wp_plugin/stmt.c, line 32) at block
- by Frama-C kernel.
- by Unreachable Annotations.
-[ Valid ] Post-condition (file tests/wp_plugin/stmt.c, line 33) at block
- by Unreachable Annotations.
-[ Valid ] Assigns (file tests/wp_plugin/stmt.c, line 36) at block
- by Unreachable Annotations.
-[ Valid ] Assertion (file tests/wp_plugin/stmt.c, line 32)
- by Wp.typed.
-[ Valid ] Default behavior at block
- by Frama-C kernel.
-[ Valid ] Default behavior
- by Frama-C kernel.
-
---------------------------------------------------------------------------------
---- Properties of Function 'h'
---------------------------------------------------------------------------------
-
-[ Valid ] Post-condition (file tests/wp_plugin/stmt.c, line 40)
- by Wp.typed.
-[ Valid ] Exit-condition (file tests/wp_plugin/stmt.c, line 43) at block
- by Unreachable Annotations.
-[ Valid ] Post-condition (file tests/wp_plugin/stmt.c, line 44) at block
- by Unreachable Annotations.
-[ Valid ] Return-condition for 'POS' (file tests/wp_plugin/stmt.c, line 48) at block
- by Frama-C kernel.
-[ Valid ] Return-condition for 'NEG' (file tests/wp_plugin/stmt.c, line 51) at block
- by Frama-C kernel.
-[ Valid ] Assigns (file tests/wp_plugin/stmt.c, line 53) at block
- by Unreachable Annotations.
-[ Valid ] Assertion (generated)
- by Wp.typed.
-[ Valid ] Assertion (generated)
- by Wp.typed.
-[ Valid ] Behavior 'NEG' at block
- by Frama-C kernel.
-[ Valid ] Behavior 'POS' at block
- by Frama-C kernel.
-[ Valid ] Default behavior at block
- by Frama-C kernel.
-[ Valid ] Default behavior
- by Frama-C kernel.
-
---------------------------------------------------------------------------------
---- Status Report Summary
---------------------------------------------------------------------------------
- 29 Completely validated
- 29 Total
---------------------------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/stmt.c b/src/plugins/wp/tests/wp_plugin/stmt.c
deleted file mode 100644
index bb82e910c1c..00000000000
--- a/src/plugins/wp/tests/wp_plugin/stmt.c
+++ /dev/null
@@ -1,55 +0,0 @@
-/* run.config
- OPT: -load-module report -then -report
-*/
-
-/* run.config_qualif
- OPT: -load-module report -then -report
- EXECNOW: LOG stmt.log LOG f.dot LOG f_default_for_stmt_2.dot LOG g.dot LOG g_default_for_stmt_11.dot @frama-c@ -no-autoload-plugins -load-module wp -wp-precond-weakening -wp -wp-warn-key pedantic-assigns=inactive -wp-dump -wp-out tests/wp_plugin/result_qualif -wp-msg-key shell @PTEST_FILE@ 1> tests/wp_plugin/result_qualif/stmt.log
-*/
-
-/*@ ensures a > 0 ==> \result == a + b;
- @ ensures a <= 0 ==> \result == -1;
-*/
-int f(int a, int b) {
-
- /*@ exits \false;
- @ returns \result == a + b;
- @ ensures a <= 0;
- @ assigns \nothing;
- */
- if (a > 0)
- return a + b;
-
- return -1;
-}
-
-
-/*@ ensures \result == a + b;
-*/
-int g(int a, int b) {
-
- /*@ exits \false;
- @ returns \result == a + b;
- @ ensures \false;
- @ assigns \nothing;
- */
- return a + b;
-
-}
-
-/*@ ensures \result == (e ? a : b) ; */
-int h(int e,int a,int b) {
-
- /*@ exits \false;
- @ ensures \false;
- @ assigns \nothing;
- @ behavior POS:
- @ assumes e ;
- @ returns \result == a;
- @ behavior NEG:
- @ assumes !e ;
- @ returns \result == b;
- */
- if (e) return a; else return b;
-
-}
--
GitLab