Skip to content

Commit b2c4188

Browse files
committed
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.
1 parent fdb2ebc commit b2c4188

File tree

3 files changed

+4
-3
lines changed
  • regression/cbmc

3 files changed

+4
-3
lines changed

regression/cbmc/Pointer_byte_extract5/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
#include <stdlib.h>
1+
void *malloc(__CPROVER_size_t);
22

33
typedef union
44
{

regression/cbmc/Pointer_byte_extract8/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
#include <stdlib.h>
1+
void *malloc(__CPROVER_size_t);
22

33
typedef union
44
{

regression/cbmc/address_space_size_limit2/test.c

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
1-
#include <stdlib.h>
21
#include <assert.h>
32

3+
void *malloc(__CPROVER_size_t);
4+
45
int main(int argc, char** argv)
56
{
67
char* c=(char*)malloc(10);

0 commit comments

Comments
 (0)