[eacsl] Rename Env.rte to Env.set_rte

src/plugins/e-acsl/src/code_generator/env.ml

@@ -163,7 +163,7 @@ let pop_loop env =
 (** {2 RTEs} *)
 (* ************************************************************************** *)
 
-let rte env b =
+let set_rte env b =
   let local_env, tl_env = top env in
   { env with env_stack = { local_env with rte = b } :: tl_env }
 
@@ -173,16 +173,16 @@ let generate_rte env =
 
 let with_rte ~f env rte_value =
   let old_rte_value = generate_rte env in
-  let env = rte env rte_value in
+  let env = set_rte env rte_value in
   let env = f env in
-  let env = rte env old_rte_value 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 = rte env rte_value in
+  let env = set_rte env rte_value in
   let other, env = f env in
-  let env = rte env old_rte_value in
+  let env = set_rte env old_rte_value in
   other, env
 
 (* ************************************************************************** *)

src/plugins/e-acsl/src/code_generator/env.mli

@@ -169,8 +169,8 @@ val pop_loop: t -> t
 (** {2 RTEs} *)
 (* ************************************************************************** *)
 
-val rte: t -> bool -> t
-(** [rte env x] sets RTE generation to x for the given environment *)
+val set_rte: t -> bool -> t
+(** [set_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 *)

src/plugins/e-acsl/src/code_generator/translate_predicates.ml

@@ -392,7 +392,7 @@ exception No_simple_translation of predicate
    However, it is correct to use it only in specific contexts. *)
 let untyped_to_exp p =
   let env = Env.push Env.empty in
-  let env = Env.rte env false in
+  let env = Env.set_rte env false in
   let e, _, env =
     try generalized_untyped_to_exp
           ~adata:Assert.no_data

src/plugins/e-acsl/src/code_generator/translate_terms.ml

@@ -920,7 +920,7 @@ let untyped_to_exp typ t =
   let ctx = Option.map ctx_of_typ typ in
   Typing.type_term ~use_gmp_opt:true ~lenv:[] ?ctx t;
   let env = Env.push Env.empty in
-  let env = Env.rte env false in
+  let env = Env.set_rte env false in
   let e, _, env =
     try to_exp ~adata:Assert.no_data (Kernel_function.dummy ()) env t
     with Rtl.Symbols.Unregistered _ -> raise (No_simple_translation t)