diff --git a/src/plugins/e-acsl/src/code_generator/contract.ml b/src/plugins/e-acsl/src/code_generator/contract.ml
index c8cb861fb7545b5dfc6b8d79de6151c85ee52808..2941c7092287790b086356c04af09667c4194596 100644
--- a/src/plugins/e-acsl/src/code_generator/contract.ml
+++ b/src/plugins/e-acsl/src/code_generator/contract.ml
@@ -354,25 +354,33 @@ let check_requires kf kinstr env contract =
if !must_translate_ppt_ref
(Property.ip_of_requires kf kinstr b ip_requires) then
let tp_requires = ip_requires.ip_content in
- let requires = tp_requires.tp_statement in
- let loc = requires.pred_loc in
- Cil.CurrentLoc.set loc;
- (* Prepend the name of the behavior *)
- let requires =
- { requires with pred_name = b.b_name :: requires.pred_name }
- in
- (* Create runtime check *)
- let requires_e, env =
- Translate.generalized_untyped_predicate_to_exp kf env requires
- in
- let stmt =
- Smart_stmt.runtime_check
- Smart_stmt.Precondition
- kf
- requires_e
- requires
- in
- env, stmt :: stmts
+ let pred_kind = tp_requires.tp_kind in
+ match pred_kind with
+ | Assert | Check ->
+ let requires = tp_requires.tp_statement in
+ let loc = requires.pred_loc in
+ Cil.CurrentLoc.set loc;
+ (* Prepend the name of the behavior *)
+ let requires =
+ { requires with pred_name = b.b_name :: requires.pred_name }
+ in
+ (* Create runtime check *)
+ let requires_e, env =
+ Translate.generalized_untyped_predicate_to_exp
+ kf
+ env
+ requires
+ in
+ let stmt =
+ Smart_stmt.runtime_check
+ ~pred_kind
+ Smart_stmt.Precondition
+ kf
+ requires_e
+ requires
+ in
+ env, stmt :: stmts
+ | Admit -> env, stmts
else
env, stmts)
(env, [])
@@ -501,6 +509,7 @@ let check_active_behaviors ~ppt_to_translate ~get_or_create_var kf kinstr env co
Smart_stmt.runtime_check_with_msg
~loc
msg
+ ~pred_kind:Assert
(Env.annotation_kind env)
kf
(Cil.mkBinOp ~loc bop active_bhvrs_e (Cil.one ~loc))
@@ -648,30 +657,41 @@ let check_post_conds kf kinstr env contract =
if !must_translate_ppt_ref
(Property.ip_of_ensures kf kinstr b tp) then
let tp_post_cond = ip_post_cond.ip_content in
- let post_cond = tp_post_cond.tp_statement in
- let loc = post_cond.pred_loc in
- Cil.CurrentLoc.set loc;
- match termination with
- | Normal ->
- (* Prepend the name of the behavior *)
- let post_cond =
- { post_cond with pred_name = b.b_name :: post_cond.pred_name }
- in
- (* Create runtime check *)
- let post_cond_e, env =
- Translate.generalized_untyped_predicate_to_exp kf env post_cond
- in
- let stmt =
- Smart_stmt.runtime_check
- Smart_stmt.Postcondition
- kf
- post_cond_e
- post_cond
- in
- env, stmt :: stmts
- | Exits | Breaks | Continues | Returns ->
- Error.process_error (Error.not_yet "abnormal termination case in behavior");
- env, stmts
+ let pred_kind = tp_post_cond.tp_kind in
+ match pred_kind with
+ | Assert | Check -> begin
+ let post_cond = tp_post_cond.tp_statement in
+ let loc = post_cond.pred_loc in
+ Cil.CurrentLoc.set loc;
+ match termination with
+ | Normal ->
+ (* Prepend the name of the behavior *)
+ let post_cond =
+ { post_cond with
+ pred_name = b.b_name :: post_cond.pred_name }
+ in
+ (* Create runtime check *)
+ let post_cond_e, env =
+ Translate.generalized_untyped_predicate_to_exp
+ kf
+ env
+ post_cond
+ in
+ let stmt =
+ Smart_stmt.runtime_check
+ ~pred_kind
+ Smart_stmt.Postcondition
+ kf
+ post_cond_e
+ post_cond
+ in
+ env, stmt :: stmts
+ | Exits | Breaks | Continues | Returns ->
+ Error.process_error
+ (Error.not_yet "abnormal termination case in behavior");
+ env, stmts
+ end
+ | Admit -> env, stmts
else
env, stmts)
(env, [])
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 688905079da3776c370c325c926742cf09f8a91e..fd0f45a325cf236baabe260b3b7fc303161bed62 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 Smart_stmt.RTE kf e p
+ Smart_stmt.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 1948f3a857ba062a100023b00c0b6c0ad2c0a8ea..ab0c7fa3d38c81d2a0e42f34332bdcb9897d0ed0 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -251,7 +251,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 Smart_stmt.RTE kf e p, env
+ Smart_stmt.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/memory_translate.ml b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
index 976c5c91d3ea809a1739bb30fd0b722f0f1b70d3..41fedc2159be7bf64f11fbd1c3ae434ab874fb70 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
@@ -158,7 +158,7 @@ let gmp_to_sizet ~loc kf env size p =
None
sizet
(fun vi _ ->
- [ Smart_stmt.runtime_check Smart_stmt.RTE kf guard p;
+ [ Smart_stmt.runtime_check ~pred_kind:Assert Smart_stmt.RTE kf guard p;
Smart_stmt.rtl_call ~loc
~result:(Cil.var vi)
~prefix:""
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 81056b5d8b5969839d6eca4c3bc6abccede0367e..b5b44048da759670b1884a7e9d2123655d6afd62 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -372,6 +372,7 @@ and context_insensitive_term_to_exp kf env t =
assert (Gmp_types.Z.is_t ty);
let cond =
Smart_stmt.runtime_check
+ ~pred_kind:Assert
(Env.annotation_kind env)
kf
guard
@@ -456,6 +457,7 @@ and context_insensitive_term_to_exp kf env t =
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
+ ~pred_kind:Assert
Smart_stmt.RTE
kf
coerce_guard
@@ -520,6 +522,7 @@ and context_insensitive_term_to_exp kf env t =
let e1_guard_cond =
let pred = Logic_const.prel ~loc (Rge, t1, zero) in
let cond = Smart_stmt.runtime_check
+ ~pred_kind:Assert
Smart_stmt.RTE
kf
e1_guard
@@ -1040,6 +1043,7 @@ and predicate_content_to_exp ?name kf env p =
in
let stmt =
Smart_stmt.runtime_check
+ ~pred_kind:Assert
Smart_stmt.RTE
kf
e
@@ -1152,25 +1156,29 @@ and translate_rte ?filter kf env e =
translate_rte_annots Printer.pp_exp e kf env l
and translate_predicate ?pred_to_print kf env p =
- Options.feedback ~dkey ~level:3 "translating predicate %a"
- Printer.pp_toplevel_predicate p;
- let pred_to_print =
- match pred_to_print with
- | Some pred ->
- Options.feedback ~dkey ~level:3 "(predicate to print %a)"
- Printer.pp_predicate pred;
- pred
- | None -> p.tp_statement
- in
- let e, env = generalized_untyped_predicate_to_exp kf env p.tp_statement in
- Env.add_stmt
- env
- kf
- (Smart_stmt.runtime_check
- (Env.annotation_kind env)
- kf
- e
- pred_to_print)
+ match p.tp_kind with
+ | Assert | Check ->
+ Options.feedback ~dkey ~level:3 "translating predicate %a"
+ Printer.pp_toplevel_predicate p;
+ let pred_to_print =
+ match pred_to_print with
+ | Some pred ->
+ Options.feedback ~dkey ~level:3 "(predicate to print %a)"
+ Printer.pp_predicate pred;
+ pred
+ | None -> p.tp_statement
+ in
+ let e, env = generalized_untyped_predicate_to_exp kf env p.tp_statement in
+ Env.add_stmt
+ env
+ kf
+ (Smart_stmt.runtime_check
+ ~pred_kind:p.tp_kind
+ (Env.annotation_kind env)
+ kf
+ e
+ pred_to_print)
+ | Admit -> env
let predicate_to_exp_without_rte ?name kf env p =
predicate_to_exp ?name kf env p (* forget optional argument ?rte *)