From cb0d67a84bd73b571df59a009ef9a81f0eb39dfd Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 28 May 2015 14:54:06 +0200
Subject: [PATCH] [typing] fix typing of \block_length and \offset
---
src/plugins/e-acsl/doc/Changelog | 1 +
.../e-acsl-runtime/oracle/gen_mainargs.c | 45 ++++++++++++++++++-
src/plugins/e-acsl/translate.ml | 2 +-
src/plugins/e-acsl/typing.ml | 26 +++++++----
src/plugins/e-acsl/typing.mli | 2 +-
5 files changed, 64 insertions(+), 12 deletions(-)
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index a8ccb4ffa76..5eefc9d5eaa 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 2dffc64ca52..a4eacb8e664 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 824eb210ff2..b177a968fcd 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 89ae8344e8f..36a1af9f2ec 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 f2cbdab0616..71cd5d84e6b 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. *)
--
GitLab