diffblue · romainbrenguier · Dec 31, 2016 · Feb 17, 2017 · Feb 24, 2017 · Feb 27, 2017
diff --git a/regression/strings/cprover-string-hack.h b/regression/strings/cprover-string-hack.h
@@ -1,6 +1,5 @@
-typedef struct __CPROVER_string { char *s; } __CPROVER_string;
-//typedef struct __CPROVER_char { char c; } __CPROVER_char;
-typedef unsigned char __CPROVER_char;
+typedef struct __attribute__((__packed__)) __CPROVER_refined_string_type { int length; char content[]; } __CPROVER_refined_string_type;
+typedef __CPROVER_refined_string_type __CPROVER_string;
 
 /******************************************************************************
  * CPROVER string functions
@@ -54,19 +53,19 @@ typedef unsigned char __CPROVER_char;
 /******************************************************************************
  * don't use these directly
  ******************************************************************************/
-extern __CPROVER_char __CPROVER_uninterpreted_string_char_at_func(__CPROVER_string str, int pos);
+extern char __CPROVER_uninterpreted_string_char_at_func(__CPROVER_string str, int pos);
 extern __CPROVER_bool __CPROVER_uninterpreted_string_equal_func(__CPROVER_string str1, __CPROVER_string str2);
 extern __CPROVER_string __CPROVER_uninterpreted_string_literal_func(char * str);
-extern __CPROVER_char __CPROVER_uninterpreted_char_literal_func();
+extern char __CPROVER_uninterpreted_char_literal_func();
 extern __CPROVER_string __CPROVER_uninterpreted_string_concat_func(__CPROVER_string str1, __CPROVER_string str2);
 extern int __CPROVER_uninterpreted_string_length_func(__CPROVER_string str);
 extern __CPROVER_string __CPROVER_uninterpreted_string_substring_func(__CPROVER_string str, int i, int j);
 extern __CPROVER_bool __CPROVER_uninterpreted_string_is_prefix_func(__CPROVER_string pref, __CPROVER_string str);
 extern __CPROVER_bool __CPROVER_uninterpreted_string_is_suffix_func(__CPROVER_string suff, __CPROVER_string str);
 extern __CPROVER_bool __CPROVER_uninterpreted_string_contains_func(__CPROVER_string str1, __CPROVER_string str2);
-extern int __CPROVER_uninterpreted_string_index_of_func(__CPROVER_string str, __CPROVER_char c);
-extern int __CPROVER_uninterpreted_string_last_index_of_func(__CPROVER_string str, __CPROVER_char c);
-extern __CPROVER_string __CPROVER_uninterpreted_string_char_set_func(__CPROVER_string str, int pos, __CPROVER_char c);
+extern int __CPROVER_uninterpreted_string_index_of_func(__CPROVER_string str, char c);
+extern int __CPROVER_uninterpreted_string_last_index_of_func(__CPROVER_string str, char c);
+extern __CPROVER_string __CPROVER_uninterpreted_string_char_set_func(__CPROVER_string str, int pos, char c);
 extern __CPROVER_string __CPROVER_uninterpreted_string_copy_func(__CPROVER_string str);
 extern int __CPROVER_uninterpreted_string_parse_int_func(__CPROVER_string str);
 extern __CPROVER_string __CPROVER_uninterpreted_string_of_int_func(int i);
diff --git a/regression/strings/fixed_bugs/Makefile b/regression/strings/fixed_bugs/Makefile
@@ -0,0 +1,9 @@
+
+test:
+	@../../test.pl -c ../../../../src/cbmc/cbmc
+
+testfuture:
+	@../../test.pl -c ../../../../src/cbmc/cbmc -CF
+
+testall:
+	@../../test.pl -c ../../../../src/cbmc/cbmc -CFTK
diff --git a/regression/strings/fixed_bugs/test-gen-095/test.class b/regression/strings/fixed_bugs/test-gen-095/test.class
diff --git a/regression/strings/fixed_bugs/test-gen-095/test.desc b/regression/strings/fixed_bugs/test-gen-095/test.desc
@@ -0,0 +1,7 @@
+KNOWNBUG
+test.class
+--string-refine
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
diff --git a/regression/strings/fixed_bugs/test-gen-095/test.java b/regression/strings/fixed_bugs/test-gen-095/test.java
@@ -0,0 +1,10 @@
+public class test
+{
+   public static void main(String[] args)
+   {
+      StringBuilder sb = new StringBuilder(args[0]);
+      sb.append("Z");
+      String s = sb.toString();
+      assert(s.equals("fg"));
+   }
+}
diff --git a/regression/strings/java_case/test.desc b/regression/strings/java_case/test.desc
diff --git a/regression/strings/java_case/test_case.class b/regression/strings/java_case/test_case.class
diff --git a/regression/strings/java_case/test_case.java b/regression/strings/java_case/test_case.java
diff --git a/regression/strings/java_char_array/test.desc b/regression/strings/java_char_array/test.desc
diff --git a/regression/strings/java_char_array/test_char_array.class b/regression/strings/java_char_array/test_char_array.class
diff --git a/regression/strings/java_char_array/test_char_array.java b/regression/strings/java_char_array/test_char_array.java
diff --git a/regression/strings/java_char_array_init/test.desc b/regression/strings/java_char_array_init/test.desc
diff --git a/regression/strings/java_char_array_init/test_init.class b/regression/strings/java_char_array_init/test_init.class
diff --git a/regression/strings/java_char_array_init/test_init.java b/regression/strings/java_char_array_init/test_init.java
diff --git a/regression/strings/java_char_at/test.desc b/regression/strings/java_char_at/test.desc
diff --git a/regression/strings/java_char_at/test_char_at.class b/regression/strings/java_char_at/test_char_at.class
diff --git a/regression/strings/java_char_at/test_char_at.java b/regression/strings/java_char_at/test_char_at.java
diff --git a/regression/strings/java_code_point/test.desc b/regression/strings/java_code_point/test.desc
diff --git a/regression/strings/java_code_point/test_code_point.class b/regression/strings/java_code_point/test_code_point.class
diff --git a/regression/strings/java_code_point/test_code_point.java b/regression/strings/java_code_point/test_code_point.java
diff --git a/regression/strings/java_compare/test.desc b/regression/strings/java_compare/test.desc
diff --git a/regression/strings/java_compare/test_compare.class b/regression/strings/java_compare/test_compare.class
diff --git a/regression/strings/java_compare/test_compare.java b/regression/strings/java_compare/test_compare.java
diff --git a/regression/strings/java_concat/test.desc b/regression/strings/java_concat/test.desc
diff --git a/regression/strings/java_concat/test_concat.class b/regression/strings/java_concat/test_concat.class
diff --git a/regression/strings/java_concat/test_concat.java b/regression/strings/java_concat/test_concat.java
diff --git a/regression/strings/java_contains/test.desc b/regression/strings/java_contains/test.desc
diff --git a/regression/strings/java_contains/test_contains.class b/regression/strings/java_contains/test_contains.class
diff --git a/regression/strings/java_contains/test_contains.java b/regression/strings/java_contains/test_contains.java
diff --git a/regression/strings/java_delete/test.desc b/regression/strings/java_delete/test.desc
diff --git a/regression/strings/java_delete/test_delete.class b/regression/strings/java_delete/test_delete.class
diff --git a/regression/strings/java_delete/test_delete.java b/regression/strings/java_delete/test_delete.java
diff --git a/regression/strings/java_easychair/easychair.java b/regression/strings/java_easychair/easychair.java
diff --git a/regression/strings/java_easychair/test.desc b/regression/strings/java_easychair/test.desc
diff --git a/regression/strings/java_empty/test.desc b/regression/strings/java_empty/test.desc
diff --git a/regression/strings/java_empty/test_empty.class b/regression/strings/java_empty/test_empty.class
diff --git a/regression/strings/java_empty/test_empty.java b/regression/strings/java_empty/test_empty.java
diff --git a/regression/strings/java_equal/test.desc b/regression/strings/java_equal/test.desc
diff --git a/regression/strings/java_equal/test_equal.java b/regression/strings/java_equal/test_equal.java
diff --git a/regression/strings/java_float/test.desc b/regression/strings/java_float/test.desc