diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index a8ccb4ffa76dedab4fcdfb60debd80d7c79a945e..5eefc9d5eaa3432dc1ba3ee66b0d8146b5d2a4c3 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,7 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
+-* E-ACSL [2015/05/28] Fix types of \block_length and \offset.
- E-ACSL [2015/05/27] Search .h in the E-ACSL memory model by
default (easier to use declarations like __memory_size).
- E-ACSL [2015/05/27] Compatibility with new Frama-C Sodium option
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
index 2dffc64ca52c9d92ecebf5280aeccf4b6103bc8a..a4eacb8e6646e4f08ae91d23d1efdf2e309fb59b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
@@ -32,6 +32,39 @@ axiomatic dynamic_allocation {
*/
/*@ ghost extern int __e_acsl_init; */
+/*@ requires ¬\initialized(z);
+ ensures \valid(\old(z));
+ ensures \initialized(\old(z));
+ assigns *z;
+ assigns *z \from n;
+ allocates \old(z);
+ */
+extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_ui(__mpz_struct * /*[1]*/ z,
+ unsigned long n);
+
+/*@ requires ¬\initialized(z);
+ ensures \valid(\old(z));
+ ensures \initialized(\old(z));
+ assigns *z;
+ assigns *z \from n;
+ allocates \old(z);
+ */
+extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
+ long n);
+
+/*@ requires \valid(x);
+ assigns *x;
+ assigns *x \from *x; */
+extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
+ assigns \result;
+ assigns \result \from *z1, *z2;
+ */
+extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2);
+
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __init_args(int argc_ref,
char **argv_ref);
@@ -404,11 +437,19 @@ int main(int argc, char **argv)
/*@ assert \block_length(argv) ≡ (argc+1)*sizeof(char *); */
{
unsigned long __e_acsl_block_length;
+ mpz_t __e_acsl_block_length_2;
+ mpz_t __e_acsl;
+ int __e_acsl_eq;
__e_acsl_block_length = __block_length((void *)argv);
- e_acsl_assert(__e_acsl_block_length == (unsigned long)(((long)argc + (long)1) * 8L),
- (char *)"Assertion",(char *)"main",
+ __gmpz_init_set_ui(__e_acsl_block_length_2,__e_acsl_block_length);
+ __gmpz_init_set_si(__e_acsl,((long)argc + (long)1) * 8L);
+ __e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__e_acsl_block_length_2),
+ (__mpz_struct const *)(__e_acsl));
+ e_acsl_assert(__e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
(char *)"\\block_length(argv) == (argc+1)*sizeof(char *)",
15);
+ __gmpz_clear(__e_acsl_block_length_2);
+ __gmpz_clear(__e_acsl);
}
/*@ assert *(argv+argc) ≡ \null; */
{
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 824eb210ff2d10dbb2dea99dbdbdcec33bb1761e..b177a968fcdbf9fa7463b5988de4b06fc19bbc43 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -84,7 +84,7 @@ let name_of_mpz_arith_bop = function
let constant_to_exp ~loc = function
| Integer(n, repr) ->
(try
- let kind = Typing.typ_of_integer n (Integer.ge n Integer.zero) in
+ let kind = Typing.ikind_of_integer n (Integer.ge n Integer.zero) in
if Typing.is_representable n kind then
Cil.kinteger64 ~loc ~kind ?repr n, false
else
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index 89ae8344e8ffdc894c07b2d230689d65add3567d..36a1af9f2ec5111cc5c1cba82d7379ba9d6071d9 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -57,7 +57,7 @@ let pretty_eacsl_typ fmt = function
| Z -> Format.fprintf fmt "Z"
| No_integral lty -> Format.fprintf fmt "%a" Printer.pp_logic_type lty
-let typ_of_integer i unsigned =
+let ikind_of_integer i unsigned =
(* int whenever possible to prevent superfluous casts in the generated code *)
if Cil.fitsInInt IInt i then IInt else Cil.intKindForValue i unsigned
@@ -65,8 +65,8 @@ let typ_of_eacsl_typ = function
| Interv(l, u) ->
let is_pos = Z.ge l Z.zero in
(try
- let ty_l = TInt(typ_of_integer l is_pos, []) in
- let ty_u = TInt(typ_of_integer u is_pos, []) in
+ let ty_l = TInt(ikind_of_integer l is_pos, []) in
+ let ty_u = TInt(ikind_of_integer u is_pos, []) in
Cil.arithmeticConversion ty_l ty_u
with Cil.Not_representable ->
Mpz.t ())
@@ -322,12 +322,22 @@ let rec type_term t =
dup (join ty2) ty3
| Tat(t, _)
| Tbase_addr(_, t) -> dup type_term t
- | Toffset(_, t)
- | Tblock_length(_, t) ->
+ | Toffset(_, t) ->
ignore (type_term t);
- (* TODO: to be improved by computing the length of the type of the
- pointer *)
- dup eacsl_typ_of_typ Cil.theMachine.Cil.typeOfSizeOf
+ let n = Z.div (Bit_utils.max_bit_address ()) (Z.of_int 8) in
+ let ty =
+ try TInt(ikind_of_integer n true, [])
+ with Cil.Not_representable -> Mpz.t ()
+ in
+ dup eacsl_typ_of_typ ty
+ | Tblock_length(_, t) ->
+ ignore (type_term t);
+ let n = Z.div (Bit_utils.max_bit_size ()) (Z.of_int 8) in
+ let ty =
+ try TInt(ikind_of_integer n true, [])
+ with Cil.Not_representable -> Mpz.t ()
+ in
+ dup eacsl_typ_of_typ ty
| Tnull -> dup int_to_interv 0
| TLogic_coerce(_, t) -> dup type_term t
| TCoerce(t, ty) ->
diff --git a/src/plugins/e-acsl/typing.mli b/src/plugins/e-acsl/typing.mli
index f2cbdab0616d411200d2705bca34134c5e80935c..71cd5d84e6b29cf27d4857eb63a3d404441a8649 100644
--- a/src/plugins/e-acsl/typing.mli
+++ b/src/plugins/e-acsl/typing.mli
@@ -26,7 +26,7 @@ open Cil_types
(** {2 Typing} *)
(******************************************************************************)
-val typ_of_integer: Integer.t -> bool -> ikind
+val ikind_of_integer: Integer.t -> bool -> ikind
(** Compute the best type of a bigint. The boolean must be [true] for unsigned
and [false] for signed.
@raise Cil.Not_representable if the integer does not fit in any C type. *)