[e-acsl] code review

src/plugins/e-acsl/src/analyses/bound_variables.ml

@@ -694,19 +694,19 @@ end
         (Err (Error.Not_yet "unguarded \\exists quantification"))
     | _ -> ()
 
-  let gannot a =
-    match a with
-    | Dfun_or_pred (li,loc) ->
-      (match li.l_body with
-       | LBpred p ->
-         (match Logic_normalizer.get_pred p with
-          | PoT_pred p -> process_quantif ~loc p
-          | PoT_term _ -> ())
-       | _ -> ())
-
-    | _ -> ()
-
-  let do_predicates () =
+  let do_user_predicates () =
+    let gannot a =
+      match a with
+      | Dfun_or_pred (li,loc) ->
+        (match li.l_body with
+         | LBpred p ->
+           (match Logic_normalizer.get_pred p with
+            | PoT_pred p -> process_quantif ~loc p
+            | PoT_term _ -> ())
+         | _ -> ())
+
+      | _ -> ()
+    in
     Annotations.iter_global (fun _ a -> gannot a)
 
   let preprocessor = object
@@ -725,7 +725,7 @@ end
     Visitor.visitFramacFileSameGlobals
       (preprocessor :> Visitor.frama_c_inplace)
       ast;
-    do_predicates ()
+    do_user_predicates ()
 
   let compute_annot annot =
     ignore

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

@@ -243,9 +243,10 @@ let to_exp ~loc kf env pot label =
     | Lscope.PoT_pred _ ->
       Cil.intType
     | Lscope.PoT_term t ->
-      begin match Typing.get_number_ty ~lenv:(Env.Local_vars.get env) t with
+      let lenv = (Env.Local_vars.get env) in
+      begin match Typing.get_number_ty ~lenv t with
         | Typing.(C_integer _ | C_float _ | Nan) ->
-          Typing.get_typ ~lenv:(Env.Local_vars.get env) t
+          Typing.get_typ ~lenv t
         | Typing.(Rational | Real) ->
           Error.not_yet "\\at on purely logic variables and over real type"
         | Typing.Gmpz ->
@@ -269,12 +270,10 @@ let to_exp ~loc kf env pot label =
          let t_size =
            Logic_const.term ~loc (TBinOp(Mult, t_sizeof, t_size)) lty_sizeof
          in
-         Typing.type_term
-           ~use_gmp_opt:false
-           ~lenv:(Env.Local_vars.get env)
-           t_size;
+         let lenv = Env.Local_vars.get env in
+         Typing.type_term ~use_gmp_opt:false ~lenv t_size;
          let malloc_stmt =
-           match Typing.get_number_ty ~lenv:(Env.Local_vars.get env) t_size with
+           match Typing.get_number_ty ~lenv t_size with
            | Typing.C_integer IInt ->
              let e_size, _, _ =
                term_to_exp ~adata:Assert.no_data kf env t_size

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

@@ -405,8 +405,7 @@ let raise_errors = function
   | LBterm _
   | LBpred _ -> ()
 
-let app_to_exp ~adata ~loc ?tapp kf env ?eargs
-    ((li, targs) : logic_info * term list) =
+let app_to_exp ~adata ~loc ?tapp kf env ?eargs li targs =
   let fname = li.l_var_info.lv_name in
   (* build the varinfo (as an expression) which stores the result of the
      function call. *)
@@ -423,7 +422,7 @@ let app_to_exp ~adata ~loc ?tapp kf env ?eargs
             targs
             ([], adata, env)
         | Some eargs ->
-          if List.compare_lengths targs eargs != 0 then
+          if List.compare_lengths targs eargs <> 0 then
             Options.fatal
               "[Tapp] unexpected number of arguments when calling %s"
               fname;
@@ -460,7 +459,7 @@ let app_to_exp ~adata ~loc ?tapp kf env ?eargs
                 targs
                 ([], adata, env)
             | Some eargs ->
-              if List.compare_lengths targs eargs != 0 then
+              if List.compare_lengths targs eargs <> 0 then
                 Options.fatal
                   "[Tapp] unexpected number of arguments when calling %s"
                   fname;
@@ -507,117 +506,6 @@ let app_to_exp ~adata ~loc ?tapp kf env ?eargs
   in
   e, adata, env
 
-(* let tapp_to_exp ~adata kf env ?eargs tapp = *)
-(*   match tapp.term_node with *)
-(*   | Tapp(li, l, targs) -> *)
-(*     let loc = tapp.term_loc in *)
-(*     let fname = li.l_var_info.lv_name in *)
-(*     (\* build the varinfo (as an expression) which stores the result of the *)
-(*        function call. *\) *)
-(*     let _, e, adata, env = *)
-(*       if Builtins.mem li.l_var_info.lv_name then *)
-(*         match l with *)
-(*         | _::_ -> Error.not_yet "E-ACSL built-in functions with labels" *)
-(*         | [] -> *)
-(*           (\* E-ACSL built-in function call *\) *)
-(*           let args, adata, env = *)
-(*             match eargs with *)
-(*             | None -> *)
-(*               List.fold_right *)
-(*                 (fun targ (l, adata, env) -> *)
-(*                    let e, adata, env = !term_to_exp_ref ~adata kf env targ in *)
-(*                    e :: l, adata, env) *)
-(*                 targs *)
-(*                 ([], adata, env) *)
-(*             | Some eargs -> *)
-(*               if List.compare_lengths targs eargs != 0 then *)
-(*                 Options.fatal *)
-(*                   "[Tapp] unexpected number of arguments when calling %s" *)
-(*                   fname; *)
-(*               eargs, adata, env *)
-(*           in *)
-(*           let vi, e, env = *)
-(*             Env.new_var *)
-(*               ~loc *)
-(*               ~name:(fname ^ "_app") *)
-(*               env *)
-(*               kf *)
-(*               (Some tapp) *)
-(*               (Misc.cty (Option.get li.l_type)) *)
-(*               (fun vi _ -> *)
-(*                  [ Smart_stmt.rtl_call ~loc *)
-(*                      ~result:(Cil.var vi) *)
-(*                      ~prefix:"" *)
-(*                      fname *)
-(*                      args ]) *)
-(*           in *)
-(*           vi, e, adata, env *)
-(*       else *)
-(*         begin *)
-(*           raise_errors l li.l_body; *)
-(*           (\* build the arguments and compute the integer_ty of the parameters *\) *)
-(*           let params_ty, args, adata, env = *)
-(*             let eargs, adata, env = *)
-(*               match eargs with *)
-(*               | None -> *)
-(*                 List.fold_right *)
-(*                   (fun targ (eargs, adata, env) -> *)
-(*                      let e, adata, env = !term_to_exp_ref ~adata kf env targ in *)
-(*                      e :: eargs, adata, env) *)
-(*                   targs *)
-(*                   ([], adata, env) *)
-(*               | Some eargs -> *)
-(*                 if List.compare_lengths targs eargs != 0 then *)
-(*                   Options.fatal *)
-(*                     "[Tapp] unexpected number of arguments when calling %s" *)
-(*                     fname; *)
-(*                 eargs, adata, env *)
-(*             in *)
-(*             try *)
-(*               List.fold_right2 *)
-(*                 (fun targ earg (params_ty, args, adata, env) -> *)
-(*                    let param_ty = *)
-(*                      Typing.get_number_ty *)
-(*                        ~lenv:(Env.Local_vars.get env) *)
-(*                        targ *)
-(*                    in *)
-(*                    let e, env = *)
-(*                      try *)
-(*                        let ty = Typing.typ_of_number_ty param_ty in *)
-(*                        Typed_number.add_cast *)
-(*                          ~loc *)
-(*                          env *)
-(*                          kf *)
-(*                          (Some ty) *)
-(*                          Typed_number.C_number *)
-(*                          (Some targ) *)
-(*                          earg *)
-(*                      with Typing.Not_a_number -> *)
-(*                        earg, env *)
-(*                    in *)
-(*                    param_ty :: params_ty, e :: args, adata, env) *)
-(*                 targs eargs *)
-(*                 ([], [], adata ,env) *)
-(*             with Invalid_argument _ -> *)
-(*               Options.fatal *)
-(*                 "[Tapp] unexpected number of arguments when calling %s" *)
-(*                 fname *)
-(*           in *)
-(*           let gen_fname = *)
-(*             Varname.get ~scope:Varname.Global (Functions.RTL.mk_gen_name fname) *)
-(*           in *)
-(*           let vi, e, env = *)
-(*             function_to_exp ~loc ~tapp gen_fname env kf li params_ty args *)
-(*           in *)
-(*           vi, e, adata, env *)
-(*         end *)
-(*     in *)
-(*     e, adata, env *)
-(*   | _ -> *)
-(*     Options.fatal *)
-(*       "tapp_to_exp called with '%a' instead of Tapp term" *)
-(*       Printer.pp_term tapp *)
-
 (*
 Local Variables:
 compile-command: "make -C ../.."

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

@@ -43,10 +43,13 @@ val app_to_exp:
   kernel_function ->
   Env.t ->
   ?eargs:exp list ->
-  logic_info * term list ->
+  logic_info ->
+  term list ->
   exp * Assert.t * Env.t
-(** Translate a Tapp term to an expression. If the optional argument [eargs] is
-    provided, then these expressions are used as arguments of the fonction. *)
+(** Translate a Tapp term or a Papp predicate to an expression. If the optional
+    argument [eargs] is provided, then these expressions are used as arguments
+    of the fonction. The optional argument [tapp] is the term corresponding to
+    the call, in case we are translating a term *)
 
 val add_generated_functions: global list -> global list
 (* @return the input list of globals in which the generated functions have been

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

@@ -65,8 +65,9 @@ let handle_annotations env kf stmt =
            | Some (t, measure_opt) ->
              let env = Env.set_annotation_kind env Smart_stmt.Variant in
              let env = Env.push env in
-             Typing.type_term ~use_gmp_opt:true ~lenv:(Env.Local_vars.get env) t;
-             let ty = Typing.get_typ ~lenv:(Env.Local_vars.get env) t in
+             let lenv = Env.Local_vars.get env in
+             Typing.type_term ~use_gmp_opt:true ~lenv t;
+             let ty = Typing.get_typ ~lenv t in
              if Gmp_types.is_t ty then Error.not_yet "loop variant using GMP";
              let e, _, env = !term_to_exp_ref ~adata:Assert.no_data kf env t in
              let vi_old, e_old, env =
@@ -96,6 +97,7 @@ let handle_annotations env kf stmt =
       | [] -> begin
           (* No statements remaining in the loop: variant check *)
           let env = Env.set_annotation_kind env Smart_stmt.Variant in
+          let lenv = Env.Local_vars.get env in
           match variant with
           | Some (t, e_old, Some measure) ->
             let env = Env.push env in
@@ -106,10 +108,7 @@ let handle_annotations env kf stmt =
                 term_name = [];
                 term_type = Linteger;}
             in
-            Typing.type_term
-              ~use_gmp_opt:true
-              ~lenv:(Env.Local_vars.get env)
-              tapp;
+            Typing.type_term ~use_gmp_opt:true ~lenv tapp;
             let e, _, env = !term_to_exp_ref ~adata:Assert.no_data kf env t in
             let e_tapp, _, env =
               Logic_functions.app_to_exp
@@ -119,7 +118,8 @@ let handle_annotations env kf stmt =
                 kf
                 env
                 ~eargs:[e_old; e]
-                (measure, [t_old; t])
+                measure
+                [t_old; t]
             in
             let msg =
               Format.asprintf
@@ -169,9 +169,7 @@ let handle_annotations env kf stmt =
             let variant_pos =
               Logic_const.prel ~loc (Rge, t_old, Logic_const.tinteger ~loc 0)
             in
-            Typing.type_named_predicate
-              ~lenv:(Env.Local_vars.get env)
-              variant_pos;
+            Typing.type_named_predicate ~lenv variant_pos;
             let variant_pos_e, _, env =
               !predicate_to_exp_ref ~adata:Assert.no_data kf env variant_pos
             in
@@ -205,9 +203,7 @@ let handle_annotations env kf stmt =
             let variant_dec =
               Logic_const.prel ~loc (Rgt, t_old, t)
             in
-            Typing.type_named_predicate
-              ~lenv:(Env.Local_vars.get env)
-              variant_dec;
+            Typing.type_named_predicate ~lenv variant_dec;
             let variant_dec_e, _, env =
               !predicate_to_exp_ref ~adata:Assert.no_data kf env variant_dec
             in
@@ -289,17 +285,18 @@ let handle_annotations env kf stmt =
 (**************************** Nested loops ********************************)
 (**************************************************************************)
 let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
+  let lenv = Env.Local_vars.get env in
   let term_to_exp = !term_to_exp_ref ~adata:Assert.no_data in
   match lscope_vars with
   | [] ->
     mk_innermost_block env
   | Lscope.Lvs_quantif(t1, rel1, logic_x, rel2, t2) :: lscope_vars' ->
     assert (rel1 == Rle && rel2 == Rlt);
-    Typing.type_term ~use_gmp_opt:false ~lenv:(Env.Local_vars.get env) t1;
-    Typing.type_term ~use_gmp_opt:false ~lenv:(Env.Local_vars.get env) t2;
+    Typing.type_term ~use_gmp_opt:false ~lenv t1;
+    Typing.type_term ~use_gmp_opt:false ~lenv t2;
     let ctx =
-      let ty1 = Typing.get_number_ty ~lenv:(Env.Local_vars.get env) t1 in
-      let ty2 = Typing.get_number_ty ~lenv:(Env.Local_vars.get env) t2 in
+      let ty1 = Typing.get_number_ty ~lenv t1 in
+      let ty2 = Typing.get_number_ty ~lenv t2 in
       Typing.join ty1 ty2
     in
     let t_plus_one ?ty t =
@@ -308,9 +305,9 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
       let res = Logic_const.term ~loc (TBinOp(PlusA, t, tone)) Linteger in
       Option.iter
         (fun ty ->
-           Typing.unsafe_set tone ~ctx:ty ~lenv:(Env.Local_vars.get env) ctx;
-           Typing.unsafe_set t ~ctx:ty ~lenv:(Env.Local_vars.get env) ctx;
-           Typing.unsafe_set res ~lenv:(Env.Local_vars.get env) ty)
+           Typing.unsafe_set tone ~ctx:ty ~lenv ctx;
+           Typing.unsafe_set t ~ctx:ty ~lenv ctx;
+           Typing.unsafe_set res ~lenv ty)
         ty;
       res
     in
@@ -355,11 +352,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
           (TBinOp(Lt, tlv, { t2 with term_node = t2.term_node } ))
           Linteger
     in
-    Typing.type_term
-      ~use_gmp_opt:false
-      ~lenv:(Env.Local_vars.get env)
-      ~ctx:Typing.c_int
-      guard;
+    Typing.type_term ~use_gmp_opt:false ~lenv ~ctx:Typing.c_int guard;
     let guard_exp, _, env = term_to_exp kf (Env.push env) guard in
     let break_stmt = Smart_stmt.break ~loc:guard_exp.eloc in
     let guard_blk, env = Env.pop_and_get
@@ -425,7 +418,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
     Env.Logic_binding.remove env logic_x;
     [ start ;  stmt ], env
   | Lscope.Lvs_let(lv, t) :: lscope_vars' ->
-    let ty = Typing.get_typ ~lenv:(Env.Local_vars.get env) t in
+    let ty = Typing.get_typ ~lenv t in
     let vi_of_lv, exp_of_lv, env = Env.Logic_binding.add ~ty env kf lv in
     let e, _, env = term_to_exp kf env t in
     let ty = Cil.typeOf e in

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

@@ -264,9 +264,10 @@ let range_to_ptr_and_size ~adata ~loc kf env ptr r p =
     in
     Logic_const.term ~loc (Tlet (size_term_info, size_term_if)) Linteger
   in
-  Typing.type_term ~use_gmp_opt:false ~lenv:(Env.Local_vars.get env) size_term;
+  let lenv = Env.Local_vars.get env in
+  Typing.type_term ~use_gmp_opt:false ~lenv size_term;
   let size, adata, env =
-    match Typing.get_number_ty size_term  ~lenv:(Env.Local_vars.get env) with
+    match Typing.get_number_ty size_term  ~lenv with
     | Typing.Gmpz ->
       (* Start by translating [size_term] to an expression so that the full term
          with [\let] is not passed around. *)

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

@@ -40,13 +40,14 @@ let relation_to_binop = function
   | Rneq -> Ne
 
 let constant_to_exp ~loc env t c =
+  let lenv = Env.Local_vars.get env in
   let mk_real s =
     let s = Rational.normalize_str s in
     Cil.mkString ~loc s, Typed_number.Str_R
   in
   match c with
   | Integer(n, _repr) ->
-    let ity = Typing.get_number_ty ~lenv:(Env.Local_vars.get env) t in
+    let ity = Typing.get_number_ty ~lenv t in
     (match ity with
      | Typing.Nan -> assert false
      | Typing.Real -> Error.not_yet "real number constant"
@@ -57,7 +58,7 @@ let constant_to_exp ~loc env t c =
      | Typing.C_float fkind ->
        Cil.kfloat ~loc fkind (Int64.to_float (Integer.to_int64_exn n)), C_number
      | Typing.C_integer kind ->
-       let cast = Typing.get_cast ~lenv:(Env.Local_vars.get env) t in
+       let cast = Typing.get_cast ~lenv t in
        match cast, kind with
        | Some ty, (ILongLong | IULongLong) when Gmp_types.Z.is_t ty ->
          (* too large integer *)
@@ -196,12 +197,13 @@ and tlval_to_lval kf env (host, offset) =
    extended quantifier ("\sum" or "\product").  Do not take care of "\numof"
    that have already been converted to "\sum". *)
 and extended_quantifier_to_exp ~adata ~loc kf env t t_min t_max lambda name =
+  let lenv = Env.Local_vars.get env in
   match lambda.term_node with
   | Tlambda([ k ] ,lt)
     when name.lv_name = "\\product" || name.lv_name = "\\sum"
     ->
-    let ty_op = Typing.get_typ ~lenv:(Env.Local_vars.get env) t in
-    let ty_k = match Typing.get_cast ~lenv:(Env.Local_vars.get env) t_min with
+    let ty_op = Typing.get_typ ~lenv t in
+    let ty_k = match Typing.get_cast ~lenv t_min with
       | Some e -> e
       | _ -> Options.fatal "unexpected error in \\sum translation"
     in
@@ -295,6 +297,7 @@ and extended_quantifier_to_exp ~adata ~loc kf env t t_min t_max lambda name =
 
 and context_insensitive_term_to_exp ~adata kf env t =
   let loc = t.term_loc in
+  let lenv = Env.Local_vars.get env in
   match t.term_node with
   | TConst c ->
     let c, strnum = constant_to_exp ~loc env t c in
@@ -327,7 +330,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
     let adata, env = Assert.register_term ~loc kf env t e adata in
     e, adata, env, Typed_number.C_number, "alignof"
   | TUnOp(Neg | BNot as op, t') ->
-    let ty = Typing.get_typ ~lenv:(Env.Local_vars.get env) t in
+    let ty = Typing.get_typ ~lenv t in
     let e, adata, env = term_to_exp ~adata kf env t' in
     if Gmp_types.Z.is_t ty then
       let name, vname = match op with
@@ -350,12 +353,12 @@ and context_insensitive_term_to_exp ~adata kf env t =
     else
       Cil.new_exp ~loc (UnOp(op, e, ty)), adata, env, Typed_number.C_number, ""
   | TUnOp(LNot, t) ->
-    let ty = Typing.get_op ~lenv:(Env.Local_vars.get env) t in
+    let ty = Typing.get_op ~lenv t in
     if Gmp_types.Z.is_t ty then
       (* [!t] is converted into [t == 0] *)
       let zero = Logic_const.tinteger 0 in
-      let ctx = Typing.get_number_ty ~lenv:(Env.Local_vars.get env) t in
-      Typing.type_term ~use_gmp_opt:true ~ctx ~lenv:(Env.Local_vars.get env) zero;
+      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
           ~adata
@@ -377,7 +380,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
       e, adata, env, Typed_number.C_number, ""
     end
   | TBinOp(PlusA | MinusA | Mult as bop, t1, t2) ->
-    let ty = Typing.get_typ ~lenv:(Env.Local_vars.get env) t in
+    let ty = Typing.get_typ ~lenv t in
     let e1, adata, env = term_to_exp ~adata kf env t1 in
     let e2, adata, env = term_to_exp ~adata kf env t2 in
     if Gmp_types.Z.is_t ty then
@@ -400,7 +403,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
       e, adata, env, Typed_number.C_number, ""
     end
   | TBinOp(Div | Mod as bop, t1, t2) ->
-    let ty = Typing.get_typ ~lenv:(Env.Local_vars.get env) t in
+    let ty = Typing.get_typ ~lenv t in
     let e1, adata, env = term_to_exp ~adata kf env t1 in
     let t2_to_exp adata env = term_to_exp ~adata kf env t2 in
     if Gmp_types.Z.is_t ty then
@@ -412,14 +415,14 @@ and context_insensitive_term_to_exp ~adata kf env t =
       let adata, env = Assert.merge_right ~loc kf env adata2 adata in
       (* TODO: preventing division by zero should not be required anymore.
          RTE should do this automatically. *)
-      let ctx = Typing.get_number_ty ~lenv:(Env.Local_vars.get env) t in
+      let ctx = Typing.get_number_ty ~lenv t in
       let t = Some t in
       let name = Gmp.name_of_mpz_arith_bop bop in
       (* [TODO] can now do better since the type system got some info about
          possible values of [t2] *)
       (* guarding divisions and modulos *)
       let zero = Logic_const.tinteger 0 in
-      Typing.type_term ~use_gmp_opt:true ~ctx ~lenv:(Env.Local_vars.get env) zero;
+      Typing.type_term ~use_gmp_opt:true ~ctx ~lenv zero;
       (* do not generate [e2] from [t2] twice *)
       let guard, _, env =
         let name = Misc.name_of_binop bop ^ "_guard" in
@@ -459,14 +462,14 @@ and context_insensitive_term_to_exp ~adata kf env t =
     end
   | TBinOp(Lt | Gt | Le | Ge | Eq | Ne as bop, t1, t2) ->
     (* comparison operators *)
-    let ity = Typing.get_integer_op ~lenv:(Env.Local_vars.get env) t in
+    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)
     in
     e, adata, env, Typed_number.C_number, ""
   | TBinOp((Shiftlt | Shiftrt) as bop, t1, t2) ->
     (* left/right shift *)
-    let ty = Typing.get_typ ~lenv:(Env.Local_vars.get env) t in
+    let ty = Typing.get_typ ~lenv t in
     let t1_to_exp adata env = term_to_exp ~adata kf env t1 in
     let t2_to_exp adata env = term_to_exp ~adata kf env t2 in
     if Gmp_types.Z.is_t ty then
@@ -491,12 +494,12 @@ and context_insensitive_term_to_exp ~adata kf env t =
         | TLogic_coerce (_, t) -> term_to_name t
         | _ -> ""
       in
-      let ctx = Typing.get_number_ty ~lenv:(Env.Local_vars.get env) t in
+      let ctx = Typing.get_number_ty ~lenv t in
       let bop_name = Misc.name_of_binop bop in
       let e1_name = term_to_name t1 in
       let e2_name = term_to_name t2 in
       let zero = Logic_const.tinteger 0 in
-      Typing.type_term ~use_gmp_opt:true ~ctx ~lenv:(Env.Local_vars.get env) zero;
+      Typing.type_term ~use_gmp_opt:true ~ctx ~lenv zero;
 
       (* Check that e2 is representable in mp_bitcnt_t *)
       let coerce_guard, env =
@@ -688,7 +691,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
     e, adata, env, Typed_number.C_number, ""
   | TBinOp((BOr | BXor | BAnd) as bop, t1, t2) ->
     (* other logic/arith operators  *)
-    let ty = Typing.get_typ ~lenv:(Env.Local_vars.get env) t in
+    let ty = Typing.get_typ ~lenv t in
     let e1, adata, env = term_to_exp ~adata kf env t1 in
     let e2, adata, env = term_to_exp ~adata kf env t2 in
     if Gmp_types.Z.is_t ty then
@@ -723,11 +726,11 @@ and context_insensitive_term_to_exp ~adata kf env t =
     let e = Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)) in
     e, adata, env, Typed_number.C_number, ""
   | TBinOp(MinusPP, t1, t2) ->
-    begin match Typing.get_number_ty ~lenv:(Env.Local_vars.get env) t with
+    begin match Typing.get_number_ty ~lenv t with
       | Typing.C_integer _ ->
         let e1, adata, env = term_to_exp ~adata kf env t1 in
         let e2, adata, env = term_to_exp ~adata kf env t2 in
-        let ty = Typing.get_typ ~lenv:(Env.Local_vars.get env) t in
+        let ty = Typing.get_typ ~lenv t in
         let e = Cil.new_exp ~loc (BinOp(MinusPP, e1, e2, ty)) in
         e, adata, env, Typed_number.C_number, ""
       | Typing.Gmpz ->
@@ -769,7 +772,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
     assert false
   | Tapp(li, [], args) ->
     let e, adata, env =
-      Logic_functions.app_to_exp ~adata ~loc ~tapp:t kf env (li, args) in
+      Logic_functions.app_to_exp ~adata ~loc ~tapp:t kf env li args in
     let adata, env = Assert.register_term ~loc kf env t e adata in
     e, adata, env, Typed_number.C_number, "app"
   | Tapp(_, _ :: _, _) ->
@@ -1016,10 +1019,11 @@ and at_to_exp_no_lscope env kf t_opt label e =
 
 and env_of_li ~adata li kf env loc =
   let t = Misc.term_of_li li in
-  let ty = Typing.get_typ ~lenv:(Env.Local_vars.get env) t 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:(Env.Local_vars.get env) t with
+  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 ->
@@ -1036,6 +1040,7 @@ and env_of_li ~adata li kf env loc =
    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
@@ -1043,7 +1048,7 @@ and predicate_content_to_exp ~adata ?name kf env p =
   | 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
+      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"
@@ -1052,7 +1057,7 @@ and predicate_content_to_exp ~adata ?name kf env p =
   | Prel(rel, t1, t2) ->
     let ity =
       Typing.get_integer_op_of_predicate
-        ~lenv:(Env.Local_vars.get env)
+        ~lenv
         p
     in
     comparison_to_exp ~adata ~loc kf env ity (relation_to_binop rel) t1 t2 None
@@ -1372,6 +1377,7 @@ let predicate_to_exp_without_rte ~adata kf env p =
   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
@@ -1386,7 +1392,7 @@ let gmp_to_sizet ~adata ~loc ~name ?(check_lower_bound=true) ?pp kf env t =
           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:(Env.Local_vars.get env) lower_guard;
+      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
@@ -1416,7 +1422,7 @@ let gmp_to_sizet ~adata ~loc ~name ?(check_lower_bound=true) ?pp kf env t =
       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:(Env.Local_vars.get env) upper_guard;
+  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