9#ifndef CPROVER_GOTO_SYMEX_SIMPLIFY_EXPR_WITH_VALUE_SET_H
10#define CPROVER_GOTO_SYMEX_SIMPLIFY_EXPR_WITH_VALUE_SET_H
A base class for relations, i.e., binary predicates whose two operands have the same type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The offset (in bytes) of a pointer relative to the object.
resultt simplify_pointer_offset(const pointer_offset_exprt &) override
simplify_expr_with_value_sett(const value_sett &_vs, const irep_idt &_mode, const namespacet &_ns)
const value_sett & value_set
resultt simplify_inequality(const binary_relation_exprt &) override
simplifies inequalities !=, <=, <, >=, >, and also ==
resultt simplify_inequality_pointer_object(const binary_relation_exprt &) override
When all candidates in the value set have the same offset we can replace a pointer_offset expression ...
const irep_idt language_mode
simplify_exprt(const namespacet &_ns)
State type in value_set_domaint, used in value-set analysis and goto-symex.
resultt
The result of goto verifying.