[eacsl] Split the name from the predicate in `runtime_check_with_msg`

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);

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 */

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

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].