Skip to content

Commit d69fffb

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 a613337 commit d69fffb

File tree

1 file changed

+6
-2
lines changed

1 file changed

+6
-2
lines changed

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)