Runtime representation of a write set. More...
Collaboration diagram for __CPROVER_contracts_write_set_t:Public Attributes | |
| __CPROVER_contracts_car_set_t | contract_assigns |
| Set of car derived from the contract. More... | |
| __CPROVER_contracts_obj_set_t | contract_frees |
| Set of freeable pointers derived from the contract (indexed mode) More... | |
| __CPROVER_contracts_obj_set_t | contract_frees_append |
| Set of freeable pointers derived from the contract (append mode) More... | |
| __CPROVER_contracts_obj_set_t | allocated |
| Set of objects allocated by the function under analysis (indexed mode) More... | |
| __CPROVER_contracts_obj_set_t | deallocated |
| Set of objects deallocated by the function under analysis (indexed mode) More... | |
| __CPROVER_contracts_obj_set_ptr_t | linked_is_fresh |
| Pointer to object set supporting the is_fresh predicate checks (indexed mode) More... | |
| __CPROVER_contracts_obj_set_ptr_t | linked_allocated |
| Object set recording the is_fresh allocations in post conditions. More... | |
| __CPROVER_contracts_obj_set_ptr_t | linked_deallocated |
| Object set recording the deallocations (used by was_freed) More... | |
| unsigned char | assume_requires_ctx |
| True iff the write set checks requires clauses in an assumption ctx. More... | |
| unsigned char | assert_requires_ctx |
| True iff the write set checks requires clauses in an assertion ctx. More... | |
| unsigned char | assume_ensures_ctx |
| True iff the write set checks ensures clauses in an assumption ctx. More... | |
| unsigned char | assert_ensures_ctx |
| True iff this write set checks ensures clauses in an assertion ctx. More... | |
| unsigned char | allow_allocate |
| True iff dynamic allocation is allowed (default: true) More... | |
| unsigned char | allow_deallocate |
| True iff dynamic deallocation is allowed (default: true) More... | |
Detailed Description
Runtime representation of a write set.
Definition at line 71 of file cprover_contracts.c.
Member Data Documentation
◆ allocated
| __CPROVER_contracts_obj_set_t __CPROVER_contracts_write_set_t::allocated |
Set of objects allocated by the function under analysis (indexed mode)
Definition at line 81 of file cprover_contracts.c.
◆ allow_allocate
| unsigned char __CPROVER_contracts_write_set_t::allow_allocate |
True iff dynamic allocation is allowed (default: true)
Definition at line 101 of file cprover_contracts.c.
◆ allow_deallocate
| unsigned char __CPROVER_contracts_write_set_t::allow_deallocate |
True iff dynamic deallocation is allowed (default: true)
Definition at line 103 of file cprover_contracts.c.
◆ assert_ensures_ctx
| unsigned char __CPROVER_contracts_write_set_t::assert_ensures_ctx |
True iff this write set checks ensures clauses in an assertion ctx.
Definition at line 99 of file cprover_contracts.c.
◆ assert_requires_ctx
| unsigned char __CPROVER_contracts_write_set_t::assert_requires_ctx |
True iff the write set checks requires clauses in an assertion ctx.
Definition at line 95 of file cprover_contracts.c.
◆ assume_ensures_ctx
| unsigned char __CPROVER_contracts_write_set_t::assume_ensures_ctx |
True iff the write set checks ensures clauses in an assumption ctx.
Definition at line 97 of file cprover_contracts.c.
◆ assume_requires_ctx
| unsigned char __CPROVER_contracts_write_set_t::assume_requires_ctx |
True iff the write set checks requires clauses in an assumption ctx.
Definition at line 93 of file cprover_contracts.c.
◆ contract_assigns
| __CPROVER_contracts_car_set_t __CPROVER_contracts_write_set_t::contract_assigns |
Set of car derived from the contract.
Definition at line 74 of file cprover_contracts.c.
◆ contract_frees
| __CPROVER_contracts_obj_set_t __CPROVER_contracts_write_set_t::contract_frees |
Set of freeable pointers derived from the contract (indexed mode)
Definition at line 76 of file cprover_contracts.c.
◆ contract_frees_append
| __CPROVER_contracts_obj_set_t __CPROVER_contracts_write_set_t::contract_frees_append |
Set of freeable pointers derived from the contract (append mode)
Definition at line 78 of file cprover_contracts.c.
◆ deallocated
| __CPROVER_contracts_obj_set_t __CPROVER_contracts_write_set_t::deallocated |
Set of objects deallocated by the function under analysis (indexed mode)
Definition at line 84 of file cprover_contracts.c.
◆ linked_allocated
| __CPROVER_contracts_obj_set_ptr_t __CPROVER_contracts_write_set_t::linked_allocated |
Object set recording the is_fresh allocations in post conditions.
Definition at line 89 of file cprover_contracts.c.
◆ linked_deallocated
| __CPROVER_contracts_obj_set_ptr_t __CPROVER_contracts_write_set_t::linked_deallocated |
Object set recording the deallocations (used by was_freed)
Definition at line 91 of file cprover_contracts.c.
◆ linked_is_fresh
| __CPROVER_contracts_obj_set_ptr_t __CPROVER_contracts_write_set_t::linked_is_fresh |
Pointer to object set supporting the is_fresh predicate checks (indexed mode)
Definition at line 87 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
