Skip to content

Commit 3e8b6df

Browse files
committed
Document __CPROVER_rw_ok
This adds documentation for __CPROVER_rw_ok, in addition to r_ok and w_ok.
1 parent 07895ef commit 3e8b6df

File tree

1 file changed

+4
-3
lines changed

1 file changed

+4
-3
lines changed

doc/architectural/memory-primitives.md

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -169,12 +169,13 @@ to pointers that point to within a memory object.
169169
170170
## Checking if a memory segment has at least a given size
171171
172-
The following two primitives can be used to check whether there is a memory
173-
segment starting at the given pointer and extending for at least the given
174-
number of bytes:
172+
The following three primitives can be used to check whether there is a
173+
memory segment starting at the given pointer and extending for at least the
174+
given number of bytes:
175175
176176
- `_Bool __CPROVER_r_ok(const void *p, size_t size)`
177177
- `_Bool __CPROVER_w_ok(const void *p, size_t size)`
178+
- `_Bool __CPROVER_rw_ok(const void *p, size_t size)`
178179
179180
At present, both primitives are equivalent as all memory in CBMC is considered
180181
both readable and writeable. If `p` is the null pointer, the primitives return

0 commit comments

Comments
 (0)