__CPROVER_contracts_car_t Struct Reference

A conditionally writable range of bytes. More...

Public Attributes
unsigned char	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 24 of file cprover_contracts.c.

Member Data Documentation

is_writable

unsigned char __CPROVER_contracts_car_t::is_writable

True iff __CPROVER_w_ok(lb, size) holds at creation.

Definition at line 27 of file cprover_contracts.c.

lb

void* __CPROVER_contracts_car_t::lb

Lower bound address of the range.

Definition at line 31 of file cprover_contracts.c.

size

__CPROVER_size_t __CPROVER_contracts_car_t::size

Size of the range in bytes.

Definition at line 29 of file cprover_contracts.c.

ub

void* __CPROVER_contracts_car_t::ub

Upper bound address of the range.

Definition at line 33 of file cprover_contracts.c.

---

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

• /home/runner/work/cbmc/cbmc/src/ansi-c/library/cprover_contracts.c