Merge pull request #1410 from LAJW/fix-test-gen

Joel Allred · web-flow · commit b4f57ee70653 · 2017-09-20T17:48:36.000+01:00
TG-634 (Rollback) Remove invariant causing failure in unit test generation involving CharSequences
diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp
@@ -882,13 +882,6 @@ void java_object_factoryt::gen_nondet_struct_init(
               binary_relation_exprt(me, ID_le, max_length)));
           }
         }
-        else
-        {
-          INVARIANT(
-            class_identifier!="java.lang.CharSequence" &&
-              class_identifier!="java.lang.AbstractStringBuilder",
-            "Trying to initialize abstract class");
-        }
       }
     }
   }

Original file line number	Diff line number	Diff line change
`@@ -882,13 +882,6 @@ void java_object_factoryt::gen_nondet_struct_init(`
`882`	`882`	`binary_relation_exprt(me, ID_le, max_length)));`
`883`	`883`	`}`
`884`	`884`	`}`
`885`		`- else`
`886`		`- {`
`887`		`- INVARIANT(`
`888`		`- class_identifier!="java.lang.CharSequence" &&`
`889`		`- class_identifier!="java.lang.AbstractStringBuilder",`
`890`		`- "Trying to initialize abstract class");`
`891`		`- }`
`892`	`885`	`}`
`893`	`886`	`}`
`894`	`887`	`}`