From 51efacc6618db378b56f563882c0a2d090b9a2c4 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Thu, 25 Nov 2021 16:15:35 +0100
Subject: [PATCH] [eacsl] Split the name from the predicate in
`runtime_check_with_msg`
---
.../instrumentation_model/e_acsl_assert.c | 18 ++++++++++++---
.../e_acsl_assert_data.h | 2 ++
.../e-acsl/src/code_generator/assert.ml | 23 +++++++++++++++----
.../e-acsl/src/code_generator/assert.mli | 8 ++++---
4 files changed, 41 insertions(+), 10 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 0d1158d3b7b..e08e827589b 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 7a91b70ac09..aa94970d5ce 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 2321d56a757..f2528e9c6df 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 d81ed28c982..30ae0b268d0 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].
--
GitLab