Merge branch 'master' into master

Author: ManuelLerchner

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

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

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 <stdlib.h>
+#include <goblint.h>
+
+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);
+}

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 <stdlib.h>
+
+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;
+}