|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
sizeof(T) expression. More...
#include <irep2_expr.h>
Public Member Functions | |
| sizeof2t (const type2tc &type, const expr2tc &val, const type2tc &sizeof_t) | |
| sizeof2t (const sizeof2t &ref)=default | |
| expr2tc | do_simplify () const override |
| expr-specific simplification methods. | |
| 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. | |
| 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 |
| type2tc | sizeof_type |
| 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 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) |
sizeof(T) expression.
Replaces the legacy sizeof-type irep attribute side channel (esbmc/esbmc#5337) with two first-class reflected fields:
|
default |
|
overridevirtual |
expr-specific simplification methods.
By default, an expression can't be simplified, and this method returns a nil expression to show that. However if simplification is possible, the subclass overrides this and if it can simplify its operands, returns a new simplified expression. It should attempt to modify itself (it's const).
If simplification failed the first time around, the simplify method will simplify this expressions individual operands, and will then call an expr with the simplified operands to see if it's now become simplifiable. This call occurs whether or not any operands were actually simplified, see below.
The 'second' parameter can be used to avoid invoking expensive attempts to simplify an expression more than once - on the first call to do_simplify this parameter will be false, then on the second it's be true, allowing method implementation to save the expensive stuff until all of its operands have certainly been simplified.
Currently simplification does some things that it shouldn't: pointer arithmetic for example. I'm not sure where this can be relocated to though.
Reimplemented from expr2t.
|
static |
|
staticconstexpr |
| type2tc sizeof2t::sizeof_type |
| expr2tc sizeof2t::value |