|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
#include <irep2_expr.h>
Public Member Functions | |
| code_switch2t (const expr2tc &v, const expr2tc &b, const locationt &loc=locationt()) | |
| code_switch2t (const code_switch2t &ref)=default | |
| Public Member Functions inherited from expr2t | |
| virtual | ~expr2t ()=default |
| expr2tc | clone () const |
| expr2tc | with_type (const type2tc &new_type) const |
| Build a fresh expression of the same kind and field values as this one, but with a different type. | |
| bool | operator== (const expr2t &ref) const |
| bool | operator< (const expr2t &ref) const |
| bool | operator!= (const expr2t &ref) const |
| std::string | pretty (unsigned int indent=0) const |
| Produce textual representation of this expr. | |
| DUMP_METHOD void | dump () const |
| Write textual representation of this object to stdout. | |
| size_t | crc () const |
| Calculate a hash/digest of the current expr. | |
| bool | cmp (const expr2t &ref) const |
| Structural comparison. | |
| int | lt (const expr2t &ref) const |
| Trinary structural ordering. | |
| list_of_memberst | tostring (unsigned int indent) const |
| Convert fields of subclasses to a string representation. | |
| const expr2tc * | get_sub_expr (size_t idx) const |
| Fetch a sub-operand. | |
| size_t | get_num_sub_exprs () const |
| Count the number of sub-exprs there are. | |
| expr2tc | simplify () const |
| Simplify an expression. | |
| expr2tc | simplify (bool suppress_reassoc) const |
| Simplify with reassociation suppression. | |
| virtual expr2tc | do_simplify () const |
| expr-specific simplification methods. | |
| template<typename T> | |
| void | foreach_operand (T &&t) const |
| Indirect, abstract operand iteration. | |
| template<typename T> | |
| void | Foreach_operand (T &&t) |
| Public Member Functions inherited from irep2t | |
| irep2t () noexcept | |
| irep2t (const irep2t &) noexcept | |
| irep2t & | operator= (const irep2t &)=delete |
| virtual | ~irep2t ()=default |
| void | mark_writer () const noexcept |
| void | clear_writer () const noexcept |
Public Attributes | |
| expr2tc | value |
| expr2tc | body |
| locationt | location |
| Public Attributes inherited from expr2t | |
| const expr_ids | expr_id |
| Instance of expr_ids recording tihs exprs type. | |
| const type2tc | type |
| Type of this expr. | |
| std::atomic< size_t > | crc_val |
| Public Attributes inherited from irep2t | |
| std::atomic< unsigned int > | refcount |
| std::atomic< std::uintptr_t > | writer_thread |
Static Public Attributes | |
| static constexpr std::size_t | excluded_field_bytes = sizeof(locationt) |
| static constexpr auto | fields |
| static std::string | field_names [esbmct::num_type_fields] |
Additional Inherited Members | |
| Public Types inherited from expr2t | |
| enum | expr_ids { end_expr_id } |
| Enumeration identifying each sort of expr. More... | |
| typedef esbmct::function_ref< void(const expr2tc &)> | const_op_delegate |
| typedef esbmct::function_ref< void(expr2tc &)> | op_delegate |
| typedef expr2tc | container_type |
| typedef expr2t | base_type |
| Static Public Member Functions inherited from irep2t | |
| static std::uintptr_t | current_thread_tag () noexcept |
| Protected Member Functions inherited from expr2t | |
| expr2t (const type2tc &type, expr_ids id) | |
| Primary constructor. | |
| expr2t (const expr2t &ref) | |
| Copy constructor. | |
| void | foreach_operand_impl_const (const_op_delegate &expr) const |
| void | foreach_operand_impl (op_delegate &expr) |
|
inline |
|
default |
| expr2tc code_switch2t::body |
|
staticconstexpr |
|
static |
|
staticconstexpr |
| locationt code_switch2t::location |
| expr2tc code_switch2t::value |