cprover
|
Dereferencing Operations on GOTO Programs. More...
#include "goto_program_dereference.h"
#include <util/expr_util.h>
#include <util/simplify_expr.h>
#include <util/base_type.h>
#include <util/std_code.h>
#include <util/symbol_table.h>
#include <util/guard.h>
#include <util/options.h>
Go to the source code of this file.
Functions | |
void | remove_pointers (goto_programt &goto_program, symbol_tablet &symbol_table, value_setst &value_sets) |
void | remove_pointers (goto_modelt &goto_model, value_setst &value_sets) |
Remove dereferences in all expressions contained in the program goto_model . More... | |
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) |
void | dereference (goto_programt::const_targett target, exprt &expr, const namespacet &ns, value_setst &value_sets) |
Remove dereferences in expr using value_sets to determine to what objects the pointers may be pointing to. More... | |
Dereferencing Operations on GOTO Programs.
Definition in file goto_program_dereference.cpp.
void dereference | ( | goto_programt::const_targett | target, |
exprt & | expr, | ||
const namespacet & | ns, | ||
value_setst & | value_sets | ||
) |
Remove dereferences in expr
using value_sets
to determine to what objects the pointers may be pointing to.
Definition at line 462 of file goto_program_dereference.cpp.
void pointer_checks | ( | goto_programt & | goto_program, |
symbol_tablet & | symbol_table, | ||
const optionst & | options, | ||
value_setst & | value_sets | ||
) |
Definition at line 435 of file goto_program_dereference.cpp.
void pointer_checks | ( | goto_functionst & | goto_functions, |
symbol_tablet & | symbol_table, | ||
const optionst & | options, | ||
value_setst & | value_sets | ||
) |
Definition at line 448 of file goto_program_dereference.cpp.
void remove_pointers | ( | goto_programt & | goto_program, |
symbol_tablet & | symbol_table, | ||
value_setst & | value_sets | ||
) |
Definition at line 400 of file goto_program_dereference.cpp.
void remove_pointers | ( | goto_modelt & | goto_model, |
value_setst & | value_sets | ||
) |
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 418 of file goto_program_dereference.cpp.