CBMC: /home/runner/work/cbmc/cbmc/src/goto-programs/remove_function_pointers.h File Reference

CBMC

Loading...

Searching...

No Matches

remove_function_pointers.h File Reference

Remove Indirect Function Calls. More...

#include "goto_program.h"
#include <unordered_set>

+ Include dependency graph for remove_function_pointers.h:

+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

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

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.

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.

bool has_function_pointers (const goto_functionst &)

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

bool has_function_pointers (const goto_modelt &)

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

Detailed Description

Remove Indirect Function Calls.

Definition in file remove_function_pointers.h.

Function Documentation

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

◆ has_function_pointers() [1/2]

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 562 of file remove_function_pointers.cpp.

◆ has_function_pointers() [2/2]

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 571 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_handler Message handler to print warnings

symbol_table Symbol table

goto_program The goto program that contains target

function_id Name of function containing the target

target location with function call with function pointer

functions The 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 535 of file remove_function_pointers.cpp.