cprover
|
Value Set. More...
#include <util/namespace.h>
#include <goto-programs/goto_functions.h>
#include "value_sets.h"
#include "value_set_dereference.h"
Go to the source code of this file.
Classes | |
class | goto_program_dereferencet |
Functions | |
void | dereference (goto_programt::const_targett target, exprt &expr, const namespacet &ns, value_setst &value_sets) |
void | remove_pointers (goto_programt &goto_program, symbol_tablet &symbol_table, value_setst &value_sets) |
void | remove_pointers (goto_functionst &goto_functions, symbol_tablet &symbol_table, value_setst &value_sets) |
void | pointer_checks (goto_programt &goto_program, symbol_tablet &symbol_table, const optionst &options, value_setst &value_sets) |
void | pointer_checks (goto_functionst &goto_functions, symbol_tablet &symbol_table, const optionst &options, value_setst &value_sets) |
Value Set.
Definition in file goto_program_dereference.h.
void dereference | ( | goto_programt::const_targett | target, |
exprt & | expr, | ||
const namespacet & | ns, | ||
value_setst & | value_sets | ||
) |
Definition at line 434 of file goto_program_dereference.cpp.
References goto_program_dereferencet::dereference_expression(), and goto_program_dereferencet::options.
void pointer_checks | ( | goto_programt & | goto_program, |
symbol_tablet & | symbol_table, | ||
const optionst & | options, | ||
value_setst & | value_sets | ||
) |
Definition at line 410 of file goto_program_dereference.cpp.
References goto_program_dereferencet::ns, and goto_program_dereferencet::pointer_checks().
void pointer_checks | ( | goto_functionst & | goto_functions, |
symbol_tablet & | symbol_table, | ||
const optionst & | options, | ||
value_setst & | value_sets | ||
) |
Definition at line 422 of file goto_program_dereference.cpp.
References goto_program_dereferencet::ns, and goto_program_dereferencet::pointer_checks().
void remove_pointers | ( | goto_programt & | goto_program, |
symbol_tablet & | symbol_table, | ||
value_setst & | value_sets | ||
) |
Definition at line 379 of file goto_program_dereference.cpp.
References goto_program_dereferencet::dereference_program(), goto_program_dereferencet::ns, and goto_program_dereferencet::options.
Referenced by goto_instrument_parse_optionst::instrument_goto_program().
void remove_pointers | ( | goto_functionst & | goto_functions, |
symbol_tablet & | symbol_table, | ||
value_setst & | value_sets | ||
) |
Definition at line 394 of file goto_program_dereference.cpp.
References goto_program_dereferencet::dereference_program(), Forall_goto_functions, goto_program_dereferencet::ns, and goto_program_dereferencet::options.