Skip to content
Snippets Groups Projects
Commit 8e1e6d69 authored by Julien Signoles's avatar Julien Signoles
Browse files

[typing] fix bug when comparing pointers

parent 632573a2
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/new_typing.ml
+ 7
− 4
View file @ 8e1e6d69
......@@ -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
......
src/plugins/e-acsl/new_typing.mli
+ 3
− 2
View file @ 8e1e6d69
......@@ -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
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.res.oracle
+ 3
− 1
View file @ 8e1e6d69
......@@ -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.
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_memsize.c
+ 24
− 32
View file @ 8e1e6d69
......@@ -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);
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.res.oracle
+ 3
− 1
View file @ 8e1e6d69
......@@ -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.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment