CBMC
|
Value Set. More...
Go to the source code of this file.
Classes | |
class | goto_program_dereferencet |
Wrapper for functions removing dereferences in expressions contained in a goto program. More... | |
Macros | |
#define | OPT_REMOVE_POINTERS "(remove-pointers)" |
#define | HELP_REMOVE_POINTERS |
Functions | |
void | dereference (const irep_idt &function_id, goto_programt::const_targett target, exprt &expr, const namespacet &, value_setst &, message_handlert &) |
Remove dereferences in expr using value_sets to determine to what objects the pointers may be pointing to. More... | |
void | remove_pointers (goto_modelt &, value_setst &, message_handlert &) |
Remove dereferences in all expressions contained in the program goto_model . More... | |
Value Set.
Definition in file goto_program_dereference.h.
#define HELP_REMOVE_POINTERS |
Definition at line 108 of file goto_program_dereference.h.
#define OPT_REMOVE_POINTERS "(remove-pointers)" |
Definition at line 106 of file goto_program_dereference.h.
void dereference | ( | const irep_idt & | function_id, |
goto_programt::const_targett | target, | ||
exprt & | expr, | ||
const namespacet & | ns, | ||
value_setst & | value_sets, | ||
message_handlert & | message_handler | ||
) |
Remove dereferences in expr
using value_sets
to determine to what objects the pointers may be pointing to.
Definition at line 278 of file goto_program_dereference.cpp.
void remove_pointers | ( | goto_modelt & | goto_model, |
value_setst & | value_sets, | ||
message_handlert & | message_handler | ||
) |
Remove dereferences in all expressions contained in the program goto_model
.
value_sets
is used to determine to what objects the pointers may be pointing to.
Definition at line 260 of file goto_program_dereference.cpp.