|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Constant integer class. More...
#include <irep2_expr.h>
Public Member Functions | |
| constant_int2t (const type2tc &type, const BigInt &input, const irep_idt &fmt=irep_idt()) | |
| Primary constructor. | |
| constant_int2t (const constant_int2t &ref)=default | |
| unsigned long | as_ulong () const |
| Accessor for fetching machine-word unsigned integer of this constant. | |
| long | as_long () const |
| Accessor for fetching machine-word integer of this constant. | |
| 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 | |
| BigInt | value |
| irep_idt | cformat |
| How the literal was written in the source, as #cformat records it. | |
| 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 constexpr std::size_t | excluded_field_bytes = sizeof(irep_idt) |
| 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) |
Constant integer class.
Records a constant integer of an arbitary precision, signed or unsigned. Simplification operations will cause the integer to be clipped to whatever bit size is in expr type.
|
inline |
Primary constructor.
| type | Type of this integer. |
| input | BigInt object containing the integer we're dealing with |
|
default |
| long constant_int2t::as_long | ( | ) | const |
Accessor for fetching machine-word integer of this constant.
| unsigned long constant_int2t::as_ulong | ( | ) | const |
Accessor for fetching machine-word unsigned integer of this constant.
| irep_idt constant_int2t::cformat |
How the literal was written in the source, as #cformat records it.
Unreflected: two constants of the same value and type are the same constant however they were spelled, so this must not reach hashing or equality. Kept because c_expr2string prefers it over deriving the text from the type, and dropping it re-renders every printed literal (docs/roadmap/frontends-to-irep2.md ยง63).
|
staticconstexpr |
|
static |
|
staticconstexpr |
| BigInt constant_int2t::value |