From af6faaf30f254a3b88578773640b57c30b0eb2e8 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Tue, 16 Feb 2021 10:27:24 +0100
Subject: [PATCH] [eacsl] Update `__e_acsl_assert()` to support a `blocking`
parameter
---
.../instrumentation_model/e_acsl_assert.c | 10 ++++---
.../instrumentation_model/e_acsl_assert.h | 18 +++++++++----
.../e-acsl/src/code_generator/smart_stmt.ml | 14 +++++++---
.../e-acsl/src/code_generator/smart_stmt.mli | 26 +++++++++++--------
4 files changed, 45 insertions(+), 23 deletions(-)
diff --git a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.c b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.c
index 076a44f350f..e6a105f2ecc 100644
--- a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.c
+++ b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.c
@@ -36,8 +36,8 @@ int eacsl_runtime_sound_verdict = 1;
#ifndef E_ACSL_EXTERNAL_ASSERT
/*! \brief Default implementation of E-ACSL runtime assertions */
-void eacsl_runtime_assert(int predicate, const char *kind, const char *fct,
- const char *pred_txt, const char * file, int line) {
+void eacsl_runtime_assert(int predicate, int blocking, const char *kind,
+ const char *fct, const char *pred_txt, const char * file, int line) {
if (eacsl_runtime_sound_verdict) {
if (! predicate) {
STDERR("%s: In function '%s'\n"
@@ -45,13 +45,15 @@ void eacsl_runtime_assert(int predicate, const char *kind, const char *fct,
"\tThe failing predicate is:\n"
"\t%s.\n",
file, fct, file, line, kind, pred_txt);
+ if (blocking) {
#ifndef E_ACSL_NO_ASSERT_FAIL /* Do fail on assertions */
#ifdef E_ACSL_FAIL_EXITCODE /* Fail by exit with a given code */
- exit(E_ACSL_FAIL_EXITCODE);
+ exit(E_ACSL_FAIL_EXITCODE);
#else
- raise_abort(file, line); /* Raise abort signal */
+ raise_abort(file, line); /* Raise abort signal */
#endif
#endif
+ }
}
} else
STDERR("%s: In function '%s'\n"
diff --git a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.h b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.h
index 46e8fe3a6ad..6cc1a782efd 100644
--- a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.h
+++ b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.h
@@ -41,15 +41,23 @@ extern int eacsl_runtime_sound_verdict;
/*! \brief Runtime assertion verifying a given predicate
* \param pred integer code of a predicate
- * \param kind C string representing a kind an annotation (e.g., "Assertion")
+ * \param blocking integer representing if the assertion is blocking or not
+ * \param kind C string representing a kind of annotation (e.g., "Assertion")
* \param fct
* \param pred_txt stringified predicate
* \param file un-instrumented file of predicate placement
* \param line line of predicate placement in the un-instrumented file */
-/*@ requires pred != 0;
- @ assigns \nothing; */
-void eacsl_runtime_assert(int pred, const char *kind, const char *fct,
- const char *pred_txt, const char * file, int line)
+/*@ assigns \nothing;
+ @ behavior blocking:
+ @ assumes blocking != 0;
+ @ requires pred != 0;
+ @ behavior non_blocking:
+ @ assumes blocking == 0;
+ @ check requires pred != 0;
+ @ complete behaviors;
+ @ disjoint behaviors; */
+void eacsl_runtime_assert(int pred, int blocking, const char *kind,
+ const char *fct, const char *pred_txt, const char * file, int line)
__attribute__((FC_BUILTIN));
#endif // E_ACSL_ASSERT_H
diff --git a/src/plugins/e-acsl/src/code_generator/smart_stmt.ml b/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
index c126fe01e0b..1cc37e8113c 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
+++ b/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
@@ -177,25 +177,33 @@ let mark_readonly vi =
let loc = vi.vdecl in
rtl_call ~loc "mark_readonly" [ Cil.evar ~loc vi ]
-let runtime_check_with_msg ~loc msg kind kf e =
+let runtime_check_with_msg ~loc msg ~pred_kind kind kf e =
+ let blocking =
+ match pred_kind with
+ | Assert -> Cil.one ~loc
+ | Check -> Cil.zero ~loc
+ | Admit ->
+ Options.fatal "No runtime check should be generated for 'admit' clauses"
+ in
let file = (fst loc).Filepath.pos_path in
let line = (fst loc).Filepath.pos_lnum in
rtl_call ~loc
"assert"
[ e;
+ blocking;
kind_to_string loc kind;
Cil.mkString ~loc (Functions.RTL.get_original_name kf);
Cil.mkString ~loc msg;
Cil.mkString ~loc (Filepath.Normalized.to_pretty_string file);
Cil.integer loc line ]
-let runtime_check kind kf e p =
+let runtime_check ~pred_kind kind kf e p =
let loc = p.pred_loc in
let msg =
Kernel.Unicode.without_unicode
(Format.asprintf "%a@?" Printer.pp_predicate) p
in
- runtime_check_with_msg ~loc msg kind kf e
+ runtime_check_with_msg ~loc msg ~pred_kind kind kf e
(*
Local Variables:
diff --git a/src/plugins/e-acsl/src/code_generator/smart_stmt.mli b/src/plugins/e-acsl/src/code_generator/smart_stmt.mli
index abd797824e9..c56404a5a71 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_stmt.mli
+++ b/src/plugins/e-acsl/src/code_generator/smart_stmt.mli
@@ -107,19 +107,23 @@ type annotation_kind =
| RTE
val runtime_check:
- annotation_kind -> kernel_function -> exp -> predicate -> stmt
-(** [runtime_check kind kf e p] generates a runtime check for predicate [p]
- by building a call to [__e_acsl_assert]. [e] (or [!e] if [reverse] is set to
- [true]) is the C translation of [p], [kf] is the current kernel_function and
- [kind] is the annotation kind of [p]. *)
+ pred_kind:predicate_kind -> annotation_kind -> kernel_function -> exp ->
+ predicate -> stmt
+(** [runtime_check ~pred_kind kind kf e p] generates a runtime check for
+ predicate [p] by building a call to [__e_acsl_assert]. [e] (or [!e] if
+ [reverse] is set to [true]) is the C translation of [p], [kf] is the current
+ kernel_function, [kind] is the annotation kind of [p] and [pred_kind]
+ indicates if the assert should be blocking or not. *)
val runtime_check_with_msg:
- loc:location -> string -> annotation_kind -> kernel_function -> exp -> stmt
-(** [runtime_check_with_msg kind kf e msg] generates a runtime check for [e]
- (or [!e] if [reverse] is [true]) by building a call to [__e_acsl_assert].
- [msg] is the message printed if the runtime check fails. [loc] is the
- location printed in the message if the runtime check fails. [kf] is the
- current kernel_function and [kind] is the annotation kind of [p]. *)
+ loc:location -> string -> pred_kind:predicate_kind -> annotation_kind ->
+ kernel_function -> exp -> stmt
+(** [runtime_check_with_msg ~loc msg ~pred_kind kind kf e] generates a runtime
+ check for [e] (or [!e] if [reverse] is [true]) by building a call to
+ [__e_acsl_assert]. [msg] is the message printed if the runtime check fails.
+ [loc] is the location printed in the message if the runtime check fails.
+ [kf] is the current kernel_function, [kind] is the annotation kind of [p]
+ and [pred_kind] indicates if the assert should be blocking or not. *)
(*
Local Variables:
--
GitLab