diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
index 595dc566e1e836413c056e3c2c462ff3fedcf11a..cf56b61500be166e282712a7a2e2adda699481bf 100644
--- a/src/plugins/e-acsl/src/code_generator/env.ml
+++ b/src/plugins/e-acsl/src/code_generator/env.ml
@@ -135,6 +135,20 @@ let generate_rte env =
let local_env, _ = top env in
local_env.rte
+let with_rte ~f env rte_value =
+ let old_rte_value = generate_rte env in
+ let env = rte env rte_value in
+ let env = f env in
+ let env = rte env old_rte_value in
+ env
+
+let with_rte_and_result ~f env rte_value =
+ let old_rte_value = generate_rte env in
+ let env = rte env rte_value in
+ let other, env = f env in
+ let env = rte env old_rte_value in
+ other, env
+
(* ************************************************************************** *)
(* eta-expansion required for typing generalisation *)
@@ -201,9 +215,9 @@ let do_new_var ~loc ?(scope=Varname.Block) ?(name="") env kf t ty mk_stmts =
env_stack = local_env :: tl_env }
| Varname.Block ->
let local_env =
- { block_info = new_block;
- mp_tbl = extend_tbl local_env.mp_tbl;
- rte = false (* must be already checked by mk_stmts *) }
+ { local_env with
+ block_info = new_block;
+ mp_tbl = extend_tbl local_env.mp_tbl }
in
{ env with
cpt = n;
@@ -213,8 +227,7 @@ let do_new_var ~loc ?(scope=Varname.Block) ?(name="") env kf t ty mk_stmts =
let new_global_vars = (v, lscope) :: env.new_global_vars in
let local_env =
{ local_env with
- block_info = new_block;
- rte = false (* must be already checked by mk_stmts *) }
+ block_info = new_block }
in
{ env with
new_global_vars = new_global_vars;
diff --git a/src/plugins/e-acsl/src/code_generator/env.mli b/src/plugins/e-acsl/src/code_generator/env.mli
index 3a5aebf2f5d4f1a0ea67af77099032535365f8e7..cb6633546cfaaa5527c2be9d5d7ce56e470c59f9 100644
--- a/src/plugins/e-acsl/src/code_generator/env.mli
+++ b/src/plugins/e-acsl/src/code_generator/env.mli
@@ -165,7 +165,26 @@ val pop_loop: t -> predicate list * t
(* ************************************************************************** *)
val rte: t -> bool -> t
+(** [rte env x] sets RTE generation to x for the given environment *)
+
val generate_rte: t -> bool
+(** Returns the current value of RTE generation for the given environment *)
+
+val with_rte: f:(t -> t) -> t -> bool -> t
+(** [with_rte ~f env x] executes the given closure with RTE generation set to x,
+ and reset RTE generation to its original value afterwards.
+ This function does not handle exceptions at all. The user must handle them
+ either directly in the [f] closure or around the call to the function. *)
+
+val with_rte_and_result: f:(t -> 'a * t) -> t -> bool -> 'a * t
+(** [with_rte_and_result ~f env x] executes the given closure with RTE
+ generation set to x, and reset RTE generation to its original value
+ afterwards. [f] is a closure that takes an environment an returns a pair
+ where the first member is an arbitrary value and the second member is the
+ environment. The function will return the first member of the returned pair
+ of the closure along with the updated environment.
+ This function does not handle exceptions at all. The user must handle them
+ either directly in the [f] closure or around the call to the function. *)
(* ************************************************************************** *)
(** {2 Context for error handling} *)
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 be6fbc2bc7a5d9b7025d7896c52e0abe2b89d2d6..38166949656b8f5e50598e58004cac88cca831ed 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
@@ -115,7 +115,10 @@ let rec eliminate_ranges_from_index_of_toffset ~loc toffset quantifiers =
let call ~loc kf name ctx env t =
assert (name = "base_addr" || name = "block_length"
|| name = "offset" || name ="freeable");
- let e, env = !term_to_exp_ref kf (Env.rte env true) t in
+ let e, env =
+ Env.with_rte_and_result env true
+ ~f:(fun env -> !term_to_exp_ref kf env t)
+ in
Env.rtl_call_to_new_var
~loc
~name
@@ -194,7 +197,10 @@ let range_to_ptr_and_size ~loc kf env ptr r p =
(Ctype typ_charptr)
in
Typing.type_term ~use_gmp_opt:false ~ctx:Typing.nan ptr;
- let ptr, env = !term_to_exp_ref kf (Env.rte env true) ptr in
+ let ptr, env =
+ Env.with_rte_and_result env true
+ ~f:(fun env -> !term_to_exp_ref kf env ptr)
+ in
(* size *)
let size_term =
(* Since [s] and [n1] have been typed through [ptr],
@@ -252,7 +258,10 @@ let range_to_ptr_and_size ~loc kf env ptr r p =
expression in bytes and [env] is the current environment.
[p] is the predicate under test. *)
let term_to_ptr_and_size ~loc kf env t =
- let e, env = !term_to_exp_ref kf (Env.rte env true) t in
+ let e, env =
+ Env.with_rte_and_result env true
+ ~f:(fun env -> !term_to_exp_ref kf env t)
+ in
let ty = Misc.cty t.term_type in
let sizeof = Smart_exp.ptr_sizeof ~loc ty in
e, sizeof, env
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 9ad2815d009281c1143843a02d583511f334e229..2570aa9bbfb2c6436d373bf25d5c4c3ddbaab96f 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -537,21 +537,28 @@ and context_insensitive_term_to_exp kf env t =
end
| TBinOp(LOr, t1, t2) ->
(* t1 || t2 <==> if t1 then true else t2 *)
- let e1, env1 = term_to_exp kf (Env.rte env true) t1 in
- let env' = Env.push env1 in
- let res2 = term_to_exp kf (Env.push env') t2 in
let e, env =
- conditional_to_exp ~name:"or" loc kf (Some t) e1 (Cil.one loc, env') res2
+ Env.with_rte_and_result env true
+ ~f:(fun env ->
+ let e1, env1 = term_to_exp kf env t1 in
+ let env' = Env.push env1 in
+ let res2 = term_to_exp kf (Env.push env') t2 in
+ conditional_to_exp
+ ~name:"or" loc kf (Some t) e1 (Cil.one loc, env') res2
+ )
in
e, env, C_number, ""
| TBinOp(LAnd, t1, t2) ->
(* t1 && t2 <==> if t1 then t2 else false *)
- let e1, env1 = term_to_exp kf (Env.rte env true) t1 in
- let _, env2 as res2 = term_to_exp kf (Env.push env1) t2 in
- let env3 = Env.push env2 in
let e, env =
- conditional_to_exp
- ~name:"and" loc kf (Some t) e1 res2 (Cil.zero loc, env3)
+ Env.with_rte_and_result env true
+ ~f:(fun env ->
+ let e1, env1 = term_to_exp kf env t1 in
+ let _, env2 as res2 = term_to_exp kf (Env.push env1) t2 in
+ let env3 = Env.push env2 in
+ conditional_to_exp
+ ~name:"and" loc kf (Some t) e1 res2 (Cil.zero loc, env3)
+ )
in
e, env, C_number, ""
| TBinOp((BOr | BXor | BAnd) as bop, t1, t2) ->
@@ -671,10 +678,15 @@ and context_insensitive_term_to_exp kf env t =
| Tlambda _ -> Env.not_yet env "functional"
| TDataCons _ -> Env.not_yet env "constructor"
| Tif(t1, t2, t3) ->
- let e1, env1 = term_to_exp kf (Env.rte env true) t1 in
- let (_, env2 as res2) = term_to_exp kf (Env.push env1) t2 in
- let res3 = term_to_exp kf (Env.push env2) t3 in
- let e, env = conditional_to_exp loc kf (Some t) e1 res2 res3 in
+ let e, env =
+ Env.with_rte_and_result env true
+ ~f:(fun env ->
+ let e1, env1 = term_to_exp kf env t1 in
+ let (_, env2 as res2) = term_to_exp kf (Env.push env1) t2 in
+ let res3 = term_to_exp kf (Env.push env2) t3 in
+ conditional_to_exp loc kf (Some t) e1 res2 res3
+ )
+ in
e, env, C_number, ""
| Tat(t, BuiltinLabel Here) ->
let e, env = term_to_exp kf env t in
@@ -731,21 +743,23 @@ and term_to_exp kf env t =
let generate_rte = Env.generate_rte env in
Options.feedback ~dkey ~level:4 "translating term %a (rte? %b)"
Printer.pp_term t generate_rte;
- let env = Env.rte env false in
- let t = match t.term_node with TLogic_coerce(_, t) -> t | _ -> t in
- let e, env, sty, name = context_insensitive_term_to_exp kf env t in
- let env = if generate_rte then translate_rte kf env e else env in
- let cast = Typing.get_cast t in
- let name = if name = "" then None else Some name in
- add_cast
- ~loc:t.term_loc
- ?name
- env
- kf
- cast
- sty
- (Some t)
- e
+ Env.with_rte_and_result env false
+ ~f:(fun env ->
+ let t = match t.term_node with TLogic_coerce(_, t) -> t | _ -> t in
+ let e, env, sty, name = context_insensitive_term_to_exp kf env t in
+ let env = if generate_rte then translate_rte kf env e else env in
+ let cast = Typing.get_cast t in
+ let name = if name = "" then None else Some name in
+ add_cast
+ ~loc:t.term_loc
+ ?name
+ env
+ kf
+ cast
+ sty
+ (Some t)
+ e
+ )
(* generate the C code equivalent to [t1 bop t2]. *)
and comparison_to_exp
@@ -890,19 +904,25 @@ and predicate_content_to_exp ?name kf env p =
comparison_to_exp ~loc kf env ity (relation_to_binop rel) t1 t2 None
| Pand(p1, p2) ->
(* p1 && p2 <==> if p1 then p2 else false *)
- let e1, env1 = predicate_to_exp kf (Env.rte env true) p1 in
- let _, env2 as res2 =
- predicate_to_exp kf (Env.push env1) p2 in
- let env3 = Env.push env2 in
- let name = match name with None -> "and" | Some n -> n in
- conditional_to_exp ~name loc kf None e1 res2 (Cil.zero loc, env3)
+ Env.with_rte_and_result env true
+ ~f:(fun env ->
+ let e1, env1 = predicate_to_exp kf env p1 in
+ let _, env2 as res2 =
+ predicate_to_exp kf (Env.push env1) p2 in
+ let env3 = Env.push env2 in
+ let name = match name with None -> "and" | Some n -> n in
+ conditional_to_exp ~name loc kf None e1 res2 (Cil.zero loc, env3)
+ )
| Por(p1, p2) ->
(* p1 || p2 <==> if p1 then true else p2 *)
- let e1, env1 = predicate_to_exp kf (Env.rte env true) p1 in
- let env' = Env.push env1 in
- let res2 = predicate_to_exp kf (Env.push env') p2 in
- let name = match name with None -> "or" | Some n -> n in
- conditional_to_exp ~name loc kf None e1 (Cil.one loc, env') res2
+ Env.with_rte_and_result env true
+ ~f:(fun env ->
+ let e1, env1 = predicate_to_exp kf env p1 in
+ let env' = Env.push env1 in
+ let res2 = predicate_to_exp kf (Env.push env') p2 in
+ let name = match name with None -> "or" | Some n -> n in
+ conditional_to_exp ~name loc kf None e1 (Cil.one loc, env') res2
+ )
| Pxor _ -> Env.not_yet env "xor"
| Pimplies(p1, p2) ->
(* (p1 ==> p2) <==> !p1 || p2 *)
@@ -924,11 +944,14 @@ and predicate_content_to_exp ?name kf env p =
let e, env = predicate_to_exp kf env p in
Cil.new_exp ~loc (UnOp(LNot, e, Cil.intType)), env
| Pif(t, p2, p3) ->
- let e1, env1 = term_to_exp kf (Env.rte env true) t in
- let (_, env2 as res2) =
- predicate_to_exp kf (Env.push env1) p2 in
- let res3 = predicate_to_exp kf (Env.push env2) p3 in
- conditional_to_exp loc kf None e1 res2 res3
+ Env.with_rte_and_result env true
+ ~f:(fun env ->
+ let e1, env1 = term_to_exp kf env t in
+ let (_, env2 as res2) =
+ predicate_to_exp kf (Env.push env1) p2 in
+ let res3 = predicate_to_exp kf (Env.push env2) p3 in
+ conditional_to_exp loc kf None e1 res2 res3
+ )
| Plet(li, p) ->
let lvs = Lscope.Lvs_let(li.l_var_info, Misc.term_of_li li) in
let env = Env.Logic_scope.extend env lvs in
@@ -1035,19 +1058,21 @@ and predicate_content_to_exp ?name kf env p =
and predicate_to_exp ?name kf ?rte env p =
let rte = match rte with None -> Env.generate_rte env | Some b -> b in
- let env = Env.rte env false in
- let e, env = predicate_content_to_exp ?name kf env p in
- let env = if rte then translate_rte kf env e else env in
- let cast = Typing.get_cast_of_predicate p in
- add_cast
- ~loc:p.pred_loc
- ?name
- env
- kf
- cast
- C_number
- None
- e
+ Env.with_rte_and_result env false
+ ~f:(fun env ->
+ let e, env = predicate_content_to_exp ?name kf env p in
+ let env = if rte then translate_rte kf env e else env in
+ let cast = Typing.get_cast_of_predicate p in
+ add_cast
+ ~loc:p.pred_loc
+ ?name
+ env
+ kf
+ cast
+ C_number
+ None
+ e
+ )
and generalized_untyped_predicate_to_exp ?name kf ?rte ?must_clear_typing env p =
(* If [rte] is true, it means we're translating the root predicate of an
@@ -1083,7 +1108,10 @@ and translate_rte_annots:
let p = p.tp_statement in
let lscope_reset_old = Env.Logic_scope.get_reset env in
let env = Env.Logic_scope.set_reset env false in
- let env = translate_predicate kf (Env.rte env false) p in
+ let env =
+ Env.with_rte env false
+ ~f:(fun env -> translate_predicate kf env p)
+ in
let env = Env.Logic_scope.set_reset env lscope_reset_old in
env)
env
diff --git a/src/plugins/e-acsl/src/code_generator/translate_annots.ml b/src/plugins/e-acsl/src/code_generator/translate_annots.ml
index a65ac3567b95ad3ee2fc4b871ae4bf8dd681b526..bc7ffca4cf1ce0942b2a0e9070d91a85b6269ea4 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_annots.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_annots.ml
@@ -70,10 +70,12 @@ let pre_funspec kf kinstr env funspec =
let env = convert_unsupported_clauses env in
let loc = Kernel_function.get_location kf in
let contract = Contract.create ~loc funspec in
- Contract.translate_preconditions kf kinstr env contract
+ Env.with_rte env true
+ ~f:(fun env -> Contract.translate_preconditions kf kinstr env contract)
let post_funspec kf kinstr env =
- Contract.translate_postconditions kf kinstr env
+ Env.with_rte env true
+ ~f:(fun env -> Contract.translate_postconditions kf kinstr env)
let pre_code_annotation kf stmt env annot =
let convert env = match annot.annot_content with
@@ -82,7 +84,8 @@ let pre_code_annotation kf stmt env annot =
let env = Env.set_annotation_kind env Smart_stmt.Assertion in
if l <> [] then
Env.not_yet env "@[assertion applied only on some behaviors@]";
- Translate.translate_predicate kf env p.tp_statement
+ Env.with_rte env true
+ ~f:(fun env -> Translate.translate_predicate kf env p.tp_statement)
else
env
| AStmtSpec(l, spec) ->
@@ -90,13 +93,18 @@ let pre_code_annotation kf stmt env annot =
Env.not_yet env "@[statement contract applied only on some behaviors@]";
let loc = Stmt.loc stmt in
let contract = Contract.create ~loc spec in
- Contract.translate_preconditions kf (Kstmt stmt) env contract
+ Env.with_rte env true
+ ~f:(fun env ->
+ Contract.translate_preconditions kf (Kstmt stmt) env contract)
| AInvariant(l, loop_invariant, p) ->
if must_translate (Property.ip_of_code_annot_single kf stmt annot) then
let env = Env.set_annotation_kind env Smart_stmt.Invariant in
if l <> [] then
Env.not_yet env "@[invariant applied only on some behaviors@]";
- let env = Translate.translate_predicate kf env p.tp_statement in
+ let env =
+ Env.with_rte env true
+ ~f:(fun env -> Translate.translate_predicate kf env p.tp_statement)
+ in
if loop_invariant then
Env.add_loop_invariant env p.tp_statement
else env
@@ -127,7 +135,9 @@ let pre_code_annotation kf stmt env annot =
let post_code_annotation kf stmt env annot =
let convert env = match annot.annot_content with
- | AStmtSpec(_, _) -> Contract.translate_postconditions kf (Kstmt stmt) env
+ | AStmtSpec(_, _) ->
+ Env.with_rte env true
+ ~f:(fun env -> Contract.translate_postconditions kf (Kstmt stmt) env)
| AAssert _
| AInvariant _
| AVariant _
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/at_on-purely-logic-variables.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/at_on-purely-logic-variables.res.oracle
index ceb8eed7a93e5cd46801202607b737a163b9b95f..8df5dd5c3147da4920741cd471afd6512ac092fe 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/at_on-purely-logic-variables.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/at_on-purely-logic-variables.res.oracle
@@ -52,6 +52,10 @@
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:43: Warning:
assertion got status unknown.
+[eva:alarm] tests/arith/at_on-purely-logic-variables.c:7: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/arith/at_on-purely-logic-variables.c:7: Warning:
+ function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:7: Warning:
accessing uninitialized left-value.
assert \initialized(__gen_e_acsl_at + (int)((int)(__gen_e_acsl_n - 1) - 1));
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c
index 205c4799a854078e9477b9ef4546492c0726ef6b..55c43cab27b2077a3433af728a43b978e40bc6cd 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c
@@ -610,19 +610,50 @@ void __gen_e_acsl_f(int *t)
{
int __gen_e_acsl_m_3;
__gen_e_acsl_m_3 = 4;
- *(__gen_e_acsl_at_4 + 0) = *(t + (__gen_e_acsl_m_3 - 4));
+ {
+ int __gen_e_acsl_valid_read_7;
+ __gen_e_acsl_valid_read_7 = __e_acsl_valid_read((void *)(t + (int)(
+ __gen_e_acsl_m_3 - 4L)),
+ sizeof(int),(void *)t,
+ (void *)(& t));
+ __e_acsl_assert(__gen_e_acsl_valid_read_7,"RTE","f",
+ "mem_access: \\valid_read(t + (int)(__gen_e_acsl_m_3 - 4))",
+ "tests/arith/at_on-purely-logic-variables.c",8);
+ *(__gen_e_acsl_at_4 + 0) = *(t + (__gen_e_acsl_m_3 - 4));
+ }
}
{
int __gen_e_acsl_m_2;
__gen_e_acsl_m_2 = 4;
- *(__gen_e_acsl_at_3 + 0) = *(t + __gen_e_acsl_m_2) == -4;
+ {
+ int __gen_e_acsl_valid_read_5;
+ __gen_e_acsl_valid_read_5 = __e_acsl_valid_read((void *)(t + __gen_e_acsl_m_2),
+ sizeof(int),(void *)t,
+ (void *)(& t));
+ __e_acsl_assert(__gen_e_acsl_valid_read_5,"RTE","f",
+ "mem_access: \\valid_read(t + __gen_e_acsl_m_2)",
+ "tests/arith/at_on-purely-logic-variables.c",8);
+ *(__gen_e_acsl_at_3 + 0) = *(t + __gen_e_acsl_m_2) == -4;
+ }
}
{
int __gen_e_acsl_n_3;
__gen_e_acsl_n_3 = 1 + 1;
while (1) {
if (__gen_e_acsl_n_3 <= 3) ; else break;
- *(__gen_e_acsl_at_2 + ((__gen_e_acsl_n_3 - 1) - 1)) = *(t + (__gen_e_acsl_n_3 - 1)) > 5;
+ {
+ int __gen_e_acsl_valid_read_3;
+ __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(t + (int)(
+ __gen_e_acsl_n_3 - 1L)),
+ sizeof(int),
+ (void *)t,
+ (void *)(& t));
+ __e_acsl_assert(__gen_e_acsl_valid_read_3,"RTE","f",
+ "mem_access: \\valid_read(t + (int)(__gen_e_acsl_n_3 - 1))",
+ "tests/arith/at_on-purely-logic-variables.c",7);
+ *(__gen_e_acsl_at_2 + ((__gen_e_acsl_n_3 - 1) - 1)) = *(t + (
+ __gen_e_acsl_n_3 - 1)) > 5;
+ }
__gen_e_acsl_n_3 ++;
}
}
@@ -631,7 +662,16 @@ void __gen_e_acsl_f(int *t)
__gen_e_acsl_n_2 = 1 + 1;
while (1) {
if (__gen_e_acsl_n_2 <= 3) ; else break;
- *(__gen_e_acsl_at + ((__gen_e_acsl_n_2 - 1) - 1)) = *(t + __gen_e_acsl_n_2) == 12;
+ {
+ int __gen_e_acsl_valid_read;
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(t + __gen_e_acsl_n_2),
+ sizeof(int),(void *)t,
+ (void *)(& t));
+ __e_acsl_assert(__gen_e_acsl_valid_read,"RTE","f",
+ "mem_access: \\valid_read(t + __gen_e_acsl_n_2)",
+ "tests/arith/at_on-purely-logic-variables.c",7);
+ *(__gen_e_acsl_at + ((__gen_e_acsl_n_2 - 1) - 1)) = *(t + __gen_e_acsl_n_2) == 12;
+ }
__gen_e_acsl_n_2 ++;
}
}
@@ -640,22 +680,22 @@ void __gen_e_acsl_f(int *t)
int __gen_e_acsl_forall;
int __gen_e_acsl_n;
int __gen_e_acsl_m;
- int __gen_e_acsl_valid_read_3;
+ int __gen_e_acsl_valid_read_6;
int __gen_e_acsl_and_2;
__gen_e_acsl_forall = 1;
__gen_e_acsl_n = 1 + 1;
while (1) {
if (__gen_e_acsl_n <= 3) ; else break;
{
- int __gen_e_acsl_valid_read;
+ int __gen_e_acsl_valid_read_2;
int __gen_e_acsl_and;
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(__gen_e_acsl_at + (int)(
- (long)((int)(
- __gen_e_acsl_n - 1L)) - 1L)),
- sizeof(int),
- (void *)__gen_e_acsl_at,
- (void *)(& __gen_e_acsl_at));
- __e_acsl_assert(__gen_e_acsl_valid_read,"RTE","f",
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(__gen_e_acsl_at + (int)(
+ (long)((int)(
+ __gen_e_acsl_n - 1L)) - 1L)),
+ sizeof(int),
+ (void *)__gen_e_acsl_at,
+ (void *)(& __gen_e_acsl_at));
+ __e_acsl_assert(__gen_e_acsl_valid_read_2,"RTE","f",
"mem_access:\n \\valid_read(__gen_e_acsl_at + (int)((int)(__gen_e_acsl_n - 1) - 1))",
"tests/arith/at_on-purely-logic-variables.c",7);
/*@ assert
@@ -664,14 +704,14 @@ void __gen_e_acsl_f(int *t)
(int)((int)(__gen_e_acsl_n - 1) - 1));
*/
if (*(__gen_e_acsl_at + ((__gen_e_acsl_n - 1) - 1))) {
- int __gen_e_acsl_valid_read_2;
- __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_2 + (int)(
+ int __gen_e_acsl_valid_read_4;
+ __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_2 + (int)(
(long)((int)(
__gen_e_acsl_n - 1L)) - 1L)),
sizeof(int),
(void *)__gen_e_acsl_at_2,
(void *)(& __gen_e_acsl_at_2));
- __e_acsl_assert(__gen_e_acsl_valid_read_2,"RTE","f",
+ __e_acsl_assert(__gen_e_acsl_valid_read_4,"RTE","f",
"mem_access:\n \\valid_read(__gen_e_acsl_at_2 + (int)((int)(__gen_e_acsl_n - 1) - 1))",
"tests/arith/at_on-purely-logic-variables.c",7);
/*@ assert
@@ -695,20 +735,20 @@ void __gen_e_acsl_f(int *t)
"\\forall integer n;\n 1 < n <= 3 ==> \\old(*(t + n) == 12) && \\old(*(t + (n - 1)) > 5)",
"tests/arith/at_on-purely-logic-variables.c",6);
__gen_e_acsl_m = 4;
- __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_3 + 0),
+ __gen_e_acsl_valid_read_6 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_3 + 0),
sizeof(int),
(void *)__gen_e_acsl_at_3,
(void *)(& __gen_e_acsl_at_3));
- __e_acsl_assert(__gen_e_acsl_valid_read_3,"RTE","f",
+ __e_acsl_assert(__gen_e_acsl_valid_read_6,"RTE","f",
"mem_access: \\valid_read(__gen_e_acsl_at_3 + 0)",
"tests/arith/at_on-purely-logic-variables.c",8);
if (*(__gen_e_acsl_at_3 + 0)) {
- int __gen_e_acsl_valid_read_4;
- __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_4 + 0),
+ int __gen_e_acsl_valid_read_8;
+ __gen_e_acsl_valid_read_8 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_4 + 0),
sizeof(int),
(void *)__gen_e_acsl_at_4,
(void *)(& __gen_e_acsl_at_4));
- __e_acsl_assert(__gen_e_acsl_valid_read_4,"RTE","f",
+ __e_acsl_assert(__gen_e_acsl_valid_read_8,"RTE","f",
"mem_access: \\valid_read(__gen_e_acsl_at_4 + 0)",
"tests/arith/at_on-purely-logic-variables.c",8);
__gen_e_acsl_and_2 = *(__gen_e_acsl_at_4 + 0) == 9;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_rte.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_rte.c
new file mode 100644
index 0000000000000000000000000000000000000000..f12c75292b7cb7ccfb227dfe8b6f74734708cfa4
--- /dev/null
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_rte.c
@@ -0,0 +1,168 @@
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdio.h"
+extern int __e_acsl_sound_verdict;
+
+/*@ requires 1 % a ≡ 1;
+ ensures 1 % \old(b) ≡ 1;
+
+ behavior bhvr:
+ assumes 1 % c ≡ 1;
+ requires 1 % d ≡ 1;
+ requires 1 % f ≡ 1 ∨ 1 % g ≡ 1;
+ requires 1 % h ≡ 1 ∧ 1 % i ≡ 1;
+ requires \let var = 1; var % j ≡ 1;
+ requires ∀ ℤ var; 0 ≤ var < k ⇒ var % k ≡ var;
+ requires ∃ ℤ var; 0 ≤ var < l ∧ var % l ≡ var;
+ ensures 1 % \old(e) ≡ 1;
+ */
+void __gen_e_acsl_test(int a, int b, int c, int d, int e, int f, int g,
+ int h, int i, int j, int k, int l);
+
+void test(int a, int b, int c, int d, int e, int f, int g, int h, int i,
+ int j, int k, int l)
+{
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ __gen_e_acsl_test(2,3,4,5,6,7,8,9,10,11,12,13);
+ __retres = 0;
+ return __retres;
+}
+
+/*@ requires 1 % a ≡ 1;
+ ensures 1 % \old(b) ≡ 1;
+
+ behavior bhvr:
+ assumes 1 % c ≡ 1;
+ requires 1 % d ≡ 1;
+ requires 1 % f ≡ 1 ∨ 1 % g ≡ 1;
+ requires 1 % h ≡ 1 ∧ 1 % i ≡ 1;
+ requires \let var = 1; var % j ≡ 1;
+ requires ∀ ℤ var; 0 ≤ var < k ⇒ var % k ≡ var;
+ requires ∃ ℤ var; 0 ≤ var < l ∧ var % l ≡ var;
+ ensures 1 % \old(e) ≡ 1;
+ */
+void __gen_e_acsl_test(int a, int b, int c, int d, int e, int f, int g,
+ int h, int i, int j, int k, int l)
+{
+ int __gen_e_acsl_at_2;
+ int __gen_e_acsl_at;
+ __e_acsl_contract_t *__gen_e_acsl_contract;
+ {
+ int __gen_e_acsl_assumes_value;
+ __gen_e_acsl_contract = __e_acsl_contract_init((size_t)1);
+ __e_acsl_assert(c != 0,"RTE","test","division_by_zero: c != 0",
+ "tests/constructs/rte.i",11);
+ __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0,
+ 1 % c == 1);
+ __e_acsl_assert(a != 0,"RTE","test","division_by_zero: a != 0",
+ "tests/constructs/rte.i",7);
+ __e_acsl_assert(1 % a == 1,"Precondition","test","1 % a == 1",
+ "tests/constructs/rte.i",7);
+ __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes
+ ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)0);
+ if (__gen_e_acsl_assumes_value) {
+ int __gen_e_acsl_or;
+ int __gen_e_acsl_and;
+ int __gen_e_acsl_var;
+ int __gen_e_acsl_forall;
+ int __gen_e_acsl_var_2;
+ int __gen_e_acsl_exists;
+ int __gen_e_acsl_var_3;
+ __e_acsl_assert(d != 0,"RTE","test","division_by_zero: d != 0",
+ "tests/constructs/rte.i",12);
+ __e_acsl_assert(f != 0,"RTE","test","division_by_zero: f != 0",
+ "tests/constructs/rte.i",13);
+ if (1 % f == 1) __gen_e_acsl_or = 1;
+ else {
+ __e_acsl_assert(g != 0,"RTE","test","division_by_zero: g != 0",
+ "tests/constructs/rte.i",13);
+ __gen_e_acsl_or = 1 % g == 1;
+ }
+ __e_acsl_assert(h != 0,"RTE","test","division_by_zero: h != 0",
+ "tests/constructs/rte.i",14);
+ if (1 % h == 1) {
+ __e_acsl_assert(i != 0,"RTE","test","division_by_zero: i != 0",
+ "tests/constructs/rte.i",14);
+ __gen_e_acsl_and = 1 % i == 1;
+ }
+ else __gen_e_acsl_and = 0;
+ __gen_e_acsl_var = 1;
+ __e_acsl_assert(j != 0,"RTE","test","division_by_zero: j != 0",
+ "tests/constructs/rte.i",15);
+ __gen_e_acsl_forall = 1;
+ __gen_e_acsl_var_2 = 0;
+ while (1) {
+ if (__gen_e_acsl_var_2 < k) ; else break;
+ __e_acsl_assert(k != 0,"RTE","test","division_by_zero: k != 0",
+ "tests/constructs/rte.i",16);
+ if (__gen_e_acsl_var_2 % k == __gen_e_acsl_var_2) ;
+ else {
+ __gen_e_acsl_forall = 0;
+ goto e_acsl_end_loop1;
+ }
+ __gen_e_acsl_var_2 ++;
+ }
+ e_acsl_end_loop1: ;
+ __gen_e_acsl_exists = 0;
+ __gen_e_acsl_var_3 = 0;
+ while (1) {
+ if (__gen_e_acsl_var_3 < l) ; else break;
+ __e_acsl_assert(l != 0,"RTE","test","division_by_zero: l != 0",
+ "tests/constructs/rte.i",17);
+ if (! (__gen_e_acsl_var_3 % l == __gen_e_acsl_var_3)) ;
+ else {
+ __gen_e_acsl_exists = 1;
+ goto e_acsl_end_loop2;
+ }
+ __gen_e_acsl_var_3 ++;
+ }
+ e_acsl_end_loop2: ;
+ __e_acsl_assert(__gen_e_acsl_exists,"Precondition","test",
+ "bhvr: \\exists integer var; 0 <= var < l && var % l == var",
+ "tests/constructs/rte.i",17);
+ __e_acsl_assert(__gen_e_acsl_forall,"Precondition","test",
+ "bhvr: \\forall integer var; 0 <= var < k ==> var % k == var",
+ "tests/constructs/rte.i",16);
+ __e_acsl_assert(__gen_e_acsl_var % j == 1,"Precondition","test",
+ "bhvr: \\let var = 1; var % j == 1",
+ "tests/constructs/rte.i",15);
+ __e_acsl_assert(__gen_e_acsl_and,"Precondition","test",
+ "bhvr: 1 % h == 1 && 1 % i == 1",
+ "tests/constructs/rte.i",14);
+ __e_acsl_assert(__gen_e_acsl_or,"Precondition","test",
+ "bhvr: 1 % f == 1 || 1 % g == 1",
+ "tests/constructs/rte.i",13);
+ __e_acsl_assert(1 % d == 1,"Precondition","test","bhvr: 1 % d == 1",
+ "tests/constructs/rte.i",12);
+ }
+ }
+ __gen_e_acsl_at_2 = e;
+ __gen_e_acsl_at = b;
+ test(a,b,c,d,e,f,g,h,i,j,k,l);
+ {
+ int __gen_e_acsl_assumes_value_2;
+ __e_acsl_assert(__gen_e_acsl_at != 0,"RTE","test",
+ "division_by_zero: __gen_e_acsl_at != 0",
+ "tests/constructs/rte.i",8);
+ __e_acsl_assert(1 % __gen_e_acsl_at == 1,"Postcondition","test",
+ "1 % \\old(b) == 1","tests/constructs/rte.i",8);
+ __gen_e_acsl_assumes_value_2 = __e_acsl_contract_get_behavior_assumes
+ ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)0);
+ if (__gen_e_acsl_assumes_value_2) {
+ __e_acsl_assert(__gen_e_acsl_at_2 != 0,"RTE","test",
+ "division_by_zero: __gen_e_acsl_at_2 != 0",
+ "tests/constructs/rte.i",18);
+ __e_acsl_assert(1 % __gen_e_acsl_at_2 == 1,"Postcondition","test",
+ "bhvr: 1 % \\old(e) == 1","tests/constructs/rte.i",18);
+ }
+ __e_acsl_contract_clean(__gen_e_acsl_contract);
+ return;
+ }
+}
+
+
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/rte.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_ci/rte.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..59a91431c62c3df5798cb861bd233db93ff56dd4
--- /dev/null
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/rte.res.oracle
@@ -0,0 +1,13 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/constructs/rte.i:24: Warning:
+ function __gen_e_acsl_test, behavior bhvr: precondition \let var = 1;
+ var % j ≡ 1 got status unknown.
+[eva:alarm] tests/constructs/rte.i:24: Warning:
+ function __gen_e_acsl_test, behavior bhvr: precondition ∀ ℤ var;
+ 0 ≤ var < k ⇒
+ var % k ≡ var got status unknown.
+[eva:alarm] tests/constructs/rte.i:24: Warning:
+ function __gen_e_acsl_test, behavior bhvr: precondition ∃ ℤ var;
+ 0 ≤ var < l ∧
+ var % l ≡ var got status unknown.
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/rte.e-acsl.err.log b/src/plugins/e-acsl/tests/constructs/oracle_dev/rte.e-acsl.err.log
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/constructs/rte.i b/src/plugins/e-acsl/tests/constructs/rte.i
new file mode 100644
index 0000000000000000000000000000000000000000..f80f978c8f7e5b359989b0639da72935e11e9c07
--- /dev/null
+++ b/src/plugins/e-acsl/tests/constructs/rte.i
@@ -0,0 +1,26 @@
+/* run.config_ci, run.config_dev
+ * COMMENT: Check that the RTE checks are generated for every part of a
+ * behavior, and are generated at the right place.
+ */
+
+/*@
+ requires 1 % a == 1;
+ ensures 1 % b == 1;
+
+ behavior bhvr:
+ assumes 1 % c == 1;
+ requires 1 % d == 1;
+ requires (1 % f == 1) || (1 % g == 1);
+ requires (1 % h == 1) && (1 % i == 1);
+ requires \let var = 1; var % j == 1;
+ requires \forall integer var; 0 <= var < k ==> var % k == var;
+ requires \exists integer var; 0 <= var < l && var % l == var;
+ ensures 1 % e == 1;
+*/
+void test(int a, int b, int c, int d, int e, int f, int g, int h, int i, int j, int k, int l) {
+}
+
+int main(void) {
+ test(2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13);
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-functions.c b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-functions.c
index f317d0df3bcefc001519a56a8c2a001604f0a30e..eb68292992dbc87694f7f832d25339504f5db263 100644
--- a/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-functions.c
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-functions.c
@@ -77,18 +77,24 @@ int __gen_e_acsl_f(int *p)
int __retres;
{
int __gen_e_acsl_initialized;
+ int __gen_e_acsl_valid_read;
__e_acsl_store_block((void *)(& p),(size_t)8);
__gen_e_acsl_initialized = __e_acsl_initialized((void *)p,sizeof(int));
__e_acsl_assert(__gen_e_acsl_initialized,"Precondition","f",
"\\initialized(p)","tests/special/e-acsl-functions.c",7);
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)p,sizeof(int),
+ (void *)p,(void *)(& p));
+ __e_acsl_assert(__gen_e_acsl_valid_read,"RTE","f",
+ "mem_access: \\valid_read(p)",
+ "tests/special/e-acsl-functions.c",8);
__e_acsl_assert(*p == 0,"Precondition","f","*p == 0",
"tests/special/e-acsl-functions.c",8);
}
{
- int __gen_e_acsl_valid_read;
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)p,sizeof(int),
- (void *)p,(void *)(& p));
- __e_acsl_assert(__gen_e_acsl_valid_read,"RTE","f",
+ int __gen_e_acsl_valid_read_2;
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)p,sizeof(int),
+ (void *)p,(void *)(& p));
+ __e_acsl_assert(__gen_e_acsl_valid_read_2,"RTE","f",
"mem_access: \\valid_read(p)",
"tests/special/e-acsl-functions.c",9);
__gen_e_acsl_at = *p;
diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-valid.c b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-valid.c
index 890e84bc928baf7442348bff76b96f4437330ebc..e611ff7fd1b7dfe6a16264968bca289f03bafaeb 100644
--- a/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-valid.c
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-valid.c
@@ -106,19 +106,37 @@ void __gen_e_acsl_f(int *x, int *y)
int *__gen_e_acsl_at;
__e_acsl_contract_t *__gen_e_acsl_contract;
{
+ int __gen_e_acsl_valid_read;
+ int __gen_e_acsl_valid_read_2;
int __gen_e_acsl_valid;
+ int __gen_e_acsl_valid_read_3;
int __gen_e_acsl_active_bhvrs;
__e_acsl_store_block((void *)(& y),(size_t)8);
__e_acsl_store_block((void *)(& x),(size_t)8);
__gen_e_acsl_contract = __e_acsl_contract_init((size_t)2);
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)x,sizeof(int),
+ (void *)x,(void *)(& x));
+ __e_acsl_assert(__gen_e_acsl_valid_read,"RTE","f",
+ "mem_access: \\valid_read(x)",
+ "tests/special/e-acsl-valid.c",15);
__e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0,
*x == 1);
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)x,sizeof(int),
+ (void *)x,(void *)(& x));
+ __e_acsl_assert(__gen_e_acsl_valid_read_2,"RTE","f",
+ "mem_access: \\valid_read(x)",
+ "tests/special/e-acsl-valid.c",19);
__e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)1,
*x == 0);
__gen_e_acsl_valid = __e_acsl_valid((void *)y,sizeof(int),(void *)y,
(void *)(& y));
__e_acsl_assert(__gen_e_acsl_valid,"Precondition","f","\\valid(y)",
"tests/special/e-acsl-valid.c",10);
+ __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)x,sizeof(int),
+ (void *)x,(void *)(& x));
+ __e_acsl_assert(__gen_e_acsl_valid_read_3,"RTE","f",
+ "mem_access: \\valid_read(x)",
+ "tests/special/e-acsl-valid.c",11);
__e_acsl_assert(*x >= 0,"Precondition","f","*x >= 0",
"tests/special/e-acsl-valid.c",11);
__gen_e_acsl_active_bhvrs = __e_acsl_contract_partial_count_all_behaviors
@@ -135,10 +153,10 @@ void __gen_e_acsl_f(int *x, int *y)
__gen_e_acsl_at_4 = x;
__gen_e_acsl_at_3 = x;
{
- int __gen_e_acsl_valid_read;
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)x,sizeof(int),
- (void *)x,(void *)(& x));
- __e_acsl_assert(__gen_e_acsl_valid_read,"RTE","f",
+ int __gen_e_acsl_valid_read_4;
+ __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)x,sizeof(int),
+ (void *)x,(void *)(& x));
+ __e_acsl_assert(__gen_e_acsl_valid_read_4,"RTE","f",
"mem_access: \\valid_read(x)",
"tests/special/e-acsl-valid.c",12);
__gen_e_acsl_at_2 = (long)*x;
@@ -146,13 +164,13 @@ void __gen_e_acsl_f(int *x, int *y)
__gen_e_acsl_at = x;
f(x,y);
{
- int __gen_e_acsl_valid_read_2;
+ int __gen_e_acsl_valid_read_5;
int __gen_e_acsl_assumes_value;
- __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)__gen_e_acsl_at,
+ __gen_e_acsl_valid_read_5 = __e_acsl_valid_read((void *)__gen_e_acsl_at,
sizeof(int),
(void *)__gen_e_acsl_at,
(void *)(& __gen_e_acsl_at));
- __e_acsl_assert(__gen_e_acsl_valid_read_2,"RTE","f",
+ __e_acsl_assert(__gen_e_acsl_valid_read_5,"RTE","f",
"mem_access: \\valid_read(__gen_e_acsl_at)",
"tests/special/e-acsl-valid.c",12);
__e_acsl_assert((long)*__gen_e_acsl_at == __gen_e_acsl_at_2 + 1L,
@@ -161,12 +179,12 @@ void __gen_e_acsl_f(int *x, int *y)
__gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes
((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)0);
if (__gen_e_acsl_assumes_value) {
- int __gen_e_acsl_valid_read_3;
- __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)__gen_e_acsl_at_3,
+ int __gen_e_acsl_valid_read_6;
+ __gen_e_acsl_valid_read_6 = __e_acsl_valid_read((void *)__gen_e_acsl_at_3,
sizeof(int),
(void *)__gen_e_acsl_at_3,
(void *)(& __gen_e_acsl_at_3));
- __e_acsl_assert(__gen_e_acsl_valid_read_3,"RTE","f",
+ __e_acsl_assert(__gen_e_acsl_valid_read_6,"RTE","f",
"mem_access: \\valid_read(__gen_e_acsl_at_3)",
"tests/special/e-acsl-valid.c",17);
__e_acsl_assert(*__gen_e_acsl_at_3 < 0,"Postcondition","f",
@@ -175,12 +193,12 @@ void __gen_e_acsl_f(int *x, int *y)
__gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes
((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)1);
if (__gen_e_acsl_assumes_value) {
- int __gen_e_acsl_valid_read_4;
- __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)__gen_e_acsl_at_4,
+ int __gen_e_acsl_valid_read_7;
+ __gen_e_acsl_valid_read_7 = __e_acsl_valid_read((void *)__gen_e_acsl_at_4,
sizeof(int),
(void *)__gen_e_acsl_at_4,
(void *)(& __gen_e_acsl_at_4));
- __e_acsl_assert(__gen_e_acsl_valid_read_4,"RTE","f",
+ __e_acsl_assert(__gen_e_acsl_valid_read_7,"RTE","f",
"mem_access: \\valid_read(__gen_e_acsl_at_4)",
"tests/special/e-acsl-valid.c",20);
__e_acsl_assert(*__gen_e_acsl_at_4 == 1,"Postcondition","f",