Merge pull request #822 from allredj/test-gen-string-fix-170

Fixes in pre-processing for issue #170

Author: peterschrammel

regression/strings-smoke-tests/java_append_char/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_append_char.class
 --refine-strings
 ^EXIT=0$

regression/strings-smoke-tests/java_append_int/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_append_int.class
 --refine-strings
 ^EXIT=0$

regression/strings-smoke-tests/java_append_object/test.desc

@@ -5,3 +5,4 @@ test_append_object.class
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+Issue: diffblue/test-gen#82

regression/strings-smoke-tests/java_append_string/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_append_string.class
 --refine-strings
 ^EXIT=0$

regression/strings-smoke-tests/java_case/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_case.class
 --refine-strings
 ^EXIT=0$

regression/strings-smoke-tests/java_char_array/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_char_array.class
 --refine-strings
 ^EXIT=0$

regression/strings-smoke-tests/java_char_array_init/test.desc

@@ -5,3 +5,4 @@ test_init.class
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+cbmc/test-gen#259

regression/strings-smoke-tests/java_char_at/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_char_at.class
 --refine-strings
 ^EXIT=0$

regression/strings-smoke-tests/java_code_point/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_code_point.class
 --refine-strings
 ^EXIT=0$

regression/strings-smoke-tests/java_compare/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_compare.class
 --refine-strings
 ^EXIT=0$

regression/strings-smoke-tests/java_concat/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_concat.class
 --refine-strings
 ^EXIT=10$

regression/strings-smoke-tests/java_contains/test.desc

@@ -1,8 +1,9 @@
-FUTURE
+KNOWNBUG
 test_contains.class
 --refine-strings
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
 ^\[.*assertion.2\].* line 9.* FAILURE$
 --
+Issue: diffblue/test-gen#201

regression/strings-smoke-tests/java_delete/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_delete.class
 --refine-strings
 ^EXIT=0$

regression/strings-smoke-tests/java_delete_char_at/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_delete_char_at.class
 --refine-strings
 ^EXIT=0$

regression/strings-smoke-tests/java_empty/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_empty.class
 --refine-strings
 ^EXIT=0$

regression/strings-smoke-tests/java_endswith/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_endswith.class
 --refine-strings
 ^EXIT=10$

regression/strings-smoke-tests/java_equal/test.desc

@@ -1,6 +1,6 @@
-FUTURE
+CORE
 test_equal.class
---refine-strings
+--refine-strings --string-max-length 100 --string-max-length 100
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* FAILURE$

regression/strings-smoke-tests/java_float/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_float.class
 --refine-strings
 ^EXIT=0$

regression/strings-smoke-tests/java_hash_code/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_hash_code.class
 --refine-strings
 ^EXIT=10$

regression/strings-smoke-tests/java_index_of/test.desc

@@ -1,7 +1,8 @@
-FUTURE
+KNOWNBUG
 test_index_of.class
 --refine-strings
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+Issue: cbmc/test-gen#77

regression/strings-smoke-tests/java_index_of_char/test.desc

@@ -1,7 +1,8 @@
-FUTURE
+CORE
 test_index_of_char.class
 --refine-strings
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+Issue: cbmc/test-gen#77

regression/strings-smoke-tests/java_insert_char/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_insert_char.class
 --refine-strings
 ^EXIT=0$

regression/strings-smoke-tests/java_insert_char_array/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_insert_char_array.class
 --refine-strings
 ^EXIT=0$

regression/strings-smoke-tests/java_insert_int/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_insert_int.class
 --refine-strings
 ^EXIT=0$

regression/strings-smoke-tests/java_insert_multiple/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_insert_multiple.class
 --refine-strings
 ^EXIT=0$

regression/strings-smoke-tests/java_insert_string/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_insert_string.class
 --refine-strings
 ^EXIT=0$

regression/strings-smoke-tests/java_int_to_string/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_int.class
 --refine-strings
 ^EXIT=0$

regression/strings-smoke-tests/java_intern/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_intern.class
 --refine-strings
 ^EXIT=0$

regression/strings-smoke-tests/java_last_index_of/test.desc

@@ -1,7 +1,8 @@
-FUTURE
+KNOWNBUG
 test_last_index_of.class
 --refine-strings
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+Issue: diffblue/test-gen#77

regression/strings-smoke-tests/java_last_index_of_char/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_last_index_of_char.class
 --refine-strings
 ^EXIT=0$

regression/strings-smoke-tests/java_length/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_length.class
 --refine-strings
 ^EXIT=0$

regression/strings-smoke-tests/java_parseint/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_parseint.class
 --refine-strings
 ^EXIT=10$

regression/strings-smoke-tests/java_replace/test.desc

@@ -1,7 +1,8 @@
 FUTURE
 test_replace.class
---refine-strings
+--refine-strings --string-max-length 100
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+diffblue/test-gen#256

regression/strings-smoke-tests/java_replace_char/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_replace_char.class
 --refine-strings
 ^EXIT=0$

regression/strings-smoke-tests/java_set_char_at/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_set_char_at.class
 --refine-strings
 ^EXIT=0$

regression/strings-smoke-tests/java_set_length/test.desc

@@ -1,6 +1,6 @@
-FUTURE
+CORE
 test_set_length.class
---refine-strings
+--refine-strings --string-max-length 100
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$

regression/strings-smoke-tests/java_starts_with/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_starts_with.class
 --refine-strings
 ^EXIT=10$

regression/strings-smoke-tests/java_string_builder_length/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_sb_length.class
 --refine-strings
 ^EXIT=0$

regression/strings-smoke-tests/java_subsequence/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_subsequence.class
 --refine-strings
 ^EXIT=0$

regression/strings-smoke-tests/java_substring/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_substring.class
 --refine-strings
 ^EXIT=0$

regression/strings-smoke-tests/java_trim/test.desc

@@ -1,6 +1,6 @@
-FUTURE
+CORE
 test_trim.class
---refine-strings
+--refine-strings --string-max-length 100
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 6.* SUCCESS$

src/goto-programs/string_refine_preprocess.cpp

@@ -648,19 +648,15 @@ void string_refine_preprocesst::make_string_function(
   {
     if(signature.back()=='S')
     {
-      code_typet ft=function_type;
-      ft.return_type()=jls_ptr;
-      typecast_exprt lhs2(lhs, jls_ptr);
-
       make_string_assign(
         goto_program,
         target,
-        lhs2,
-        ft,
+        lhs,
+        function_type,
         function_name,
         arguments,
         location,
-         signature);
+        signature);
     }
     else
       make_normal_assign(
@@ -746,6 +742,7 @@ void string_refine_preprocesst::make_string_function(
 
   std::string new_sig=signature;
   exprt lhs;
+
   if(assign_first_arg)
   {
     assert(!function_call.arguments().empty());
@@ -759,9 +756,6 @@ void string_refine_preprocesst::make_string_function(
   else
     lhs=function_call.lhs();
 
-  if(lhs.id()==ID_typecast)
-    lhs=to_typecast_expr(lhs).op();
-
   new_type.return_type()=lhs.type();
 
   make_string_function(
@@ -1400,19 +1394,19 @@ void string_refine_preprocesst::initialize_string_function_table()
   signatures["java::java.lang.String.contains:(Ljava/lang/CharSequence;)Z"]=
     "SSZ";
   signatures["java::java.lang.StringBuilder.insert:(IZ)"
-             "Ljava/lang/StringBuilder;"]="SIZS";
+             "Ljava/lang/StringBuilder;"]="SIZ_";
   signatures["java::java.lang.StringBuilder.insert:(IJ)"
-             "Ljava/lang/StringBuilder;"]="SIJS";
+             "Ljava/lang/StringBuilder;"]="SIJ_";
   signatures["java::java.lang.StringBuilder.insert:(II)"
-             "Ljava/lang/StringBuilder;"]="SIIS";
+             "Ljava/lang/StringBuilder;"]="SII_";
   signatures["java::java.lang.StringBuilder.insert:(IC)"
-             "Ljava/lang/StringBuilder;"]="SICS";
+             "Ljava/lang/StringBuilder;"]="SIC_";
   signatures["java::java.lang.StringBuilder.insert:(ILjava/lang/String;)"
-             "Ljava/lang/StringBuilder;"]="SISS";
+             "Ljava/lang/StringBuilder;"]="SIS_";
   signatures["java::java.lang.StringBuilder.insert:(ILjava/lang/String;)"
-             "Ljava/lang/StringBuilder;"]="SISS";
+             "Ljava/lang/StringBuilder;"]="SIS_";
   signatures["java::java.lang.StringBuilder.insert:(I[C)"
-             "Ljava/lang/StringBuilder;"]="SI[S";
+             "Ljava/lang/StringBuilder;"]="SI[_";
   signatures["java::java.lang.String.intern:()Ljava/lang/String;"]="SV";
 }