Skip to content

Commit 7417bef

Browse files
author
Enrico Steffinlongo
committed
Fix missing alloca definition on regression test
Windows requires alloca to be defined otherwise an invariant will be violated (the invariant violation will be changed in another subsequent PR).
1 parent 4655ef4 commit 7417bef

File tree

1 file changed

+4
-0
lines changed
  • regression/cbmc-shadow-memory/nondet-size-arrays1

1 file changed

+4
-0
lines changed

regression/cbmc-shadow-memory/nondet-size-arrays1/main.c

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,10 @@
11
#include <assert.h>
22
#include <stdlib.h>
33

4+
#ifdef _WIN32
5+
void *alloca(size_t alloca_size);
6+
#endif
7+
48
int main()
59
{
610
__CPROVER_field_decl_local("field1", (char)0);

0 commit comments

Comments
 (0)