A conditionally writable range of bytes. More...

Public Attributes
unsigned char	is_writable
	True iff __CPROVER_w_ok(lb, size) holds at creation. More...

__CPROVER_size_t	size
	Size of the range in bytes. More...

void *	lb
	Lower bound address of the range. More...

void *	ub
	Upper bound address of the range. More...

Detailed Description

A conditionally writable range of bytes.

Definition at line 24 of file cprover_contracts.c.

Member Data Documentation

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.

void* __CPROVER_contracts_car_t::lb

Lower bound address of the range.

Definition at line 31 of file cprover_contracts.c.

__CPROVER_size_t __CPROVER_contracts_car_t::size

Size of the range in bytes.

Definition at line 29 of file cprover_contracts.c.

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: