From 8f29bdb8b3e8e22f2ba91cb61738f7e6c0b09774 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 1 Dec 2021 15:46:35 +0100
Subject: [PATCH] [eacsl] Split module translate

---
 src/plugins/e-acsl/E_ACSL.mli                 |   4 +-
 src/plugins/e-acsl/Makefile.in                |   5 +-
 src/plugins/e-acsl/headers/header_spec.txt    |  10 +-
 .../e-acsl/src/code_generator/contract.ml     |  35 +-
 .../e-acsl/src/code_generator/contract.mli    |   8 -
 .../e-acsl/src/code_generator/injector.ml     |   2 +-
 src/plugins/e-acsl/src/code_generator/libc.ml |   4 +-
 .../e-acsl/src/code_generator/quantif.ml      |   2 +-
 .../src/code_generator/translate_annots.ml    |  41 +-
 .../src/code_generator/translate_annots.mli   |  11 +-
 .../code_generator/translate_predicates.ml    | 395 ++++++++++
 ...translate.mli => translate_predicates.mli} |  63 +-
 .../src/code_generator/translate_rtes.ml      |  79 ++
 .../src/code_generator/translate_rtes.mli     |  45 ++
 .../{translate.ml => translate_terms.ml}      | 688 +-----------------
 .../src/code_generator/translate_terms.mli    |  57 ++
 .../src/code_generator/translate_utils.ml     | 349 +++++++++
 .../src/code_generator/translate_utils.mli    | 134 ++++
 18 files changed, 1151 insertions(+), 781 deletions(-)
 create mode 100644 src/plugins/e-acsl/src/code_generator/translate_predicates.ml
 rename src/plugins/e-acsl/src/code_generator/{translate.mli => translate_predicates.mli} (68%)
 create mode 100644 src/plugins/e-acsl/src/code_generator/translate_rtes.ml
 create mode 100644 src/plugins/e-acsl/src/code_generator/translate_rtes.mli
 rename src/plugins/e-acsl/src/code_generator/{translate.ml => translate_terms.ml} (60%)
 create mode 100644 src/plugins/e-acsl/src/code_generator/translate_terms.mli
 create mode 100644 src/plugins/e-acsl/src/code_generator/translate_utils.ml
 create mode 100644 src/plugins/e-acsl/src/code_generator/translate_utils.mli

diff --git a/src/plugins/e-acsl/E_ACSL.mli b/src/plugins/e-acsl/E_ACSL.mli
index 813638711ec..62c147d84b9 100644
--- a/src/plugins/e-acsl/E_ACSL.mli
+++ b/src/plugins/e-acsl/E_ACSL.mli
@@ -29,7 +29,7 @@ module Error: sig
   exception Not_yet of string
 end
 
-module Translate: sig
+module Translate_terms: sig
   exception No_simple_term_translation of term
   val untyped_term_to_exp: typ option -> term -> exp
   (** @raise Typing_error when the given term cannot be typed (something wrong
@@ -37,7 +37,9 @@ module Translate: sig
       @raise Not_yet when the given term contains an unsupported construct.
       @raise No_simple_term_translation when the given term cannot be translated
       into a single expression. *)
+end
 
+module Translate_predicates: sig
   exception No_simple_predicate_translation of predicate
   val untyped_predicate_to_exp: predicate -> exp
   (** @raise Typing_error when the given predicate cannot be typed
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index e612b382343..25672c530b4 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -90,7 +90,10 @@ SRC_CODE_GENERATOR:= \
 	at_with_lscope \
 	memory_translate \
 	logic_array \
-	translate \
+	translate_utils \
+	translate_terms \
+	translate_predicates \
+	translate_rtes \
 	contract \
 	translate_annots \
 	temporal \
diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
index 506060af0d6..4c8e1b25736 100644
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ b/src/plugins/e-acsl/headers/header_spec.txt
@@ -135,10 +135,16 @@ src/code_generator/smart_stmt.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/smart_stmt.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/temporal.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/temporal.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/translate.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/translate.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/translate_annots.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/translate_annots.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/translate_predicates.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/translate_predicates.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/translate_rtes.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/translate_rtes.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/translate_terms.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/translate_terms.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/translate_utils.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/translate_utils.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/typed_number.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/typed_number.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/libraries/builtins.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
diff --git a/src/plugins/e-acsl/src/code_generator/contract.ml b/src/plugins/e-acsl/src/code_generator/contract.ml
index 7f300b20d9c..1ed15a8d553 100644
--- a/src/plugins/e-acsl/src/code_generator/contract.ml
+++ b/src/plugins/e-acsl/src/code_generator/contract.ml
@@ -23,16 +23,6 @@
 open Cil_types
 open Contract_types
 
-(**************************************************************************)
-(********************** Forward references ********************************)
-(**************************************************************************)
-
-let must_translate_ppt_ref : (Property.t -> bool) ref =
-  Extlib.mk_fun "must_translate_ppt_ref"
-
-let must_translate_ppt_opt_ref : (Property.t option -> bool) ref =
-  Extlib.mk_fun "must_translate_ppt_opt_ref"
-
 (**************************************************************************)
 (********************** Contract ********************************)
 (**************************************************************************)
@@ -109,7 +99,7 @@ end = struct
   let set_assumes ~loc env kf contract idx assumes =
     let idx_e = Cil.integer ~loc idx in
     let assumes_e, _, env =
-      Translate.generalized_untyped_predicate_to_exp
+      Translate_predicates.generalized_untyped_predicate_to_exp
         ~adata:Assert.no_data
         kf
         env
@@ -332,12 +322,12 @@ let check_default_requires kf kinstr env contract =
   | Some b ->
     fold_left_handle_error
       (fun env ip_requires ->
-         if !must_translate_ppt_ref
+         if Translate_utils.must_translate
              (Property.ip_of_requires kf kinstr b ip_requires) then
            let tp_requires = ip_requires.ip_content in
            let loc = tp_requires.tp_statement.pred_loc in
            Cil.CurrentLoc.set loc;
-           Translate.translate_predicate kf env tp_requires
+           Translate_predicates.translate_predicate kf env tp_requires
          else
            env)
       env
@@ -361,7 +351,7 @@ let check_other_requires kf kinstr env contract =
       let env, stmts =
         fold_left_handle_error_with_args
           (fun (env, stmts) ip_requires ->
-             if !must_translate_ppt_ref
+             if Translate_utils.must_translate
                  (Property.ip_of_requires kf kinstr b ip_requires) then
                let tp_requires = ip_requires.ip_content in
                let pred_kind = tp_requires.tp_kind in
@@ -378,7 +368,7 @@ let check_other_requires kf kinstr env contract =
                  (* Create runtime check *)
                  let adata, env = Assert.empty ~loc kf env in
                  let requires_e, adata, env =
-                   Translate.generalized_untyped_predicate_to_exp
+                   Translate_predicates.generalized_untyped_predicate_to_exp
                      ~adata
                      kf
                      env
@@ -450,7 +440,6 @@ type translate_ppt =
     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 must_translate = !must_translate_ppt_ref in
   let loc = contract.location in
   Cil.CurrentLoc.set loc;
   let do_clause env bhvrs =
@@ -459,13 +448,13 @@ let check_active_behaviors ~ppt_to_translate ~get_or_create_var kf kinstr env co
     let must_translate_complete =
       match ppt_to_translate with
       | Both | Complete ->
-        must_translate (Property.ip_of_complete kf kinstr ~active bhvrs_list)
+        Translate_utils.must_translate (Property.ip_of_complete kf kinstr ~active bhvrs_list)
       | Disjoint -> false
     in
     let must_translate_disjoint =
       match ppt_to_translate with
       | Both | Disjoint ->
-        must_translate (Property.ip_of_disjoint kf kinstr ~active bhvrs_list)
+        Translate_utils.must_translate (Property.ip_of_disjoint kf kinstr ~active bhvrs_list)
       | Complete -> false
     in
 
@@ -646,7 +635,7 @@ let check_post_conds kf kinstr env contract =
         (fun env ->
            let active = [] in (* TODO: 'for' behaviors, e-acsl#109 *)
            let ppt = Property.ip_assigns_of_behavior kf kinstr ~active b in
-           if b.b_assigns <> WritesAny && !must_translate_ppt_opt_ref ppt
+           if b.b_assigns <> WritesAny && Translate_utils.must_translate_opt ppt
            then Env.not_yet env "assigns clause in behavior";
            (* ignore b.b_extended since we never translate them *)
            env)
@@ -655,7 +644,7 @@ let check_post_conds kf kinstr env contract =
     if Cil.is_default_behavior b then
       fold_left_handle_error
         (fun env ((termination, ip_post_cond) as tp) ->
-           if !must_translate_ppt_ref
+           if Translate_utils.must_translate
                (Property.ip_of_ensures kf kinstr b tp) then
              let tp_post_cond = ip_post_cond.ip_content in
              let loc = tp_post_cond.tp_statement.pred_loc in
@@ -664,7 +653,7 @@ let check_post_conds kf kinstr env contract =
              | Normal ->
                (* If translating the default behavior, directly translate the
                   predicate *)
-               Translate.translate_predicate kf env tp_post_cond
+               Translate_predicates.translate_predicate kf env tp_post_cond
              | Exits | Breaks | Continues | Returns ->
                Error.print_not_yet "abnormal termination case in behavior";
                env
@@ -680,7 +669,7 @@ let check_post_conds kf kinstr env contract =
       let env, stmts =
         fold_left_handle_error_with_args
           (fun (env, stmts) ((termination, ip_post_cond) as tp) ->
-             if !must_translate_ppt_ref
+             if Translate_utils.must_translate
                  (Property.ip_of_ensures kf kinstr b tp) then
                let tp_post_cond = ip_post_cond.ip_content in
                let pred_kind = tp_post_cond.tp_kind in
@@ -702,7 +691,7 @@ let check_post_conds kf kinstr env contract =
                      (* Create runtime check *)
                      let adata, env = Assert.empty ~loc kf env in
                      let post_cond_e, adata, env =
-                       Translate.generalized_untyped_predicate_to_exp
+                       Translate_predicates.generalized_untyped_predicate_to_exp
                          ~adata
                          kf
                          env
diff --git a/src/plugins/e-acsl/src/code_generator/contract.mli b/src/plugins/e-acsl/src/code_generator/contract.mli
index df12966e4ec..d9db3d14ae9 100644
--- a/src/plugins/e-acsl/src/code_generator/contract.mli
+++ b/src/plugins/e-acsl/src/code_generator/contract.mli
@@ -37,11 +37,3 @@ val translate_preconditions: kernel_function -> kinstr -> Env.t -> t -> Env.t
 
 val translate_postconditions: kernel_function -> kinstr -> Env.t -> Env.t
 (** Translate the postconditions of the given contract into the environment *)
-
-(**************************************************************************)
-(********************** Forward references ********************************)
-(**************************************************************************)
-
-val must_translate_ppt_ref: (Property.t -> bool) ref
-
-val must_translate_ppt_opt_ref: (Property.t option -> bool) ref
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index e564026ed9b..1a953ebb8fe 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -215,7 +215,7 @@ let add_new_block_in_stmt env kf stmt =
           List.iter
             (Typing.preprocess_rte ~lenv:(Env.Local_vars.get env))
             rtes;
-          Translate.translate_rte_annots Printer.pp_stmt stmt kf env rtes
+          Translate_rtes.translate_rte_annots Printer.pp_stmt stmt kf env rtes
         end else
           env
       in
diff --git a/src/plugins/e-acsl/src/code_generator/libc.ml b/src/plugins/e-acsl/src/code_generator/libc.ml
index c048c5cd1ba..5c1a5f60c8e 100644
--- a/src/plugins/e-acsl/src/code_generator/libc.ml
+++ b/src/plugins/e-acsl/src/code_generator/libc.ml
@@ -191,7 +191,7 @@ let term_to_sizet_exp ~loc ~name ?(check_lower_bound=true) kf env t =
   match Typing.get_number_ty ~lenv:(Env.Local_vars.get env) t with
   | Typing.Gmpz ->
     let e, _, env =
-      Translate.gmp_to_sizet
+      Translate_utils.gmp_to_sizet
         ~adata:Assert.no_data
         ~loc
         ~name
@@ -203,7 +203,7 @@ let term_to_sizet_exp ~loc ~name ?(check_lower_bound=true) kf env t =
     e, env
   | Typing.(C_integer _ | C_float _) as nty ->
     (* We know that [t] can be translated to a C type, so we start with that *)
-    let e, _, env = Translate.term_to_exp ~adata:Assert.no_data kf env t in
+    let e, _, env = Translate_terms.term_to_exp ~adata:Assert.no_data kf env t in
     (* Then we can check if the expression will fit in a [size_t] *)
     let sizet = Cil.(theMachine.typeOfSizeOf) in
     let sizet_kind = Cil.(theMachine.kindOfSizeOf) in
diff --git a/src/plugins/e-acsl/src/code_generator/quantif.ml b/src/plugins/e-acsl/src/code_generator/quantif.ml
index 4e331d96729..2a5e0a68ade 100644
--- a/src/plugins/e-acsl/src/code_generator/quantif.ml
+++ b/src/plugins/e-acsl/src/code_generator/quantif.ml
@@ -23,7 +23,7 @@
 open Cil_types
 open Cil
 
-(** Forward reference for [Translate.predicate_to_exp]. *)
+(** Forward reference for [Translate_predicates.to_exp]. *)
 let predicate_to_exp_ref
   : (adata:Assert.t ->
      kernel_function ->
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 f83509dfe97..3b88b8ccdd4 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_annots.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_annots.ml
@@ -28,42 +28,19 @@ open Cil_datatype
    statements (if any) for runtime assertion checking. *)
 (* ************************************************************************** *)
 
-let must_translate ppt =
-  Options.Valid.get ()
-  || match Property_status.get ppt with
-  | Never_tried
-  | Inconsistent _
-  | Best ((False_if_reachable | False_and_reachable | Dont_know), _) ->
-    true
-  | Best (True, _) ->
-    (* [TODO] generating code for "valid under hypotheses" properties could be
-       useful for some use cases (in particular, when E-ACSL does not stop on
-       the very first error).
-       ==> introduce a new option or modify the behavior of -e-acsl-valid,
-       see e-acsl#35 *)
-    false
-
-let must_translate_opt = function
-  | None -> false
-  | Some ppt -> must_translate ppt
-
-let () =
-  Contract.must_translate_ppt_ref := must_translate;
-  Contract.must_translate_ppt_opt_ref := must_translate_opt
-
 let pre_funspec kf kinstr env funspec =
   let unsupported f x = ignore (Env.handle_error (fun env -> f x; env) env) in
   let convert_unsupported_clauses env =
     unsupported
       (fun spec ->
          let ppt = Property.ip_decreases_of_spec kf kinstr spec in
-         if must_translate_opt ppt then Env.not_yet env "decreases clause")
+         if Translate_utils.must_translate_opt ppt then Env.not_yet env "decreases clause")
       funspec;
     (* TODO: spec.spec_terminates is not part of the E-ACSL subset *)
     unsupported
       (fun spec ->
          let ppt = Property.ip_terminates_of_spec kf kinstr spec in
-         if must_translate_opt ppt then Env.not_yet env "terminates clause")
+         if Translate_utils.must_translate_opt ppt then Env.not_yet env "terminates clause")
       funspec;
     env
   in
@@ -81,12 +58,12 @@ let post_funspec kf kinstr env =
 let pre_code_annotation kf stmt env annot =
   let convert env = match annot.annot_content with
     | AAssert(l, p) ->
-      if must_translate (Property.ip_of_code_annot_single kf stmt annot) then
+      if Translate_utils.must_translate (Property.ip_of_code_annot_single kf stmt annot) then
         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
-          ~f:(fun env -> Translate.translate_predicate kf env p)
+          ~f:(fun env -> Translate_predicates.translate_predicate kf env p)
       else
         env
     | AStmtSpec(l, spec) ->
@@ -98,13 +75,13 @@ let pre_code_annotation kf stmt env annot =
         ~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
+      if Translate_utils.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 =
           Env.with_rte env true
-            ~f:(fun env -> Translate.translate_predicate kf env p)
+            ~f:(fun env -> Translate_predicates.translate_predicate kf env p)
         in
         if loop_invariant then
           Env.add_loop_invariant env p
@@ -112,7 +89,7 @@ let pre_code_annotation kf stmt env annot =
       else
         env
     | AVariant (t, measure) ->
-      if must_translate (Property.ip_of_code_annot_single kf stmt annot)
+      if Translate_utils.must_translate (Property.ip_of_code_annot_single kf stmt annot)
       then Env.set_loop_variant env ?measure t
       else env
     | AAssigns _ ->
@@ -120,13 +97,13 @@ let pre_code_annotation kf stmt env annot =
          to be fixed when implementing e-acsl#29 *)
       let ppts = Property.ip_of_code_annot kf stmt annot in
       List.iter
-        (fun ppt -> if must_translate ppt then Env.not_yet env "assigns")
+        (fun ppt -> if Translate_utils.must_translate ppt then Env.not_yet env "assigns")
         ppts;
       env
     | AAllocation _ ->
       let ppts = Property.ip_of_code_annot kf stmt annot in
       List.iter
-        (fun ppt -> if must_translate ppt then Env.not_yet env "allocation")
+        (fun ppt -> if Translate_utils.must_translate ppt then Env.not_yet env "allocation")
         ppts;
       env
     | APragma _ -> Env.not_yet env "pragma"
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 7fcd0651c9f..3c5669a3f97 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_annots.mli
+++ b/src/plugins/e-acsl/src/code_generator/translate_annots.mli
@@ -26,15 +26,6 @@ open Cil_types
     statements (if any) for runtime assertion checking. These C statements are
     part of the resulting environment. *)
 
-val must_translate: Property.t -> bool
-(** Return true if the given property must be translated (ie. if the valid
-    properties must be translated or if its status is not [True]), false
-    otherwise. *)
-
-val must_translate_opt: Property.t option -> bool
-(** Same than [must_translate] but for [Property.t option]. Return false if the
-    option is [None]. *)
-
 val pre_funspec: kernel_function -> kinstr -> Env.t -> funspec -> Env.t
 (** Translate the preconditions of the given function contract in the
     environment. The contract is attached to the kernel_function.
@@ -72,6 +63,6 @@ val post_code_annotation:
 
 (*
 Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
 End:
 *)
diff --git a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
new file mode 100644
index 00000000000..f0616ff4952
--- /dev/null
+++ b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
@@ -0,0 +1,395 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
+(*                                                                        *)
+(*  Copyright (C) 2012-2021                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+(** Generate C implementations of E-ACSL predicates. *)
+
+open Cil_types
+open Cil_datatype
+let dkey = Options.dkey_translation
+
+(**************************************************************************)
+(********************** Forward references ********************************)
+(**************************************************************************)
+
+let translate_rte_annots_ref
+  : ((Format.formatter -> code_annotation -> unit) ->
+     code_annotation ->
+     kernel_function ->
+     Env.t ->
+     code_annotation list ->
+     Env.t) ref
+  =
+  ref (fun _pp _elt _kf _env _l ->
+      Extlib.mk_labeled_fun "translate_rte_annots_ref")
+
+let translate_rte_exp_ref
+  : (?filter:(code_annotation -> bool) ->
+     kernel_function ->
+     Env.t ->
+     exp ->
+     Env.t) ref
+  =
+  ref (fun ?filter:_ _kf _env _e ->
+      Extlib.mk_labeled_fun "translate_rte_exp_ref")
+
+(* ************************************************************************** *)
+(* Transforming predicates into C expressions (if any) *)
+(* ************************************************************************** *)
+
+let relation_to_binop = function
+  | Rlt -> Lt
+  | Rgt -> Gt
+  | Rle -> Le
+  | Rge -> Ge
+  | Req -> Eq
+  | Rneq -> Ne
+
+(* Convert an ACSL predicate into a corresponding C expression (if any) in the
+   given environment. Also extend this environment which includes the generating
+   constructs. *)
+let rec predicate_content_to_exp ~adata ?name kf env p =
+  let loc = p.pred_loc in
+  let lenv = Env.Local_vars.get env in
+  Cil.CurrentLoc.set loc;
+  match p.pred_content with
+  | Pfalse -> Cil.zero ~loc, adata, env
+  | Ptrue -> Cil.one ~loc, adata, env
+  | Papp (_, _::_,_) -> Env.not_yet env "predicates with labels"
+  | Papp (li, [], args) ->
+    let e, adata, env =
+      Logic_functions.app_to_exp ~adata ~loc kf env li args in
+    let adata, env = Assert.register_pred ~loc kf env p e adata in
+    e, adata, env
+  | Pdangling _ -> Env.not_yet env "\\dangling"
+  | Pobject_pointer _ -> Env.not_yet env "\\object_pointer"
+  | Pvalid_function _ -> Env.not_yet env "\\valid_function"
+  | Prel(rel, t1, t2) ->
+    let ity =
+      Typing.get_integer_op_of_predicate ~lenv p
+    in
+    Translate_utils.comparison_to_exp ~adata ~loc kf env ity (relation_to_binop rel) t1 t2 None
+  | Pand(p1, p2) ->
+    (* p1 && p2 <==> if p1 then p2 else false *)
+    Extlib.flatten
+      (Env.with_rte_and_result env true
+         ~f:(fun env ->
+             let e1, adata, env1 = predicate_to_exp ~adata kf env p1 in
+             let e2, adata, env2 =
+               predicate_to_exp ~adata kf (Env.push env1) p2 in
+             let res2 = e2, env2 in
+             let env3 = Env.push env2 in
+             let name = match name with None -> "and" | Some n -> n in
+             Extlib.nest
+               adata
+               (Translate_utils.conditional_to_exp
+                  ~name
+                  ~loc
+                  kf
+                  None
+                  e1
+                  res2
+                  (Cil.zero loc, env3))
+           ))
+  | Por(p1, p2) ->
+    (* p1 || p2 <==> if p1 then true else p2 *)
+    Extlib.flatten
+      (Env.with_rte_and_result env true
+         ~f:(fun env ->
+             let e1, adata, env1 = predicate_to_exp ~adata kf env p1 in
+             let env' = Env.push env1 in
+             let e2, adata, env2 =
+               predicate_to_exp ~adata kf (Env.push env') p2
+             in
+             let res2 = e2, env2 in
+             let name = match name with None -> "or" | Some n -> n in
+             Extlib.nest
+               adata
+               (Translate_utils.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 *)
+    predicate_to_exp
+      ~adata
+      ~name:"implies"
+      kf
+      env
+      (Logic_const.por ~loc ((Logic_const.pnot ~loc p1), p2))
+  | Piff(p1, p2) ->
+    (* (p1 <==> p2) <==> (p1 ==> p2 && p2 ==> p1) *)
+    predicate_to_exp
+      ~adata
+      ~name:"equiv"
+      kf
+      env
+      (Logic_const.pand ~loc
+         (Logic_const.pimplies ~loc (p1, p2),
+          Logic_const.pimplies ~loc (p2, p1)))
+  | Pnot p ->
+    let e, adata, env = predicate_to_exp ~adata kf env p in
+    Smart_exp.lnot ~loc e, adata, env
+  | Pif(t, p2, p3) ->
+    Extlib.flatten
+      (Env.with_rte_and_result env true
+         ~f:(fun env ->
+             let e1, adata, env1 = Translate_terms.term_to_exp ~adata kf env t in
+             let e2, adata, env2 =
+               predicate_to_exp ~adata kf (Env.push env1) p2 in
+             let res2 = e2, env2 in
+             let e3, adata, env3 =
+               predicate_to_exp ~adata kf (Env.push env2) p3
+             in
+             let res3 = e3, env3 in
+             Extlib.nest
+               adata
+               (Translate_utils.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
+    let adata, env = Translate_utils.env_of_li ~adata ~loc kf env li in
+    let e, adata, env = predicate_to_exp ~adata kf env p in
+    Interval.Env.remove li.l_var_info;
+    e, adata, env
+  | Pforall _ | Pexists _ ->
+    let e, env = Quantif.quantif_to_exp kf env p in
+    let adata, env = Assert.register_pred ~loc kf env p e adata in
+    e, adata, env
+  | Pat(p, BuiltinLabel Here) ->
+    predicate_to_exp ~adata kf env p
+  | Pat(p', label) ->
+    let lscope = Env.Logic_scope.get env in
+    let pot = Lscope.PoT_pred p' in
+    if Lscope.is_used lscope pot then
+      let e, env = At_with_lscope.to_exp ~loc kf env pot label in
+      let adata, env = Assert.register_pred ~loc kf env p e adata in
+      e, adata, env
+    else begin
+      (* convert [t'] to [e] in a separated local env *)
+      let e, adata, env = predicate_to_exp ~adata kf (Env.push env) p' in
+      let e, env, sty = Translate_utils.at_to_exp_no_lscope kf env None label e in
+      assert (sty = Typed_number.C_number);
+      let adata, env = Assert.register_pred ~loc kf env p e adata in
+      e, adata, env
+    end
+  | Pvalid_read(BuiltinLabel Here, t) as pc
+  | (Pvalid(BuiltinLabel Here, t) as pc) ->
+    let call_valid ~adata t p =
+      let name = match pc with
+        | Pvalid _ -> "valid"
+        | Pvalid_read _ -> "valid_read"
+        | _ -> assert false
+      in
+      let e, adata, env =
+        Memory_translate.call_valid ~adata ~loc kf name Cil.intType env t p
+      in
+      let adata, env = Assert.register_pred ~loc kf env p e adata in
+      e, adata, env
+    in
+    (* we already transformed \valid(t) into \initialized(&t) && \valid(t):
+       now convert this right-most valid. *)
+    call_valid ~adata t p
+  | Pvalid _ -> Env.not_yet env "labeled \\valid"
+  | Pvalid_read _ -> Env.not_yet env "labeled \\valid_read"
+  | Pseparated tlist ->
+    let env =
+      List.fold_left
+        (fun env t ->
+           let name = "separated_guard" in
+           let p = Logic_const.pvalid_read ~loc (BuiltinLabel Here, t) in
+           let p = { p with pred_name = name :: p.pred_name } in
+           let tp = Logic_const.toplevel_predicate ~kind:Assert p in
+           let annot = Logic_const.new_code_annotation (AAssert ([],tp)) in
+           Typing.preprocess_rte (Env.Local_vars.get env) annot;
+           !translate_rte_annots_ref Printer.pp_code_annotation annot kf env [annot]
+        )
+        env
+        tlist
+    in
+    let e, adata, env =
+      Memory_translate.call_with_size
+        ~adata
+        ~loc
+        kf
+        "separated"
+        Cil.intType
+        env
+        tlist
+        p
+    in
+    let adata, env = Assert.register_pred ~loc kf env p e adata in
+    e, adata, env
+  | Pinitialized(BuiltinLabel Here, t) ->
+    let e, adata, env =
+      (match t.term_node with
+       (* optimisation when we know that the initialisation is ok *)
+       | TAddrOf (TResult _, TNoOffset) -> Cil.one ~loc, adata, env
+       | TAddrOf (TVar { lv_origin = Some vi }, TNoOffset)
+         when
+           vi.vformal || vi.vglob || Functions.RTL.is_generated_name vi.vname ->
+         Cil.one ~loc, adata, env
+       | _ ->
+         let e, adata, env =
+           Memory_translate.call_with_size
+             ~adata
+             ~loc
+             kf
+             "initialized"
+             Cil.intType
+             env
+             [ t ]
+             p
+         in
+         let adata, env = Assert.register_pred ~loc kf env p e adata in
+         e, adata, env)
+    in
+    e, adata, env
+  | Pinitialized _ -> Env.not_yet env "labeled \\initialized"
+  | Pallocable _ -> Env.not_yet env "\\allocate"
+  | Pfreeable(BuiltinLabel Here, t) ->
+    let e, adata, env =
+      Memory_translate.call ~adata ~loc kf "freeable" Cil.intType env t
+    in
+    let adata, env = Assert.register_pred ~loc kf env p e adata in
+    e, adata, env
+  | Pfreeable _ -> Env.not_yet env "labeled \\freeable"
+  | Pfresh _ -> Env.not_yet env "\\fresh"
+
+and predicate_to_exp ~adata ?name kf ?rte env p =
+  match Logic_normalizer.get_pred p with
+  | PoT_term t -> Translate_terms.term_to_exp ~adata kf env t
+  | 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
+         ~f:(fun env ->
+             let e, adata, env =
+               predicate_content_to_exp ~adata ?name kf env p
+             in
+             let env = if rte then !translate_rte_exp_ref kf env e else env in
+             let cast =
+               Typing.get_cast_of_predicate
+                 ~lenv:(Env.Local_vars.get env)
+                 p
+             in
+             Extlib.nest
+               adata
+               (Typed_number.add_cast
+                  ~loc:p.pred_loc
+                  ?name
+                  env
+                  kf
+                  cast
+                  Typed_number.C_number
+                  None
+                  e)
+           ))
+
+let generalized_untyped_predicate_to_exp ~adata ?name kf ?rte env p =
+  (* If [rte] is true, it means we're translating the root predicate of an
+     assertion and we need to generate the RTE for it. The typing environment
+     must be cleared. Otherwise, if [rte] is false, it means we're already
+     translating RTE predicates as part of the translation of another root
+     predicate, and the typing environment must be kept. *)
+  let rte = match rte with None -> Env.generate_rte env | Some b -> b in
+  let e, adata, env = predicate_to_exp ~adata ?name kf ~rte env p in
+  assert (Typ.equal (Cil.typeOf e) Cil.intType);
+  let env = Env.Logic_scope.reset env in
+  e, adata, env
+
+let translate_predicate ?pred_to_print kf env p =
+  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 adata, env = Assert.empty ~loc:p.tp_statement.pred_loc kf env in
+    let e, adata, env =
+      generalized_untyped_predicate_to_exp ~adata kf env p.tp_statement
+    in
+    let stmt, env =
+      Assert.runtime_check
+        ~adata
+        ~pred_kind:p.tp_kind
+        (Env.annotation_kind env)
+        kf
+        env
+        e
+        pred_to_print
+    in
+    Env.add_stmt
+      env
+      kf
+      stmt
+  | Admit -> env
+
+let predicate_to_exp_without_rte ~adata kf env p =
+  (* forget optional argument ?rte and ?name*)
+  predicate_to_exp ~adata kf env p
+
+let () =
+  Translate_utils.predicate_to_exp_ref := predicate_to_exp;
+  Loops.translate_predicate_ref := translate_predicate;
+  Loops.predicate_to_exp_ref := predicate_to_exp_without_rte;
+  Quantif.predicate_to_exp_ref := predicate_to_exp_without_rte;
+  At_with_lscope.predicate_to_exp_ref := predicate_to_exp_without_rte;
+  Memory_translate.predicate_to_exp_ref := predicate_to_exp_without_rte;
+  Logic_functions.predicate_to_exp_ref := predicate_to_exp_without_rte
+
+exception No_simple_predicate_translation of predicate
+
+(* This function is used by Guillaume.
+   However, it is correct to use it only in specific contexts. *)
+let untyped_predicate_to_exp p =
+  let env = Env.push Env.empty in
+  let env = Env.rte env false in
+  let e, _, env =
+    try generalized_untyped_predicate_to_exp
+          ~adata:Assert.no_data
+          (Kernel_function.dummy ())
+          env
+          p
+    with Rtl.Symbols.Unregistered _ -> raise (No_simple_predicate_translation p)
+  in
+  if not (Env.has_no_new_stmt env)
+  then raise (No_simple_predicate_translation p);
+  e
+
+(*
+Local Variables:
+compile-command: "make -C ../../../../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/code_generator/translate.mli b/src/plugins/e-acsl/src/code_generator/translate_predicates.mli
similarity index 68%
rename from src/plugins/e-acsl/src/code_generator/translate.mli
rename to src/plugins/e-acsl/src/code_generator/translate_predicates.mli
index ea9ff115508..8bdae9d2b9e 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.mli
+++ b/src/plugins/e-acsl/src/code_generator/translate_predicates.mli
@@ -22,7 +22,7 @@
 
 open Cil_types
 
-(** Generate C implementations of E-ACSL predicates and terms. *)
+(** Generate C implementations of E-ACSL predicates. *)
 
 val predicate_to_exp:
   adata:Assert.t ->
@@ -54,56 +54,33 @@ val translate_predicate:
     If [pred_to_print] is set, then the runtime check will use this predicate as
     message. *)
 
-val term_to_exp:
-  adata:Assert.t ->
-  kernel_function ->
-  Env.t ->
-  term ->
-  exp * Assert.t * Env.t
-(** Convert an ACSL term into a corresponding C expression. *)
-
-val translate_rte_annots:
-  (Format.formatter -> 'a -> unit) ->
-  'a ->
-  kernel_function ->
-  Env.t ->
-  code_annotation list ->
-  Env.t
-(** Translate the given RTE annotations into runtime checks in the given
-    environment. *)
-
-val gmp_to_sizet:
-  adata:Assert.t ->
-  loc:location ->
-  name:string ->
-  ?check_lower_bound:bool ->
-  ?pp:term ->
-  kernel_function ->
-  Env.t ->
-  term ->
-  exp * Assert.t * Env.t
-(** Translate the given GMP integer to an expression of type [size_t]. RTE
-    checks are generated to ensure that the GMP value holds in this type.
-    The parameter [name] is used to generate relevant predicate names.
-    If [check_lower_bound] is set to [false], then the GMP value is assumed to
-    be positive.
-    If [pp] is provided, this term is used in the messages of the RTE checks. *)
-
-exception No_simple_term_translation of term
-(** Exceptin raised if [untyped_term_to_exp] would generate new statements in
-    the environment *)
-
 exception No_simple_predicate_translation of predicate
 (** Exceptin raised if [untyped_predicate_to_exp] would generate new statements
     in the environment *)
 
-val untyped_term_to_exp: typ option -> term -> exp
-(** Convert an untyped ACSL term into a corresponding C expression. *)
-
 val untyped_predicate_to_exp: predicate -> exp
 (** Convert an untyped ACSL predicate into a corresponding C expression. This
     expression is valid only in certain contexts and shouldn't be used. *)
 
+(**************************************************************************)
+(********************** Forward references ********************************)
+(**************************************************************************)
+
+val translate_rte_annots_ref:
+  ((Format.formatter -> code_annotation -> unit) ->
+   code_annotation ->
+   kernel_function ->
+   Env.t ->
+   code_annotation list ->
+   Env.t) ref
+
+val translate_rte_exp_ref:
+  (?filter:(code_annotation -> bool) ->
+   kernel_function ->
+   Env.t ->
+   exp ->
+   Env.t) ref
+
 (*
 Local Variables:
 compile-command: "make -C ../../../../.."
diff --git a/src/plugins/e-acsl/src/code_generator/translate_rtes.ml b/src/plugins/e-acsl/src/code_generator/translate_rtes.ml
new file mode 100644
index 00000000000..59be7b215c3
--- /dev/null
+++ b/src/plugins/e-acsl/src/code_generator/translate_rtes.ml
@@ -0,0 +1,79 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
+(*                                                                        *)
+(*  Copyright (C) 2012-2021                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+(** Generate and translate RTE annotations. *)
+
+open Cil_types
+let dkey = Options.dkey_translation
+
+let translate_rte_annots pp elt kf env l =
+  let old_kind = Env.annotation_kind env in
+  let env = Env.set_annotation_kind env Smart_stmt.RTE in
+  let env =
+    List.fold_left
+      (fun env a -> match a.annot_content with
+         | AAssert(_, p) ->
+           Env.handle_error
+             (fun env ->
+                Options.feedback ~dkey ~level:4 "prevent RTE from %a" pp elt;
+                (* The logic scope MUST NOT be reset here since we still might
+                   be in the middle of the translation of the original
+                   predicate. *)
+                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
+                    ~f:(fun env -> Translate_predicates.translate_predicate kf env p)
+                in
+                let env = Env.Logic_scope.set_reset env lscope_reset_old in
+                env)
+             env
+         | _ -> assert false)
+      env
+      l
+  in
+  Env.set_annotation_kind env old_kind
+
+let () =
+  Translate_predicates.translate_rte_annots_ref := translate_rte_annots
+
+let translate_rte ?filter kf env e =
+  let stmt = Cil.mkStmtOneInstr ~valid_sid:true (Skip e.eloc) in
+  let l = Rte.exp kf stmt e in
+  let l =
+    match filter with
+    | Some f -> List.filter f l
+    | None -> l
+  in
+  List.iter (Typing.preprocess_rte ~lenv:(Env.Local_vars.get env)) l;
+  translate_rte_annots Printer.pp_exp e kf env l
+
+let () =
+  Translate_terms.translate_rte_exp_ref := translate_rte;
+  Translate_predicates.translate_rte_exp_ref := translate_rte;
+  Logic_array.translate_rte_ref := translate_rte
+
+(*
+Local Variables:
+compile-command: "make -C ../../../../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/code_generator/translate_rtes.mli b/src/plugins/e-acsl/src/code_generator/translate_rtes.mli
new file mode 100644
index 00000000000..8934e503dcb
--- /dev/null
+++ b/src/plugins/e-acsl/src/code_generator/translate_rtes.mli
@@ -0,0 +1,45 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
+(*                                                                        *)
+(*  Copyright (C) 2012-2021                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Cil_types
+
+(** Generate and translate RTE annotations. *)
+
+val translate_rte_annots:
+  (Format.formatter -> 'a -> unit) ->
+  'a ->
+  kernel_function ->
+  Env.t ->
+  code_annotation list ->
+  Env.t
+(** Translate the given RTE annotations into runtime checks in the given
+    environment. *)
+
+val translate_rte: ?filter:(code_annotation -> bool) -> kernel_function -> Env.t -> exp -> Env.t
+(** Generate RTE annotations from the given expression and translate them in the
+    given environment. *)
+
+(*
+Local Variables:
+compile-command: "make -C ../../../../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
similarity index 60%
rename from src/plugins/e-acsl/src/code_generator/translate.ml
rename to src/plugins/e-acsl/src/code_generator/translate_terms.ml
index 4a67b008be3..e403fc6441e 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
@@ -20,25 +20,29 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(** Generate C implementations of E-ACSL predicates and terms. *)
+(** Generate C implementations of E-ACSL terms. *)
 
-module E_acsl_label = Label
 open Cil_types
-open Cil_datatype
 let dkey = Options.dkey_translation
 
+(**************************************************************************)
+(********************** Forward references ********************************)
+(**************************************************************************)
+
+let translate_rte_exp_ref
+  : (?filter:(code_annotation -> bool) ->
+     kernel_function ->
+     Env.t ->
+     exp ->
+     Env.t) ref
+  =
+  ref (fun ?filter:_ _kf _env _e ->
+      Extlib.mk_labeled_fun "translate_rte_exp_ref")
+
 (* ************************************************************************** *)
-(* Transforming terms and predicates into C expressions (if any) *)
+(* Transforming terms into C expressions (if any) *)
 (* ************************************************************************** *)
 
-let relation_to_binop = function
-  | Rlt -> Lt
-  | Rgt -> Gt
-  | Rle -> Le
-  | Rge -> Ge
-  | Req -> Eq
-  | Rneq -> Ne
-
 let constant_to_exp ~loc env t c =
   let lenv = Env.Local_vars.get env in
   let mk_real s =
@@ -82,46 +86,6 @@ let constant_to_exp ~loc env t c =
     else mk_real lr.r_literal
   | LEnum e -> Cil.new_exp ~loc (Const (CEnum e)), Typed_number.C_number
 
-let conditional_to_exp ?(name="if") loc kf t_opt e1 (e2, env2) (e3, env3) =
-  let env = Env.pop (Env.pop env3) in
-  match e1.enode with
-  | Const(CInt64(n, _, _)) when Integer.is_zero n ->
-    e3, Env.transfer ~from:env3 env
-  | Const(CInt64(n, _, _)) when Integer.is_one n ->
-    e2, Env.transfer ~from:env2 env
-  | _ ->
-    let ty = match t_opt with
-      | None (* predicate *) -> Cil.intType
-      | Some t -> Typing.get_typ ~lenv:(Env.Local_vars.get env) t
-    in
-    let _, e, env =
-      Env.new_var
-        ~loc
-        ~name
-        env
-        kf
-        t_opt
-        ty
-        (fun v ev ->
-           let lv = Cil.var v in
-           let ty = Cil.typeOf ev in
-           let init_set =
-             assert (not (Gmp_types.Q.is_t ty));
-             Gmp.init_set
-           in
-           let affect e = init_set ~loc lv ev e in
-           let then_blk, _ =
-             let s = affect e2 in
-             Env.pop_and_get env2 s ~global_clear:false Env.Middle
-           in
-           let else_blk, _ =
-             let s = affect e3 in
-             Env.pop_and_get env3 s ~global_clear:false Env.Middle
-           in
-           [ Smart_stmt.if_stmt ~loc ~cond:e1 then_blk ~else_blk ])
-    in
-    e, env
-
 (* Create and initialize a variable in the [env] according to [ty], [name] and [exp_init],
    return a tuple [varinfo * exp] and the [env] extended with the new variable. *)
 let create_and_init_var ~loc kf ty name exp_init env =
@@ -360,7 +324,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
       let ctx = Typing.get_number_ty ~lenv t in
       Typing.type_term ~use_gmp_opt:true ~ctx ~lenv zero;
       let e, adata, env =
-        comparison_to_exp
+        Translate_utils.comparison_to_exp
           ~adata
           kf
           ~loc
@@ -426,7 +390,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
       (* do not generate [e2] from [t2] twice *)
       let guard, _, env =
         let name = Misc.name_of_binop bop ^ "_guard" in
-        comparison_to_exp
+        Translate_utils.comparison_to_exp
           ~adata:Assert.no_data ~loc kf env Typing.gmpz ~e1:e2 ~name Ne t2 zero t
       in
       let p = Logic_const.prel ~loc (Rneq, t2, zero) in
@@ -464,7 +428,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
     (* comparison operators *)
     let ity = Typing.get_integer_op ~lenv t in
     let e, adata, env =
-      comparison_to_exp ~adata ~loc kf env ity bop t1 t2 (Some t)
+      Translate_utils.comparison_to_exp ~adata ~loc kf env ity bop t1 t2 (Some t)
     in
     e, adata, env, Typed_number.C_number, ""
   | TBinOp((Shiftlt | Shiftrt) as bop, t1, t2) ->
@@ -576,7 +540,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
           [ result_e; e1; e2_as_bitcnt_e ]
       in
 
-      (* Put t in an option to use with comparison_to_exp and
+      (* Put t in an option to use with Translate_utils.comparison_to_exp and
          Env.new_var_and_mpz_init *)
       let t = Some t in
 
@@ -599,7 +563,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
              then check e1 >= 0 *)
           let e1_guard, _, env =
             let name = e1_name ^ bop_name ^ "_guard" in
-            comparison_to_exp
+            Translate_utils.comparison_to_exp
               ~adata:Assert.no_data
               ~loc
               kf
@@ -665,8 +629,8 @@ and context_insensitive_term_to_exp ~adata kf env t =
                let res2 = e2, env2 in
                Extlib.nest
                  adata
-                 (conditional_to_exp
-                    ~name:"or" loc kf (Some t) e1 (Cil.one loc, env') res2)
+                 (Translate_utils.conditional_to_exp
+                    ~name:"or" ~loc kf (Some t) e1 (Cil.one loc, env') res2)
              ))
     in
     e, adata, env, Typed_number.C_number, ""
@@ -684,8 +648,8 @@ and context_insensitive_term_to_exp ~adata kf env t =
                let env3 = Env.push env2 in
                Extlib.nest
                  adata
-                 (conditional_to_exp
-                    ~name:"and" loc kf (Some t) e1 res2 (Cil.zero loc, env3))
+                 (Translate_utils.conditional_to_exp
+                    ~name:"and" ~loc kf (Some t) e1 res2 (Cil.zero loc, env3))
              ))
     in
     e, adata, env, Typed_number.C_number, ""
@@ -797,7 +761,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
                let res3 = e3, env3 in
                Extlib.nest
                  adata
-                 (conditional_to_exp loc kf (Some t) e1 res2 res3)
+                 (Translate_utils.conditional_to_exp ~loc kf (Some t) e1 res2 res3)
              ))
     in
     e, adata, env, Typed_number.C_number, ""
@@ -813,7 +777,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
       e, adata, env, Typed_number.C_number, ""
     else
       let e, _, env = term_to_exp ~adata:Assert.no_data kf (Env.push env) t' in
-      let e, env, sty = at_to_exp_no_lscope env kf (Some t) label e in
+      let e, env, sty = Translate_utils.at_to_exp_no_lscope kf env (Some t) label e in
       let adata, env = Assert.register_term ~loc kf env t e adata in
       e, adata, env, sty, ""
   | Tbase_addr(BuiltinLabel Here, t') ->
@@ -863,7 +827,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
   | Tlet(li, t) ->
     let lvs = Lscope.Lvs_let(li.l_var_info, Misc.term_of_li li) in
     let env = Env.Logic_scope.extend env lvs in
-    let adata, env = env_of_li ~adata li kf env loc in
+    let adata, env = Translate_utils.env_of_li ~adata ~loc kf env li in
     let e, adata, env = term_to_exp ~adata kf env t in
     Interval.Env.remove li.l_var_info;
     e, adata, env, Typed_number.C_number, ""
@@ -884,7 +848,7 @@ and term_to_exp ~adata kf env t =
            let e, adata, env, sty, name =
              context_insensitive_term_to_exp ~adata kf env t
            in
-           let env = if generate_rte then translate_rte kf env e else env in
+           let env = if generate_rte then !translate_rte_exp_ref kf env e else env in
            let cast = Typing.get_cast ~lenv:(Env.Local_vars.get env) t in
            let name = if name = "" then None else Some name in
            Extlib.nest
@@ -900,604 +864,14 @@ and term_to_exp ~adata kf env t =
                 e)
          ))
 
-(* generate the C code equivalent to [t1 bop t2]. *)
-and comparison_to_exp
-    ~adata
-    ~loc
-    ?e1
-    kf
-    env
-    ity
-    bop
-    ?(name = Misc.name_of_binop bop)
-    t1
-    t2
-    t_opt
-  =
-  let e1, adata, env =
-    match e1 with
-    | None ->
-      let e1, adata, env = term_to_exp ~adata kf env t1 in
-      e1, adata, env
-    | Some e1 ->
-      e1, adata, env
-  in
-  let ty1 = Cil.typeOf e1 in
-  let e2, adata, env = term_to_exp ~adata kf env t2 in
-  let ty2 = Cil.typeOf e2 in
-  let e, env =
-    match Logic_aggr.get_t ty1, Logic_aggr.get_t ty2 with
-    | Logic_aggr.Array, Logic_aggr.Array ->
-      Logic_array.comparison_to_exp
-        ~loc
-        kf
-        env
-        ~name
-        bop
-        e1
-        e2
-    | Logic_aggr.StructOrUnion, Logic_aggr.StructOrUnion ->
-      Env.not_yet env "comparison between two structs or unions"
-    | Logic_aggr.NotAggregate, Logic_aggr.NotAggregate -> begin
-        match ity with
-        | Typing.C_integer _ | Typing.C_float _ | Typing.Nan ->
-          Cil.mkBinOp ~loc bop e1 e2, env
-        | Typing.Gmpz ->
-          let _, e, env = Env.new_var
-              ~loc
-              env
-              kf
-              t_opt
-              ~name
-              Cil.intType
-              (fun v _ ->
-                 [ Smart_stmt.rtl_call ~loc
-                     ~result:(Cil.var v)
-                     ~prefix:""
-                     "__gmpz_cmp"
-                     [ e1; e2 ] ])
-          in
-          Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env
-        | Typing.Rational ->
-          Rational.cmp ~loc bop e1 e2 env kf t_opt
-        | Typing.Real ->
-          Error.not_yet "comparison involving real numbers"
-      end
-    | _, _ ->
-      Options.fatal
-        ~current:true
-        "Comparison involving incompatible types: '%a' and '%a'"
-        Printer.pp_typ ty1
-        Printer.pp_typ ty2
-  in
-  e, adata, env
-
-and at_to_exp_no_lscope env kf t_opt label e =
-  let stmt = E_acsl_label.get_stmt kf label in
-  (* generate a new variable denoting [\at(t',label)].
-     That is this variable which is the resulting expression.
-     ACSL typing rule ensures that the type of this variable is the same as
-     the one of [e]. *)
-  let loc = Stmt.loc stmt in
-  let res_v, res, new_env =
-    Env.new_var
-      ~loc
-      ~name:"at"
-      ~scope:Varname.Function
-      env
-      kf
-      t_opt
-      (Cil.typeOf e)
-      (fun _ _ -> [])
-  in
-  let env_ref = ref new_env in
-  (* visitor modifying in place the labeled statement in order to store [e]
-     in the resulting variable at this location (which is the only correct
-     one). *)
-  let o = object
-    inherit Visitor.frama_c_inplace
-    method !vstmt_aux stmt =
-      (* either a standard C affectation or a call to an initializer according
-         to the type of [e] *)
-      let ty = Cil.typeOf e in
-      let init_set =
-        if Gmp_types.Q.is_t ty then Rational.init_set else Gmp.init_set
-      in
-      let new_stmt = init_set ~loc (Cil.var res_v) res e in
-      assert (!env_ref == new_env);
-      (* generate the new block of code for the labeled statement and the
-         corresponding environment *)
-      let block, new_env =
-        Env.pop_and_get new_env new_stmt ~global_clear:false Env.Middle
-      in
-      env_ref := Env.extend_stmt_in_place new_env stmt ~label block;
-      Cil.ChangeTo stmt
-  end
-  in
-  ignore (Visitor.visitFramacStmt o stmt);
-  res, !env_ref, Typed_number.C_number
-
-and env_of_li ~adata li kf env loc =
-  match li.l_var_info.lv_type with
-  | Ctype _ | Linteger | Lreal ->
-    let t = Misc.term_of_li li in
-    let lenv = Env.Local_vars.get env in
-    let ty = Typing.get_typ ~lenv t in
-    let vi, vi_e, env = Env.Logic_binding.add ~ty env kf li.l_var_info in
-    let e, adata, env = term_to_exp ~adata kf env t in
-    let stmt = match Typing.get_number_ty ~lenv t with
-      | Typing.(C_integer _ | C_float _ | Nan) ->
-        Smart_stmt.assigns ~loc ~result:(Cil.var vi) e
-      | Typing.Gmpz ->
-        Gmp.init_set ~loc (Cil.var vi) vi_e e
-      | Typing.Rational ->
-        Rational.init_set ~loc (Cil.var vi) vi_e e
-      | Typing.Real ->
-        Error.not_yet "real number"
-    in
-    adata, Env.add_stmt env kf stmt
-  | Ltype _ ->
-    Env.not_yet env "user-defined logic type"
-  | Lvar _ ->
-    Env.not_yet env "type variable"
-  | Larrow _ ->
-    Env.not_yet env "lambda-abstraction"
-
-(* Convert an ACSL predicate into a corresponding C expression (if any) in the
-   given environment. Also extend this environment which includes the generating
-   constructs. *)
-and predicate_content_to_exp ~adata ?name kf env p =
-  let loc = p.pred_loc in
-  let lenv = Env.Local_vars.get env in
-  Cil.CurrentLoc.set loc;
-  match p.pred_content with
-  | Pfalse -> Cil.zero ~loc, adata, env
-  | Ptrue -> Cil.one ~loc, adata, env
-  | Papp (_, _::_,_) -> Env.not_yet env "predicates with labels"
-  | Papp (li, [], args) ->
-    let e, adata, env =
-      Logic_functions.app_to_exp ~adata ~loc kf env li args in
-    let adata, env = Assert.register_pred ~loc kf env p e adata in
-    e, adata, env
-  | Pdangling _ -> Env.not_yet env "\\dangling"
-  | Pobject_pointer _ -> Env.not_yet env "\\object_pointer"
-  | Pvalid_function _ -> Env.not_yet env "\\valid_function"
-  | Prel(rel, t1, t2) ->
-    let ity =
-      Typing.get_integer_op_of_predicate ~lenv p
-    in
-    comparison_to_exp ~adata ~loc kf env ity (relation_to_binop rel) t1 t2 None
-  | Pand(p1, p2) ->
-    (* p1 && p2 <==> if p1 then p2 else false *)
-    Extlib.flatten
-      (Env.with_rte_and_result env true
-         ~f:(fun env ->
-             let e1, adata, env1 = predicate_to_exp ~adata kf env p1 in
-             let e2, adata, env2 =
-               predicate_to_exp ~adata kf (Env.push env1) p2 in
-             let res2 = e2, env2 in
-             let env3 = Env.push env2 in
-             let name = match name with None -> "and" | Some n -> n in
-             Extlib.nest
-               adata
-               (conditional_to_exp
-                  ~name
-                  loc
-                  kf
-                  None
-                  e1
-                  res2
-                  (Cil.zero loc, env3))
-           ))
-  | Por(p1, p2) ->
-    (* p1 || p2 <==> if p1 then true else p2 *)
-    Extlib.flatten
-      (Env.with_rte_and_result env true
-         ~f:(fun env ->
-             let e1, adata, env1 = predicate_to_exp ~adata kf env p1 in
-             let env' = Env.push env1 in
-             let e2, adata, env2 =
-               predicate_to_exp ~adata kf (Env.push env') p2
-             in
-             let res2 = e2, env2 in
-             let name = match name with None -> "or" | Some n -> n in
-             Extlib.nest
-               adata
-               (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 *)
-    predicate_to_exp
-      ~adata
-      ~name:"implies"
-      kf
-      env
-      (Logic_const.por ~loc ((Logic_const.pnot ~loc p1), p2))
-  | Piff(p1, p2) ->
-    (* (p1 <==> p2) <==> (p1 ==> p2 && p2 ==> p1) *)
-    predicate_to_exp
-      ~adata
-      ~name:"equiv"
-      kf
-      env
-      (Logic_const.pand ~loc
-         (Logic_const.pimplies ~loc (p1, p2),
-          Logic_const.pimplies ~loc (p2, p1)))
-  | Pnot p ->
-    let e, adata, env = predicate_to_exp ~adata kf env p in
-    Smart_exp.lnot ~loc e, adata, env
-  | Pif(t, p2, p3) ->
-    Extlib.flatten
-      (Env.with_rte_and_result env true
-         ~f:(fun env ->
-             let e1, adata, env1 = term_to_exp ~adata kf env t in
-             let e2, adata, env2 =
-               predicate_to_exp ~adata kf (Env.push env1) p2 in
-             let res2 = e2, env2 in
-             let e3, adata, env3 =
-               predicate_to_exp ~adata kf (Env.push env2) p3
-             in
-             let res3 = e3, env3 in
-             Extlib.nest
-               adata
-               (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
-    let adata, env = env_of_li ~adata li kf env loc in
-    let e, adata, env = predicate_to_exp ~adata kf env p in
-    Interval.Env.remove li.l_var_info;
-    e, adata, env
-  | Pforall _ | Pexists _ ->
-    let e, env = Quantif.quantif_to_exp kf env p in
-    let adata, env = Assert.register_pred ~loc kf env p e adata in
-    e, adata, env
-  | Pat(p, BuiltinLabel Here) ->
-    predicate_to_exp ~adata kf env p
-  | Pat(p', label) ->
-    let lscope = Env.Logic_scope.get env in
-    let pot = Lscope.PoT_pred p' in
-    if Lscope.is_used lscope pot then
-      let e, env = At_with_lscope.to_exp ~loc kf env pot label in
-      let adata, env = Assert.register_pred ~loc kf env p e adata in
-      e, adata, env
-    else begin
-      (* convert [t'] to [e] in a separated local env *)
-      let e, adata, env = predicate_to_exp ~adata kf (Env.push env) p' in
-      let e, env, sty = at_to_exp_no_lscope env kf None label e in
-      assert (sty = Typed_number.C_number);
-      let adata, env = Assert.register_pred ~loc kf env p e adata in
-      e, adata, env
-    end
-  | Pvalid_read(BuiltinLabel Here, t) as pc
-  | (Pvalid(BuiltinLabel Here, t) as pc) ->
-    let call_valid ~adata t p =
-      let name = match pc with
-        | Pvalid _ -> "valid"
-        | Pvalid_read _ -> "valid_read"
-        | _ -> assert false
-      in
-      let e, adata, env =
-        Memory_translate.call_valid ~adata ~loc kf name Cil.intType env t p
-      in
-      let adata, env = Assert.register_pred ~loc kf env p e adata in
-      e, adata, env
-    in
-    (* we already transformed \valid(t) into \initialized(&t) && \valid(t):
-       now convert this right-most valid. *)
-    call_valid ~adata t p
-  | Pvalid _ -> Env.not_yet env "labeled \\valid"
-  | Pvalid_read _ -> Env.not_yet env "labeled \\valid_read"
-  | Pseparated tlist ->
-    let env =
-      List.fold_left
-        (fun env t ->
-           let name = "separated_guard" in
-           let p = Logic_const.pvalid_read ~loc (BuiltinLabel Here, t) in
-           let p = { p with pred_name = name :: p.pred_name } in
-           let tp = Logic_const.toplevel_predicate ~kind:Assert p in
-           let annot = Logic_const.new_code_annotation (AAssert ([],tp)) in
-           Typing.preprocess_rte (Env.Local_vars.get env) annot;
-           translate_rte_annots Printer.pp_code_annotation annot kf env [annot]
-        )
-        env
-        tlist
-    in
-    let e, adata, env =
-      Memory_translate.call_with_size
-        ~adata
-        ~loc
-        kf
-        "separated"
-        Cil.intType
-        env
-        tlist
-        p
-    in
-    let adata, env = Assert.register_pred ~loc kf env p e adata in
-    e, adata, env
-  | Pinitialized(BuiltinLabel Here, t) ->
-    let e, adata, env =
-      (match t.term_node with
-       (* optimisation when we know that the initialisation is ok *)
-       | TAddrOf (TResult _, TNoOffset) -> Cil.one ~loc, adata, env
-       | TAddrOf (TVar { lv_origin = Some vi }, TNoOffset)
-         when
-           vi.vformal || vi.vglob || Functions.RTL.is_generated_name vi.vname ->
-         Cil.one ~loc, adata, env
-       | _ ->
-         let e, adata, env =
-           Memory_translate.call_with_size
-             ~adata
-             ~loc
-             kf
-             "initialized"
-             Cil.intType
-             env
-             [ t ]
-             p
-         in
-         let adata, env = Assert.register_pred ~loc kf env p e adata in
-         e, adata, env)
-    in
-    e, adata, env
-  | Pinitialized _ -> Env.not_yet env "labeled \\initialized"
-  | Pallocable _ -> Env.not_yet env "\\allocate"
-  | Pfreeable(BuiltinLabel Here, t) ->
-    let e, adata, env =
-      Memory_translate.call ~adata ~loc kf "freeable" Cil.intType env t
-    in
-    let adata, env = Assert.register_pred ~loc kf env p e adata in
-    e, adata, env
-  | Pfreeable _ -> Env.not_yet env "labeled \\freeable"
-  | Pfresh _ -> Env.not_yet env "\\fresh"
-
-and predicate_to_exp ~adata ?name kf ?rte env p =
-  match Logic_normalizer.get_pred p with
-  | PoT_term t -> term_to_exp ~adata kf env t
-  | 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
-         ~f:(fun env ->
-             let e, adata, env =
-               predicate_content_to_exp ~adata ?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
-                 ~lenv:(Env.Local_vars.get env)
-                 p
-             in
-             Extlib.nest
-               adata
-               (Typed_number.add_cast
-                  ~loc:p.pred_loc
-                  ?name
-                  env
-                  kf
-                  cast
-                  Typed_number.C_number
-                  None
-                  e)
-           ))
-
-and generalized_untyped_predicate_to_exp ~adata ?name kf ?rte env p =
-  (* If [rte] is true, it means we're translating the root predicate of an
-     assertion and we need to generate the RTE for it. The typing environment
-     must be cleared. Otherwise, if [rte] is false, it means we're already
-     translating RTE predicates as part of the translation of another root
-     predicate, and the typing environment must be kept. *)
-  let rte = match rte with None -> Env.generate_rte env | Some b -> b in
-  let e, adata, env = predicate_to_exp ~adata ?name kf ~rte env p in
-  assert (Typ.equal (Cil.typeOf e) Cil.intType);
-  let env = Env.Logic_scope.reset env in
-  e, adata, env
-
-and translate_rte_annots:
-  'a. (Format.formatter -> 'a -> unit) -> 'a ->
-  kernel_function -> Env.t -> code_annotation list -> Env.t =
-  fun pp elt kf env l ->
-  let old_kind = Env.annotation_kind env in
-  let env = Env.set_annotation_kind env Smart_stmt.RTE in
-  let env =
-    List.fold_left
-      (fun env a -> match a.annot_content with
-         | AAssert(_, p) ->
-           Env.handle_error
-             (fun env ->
-                Options.feedback ~dkey ~level:4 "prevent RTE from %a" pp elt;
-                (* The logic scope MUST NOT be reset here since we still might
-                   be in the middle of the translation of the original
-                   predicate. *)
-                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
-                    ~f:(fun env -> translate_predicate kf env p)
-                in
-                let env = Env.Logic_scope.set_reset env lscope_reset_old in
-                env)
-             env
-         | _ -> assert false)
-      env
-      l
-  in
-  Env.set_annotation_kind env old_kind
-
-and translate_rte ?filter kf env e =
-  let stmt = Cil.mkStmtOneInstr ~valid_sid:true (Skip e.eloc) in
-  let l = Rte.exp kf stmt e in
-  let l =
-    match filter with
-    | Some f -> List.filter f l
-    | None -> l
-  in
-  List.iter (Typing.preprocess_rte ~lenv:(Env.Local_vars.get env)) l;
-  translate_rte_annots Printer.pp_exp e kf env l
-
-and translate_predicate ?pred_to_print kf env p =
-  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 adata, env = Assert.empty ~loc:p.tp_statement.pred_loc kf env in
-    let e, adata, env =
-      generalized_untyped_predicate_to_exp ~adata kf env p.tp_statement
-    in
-    let stmt, env =
-      Assert.runtime_check
-        ~adata
-        ~pred_kind:p.tp_kind
-        (Env.annotation_kind env)
-        kf
-        env
-        e
-        pred_to_print
-    in
-    Env.add_stmt
-      env
-      kf
-      stmt
-  | Admit -> env
-
-let predicate_to_exp_without_rte ~adata kf env p =
-  (* forget optional argument ?rte and ?name*)
-  predicate_to_exp ~adata kf env p
-
-let gmp_to_sizet ~adata ~loc ~name ?(check_lower_bound=true) ?pp kf env t =
-  let lenv = Env.Local_vars.get env in
-  let pp = match pp with Some size_pp -> size_pp | None -> t in
-  let sizet = Cil.(theMachine.typeOfSizeOf) in
-  let stmts = [] in
-  (* Lower guard *)
-  let stmts, env =
-    if check_lower_bound then begin
-      let zero_term = Cil.lzero ~loc () in
-      let pred_name = Format.sprintf "%s_greater_or_eq_than_0" name in
-      let lower_guard_pp = Logic_const.prel ~loc (Rge, pp, zero_term) in
-      let lower_guard_pp =
-        { lower_guard_pp with
-          pred_name = pred_name :: lower_guard_pp.pred_name }
-      in
-      let lower_guard = Logic_const.prel ~loc (Rge, t, zero_term) in
-      Typing.type_named_predicate ~lenv lower_guard;
-      let adata_lower_guard, env = Assert.empty ~loc kf env in
-      let lower_guard, adata_lower_guard, env =
-        predicate_to_exp ~adata:adata_lower_guard kf env lower_guard
-      in
-      let assertion, env =
-        Assert.runtime_check
-          ~adata:adata_lower_guard
-          ~pred_kind:Assert
-          Smart_stmt.RTE
-          kf
-          env
-          lower_guard
-          lower_guard_pp
-      in
-      assertion :: stmts, env
-    end
-    else stmts, env
-  in
-  (* Upper guard *)
-  let sizet_max =
-    Logic_const.tint ~loc (Cil.max_unsigned_number (Cil.bitsSizeOf sizet))
-  in
-  let pred_name = Format.sprintf "%s_lesser_or_eq_than_SIZE_MAX" name in
-  let upper_guard_pp = Logic_const.prel ~loc (Rle, pp, sizet_max) in
-  let upper_guard_pp =
-    { upper_guard_pp with
-      pred_name = pred_name :: upper_guard_pp.pred_name }
-  in
-  let upper_guard = Logic_const.prel ~loc (Rle, t, sizet_max) in
-  Typing.type_named_predicate ~lenv upper_guard;
-  let adata_upper_guard, env = Assert.empty ~loc kf env in
-  let upper_guard, adata_upper_guard, env =
-    predicate_to_exp ~adata:adata_upper_guard kf env upper_guard
-  in
-  let assertion, env =
-    Assert.runtime_check
-      ~adata:adata_upper_guard
-      ~pred_kind:Assert
-      Smart_stmt.RTE
-      kf
-      env
-      upper_guard
-      upper_guard_pp
-  in
-  let stmts = assertion :: stmts in
-  (* Translate term [t] into an exp of type [size_t] *)
-  let gmp_e, adata, env = term_to_exp ~adata kf env t in
-  let  _, e, env = Env.new_var
-      ~loc
-      ~name:"size"
-      env
-      kf
-      None
-      sizet
-      (fun vi _ ->
-         let rtl_call =
-           Smart_stmt.rtl_call ~loc
-             ~result:(Cil.var vi)
-             ~prefix:""
-             "__gmpz_get_ui"
-             [ gmp_e ]
-         in
-         List.rev (rtl_call :: stmts))
-  in
-  e, adata, env
-
 let () =
+  Translate_utils.term_to_exp_ref := term_to_exp;
   Loops.term_to_exp_ref := term_to_exp;
-  Loops.translate_predicate_ref := translate_predicate;
-  Loops.predicate_to_exp_ref := predicate_to_exp_without_rte;
-  Quantif.predicate_to_exp_ref := predicate_to_exp_without_rte;
   At_with_lscope.term_to_exp_ref := term_to_exp;
-  At_with_lscope.predicate_to_exp_ref := predicate_to_exp_without_rte;
   Memory_translate.term_to_exp_ref := term_to_exp;
-  Memory_translate.predicate_to_exp_ref := predicate_to_exp_without_rte;
-  Memory_translate.gmp_to_sizet_ref := gmp_to_sizet;
-  Logic_functions.term_to_exp_ref := term_to_exp;
-  Logic_functions.predicate_to_exp_ref := predicate_to_exp_without_rte;
-  Logic_array.translate_rte_ref := translate_rte
+  Logic_functions.term_to_exp_ref := term_to_exp
 
 exception No_simple_term_translation of term
-exception No_simple_predicate_translation of predicate
-
-(* This function is used by Guillaume.
-   However, it is correct to use it only in specific contexts. *)
-let untyped_predicate_to_exp p =
-  let env = Env.push Env.empty in
-  let env = Env.rte env false in
-  let e, _, env =
-    try generalized_untyped_predicate_to_exp
-          ~adata:Assert.no_data
-          (Kernel_function.dummy ())
-          env
-          p
-    with Rtl.Symbols.Unregistered _ -> raise (No_simple_predicate_translation p)
-  in
-  if not (Env.has_no_new_stmt env)
-  then raise (No_simple_predicate_translation p);
-  e
 
 (* This function is used by plug-in [Cfp]. *)
 let untyped_term_to_exp typ t =
diff --git a/src/plugins/e-acsl/src/code_generator/translate_terms.mli b/src/plugins/e-acsl/src/code_generator/translate_terms.mli
new file mode 100644
index 00000000000..ac50cf18e80
--- /dev/null
+++ b/src/plugins/e-acsl/src/code_generator/translate_terms.mli
@@ -0,0 +1,57 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
+(*                                                                        *)
+(*  Copyright (C) 2012-2021                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Cil_types
+
+(** Generate C implementations of E-ACSL terms. *)
+
+val term_to_exp:
+  adata:Assert.t ->
+  kernel_function ->
+  Env.t ->
+  term ->
+  exp * Assert.t * Env.t
+(** Convert an ACSL term into a corresponding C expression. *)
+
+exception No_simple_term_translation of term
+(** Exceptin raised if [untyped_term_to_exp] would generate new statements in
+    the environment *)
+
+val untyped_term_to_exp: typ option -> term -> exp
+(** Convert an untyped ACSL term into a corresponding C expression. *)
+
+(**************************************************************************)
+(********************** Forward references ********************************)
+(**************************************************************************)
+
+val translate_rte_exp_ref:
+  (?filter:(code_annotation -> bool) ->
+   kernel_function ->
+   Env.t ->
+   exp ->
+   Env.t) ref
+
+(*
+Local Variables:
+compile-command: "make -C ../../../../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/code_generator/translate_utils.ml b/src/plugins/e-acsl/src/code_generator/translate_utils.ml
new file mode 100644
index 00000000000..5b7e7871488
--- /dev/null
+++ b/src/plugins/e-acsl/src/code_generator/translate_utils.ml
@@ -0,0 +1,349 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
+(*                                                                        *)
+(*  Copyright (C) 2012-2021                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+(** Utility functions for generating C implementations. *)
+
+module E_acsl_label = Label
+open Cil_types
+open Cil_datatype
+
+(**************************************************************************)
+(********************** Forward references ********************************)
+(**************************************************************************)
+
+let term_to_exp_ref
+  : (adata:Assert.t ->
+     kernel_function ->
+     Env.t ->
+     term ->
+     exp * Assert.t * Env.t) ref
+  =
+  ref (fun ~adata:_ _kf _env _t -> Extlib.mk_labeled_fun "term_to_exp_ref")
+
+let predicate_to_exp_ref
+  : (adata:Assert.t ->
+     ?name:string ->
+     kernel_function ->
+     ?rte:bool ->
+     Env.t ->
+     predicate ->
+     exp * Assert.t * Env.t) ref
+  =
+  ref (fun ~adata:_ ?name:_ _kf ?rte:_ _env _p ->
+      Extlib.mk_labeled_fun "predicate_to_exp_ref")
+
+(**************************************************************************)
+(********************** Utility functions *********************************)
+(**************************************************************************)
+
+let must_translate ppt =
+  Options.Valid.get ()
+  || match Property_status.get ppt with
+  | Never_tried
+  | Inconsistent _
+  | Best ((False_if_reachable | False_and_reachable | Dont_know), _) ->
+    true
+  | Best (True, _) ->
+    (* [TODO] generating code for "valid under hypotheses" properties could be
+       useful for some use cases (in particular, when E-ACSL does not stop on
+       the very first error).
+       ==> introduce a new option or modify the behavior of -e-acsl-valid,
+       see e-acsl#35 *)
+    false
+
+let must_translate_opt = function
+  | None -> false
+  | Some ppt -> must_translate ppt
+
+let gmp_to_sizet ~adata ~loc ~name ?(check_lower_bound=true) ?pp kf env t =
+  let lenv = Env.Local_vars.get env in
+  let pp = match pp with Some size_pp -> size_pp | None -> t in
+  let sizet = Cil.(theMachine.typeOfSizeOf) in
+  let stmts = [] in
+  (* Lower guard *)
+  let stmts, env =
+    if check_lower_bound then begin
+      let zero_term = Cil.lzero ~loc () in
+      let pred_name = Format.sprintf "%s_greater_or_eq_than_0" name in
+      let lower_guard_pp = Logic_const.prel ~loc (Rge, pp, zero_term) in
+      let lower_guard_pp =
+        { lower_guard_pp with
+          pred_name = pred_name :: lower_guard_pp.pred_name }
+      in
+      let lower_guard = Logic_const.prel ~loc (Rge, t, zero_term) in
+      Typing.type_named_predicate ~lenv lower_guard;
+      let adata_lower_guard, env = Assert.empty ~loc kf env in
+      let lower_guard, adata_lower_guard, env =
+        !predicate_to_exp_ref ~adata:adata_lower_guard kf env lower_guard
+      in
+      let assertion, env =
+        Assert.runtime_check
+          ~adata:adata_lower_guard
+          ~pred_kind:Assert
+          Smart_stmt.RTE
+          kf
+          env
+          lower_guard
+          lower_guard_pp
+      in
+      assertion :: stmts, env
+    end
+    else stmts, env
+  in
+  (* Upper guard *)
+  let sizet_max =
+    Logic_const.tint ~loc (Cil.max_unsigned_number (Cil.bitsSizeOf sizet))
+  in
+  let pred_name = Format.sprintf "%s_lesser_or_eq_than_SIZE_MAX" name in
+  let upper_guard_pp = Logic_const.prel ~loc (Rle, pp, sizet_max) in
+  let upper_guard_pp =
+    { upper_guard_pp with
+      pred_name = pred_name :: upper_guard_pp.pred_name }
+  in
+  let upper_guard = Logic_const.prel ~loc (Rle, t, sizet_max) in
+  Typing.type_named_predicate ~lenv upper_guard;
+  let adata_upper_guard, env = Assert.empty ~loc kf env in
+  let upper_guard, adata_upper_guard, env =
+    !predicate_to_exp_ref ~adata:adata_upper_guard kf env upper_guard
+  in
+  let assertion, env =
+    Assert.runtime_check
+      ~adata:adata_upper_guard
+      ~pred_kind:Assert
+      Smart_stmt.RTE
+      kf
+      env
+      upper_guard
+      upper_guard_pp
+  in
+  let stmts = assertion :: stmts in
+  (* Translate term [t] into an exp of type [size_t] *)
+  let gmp_e, adata, env = !term_to_exp_ref ~adata kf env t in
+  let  _, e, env = Env.new_var
+      ~loc
+      ~name:"size"
+      env
+      kf
+      None
+      sizet
+      (fun vi _ ->
+         let rtl_call =
+           Smart_stmt.rtl_call ~loc
+             ~result:(Cil.var vi)
+             ~prefix:""
+             "__gmpz_get_ui"
+             [ gmp_e ]
+         in
+         List.rev (rtl_call :: stmts))
+  in
+  e, adata, env
+
+let () =
+  Memory_translate.gmp_to_sizet_ref := gmp_to_sizet
+
+let comparison_to_exp
+    ~adata
+    ~loc
+    kf
+    env
+    ity
+    ?e1
+    bop
+    t1
+    t2
+    ?(name = Misc.name_of_binop bop)
+    t_opt
+  =
+  let e1, adata, env =
+    match e1 with
+    | None ->
+      let e1, adata, env = !term_to_exp_ref ~adata kf env t1 in
+      e1, adata, env
+    | Some e1 ->
+      e1, adata, env
+  in
+  let ty1 = Cil.typeOf e1 in
+  let e2, adata, env = !term_to_exp_ref ~adata kf env t2 in
+  let ty2 = Cil.typeOf e2 in
+  let e, env =
+    match Logic_aggr.get_t ty1, Logic_aggr.get_t ty2 with
+    | Logic_aggr.Array, Logic_aggr.Array ->
+      Logic_array.comparison_to_exp
+        ~loc
+        kf
+        env
+        ~name
+        bop
+        e1
+        e2
+    | Logic_aggr.StructOrUnion, Logic_aggr.StructOrUnion ->
+      Env.not_yet env "comparison between two structs or unions"
+    | Logic_aggr.NotAggregate, Logic_aggr.NotAggregate -> begin
+        match ity with
+        | Typing.C_integer _ | Typing.C_float _ | Typing.Nan ->
+          Cil.mkBinOp ~loc bop e1 e2, env
+        | Typing.Gmpz ->
+          let _, e, env = Env.new_var
+              ~loc
+              env
+              kf
+              t_opt
+              ~name
+              Cil.intType
+              (fun v _ ->
+                 [ Smart_stmt.rtl_call ~loc
+                     ~result:(Cil.var v)
+                     ~prefix:""
+                     "__gmpz_cmp"
+                     [ e1; e2 ] ])
+          in
+          Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env
+        | Typing.Rational ->
+          Rational.cmp ~loc bop e1 e2 env kf t_opt
+        | Typing.Real ->
+          Error.not_yet "comparison involving real numbers"
+      end
+    | _, _ ->
+      Options.fatal
+        ~current:true
+        "Comparison involving incompatible types: '%a' and '%a'"
+        Printer.pp_typ ty1
+        Printer.pp_typ ty2
+  in
+  e, adata, env
+
+let conditional_to_exp ?(name="if") ~loc kf t_opt e1 (e2, env2) (e3, env3) =
+  let env = Env.pop (Env.pop env3) in
+  match e1.enode with
+  | Const(CInt64(n, _, _)) when Integer.is_zero n ->
+    e3, Env.transfer ~from:env3 env
+  | Const(CInt64(n, _, _)) when Integer.is_one n ->
+    e2, Env.transfer ~from:env2 env
+  | _ ->
+    let ty = match t_opt with
+      | None (* predicate *) -> Cil.intType
+      | Some t -> Typing.get_typ ~lenv:(Env.Local_vars.get env) t
+    in
+    let _, e, env =
+      Env.new_var
+        ~loc
+        ~name
+        env
+        kf
+        t_opt
+        ty
+        (fun v ev ->
+           let lv = Cil.var v in
+           let ty = Cil.typeOf ev in
+           let init_set =
+             assert (not (Gmp_types.Q.is_t ty));
+             Gmp.init_set
+           in
+           let affect e = init_set ~loc lv ev e in
+           let then_blk, _ =
+             let s = affect e2 in
+             Env.pop_and_get env2 s ~global_clear:false Env.Middle
+           in
+           let else_blk, _ =
+             let s = affect e3 in
+             Env.pop_and_get env3 s ~global_clear:false Env.Middle
+           in
+           [ Smart_stmt.if_stmt ~loc ~cond:e1 then_blk ~else_blk ])
+    in
+    e, env
+
+let env_of_li ~adata ~loc kf env li =
+  match li.l_var_info.lv_type with
+  | Ctype _ | Linteger | Lreal ->
+    let t = Misc.term_of_li li in
+    let lenv = Env.Local_vars.get env in
+    let ty = Typing.get_typ ~lenv t in
+    let vi, vi_e, env = Env.Logic_binding.add ~ty env kf li.l_var_info in
+    let e, adata, env = !term_to_exp_ref ~adata kf env t in
+    let stmt = match Typing.get_number_ty ~lenv t with
+      | Typing.(C_integer _ | C_float _ | Nan) ->
+        Smart_stmt.assigns ~loc ~result:(Cil.var vi) e
+      | Typing.Gmpz ->
+        Gmp.init_set ~loc (Cil.var vi) vi_e e
+      | Typing.Rational ->
+        Rational.init_set ~loc (Cil.var vi) vi_e e
+      | Typing.Real ->
+        Error.not_yet "real number"
+    in
+    adata, Env.add_stmt env kf stmt
+  | Ltype _ ->
+    Env.not_yet env "user-defined logic type"
+  | Lvar _ ->
+    Env.not_yet env "type variable"
+  | Larrow _ ->
+    Env.not_yet env "lambda-abstraction"
+
+let at_to_exp_no_lscope kf env t_opt label e =
+  let stmt = E_acsl_label.get_stmt kf label in
+  (* generate a new variable denoting [\at(t',label)].
+     That is this variable which is the resulting expression.
+     ACSL typing rule ensures that the type of this variable is the same as
+     the one of [e]. *)
+  let loc = Stmt.loc stmt in
+  let res_v, res, new_env =
+    Env.new_var
+      ~loc
+      ~name:"at"
+      ~scope:Varname.Function
+      env
+      kf
+      t_opt
+      (Cil.typeOf e)
+      (fun _ _ -> [])
+  in
+  let env_ref = ref new_env in
+  (* visitor modifying in place the labeled statement in order to store [e]
+     in the resulting variable at this location (which is the only correct
+     one). *)
+  let o = object
+    inherit Visitor.frama_c_inplace
+    method !vstmt_aux stmt =
+      (* either a standard C affectation or a call to an initializer according
+         to the type of [e] *)
+      let ty = Cil.typeOf e in
+      let init_set =
+        if Gmp_types.Q.is_t ty then Rational.init_set else Gmp.init_set
+      in
+      let new_stmt = init_set ~loc (Cil.var res_v) res e in
+      assert (!env_ref == new_env);
+      (* generate the new block of code for the labeled statement and the
+         corresponding environment *)
+      let block, new_env =
+        Env.pop_and_get new_env new_stmt ~global_clear:false Env.Middle
+      in
+      env_ref := Env.extend_stmt_in_place new_env stmt ~label block;
+      Cil.ChangeTo stmt
+  end
+  in
+  ignore (Visitor.visitFramacStmt o stmt);
+  res, !env_ref, Typed_number.C_number
+
+(*
+Local Variables:
+compile-command: "make -C ../../../../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/code_generator/translate_utils.mli b/src/plugins/e-acsl/src/code_generator/translate_utils.mli
new file mode 100644
index 00000000000..a7a7489ab8e
--- /dev/null
+++ b/src/plugins/e-acsl/src/code_generator/translate_utils.mli
@@ -0,0 +1,134 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
+(*                                                                        *)
+(*  Copyright (C) 2012-2021                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Cil_types
+
+(** Utility functions for generating C implementations. *)
+
+val must_translate: Property.t -> bool
+(** @return true if the given property must be translated (ie. if the valid
+    properties must be translated or if its status is not [True]), false
+    otherwise. *)
+
+val must_translate_opt: Property.t option -> bool
+(** Same than [must_translate] but for [Property.t option]. Return false if the
+    option is [None]. *)
+
+val gmp_to_sizet:
+  adata:Assert.t ->
+  loc:location ->
+  name:string ->
+  ?check_lower_bound:bool ->
+  ?pp:term ->
+  kernel_function ->
+  Env.t ->
+  term ->
+  exp * Assert.t * Env.t
+(** Translate the given GMP integer to an expression of type [size_t]. RTE
+    checks are generated to ensure that the GMP value holds in this type.
+    The parameter [name] is used to generate relevant predicate names.
+    If [check_lower_bound] is set to [false], then the GMP value is assumed to
+    be positive.
+    If [pp] is provided, this term is used in the messages of the RTE checks. *)
+
+val comparison_to_exp:
+  adata:Assert.t ->
+  loc:location ->
+  kernel_function ->
+  Env.t ->
+  Typing.number_ty ->
+  ?e1:exp ->
+  binop ->
+  term ->
+  term ->
+  ?name:string ->
+  term option ->
+  exp * Assert.t * Env.t
+(** [comparison_to_exp ~data ~loc kf env ity ?e1 ?name bop t1 t2 topt] generates
+    the C code equivalent to [t1 bop t2] in the given environment with the
+    given assertion context.
+    [ity] is the number type of the comparison when comparing scalar numbers.
+    [e1] is the expression representing [t1] if the term has already been
+    translated.
+    [name] is used to generate temporary variable names.
+    [topt] is the term holding the result of the comparison. *)
+
+val conditional_to_exp:
+  ?name:string ->
+  loc:location ->
+  kernel_function ->
+  term option ->
+  exp ->
+  exp * Env.t ->
+  exp * Env.t ->
+  exp * Env.t
+(** [conditional_to_exp ?name ~loc kf t_opt e1 (e2, env2) (e3, env3)] generates
+    the C code equivalent to [e1 ? e2 : e3] in the given  environment.
+    [env2] and [env3] are the environment respectively for [e2] and [e3].
+    [t_opt] is the term holding the result of the conditional. *)
+
+val env_of_li:
+  adata:Assert.t ->
+  loc:location ->
+  kernel_function ->
+  Env.t ->
+  logic_info ->
+  Assert.t * Env.t
+(** [env_of_li ~adata ~loc kf env li] translates the logic info [li] in the
+    given environment with the given assertion context. *)
+
+val at_to_exp_no_lscope:
+  kernel_function ->
+  Env.t ->
+  term option ->
+  logic_label ->
+  exp ->
+  exp * Env.t * Typed_number.strnum
+(** [at_to_exp_no_lscope kf env t_opt llabel e] generates an expression
+    representing the expression [e] at the label [llabel].
+    [t_opt] is the term representing [\at(e, llabel)]. *)
+
+(**************************************************************************)
+(********************** Forward references ********************************)
+(**************************************************************************)
+
+val term_to_exp_ref:
+  (adata:Assert.t ->
+   kernel_function ->
+   Env.t ->
+   term ->
+   exp * Assert.t * Env.t) ref
+
+val predicate_to_exp_ref:
+  (adata:Assert.t ->
+   ?name:string ->
+   kernel_function ->
+   ?rte:bool ->
+   Env.t ->
+   predicate ->
+   exp * Assert.t * Env.t) ref
+
+(*
+Local Variables:
+compile-command: "make -C ../../../../.."
+End:
+*)
-- 
GitLab