Bugfix: Java symbol types must have mode ID_java

peterschrammel · peterschrammel · commit befc2252ed89 · 2018-03-18T15:27:57.000Z
diff --git a/src/java_bytecode/java_bytecode_typecheck_type.cpp b/src/java_bytecode/java_bytecode_typecheck_type.cpp
@@ -20,12 +20,14 @@ void java_bytecode_typecheckt::typecheck_type(typet &type)
   {
     irep_idt identifier=to_symbol_type(type).get_identifier();
 
-    const auto type_symbol = symbol_table.lookup(identifier);
+    auto type_symbol = symbol_table.get_writeable(identifier);
     DATA_INVARIANT(
       type_symbol, "symbol " + id2string(identifier) + " must exist already");
     DATA_INVARIANT(
       type_symbol->is_type,
       "symbol " + id2string(identifier) + " must be a type");
+
+    type_symbol->mode = ID_java;
   }
   else if(type.id()==ID_pointer)
   {

Original file line number	Diff line number	Diff line change
`@@ -20,12 +20,14 @@ void java_bytecode_typecheckt::typecheck_type(typet &type)`
`20`	`20`	`{`
`21`	`21`	`irep_idt identifier=to_symbol_type(type).get_identifier();`
`22`	`22`
`23`		`- const auto type_symbol = symbol_table.lookup(identifier);`
	`23`	`+ auto type_symbol = symbol_table.get_writeable(identifier);`
`24`	`24`	`DATA_INVARIANT(`
`25`	`25`	`type_symbol, "symbol " + id2string(identifier) + " must exist already");`
`26`	`26`	`DATA_INVARIANT(`
`27`	`27`	`type_symbol->is_type,`
`28`	`28`	`"symbol " + id2string(identifier) + " must be a type");`
	`29`	`+`
	`30`	`+ type_symbol->mode = ID_java;`
`29`	`31`	`}`
`30`	`32`	`else if(type.id()==ID_pointer)`
`31`	`33`	`{`