Skip to content

Commit 11c949f

Browse files
committed
C++ model library: fix forward declarations
All functions must be declared before being used, and library checks should not fail due to duplicate definitions.
1 parent c9f576e commit 11c949f

File tree

1 file changed

+8
-0
lines changed

1 file changed

+8
-0
lines changed

src/cpp/library/new.c

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27,8 +27,10 @@ inline void *__new(__typeof__(sizeof(int)) malloc_size)
2727
/* FUNCTION: __new_array */
2828

2929
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
30+
#ifndef LIBRARY_CHECK
3031
const void *__CPROVER_new_object = 0;
3132
__CPROVER_bool __CPROVER_malloc_is_new_array = 0;
33+
#endif
3234

3335
inline void *__new_array(__CPROVER_size_t count, __CPROVER_size_t size)
3436
{
@@ -63,9 +65,12 @@ inline void *__placement_new(__typeof__(sizeof(int)) malloc_size, void *p)
6365

6466
/* FUNCTION: __delete */
6567

68+
void __CPROVER_deallocate(void *);
6669
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
70+
#ifndef LIBRARY_CHECK
6771
const void *__CPROVER_new_object = 0;
6872
__CPROVER_bool __CPROVER_malloc_is_new_array = 0;
73+
#endif
6974

7075
inline void __delete(void *ptr)
7176
{
@@ -98,9 +103,12 @@ inline void __delete(void *ptr)
98103

99104
/* FUNCTION: __delete_array */
100105

106+
void __CPROVER_deallocate(void *);
101107
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
108+
#ifndef LIBRARY_CHECK
102109
const void *__CPROVER_new_object = 0;
103110
__CPROVER_bool __CPROVER_malloc_is_new_array = 0;
111+
#endif
104112

105113
inline void __delete_array(void *ptr)
106114
{

0 commit comments

Comments
 (0)