Add tests for strchr

using the string-refinement solver.

Author: petr-bauch

regression/cbmc/string-refinement-strchr1/test.c

@@ -0,0 +1,15 @@
+#include <assert.h>
+#include <string.h>
+
+int main()
+{
+  char test[] = "foo";
+
+  char *first_o = strchr(test, 'o');
+  assert(*first_o == test[1]);
+  assert(*first_o == test[0]);
+  char *first_t = strchr(test, 't');
+  assert(*first_t == test[1]);
+  assert(*first_t == test[0]);
+  return 0;
+}

regression/cbmc/string-refinement-strchr1/test.desc

@@ -0,0 +1,12 @@
+CORE broken-smt-backend
+test.c
+--refine-strings --max-nondet-string-length 10
+^EXIT=10$
+^SIGNAL=0$
+^\[main.assertion.\d+\] line \d+ assertion \*first_o == test\[1\]: SUCCESS$
+^\[main.assertion.\d+\] line \d+ assertion \*first_o == test\[0\]: FAILURE$
+^\[main.assertion.\d+\] line \d+ assertion \*first_t == test\[1\]: FAILURE$
+^\[main.assertion.\d+\] line \d+ assertion \*first_t == test\[0\]: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc/string-refinement-strchr2/test.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+#include <string.h>
+
+int main()
+{
+  int i;
+  char *test = i ? "fo\0tis" : "notfoti";
+
+  char *first_o = strchr(test, 'o');
+  assert(first_o != NULL);
+  assert(*first_o == test[0]);
+  return 0;
+}

regression/cbmc/string-refinement-strchr2/test.desc

@@ -0,0 +1,10 @@
+CORE broken-smt-backend
+test.c
+--refine-strings
+^EXIT=10$
+^SIGNAL=0$
+^\[main.assertion.\d+\] line \d+ assertion first_o != (NULL|\(\(void \*\)0\)): SUCCESS$
+^\[main.assertion.\d+\] line \d+ assertion \*first_o == test\[0\]: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring