diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index aabe3b48e767d435cc5bf269e10af2c3c1b81425..5aab9fbc89d442697ff0c23e63064552d0e55623 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -74,11 +74,11 @@ CODE_GENERATOR_CMI:=$(addprefix src/code_generator/, $(CODE_GENERATOR_CMI))
SRC_CODE_GENERATOR:= \
smart_exp \
- assert \
smart_stmt \
gmp \
label \
env \
+ assert \
rational \
typed_number \
logic_functions \
diff --git a/src/plugins/e-acsl/src/code_generator/assert.ml b/src/plugins/e-acsl/src/code_generator/assert.ml
index b038e1bcaa13d577f63276de0ac7c6836ca739c1..55cfde74618fa5bd4ebdde26a0fb543fb2cd1952 100644
--- a/src/plugins/e-acsl/src/code_generator/assert.ml
+++ b/src/plugins/e-acsl/src/code_generator/assert.ml
@@ -90,3 +90,42 @@ let register_term ~loc kf env ?force t e adata =
let register_pred ~loc kf env ?force p e adata =
let name = Format.asprintf "@[%a@]" Printer.pp_predicate p in
register ~loc kf env name ?force e adata
+
+let kind_to_string loc k =
+ Cil.mkString
+ ~loc
+ (match k with
+ | Smart_stmt.Assertion -> "Assertion"
+ | Smart_stmt.Precondition -> "Precondition"
+ | Smart_stmt.Postcondition -> "Postcondition"
+ | Smart_stmt.Invariant -> "Invariant"
+ | Smart_stmt.Variant -> "Variant"
+ | Smart_stmt.RTE -> "RTE")
+
+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
+ 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 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 ~pred_kind kind kf e
diff --git a/src/plugins/e-acsl/src/code_generator/assert.mli b/src/plugins/e-acsl/src/code_generator/assert.mli
index 573bcb7a5e2c5f52724855b09d37d1334b58ee2b..dc33a5e8cb944dcbdda90056a17c299dc2d7badd 100644
--- a/src/plugins/e-acsl/src/code_generator/assert.mli
+++ b/src/plugins/e-acsl/src/code_generator/assert.mli
@@ -92,3 +92,31 @@ val register_pred:
corresponding to the predicate [p] to the assertion context [adata]. The
parameter [force] has the same signification than for the function
[register]. *)
+
+val runtime_check:
+ pred_kind:predicate_kind ->
+ Smart_stmt.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 ->
+ pred_kind:predicate_kind ->
+ Smart_stmt.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. *)
diff --git a/src/plugins/e-acsl/src/code_generator/contract.ml b/src/plugins/e-acsl/src/code_generator/contract.ml
index 20dc21dd7a67a47b9792961ae60d43af11a93692..9e81de5400a5f7b33ed1ea39652575d46fb02048 100644
--- a/src/plugins/e-acsl/src/code_generator/contract.ml
+++ b/src/plugins/e-acsl/src/code_generator/contract.ml
@@ -364,7 +364,7 @@ let check_requires kf kinstr env contract =
requires
in
let stmt =
- Smart_stmt.runtime_check
+ Assert.runtime_check
~pred_kind
Smart_stmt.Precondition
kf
@@ -498,7 +498,7 @@ let check_active_behaviors ~ppt_to_translate ~get_or_create_var kf kinstr env co
(* Create assertions for complete and disjoint behaviors checks *)
let create_assert_stmt bop msg =
- Smart_stmt.runtime_check_with_msg
+ Assert.runtime_check_with_msg
~loc
msg
~pred_kind:Assert
@@ -669,7 +669,7 @@ let check_post_conds kf kinstr env contract =
post_cond
in
let stmt =
- Smart_stmt.runtime_check
+ Assert.runtime_check
~pred_kind
Smart_stmt.Postcondition
kf
diff --git a/src/plugins/e-acsl/src/code_generator/logic_array.ml b/src/plugins/e-acsl/src/code_generator/logic_array.ml
index fd0f45a325cf236baabe260b3b7fc303161bed62..1cec9121aed53af9b8e0b80942a29bbfbaab1713 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_array.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_array.ml
@@ -241,7 +241,7 @@ let comparison_to_exp ~loc kf env ~name bop array1 array2 =
in
let p = { p with pred_name = "array_coercion" :: p.pred_name } in
let stmt =
- Smart_stmt.runtime_check ~pred_kind:Assert Smart_stmt.RTE kf e p
+ Assert.runtime_check ~pred_kind:Assert Smart_stmt.RTE kf e p
in
stmt :: stmts, env
in
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index eba5a6884df10a98ab4fa6cb95c70f4f48de59fc..804eac52375bab9829e69ec75c0afd4d3ce36774 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -108,7 +108,7 @@ let handle_annotations env kf stmt =
Printer.pp_term t
in
let stmt =
- Smart_stmt.runtime_check_with_msg
+ Assert.runtime_check_with_msg
~loc
msg
~pred_kind:Assert
@@ -148,14 +148,14 @@ let handle_annotations env kf stmt =
in
let stmt =
Smart_stmt.block_from_stmts [
- Smart_stmt.runtime_check_with_msg
+ Assert.runtime_check_with_msg
~loc
msg1
~pred_kind:Assert
Smart_stmt.Variant
kf
variant_pos_e;
- Smart_stmt.runtime_check_with_msg
+ Assert.runtime_check_with_msg
~loc
msg2
~pred_kind:Assert
@@ -300,7 +300,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
| Some p ->
let e, env = !predicate_to_exp_ref kf (Env.push env) p in
let stmt, env =
- Smart_stmt.runtime_check ~pred_kind:Assert Smart_stmt.RTE kf e p, env
+ Assert.runtime_check ~pred_kind:Assert Smart_stmt.RTE kf e p, env
in
let b, env = Env.pop_and_get env stmt ~global_clear:false Env.After in
let guard_for_small_type = Smart_stmt.block_stmt b in
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 9799cadb813983e5a73c2fdc5844fa035b8beb34..03c60a57aaa876b23ea79bf3357ee5af75ee8e17 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
+++ b/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
@@ -39,25 +39,6 @@ let if_stmt ~loc ~cond ?(else_blk=Cil.mkBlock []) then_blk =
let break ~loc = stmt (Break loc)
-type annotation_kind =
- | Assertion
- | Precondition
- | Postcondition
- | Invariant
- | Variant
- | RTE
-
-let kind_to_string loc k =
- Cil.mkString
- ~loc
- (match k with
- | Assertion -> "Assertion"
- | Precondition -> "Precondition"
- | Postcondition -> "Postcondition"
- | Invariant -> "Invariant"
- | Variant -> "Variant"
- | RTE -> "RTE")
-
let block stmt b = match b.bstmts with
| [] ->
(match stmt.skind with
@@ -179,33 +160,13 @@ 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 ~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 ~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 ~pred_kind kind kf e
+type annotation_kind =
+ | Assertion
+ | Precondition
+ | Postcondition
+ | Invariant
+ | Variant
+ | RTE
(*
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 4cdeb0fd23d1f0d62cb58b15806a3c321dc45c55..ddf4f39ee602a0ce89d14af0ba2eded06f5d094e 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_stmt.mli
+++ b/src/plugins/e-acsl/src/code_generator/smart_stmt.mli
@@ -107,25 +107,6 @@ type annotation_kind =
| Variant
| RTE
-val runtime_check:
- 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 -> 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:
compile-command: "make -C ../../../../.."
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 2d42a0c8fa0c0b5deafc1eccdb528832c9f0362d..329ea22e307825b3f10d51f450b207f93470f914 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -390,7 +390,7 @@ and context_insensitive_term_to_exp kf env t =
let mk_stmts _v e =
assert (Gmp_types.Z.is_t ty);
let cond =
- Smart_stmt.runtime_check
+ Assert.runtime_check
~pred_kind:Assert
(Env.annotation_kind env)
kf
@@ -475,7 +475,8 @@ and context_insensitive_term_to_exp kf env t =
in
let pname = bop_name ^ "_rhs_fits_in_mp_bitcnt_t" in
let pred = { pred with pred_name = pname :: pred.pred_name } in
- let cond = Smart_stmt.runtime_check
+ let cond =
+ Assert.runtime_check
~pred_kind:Assert
Smart_stmt.RTE
kf
@@ -540,7 +541,8 @@ and context_insensitive_term_to_exp kf env t =
in
let e1_guard_cond =
let pred = Logic_const.prel ~loc (Rge, t1, zero) in
- let cond = Smart_stmt.runtime_check
+ let cond =
+ Assert.runtime_check
~pred_kind:Assert
Smart_stmt.RTE
kf
@@ -1138,7 +1140,7 @@ and translate_predicate ?pred_to_print kf env p =
Env.add_stmt
env
kf
- (Smart_stmt.runtime_check
+ (Assert.runtime_check
~pred_kind:p.tp_kind
(Env.annotation_kind env)
kf
@@ -1167,7 +1169,7 @@ let gmp_to_sizet ~loc ~name ?(check_lower_bound=true) ?pp kf env t =
Typing.type_named_predicate ~must_clear:false lower_guard;
let lower_guard, env = predicate_to_exp kf env lower_guard in
let assertion =
- Smart_stmt.runtime_check
+ Assert.runtime_check
~pred_kind:Assert
Smart_stmt.RTE
kf
@@ -1192,7 +1194,7 @@ let gmp_to_sizet ~loc ~name ?(check_lower_bound=true) ?pp kf env t =
Typing.type_named_predicate ~must_clear:false upper_guard;
let upper_guard, env = predicate_to_exp kf env upper_guard in
let assertion =
- Smart_stmt.runtime_check
+ Assert.runtime_check
~pred_kind:Assert
Smart_stmt.RTE
kf