cprover
|
#include "value_set_fi_fp_removal.h"
#include <goto-programs/goto_model.h>
#include <goto-programs/remove_function_pointers.h>
#include <pointer-analysis/value_set_analysis_fi.h>
#include <util/base_type.h>
#include <util/c_types.h>
#include <util/expanding_vector.h>
#include <util/fresh_symbol.h>
#include <util/message.h>
#include <util/namespace.h>
#include <util/std_code.h>
#include <util/union_find.h>
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... | |
void fix_argument_types | ( | code_function_callt & | function_call, |
const namespacet & | ns | ||
) |
Definition at line 29 of file value_set_fi_fp_removal.cpp.
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.
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.
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
goto_model | goto model to be modified |
message_handler | message handler for status output |
Definition at line 188 of file value_set_fi_fp_removal.cpp.