Skip to content

Commit 8a44e73

Browse files
committed
Do not try to generate void objects
For void pointers (or structs containing void pointers) we cannot generate "void" typed objects. Instead, generate char-typed objects as a fall-back.
1 parent 0b8c742 commit 8a44e73

File tree

3 files changed

+30
-2
lines changed

3 files changed

+30
-2
lines changed
Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
#include <assert.h>
2+
3+
struct void_ptr
4+
{
5+
void *ptr;
6+
};
7+
8+
void havoc_struct(struct void_ptr *s);
9+
10+
int main(void)
11+
{
12+
struct void_ptr s;
13+
havoc_struct(&s);
14+
if(s.ptr)
15+
*(char *)s.ptr = 42;
16+
assert(!s.ptr || *(char *)s.ptr == 42);
17+
return 0;
18+
}
Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
main.c
3+
--generate-function-body 'havoc_struct' --generate-function-body-options 'havoc,params:.*'
4+
^VERIFICATION SUCCESSFUL$
5+
^SIGNAL=0$
6+
^EXIT=0$

src/ansi-c/c_nondet_symbol_factory.cpp

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -71,8 +71,12 @@ void symbol_factoryt::gen_nondet_init(
7171

7272
code_blockt non_null_inst;
7373

74-
exprt init_expr =
75-
allocate_objects.allocate_object(non_null_inst, expr, subtype, lifetime);
74+
typet object_type = subtype;
75+
if(object_type.id() == ID_empty)
76+
object_type = char_type();
77+
78+
exprt init_expr = allocate_objects.allocate_object(
79+
non_null_inst, expr, object_type, lifetime);
7680

7781
gen_nondet_init(non_null_inst, init_expr, depth + 1, recursion_set, true);
7882

0 commit comments

Comments
 (0)