CBMC
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 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...
 

Function Documentation

◆ generate_function_bodies() [1/2]

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.

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 501 of file generate_function_bodies.cpp.

◆ generate_function_bodies() [2/2]

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.

Parameters
function_nameThe function whose body should be generated
call_site_idthe number of the call site
generate_function_bodythe previously constructed body generator
modelthe goto-model to be modified
message_handlerthe message-handler

Definition at line 537 of file generate_function_bodies.cpp.

◆ generate_function_bodies_factory()

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.

See also
generate_function_bodies for the syntax of the options parameter

Definition at line 375 of file generate_function_bodies.cpp.