[libC] fixes specification of abort and exit functions: adding a test for wp plugin

src/plugins/wp/tests/wp_bts/issue-684-exit.c

+#include "stdlib.h"
+/*@ assigns \nothing;
+  @ exits \exit_status == state;
+  @ ensures \false;
+*/
+void inconditional_exit(int state) {
+  exit (state);
+}

src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle

+# 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.
+
+------------------------------------------------------------

src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.0.report.json

+{ "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 } } } } }

src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.res.oracle

+# 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%
+-------------------------------------------------------------