Skip to content

Commit 7c4a98a

Browse files
author
Daniel Kroening
committed
do not attempt to havoc void-typed objects; fixes issue #2663
1 parent 78d22fb commit 7c4a98a

File tree

1 file changed

+3
-1
lines changed

1 file changed

+3
-1
lines changed

src/goto-programs/generate_function_bodies.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -271,7 +271,9 @@ class havoc_generate_function_bodiest : public generate_function_bodiest,
271271
if(
272272
parameter.type().id() == ID_pointer &&
273273
std::regex_match(
274-
id2string(parameter.get_base_name()), parameters_to_havoc))
274+
id2string(parameter.get_base_name()), parameters_to_havoc) &&
275+
parameter.type().subtype().id() != ID_empty &&
276+
parameter.type().subtype().id() != ID_code)
275277
{
276278
// if (param != nullptr) { *param = nondet(); }
277279
auto goto_instruction = add_instruction();

0 commit comments

Comments
 (0)