From 98a3ea954001b1486e0a16192b4b3f2fc46f93b7 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 11 Jun 2019 06:09:45 +0000
Subject: [PATCH] C library/free: distinguish invalid pointer from invalid free

This makes counterexamples easier to understand when an invalid pointer
is being passed to free(), and also supports SV-COMP, where we
previously only distinguished these cases via a hack in the wrapper
script.
---
 regression/cbmc-library/free-01/main.c    | 5 ++---
 regression/cbmc-library/free-01/test.desc | 9 +++++----
 regression/cbmc/alloca1/test.desc         | 2 +-
 src/ansi-c/library/stdlib.c               | 3 +++
 4 files changed, 11 insertions(+), 8 deletions(-)

diff --git a/regression/cbmc-library/free-01/main.c b/regression/cbmc-library/free-01/main.c
index 92ade98ae7..ddec781b59 100644
--- a/regression/cbmc-library/free-01/main.c
+++ b/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;
 }
diff --git a/regression/cbmc-library/free-01/test.desc b/regression/cbmc-library/free-01/test.desc
index 9542d988e8..769ba573e7 100644
--- a/regression/cbmc-library/free-01/test.desc
+++ b/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
diff --git a/regression/cbmc/alloca1/test.desc b/regression/cbmc/alloca1/test.desc
index 66fa40a953..79c333b225 100644
--- a/regression/cbmc/alloca1/test.desc
+++ b/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
diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c
index b95df78422..d80ecd1264 100644
--- a/src/ansi-c/library/stdlib.c
+++ b/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,