Merge branch 'feature/thibaut/e-acsl-preprocess-quantifiers' into 'master'

[e-ascl] Preprocessing phase for quantifiers

Closes e-acsl#149

See merge request frama-c/frama-c!3168

src/plugins/e-acsl/Makefile.in

@@ -63,7 +63,8 @@ SRC_ANALYSES:= \
 	exit_points \
 	lscope \
 	interval \
-	typing
+	typing \
+	bound_variables
 SRC_ANALYSES:=$(addprefix src/analyses/, $(SRC_ANALYSES))
 
 # code generator

src/plugins/e-acsl/doc/Changelog

@@ -25,6 +25,9 @@
 Plugin E-ACSL <next-release>
 ############################
 
+-* E-ACSL       [2021-07-30] Fix incorrect evaluation of quantified
+	        predicates when a strict guard overlaps with the type of the
+	        bound variable (unlikely in practice) (frama-c/e-acsl#149).
 -  E-ACSL       [2021-07-06] Add support for the extended quantifier \sum.
 -* E-ACSL       [2021-06-22] Fix a crash that occured when using certain
                 combinations of nested blocks and annotations.

src/plugins/e-acsl/headers/header_spec.txt

@@ -67,6 +67,8 @@ share/e-acsl/observation_model/e_acsl_observation_model.c: CEA_LGPL_OR_PROPRIETA
 share/e-acsl/observation_model/e_acsl_observation_model.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 share/e-acsl/e_acsl.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 share/e-acsl/e_acsl_rtl.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/analyses/bound_variables.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/analyses/bound_variables.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/analyses/exit_points.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/analyses/exit_points.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/analyses/interval.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL

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

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
+(*                                                                        *)
+(*  Copyright (C) 2012-2020                                               *)
+(*    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
+open Cil_datatype
+
+
+val compute_guards: location -> is_forall:bool -> predicate -> Logic_var.t list -> predicate -> unit
+(** Take a predicate starting with a quantifier and store the scope of its variable *)
+
+val get_preprocessed_quantifier: predicate -> (term * logic_var * term) list * predicate
+(** @return the preprocessed of a quantified predicate
+    the [(term * logic_var * term) list] is the list of all the quantified variables
+    along with their syntactic guards, and the [predicate] is the goal: the original
+    predicate with all the quantifiers removed *)
+
+val get_guard_for_small_type : logic_var -> predicate option
+(** @return the optional additional guard for a quantified logic variables. It may
+    happen that the syntactic guard of the variable can be refined with the type
+    of the variable, this additional predicate translates this refinement *)
+
+val clear_guards : unit -> unit
+(** Clear the table of guard conditions for quantified variables *)

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

@@ -231,6 +231,17 @@ let rec interv_of_typ ty = match Cil.unrollType ty with
   | TNamed _ ->
     assert false
 
+let rec extended_interv_of_typ ty = match interv_of_typ ty with
+  | Ival iv ->
+    let l,u = Ival.min_int iv, Ival.max_int iv in
+    let u = match u with
+      | Some u -> Some (Integer.add u Integer.one)
+      | None -> None
+    in
+    Ival (Ival.inject_range l u);
+  | Rational | Real | Nan | Float (_,_) as i
+    -> i
+
 (* Compute the interval of the extended quantifier \sum, \product and \numof.
    [lbd_ival] is the interval of the lambda term, [k_ival] is the interval of the
    quantifier and [name]  is the identifier of the extended quantifier (\sum,

src/plugins/e-acsl/src/analyses/interval.mli

@@ -79,6 +79,13 @@ val interv_of_typ: Cil_types.typ -> t
     @raise Is_a_real if the given type is a float type.
     @raise Not_a_number if the given type does not represent any number. *)
 
+val extended_interv_of_typ: Cil_types.typ -> t
+(** @return the interval [n..m+1] when interv_of_typ returns [n..m].
+    It is in particular useful for computing bounds of quantified variables.
+    @raise Is_a_real if the given type is a float type.
+    @raise Not_a_number if the given type does not represent any number. *)
+
+
 (* ************************************************************************** *)
 (** {3 Environment for interval computations} *)
 (* ************************************************************************** *)

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

@@ -445,7 +445,7 @@ let transfer ~from env = match from.env_stack, env.env_stack with
 type where = Before | Middle | After
 let pop_and_get ?(split=false) env stmt ~global_clear where =
   let split = split && stmt.labels = [] in
-  (*  Options.feedback "pop_and_get from %a (%b)" Printer.pp_stmt stmt split;*)
+  (* Options.feedback "pop_and_get from %a (%b)" Printer.pp_stmt stmt split; *)
   let local_env, tl = top env in
   let clear =
     if global_clear then begin

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

@@ -831,6 +831,7 @@ let reset_all ast =
   Logic_functions.reset ();
   Literal_strings.reset ();
   Global_observer.reset ();
+  Bound_variables.clear_guards ();
   Typing.clear ();
   (* reset some kernel states: *)
   (* reset the CFG that has been heavily modified by the code generation step *)

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

@@ -200,75 +200,15 @@ let handle_annotations env kf stmt =
 (**************************************************************************)
 (**************************** Nested loops ********************************)
 (**************************************************************************)
-
-(* It could happen that the bounds provided for a quantifier [lv] are bigger
-   than its type. [bounds_for_small_type] handles such cases
-   and provides smaller bounds whenever possible.
-   Let B be the inferred interval and R the range of [lv.typ]
-   - Case 1: B \subseteq R
-     Example: [\forall unsigned char c; 4 <= c <= 100 ==> 0 <= c <= 255]
-     Return: B
-   - Case 2: B \not\subseteq R and the bounds of B are inferred exactly
-     Example: [\forall unsigned char c; 4 <= c <= 300 ==> 0 <= c <= 255]
-     Return: B \intersect R
-   - Case 3: B \not\subseteq R and the bounds of B are NOT inferred exactly
-     Example: [\let m = n > 0 ? 4 : 341; \forall char u; 1 < u < m ==> u > 0]
-     Return: R with a guard guaranteeing that [lv] does not overflow *)
-let bounds_for_small_type ~loc (t1, lv, t2) =
-  match lv.lv_type with
-  | Ltype _ | Lvar _ | Lreal | Larrow _ ->
-    Options.abort "quantification over non-integer type is not part of E-ACSL"
-
-  | Linteger ->
-    t1, t2, None
-
-  | Ctype ty ->
-    let iv1 = Interval.(extract_ival (infer t1)) in
-    let iv2 = Interval.(extract_ival (infer t2)) in
-    (* Ival.join is NOT correct here:
-       Eg: (Ival.join [-3..-3] [300..300]) gives {-3, 300}
-       but NOT [-3..300] *)
-    let iv = Ival.inject_range (Ival.min_int iv1) (Ival.max_int iv2) in
-    let ity = Interval.extract_ival (Interval.interv_of_typ ty) in
-    if Ival.is_included iv ity then
-      (* case 1 *)
-      t1, t2, None
-    else if Ival.is_singleton_int iv1 && Ival.is_singleton_int iv2 then begin
-      (* case 2 *)
-      let i = Ival.meet iv ity in
-      (* now we potentially have a better interval for [lv]
-         ==> update the binding *)
-      Interval.Env.replace lv (Interval.Ival i);
-      (* the smaller bounds *)
-      let min, max = Misc.finite_min_and_max i in
-      let t1 = Logic_const.tint ~loc min in
-      let t2 = Logic_const.tint ~loc max in
-      let ctx = Typing.number_ty_of_typ ~post:false ty in
-      (* we are assured that we will not have a GMP,
-         once again because we intersected with [ity] *)
-      Typing.type_term ~use_gmp_opt:false ~ctx t1;
-      Typing.type_term ~use_gmp_opt:false ~ctx t2;
-      t1, t2, None
-    end else
-      (* case 3 *)
-      let min, max = Misc.finite_min_and_max ity in
-      let guard_lower = Logic_const.tint ~loc min in
-      let guard_upper = Logic_const.tint ~loc max in
-      let lv_term = Logic_const.tvar ~loc lv in
-      let guard_lower = Logic_const.prel ~loc (Rle, guard_lower, lv_term) in
-      let guard_upper = Logic_const.prel ~loc (Rle, lv_term, guard_upper) in
-      let guard = Logic_const.pand ~loc (guard_lower, guard_upper) in
-      t1, t2, Some guard
-
 let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
   let term_to_exp = !term_to_exp_ref in
   match lscope_vars with
   | [] ->
     mk_innermost_block env
   | Lscope.Lvs_quantif(t1, rel1, logic_x, rel2, t2) :: lscope_vars' ->
-    let t1, t2, guard_for_small_type_opt =
-      bounds_for_small_type ~loc (t1, logic_x, t2)
-    in
+    assert (rel1 == Rle && rel2 == Rlt);
+    Typing.type_term ~use_gmp_opt:false t1;
+    Typing.type_term ~use_gmp_opt:false t2;
     let ctx =
       let ty1 = Typing.get_number_ty t1 in
       let ty2 = Typing.get_number_ty t2 in
@@ -286,41 +226,14 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
         ty;
       res
     in
-    let t1 = match rel1 with
-      | Rlt ->
-        let t = t_plus_one t1 in
-        Typing.type_term ~use_gmp_opt:false ~ctx t;
-        t
-      | Rle ->
-        t1
-      | Rgt | Rge | Req | Rneq ->
-        assert false
-    in
-    let t2_one, bop2 = match rel2 with
-      | Rlt ->
-        t2, Lt
-      | Rle ->
-        (* we increment the loop counter one more time (at the end of the
-           loop). Thus to prevent overflow, check the type of [t2+1]
-           instead of [t2]. *)
-        t_plus_one t2, Le
-      | Rgt | Rge | Req | Rneq ->
-        assert false
-    in
-    Typing.type_term ~use_gmp_opt:false ~ctx t2_one;
-    let ctx_one =
-      let ty1 = Typing.get_number_ty t1 in
-      let ty2 = Typing.get_number_ty t2_one in
-      Typing.join ty1 ty2
-    in
     let ty =
-      try Typing.typ_of_number_ty ctx_one
+      try Typing.typ_of_number_ty ctx
       with Typing.Not_a_number -> assert false
     in
     (* loop counter corresponding to the quantified variable *)
     let var_x, x, env = Env.Logic_binding.add ~ty env kf logic_x in
     let lv_x = var var_x in
-    let env = match ctx_one with
+    let env = match ctx with
       | Typing.C_integer _ -> env
       | Typing.Gmpz -> Env.add_stmt env kf (Gmp.init ~loc x)
       | Typing.(C_float _ | Rational | Real | Nan) -> assert false
@@ -337,13 +250,22 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
         ~global_clear:false
         Env.Middle
     in
-    (* generate the guard [x bop t2] *)
+    (* generate the guard [x < t2] *)
     let block_to_stmt b = Smart_stmt.block_stmt b in
     let tlv = Logic_const.tvar ~loc logic_x in
+    (* if [t2] is of the form [t2'+1], generate the guard [x <= t2']
+       to avoid the extra addition (relevant when computing with GMP) *)
     let guard =
-      (* must copy [t2] to force being typed again *)
-      Logic_const.term ~loc
-        (TBinOp(bop2, tlv, { t2 with term_node = t2.term_node } )) Linteger
+      match t2.term_node with
+      | TBinOp (PlusA, t2_minus_one, {term_node = TConst(Integer (n, _))}) when Integer.is_one n ->
+        Logic_const.term ~loc
+          (TBinOp(Le, tlv, { t2_minus_one with term_node = t2_minus_one.term_node }))
+          Linteger
+      | _ ->
+        (* must copy [t2] to force it being typed again *)
+        Logic_const.term ~loc
+          (TBinOp(Lt, tlv, { t2 with term_node = t2.term_node } ))
+          Linteger
     in
     Typing.type_term ~use_gmp_opt:false ~ctx:Typing.c_int guard;
     let guard_exp, env = term_to_exp kf (Env.push env) guard in
@@ -361,7 +283,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
     let guard = block_to_stmt guard_blk in
     (* increment the loop counter [x++];
        previous typing ensures that [x++] fits type [ty] *)
-    let tlv_one = t_plus_one ~ty:ctx_one tlv in
+    let tlv_one = t_plus_one ~ty:ctx tlv in
     let incr, env = term_to_exp kf (Env.push env) tlv_one in
     let next_blk, env = Env.pop_and_get
         env
@@ -371,6 +293,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
     in
     (* generate the whole loop *)
     let next = block_to_stmt next_blk in
+    let guard_for_small_type_opt = Bound_variables.get_guard_for_small_type logic_x in
     let stmts, env = match guard_for_small_type_opt with
       | None ->
         guard :: body @ [ next ], env

src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.res.oracle

@@ -24,7 +24,7 @@
   assert
   \initialized(__gen_e_acsl_at_6 +
                (int)((int)((int)(__gen_e_acsl_u_3 - 9) * 32) +
-                     (int)((int)(__gen_e_acsl_v_3 - -5) - 1)));
+                     (int)(__gen_e_acsl_v_3 - -4)));
 [eva:alarm] tests/arith/at_on-purely-logic-variables.c:45: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] tests/arith/at_on-purely-logic-variables.c:43: Warning: 

src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c

@@ -142,9 +142,9 @@ int main(void)
               int __gen_e_acsl_u_7;
               __gen_e_acsl_u_7 = 42;
               *(__gen_e_acsl_at_7 + ((__gen_e_acsl_u_6 - 10) * 300 + (
-                                     ((__gen_e_acsl_v_6 - -10) - 1) * 100 + (
-                                     (__gen_e_acsl_w_2 - 100) - 1)))) = 
-              (((n - (long)__gen_e_acsl_u_6) + __gen_e_acsl_u_7) + __gen_e_acsl_v_6) + __gen_e_acsl_w_2 > 0L;
+                                     (__gen_e_acsl_v_6 - -9) * 100 + (
+                                     __gen_e_acsl_w_2 - 101)))) = (((
+                                                                    n - (long)__gen_e_acsl_u_6) + __gen_e_acsl_u_7) + __gen_e_acsl_v_6) + __gen_e_acsl_w_2 > 0L;
             }
             __gen_e_acsl_w_2 ++;
           }
@@ -167,7 +167,7 @@ int main(void)
             else __gen_e_acsl_if_2 = 3;
             if (__gen_e_acsl_v_4 <= __gen_e_acsl_if_2) ; else break;
           }
-          *(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_4 - 9) * 32 + ((__gen_e_acsl_v_4 - -5) - 1))) = 
+          *(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_4 - 9) * 32 + (__gen_e_acsl_v_4 - -4))) = 
           (n + (long)__gen_e_acsl_u_4) + __gen_e_acsl_v_4 > 0L;
           __gen_e_acsl_v_4 ++;
         }
@@ -189,7 +189,7 @@ int main(void)
             long __gen_e_acsl_if;
             if (__gen_e_acsl_u_2 > 0) __gen_e_acsl_if = n + (long)__gen_e_acsl_k_2;
             else __gen_e_acsl_if = __gen_e_acsl_u_2 + __gen_e_acsl_v_2;
-            *(__gen_e_acsl_at_3 + ((__gen_e_acsl_u_2 - 9) * 11 + ((__gen_e_acsl_v_2 - -5) - 1))) = 
+            *(__gen_e_acsl_at_3 + ((__gen_e_acsl_u_2 - 9) * 11 + (__gen_e_acsl_v_2 - -4))) = 
             __gen_e_acsl_if > 0L;
           }
           __gen_e_acsl_v_2 ++;
@@ -271,15 +271,14 @@ int main(void)
                                                             (long)((int)(
                                                             (long)((int)(
                                                             __gen_e_acsl_u - 9L)) * 11L)) + (int)(
-                                                            (int)(__gen_e_acsl_v - -5L) - 1))),
+                                                            __gen_e_acsl_v - -4L))),
                                                             sizeof(int),
                                                             (void *)__gen_e_acsl_at_3,
                                                             (void *)(& __gen_e_acsl_at_3));
             __e_acsl_assert(__gen_e_acsl_valid_read_3,1,"RTE","main",
-                            "mem_access:\n  \\valid_read(__gen_e_acsl_at_3 +\n              (int)((int)((int)(__gen_e_acsl_u - 9) * 11) +\n                    (int)((int)(__gen_e_acsl_v - -5) - 1)))",
+                            "mem_access:\n  \\valid_read(__gen_e_acsl_at_3 +\n              (int)((int)((int)(__gen_e_acsl_u - 9) * 11) +\n                    (int)(__gen_e_acsl_v - -4)))",
                             "tests/arith/at_on-purely-logic-variables.c",34);
-            if (*(__gen_e_acsl_at_3 + ((__gen_e_acsl_u - 9) * 11 + ((
-                                                                    __gen_e_acsl_v - -5) - 1)))) 
+            if (*(__gen_e_acsl_at_3 + ((__gen_e_acsl_u - 9) * 11 + (__gen_e_acsl_v - -4)))) 
               ;
             else {
               __gen_e_acsl_forall = 0;
@@ -333,7 +332,7 @@ int main(void)
       __gen_e_acsl_k_4 = -9 + 1;
       while (1) {
         if (__gen_e_acsl_k_4 < 0) ; else break;
-        *(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_4 - -9) - 1)) = m + (long)__gen_e_acsl_k_4;
+        *(__gen_e_acsl_at_5 + (__gen_e_acsl_k_4 - -8)) = m + (long)__gen_e_acsl_k_4;
         __gen_e_acsl_k_4 ++;
       }
     }
@@ -349,16 +348,15 @@ int main(void)
       if (__gen_e_acsl_k_3 < 0) ; else break;
       {
         int __gen_e_acsl_valid_read_5;
-        __gen_e_acsl_valid_read_5 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_5 + (
-                                                                 (int)(
-                                                                 __gen_e_acsl_k_3 - -9L) - 1)),
+        __gen_e_acsl_valid_read_5 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_5 + (int)(
+                                                                 __gen_e_acsl_k_3 - -8L)),
                                                         sizeof(long),
                                                         (void *)__gen_e_acsl_at_5,
                                                         (void *)(& __gen_e_acsl_at_5));
         __e_acsl_assert(__gen_e_acsl_valid_read_5,1,"RTE","main",
-                        "mem_access:\n  \\valid_read(__gen_e_acsl_at_5 + (int)((int)(__gen_e_acsl_k_3 - -9) - 1))",
+                        "mem_access: \\valid_read(__gen_e_acsl_at_5 + (int)(__gen_e_acsl_k_3 - -8))",
                         "tests/arith/at_on-purely-logic-variables.c",41);
-        if (! (*(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_3 - -9) - 1)) == 0L)) 
+        if (! (*(__gen_e_acsl_at_5 + (__gen_e_acsl_k_3 - -8)) == 0L)) 
           ;
         else {
           __gen_e_acsl_exists_3 = 1;
@@ -399,23 +397,21 @@ int main(void)
                                                             (long)((int)(
                                                             (long)((int)(
                                                             __gen_e_acsl_u_3 - 9L)) * 32L)) + (int)(
-                                                            (int)(__gen_e_acsl_v_3 - -5L) - 1))),
+                                                            __gen_e_acsl_v_3 - -4L))),
                                                             sizeof(int),
                                                             (void *)__gen_e_acsl_at_6,
                                                             (void *)(& __gen_e_acsl_at_6));
             __e_acsl_assert(__gen_e_acsl_valid_read_6,1,"RTE","main",
-                            "mem_access:\n  \\valid_read(__gen_e_acsl_at_6 +\n              (int)((int)((int)(__gen_e_acsl_u_3 - 9) * 32) +\n                    (int)((int)(__gen_e_acsl_v_3 - -5) - 1)))",
+                            "mem_access:\n  \\valid_read(__gen_e_acsl_at_6 +\n              (int)((int)((int)(__gen_e_acsl_u_3 - 9) * 32) +\n                    (int)(__gen_e_acsl_v_3 - -4)))",
                             "tests/arith/at_on-purely-logic-variables.c",45);
             /*@ assert
                 Eva: initialization:
                   \initialized(__gen_e_acsl_at_6 +
                                (int)((int)((int)(__gen_e_acsl_u_3 - 9) * 32)
-                                     +
-                                     (int)((int)(__gen_e_acsl_v_3 - -5) - 1)));
+                                     + (int)(__gen_e_acsl_v_3 - -4)));
             */
             if (*(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_3 - 9) * 32 + (
-                                       (__gen_e_acsl_v_3 - -5) - 1)))) 
-              ;
+                                       __gen_e_acsl_v_3 - -4)))) ;
             else {
               __gen_e_acsl_forall_2 = 0;
               goto e_acsl_end_loop6;
@@ -483,20 +479,18 @@ int main(void)
                                                                 __gen_e_acsl_u_5 - 10L)) * 300L)) + (int)(
                                                                 (long)((int)(
                                                                 (long)((int)(
-                                                                (int)(
-                                                                __gen_e_acsl_v_5 - -10L) - 1)) * 100L)) + (int)(
-                                                                (long)((int)(
-                                                                __gen_e_acsl_w - 100L)) - 1L)))),
+                                                                __gen_e_acsl_v_5 - -9L)) * 100L)) + (int)(
+                                                                __gen_e_acsl_w - 101L)))),
                                                                 sizeof(int),
                                                                 (void *)__gen_e_acsl_at_7,
                                                                 (void *)(& __gen_e_acsl_at_7));
                 __e_acsl_assert(__gen_e_acsl_valid_read_7,1,"RTE","main",
-                                "mem_access:\n  \\valid_read(__gen_e_acsl_at_7 +\n              (int)((int)((int)(__gen_e_acsl_u_5 - 10) * 300) +\n                    (int)((int)((int)((int)(__gen_e_acsl_v_5 - -10) - 1) *\n                                100)\n                          + (int)((int)(__gen_e_acsl_w - 100) - 1))))",
+                                "mem_access:\n  \\valid_read(__gen_e_acsl_at_7 +\n              (int)((int)((int)(__gen_e_acsl_u_5 - 10) * 300) +\n                    (int)((int)((int)(__gen_e_acsl_v_5 - -9) * 100) +\n                          (int)(__gen_e_acsl_w - 101))))",
                                 "tests/arith/at_on-purely-logic-variables.c",
                                 57);
                 if (! *(__gen_e_acsl_at_7 + ((__gen_e_acsl_u_5 - 10) * 300 + (
-                                             ((__gen_e_acsl_v_5 - -10) - 1) * 100 + (
-                                             (__gen_e_acsl_w - 100) - 1))))) 
+                                             (__gen_e_acsl_v_5 - -9) * 100 + (
+                                             __gen_e_acsl_w - 101))))) 
                   ;
                 else {
                   __gen_e_acsl_exists_7 = 1;
@@ -617,8 +611,7 @@ void __gen_e_acsl_f(int *t)
         __e_acsl_assert(__gen_e_acsl_valid_read_3,1,"RTE","f",
                         "mem_access: \\valid_read(t + (int)(__gen_e_acsl_n_3 - 1))",
                         "tests/arith/at_on-purely-logic-variables.c",7);
-        *(__gen_e_acsl_at_2 + ((__gen_e_acsl_n_3 - 1) - 1)) = *(t + (
-                                                                __gen_e_acsl_n_3 - 1)) > 5;
+        *(__gen_e_acsl_at_2 + (__gen_e_acsl_n_3 - 2)) = *(t + (__gen_e_acsl_n_3 - 1)) > 5;
       }
       __gen_e_acsl_n_3 ++;
     }
@@ -636,7 +629,7 @@ void __gen_e_acsl_f(int *t)
         __e_acsl_assert(__gen_e_acsl_valid_read,1,"RTE","f",
                         "mem_access: \\valid_read(t + __gen_e_acsl_n_2)",
                         "tests/arith/at_on-purely-logic-variables.c",7);
-        *(__gen_e_acsl_at + ((__gen_e_acsl_n_2 - 1) - 1)) = *(t + __gen_e_acsl_n_2) == 12;
+        *(__gen_e_acsl_at + (__gen_e_acsl_n_2 - 2)) = *(t + __gen_e_acsl_n_2) == 12;
       }
       __gen_e_acsl_n_2 ++;
     }
@@ -656,26 +649,24 @@ void __gen_e_acsl_f(int *t)
         int __gen_e_acsl_valid_read_2;
         int __gen_e_acsl_and;
         __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(__gen_e_acsl_at + (int)(
-                                                                 (long)((int)(
-                                                                 __gen_e_acsl_n - 1L)) - 1L)),
+                                                                 __gen_e_acsl_n - 2L)),
                                                         sizeof(int),
                                                         (void *)__gen_e_acsl_at,
                                                         (void *)(& __gen_e_acsl_at));
         __e_acsl_assert(__gen_e_acsl_valid_read_2,1,"RTE","f",
-                        "mem_access:\n  \\valid_read(__gen_e_acsl_at + (int)((int)(__gen_e_acsl_n - 1) - 1))",
+                        "mem_access: \\valid_read(__gen_e_acsl_at + (int)(__gen_e_acsl_n - 2))",
                         "tests/arith/at_on-purely-logic-variables.c",7);
-        if (*(__gen_e_acsl_at + ((__gen_e_acsl_n - 1) - 1))) {
+        if (*(__gen_e_acsl_at + (__gen_e_acsl_n - 2))) {
           int __gen_e_acsl_valid_read_4;
           __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_2 + (int)(
-                                                                   (long)((int)(
-                                                                   __gen_e_acsl_n - 1L)) - 1L)),
+                                                                   __gen_e_acsl_n - 2L)),
                                                           sizeof(int),
                                                           (void *)__gen_e_acsl_at_2,
                                                           (void *)(& __gen_e_acsl_at_2));
           __e_acsl_assert(__gen_e_acsl_valid_read_4,1,"RTE","f",
-                          "mem_access:\n  \\valid_read(__gen_e_acsl_at_2 + (int)((int)(__gen_e_acsl_n - 1) - 1))",
+                          "mem_access: \\valid_read(__gen_e_acsl_at_2 + (int)(__gen_e_acsl_n - 2))",
                           "tests/arith/at_on-purely-logic-variables.c",7);
-          __gen_e_acsl_and = *(__gen_e_acsl_at_2 + ((__gen_e_acsl_n - 1) - 1));
+          __gen_e_acsl_and = *(__gen_e_acsl_at_2 + (__gen_e_acsl_n - 2));
         }
         else __gen_e_acsl_and = 0;
         if (__gen_e_acsl_and) ;

src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c

@@ -314,7 +314,7 @@ int main(void)
         {
           __e_acsl_mpz_t __gen_e_acsl__2;
           __e_acsl_mpz_t __gen_e_acsl_add;
-          __gmpz_init_set_ui(__gen_e_acsl__2,1UL);
+          __gmpz_init_set_str(__gen_e_acsl__2,"1",10);
           __gmpz_init(__gen_e_acsl_add);
           __gmpz_add(__gen_e_acsl_add,
                      (__e_acsl_mpz_struct const *)(__gen_e_acsl_i_4),

src/plugins/e-acsl/tests/bts/issue-eacsl-149.c

+#include <limits.h>
+
+int main (int argc, char *argv[]) {
+  /*@ assert \exists unsigned int x; -1 < x < 5 && x == 0;*/
+  /*@ assert !(\forall unsigned int x; -1 < x < 5 ==> x != 0);*/
+  return 0;
+}

src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-149.c

+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdio.h"
+int main(int argc, char **argv)
+{
+  int __retres;
+  {
+    int __gen_e_acsl_exists;
+    int __gen_e_acsl_x;
+    __gen_e_acsl_exists = 0;
+    /*@ assert
+        Eva: signed_overflow: (unsigned int)((int)(-1)) + 1 ≤ 2147483647;
+    */
+    __gen_e_acsl_x = (unsigned int)(-1) + 1;
+    while (1) {
+      if (__gen_e_acsl_x < 5) ; else break;
+      if (! (__gen_e_acsl_x == 0)) ;
+      else {
+        __gen_e_acsl_exists = 1;
+        goto e_acsl_end_loop1;
+      }
+      __gen_e_acsl_x ++;
+    }
+    e_acsl_end_loop1: ;
+    __e_acsl_assert(__gen_e_acsl_exists,1,"Assertion","main",
+                    "\\exists unsigned int x; -1 < x < 5 && x == 0",
+                    "tests/bts/issue-eacsl-149.c",4);
+  }
+  /*@ assert ∃ unsigned int x; -1 < x < 5 ∧ x ≡ 0; */ ;
+  {
+    int __gen_e_acsl_forall;
+    int __gen_e_acsl_x_2;
+    __gen_e_acsl_forall = 1;
+    __gen_e_acsl_x_2 = (unsigned int)(-1) + 1;
+    while (1) {
+      if (__gen_e_acsl_x_2 < 5) ; else break;
+      if (__gen_e_acsl_x_2 != 0) ;
+      else {
+        __gen_e_acsl_forall = 0;
+        goto e_acsl_end_loop2;
+      }
+      __gen_e_acsl_x_2 ++;
+    }
+    e_acsl_end_loop2: ;
+    __e_acsl_assert(! __gen_e_acsl_forall,1,"Assertion","main",
+                    "!(\\forall unsigned int x; -1 < x < 5 ==> x != 0)",
+                    "tests/bts/issue-eacsl-149.c",5);
+  }
+  /*@ assert ¬(∀ unsigned int x; -1 < x < 5 ⇒ x ≢ 0); */ ;
+  __retres = 0;
+  return __retres;
+}
+
+

src/plugins/e-acsl/tests/bts/oracle/gen_issue69.c

@@ -10,7 +10,7 @@ int main(void)
     __gen_e_acsl_forall = 1;
     __gen_e_acsl_c = (unsigned char)4;
     while (1) {
-      if (__gen_e_acsl_c <= 255) ; else break;
+      if (__gen_e_acsl_c < 256) ; else break;
       {
         int __gen_e_acsl_and;
         if (0 <= __gen_e_acsl_c) __gen_e_acsl_and = __gen_e_acsl_c <= 255;
@@ -42,9 +42,9 @@ int main(void)
     while (1) {
       {
         int __gen_e_acsl_and_2;
-        if (-128 <= __gen_e_acsl_u) __gen_e_acsl_and_2 = __gen_e_acsl_u <= 127;
+        if (-128 <= __gen_e_acsl_u) __gen_e_acsl_and_2 = __gen_e_acsl_u < 128;
         else __gen_e_acsl_and_2 = 0;
-        __e_acsl_assert(__gen_e_acsl_and_2,1,"RTE","main","-128 <= u <= 127",
+        __e_acsl_assert(__gen_e_acsl_and_2,1,"RTE","main","-128 <= u < 128",
                         "tests/bts/issue69.c",11);
       }
       if (__gen_e_acsl_u < __gen_e_acsl_m) ; else break;

src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-149.res.oracle

+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/bts/issue-eacsl-149.c:4: Warning: 
+  signed overflow. assert (unsigned int)((int)(-1)) + 1 ≤ 2147483647;