Class loader cannot handle Java class file names prefixed with ./

[peterschrammel]

The package name in "Java main class" seems to be derived from the file name passed to CBMC.
For similar reasons absolute paths cannot be handled.

cbmc ./com/datastax/driver/core/Authenticator.class --show-goto-functions
CBMC version 5.4 64-bit x86_64 linux
Parsing ./com/datastax/driver/core/Authenticator.class
Java main class: ..com.datastax.driver.core.Authenticator
failed to load class `java.lang.Object'
Converting
failed to add class symbol java::com.datastax.driver.core.Authenticator
CONVERSION ERROR

[kroening]

I have added a fix to allow ./ with c0e1999.
Let's not do absolute paths; the idea is that CBMC replicates what the Java class loader would do, and the Java class loader won't entertain ./ nor absolute paths. Use class paths for that.

[peterschrammel]

Ok. That makes perfect sense.
For Java, we should refuse to analyse filepaths that start with / or contain ./ (and ../) as they don't correspond to valid packages.