CBMC
|
#include "generate_function_bodies.h"
#include <util/fresh_symbol.h>
#include <util/pointer_expr.h>
#include <util/prefix.h>
#include <util/string2int.h>
#include <util/string_utils.h>
#include <goto-programs/goto_model.h>
#include <goto-programs/remove_skip.h>
#include <ansi-c/c_nondet_symbol_factory.h>
#include <ansi-c/goto-conversion/goto_convert.h>
#include <ansi-c/goto-conversion/goto_convert_functions.h>
Go to the source code of this file.
Functions | |
std::unique_ptr< generate_function_bodiest > | generate_function_bodies_factory (const std::string &options, const c_object_factory_parameterst &object_factory_parameters, const symbol_tablet &symbol_table, message_handlert &message_handler) |
Create the type that actually generates the functions. More... | |
void | generate_function_bodies (const std::regex &functions_regex, const generate_function_bodiest &generate_function_body, goto_modelt &model, message_handlert &message_handler) |
Generate function bodies with some default behavior: assert-false, assume-false, assert-false-assume-false, havoc, nondet-return. More... | |
void | generate_function_bodies (const std::string &function_name, const std::string &call_site_id, const generate_function_bodiest &generate_function_body, goto_modelt &model, message_handlert &message_handler) |
Generate a clone of function_name (labelled with call_site_id ) and instantiate its body with selective havocing of its parameters. More... | |
void generate_function_bodies | ( | const std::regex & | functions_regex, |
const generate_function_bodiest & | generate_function_body, | ||
goto_modelt & | model, | ||
message_handlert & | message_handler | ||
) |
Generate function bodies with some default behavior: assert-false, assume-false, assert-false-assume-false, havoc, nondet-return.
functions_regex | Specifies the functions whose body should be generated |
generate_function_body | Specifies what kind of body to generate |
model | The goto-model in which to generate the function bodies |
message_handler | Destination for status/warning messages |
Definition at line 501 of file generate_function_bodies.cpp.
void generate_function_bodies | ( | const std::string & | function_name, |
const std::string & | call_site_id, | ||
const generate_function_bodiest & | generate_function_body, | ||
goto_modelt & | model, | ||
message_handlert & | message_handler | ||
) |
Generate a clone of function_name
(labelled with call_site_id
) and instantiate its body with selective havocing of its parameters.
function_name | The function whose body should be generated |
call_site_id | the number of the call site |
generate_function_body | the previously constructed body generator |
model | the goto-model to be modified |
message_handler | the message-handler |
Definition at line 537 of file generate_function_bodies.cpp.
std::unique_ptr<generate_function_bodiest> generate_function_bodies_factory | ( | const std::string & | options, |
const c_object_factory_parameterst & | object_factory_parameters, | ||
const symbol_tablet & | symbol_table, | ||
message_handlert & | message_handler | ||
) |
Create the type that actually generates the functions.
Definition at line 375 of file generate_function_bodies.cpp.