|
CBMC
|
Fixed-width bit-vector representing a signed or unsigned integer. More...
#include <bitvector_types.h>
Inheritance diagram for integer_bitvector_typet:
Collaboration diagram for integer_bitvector_typet:Additional Inherited Members | |
Public Types inherited from irept | |
| using | baset = tree_implementationt |
Public Types inherited from sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > > | |
| using | dt = tree_nodet< irept, forward_list_as_mapt< irep_idt, irept >, true > |
| using | subt = typename dt::subt |
| using | named_subt = typename dt::named_subt |
| using | tree_implementationt = sharing_treet |
| Used to refer to this class from derived classes. | |
Static Public Member Functions inherited from bitvector_typet | |
| static void | check (const typet &type, const validation_modet vm=validation_modet::INVARIANT) |
Static Public Member Functions inherited from typet | |
| static void | check (const typet &, const validation_modet=validation_modet::INVARIANT) |
| Check that the type is well-formed (shallow checks only, i.e., subtypes are not checked) | |
| static void | validate (const typet &type, const namespacet &, const validation_modet vm=validation_modet::INVARIANT) |
| Check that the type is well-formed, assuming that its subtypes have already been checked for well-formedness. | |
| static void | validate_full (const typet &type, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT) |
| Check that the type is well-formed (full check, including checks of subtypes) | |
Static Public Member Functions inherited from irept | |
| static bool | is_comment (const irep_idt &name) |
| static std::size_t | number_of_non_comments (const named_subt &) |
| count the number of named_sub elements that are not comments | |
Protected Member Functions inherited from sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > > | |
| void | detach () |
Static Protected Member Functions inherited from sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > > | |
| static void | remove_ref (dt *old_data) |
| static void | nonrecursive_destructor (dt *old_data) |
| Does the same as remove_ref, but using an explicit stack instead of recursion. | |
Protected Attributes inherited from sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > > | |
| dt * | data |
Static Protected Attributes inherited from sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > > | |
| static dt | empty_d |
Fixed-width bit-vector representing a signed or unsigned integer.
Definition at line 102 of file bitvector_types.h.
Definition at line 105 of file bitvector_types.h.
|
inline |
Definition at line 110 of file bitvector_types.h.
| mp_integer integer_bitvector_typet::largest | ( | ) | const |
Return the largest value that can be represented using this type.
Definition at line 50 of file bitvector_types.cpp.
| constant_exprt integer_bitvector_typet::largest_expr | ( | ) | const |
Return an expression representing the largest value of this type.
Definition at line 65 of file bitvector_types.cpp.
| mp_integer integer_bitvector_typet::smallest | ( | ) | const |
Return the smallest value that can be represented using this type.
Definition at line 45 of file bitvector_types.cpp.
| constant_exprt integer_bitvector_typet::smallest_expr | ( | ) | const |
Return an expression representing the smallest value of this type.
Definition at line 60 of file bitvector_types.cpp.
| constant_exprt integer_bitvector_typet::zero_expr | ( | ) | const |
Return an expression representing the zero value of this type.
Definition at line 55 of file bitvector_types.cpp.