CBMC
|
Arrays with given size. 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 &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 | |
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 | 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 |
Arrays with given size.
Used for ordinary source-language arrays.
Definition at line 806 of file std_types.h.
Definition at line 809 of file std_types.h.
|
static |
Definition at line 20 of file std_types.cpp.
|
inline |
The type of the elements of the array.
Definition at line 833 of file std_types.h.
The type of the elements of the array.
Definition at line 827 of file std_types.h.
typet array_typet::index_type | ( | ) | const |
The type of the index expressions into any instance of this type.
Definition at line 34 of file std_types.cpp.
|
inline |
The type of the index expressions into any instance of this type.
This is added as a comment now for backwards compatibility, but will eventually be the first subtype.
Definition at line 821 of file std_types.h.
|
inline |
Definition at line 852 of file std_types.h.
|
inline |
Definition at line 857 of file std_types.h.
|
inline |
Definition at line 847 of file std_types.h.
Definition at line 840 of file std_types.h.