Merge pull request diffblue#5663 from tautschnig/string-abstraction

String abstraction fixes

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

@@ -1,7 +1,7 @@
 CORE
 test.c
 --string-abstraction --show-goto-functions
-strlen#return_value = \(.*\)s#strarg->length - POINTER_OFFSET\(s\);
+strlen#return_value = \(.*\)s#str->length - POINTER_OFFSET\(s\)\)*;
 ^EXIT=0$
 ^SIGNAL=0$
 --

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

@@ -1,5 +1,6 @@
 #include <assert.h>
 #include <stdlib.h>
+#include <string.h>
 
 int main()
 {

regression/cbmc-with-incr/Malloc13/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 --string-abstraction
 ^EXIT=0$

regression/cbmc/Malloc13/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 --string-abstraction
 ^EXIT=0$

regression/cbmc/String_Abstraction1/main.c

@@ -0,0 +1,17 @@
+#include <string.h>
+
+int main()
+{
+  char a[100], b[100], *p;
+
+  strcpy(a, "asd");
+  assert(strlen(a) == 3);
+
+  a[2] = 0;
+  assert(strlen(a) == 2);
+
+  p = strcpy(b, a);
+  assert(p == b);
+  assert(strlen(b) == 2);
+  assert(strlen(p) == 2);
+}

regression/cbmc-from-CVS/String_Abstraction10/main.c → regression/cbmc/String_Abstraction10/main.c

@@ -1,6 +1,6 @@
 #include <string.h>
 
-char a [10][100];
+char a[10][100];
 
 struct S
 {
@@ -11,11 +11,11 @@ struct S
 int main()
 {
   strcpy(a[0], "asd");
-  assert(strlen(a[0])==3);
+  assert(strlen(a[0]) == 3);
 
   strcpy(s.x, "asdasd");
-  assert(strlen(s.x)==6);
+  assert(strlen(s.x) == 6);
 
-  s.p=s.x;
-  assert(strlen(s.p)==6);
+  s.p = s.x;
+  assert(strlen(s.p) == 6);
 }

regression/cbmc-from-CVS/String_Abstraction9/test.desc → regression/cbmc/String_Abstraction10/test.desc

@@ -1,8 +1,10 @@
-CORE
+KNOWNBUG
 main.c
 --string-abstraction --pointer-check --bounds-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+Multi-dimensional arrays are not yet handled properly.

regression/cbmc/String_Abstraction11/anon-retval.c

@@ -0,0 +1,16 @@
+void *malloc(unsigned);
+
+char *foo()
+{
+  char *a;
+  a = malloc(2);
+  a[1] = 0;
+  __CPROVER_is_zero_string(a) = 1;
+  return a;
+}
+
+int main()
+{
+  __CPROVER_assert(
+    __CPROVER_is_zero_string(foo()), "CBMC failed to track return value");
+}

regression/cbmc/String_Abstraction12/char-array.c

@@ -0,0 +1,12 @@
+int main(int argc, char *argv[])
+{
+  char dest[10];
+
+  __CPROVER_assert(
+    __CPROVER_buffer_size(dest) == 10, "CBMC failed to track char array size");
+  dest[9] = '\0';
+  __CPROVER_assert(
+    __CPROVER_is_zero_string(dest), "CBMC failed to track char array (2)");
+
+  return 0;
+}

regression/cbmc-from-CVS/String_Abstraction13/constant.c → regression/cbmc/String_Abstraction13/constant.c

@@ -1,12 +1,13 @@
 
-int main() {
-  char * x;
-  char * y;
-  char * z;
-  x = (void*) 0;
+int main()
+{
+  char *x;
+  char *y;
+  char *z;
+  x = (void *)0;
   __CPROVER_assume(__CPROVER_is_zero_string(x));
   y = "bla";
-  z = (char*) 0;
+  z = (char *)0;
   __CPROVER_assume(__CPROVER_is_zero_string(z));
   assert(__CPROVER_is_zero_string(x));
   assert(__CPROVER_is_zero_string(y));

regression/cbmc-from-CVS/String_Abstraction14/pass-in-implicit.c → regression/cbmc/String_Abstraction14/pass-in-implicit.c

@@ -1,12 +1,14 @@
-void * malloc(unsigned);
+void *malloc(unsigned);
 
-void use_str(char * s) {
+void use_str(char *s)
+{
   assert(__CPROVER_is_zero_string(s));
 }
 
-int main(int argc, char* argv[]) {
+int main(int argc, char *argv[])
+{
   unsigned short len;
-  char * str;
+  char *str;
   __CPROVER_assume(len > 0);
   str = malloc(len);
   __CPROVER_assume(__CPROVER_buffer_size(str) == len);

regression/cbmc-from-CVS/String_Abstraction15/pass-in.c → regression/cbmc/String_Abstraction15/pass-in.c

@@ -1,12 +1,14 @@
-void * malloc(unsigned);
+void *malloc(unsigned);
 
-void use_str(char * s) {
+void use_str(char *s)
+{
   assert(__CPROVER_is_zero_string(s));
 }
 
-int main(int argc, char* argv[]) {
+int main(int argc, char *argv[])
+{
   unsigned short len;
-  char * str;
+  char *str;
   __CPROVER_assume(len > 0);
   str = malloc(len);
   __CPROVER_assume(__CPROVER_buffer_size(str) == len);

regression/cbmc/String_Abstraction16/ptr-arith.c

@@ -0,0 +1,16 @@
+#include <string.h>
+
+void *malloc(__CPROVER_size_t);
+
+int main(int argc, char *argv[])
+{
+  char *name;
+
+  name = malloc(10);
+  __CPROVER_assume(__CPROVER_buffer_size(name) == 20);
+  name = strcpy(name, "abcdefghi");
+  name = strcpy(name + 5 - 1, "xxxxx");
+  assert(__CPROVER_is_zero_string(name));
+
+  return 0;
+}

regression/cbmc-from-CVS/String_Abstraction17/strcpy-no-decl.c → regression/cbmc/String_Abstraction17/strcpy-no-decl.c

@@ -1,8 +1,9 @@
-void * malloc(unsigned);
+void *malloc(unsigned);
 
-char * make_str() {
+char *make_str()
+{
   unsigned short len;
-  char * str;
+  char *str;
 
   __CPROVER_assume(len > 0);
   str = malloc(len);
@@ -14,9 +15,10 @@ char * make_str() {
   return str;
 }
 
-int main(int argc, char* argv[]) {
+int main(int argc, char *argv[])
+{
   char dest[10];
-  char * name;
+  char *name;
 
   name = make_str();
   __CPROVER_assume(strlen(name) < 10);

regression/cbmc/String_Abstraction17/test.desc

@@ -0,0 +1,11 @@
+CORE
+strcpy-no-decl.c
+--string-abstraction --validate-goto-model
+Condition: strlen type inconsistency
+^EXIT=(127|134)$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+While this test currently passes when omitting --validate-goto-model, we should
+expect a report of type inconsistencies as no forward declarations are present.

regression/cbmc-from-CVS/String_Abstraction18/strcpy.c → regression/cbmc/String_Abstraction18/strcpy.c

@@ -1,10 +1,11 @@
 #include <string.h>
 
-void * malloc(unsigned);
+void *malloc(__CPROVER_size_t);
 
-char * make_str() {
+char *make_str()
+{
   unsigned short len;
-  char * str;
+  char *str;
 
   __CPROVER_assume(len > 0);
   str = malloc(len);
@@ -16,9 +17,10 @@ char * make_str() {
   return str;
 }
 
-int main(int argc, char* argv[]) {
+int main(int argc, char *argv[])
+{
   char dest[10];
-  char * name;
+  char *name;
 
   name = make_str();
   // assert(strlen(name) < 10);

regression/cbmc/String_Abstraction19/structs.c

@@ -0,0 +1,24 @@
+void *malloc(unsigned);
+
+typedef struct str_struct
+{
+  int a;
+  char *str;
+  char *str2;
+} str_struct_t;
+
+str_struct_t *foo()
+{
+  str_struct_t retval;
+  retval.str = malloc(2);
+  __CPROVER_is_zero_string(retval.str) = 1;
+  return &retval;
+}
+
+int main()
+{
+  str_struct_t *a;
+  a = foo();
+  __CPROVER_assert(
+    __CPROVER_is_zero_string(a->str), "CBMC failed to track struct");
+}