From 8e1e6d6918a207bd786a5a0cff06c8d293fa9fcd Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 22 Mar 2016 10:35:55 +0100
Subject: [PATCH] [typing] fix bug when comparing pointers
---
src/plugins/e-acsl/new_typing.ml | 11 ++--
src/plugins/e-acsl/new_typing.mli | 5 +-
.../e-acsl-runtime/oracle/freeable.res.oracle | 4 +-
.../tests/e-acsl-runtime/oracle/gen_memsize.c | 56 ++++++++-----------
.../e-acsl-runtime/oracle/memsize.res.oracle | 4 +-
5 files changed, 40 insertions(+), 40 deletions(-)
diff --git a/src/plugins/e-acsl/new_typing.ml b/src/plugins/e-acsl/new_typing.ml
index f47671881fe..7d4c9ab576d 100644
--- a/src/plugins/e-acsl/new_typing.ml
+++ b/src/plugins/e-acsl/new_typing.ml
@@ -58,10 +58,11 @@ let join ty1 ty2 = match ty1, ty2 with
Options.fatal "[typing] join failure: unexpected result %a"
Printer.pp_typ ty
+exception Not_an_integer
let typ_of_integer_ty = function
| Gmp -> Gmpz.t ()
| C_type ik -> TInt(ik, [])
- | Other -> Options.fatal "[typing] not an integer type"
+ | Other -> raise Not_an_integer
let size_t () = match Cil.theMachine.Cil.typeOfSizeOf with
| TInt(kind, _) -> C_type kind
@@ -478,17 +479,19 @@ let get_integer_ty_of_predicate p =
let get_typ t =
let info = Memo.get t in
- typ_of_integer_ty info.ty
+ try typ_of_integer_ty info.ty with Not_an_integer -> assert false
let get_cast t =
Cil.CurrentLoc.set t.term_loc;
let info = Memo.get t in
- Extlib.opt_map typ_of_integer_ty info.cast
+ try Extlib.opt_map typ_of_integer_ty info.cast
+ with Not_an_integer -> None
let get_cast_of_predicate p =
(* the env is useless *)
let info = type_predicate_named Interval.Env.empty p in
- Extlib.opt_map typ_of_integer_ty info.cast
+ try Extlib.opt_map typ_of_integer_ty info.cast
+ with Not_an_integer -> assert false
let clear = Memo.clear
diff --git a/src/plugins/e-acsl/new_typing.mli b/src/plugins/e-acsl/new_typing.mli
index aeb35c701be..d141cb457c4 100644
--- a/src/plugins/e-acsl/new_typing.mli
+++ b/src/plugins/e-acsl/new_typing.mli
@@ -57,8 +57,9 @@ val get_integer_ty: term -> integer_ty
val get_integer_ty_of_predicate: predicate named -> integer_ty
val get_typ: term -> typ
-(** Get the type of the given term. {!type_named_predicate} must already have
- been called on the englobing predicate. *)
+(** Get the type of the given term which must be an integer.
+ {!type_named_predicate} must already have been called on the englobing
+ predicate. *)
val get_cast: term -> typ option
(** Get the type which the given term must be converted to after its translation
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.res.oracle
index 92a368f6c4c..bf28a615802 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.res.oracle
@@ -5,13 +5,15 @@ tests/e-acsl-runtime/freeable.c:25:[e-acsl] warning: E-ACSL construct `complete
Ignoring annotation.
tests/e-acsl-runtime/freeable.c:25:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:179:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memsize.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memsize.c
index 630a6bcaab1..84d0d914344 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memsize.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memsize.c
@@ -10,61 +10,55 @@ int main(int argc, char **argv)
__e_acsl_full_init((void *)(& a));
a = (char *)__gen_e_acsl_malloc((unsigned long)7);
/*@ assert __e_acsl_heap_size ≡ 7; */
- __e_acsl_assert(__e_acsl_heap_size == (unsigned long)7,(char *)"Assertion",
- (char *)"main",(char *)"__e_acsl_heap_size == 7",22);
+ __e_acsl_assert(__e_acsl_heap_size == 7,(char *)"Assertion",(char *)"main",
+ (char *)"__e_acsl_heap_size == 7",22);
__e_acsl_full_init((void *)(& b));
b = (char *)__gen_e_acsl_malloc((unsigned long)14);
/*@ assert __e_acsl_heap_size ≡ 21; */
- __e_acsl_assert(__e_acsl_heap_size == (unsigned long)21,
- (char *)"Assertion",(char *)"main",
- (char *)"__e_acsl_heap_size == 21",24);
+ __e_acsl_assert(__e_acsl_heap_size == 21,(char *)"Assertion",
+ (char *)"main",(char *)"__e_acsl_heap_size == 21",24);
__gen_e_acsl_free((void *)a);
/*@ assert __e_acsl_heap_size ≡ 14; */
- __e_acsl_assert(__e_acsl_heap_size == (unsigned long)14,
- (char *)"Assertion",(char *)"main",
- (char *)"__e_acsl_heap_size == 14",28);
+ __e_acsl_assert(__e_acsl_heap_size == 14,(char *)"Assertion",
+ (char *)"main",(char *)"__e_acsl_heap_size == 14",28);
__e_acsl_full_init((void *)(& a));
a = (char *)0;
__gen_e_acsl_free((void *)a);
/*@ assert __e_acsl_heap_size ≡ 14; */
- __e_acsl_assert(__e_acsl_heap_size == (unsigned long)14,
- (char *)"Assertion",(char *)"main",
- (char *)"__e_acsl_heap_size == 14",33);
+ __e_acsl_assert(__e_acsl_heap_size == 14,(char *)"Assertion",
+ (char *)"main",(char *)"__e_acsl_heap_size == 14",33);
__e_acsl_full_init((void *)(& b));
b = (char *)__gen_e_acsl_realloc((void *)b,(unsigned long)9);
/*@ assert __e_acsl_heap_size ≡ 9; */
- __e_acsl_assert(__e_acsl_heap_size == (unsigned long)9,(char *)"Assertion",
- (char *)"main",(char *)"__e_acsl_heap_size == 9",37);
+ __e_acsl_assert(__e_acsl_heap_size == 9,(char *)"Assertion",(char *)"main",
+ (char *)"__e_acsl_heap_size == 9",37);
__e_acsl_full_init((void *)(& b));
b = (char *)__gen_e_acsl_realloc((void *)b,(unsigned long)18);
/*@ assert __e_acsl_heap_size ≡ 18; */
- __e_acsl_assert(__e_acsl_heap_size == (unsigned long)18,
- (char *)"Assertion",(char *)"main",
- (char *)"__e_acsl_heap_size == 18",41);
+ __e_acsl_assert(__e_acsl_heap_size == 18,(char *)"Assertion",
+ (char *)"main",(char *)"__e_acsl_heap_size == 18",41);
__e_acsl_full_init((void *)(& b));
b = (char *)__gen_e_acsl_realloc((void *)b,(unsigned long)0);
__e_acsl_full_init((void *)(& b));
b = (char *)0;
/*@ assert __e_acsl_heap_size ≡ 0; */
- __e_acsl_assert(__e_acsl_heap_size == (unsigned long)0,(char *)"Assertion",
- (char *)"main",(char *)"__e_acsl_heap_size == 0",46);
+ __e_acsl_assert(__e_acsl_heap_size == 0,(char *)"Assertion",(char *)"main",
+ (char *)"__e_acsl_heap_size == 0",46);
__e_acsl_full_init((void *)(& b));
b = (char *)__gen_e_acsl_realloc((void *)b,(unsigned long)8);
/*@ assert __e_acsl_heap_size ≡ 8; */
- __e_acsl_assert(__e_acsl_heap_size == (unsigned long)8,(char *)"Assertion",
- (char *)"main",(char *)"__e_acsl_heap_size == 8",50);
+ __e_acsl_assert(__e_acsl_heap_size == 8,(char *)"Assertion",(char *)"main",
+ (char *)"__e_acsl_heap_size == 8",50);
__e_acsl_full_init((void *)(& b));
b = (char *)__gen_e_acsl_realloc((void *)0,(unsigned long)8);
/*@ assert __e_acsl_heap_size ≡ 16; */
- __e_acsl_assert(__e_acsl_heap_size == (unsigned long)16,
- (char *)"Assertion",(char *)"main",
- (char *)"__e_acsl_heap_size == 16",54);
+ __e_acsl_assert(__e_acsl_heap_size == 16,(char *)"Assertion",
+ (char *)"main",(char *)"__e_acsl_heap_size == 16",54);
__e_acsl_full_init((void *)(& b));
b = (char *)__gen_e_acsl_realloc((void *)0,18446744073709551615UL);
/*@ assert __e_acsl_heap_size ≡ 16; */
- __e_acsl_assert(__e_acsl_heap_size == (unsigned long)16,
- (char *)"Assertion",(char *)"main",
- (char *)"__e_acsl_heap_size == 16",58);
+ __e_acsl_assert(__e_acsl_heap_size == 16,(char *)"Assertion",
+ (char *)"main",(char *)"__e_acsl_heap_size == 16",58);
/*@ assert b ≡ (char *)((void *)0); */
__e_acsl_assert(b == (char *)0,(char *)"Assertion",(char *)"main",
(char *)"b == (char *)((void *)0)",59);
@@ -72,18 +66,16 @@ int main(int argc, char **argv)
b = (char *)__gen_e_acsl_calloc(18446744073709551615UL,
18446744073709551615UL);
/*@ assert __e_acsl_heap_size ≡ 16; */
- __e_acsl_assert(__e_acsl_heap_size == (unsigned long)16,
- (char *)"Assertion",(char *)"main",
- (char *)"__e_acsl_heap_size == 16",63);
+ __e_acsl_assert(__e_acsl_heap_size == 16,(char *)"Assertion",
+ (char *)"main",(char *)"__e_acsl_heap_size == 16",63);
/*@ assert b ≡ (char *)((void *)0); */
__e_acsl_assert(b == (char *)0,(char *)"Assertion",(char *)"main",
(char *)"b == (char *)((void *)0)",64);
__e_acsl_full_init((void *)(& b));
b = (char *)__gen_e_acsl_malloc(18446744073709551615UL);
/*@ assert __e_acsl_heap_size ≡ 16; */
- __e_acsl_assert(__e_acsl_heap_size == (unsigned long)16,
- (char *)"Assertion",(char *)"main",
- (char *)"__e_acsl_heap_size == 16",68);
+ __e_acsl_assert(__e_acsl_heap_size == 16,(char *)"Assertion",
+ (char *)"main",(char *)"__e_acsl_heap_size == 16",68);
/*@ assert b ≡ (char *)((void *)0); */
__e_acsl_assert(b == (char *)0,(char *)"Assertion",(char *)"main",
(char *)"b == (char *)((void *)0)",69);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.res.oracle
index 636c9e84d45..a9fc435b528 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.res.oracle
@@ -26,13 +26,15 @@ FRAMAC_SHARE/libc/stdlib.h:213:[e-acsl] warning: E-ACSL construct `complete beha
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:213:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:179:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:178:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
--
GitLab