cprover
|
Fixed-width bit-vector representing a signed or unsigned integer. More...
#include <bitvector_types.h>
Additional Inherited Members | |
![]() | |
using | baset = tree_implementationt |
![]() | |
using | dt |
using | subt |
using | named_subt |
using | tree_implementationt |
Used to refer to this class from derived classes. | |
![]() | |
static void | check (const typet &type, const validation_modet vm=validation_modet::INVARIANT) |
![]() | |
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 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 | |
![]() | |
void | detach () |
![]() | |
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. | |
![]() | |
dt * | data |
![]() | |
static dt | empty_d |
Fixed-width bit-vector representing a signed or unsigned integer.
Definition at line 98 of file bitvector_types.h.
Definition at line 101 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 38 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 53 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 33 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 48 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 43 of file bitvector_types.cpp.