CBMC
|
Base class of fixed-width bit-vector types. More...
#include <std_types.h>
Static Public Member Functions | |
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 | |
Base class of fixed-width bit-vector types.
Superclass of anything represented by bits, for example integers (in 32 or 64-bit representation), floating point numbers etc. In contrast, integer_typet is a direct integer representation.
Definition at line 908 of file std_types.h.
Definition at line 911 of file std_types.h.
Definition at line 915 of file std_types.h.
|
inline |
Definition at line 920 of file std_types.h.
|
inlinestatic |
Definition at line 939 of file std_types.h.
|
inline |
Definition at line 925 of file std_types.h.
|
inline |
Definition at line 932 of file std_types.h.
std::size_t bitvector_typet::width | ( | ) | const |
Definition at line 158 of file std_types.cpp.
void bitvector_typet::width | ( | const mp_integer & | width | ) |
Definition at line 163 of file std_types.cpp.