__CPROVER_contracts_car_t Struct Reference

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.

Detailed Description

A conditionally writable range of bytes.

Definition at line 25 of file cprover_contracts.c.

Member Data Documentation

is_writable

__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.

lb

void* __CPROVER_contracts_car_t::lb

Lower bound address of the range.

Definition at line 32 of file cprover_contracts.c.

size

__CPROVER_size_t __CPROVER_contracts_car_t::size

Size of the range in bytes.

Definition at line 30 of file cprover_contracts.c.

ub

void* __CPROVER_contracts_car_t::ub

Upper bound address of the range.

Definition at line 34 of file cprover_contracts.c.

---

The documentation for this struct was generated from the following file:

• ansi-c/library/cprover_contracts.c