diff --git a/share/libc/stdlib.h b/share/libc/stdlib.h
index 5d903a44e9dbe994c36705a2f06681347ee5175c..a41a685c5321cca6c0ff95c1b67f97c9d8492494 100644
--- a/share/libc/stdlib.h
+++ b/share/libc/stdlib.h
@@ -454,8 +454,11 @@ extern void *realloc(void *ptr, size_t size);
/* ISO C: 7.20.4 */
-/*@ assigns \nothing;
- @ ensures never_terminates: \false; */
+/*@
+ assigns \exit_status \from \nothing;
+ exits status: \exit_status != EXIT_SUCCESS;
+ ensures never_terminates: \false;
+ */
extern void abort(void) __attribute__ ((__noreturn__));
/*@ assigns \result \from \nothing ;*/
@@ -465,7 +468,8 @@ extern int atexit(void (*func)(void));
extern int at_quick_exit(void (*func)(void));
/*@
- assigns \nothing;
+ assigns \exit_status \from status;
+ exits status: \exit_status == status;
ensures never_terminates: \false;
*/
extern void exit(int status) __attribute__ ((__noreturn__));
diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index 3df4c0086321b7029848e3f25d6b536634a12e38..ea48d5ad04b302cde1962649b6154f0c8b2e16db 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -115,20 +115,21 @@ let eval_assigns kf state assigns =
not (Kernel_function.is_formal v kf)
| Base.CLogic_Var _ | Base.Null | Base.String _ -> true)
in
+ let out_term = out.it_content in
let outputs_under, outputs_over, deps =
try
- if Logic_utils.is_result out.it_content
+ if Logic_const.(is_result out_term || is_exit_status out_term)
then (Zone.bottom, Zone.bottom, Zone.bottom)
else
let loc_out_under, loc_out_over, deps =
- !Db.Properties.Interp.loc_to_loc_under_over ~result:None state out.it_content
+ !Db.Properties.Interp.loc_to_loc_under_over ~result:None state out_term
in
(enumerate_valid_bits_under Write loc_out_under,
enumerate_valid_bits Write loc_out_over,
clean_deps deps)
with Db.Properties.Interp.No_conversion ->
Inout_parameters.warning ~current:true ~once:true
- "failed to interpret assigns clause '%a'" Printer.pp_term out.it_content;
+ "failed to interpret assigns clause '%a'" Printer.pp_term out_term;
(Zone.bottom, Zone.top, Zone.top)
in
(* Compute all inputs as a zone *)
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%
+-------------------------------------------------------------
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index d0942621eceadea65324eea022577dd0fad7f0f9..f1bb1d42421189f8e087c94215e6f4d70d1cf335 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -2346,8 +2346,11 @@ extern void free(void *p);
*/
extern void *realloc(void *ptr, size_t size);
-/*@ ensures never_terminates: \false;
- assigns \nothing; */
+/*@ exits status: \exit_status ≢ 0;
+ ensures never_terminates: \false;
+
+ assigns \exit_status \from \nothing;
+ */
extern __attribute__((__noreturn__)) void abort(void);
/*@ assigns \result;
@@ -2358,8 +2361,11 @@ extern int atexit(void (*func)(void));
assigns \result \from \nothing; */
extern int at_quick_exit(void (*func)(void));
-/*@ ensures never_terminates: \false;
- assigns \nothing; */
+/*@ exits status: \exit_status ≡ \old(status);
+ ensures never_terminates: \false;
+
+ assigns \exit_status \from status;
+ */
extern __attribute__((__noreturn__)) void exit(int status);
/*@ ensures never_terminates: \false;
diff --git a/tests/spec/oracle/assigns_result.res.oracle b/tests/spec/oracle/assigns_result.res.oracle
index be625108d0cc0a76d746cf2a203d0f00b79b70d4..f492644ff778a0fd8afe7cbcf2d9cd7cf94f4062 100644
--- a/tests/spec/oracle/assigns_result.res.oracle
+++ b/tests/spec/oracle/assigns_result.res.oracle
@@ -11,8 +11,6 @@
[eva] Done for function f
[eva] computing for function g <- main.
Called from tests/spec/assigns_result.i:16.
-[inout] tests/spec/assigns_result.i:16: Warning:
- failed to interpret assigns clause '\exit_status'
[eva] using specification for function g
[eva] tests/spec/assigns_result.i:16: Warning:
cannot interpret assigns clause \exit_status