Add test verifying that the string abstraction is enabled

This checks the body of goto functions whose implementation depends
on whether the string abstraction macro is defined.

Author: Thomas Kiley

regression/cbmc-library/string-abstraction/test-c-with-string-abstraction.desc

@@ -0,0 +1,10 @@
+CORE
+test.c
+--string-abstraction --show-goto-functions
+strlen#return_value = \(.*\)s#strarg->length - POINTER_OFFSET\(s\);
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Ensure that the --string-abstraction flag enables the string abstraction
+version of string functions

regression/cbmc-library/string-abstraction/test-c-without-string-abstraction.desc

@@ -0,0 +1,10 @@
+CORE
+test.c
+--show-goto-functions
+IF !\(\(signed int\)s\[\(.*\)len\] != 0\) THEN GOTO 2
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Ensure that if the string abstraction flag is not provided, the regular model for
+string functions is used (in this case searching for the terminator).

regression/cbmc-library/string-abstraction/test.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main()
+{
+  char *x = malloc(sizeof(char) * 10);
+  x[8] = '\0';
+  assert(strlen(x) == 8);
+}