Merge pull request #982 from tautschnig/pointer-handling

Fixes and improvements to dynamic memory handling

Author: kroening

regression/cbmc-with-incr/Malloc17/main.c

@@ -4,7 +4,7 @@ unsigned char* init1()
   if (size!=1) return 0;
 
   assert(sizeof(unsigned char)==1);
-  unsigned char* buffer=__CPROVER_malloc(1);
+  unsigned char* buffer=__CPROVER_allocate(1, 0);
   assert(buffer!=0);
 
   buffer[0]=0;
@@ -18,7 +18,7 @@ unsigned char* init2()
   if (size!=1) return 0;
 
   assert(sizeof(unsigned char)==1);
-  unsigned char* buffer=__CPROVER_malloc(1*sizeof(unsigned char));
+  unsigned char* buffer=__CPROVER_allocate(1*sizeof(unsigned char), 0);
   assert(buffer!=0);
 
   buffer[0]=0;
@@ -32,7 +32,7 @@ unsigned char* init3()
   if (size!=1) return 0;
 
   assert(sizeof(unsigned char)==1);
-  unsigned char* buffer=__CPROVER_malloc(sizeof(unsigned char)*1);
+  unsigned char* buffer=__CPROVER_allocate(sizeof(unsigned char)*1, 0);
   assert(buffer!=0);
 
   buffer[0]=0;

regression/cbmc-with-incr/Malloc18/main.c

@@ -4,7 +4,7 @@ unsigned char* init()
   if (size!=1) return 0;
 
   assert(sizeof(unsigned char)==1);
-  unsigned char* buffer=__CPROVER_malloc(size);
+  unsigned char* buffer=__CPROVER_allocate(size, 0);
   assert(buffer!=0);
 
   buffer[0]=0;

regression/cbmc-with-incr/Malloc19/main.c

@@ -22,7 +22,7 @@ int main()
 {
     // Create node
     struct node *nd;
-    nd = (struct node *)__CPROVER_malloc(sizeof(struct node));
+    nd = (struct node *)__CPROVER_allocate(sizeof(struct node), 0);
 
     // Link node
     struct list_head *hd = &(nd->linkage);

regression/cbmc/Calloc1/main.c

@@ -0,0 +1,9 @@
+#include <stdlib.h>
+#include <assert.h>
+
+int main()
+{
+  int *x=calloc(sizeof(int), 1);
+  assert(*x==0);
+  return 0;
+}

regression/cbmc/Calloc1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/Malloc17/main.c

@@ -4,7 +4,7 @@ unsigned char* init1()
   if (size!=1) return 0;
 
   assert(sizeof(unsigned char)==1);
-  unsigned char* buffer=__CPROVER_malloc(1);
+  unsigned char* buffer=__CPROVER_allocate(1, 0);
   assert(buffer!=0);
 
   buffer[0]=0;
@@ -18,7 +18,7 @@ unsigned char* init2()
   if (size!=1) return 0;
 
   assert(sizeof(unsigned char)==1);
-  unsigned char* buffer=__CPROVER_malloc(1*sizeof(unsigned char));
+  unsigned char* buffer=__CPROVER_allocate(1*sizeof(unsigned char), 0);
   assert(buffer!=0);
 
   buffer[0]=0;
@@ -32,7 +32,7 @@ unsigned char* init3()
   if (size!=1) return 0;
 
   assert(sizeof(unsigned char)==1);
-  unsigned char* buffer=__CPROVER_malloc(sizeof(unsigned char)*1);
+  unsigned char* buffer=__CPROVER_allocate(sizeof(unsigned char)*1, 0);
   assert(buffer!=0);
 
   buffer[0]=0;

regression/cbmc/Malloc18/main.c

@@ -3,7 +3,7 @@ unsigned char* init()
   unsigned long buffer_size;
   if(buffer_size!=1) return 0;
 
-  unsigned char* buffer=__CPROVER_malloc(buffer_size);
+  unsigned char* buffer=__CPROVER_allocate(buffer_size, 0);
   __CPROVER_assert(buffer!=0, "malloc did not return NULL");
 
   buffer[0]=10;

regression/cbmc/Malloc19/main.c

@@ -22,7 +22,7 @@ int main()
 {
     // Create node
     struct node *nd;
-    nd = (struct node *)__CPROVER_malloc(sizeof(struct node));
+    nd = (struct node *)__CPROVER_allocate(sizeof(struct node), 0);
 
     // Link node
     struct list_head *hd = &(nd->linkage);

regression/cbmc/Malloc24/main.c

@@ -0,0 +1,47 @@
+#include <stdlib.h>
+
+struct node
+{
+    int value;
+    struct node *next;
+};
+
+struct list
+{
+  int size;
+  struct node *head;
+};
+
+void removeLast(struct list * l)
+{
+  int index = l->size - 1;
+  struct node **current;
+  for(current = &(l->head); index && *current; index--)
+    current = &(*current)->next;
+  *current = (*current)->next;
+  l->size--;
+}
+
+int main () {
+  //build a 2-nodes list
+  struct node *n0 = malloc(sizeof(struct node));
+  struct node *n1 = malloc(sizeof(struct node));
+  struct list *l = malloc(sizeof(struct list));
+  l->size = 2;
+  l->head = n0;
+
+  n0->next=n1;
+  n1->next=NULL;
+
+  //remove last node from list
+
+  //this passes
+  // struct node **current = &(l->head);
+  // current = &(*current)->next;
+  // *current = (*current)->next;
+  // l->size--;
+  //this doesn't
+  removeLast(l);
+
+  __CPROVER_assert(n0->next == NULL , "not NULL");
+}

regression/cbmc/Malloc24/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--unwind 4 --pointer-check --unwinding-assertions
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring