[e-acsl] second code review

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

@@ -697,14 +697,10 @@ end
   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 _ -> ())
-         | _ -> ())
-
+      | Dfun_or_pred ({l_body = LBpred p},loc) ->
+        (match Logic_normalizer.get_pred p with
+         | PoT_pred p -> process_quantif ~loc p
+         | PoT_term _ -> ())
       | _ -> ()
     in
     Annotations.iter_global (fun _ a -> gannot a)

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

@@ -65,9 +65,10 @@ 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
-             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
+             (* There cannot be bound logical variables since we cannot write
+                loops inside logic functions or predicates, hence lenv is []*)
+             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 =

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

@@ -1056,9 +1056,7 @@ and predicate_content_to_exp ~adata ?name kf env p =
   | Pvalid_function _ -> Env.not_yet env "\\valid_function"
   | Prel(rel, t1, t2) ->
     let ity =
-      Typing.get_integer_op_of_predicate
-        ~lenv
-        p
+      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) ->