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 f5903c27cebde17678869f611dc67b077a86ea81..9ef9071f298c9d468daabf7d1648fa5ed6093f0b 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,31 +36,38 @@ 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, int blocking, const char *kind,
- const char *fct, const char *pred_txt,
- const char *file, int line) {
+void eacsl_runtime_assert(int predicate, eacsl_assert_data_t *data) {
if (eacsl_runtime_sound_verdict) {
if (!predicate) {
+ // clang-format off
STDERR("%s: In function '%s'\n"
"%s:%d: Error: %s failed:\n"
"\tThe failing predicate is:\n"
"\t%s.\n",
- file, fct, file, line, kind, pred_txt);
- if (blocking) {
+ data->file, data->fct,
+ data->file, data->line, data->kind,
+ data->pred_txt);
+ // clang-format on
+ if (data->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);
# else
- raise_abort(file, line); /* Raise abort signal */
+ raise_abort(data->file, data->line); /* Raise abort signal */
# endif
# endif
}
}
- } else
+ } else {
+ // clang-format off
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",
- file, fct, file, line, kind, predicate ? "ok" : "FAIL", pred_txt);
+ data->file, data->fct,
+ data->file, data->line, data->kind, predicate ? "ok" : "FAIL",
+ data->pred_txt);
+ // clang-format on
+ }
}
#endif
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 5a7dec8c2e9af58f59269a73abcc152cbddad4c3..b3ec636c80334f5e99908cb39109b585bdc50d3f 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
@@ -31,6 +31,7 @@
#include "../internals/e_acsl_alias.h"
#define eacsl_runtime_sound_verdict export_alias(sound_verdict)
+#define eacsl_assert_data_t export_alias(assert_data_t)
#define eacsl_runtime_assert export_alias(assert)
/*! E-ACSL instrumentation automatically sets this global to 0 if its verdict
@@ -39,26 +40,38 @@
For arithmetic properties, the verdict is always sound (?). */
extern int __attribute__((FC_BUILTIN)) eacsl_runtime_sound_verdict;
+/*! Data holding context information for E-ACSL assertions. */
+typedef struct eacsl_assert_data_t {
+ /*! integer representing if the assertion is blocking or not */
+ int blocking;
+ /*! C string representing a kind of annotation (e.g., "Assertion") */
+ const char *kind;
+ /*! stringified predicate */
+ const char *pred_txt;
+ /*! un-instrumented file of predicate placement */
+ const char *file;
+ /*! function of predicate placement in the un-instrumented file */
+ const char *fct;
+ /*! line of predicate placement in the un-instrumented file */
+ int line;
+ /*! values contributing to the predicate */
+ void *values;
+} __attribute__((__FC_BUILTIN__)) eacsl_assert_data_t;
+
/*! \brief Runtime assertion verifying a given predicate
- * \param pred integer code of a predicate
- * \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 */
-/*@ assigns \nothing;
+ * \param predicate integer code of a predicate
+ * \param data context data for the predicate. */
+/*@ requires \valid_read(data) && \initialized(data);
+ @ assigns \nothing;
@ behavior blocking:
- @ assumes blocking != 0;
- @ requires pred != 0;
+ @ assumes data->blocking != 0;
+ @ requires predicate != 0;
@ behavior non_blocking:
- @ assumes blocking == 0;
- @ check requires pred != 0;
+ @ assumes data->blocking == 0;
+ @ check requires predicate != 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)
+void eacsl_runtime_assert(int predicate, eacsl_assert_data_t *data)
__attribute__((FC_BUILTIN));
#endif // E_ACSL_ASSERT_H
diff --git a/src/plugins/e-acsl/src/code_generator/assert.ml b/src/plugins/e-acsl/src/code_generator/assert.ml
index 8be5d95be4be239351847fa5fe05151de1089ea0..6697390b0ee25494145821366952cb95823766ab 100644
--- a/src/plugins/e-acsl/src/code_generator/assert.ml
+++ b/src/plugins/e-acsl/src/code_generator/assert.ml
@@ -31,7 +31,10 @@ open Cil_types
type data = {
(** Indicates if some data have been registered in the context or not. *)
data_registered: bool;
- (* FIXME: fields added to hold information about the C variable in MR !3288 *)
+ (** [varinfo] representing the C variable for the assertion data. *)
+ data_vi: varinfo;
+ (** [exp] representing a pointer to the C variable for the assertion data. *)
+ data_ptr: exp;
}
(** External type representing the assertion context. Either [Some data] if we
@@ -40,10 +43,32 @@ type t = data option
let no_data = None
+(** C type for the [assert_data_t] structure. *)
+let assert_data_ctyp_lazy =
+ lazy (Globals.Types.find_type
+ Logic_typing.Typedef (Functions.RTL.mk_api_name "assert_data_t"))
+
let empty ~loc kf env =
- (* FIXME: C variable created in MR !3288 *)
- ignore (loc, kf);
- let data = { data_registered = false } in
+ let assert_data_cty = Lazy.force assert_data_ctyp_lazy in
+ let data_vi, _, env =
+ Env.new_var
+ ~loc
+ ~name:"assert_data"
+ env
+ kf
+ None
+ assert_data_cty
+ (fun vi _ ->
+ [ Smart_stmt.struct_local_init
+ ~loc
+ vi
+ [ "values", Smart_exp.null ~loc ] ])
+ in
+ let data =
+ { data_registered = false;
+ data_vi;
+ data_ptr = Cil.mkAddrOfVi data_vi }
+ in
Some data , env
let with_data_from ~loc kf env from =
@@ -75,8 +100,8 @@ let register ~loc kf env ?(force=false) name e adata =
The registration can be forced for expressions like [sizeof(int)] for
instance that are [Const] values but not directly known. *)
Some adata, env
- | Some _adata, _ ->
- let adata = { data_registered = true } in
+ | Some adata, _ ->
+ let adata = { adata with data_registered = true } in
(* FIXME: value registered to [adata] in MR !3288 *)
ignore (loc, kf, env, name);
Some adata, env
@@ -108,7 +133,17 @@ 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 e =
+let runtime_check_with_msg ~adata ~loc msg ~pred_kind kind kf env predicate_e =
+ let env = Env.push env in
+ let data_ptr, data_vi, env =
+ match adata with
+ | Some { data_ptr; data_vi } ->
+ data_ptr, data_vi, env
+ | None ->
+ let adata, env = empty ~loc kf env in
+ let adata = Option.get adata in
+ adata.data_ptr, adata.data_vi, env
+ in
let blocking =
match pred_kind with
| Assert -> Cil.one ~loc
@@ -116,23 +151,33 @@ let runtime_check_with_msg ~adata ~loc msg ~pred_kind kind kf env e =
| Admit ->
Options.fatal "No runtime check should be generated for 'admit' clauses"
in
+ let kind = kind_to_string loc kind in
+ let pred_txt = Cil.mkString ~loc msg in
let start_pos = fst loc in
- let file = start_pos.Filepath.pos_path in
- let line = start_pos.Filepath.pos_lnum in
- (* FIXME: [adata] support in MR !3288 *)
- ignore adata;
- let stmt =
- Smart_stmt.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 file =
+ Cil.mkString
+ ~loc
+ (Filepath.Normalized.to_pretty_string start_pos.Filepath.pos_path)
+ in
+ 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 "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 block, env =
+ Env.pop_and_get
+ env
+ (Smart_stmt.block_from_stmts (List.rev stmts))
+ ~global_clear:false
+ Env.Middle
in
- stmt, env
+ Smart_stmt.block_stmt block, env
let runtime_check ~adata ~pred_kind kind kf env e p =
let loc = p.pred_loc in