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 0d1158d3b7bf95f8f254905f500a2ec0ae883bd5..e08e827589b870e8a7a5caa3388b3ef405276366 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
@@ -46,6 +46,12 @@ void eacsl_print_values(eacsl_assert_data_t *data) {
}
#ifndef E_ACSL_EXTERNAL_ASSERT
+
+/*! \brief Return `str` id `cond` is true, an empty string otherwise. */
+# define STR_IF(cond, str) ((cond) ? (str) : "")
+/*! \brief Return `str` if the string is not null, an empty string otherwise. */
+# define STR_IF_NOT_NULL(str) STR_IF(str, str)
+
/*! \brief Default implementation of E-ACSL runtime assertions */
void eacsl_runtime_assert(int predicate, eacsl_assert_data_t *data) {
if (eacsl_runtime_sound_verdict) {
@@ -55,9 +61,11 @@ void eacsl_runtime_assert(int predicate, eacsl_assert_data_t *data) {
STDERR("%s: In function '%s'\n"
"%s:%d: Error: %s failed:\n"
"\tThe failing predicate is:\n"
- "\t%s.\n",
+ "\t%s%s%s.\n",
data->file, data->fct,
data->file, data->line, data->kind,
+ STR_IF_NOT_NULL(data->name),
+ STR_IF(data->name, ":\n\t\t"),
data->pred_txt);
// clang-format on
eacsl_print_values(data);
@@ -78,9 +86,11 @@ void eacsl_runtime_assert(int predicate, eacsl_assert_data_t *data) {
// clang-format off
STDERR("%s: In function '%s'\n"
"%s:%d: %s valid:\n"
- "\t%s.\n",
+ "\t%s%s%s.\n",
data->file, data->fct,
data->file, data->line, data->kind,
+ STR_IF_NOT_NULL(data->name),
+ STR_IF(data->name, ":\n\t\t"),
data->pred_txt);
// clang-format on
eacsl_print_values(data);
@@ -93,9 +103,11 @@ void eacsl_runtime_assert(int predicate, eacsl_assert_data_t *data) {
STDERR("%s: In function '%s'\n"
"%s:%d: Warning: no sound verdict for %s (guess: %s).\n"
"\tthe considered predicate is:\n"
- "\t%s\n",
+ "\t%s%s%s\n",
data->file, data->fct,
data->file, data->line, data->kind, predicate ? "ok" : "FAIL",
+ STR_IF_NOT_NULL(data->name),
+ STR_IF(data->name, ":\n\t\t"),
data->pred_txt);
// clang-format on
eacsl_print_values(data);
diff --git a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert_data.h b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert_data.h
index 7a91b70ac09bd140111b81f58e064ce8d63a55ae..aa94970d5ceaccc64dceb6cb373404835d9310e8 100644
--- a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert_data.h
+++ b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert_data.h
@@ -190,6 +190,8 @@ typedef struct eacsl_assert_data_t {
int blocking;
/*! C string representing a kind of annotation (e.g., "Assertion") */
const char *kind;
+ /*! name identifying the predicate */
+ const char *name;
/*! stringified predicate */
const char *pred_txt;
/*! un-instrumented file of predicate placement */
diff --git a/src/plugins/e-acsl/src/code_generator/assert.ml b/src/plugins/e-acsl/src/code_generator/assert.ml
index 2321d56a757a74b949cb501e0ee961096daf2f61..f2528e9c6dfabee5d8a98719a5063c08ee2abc38 100644
--- a/src/plugins/e-acsl/src/code_generator/assert.ml
+++ b/src/plugins/e-acsl/src/code_generator/assert.ml
@@ -205,7 +205,7 @@ let kind_to_string loc k =
| Smart_stmt.Variant -> "Variant"
| Smart_stmt.RTE -> "RTE")
-let runtime_check_with_msg ~adata ~loc msg ~pred_kind kind kf env predicate_e =
+let runtime_check_with_msg ~adata ~loc ?(name="") msg ~pred_kind kind kf env predicate_e =
let env = Env.push env in
let data_registered, data_ptr, data_vi, env =
match adata with
@@ -234,14 +234,27 @@ let runtime_check_with_msg ~adata ~loc msg ~pred_kind kind kf env predicate_e =
let fct = Cil.mkString ~loc (Functions.RTL.get_original_name kf) in
let line = Cil.integer ~loc start_pos.Filepath.pos_lnum in
let stmts =
- [ Smart_stmt.rtl_call ~loc "assert" [ predicate_e; data_ptr ];
- Smart_stmt.assigns_field ~loc data_vi "line" line;
+ [ Smart_stmt.assigns_field ~loc data_vi "line" line;
Smart_stmt.assigns_field ~loc data_vi "fct" fct;
Smart_stmt.assigns_field ~loc data_vi "file" file;
Smart_stmt.assigns_field ~loc data_vi "pred_txt" pred_txt;
Smart_stmt.assigns_field ~loc data_vi "kind" kind;
Smart_stmt.assigns_field ~loc data_vi "blocking" blocking ]
in
+ let stmts =
+ if Datatype.String.equal name "" then
+ stmts
+ else
+ Smart_stmt.assigns_field
+ ~loc
+ data_vi
+ "name"
+ (Cil.mkString ~loc name)
+ :: stmts
+ in
+ let stmts =
+ Smart_stmt.rtl_call ~loc "assert" [ predicate_e; data_ptr ] :: stmts
+ in
let stmts=
if data_registered then
Smart_stmt.rtl_call ~loc "assert_clean" [ data_ptr ] :: stmts
@@ -259,5 +272,7 @@ let runtime_check_with_msg ~adata ~loc msg ~pred_kind kind kf env predicate_e =
let runtime_check ~adata ~pred_kind kind kf env e p =
let loc = p.pred_loc in
+ let name = String.concat "/" p.pred_name in
+ let p = { p with pred_name = [] } in
let msg = Format.asprintf "%a@?" Printer.pp_predicate p in
- runtime_check_with_msg ~adata ~loc msg ~pred_kind kind kf env e
+ runtime_check_with_msg ~adata ~loc ~name msg ~pred_kind kind kf env e
diff --git a/src/plugins/e-acsl/src/code_generator/assert.mli b/src/plugins/e-acsl/src/code_generator/assert.mli
index d81ed28c982d1fe1ac45c66cb85e13326ed4b61b..30ae0b268d0f09f5e14dbea4654f98576a5fdbe5 100644
--- a/src/plugins/e-acsl/src/code_generator/assert.mli
+++ b/src/plugins/e-acsl/src/code_generator/assert.mli
@@ -118,6 +118,7 @@ val runtime_check:
val runtime_check_with_msg:
adata:t ->
loc:location ->
+ ?name:string ->
string ->
pred_kind:predicate_kind ->
Smart_stmt.annotation_kind ->
@@ -125,12 +126,13 @@ val runtime_check_with_msg:
Env.t ->
exp ->
stmt * Env.t
-(** [runtime_check_with_msg ~adata ~loc msg ~pred_kind kind kf env e] generates
- a runtime check for [e] (or [!e] if [reverse] is [true]) by building a call
- to [__e_acsl_assert].
+(** [runtime_check_with_msg ~adata ~loc ?name msg ~pred_kind kind kf env e]
+ generates a runtime check for [e] (or [!e] if [reverse] is [true]) by
+ building a call to [__e_acsl_assert].
[adata] is the assertion context holding the data contributing to the
assertion.
[loc] is the location printed in the message if the runtime check fails.
+ [name] is the name of the predicate printed if the runtime check fails.
[msg] is the message printed if the runtime check fails.
[pred_kind] indicates if the assert should be blocking or not.
[kind] is the annotation kind of [p].