Add test showing limitations of __CPROVER_w_ok

We do not currently have a good way of distinguishing lvalues from
rvalues, and thus actually treat __CPROVER_w_ok and __CPROVER_r_ok the
same. The test shows that this shouldn't always be done.

Author: tautschnig

regression/cbmc/r_w_ok3/main.c

@@ -0,0 +1,8 @@
+#include <assert.h>
+
+int main()
+{
+  const char *str = "foobar";
+  assert(!__CPROVER_w_ok(str, 6));
+  assert(__CPROVER_r_ok(str, 6));
+}

regression/cbmc/r_w_ok3/test.desc

@@ -0,0 +1,12 @@
+KNOWNBUG
+main.c
+
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+We currently do not distinguish __CPROVER_r_ok and __CPROVER_w_ok at the
+implementation level. To make a meaningful distinction we would need to have
+predicates about lvalues vs rvalues.