Merge pull request #4772 from tautschnig/free-deref

C library/free: distinguish invalid pointer from invalid free

Author: Daniel Kroening

regression/cbmc-library/free-01/main.c

@@ -1,9 +1,8 @@
-#include <assert.h>
 #include <stdlib.h>
 
 int main()
 {
-  free();
-  assert(0);
+  int *ptr;
+  free(ptr);
   return 0;
 }

regression/cbmc-library/free-01/test.desc

@@ -1,8 +1,9 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
-^EXIT=0$
+--pointer-check --bounds-check --stop-on-fail
+free argument must be NULL or valid pointer
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc/alloca1/test.desc

@@ -5,6 +5,6 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 free called for stack-allocated object: FAILURE$
-^\*\* 1 of 12 failed
+^\*\* 1 of 13 failed
 --
 ^warning: ignoring

src/ansi-c/library/stdlib.c

@@ -184,6 +184,9 @@ inline void free(void *ptr)
 {
   __CPROVER_HIDE:;
   // If ptr is NULL, no operation is performed.
+  __CPROVER_precondition(
+    ptr == 0 || __CPROVER_r_ok(ptr, 0),
+    "free argument must be NULL or valid pointer");
   __CPROVER_precondition(ptr==0 || __CPROVER_DYNAMIC_OBJECT(ptr),
                          "free argument must be dynamic object");
   __CPROVER_precondition(ptr==0 || __CPROVER_POINTER_OFFSET(ptr)==0,