[e-acsl] fourth review

src/plugins/e-acsl/doc/Changelog

@@ -31,6 +31,7 @@ Plugin E-ACSL 25.0 (Manganese)
 ##############################
 
 -* E-ACSL       [2022-23-05] Fix crash for quantifications over enum types (frama-c/e-acsl#199)
+-*  E-ACSL      [2022-06-09] Fix wrong cast of pointer to integer (frama-c/frama-c#1119)
 -  E-ACSL       [2022-03-04] Improve translation of `\at()` terms and
                 predicates (frama-c/e-acsl#108).
 -* E-ACSL       [2022-03-01] Fix normalization of global annotations that

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

@@ -68,6 +68,7 @@ type annotation_kind =
   | Variant
   | RTE
 
+(** Type of intervals infered by the interval inference *)
 type ival =
   | Ival of Ival.t
   | Float of fkind * float option (* a float constant, if any *)
@@ -75,6 +76,7 @@ type ival =
   | Real
   | Nan
 
+(** Type of types infered by the type inference for types representing numbers *)
 type number_ty =
   | C_integer of ikind
   | C_float of fkind

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

@@ -357,13 +357,15 @@ let rec fixpoint ~(infer : force:bool ->
     li args_ival t' ival =
   let get_res = Error.map (fun x -> x) in
   let logic_env = Logic_env.make args_ival in
+  (* If the logic function has a given C type, we use this type to infer the
+     interval. Otherwise we compute this interval as a fixpoint *)
   match li.l_type with
   | Some (Ctype typ) ->
     let ival = interv_of_typ typ in
     LF_env.add li args_ival ival;
     ignore (infer ~force:true ~logic_env t');
     ival
-  | _ ->
+  | None | Some (Linteger | Lreal | Ltype _ | Lvar _ | Larrow _) ->
     LF_env.replace li args_ival ival;
     let inferred_ival = get_res (infer ~force:true ~logic_env t') in
     if is_included inferred_ival ival
@@ -744,11 +746,14 @@ let rec infer ~force ~logic_env t =
                fixpoint ~infer li widened_profile t' (Ival Ival.bottom))
           | LBterm t' ->
             let logic_env = Logic_env.make profile in
+            (* If the logic function returns a C type, then its application
+               ranges inside this C type *)
             (match li.l_type with
-             | Some (Ctype (typ)) ->
+             | Some (Ctype typ) ->
                ignore ((infer ~force ~logic_env t'));
                interv_of_typ typ;
-             | _ -> get_res (infer ~force ~logic_env t'))
+             | None | Some (Linteger | Lreal | Ltype _ | Lvar _ | Larrow _) ->
+               get_res (infer ~force ~logic_env t'))
           | _ -> assert false)
        | LBnone when li.l_var_info.lv_name = "\\sum" ||
                      li.l_var_info.lv_name = "\\product" ->

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

@@ -43,8 +43,6 @@ let pending_typing : (unit -> unit) Stack.t = Stack.create ()
 (** Datatype and constructor *)
 (******************************************************************************)
 
-module D = Number_ty
-
 let ikind ik = C_integer ik
 let c_int = ikind IInt
 let gmpz = Gmpz
@@ -73,7 +71,9 @@ let join ty1 ty2 =
       assert false
     | Nan, (C_integer _ | C_float _ | Gmpz | Rational | Real as ty)
     | (C_integer _ | C_float _ | Gmpz | Rational | Real as ty), Nan ->
-      Options.fatal "[typing] join failure: number %a and nan" D.pretty ty
+      Options.fatal "[typing] join failure: number %a and nan"
+        Number_ty.pretty
+        ty
     | Real, (C_integer _ | C_float _ | Gmpz | Rational)
     | (C_integer _ | C_float _ | Rational | Gmpz), Real ->
       Real
@@ -115,10 +115,10 @@ let typ_of_lty = function
 (******************************************************************************)
 
 type computed_info =
-  { ty: D.t;  (* type required for the term *)
-    op: D.t; (* type required for the operation *)
-    cast: D.t option; (* if not [None], type of the context which the term
-                         must be casted to. If [None], no cast needed. *)
+  { ty: Number_ty.t;  (* type required for the term *)
+    op: Number_ty.t; (* type required for the operation *)
+    cast: Number_ty.t option; (* if not [None], type of the context which the term
+                                 must be casted to. If [None], no cast needed. *)
   }
 
 (* Memoization module which retrieves the computed info of some terms. If the
@@ -255,7 +255,7 @@ let ty_of_interv ?ctx ?(use_gmp_opt = false) = function
 (* compute a new {!computed_info} by coercing the given type [ty] to the given
    context [ctx]. [op] is the type for the operator. *)
 let coerce ~arith_operand ~ctx ~op ty =
-  if D.compare ty ctx = 1 then
+  if Number_ty.compare ty ctx = 1 then
     (* type larger than the expected context,
        so we must introduce an explicit cast *)
     { ty; op; cast = Some ctx }
@@ -416,13 +416,17 @@ let rec type_term
         | _ -> true
       in
       let cast_first = cast_first t1 t2 in
-      ignore (type_term ~use_gmp_opt:true ~arith_operand:cast_first ~ctx ~profile t1);
+      ignore
+        (type_term ~use_gmp_opt:true ~arith_operand:cast_first ~ctx ~profile t1);
       ignore
         (type_term ~use_gmp_opt:true ~arith_operand:(not cast_first) ~ctx ~profile t2);
       dup ctx_res
 
     | TBinOp ((Lt | Gt | Le | Ge | Eq | Ne), t1, t2) ->
-      assert (match ctx with None -> true | Some c -> D.compare c c_int >= 0);
+      assert
+        (match ctx with
+         |None -> true
+         | Some c -> Number_ty.compare c c_int >= 0);
       let i1 = Interval.get_from_profile ~profile t1 in
       let i2 = Interval.get_from_profile ~profile t2 in
       let ctx =
@@ -589,10 +593,24 @@ let rec type_term
                     ~profile:new_profile
                     t_body))
             pending_typing;
+          (* If the logic function has a given C number type, we generate a
+             function returning this type, otherwise we use the interval
+             inference *)
           (match li.l_type with
            | Some (Ctype (TInt (ikind, _))) ->
              dup (C_integer ikind)
-           | _ ->
+           | Some (Ctype (TFloat (fkind, _))) ->
+             dup (C_float fkind)
+           | None
+           | Some (Ctype (TVoid _
+                         | TPtr _
+                         | TEnum _
+                         | TArray _
+                         | TFun _
+                         | TNamed _
+                         | TComp _
+                         | TBuiltin_va_list _))
+           | Some (Linteger | Lreal | Ltype _ | Lvar _ | Larrow _) ->
              dup (ty_of_interv
                     ?ctx:ctx_body
                     ~use_gmp_opt:(gmp && use_gmp_opt)
@@ -812,7 +830,7 @@ and type_predicate ~profile p =
 
 let type_term ~use_gmp_opt ?ctx ~profile t =
   Options.feedback ~dkey ~level:4 "typing term '%a' in ctx '%a'."
-    Printer.pp_term t (Pretty_utils.pp_opt D.pretty) ctx;
+    Printer.pp_term t (Pretty_utils.pp_opt Number_ty.pretty) ctx;
   ignore (type_term ~use_gmp_opt ?ctx ~profile t);
   while not (Stack.is_empty pending_typing) do
     Stack.pop pending_typing ()

src/plugins/e-acsl/tests/bts/issue-framac-1119.c

+/* run.config
+   COMMENT: cf issue framac#1119
+*/
+
+#include <limits.h>
+#include <stddef.h>
+
+int find_last_of(int const *a, int len, int value) {
+  //@ ghost size_t o = len ;
+  //@ loop invariant \forall integer i ; len <= i < o ==> a[i] != value ;
+  while (len) {
+    len--;
+  }
+  return INT_MAX;
+}
+int main(void) {
+  int a[1] = {1};
+  find_last_of(a, 1, 0);
+}

src/plugins/e-acsl/tests/bts/oracle/gen_issue-framac-1119.c

+/* Generated by Frama-C */
+#include "pthread.h"
+#include "sched.h"
+#include "signal.h"
+#include "stddef.h"
+#include "stdint.h"
+#include "stdio.h"
+#include "time.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
+int find_last_of(int const *a, int len, int value)
+{
+  int __retres;
+  __e_acsl_store_block((void *)(& a),8UL);
+  size_t o = (size_t)len;
+  {
+    int __gen_e_acsl_forall;
+    __e_acsl_mpz_t __gen_e_acsl_i;
+    __e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
+    __gen_e_acsl_forall = 1;
+    __gmpz_init(__gen_e_acsl_i);
+    {
+      __e_acsl_mpz_t __gen_e_acsl_len;
+      __gmpz_init_set_si(__gen_e_acsl_len,(long)len);
+      __gmpz_set(__gen_e_acsl_i,
+                 (__e_acsl_mpz_struct const *)(__gen_e_acsl_len));
+      __gmpz_clear(__gen_e_acsl_len);
+    }
+    while (1) {
+      {
+        __e_acsl_mpz_t __gen_e_acsl_o;
+        int __gen_e_acsl_lt;
+        __gmpz_init_set_ui(__gen_e_acsl_o,o);
+        __gen_e_acsl_lt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_i),
+                                     (__e_acsl_mpz_struct const *)(__gen_e_acsl_o));
+        if (__gen_e_acsl_lt < 0) ; else break;
+        __gmpz_clear(__gen_e_acsl_o);
+      }
+      {
+        long __gen_e_acsl_i_2;
+        int __gen_e_acsl_valid_read;
+        __gen_e_acsl_i_2 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_i));
+        __e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
+          {.values = (void *)0};
+        __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(a + __gen_e_acsl_i_2),
+                                                      sizeof(int const),
+                                                      (void *)a,
+                                                      (void *)(& a));
+        __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,"a",
+                                     (void *)a);
+        __e_acsl_assert_register_long(& __gen_e_acsl_assert_data_2,
+                                      "__gen_e_acsl_i_2",0,__gen_e_acsl_i_2);
+        __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_2,
+                                       "sizeof(int const)",0,
+                                       sizeof(int const));
+        __gen_e_acsl_assert_data_2.blocking = 1;
+        __gen_e_acsl_assert_data_2.kind = "RTE";
+        __gen_e_acsl_assert_data_2.pred_txt = "\\valid_read(a + __gen_e_acsl_i_2)";
+        __gen_e_acsl_assert_data_2.file = "issue-framac-1119.c";
+        __gen_e_acsl_assert_data_2.fct = "find_last_of";
+        __gen_e_acsl_assert_data_2.line = 10;
+        __gen_e_acsl_assert_data_2.name = "mem_access";
+        __e_acsl_assert(__gen_e_acsl_valid_read,& __gen_e_acsl_assert_data_2);
+        __e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
+        /*@ assert Eva: mem_access: \valid_read(a + __gen_e_acsl_i_2); */
+        if (*(a + __gen_e_acsl_i_2) != value) ;
+        else {
+          __gen_e_acsl_forall = 0;
+          goto e_acsl_end_loop1;
+        }
+      }
+      {
+        __e_acsl_mpz_t __gen_e_acsl_;
+        __e_acsl_mpz_t __gen_e_acsl_add;
+        __gmpz_init_set_str(__gen_e_acsl_,"1",10);
+        __gmpz_init(__gen_e_acsl_add);
+        __gmpz_add(__gen_e_acsl_add,
+                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_i),
+                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+        __gmpz_set(__gen_e_acsl_i,
+                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+        __gmpz_clear(__gen_e_acsl_);
+        __gmpz_clear(__gen_e_acsl_add);
+      }
+    }
+    e_acsl_end_loop1: ;
+    __e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
+                                 "\\forall integer i; len <= i < o ==> *(a + i) != value",
+                                 0,__gen_e_acsl_forall);
+    __gen_e_acsl_assert_data.blocking = 1;
+    __gen_e_acsl_assert_data.kind = "Invariant";
+    __gen_e_acsl_assert_data.pred_txt = "\\forall integer i; len <= i < o ==> *(a + i) != value";
+    __gen_e_acsl_assert_data.file = "issue-framac-1119.c";
+    __gen_e_acsl_assert_data.fct = "find_last_of";
+    __gen_e_acsl_assert_data.line = 10;
+    __e_acsl_assert(__gen_e_acsl_forall,& __gen_e_acsl_assert_data);
+    __e_acsl_assert_clean(& __gen_e_acsl_assert_data);
+    __gmpz_clear(__gen_e_acsl_i);
+  }
+  /*@ loop invariant \forall integer i; len <= i < o ==> *(a + i) != value;
+  */
+  while (len) {
+    int __gen_e_acsl_forall_2;
+    __e_acsl_mpz_t __gen_e_acsl_i_3;
+    len --;
+    __e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
+      {.values = (void *)0};
+    __gen_e_acsl_forall_2 = 1;
+    __gmpz_init(__gen_e_acsl_i_3);
+    {
+      __e_acsl_mpz_t __gen_e_acsl_len_2;
+      __gmpz_init_set_si(__gen_e_acsl_len_2,(long)len);
+      __gmpz_set(__gen_e_acsl_i_3,
+                 (__e_acsl_mpz_struct const *)(__gen_e_acsl_len_2));
+      __gmpz_clear(__gen_e_acsl_len_2);
+    }
+    while (1) {
+      {
+        __e_acsl_mpz_t __gen_e_acsl_o_2;
+        int __gen_e_acsl_lt_2;
+        __gmpz_init_set_ui(__gen_e_acsl_o_2,o);
+        __gen_e_acsl_lt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_i_3),
+                                       (__e_acsl_mpz_struct const *)(__gen_e_acsl_o_2));
+        if (__gen_e_acsl_lt_2 < 0) ; else break;
+        __gmpz_clear(__gen_e_acsl_o_2);
+      }
+      {
+        long __gen_e_acsl_i_4;
+        int __gen_e_acsl_valid_read_2;
+        __gen_e_acsl_i_4 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_i_3));
+        __e_acsl_assert_data_t __gen_e_acsl_assert_data_4 =
+          {.values = (void *)0};
+        __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(a + __gen_e_acsl_i_4),
+                                                        sizeof(int const),
+                                                        (void *)a,
+                                                        (void *)(& a));
+        __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_4,"a",
+                                     (void *)a);
+        __e_acsl_assert_register_long(& __gen_e_acsl_assert_data_4,
+                                      "__gen_e_acsl_i_4",0,__gen_e_acsl_i_4);
+        __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_4,
+                                       "sizeof(int const)",0,
+                                       sizeof(int const));
+        __gen_e_acsl_assert_data_4.blocking = 1;
+        __gen_e_acsl_assert_data_4.kind = "RTE";
+        __gen_e_acsl_assert_data_4.pred_txt = "\\valid_read(a + __gen_e_acsl_i_4)";
+        __gen_e_acsl_assert_data_4.file = "issue-framac-1119.c";
+        __gen_e_acsl_assert_data_4.fct = "find_last_of";
+        __gen_e_acsl_assert_data_4.line = 10;
+        __gen_e_acsl_assert_data_4.name = "mem_access";
+        __e_acsl_assert(__gen_e_acsl_valid_read_2,
+                        & __gen_e_acsl_assert_data_4);
+        __e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
+        /*@ assert Eva: mem_access: \valid_read(a + __gen_e_acsl_i_4); */
+        if (*(a + __gen_e_acsl_i_4) != value) ;
+        else {
+          __gen_e_acsl_forall_2 = 0;
+          goto e_acsl_end_loop2;
+        }
+      }
+      {
+        __e_acsl_mpz_t __gen_e_acsl__2;
+        __e_acsl_mpz_t __gen_e_acsl_add_2;
+        __gmpz_init_set_str(__gen_e_acsl__2,"1",10);
+        __gmpz_init(__gen_e_acsl_add_2);
+        __gmpz_add(__gen_e_acsl_add_2,
+                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_i_3),
+                   (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+        __gmpz_set(__gen_e_acsl_i_3,
+                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
+        __gmpz_clear(__gen_e_acsl__2);
+        __gmpz_clear(__gen_e_acsl_add_2);
+      }
+    }
+    e_acsl_end_loop2: ;
+    __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,
+                                 "\\forall integer i; len <= i < o ==> *(a + i) != value",
+                                 0,__gen_e_acsl_forall_2);
+    __gen_e_acsl_assert_data_3.blocking = 1;
+    __gen_e_acsl_assert_data_3.kind = "Invariant";
+    __gen_e_acsl_assert_data_3.pred_txt = "\\forall integer i; len <= i < o ==> *(a + i) != value";
+    __gen_e_acsl_assert_data_3.file = "issue-framac-1119.c";
+    __gen_e_acsl_assert_data_3.fct = "find_last_of";
+    __gen_e_acsl_assert_data_3.line = 10;
+    __e_acsl_assert(__gen_e_acsl_forall_2,& __gen_e_acsl_assert_data_3);
+    __e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
+    __gmpz_clear(__gen_e_acsl_i_3);
+  }
+  __retres = 2147483647;
+  __e_acsl_delete_block((void *)(& a));
+  return __retres;
+}
+
+int main(void)
+{
+  int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+  int a[1] = {1};
+  __e_acsl_store_block((void *)(a),4UL);
+  __e_acsl_full_init((void *)(& a));
+  find_last_of((int const *)(a),1,0);
+  __retres = 0;
+  __e_acsl_delete_block((void *)(a));
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+

src/plugins/e-acsl/tests/bts/oracle/issue-framac-1119.res.oracle

+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] :0: Warning: 
+  function __e_acsl_assert_register_long: precondition data->values == \null ||
+                                                       \valid(data->values) got status unknown.
+[eva:alarm] issue-framac-1119.c:10: Warning: 
+  function __e_acsl_assert_register_ulong: precondition data->values == \null ||
+                                                        \valid(data->values) got status unknown.
+[eva:alarm] issue-framac-1119.c:10: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] issue-framac-1119.c:10: Warning: 
+  out of bounds read. assert \valid_read(a + __gen_e_acsl_i_2);
+[eva:alarm] issue-framac-1119.c:10: Warning: 
+  out of bounds read. assert \valid_read(a + __gen_e_acsl_i_4);