Merge pull request #2602 from diffblue/__CPROVER_r/w_ok

__CPROVER_r_ok and __CPROVER_w_ok preconditions

Author: Daniel Kroening

doc/cbmc-user-manual.md

@@ -2190,6 +2190,15 @@ 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 and Assertions](modeling-assertions.shtml).
 
+#### \_\_CPROVER\_r_ok, \_\_CPROVER\_w_ok
+
+    void __CPROVER_r_ok(const void *, size_t size);
+    void __CPROVER_w_ok(cosnt 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
 
     _Bool __CPROVER_same_object(const void *, const void *);

regression/cbmc/memcpy1/test.desc

@@ -4,7 +4,7 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-\[(__builtin___memcpy_chk|memcpy)\.pointer_dereference\.[0-9]+\] dereference failure: pointer outside object bounds in \*\(\(\(const char \*\)src \+ \(signed (long (long )?)?int\)n\) - (\(signed long (long )?int\))?1\): FAILURE$
+^\[main\.precondition_instance\..*\] memcpy source region readable: FAILURE$
 \*\* 1 of [0-9]+ failed
 --
 ^warning: ignoring

regression/cbmc/memset1/test.desc

@@ -4,7 +4,7 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-\[main.assertion.7\] assertion A\[1\]==0x01010111: FAILURE
-\*\* 1 of 12 failed 
+^\[main.assertion.7\] assertion A\[1\]==0x01010111: FAILURE$
+\*\* 1 of [0-9]+ failed
 --
 ^warning: ignoring

regression/cbmc/memset3/test.desc

@@ -4,7 +4,7 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-\[.*] dereference failure: pointer outside dynamic object bounds in .*: FAILURE
-\*\* 2 of .* failed \(.*\)
+^\[main\.precondition_instance\..*] memset destination region writeable: FAILURE$
+\*\* 1 of [0-9]+ failed \(.*\)
 --
 ^warning: ignoring