Skip to content
Snippets Groups Projects
Commit f3f0e2ea authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] removed stmt-contract

parent 02158fa3
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/wp/tests/wp_plugin/oracle/stmt.res.oracle deleted 100644 → 0
+ 0
− 141
View file @ 02158fa3
# 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
--------------------------------------------------------------------------------
src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log deleted 100644 → 0
+ 0
− 22
View file @ 02158fa3
# 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
src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle deleted 100644 → 0
+ 0
− 114
View file @ 02158fa3
# 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
--------------------------------------------------------------------------------
src/plugins/wp/tests/wp_plugin/stmt.c deleted 100644 → 0
+ 0
− 55
View file @ 02158fa3
/* 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;
}
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment