cprover
Loading...
Searching...
No Matches
remove_function_pointers.cpp File Reference

Program Transformation. More...

Include dependency graph for remove_function_pointers.cpp:

Go to the source code of this file.

Classes

class  remove_function_pointerst

Functions

static bool arg_is_type_compatible (const typet &call_type, const typet &function_type, const namespacet &ns)
bool function_is_type_compatible (bool return_value_used, const code_typet &call_type, const code_typet &function_type, const namespacet &ns)
 Returns true iff call_type can be converted to produce a function call of the same type as function_type.
static void fix_argument_types (code_function_callt &function_call)
static void fix_return_type (const irep_idt &in_function_id, code_function_callt &function_call, const source_locationt &source_location, symbol_tablet &symbol_table, goto_programt &dest)
static std::string function_pointer_assertion_comment (const std::unordered_set< symbol_exprt, irep_hash > &candidates)
void remove_function_pointer (message_handlert &message_handler, symbol_tablet &symbol_table, goto_programt &goto_program, const irep_idt &function_id, goto_programt::targett target, const std::unordered_set< symbol_exprt, irep_hash > &functions)
 Replace a call to a dynamic function at location target in the given goto-program by a case-split over a given set of functions.
void remove_function_pointers (message_handlert &_message_handler, goto_modelt &goto_model, bool only_remove_const_fps)
bool has_function_pointers (const goto_programt &goto_program)
bool has_function_pointers (const goto_functionst &goto_functions)
 returns true iff any of the given goto functions has function calls via a function pointer
bool has_function_pointers (const goto_modelt &goto_model)
 returns true iff the given goto model has function calls via a function pointer

Detailed Description

Program Transformation.

Definition in file remove_function_pointers.cpp.

Function Documentation

◆ arg_is_type_compatible()

bool arg_is_type_compatible ( const typet & call_type,
const typet & function_type,
const namespacet & ns )
static

Definition at line 102 of file remove_function_pointers.cpp.

◆ fix_argument_types()

void fix_argument_types ( code_function_callt & function_call)
static

Definition at line 180 of file remove_function_pointers.cpp.

◆ fix_return_type()

void fix_return_type ( const irep_idt & in_function_id,
code_function_callt & function_call,
const source_locationt & source_location,
symbol_tablet & symbol_table,
goto_programt & dest )
static

Definition at line 205 of file remove_function_pointers.cpp.

◆ function_is_type_compatible()

bool function_is_type_compatible ( bool return_value_used,
const code_typet & call_type,
const code_typet & function_type,
const namespacet & ns )

Returns true iff call_type can be converted to produce a function call of the same type as function_type.

Definition at line 129 of file remove_function_pointers.cpp.

◆ function_pointer_assertion_comment()

std::string function_pointer_assertion_comment ( const std::unordered_set< symbol_exprt, irep_hash > & candidates)
static

Definition at line 347 of file remove_function_pointers.cpp.

◆ has_function_pointers() [1/3]

bool has_function_pointers ( const goto_functionst & goto_functions)

returns true iff any of the given goto functions has function calls via a function pointer

Definition at line 553 of file remove_function_pointers.cpp.

◆ has_function_pointers() [2/3]

bool has_function_pointers ( const goto_modelt & goto_model)

returns true iff the given goto model has function calls via a function pointer

Definition at line 562 of file remove_function_pointers.cpp.

◆ has_function_pointers() [3/3]

bool has_function_pointers ( const goto_programt & goto_program)

Definition at line 540 of file remove_function_pointers.cpp.

◆ remove_function_pointer()

void remove_function_pointer ( message_handlert & message_handler,
symbol_tablet & symbol_table,
goto_programt & goto_program,
const irep_idt & function_id,
goto_programt::targett target,
const std::unordered_set< symbol_exprt, irep_hash > & functions )

Replace a call to a dynamic function at location target in the given goto-program by a case-split over a given set of functions.

Parameters
message_handlerMessage handler to print warnings
symbol_tableSymbol table
goto_programThe goto program that contains target
function_idName of function containing the target
targetlocation with function call with function pointer
functionsThe set of functions to consider

Definition at line 379 of file remove_function_pointers.cpp.

◆ remove_function_pointers()

void remove_function_pointers ( message_handlert & _message_handler,
goto_modelt & goto_model,
bool only_remove_const_fps )

Definition at line 526 of file remove_function_pointers.cpp.