CBMC
|
The vector type. More...
#include <std_types.h>
Protected Member Functions | |
const typet & | subtype () const |
typet & | subtype () |
![]() | |
void | detach () |
Additional Inherited Members | |
![]() | |
using | baset = tree_implementationt |
![]() | |
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 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 | |
![]() | |
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 |
The vector type.
Used to represent the short vectors used by CPU instruction sets such as MMX, SSE and AVX. They all provide registers that are something like 8 x int32, for example, and corresponding operations that operate element-wise on their operand vectors. Compared to array_typet, vector_typet has a fixed size whereas array_typet has no element-wise operators. Note that remove_vector.h
removes this data type by compilation into arrays.
Definition at line 1063 of file std_types.h.
vector_typet::vector_typet | ( | typet | index_type, |
typet | element_type, | ||
constant_exprt | size | ||
) |
Definition at line 281 of file std_types.cpp.
|
inline |
The type of the elements of the vector.
Definition at line 1086 of file std_types.h.
The type of the elements of the vector.
Definition at line 1080 of file std_types.h.
typet vector_typet::index_type | ( | ) | const |
The type of any index expression into an instance of this type.
Definition at line 291 of file std_types.cpp.
|
inline |
The type of any index expression into an instance of this type.
This is added as a comment now for backwards compatibility, but will eventually be the first subtype.
Definition at line 1074 of file std_types.h.
constant_exprt & vector_typet::size | ( | ) |
Definition at line 308 of file std_types.cpp.
const constant_exprt & vector_typet::size | ( | ) | const |
Definition at line 303 of file std_types.cpp.