diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 7b213fa5830e2d23285b1355104a7945e19c1ce3..4e1518fa0f105c7e4743c817b627c614aca41896 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/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
diff --git a/src/plugins/e-acsl/src/analyses/analyses_types.mli b/src/plugins/e-acsl/src/analyses/analyses_types.mli
index 01fc71a0b6491d0ac4f16b6f4a5ab7873af8868e..4a00a6fa9a2b5629c3fba2fc1e910939eaf43ef6 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_types.mli
+++ b/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
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index e66801dce797d4c965efb5ee438f851b97aea65d..f68cae7dcf7b99d17e06792c8fc7208ba865af0c 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/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" ->
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index 73b3208852b166bfa749ac1cfffe76881082fc07..2be2dfe179740e5b98913c43b2c297fa783bed13 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/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 ()
diff --git a/src/plugins/e-acsl/tests/bts/issue-framac-1119.c b/src/plugins/e-acsl/tests/bts/issue-framac-1119.c
new file mode 100644
index 0000000000000000000000000000000000000000..44383d02f3f5ecb0659b26266f89941c22d9210f
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/issue-framac-1119.c
@@ -0,0 +1,19 @@
+/* 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);
+}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-framac-1119.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-framac-1119.c
new file mode 100644
index 0000000000000000000000000000000000000000..35d3af3e2b31799b74a4ee8904ccca0bd672b7f0
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-framac-1119.c
@@ -0,0 +1,208 @@
+/* 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;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue-framac-1119.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue-framac-1119.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..07a2f42bf48fe04064bda92c5fd5d3e4a181859f
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/issue-framac-1119.res.oracle
@@ -0,0 +1,14 @@
+[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);