Do not use non-trivial system headers with --32

Function declarations in system headers would cause type conflicts when running on 64-bit systems. Just add a proper declaration of malloc in place instead.
smowton · Jan 30, 2018 · b2c4188 · b2c4188
1 parent fdb2ebc
commit b2c4188
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 3 deletions.
diff --git a/regression/cbmc/Pointer_byte_extract5/main.c b/regression/cbmc/Pointer_byte_extract5/main.c
@@ -1,4 +1,4 @@
-#include <stdlib.h>
+void *malloc(__CPROVER_size_t);
 
 typedef union
 {

diff --git a/regression/cbmc/Pointer_byte_extract8/main.c b/regression/cbmc/Pointer_byte_extract8/main.c
@@ -1,4 +1,4 @@
-#include <stdlib.h>
+void *malloc(__CPROVER_size_t);
 
 typedef union
 {

diff --git a/regression/cbmc/address_space_size_limit2/test.c b/regression/cbmc/address_space_size_limit2/test.c
@@ -1,6 +1,7 @@
-#include <stdlib.h>
 #include <assert.h>
 
+void *malloc(__CPROVER_size_t);
+
 int main(int argc, char** argv)
 {
   char* c=(char*)malloc(10);