From d02cf3044fb9b10209ad1d7ca2e1e6e5d2622683 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 14 Aug 2018 23:12:00 +0100 Subject: [PATCH] do not attempt to havoc void-typed objects; fixes issue #2663 --- src/goto-programs/generate_function_bodies.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/goto-programs/generate_function_bodies.cpp b/src/goto-programs/generate_function_bodies.cpp index 5e10607f651..bff0d544111 100644 --- a/src/goto-programs/generate_function_bodies.cpp +++ b/src/goto-programs/generate_function_bodies.cpp @@ -271,7 +271,9 @@ class havoc_generate_function_bodiest : public generate_function_bodiest, if( parameter.type().id() == ID_pointer && std::regex_match( - id2string(parameter.get_base_name()), parameters_to_havoc)) + id2string(parameter.get_base_name()), parameters_to_havoc) && + parameter.type().subtype().id() != ID_empty && + parameter.type().subtype().id() != ID_code) { // if (param != nullptr) { *param = nondet(); } auto goto_instruction = add_instruction();