diff --git a/src/plugins/wp/tests/wp_bts/issue-684-exit.c b/src/plugins/wp/tests/wp_bts/issue-684-exit.c new file mode 100644 index 0000000000000000000000000000000000000000..9776a3999024830d9fccfad157987f24d84bc50e --- /dev/null +++ b/src/plugins/wp/tests/wp_bts/issue-684-exit.c @@ -0,0 +1,8 @@ +#include "stdlib.h" +/*@ assigns \nothing; + @ exits \exit_status == state; + @ ensures \false; +*/ +void inconditional_exit(int state) { + exit (state); +} diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..2b2e6c21c2df88606ff2a10ab33ab0e66f8f3272 --- /dev/null +++ b/src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle @@ -0,0 +1,28 @@ +# frama-c -wp [...] +[kernel] Parsing tests/wp_bts/issue-684-exit.c (with preprocessing) +[wp] Running WP plugin... +[wp] Loading driver 'share/wp.driver' +[wp] Warning: Missing RTE guards +------------------------------------------------------------ + Function inconditional_exit +------------------------------------------------------------ + +Goal Post-condition (file tests/wp_bts/issue-684-exit.c, line 4) in 'inconditional_exit': +Prove: true. + +------------------------------------------------------------ + +Goal Exit-condition (file tests/wp_bts/issue-684-exit.c, line 3) in 'inconditional_exit': +Prove: true. + +------------------------------------------------------------ + +Goal Assigns nothing in 'inconditional_exit': +Prove: true. + +------------------------------------------------------------ + +Goal Assigns nothing in 'inconditional_exit': +Prove: true. + +------------------------------------------------------------ diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.0.report.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.0.report.json new file mode 100644 index 0000000000000000000000000000000000000000..43d68882c15550cf2332345a3d4ce10c709184ac --- /dev/null +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.0.report.json @@ -0,0 +1,22 @@ +{ "wp:global": { "qed": { "total": 4, "valid": 4 }, + "wp:main": { "total": 4, "valid": 4 } }, + "wp:functions": { "inconditional_exit": { "inconditional_exit_assigns": + { "qed": { "total": 2, + "valid": 2 }, + "wp:main": { "total": 2, + "valid": 2 } }, + "inconditional_exit_ensures": + { "qed": { "total": 1, + "valid": 1 }, + "wp:main": { "total": 1, + "valid": 1 } }, + "inconditional_exit_exits": + { "qed": { "total": 1, + "valid": 1 }, + "wp:main": { "total": 1, + "valid": 1 } }, + "wp:section": { "qed": { "total": 4, + "valid": 4 }, + "wp:main": + { "total": 4, + "valid": 4 } } } } } diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..798f9dce70e5ef0f33472fa2955b33867aa093f1 --- /dev/null +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.res.oracle @@ -0,0 +1,18 @@ +# frama-c -wp [...] +[kernel] Parsing tests/wp_bts/issue-684-exit.c (with preprocessing) +[wp] Running WP plugin... +[wp] Loading driver 'share/wp.driver' +[wp] Warning: Missing RTE guards +[wp] 4 goals scheduled +[wp] [Qed] Goal typed_inconditional_exit_ensures : Valid +[wp] [Qed] Goal typed_inconditional_exit_exits : Valid +[wp] [Qed] Goal typed_inconditional_exit_assigns_exit : Valid +[wp] [Qed] Goal typed_inconditional_exit_assigns_normal : Valid +[wp] Proved goals: 4 / 4 + Qed: 4 +[wp] Report in: 'tests/wp_bts/oracle_qualif/issue-684-exit.0.report.json' +[wp] Report out: 'tests/wp_bts/result_qualif/issue-684-exit.0.report.json' +------------------------------------------------------------- +Functions WP Alt-Ergo Total Success +inconditional_exit 4 - 4 100% +-------------------------------------------------------------