Add invariant in java_generic_symbol_type

romainbrenguier · romainbrenguier · commit 53bc89259ada · 2018-05-03T10:59:41.000+01:00
This also adapt unit tests that would make the invariant fail.
diff --git a/src/java_bytecode/java_types.cpp b/src/java_bytecode/java_types.cpp
@@ -854,7 +854,12 @@ java_generic_symbol_typet::java_generic_symbol_typet(
   set(ID_C_java_generic_symbol, true);
   const typet &base_type = java_type_from_string(base_ref, class_name_prefix);
   PRECONDITION(is_java_generic_type(base_type));
-  const java_generic_typet gen_base_type = to_java_generic_type(base_type);
+  const java_generic_typet &gen_base_type = to_java_generic_type(base_type);
+  INVARIANT(
+    type.get_identifier() == to_symbol_type(gen_base_type.subtype()).get_identifier(),
+    "identifier of "+type.pretty()+"\n and identifier of type "+
+    gen_base_type.subtype().pretty()+"\ncreated by java_type_from_string for "+
+    base_ref+" should be equal");
   generic_types().insert(
     generic_types().end(),
     gen_base_type.generic_type_arguments().begin(),
diff --git a/unit/java_bytecode/java_types/java_generic_symbol_type.cpp b/unit/java_bytecode/java_types/java_generic_symbol_type.cpp
@@ -11,13 +11,13 @@
 
 SCENARIO("java_generic_symbol_type", "[core][java_types]")
 {
-  WHEN("MyType is LGenericClass<TX;TY;>;")
+  GIVEN("LGenericClass<TX;TY;>;")
   {
-    auto symbol_type = symbol_typet("MyType");
+    auto symbol_type = symbol_typet("java::GenericClass");
     const auto generic_symbol_type = java_generic_symbol_typet(
       symbol_type, "LGenericClass<TX;TY;>;", "PrefixClassName");
 
-    REQUIRE(generic_symbol_type.get_identifier() == "MyType");
+    REQUIRE(generic_symbol_type.get_identifier() == "java::GenericClass");
 
     auto types = generic_symbol_type.generic_types();
     REQUIRE(types.size() == 2);

Original file line number	Diff line number	Diff line change
`@@ -11,13 +11,13 @@`
`11`	`11`
`12`	`12`	`SCENARIO("java_generic_symbol_type", "[core][java_types]")`
`13`	`13`	`{`
`14`		`- WHEN("MyType is LGenericClass<TX;TY;>;")`
	`14`	`+ GIVEN("LGenericClass<TX;TY;>;")`
`15`	`15`	`{`
`16`		`- auto symbol_type = symbol_typet("MyType");`
	`16`	`+ auto symbol_type = symbol_typet("java::GenericClass");`
`17`	`17`	`const auto generic_symbol_type = java_generic_symbol_typet(`
`18`	`18`	`symbol_type, "LGenericClass<TX;TY;>;", "PrefixClassName");`
`19`	`19`
`20`		`- REQUIRE(generic_symbol_type.get_identifier() == "MyType");`
	`20`	`+ REQUIRE(generic_symbol_type.get_identifier() == "java::GenericClass");`
`21`	`21`
`22`	`22`	`auto types = generic_symbol_type.generic_types();`
`23`	`23`	`REQUIRE(types.size() == 2);`