cprover
|
#include "generate_function_bodies.h"
#include <util/arith_tools.h>
#include <util/format_expr.h>
#include <util/make_unique.h>
#include <util/string_utils.h>
#include "remove_skip.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 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 A list of currently accepted command line arguments. 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 A list of currently accepted command line arguments.
assert-false: { assert(false); }
assume-false: { assume(false); }
assert-false-assume-false: { assert(false); assume(false); }
havoc[,params:regex][,globals:regex]: Assign nondet to the targets of pointer-to-non-const parameters matching regex, and non-const globals matching regex and then return nondet for non-void functions, e.g.:
int global; const int c_global; int function(int *param, const int *const_param);
havoc,params:(?!__).*,globals:(?!__).* (where (?!__) means "not preceded by __", which is recommended to avoid overwrite internal symbols), leads to
int function(int *param, consnt int *const_param) { *param = nondet_int(); global = nondet_int(); return nondet_int(); }
nondet-return: return nondet for non-void functions
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 454 of file generate_function_bodies.cpp.
References messaget::eom(), goto_functionst::function_map, generate_function_bodiest::generate_function_body(), goto_modelt::goto_functions, id2string(), message_handler, goto_modelt::symbol_table, and messaget::warning().
Referenced by goto_instrument_parse_optionst::instrument_goto_program().
std::unique_ptr<generate_function_bodiest> generate_function_bodies_factory | ( | const std::string & | options, |
const symbol_tablet & | symbol_table, | ||
message_handlert & | message_handler | ||
) |
Create the type that actually generates the functions.
Definition at line 335 of file generate_function_bodies.cpp.
References messaget::eom(), id2string(), message_handler, split_string(), symbol_table_baset::symbols, util_make_unique(), and messaget::warning().
Referenced by goto_instrument_parse_optionst::instrument_goto_program().