Problems with showing the symbol table for some class files

[mgudemann]

For some class files, --show-symbol-table fails with identifier java::java.lang.Object not found

For example for the class file of the inner class Responses$Authenticate generated from: https://github.com/v-l-a-d/java-driver/blob/2.1/driver-core/src/main/java/com/datastax/driver/core/Responses.java

the whole result is:

CBMC version 5.4 64-bit x86_64 linux
Parsing com/datastax/driver/core/Responses$Authenticate.class
Java main class: com.datastax.driver.core.Responses$Authenticate
failed to load class `com.datastax.driver.core.Message'
failed to load class `com.datastax.driver.core.Responses'
failed to load class `com.datastax.driver.core.Message$Decoder'
failed to load class `com.datastax.driver.core.Responses$Authenticate$1'
failed to load class `java.lang.StringBuilder'
failed to load class `java.lang.String'
failed to load class `com.datastax.driver.core.Message$Response'
failed to load class `com.datastax.driver.core.Message$Response$Type'
Converting

Symbols:

Symbol......: __CPROVER_malloc_object
Pretty name.: 
Module......: 
Base name...: __CPROVER_malloc_object
Mode........: C
Type........: void *
Value.......: 
Flags.......: lvalue thread_local state_var
Location....: 

Symbol......: __CPROVER_rounding_mode
Pretty name.: 
Module......: 
Base name...: __CPROVER_rounding_mode
Mode........: C
Type........: signed int
Value.......: 
Flags.......: lvalue thread_local state_var
Location....: 

identifier java::java.lang.Object not found

[smowton]

Unable to reproduce for that class; may be fixed by unrelated progress in the meantime. I'd seen this before and the core problem was that some classes that never make any Object references could lead to java.lang.Object not getting introduced into the symtab, then the array classes would try to get its symbol regardless.

Suggest this can be closed for now unless we find another case where Object is used without being introduced first.

[smowton]

Aha, it happens when classes are derived from some non-Object opaque type. Addressed in smowton@d849b3e

[smowton]

Fixed in Cristina's test_gen branch

[peterschrammel]

Likely fixed.