|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
#include <goto-programs/goto_functions.h>#include <pointer-analysis/dereference.h>#include <pointer-analysis/value_sets.h>#include <util/symtab/namespace.h>Go to the source code of this file.
Classes | |
| class | goto_program_dereferencet |
Functions | |
| void | dereference (goto_programt::const_targett target, expr2tc &expr, const namespacet &ns, value_setst &value_sets) |
| void dereference | ( | goto_programt::const_targett | target, |
| expr2tc & | expr, | ||
| const namespacet & | ns, | ||
| value_setst & | value_sets ) |