|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Constant class for string constants. More...
#include <irep2_expr.h>
Public Types | |
| using | kindt = constant_string_kindt |
| 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 |
Public Member Functions | |
| constant_string2t (const type2tc &type, const irep_idt &stringref, constant_string_kindt kind) | |
| Primary constructor. | |
| constant_string2t (const constant_string2t &ref)=default | |
| expr2tc | to_array () const |
| Convert string to a constant length array of characters. | |
| size_t | array_size () const |
| sizeof(literal)/sizeof(*literal), i.e., the number of elements in the underlying array, including the '\0' terminator | |
| expr2tc | at (size_t i) const |
| Extract the i-th element from the string for i between 0 and to_array_type(this->type).array_size (not the same as value.c_str()[i] when to_array_type(this->type).subtype != char type). | |
| 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 | |
| irep_idt | value |
| constant_string_kindt | kind |
| 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 | |
| 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 class for string constants.
Contains an irep_idt representing the constant string.
|
inline |
Primary constructor.
| type | Type of this string; presumably an array_type2t. |
| stringref | String pool'd string we're dealing with |
| kind | The kind of string literal:
|
|
default |
| size_t constant_string2t::array_size | ( | ) | const |
sizeof(literal)/sizeof(*literal), i.e., the number of elements in the underlying array, including the '\0' terminator
Extract the i-th element from the string for i between 0 and to_array_type(this->type).array_size (not the same as value.c_str()[i] when to_array_type(this->type).subtype != char type).
| expr2tc constant_string2t::to_array | ( | ) | const |
Convert string to a constant length array of characters.
|
static |
|
staticconstexpr |
| constant_string_kindt constant_string2t::kind |
| irep_idt constant_string2t::value |