diff --git a/ACSLTermOrPredicate.cpp b/ACSLTermOrPredicate.cpp
index b81e6ceab25efb8f0377a2bd37760cca60d81c19..0ae02b14663dafe5b956b2a2524add9105d3e2fe 100644
--- a/ACSLTermOrPredicate.cpp
+++ b/ACSLTermOrPredicate.cpp
@@ -6115,6 +6115,26 @@ TermOrPredicate::readToken(Parser::State& state, Parser::Arguments& arguments) {
DefineGotoCase(AfterPrimary)
}
break;
+ case KeywordToken::TExitStatus:
+ if (excludeTypeAsResult()) {
+ logic_type lt = logic_type_Linteger();
+ logic_var status =
+ logic_var_cons(
+ qualified_name_cons(NULL, "\\exit_status"), LVBUILTIN);
+ term tres =
+ term_cons(
+ term_node_TLval(
+ term_lval_cons(
+ term_lhost_TVar(status),term_offset_TNoOffset())),
+ arguments.newTokenLocation(),NULL);
+ predicate_named pres =
+ convertTermToPredicate(lt,tres,arguments);
+ pushLastArgument(lt,tres,pres);
+ arguments.extendLocationWithToken(_loc);
+ if (_doesStopTypeAmbiguity)
+ DefineTReduce;
+ DefineGotoCase(AfterPrimary)
+ }
case KeywordToken::TAt:
if (excludeTypeAsResult()) {
_startLocation = arguments.newTokenLocation();
diff --git a/ACSLToken.cpp b/ACSLToken.cpp
index f904a218931f98d8c732a2eeb91e238d29642dc0..ec40d5bbef99b47041458bf56b42889b40d8c394 100644
--- a/ACSLToken.cpp
+++ b/ACSLToken.cpp
@@ -637,10 +637,10 @@ KeywordToken::text() const {
case TSubset: t = "\\subset"; break;
case TEmpty: t = "\\empty"; break;
case TValid: t = "\\valid"; break;
- case TValidRead: t = "\\validread"; break;
- case TValidIndex: t = "\\validindex"; break;
- case TValidRange: t = "\\validrange"; break;
- case TValidFunction: t = "\\validfunction"; break;
+ case TValidRead: t = "\\valid_read"; break;
+ case TValidIndex: t = "\\valid_index"; break;
+ case TValidRange: t = "\\valid_range"; break;
+ case TValidFunction: t = "\\valid_function"; break;
case TInductive: t = "inductive"; break;
case TLoop: t = "loop"; break;
case TVariant: t = "variant"; break;
@@ -650,7 +650,7 @@ KeywordToken::text() const {
case TBreaks: t = "breaks"; break;
case TContinues: t = "continues"; break;
case TReturns: t = "returns"; break;
- case TExitStatus: t = "\\exitstatus"; break;
+ case TExitStatus: t = "\\exit_status"; break;
case TFrom: t = "\\from"; break;
case TGlobal: t = "global"; break;
case TWeak: t = "\\weak"; break;
diff --git a/convert_acsl.ml b/convert_acsl.ml
index 16c9ea78521c14d7b83c09ca00f731440716999a..b705069d8ec59610e287cb3fe603e0475fc343d8 100644
--- a/convert_acsl.ml
+++ b/convert_acsl.ml
@@ -31,7 +31,8 @@ let convert_var env is_extern_c vi =
let n, tk
= Convert_env.typedef_normalize env vi.logic_var_lv_name TStandard
in Mangling.mangle n tk None
- | LVFormal | LVQuant | LVLocal | LVCLocal-> vi.logic_var_lv_name.decl_name
+ | LVFormal | LVQuant | LVLocal | LVCLocal | LVBuiltin ->
+ vi.logic_var_lv_name.decl_name
let convert_logic_label = function
| StmtLabel s -> s
diff --git a/intermediate_format.ast b/intermediate_format.ast
index 047c4a7717d56558e7a0823accac815d71a2d890..3c8e3be007cf1aa3fc2b60dbbbc61f244311c24f 100644
--- a/intermediate_format.ast
+++ b/intermediate_format.ast
@@ -841,6 +841,7 @@ type logic_var_kind =
| LVFormal {} (** formal parameter of a logic function / predicate *)
| LVQuant {} (** Bound by a quantifier or a Lambda abstraction. *)
| LVLocal {} (** local \let *)
+ | LVBuiltin {} (** specific identifier, e.g. \\exit_status. *)
;;
type logic_var_def =
diff --git a/tests/basic/oracle/placement_new.res.oracle b/tests/basic/oracle/placement_new.res.oracle
index d47b5e1f7ba30149b9a18edf5f4952d4d7015f0b..ca34acb5b41428663672a2e2a26cfbd053057e54 100644
--- a/tests/basic/oracle/placement_new.res.oracle
+++ b/tests/basic/oracle/placement_new.res.oracle
@@ -844,6 +844,13 @@ void *calloc(size_t nmemb, size_t size);
*/
void *realloc(void *ptr, size_t size);
+/*@ exits status: \exit_status ≢ 0;
+ ensures never_terminates: \false;
+
+ assigns \exit_status \from \nothing;
+ */
+void abort(void);
+
/*@ assigns \result;
assigns \result \from \nothing; */
int atexit(void (*func)(void));
@@ -852,6 +859,13 @@ int atexit(void (*func)(void));
assigns \result \from \nothing; */
int at_quick_exit(void (*func)(void));
+/*@ exits status: \exit_status ≡ \old(status);
+ ensures never_terminates: \false;
+
+ assigns \exit_status \from status;
+ */
+void exit(int status);
+
/*@ ensures never_terminates: \false;
assigns \nothing; */
void _Exit(int status);
diff --git a/tests/basic/oracle/placement_newb.res.oracle b/tests/basic/oracle/placement_newb.res.oracle
index b0e3e6886d6cf469b5928ae283a7ea709cda43d6..a3e15f4249f144547526959759bdea1f9423ac98 100644
--- a/tests/basic/oracle/placement_newb.res.oracle
+++ b/tests/basic/oracle/placement_newb.res.oracle
@@ -813,6 +813,13 @@ void *calloc(size_t nmemb, size_t size);
*/
void *realloc(void *ptr, size_t size);
+/*@ exits status: \exit_status ≢ 0;
+ ensures never_terminates: \false;
+
+ assigns \exit_status \from \nothing;
+ */
+void abort(void);
+
/*@ assigns \result;
assigns \result \from \nothing; */
int atexit(void (*func)(void));
@@ -821,6 +828,13 @@ int atexit(void (*func)(void));
assigns \result \from \nothing; */
int at_quick_exit(void (*func)(void));
+/*@ exits status: \exit_status ≡ \old(status);
+ ensures never_terminates: \false;
+
+ assigns \exit_status \from status;
+ */
+void exit(int status);
+
/*@ ensures never_terminates: \false;
assigns \nothing; */
void _Exit(int status);
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
index 6c28ec2940a3d7d75ac17729daa080b73734705a..4c0014464f0a196ff0765ef858861cae928db0c1 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
@@ -3304,6 +3304,13 @@ void *calloc(size_t nmemb, size_t size);
*/
void *realloc(void *ptr, size_t size);
+/*@ exits status: \exit_status ≢ 0;
+ ensures never_terminates: \false;
+
+ assigns \exit_status \from \nothing;
+ */
+void abort(void);
+
/*@ assigns \result;
assigns \result \from \nothing; */
int atexit(void (*func)(void));
@@ -3312,6 +3319,13 @@ int atexit(void (*func)(void));
assigns \result \from \nothing; */
int at_quick_exit(void (*func)(void));
+/*@ exits status: \exit_status ≡ \old(status);
+ ensures never_terminates: \false;
+
+ assigns \exit_status \from status;
+ */
+void exit(int status);
+
/*@ ensures never_terminates: \false;
assigns \nothing; */
void _Exit(int status);
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
index 1c2574f4743b589c03d858bdaa70302345d37561..7fd8b8b8cbd279f859d0708f0d02d6785cc7cb8b 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
@@ -3057,6 +3057,13 @@ void *calloc(size_t nmemb, size_t size);
*/
void *realloc(void *ptr, size_t size);
+/*@ exits status: \exit_status ≢ 0;
+ ensures never_terminates: \false;
+
+ assigns \exit_status \from \nothing;
+ */
+void abort(void);
+
/*@ assigns \result;
assigns \result \from \nothing; */
int atexit(void (*func)(void));
@@ -3065,6 +3072,13 @@ int atexit(void (*func)(void));
assigns \result \from \nothing; */
int at_quick_exit(void (*func)(void));
+/*@ exits status: \exit_status ≡ \old(status);
+ ensures never_terminates: \false;
+
+ assigns \exit_status \from status;
+ */
+void exit(int status);
+
/*@ ensures never_terminates: \false;
assigns \nothing; */
void _Exit(int status);
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
index 4fda65f9c232d75e7daa429a8f6a6534559a96df..b078461faee210b07d6f13a08255372558c40299 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
@@ -3063,6 +3063,13 @@ void *calloc(size_t nmemb, size_t size);
*/
void *realloc(void *ptr, size_t size);
+/*@ exits status: \exit_status ≢ 0;
+ ensures never_terminates: \false;
+
+ assigns \exit_status \from \nothing;
+ */
+void abort(void);
+
/*@ assigns \result;
assigns \result \from \nothing; */
int atexit(void (*func)(void));
@@ -3071,6 +3078,13 @@ int atexit(void (*func)(void));
assigns \result \from \nothing; */
int at_quick_exit(void (*func)(void));
+/*@ exits status: \exit_status ≡ \old(status);
+ ensures never_terminates: \false;
+
+ assigns \exit_status \from status;
+ */
+void exit(int status);
+
/*@ ensures never_terminates: \false;
assigns \nothing; */
void _Exit(int status);