cprover
value_set_fi_fp_removal.cpp File Reference
+ Include dependency graph for value_set_fi_fp_removal.cpp:

Go to the source code of this file.

Functions

void fix_argument_types (code_function_callt &function_call, const namespacet &ns)
 
void fix_return_type (code_function_callt &function_call, goto_programt &dest, goto_modelt &goto_model)
 
void remove_function_pointer (goto_programt &goto_program, goto_programt::targett target, const std::set< symbol_exprt > &functions, goto_modelt &goto_model)
 
void value_set_fi_fp_removal (goto_modelt &goto_model, message_handlert &message_handler)
 Builds the flow-insensitive value set for all function pointers and replaces function pointers with a non-deterministic switch between this set. More...
 

Function Documentation

◆ fix_argument_types()

void fix_argument_types ( code_function_callt function_call,
const namespacet ns 
)

Definition at line 29 of file value_set_fi_fp_removal.cpp.

◆ fix_return_type()

void fix_return_type ( code_function_callt function_call,
goto_programt dest,
goto_modelt goto_model 
)

Definition at line 51 of file value_set_fi_fp_removal.cpp.

◆ remove_function_pointer()

void remove_function_pointer ( goto_programt goto_program,
goto_programt::targett  target,
const std::set< symbol_exprt > &  functions,
goto_modelt goto_model 
)

Definition at line 89 of file value_set_fi_fp_removal.cpp.

◆ value_set_fi_fp_removal()

void value_set_fi_fp_removal ( goto_modelt goto_model,
message_handlert message_handler 
)

Builds the flow-insensitive value set for all function pointers and replaces function pointers with a non-deterministic switch between this set.

If the set is empty, the function pointer is not removed. Thus remove_function_pointers should be run after this to

Parameters
goto_modelgoto model to be modified
message_handlermessage handler for status output

Definition at line 188 of file value_set_fi_fp_removal.cpp.