From df233f608e1389b236726916af13b2539292515a Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 2 Dec 2019 17:08:38 +0100
Subject: [PATCH] [ACSL++] add support for \exit_status
---
ACSLTermOrPredicate.cpp | 20 +++++++++++++++++++
ACSLToken.cpp | 10 +++++-----
convert_acsl.ml | 3 ++-
intermediate_format.ast | 1 +
tests/basic/oracle/placement_new.res.oracle | 14 +++++++++++++
tests/basic/oracle/placement_newb.res.oracle | 14 +++++++++++++
.../stl_shared_ptr_mistake10.res.oracle | 14 +++++++++++++
.../oracle/stl_shared_ptr_mistake5.res.oracle | 14 +++++++++++++
.../oracle/stl_shared_ptr_mistake6.res.oracle | 14 +++++++++++++
9 files changed, 98 insertions(+), 6 deletions(-)
diff --git a/ACSLTermOrPredicate.cpp b/ACSLTermOrPredicate.cpp
index b81e6cea..0ae02b14 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 f904a218..ec40d5bb 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 16c9ea78..b705069d 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 047c4a77..3c8e3be0 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 d47b5e1f..ca34acb5 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 b0e3e688..a3e15f42 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 6c28ec29..4c001446 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 1c2574f4..7fd8b8b8 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 4fda65f9..b078461f 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);
--
GitLab