From 58af7098a061adf45ca3aa19d0707f1e7bb51014 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 28 Apr 2021 11:32:37 +0200
Subject: [PATCH] [eacsl] Use kinstr in env
- Replace `Env.with_rte` and `Env.with_params` to be able to set `rte`
and `kinstr` for an environment;
- Remove `kinstr` parameters from the `Contract` function to use the
`kinstr` of the environment instead;
- Setup environment `kinstr` when injecting code into a statement or
when translating code or function annotation.
Regarding `Translate_annots.pre_funspec` and
`Translate_annots.post_funspec`, since they only translate function
annotations, the `kinstr` is directly set to `Kglobal` in the functions
instead of being taken as a parameter.
---
.../e-acsl/src/code_generator/contract.ml | 27 +++++-----
.../e-acsl/src/code_generator/contract.mli | 4 +-
src/plugins/e-acsl/src/code_generator/env.ml | 49 +++++++++++++------
src/plugins/e-acsl/src/code_generator/env.mli | 41 ++++++++++------
.../e-acsl/src/code_generator/injector.ml | 5 +-
.../src/code_generator/memory_translate.ml | 12 +++--
.../src/code_generator/translate_annots.ml | 46 ++++++++++++-----
.../src/code_generator/translate_annots.mli | 4 +-
.../code_generator/translate_predicates.ml | 24 ++++++---
.../src/code_generator/translate_rtes.ml | 4 +-
.../src/code_generator/translate_terms.ml | 24 ++++++---
11 files changed, 159 insertions(+), 81 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/contract.ml b/src/plugins/e-acsl/src/code_generator/contract.ml
index 4a94572f472..706c8c69780 100644
--- a/src/plugins/e-acsl/src/code_generator/contract.ml
+++ b/src/plugins/e-acsl/src/code_generator/contract.ml
@@ -315,7 +315,8 @@ let fold_left_handle_error_with_args f (env, acc) l =
(** Insert requires check for the default behavior of the given contract in the
environment. *)
-let check_default_requires kf kinstr env contract =
+let check_default_requires kf env contract =
+ let kinstr = Env.get_kinstr env in
let default_behavior =
Cil.find_default_behavior contract.spec
in
@@ -337,10 +338,11 @@ let check_default_requires kf kinstr env contract =
(** Insert requires check for the behaviors other than the default behavior of
the given contract in the environment *)
-let check_other_requires kf kinstr env contract =
+let check_other_requires kf env contract =
let get_or_create_assumes_var =
mk_get_or_create_var kf Cil.intType "assumes_value"
in
+ let kinstr = Env.get_kinstr env in
let do_behavior env b =
if Cil.is_default_behavior b then
env
@@ -440,7 +442,8 @@ type translate_ppt =
(** For each set of behavior names in [clauses], [check_active_behaviors] counts
the number of active behaviors and creates assertions for the
[ppt_to_translate]. *)
-let check_active_behaviors ~ppt_to_translate ~get_or_create_var kf kinstr env contract clauses =
+let check_active_behaviors ~ppt_to_translate ~get_or_create_var kf env contract clauses =
+ let kinstr = Env.get_kinstr env in
let loc = contract.location in
Cil.CurrentLoc.set loc;
let do_clause env bhvrs =
@@ -563,7 +566,7 @@ let check_active_behaviors ~ppt_to_translate ~get_or_create_var kf kinstr env co
(** Insert complete and disjoint behaviors check for the given contract in the
environement *)
-let check_complete_and_disjoint kf kinstr env contract =
+let check_complete_and_disjoint kf env contract =
(* Only translate the complete and disjoint clauses if all the assumes clauses
could be translated *)
if contract.all_assumes_translated then
@@ -611,7 +614,6 @@ let check_complete_and_disjoint kf kinstr env contract =
~ppt_to_translate
~get_or_create_var
kf
- kinstr
env
contract
bhvrs
@@ -630,10 +632,11 @@ let check_complete_and_disjoint kf kinstr env contract =
end
(** Insert ensures check for the given contract in the environement *)
-let check_post_conds kf kinstr env contract =
+let check_post_conds kf env contract =
let get_or_create_assumes_var =
mk_get_or_create_var kf Cil.intType "assumes_value"
in
+ let kinstr = Env.get_kinstr env in
let do_behavior env b =
let env =
Env.handle_error
@@ -763,14 +766,14 @@ let check_post_conds kf kinstr env contract =
env
contract.spec.spec_behavior
-let translate_preconditions kf kinstr env contract =
+let translate_preconditions kf env contract =
let env = Env.set_annotation_kind env Smart_stmt.Precondition in
let env = Env.push_contract env contract in
let env = init kf env contract in
(* Start with translating the requires predicate of the default behavior. *)
let env =
Env.handle_error
- (fun env -> check_default_requires kf kinstr env contract)
+ (fun env -> check_default_requires kf env contract)
env
in
(* Then setup the assumes clauses of the contract. *)
@@ -778,17 +781,17 @@ let translate_preconditions kf kinstr env contract =
(* And finally translate the requires predicates of the rest of the behaviors,
skipping over the default behavior. *)
let do_it env =
- let env = check_other_requires kf kinstr env contract in
- let env = check_complete_and_disjoint kf kinstr env contract in
+ let env = check_other_requires kf env contract in
+ let env = check_complete_and_disjoint kf env contract in
env
in
Env.handle_error do_it env
-let translate_postconditions kf kinstr env =
+let translate_postconditions kf env =
let env = Env.set_annotation_kind env Smart_stmt.Postcondition in
let contract, env = Env.pop_and_get_contract env in
let do_it env =
- let env = check_post_conds kf kinstr env contract in
+ let env = check_post_conds kf env contract in
env
in
let env = Env.handle_error do_it env in
diff --git a/src/plugins/e-acsl/src/code_generator/contract.mli b/src/plugins/e-acsl/src/code_generator/contract.mli
index d9db3d14ae9..8dc2a3a21df 100644
--- a/src/plugins/e-acsl/src/code_generator/contract.mli
+++ b/src/plugins/e-acsl/src/code_generator/contract.mli
@@ -32,8 +32,8 @@ val create: loc:location -> spec -> t
(** Create a contract from a [spec] object (either function spec or statement
spec) *)
-val translate_preconditions: kernel_function -> kinstr -> Env.t -> t -> Env.t
+val translate_preconditions: kernel_function -> Env.t -> t -> Env.t
(** Translate the preconditions of the given contract into the environement *)
-val translate_postconditions: kernel_function -> kinstr -> Env.t -> Env.t
+val translate_postconditions: kernel_function -> Env.t -> Env.t
(** Translate the postconditions of the given contract into the environment *)
diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
index b4005a462b3..e7ca3032d40 100644
--- a/src/plugins/e-acsl/src/code_generator/env.ml
+++ b/src/plugins/e-acsl/src/code_generator/env.ml
@@ -171,20 +171,6 @@ 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 = set_rte env rte_value in
- let env = f env in
- let env = set_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 = set_rte env rte_value in
- let other, env = f env in
- let env = set_rte env old_rte_value in
- other, env
-
(* ************************************************************************** *)
(** {2 Kinstr} *)
(* ************************************************************************** *)
@@ -605,6 +591,41 @@ let pop_contract env =
let _, env = pop_and_get_contract env in
env
+(* ************************************************************************** *)
+(** {2 Utilities} *)
+(* ************************************************************************** *)
+
+let with_params_and_result ?rte ?kinstr ~f env =
+ let old_rte, env =
+ match rte with
+ | Some rte ->
+ Some (generate_rte env), set_rte env rte
+ | None -> None, env
+ in
+ let old_kinstr, env =
+ match kinstr with
+ | Some kinstr ->
+ Some (get_kinstr env), set_kinstr env kinstr
+ | None -> None, env
+ in
+ let other, env = f env in
+ let env =
+ match old_kinstr with
+ | Some kinstr -> set_kinstr env kinstr
+ | None -> env
+ in
+ let env =
+ match old_rte with
+ | Some rte -> set_rte env rte
+ | None -> env
+ in
+ other, env
+
+let with_params ?rte ?kinstr ~f env =
+ let (), env =
+ with_params_and_result ?rte ?kinstr ~f:(fun env -> (), f env) env
+ in
+ env
(* debugging purpose *)
let pretty fmt env =
diff --git a/src/plugins/e-acsl/src/code_generator/env.mli b/src/plugins/e-acsl/src/code_generator/env.mli
index 4586fc3adce..19a5b6f59b4 100644
--- a/src/plugins/e-acsl/src/code_generator/env.mli
+++ b/src/plugins/e-acsl/src/code_generator/env.mli
@@ -175,22 +175,6 @@ val set_rte: t -> bool -> t
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. *)
-
module Local_vars: sig
val push_new: t -> t
val add: t -> Typing.number_ty -> t
@@ -243,6 +227,31 @@ val pop_and_get_contract: t -> contract * t
val pop_contract: t -> t
(** Pop the top contract of the environment's stack *)
+(* ************************************************************************** *)
+(** {2 Utilities} *)
+(* ************************************************************************** *)
+
+val with_params: ?rte:bool -> ?kinstr:kinstr -> f:(t -> t) -> t -> t
+(** [with_params ~rte ~kinstr ~f env] executes the given closure with the given
+ environment after having set RTE generation to [rte] and current kinstr to
+ [kinstr].
+ [f] is a closure that takes an environment and returns an environment.
+ The environment returned by the closure is updated to restore the RTE
+ generation and kinstr attributes to the values of the original environment,
+ then is returned. *)
+
+val with_params_and_result:
+ ?rte:bool -> ?kinstr:kinstr -> f:(t -> 'a * t) -> t -> 'a * t
+(** [with_params_and_result ~rte ~kinstr ~f env] executes the given closure with
+ the given environment after having set RTE generation to [rte] and current
+ kinstr to [kinstr].
+ [f] is a closure that takes an environment and returns a pair where the
+ first member is an arbitrary value and the second member is the environment.
+ The environment returned by the closure is updated to restore the RTE
+ generation and kinstr attributes to the values of the original environment,
+ then the function returns the arbitrary value returned by the closure along
+ with the updated environment. *)
+
val pretty: Format.formatter -> t -> unit
(*
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index fe2bb263fc6..dafcb58caf8 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -268,7 +268,7 @@ let add_new_block_in_stmt env kf stmt =
let env = mk_post_env env stmt in
(* also handle the postcondition of the function and clear the
env *)
- Translate_annots.post_funspec kf Kglobal env
+ Translate_annots.post_funspec kf env
else
env
in
@@ -451,6 +451,7 @@ and inject_in_stmt env kf stmt =
| Loop _ -> Env.push_loop env
| _ -> env
in
+ let env = Env.set_kinstr env (Kstmt stmt) in
(* initial environment *)
let env =
if Kernel_function.is_first_stmt kf stmt then
@@ -466,7 +467,7 @@ and inject_in_stmt env kf stmt =
(* translate the precondition of the function *)
if Functions.check kf then
let funspec = Annotations.funspec kf in
- Translate_annots.pre_funspec kf Kglobal env funspec
+ Translate_annots.pre_funspec kf env funspec
else env
else
env
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 2b4c63c55e9..08d0fdba873 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
@@ -144,10 +144,12 @@ let call ~adata ~loc kf name ctx env t =
assert (name = "base_addr" || name = "block_length"
|| name = "offset" || name ="freeable");
let (e, adata), env =
- Env.with_rte_and_result env true
+ Env.with_params_and_result
+ ~rte:true
~f:(fun env ->
let e, adata, env = !term_to_exp_ref ~adata kf env t in
(e, adata), env)
+ env
in
let e, env =
Env.rtl_call_to_new_var
@@ -219,10 +221,12 @@ let range_to_ptr_and_size ~adata ~loc kf env ptr r p =
~lenv:(Env.Local_vars.get env)
ptr;
let (ptr, adata), env =
- Env.with_rte_and_result env true
+ Env.with_params_and_result
+ ~rte:true
~f:(fun env ->
let e, adata, env = !term_to_exp_ref ~adata kf env ptr in
(e, adata), env)
+ env
in
(* size *)
let size_term =
@@ -296,10 +300,12 @@ let range_to_ptr_and_size ~adata ~loc kf env ptr r p =
[p] is the predicate under test. *)
let term_to_ptr_and_size ~adata ~loc kf env t =
let (e, adata), env =
- Env.with_rte_and_result env true
+ Env.with_params_and_result
+ ~rte:true
~f:(fun env ->
let e, adata, env = !term_to_exp_ref ~adata kf env t in
(e, adata), env)
+ env
in
let ty = Misc.cty t.term_type in
let sizeof = Smart_exp.ptr_sizeof ~loc ty in
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 42e2045604e..a1d1cfb14b6 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_annots.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_annots.ml
@@ -28,7 +28,8 @@ open Cil_datatype
statements (if any) for runtime assertion checking. *)
(* ************************************************************************** *)
-let pre_funspec kf kinstr env funspec =
+let pre_funspec kf env funspec =
+ let kinstr = Kglobal in
let unsupported f x = ignore (Env.handle_error (fun env -> f x; env) env) in
let convert_unsupported_clauses env =
unsupported
@@ -50,14 +51,21 @@ let pre_funspec kf kinstr env funspec =
Cil.CurrentLoc.set loc;
let env = convert_unsupported_clauses env in
let contract = Contract.create ~loc funspec in
- Env.with_rte env true
- ~f:(fun env -> Contract.translate_preconditions kf kinstr env contract)
+ Env.with_params
+ ~rte:true
+ ~kinstr
+ ~f:(fun env -> Contract.translate_preconditions kf env contract)
+ env
-let post_funspec kf kinstr env =
- Env.with_rte env true
- ~f:(fun env -> Contract.translate_postconditions kf kinstr env)
+let post_funspec kf env =
+ Env.with_params
+ ~rte:true
+ ~kinstr:Kglobal
+ ~f:(fun env -> Contract.translate_postconditions kf env)
+ env
let pre_code_annotation kf stmt env annot =
+ let kinstr = Kstmt stmt in
let convert env = match annot.annot_content with
| AAssert(l, p) ->
if Translate_utils.must_translate
@@ -65,8 +73,11 @@ 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@]";
- Env.with_rte env true
+ Env.with_params
+ ~rte:true
+ ~kinstr
~f:(fun env -> Translate_predicates.do_it kf env p)
+ env
else
env
| AStmtSpec(l, spec) ->
@@ -74,9 +85,11 @@ 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
- Env.with_rte env true
- ~f:(fun env ->
- Contract.translate_preconditions kf (Kstmt stmt) env contract)
+ Env.with_params
+ ~rte:true
+ ~kinstr
+ ~f:(fun env -> Contract.translate_preconditions kf env contract)
+ env
| AInvariant(l, loop_invariant, p) ->
if Translate_utils.must_translate
(Property.ip_of_code_annot_single kf stmt annot) then
@@ -84,8 +97,11 @@ let pre_code_annotation kf stmt env annot =
if l <> [] then
Env.not_yet env "@[invariant applied only on some behaviors@]";
let env =
- Env.with_rte env true
+ Env.with_params
+ ~rte:true
+ ~kinstr
~f:(fun env -> Translate_predicates.do_it kf env p)
+ env
in
if loop_invariant then
Env.add_loop_invariant env p
@@ -121,10 +137,14 @@ let pre_code_annotation kf stmt env annot =
Env.handle_error convert env
let post_code_annotation kf stmt env annot =
+ let kinstr = Kstmt stmt in
let convert env = match annot.annot_content with
| AStmtSpec(_, _) ->
- Env.with_rte env true
- ~f:(fun env -> Contract.translate_postconditions kf (Kstmt stmt) env)
+ Env.with_params
+ ~rte:true
+ ~kinstr
+ ~f:(fun env -> Contract.translate_postconditions kf env)
+ env
| AAssert _
| AInvariant _
| AVariant _
diff --git a/src/plugins/e-acsl/src/code_generator/translate_annots.mli b/src/plugins/e-acsl/src/code_generator/translate_annots.mli
index 3c5669a3f97..a9931f901e9 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_annots.mli
+++ b/src/plugins/e-acsl/src/code_generator/translate_annots.mli
@@ -26,7 +26,7 @@ open Cil_types
statements (if any) for runtime assertion checking. These C statements are
part of the resulting environment. *)
-val pre_funspec: kernel_function -> kinstr -> Env.t -> funspec -> Env.t
+val pre_funspec: kernel_function -> Env.t -> funspec -> Env.t
(** Translate the preconditions of the given function contract in the
environment. The contract is attached to the kernel_function.
@@ -34,7 +34,7 @@ val pre_funspec: kernel_function -> kinstr -> Env.t -> funspec -> Env.t
taken to call {!post_funspec} at the right time to pop the right
contract. *)
-val post_funspec: kernel_function -> kinstr -> Env.t -> Env.t
+val post_funspec: kernel_function -> Env.t -> Env.t
(** Translate the postconditions of the current function contract in the
environment.
diff --git a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
index 936a00f3d51..c65609dc83d 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
@@ -100,7 +100,8 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
| Pand(p1, p2) ->
(* p1 && p2 <==> if p1 then p2 else false *)
Extlib.flatten
- (Env.with_rte_and_result env true
+ (Env.with_params_and_result
+ ~rte:true
~f:(fun env ->
let e1, adata, env1 = to_exp ~adata kf env p1 in
let e2, adata, env2 =
@@ -118,11 +119,13 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
e1
res2
(Cil.zero loc, env3))
- ))
+ )
+ env)
| Por(p1, p2) ->
(* p1 || p2 <==> if p1 then true else p2 *)
Extlib.flatten
- (Env.with_rte_and_result env true
+ (Env.with_params_and_result
+ ~rte:true
~f:(fun env ->
let e1, adata, env1 = to_exp ~adata kf env p1 in
let env' = Env.push env1 in
@@ -141,7 +144,8 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
e1
(Cil.one loc, env')
res2)
- ))
+ )
+ env)
| Pxor _ -> Env.not_yet env "xor"
| Pimplies(p1, p2) ->
(* (p1 ==> p2) <==> !p1 || p2 *)
@@ -166,7 +170,8 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
Smart_exp.lnot ~loc e, adata, env
| Pif(t, p2, p3) ->
Extlib.flatten
- (Env.with_rte_and_result env true
+ (Env.with_params_and_result
+ ~rte:true
~f:(fun env ->
let e1, adata, env1 = Translate_terms.to_exp ~adata kf env t in
let e2, adata, env2 =
@@ -179,7 +184,8 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
Extlib.nest
adata
(Translate_utils.conditional_to_exp ~loc kf None e1 res2 res3)
- ))
+ )
+ env)
| Plet(li, p) ->
let lvs = Lvs_let(li.l_var_info, Misc.term_of_li li) in
let env = Env.Logic_scope.extend env lvs in
@@ -304,7 +310,8 @@ and to_exp ~adata ?name kf ?rte env p =
| PoT_pred p ->
let rte = match rte with None -> Env.generate_rte env | Some b -> b in
Extlib.flatten
- (Env.with_rte_and_result env false
+ (Env.with_params_and_result
+ ~rte:false
~f:(fun env ->
let e, adata, env =
predicate_content_to_exp ~adata ?name kf env p
@@ -326,7 +333,8 @@ and to_exp ~adata ?name kf ?rte env p =
Typed_number.C_number
None
e)
- ))
+ )
+ env)
let generalized_untyped_to_exp ~adata ?name kf ?rte env p =
(* If [rte] is true, it means we're translating the root predicate of an
diff --git a/src/plugins/e-acsl/src/code_generator/translate_rtes.ml b/src/plugins/e-acsl/src/code_generator/translate_rtes.ml
index cb3175ec940..cb05e6165e8 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_rtes.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_rtes.ml
@@ -41,8 +41,10 @@ let rte_annots pp elt kf env l =
let lscope_reset_old = Env.Logic_scope.get_reset env in
let env = Env.Logic_scope.set_reset env false in
let env =
- Env.with_rte env false
+ Env.with_params
+ ~rte:false
~f:(fun env -> Translate_predicates.do_it kf env p)
+ env
in
let env = Env.Logic_scope.set_reset env lscope_reset_old in
env)
diff --git a/src/plugins/e-acsl/src/code_generator/translate_terms.ml b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
index 1b48abacde0..056ae31da69 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_terms.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
@@ -641,7 +641,8 @@ and context_insensitive_term_to_exp ~adata kf env t =
(* t1 || t2 <==> if t1 then true else t2 *)
let e, adata, env =
Extlib.flatten
- (Env.with_rte_and_result env true
+ (Env.with_params_and_result
+ ~rte:true
~f:(fun env ->
let e1, adata, env1 = to_exp ~adata kf env t1 in
let env' = Env.push env1 in
@@ -653,14 +654,16 @@ and context_insensitive_term_to_exp ~adata kf env t =
adata
(Translate_utils.conditional_to_exp
~name:"or" ~loc kf (Some t) e1 (Cil.one loc, env') res2)
- ))
+ )
+ env)
in
e, adata, env, Typed_number.C_number, ""
| TBinOp(LAnd, t1, t2) ->
(* t1 && t2 <==> if t1 then t2 else false *)
let e, adata, env =
Extlib.flatten
- (Env.with_rte_and_result env true
+ (Env.with_params_and_result
+ ~rte:true
~f:(fun env ->
let e1, adata, env1 = to_exp ~adata kf env t1 in
let e2, adata, env2 =
@@ -672,7 +675,8 @@ and context_insensitive_term_to_exp ~adata kf env t =
adata
(Translate_utils.conditional_to_exp
~name:"and" ~loc kf (Some t) e1 res2 (Cil.zero loc, env3))
- ))
+ )
+ env)
in
e, adata, env, Typed_number.C_number, ""
| TBinOp((BOr | BXor | BAnd) as bop, t1, t2) ->
@@ -770,7 +774,8 @@ and context_insensitive_term_to_exp ~adata kf env t =
| Tif(t1, t2, t3) ->
let e, adata, env =
Extlib.flatten
- (Env.with_rte_and_result env true
+ (Env.with_params_and_result
+ ~rte:true
~f:(fun env ->
let e1, adata, env1 = to_exp ~adata kf env t1 in
let e2, adata, env2 =
@@ -790,7 +795,8 @@ and context_insensitive_term_to_exp ~adata kf env t =
e1
res2
res3)
- ))
+ )
+ env)
in
e, adata, env, Typed_number.C_number, ""
| Tat(t, BuiltinLabel Here) ->
@@ -873,7 +879,8 @@ and to_exp ~adata kf env t =
(Env.Local_vars.get env);
let t = Logic_normalizer.get_term t in
Extlib.flatten
- (Env.with_rte_and_result env false
+ (Env.with_params_and_result
+ ~rte:false
~f:(fun env ->
let e, adata, env, sty, name =
context_insensitive_term_to_exp ~adata kf env t
@@ -894,7 +901,8 @@ and to_exp ~adata kf env t =
sty
(Some t)
e)
- ))
+ )
+ env)
let () =
Translate_utils.term_to_exp_ref := to_exp;
--
GitLab