|
CBMC
|
A set of pointers. More...
Public Attributes | |
| __CPROVER_size_t | max_elems |
| Maximum number of elements that can be stored in the set. | |
| __CPROVER_size_t | watermark |
| next usable index in elems if less than max_elems (1 + greatest used index in elems) | |
| __CPROVER_size_t | nof_elems |
| Number of elements currently in the elems array. | |
| unsigned char | is_empty |
| True iff nof_elems is 0. | |
| unsigned char | indexed_by_object_id |
| True iff elems is indexed by the object id of the pointers. | |
| void ** | elems |
| Array of void *pointers, indexed by their object ID or some other order. | |
A set of pointers.
Definition at line 49 of file cprover_contracts.c.
| void** __CPROVER_contracts_obj_set_t::elems |
Array of void *pointers, indexed by their object ID or some other order.
Definition at line 64 of file cprover_contracts.c.
True iff elems is indexed by the object id of the pointers.
Definition at line 61 of file cprover_contracts.c.
True iff nof_elems is 0.
Definition at line 59 of file cprover_contracts.c.
| __CPROVER_size_t __CPROVER_contracts_obj_set_t::max_elems |
Maximum number of elements that can be stored in the set.
Definition at line 52 of file cprover_contracts.c.
| __CPROVER_size_t __CPROVER_contracts_obj_set_t::nof_elems |
Number of elements currently in the elems array.
Definition at line 57 of file cprover_contracts.c.
| __CPROVER_size_t __CPROVER_contracts_obj_set_t::watermark |
next usable index in elems if less than max_elems (1 + greatest used index in elems)
Definition at line 55 of file cprover_contracts.c.