34 int param_counter = 0;
35 for(
auto ¶meter :
function.type.parameters())
37 if(parameter.get_identifier().empty())
39 const std::string param_base_name =
40 parameter.get_base_name().empty()
44 id2string(function_name) +
"::" + param_base_name;
45 parameter.set_base_name(param_base_name);
46 parameter.set_identifier(new_param_identifier);
48 new_param_sym.
name = new_param_identifier;
49 new_param_sym.
type = parameter.type();
50 new_param_sym.
base_name = param_base_name;
51 auto const &function_symbol = symbol_table.
lookup_ref(function_name);
52 new_param_sym.
mode = function_symbol.mode;
53 new_param_sym.
module = function_symbol.module;
54 new_param_sym.
location = function_symbol.location;
55 symbol_table.
add(new_param_sym);
59 function_symbol.
type =
function.type;
68 const irep_idt &function_name)
const override
70 auto const &function_symbol = symbol_table.
lookup_ref(function_name);
72 auto add_instruction = [&]() {
73 auto instruction =
function.body.add_instruction();
74 instruction->function = function_name;
75 instruction->source_location = function_symbol.location;
78 auto assume_instruction = add_instruction();
80 auto end_instruction = add_instruction();
81 end_instruction->make_end_function();
91 const irep_idt &function_name)
const override
93 auto const &function_symbol = symbol_table.
lookup_ref(function_name);
95 auto add_instruction = [&]() {
96 auto instruction =
function.body.add_instruction();
97 instruction->function = function_name;
98 instruction->source_location = function_symbol.location;
99 instruction->source_location.set_function(function_name);
102 auto assert_instruction = add_instruction();
105 std::ostringstream comment_stream;
106 comment_stream <<
id2string(ID_assertion) <<
" "
107 <<
format(assert_instruction->guard);
108 assert_instruction->source_location.set_comment(comment_stream.str());
109 assert_instruction->source_location.set_property_class(ID_assertion);
110 auto end_instruction = add_instruction();
111 end_instruction->make_end_function();
122 const irep_idt &function_name)
const override
124 auto const &function_symbol = symbol_table.
lookup_ref(function_name);
126 auto add_instruction = [&]() {
127 auto instruction =
function.body.add_instruction();
128 instruction->function = function_name;
129 instruction->source_location = function_symbol.location;
130 instruction->source_location.set_function(function_name);
133 auto assert_instruction = add_instruction();
135 assert_instruction->source_location.set_function(function_name);
137 std::ostringstream comment_stream;
138 comment_stream <<
id2string(ID_assertion) <<
" "
139 <<
format(assert_instruction->guard);
140 assert_instruction->source_location.set_comment(comment_stream.str());
141 assert_instruction->source_location.set_property_class(ID_assertion);
142 auto assume_instruction = add_instruction();
143 assume_instruction->make_assumption(
false_exprt());
144 auto end_instruction = add_instruction();
145 end_instruction->make_end_function();
169 const irep_idt &function_name)
const
174 if(!lhs_type.get_bool(ID_C_constant))
178 if(lhs_type.id() == ID_struct || lhs_type.id() == ID_union)
191 for(
auto const &
component : lhs_struct_type.components())
200 else if(lhs_type.id() == ID_array)
203 if(!lhs_array_type.subtype().get_bool(ID_C_constant))
205 bool constant_known_array_size = lhs_array_type.size().is_constant();
206 if(!constant_known_array_size)
209 <<
" in function " << function_name
210 <<
": Unknown array size" <<
eom;
214 auto const array_size =
215 numeric_cast<mp_integer>(lhs_array_type.size());
217 array_size.has_value(),
218 "Array size should be known constant integer");
219 if(array_size.value() == 0)
225 <<
" in function " << function_name <<
": Array size 0"
230 for(
mp_integer i = 0; i < array_size.value(); ++i)
246 auto assign_instruction = add_instruction();
247 assign_instruction->make_assignment(
258 const irep_idt &function_name)
const override
260 auto const &function_symbol = symbol_table.
lookup_ref(function_name);
262 auto add_instruction = [&]() {
263 auto instruction =
function.body.add_instruction();
264 instruction->function = function_name;
265 instruction->source_location = function_symbol.location;
269 for(
auto const ¶meter :
function.type.parameters())
272 parameter.type().id() == ID_pointer &&
277 auto goto_instruction = add_instruction();
280 symbol_exprt(parameter.get_identifier(), parameter.type()),
285 auto label_instruction = add_instruction();
286 goto_instruction->make_goto(
289 symbol_exprt(parameter.get_identifier(), parameter.type()),
291 label_instruction->make_skip();
297 auto const &global_sym = symbol_table.
lookup_ref(global_id);
304 if(
function.type.return_type() !=
void_typet())
306 auto return_instruction = add_instruction();
307 return_instruction->make_return();
310 function.type.return_type(), function_symbol.location));
312 auto end_function_instruction = add_instruction();
313 end_function_instruction->make_end_function();
327 : runtime_error(reason)
336 const std::string &options,
340 if(options.empty() || options ==
"nondet-return")
342 return util_make_unique<havoc_generate_function_bodiest>(
343 std::vector<irep_idt>{}, std::regex{}, message_handler);
346 if(options ==
"assume-false")
348 return util_make_unique<assume_false_generate_function_bodiest>();
351 if(options ==
"assert-false")
353 return util_make_unique<assert_false_generate_function_bodiest>();
356 if(options ==
"assert-false-assume-false")
362 const std::vector<std::string> option_components =
split_string(options,
',');
363 if(!option_components.empty() && option_components[0] ==
"havoc")
365 std::regex globals_regex;
366 std::regex params_regex;
367 for(std::size_t i = 1; i < option_components.size(); ++i)
369 const std::vector<std::string> key_value_pair =
371 if(key_value_pair.size() != 2)
374 "Expected key_value_pair of form argument:value");
376 if(key_value_pair[0] ==
"globals")
378 globals_regex = key_value_pair[1];
380 else if(key_value_pair[0] ==
"params")
382 params_regex = key_value_pair[1];
387 "Unknown option \"" + key_value_pair[0] +
"\"");
390 std::vector<irep_idt> globals_to_havoc;
393 const std::regex cprover_prefix = std::regex(
"__CPROVER.*");
394 for(
auto const &symbol : symbol_table.
symbols)
397 symbol.second.is_lvalue && symbol.second.is_static_lifetime &&
398 std::regex_match(
id2string(symbol.first), globals_regex))
400 if(std::regex_match(
id2string(symbol.first), cprover_prefix))
402 messages.
warning() <<
"generate function bodies: "
403 <<
"matched global '" <<
id2string(symbol.first)
404 <<
"' begins with __CPROVER, "
405 <<
"havoc-ing this global may interfere"
408 globals_to_havoc.push_back(symbol.first);
411 return util_make_unique<havoc_generate_function_bodiest>(
412 std::move(globals_to_havoc), std::move(params_regex), message_handler);
455 const std::regex &functions_regex,
461 const std::regex cprover_prefix = std::regex(
"__CPROVER.*");
462 bool did_generate_body =
false;
466 !
function.second.body_available() &&
467 std::regex_match(
id2string(
function.first), functions_regex))
469 if(std::regex_match(
id2string(
function.first), cprover_prefix))
471 messages.
warning() <<
"generate function bodies: matched function '"
473 <<
"' begins with __CPROVER "
474 <<
"the generated body for this function "
477 did_generate_body =
true;
482 if(!did_generate_body)
485 <<
"generate function bodies: No function name matched regex"