diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 296a990b80..462383bec8 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -127,7 +127,7 @@ struct `Top) let get_ptr_deref_type ptr_typ = - match ptr_typ with + match Cil.unrollType ptr_typ with | TPtr (t, _) -> Some t | _ -> None @@ -279,10 +279,10 @@ struct M.warn "Size of lval dereference expression %a is bot. Out-of-bounds memory access may occur" d_exp e) | `Lifted es -> let casted_es = ID.cast_to (Cilfacade.ptrdiff_ikind ()) es in - let one = intdom_of_int 1 in - let casted_es = ID.sub casted_es one in - let casted_offs = ID.cast_to (Cilfacade.ptrdiff_ikind ()) offs_intdom in + let casted_offs = ID.div (ID.cast_to (Cilfacade.ptrdiff_ikind ()) offs_intdom) (ID.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int 8)) in let ptr_size_lt_offs = + let one = intdom_of_int 1 in + let casted_es = ID.sub casted_es one in begin try ID.lt casted_es casted_offs with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () end diff --git a/src/cdomain/value/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml index 615cf58e1a..cf2e5012d4 100644 --- a/src/cdomain/value/cdomains/valueDomain.ml +++ b/src/cdomain/value/cdomains/valueDomain.ml @@ -349,7 +349,7 @@ struct ************************************************************) (* is a cast t1 to t2 invertible, i.e., content-preserving in general? *) - let is_statically_safe_cast t2 t1 = match t2, t1 with + let is_statically_safe_cast t2 t1 = match unrollType t2, unrollType t1 with (*| TPtr _, t -> bitsSizeOf t <= bitsSizeOf !upointType | t, TPtr _ -> bitsSizeOf t >= bitsSizeOf !upointType*) | TFloat (fk1,_), TFloat (fk2,_) when fk1 = fk2 -> true diff --git a/tests/regression/01-cpa/76-pointer-typedef.c b/tests/regression/01-cpa/76-pointer-typedef.c new file mode 100644 index 0000000000..c5e72d7ee7 --- /dev/null +++ b/tests/regression/01-cpa/76-pointer-typedef.c @@ -0,0 +1,32 @@ +// PARAM: --set ana.malloc.unique_address_count 2 +// Extracted (using creduce) from SV-COMP task list-simple/dll2c_remove_all.i +#include +#include + +typedef struct node { + struct node *next; + struct node *prev; +} * DLL; + +void dll_remove(DLL *head) { + DLL temp = (*head)->next; + if (temp == *head) { + __goblint_check(temp == *head); + __goblint_check(temp != *head); // FAIL + free(*head); + } + else { + __goblint_check(temp != *head); + __goblint_check(temp == *head); // FAIL + (*head)->prev->next = temp; + free(*head); + *head = temp; + } +} +main() { + DLL s = malloc(sizeof(struct node)); + s->next = s->prev = malloc(sizeof(struct node)); + + dll_remove(&s); + dll_remove(&s); +} diff --git a/tests/regression/74-invalid_deref/32-dll2c_append_equal-mini.c b/tests/regression/74-invalid_deref/32-dll2c_append_equal-mini.c new file mode 100644 index 0000000000..cd0a0c4ad5 --- /dev/null +++ b/tests/regression/74-invalid_deref/32-dll2c_append_equal-mini.c @@ -0,0 +1,17 @@ +// PARAM: --set ana.activated[+] memOutOfBounds +// Minimized version of SV-COMP task list-simple/dll2c_append_equal.i +#include + +typedef struct node { + struct node *next; + struct node *prev; + int data; +} *DLL; + +int main(void) { + DLL temp = (DLL) malloc(sizeof(struct node)); + temp->next = NULL; // NOWARN + temp->prev = NULL; // NOWARN + temp->data = 1; // NOWARN + return temp; +} \ No newline at end of file