|
cprover
|
#include "simplify_expr_with_value_set.h"#include <util/expr_util.h>#include <util/pointer_expr.h>#include <util/simplify_expr.h>#include <util/ssa_expr.h>#include <pointer-analysis/add_failed_symbols.h>#include <pointer-analysis/value_set.h>#include <pointer-analysis/value_set_dereference.h>#include "goto_symex_can_forward_propagate.h"Go to the source code of this file.
Functions | |
| static std::optional< exprt > | try_evaluate_pointer_comparison (const irep_idt &operation, const symbol_exprt &symbol_expr, const exprt &other_operand, const value_sett &value_set, const irep_idt language_mode, const namespacet &ns) |
| Try to evaluate a simple pointer comparison. | |
|
static |
Try to evaluate a simple pointer comparison.
| operation | ID_equal or ID_not_equal |
| symbol_expr | The symbol expression in the condition |
| other_operand | The other expression in the condition; we only support an address of expression, a typecast of an address of expression or a null pointer, and return an empty std::optional in all other cases |
| value_set | The value-set for looking up what the symbol can point to |
| language_mode | The language mode |
| ns | A namespace |
Definition at line 33 of file simplify_expr_with_value_set.cpp.