cprover
generate_function_bodies.cpp File Reference
Include dependency graph for generate_function_bodies.cpp:

Go to the source code of this file.

Classes

class  assume_false_generate_function_bodiest
 
class  assert_false_generate_function_bodiest
 
class  assert_false_then_assume_false_generate_function_bodiest
 
class  havoc_generate_function_bodiest
 
class  generate_function_bodies_errort
 

Functions

std::unique_ptr< generate_function_bodiestgenerate_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...
 

Function Documentation

◆ generate_function_bodies()

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.

  • the type of bodies generated by them

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

Parameters
functions_regexSpecifies the functions whose body should be generated
generate_function_bodySpecifies what kind of body to generate
modelThe goto-model in which to generate the function bodies
message_handlerDestination 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().

◆ generate_function_bodies_factory()

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.

See also
generate_function_bodies for the syntax of the options parameter

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().