CBMC
|
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they have a subtype) More...
#include <pointer_expr.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 | |
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they have a subtype)
Definition at line 23 of file pointer_expr.h.
|
inline |
Definition at line 26 of file pointer_expr.h.
|
inline |
The type of the data what we point to.
This method is preferred over .subtype(), which will eventually be deprecated.
Definition at line 43 of file pointer_expr.h.
The type of the data what we point to.
This method is preferred over .subtype(), which will eventually be deprecated.
Definition at line 35 of file pointer_expr.h.
|
inlinestatic |
Definition at line 67 of file pointer_expr.h.
|
inline |
Definition at line 62 of file pointer_expr.h.
|
inline |
Definition at line 56 of file pointer_expr.h.
Definition at line 49 of file pointer_expr.h.