CBMC
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. More...
 
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. More...
 
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 More...
 
bool has_function_pointers (const goto_modelt &goto_model)
 returns true iff the given goto model has function calls via a function pointer More...
 

Detailed Description

Program Transformation.

Definition in file remove_function_pointers.cpp.

Function Documentation

◆ arg_is_type_compatible()

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

static void fix_argument_types ( code_function_callt function_call)
static

Definition at line 180 of file remove_function_pointers.cpp.

◆ fix_return_type()

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

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

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