Public Member Functions

Replace the function body with one based on the replace_function_body class being used.

Protected Member Functions

Produce a body for the passed function At this point the body of function is always empty, and all function parameters have identifiers.

Generate parameter names for unnamed parameters.

Base class for replace_function_body implementations.

Definition at line 24 of file generate_function_bodies.h.

virtual generate_function_bodiest::~generate_function_bodiest ( )

virtualdefault

void generate_function_bodiest::generate_function_body ( goto_functiont & function,

symbol_tablet & symbol_table,

const irep_idt & function_name

) const

Replace the function body with one based on the replace_function_body class being used.

Parameters: function whose body to replace

symbol_table of the current goto program

function_name Identifier of function

virtual void generate_function_bodiest::generate_function_body_impl ( goto_functiont & function,

symbol_tablet & symbol_table,

const irep_idt & function_name

) const

protectedpure virtual

Produce a body for the passed function At this point the body of function is always empty, and all function parameters have identifiers.

Parameters: function whose body to generate

symbol_table of the current goto program

function_name Identifier of function

void generate_function_bodiest::generate_parameter_names ( goto_functiont & function,

symbol_tablet & symbol_table,

const irep_idt & function_name

) const

private

Generate parameter names for unnamed parameters.

CBMC expect functions to have parameter names if they are called and have a body

The documentation for this class was generated from the following files: