Add invariant in java_generic_symbol_type

This also adapt unit tests that would make the invariant fail.

Author: romainbrenguier

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(),

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);