Adapt user manual description of memory primitives

Author: danpoe

doc/cprover-manual/api.md

@@ -20,33 +20,6 @@ to the program. If the expression evaluates to false, the execution
 aborts without failure. More detail on the use of assumptions is in the
 section on [Assumptions](../modeling/assumptions/).
 
-#### \_\_CPROVER\_r_ok, \_\_CPROVER\_w_ok
-
-```C
-void __CPROVER_r_ok(const void *, size_t size);
-void __CPROVER_w_ok(const void *, size_t size);
-```
-
-The function **\_\_CPROVER\_r_ok** returns true if reading the piece of
-memory starting at the given pointer with the given size is safe.
-**\_\_CPROVER\_w_ok** does the same with writing.
-
-#### \_\_CPROVER\_same\_object, \_\_CPROVER\_POINTER\_OBJECT, \_\_CPROVER\_POINTER\_OFFSET, \_\_CPROVER\_DYNAMIC\_OBJECT
-
-```C
-_Bool __CPROVER_same_object(const void *, const void *);
-__CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *p);
-__CPROVER_ssize_t __CPROVER_POINTER_OFFSET(const void *p);
-_Bool __CPROVER_DYNAMIC_OBJECT(const void *p);
-```
-
-The function **\_\_CPROVER\_same\_object** returns true if the two
-pointers given as arguments point to the same object. The function
-**\_\_CPROVER\_POINTER\_OFFSET** returns the offset of the given pointer
-relative to the base address of the object. The function
-**\_\_CPROVER\_DYNAMIC\_OBJECT** returns true if the pointer passed as
-arguments points to a dynamically allocated object.
-
 #### \_\_CPROVER\_input, \_\_CPROVER\_output
 
 ```C
@@ -156,6 +129,47 @@ the array **dest** with the given value.
 
 Uninterpreted functions are documented [here](./modeling-nondeterminism.md)).
 
+### Memory-Related Functions
+
+The semantics of the primitives listed in this section is described in more detail in the
+document about [Memory Primitives](http://cprover.diffblue.com/memory-primitives.html).
+
+#### \_\_CPROVER\_POINTER\_OBJECT, \_\_CPROVER\_POINTER\_OFFSET, \_\_CPROVER\_same\_object
+
+```C
+__CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *p);
+__CPROVER_ssize_t __CPROVER_POINTER_OFFSET(const void *p);
+_Bool __CPROVER_same_object(const void *p, const void *q);
+```
+
+The function **\_\_CPROVER\_POINTER\_OBJECT** returns the ID of the object the
+pointer points to. The function **\_\_CPROVER\_POINTER\_OFFSET** returns the
+offset of the given pointer relative to the base address of the object. The
+function **\_\_CPROVER\_same\_object** returns true if the two pointers given as
+arguments point to the same object.
+
+#### \_\_CPROVER\_OBJECT\_SIZE, \_\_CPROVER\_DYNAMIC\_OBJECT, \_\_CPROVER\_r\_ok, \_\_CPROVER\_w\_ok
+
+The following primitives require a pointer that is null or valid in order to
+have well-defined semantics in all usage cases. See the document about
+[Memory Primitives](http://cprover.diffblue.com/memory-primitives.html)
+for more details. It also includes a description of the `--pointer-primitive-check`
+option to verify the preconditions of the primitives.
+
+```C
+__CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *p);
+_Bool __CPROVER_DYNAMIC_OBJECT(const void *p);
+void __CPROVER_r_ok(const void *p, size_t size);
+void __CPROVER_w_ok(const void *p, size_t size);
+```
+
+The function **\_\_CPROVER_\_OBJECT\_SIZE** returns the size of the object the
+given pointer points to. The function **\_\_CPROVER\_DYNAMIC\_OBJECT** returns
+true if the pointer passed as an argument points to a dynamically allocated
+object. The function **\_\_CPROVER\_r_ok** returns true if reading the piece of
+memory starting at the given pointer with the given size is safe.
+**\_\_CPROVER\_w_ok** does the same with writing.
+
 ### Predefined Types and Symbols
 
 #### \_\_CPROVER\_bitvector