cprover
|
A conditionally writable range of bytes. More...
Public Attributes | |
__CPROVER_bool | is_writable |
True iff __CPROVER_w_ok(lb, size) holds at creation. | |
__CPROVER_size_t | size |
Size of the range in bytes. | |
void * | lb |
Lower bound address of the range. | |
void * | ub |
Upper bound address of the range. | |
A conditionally writable range of bytes.
Definition at line 25 of file cprover_contracts.c.
__CPROVER_bool __CPROVER_contracts_car_t::is_writable |
True iff __CPROVER_w_ok(lb, size) holds at creation.
Definition at line 28 of file cprover_contracts.c.
void* __CPROVER_contracts_car_t::lb |
Lower bound address of the range.
Definition at line 32 of file cprover_contracts.c.
__CPROVER_size_t __CPROVER_contracts_car_t::size |
Size of the range in bytes.
Definition at line 30 of file cprover_contracts.c.
void* __CPROVER_contracts_car_t::ub |
Upper bound address of the range.
Definition at line 34 of file cprover_contracts.c.