Open
Description
Running timeout 300 cbmc left-square.class for the attached file gave the following output:
CBMC version 5.7 64-bit x86_64 linux
Parsing left-square.class
Java main class: left-square
cbmc: ../util/std_types.h:152: symbol_typet& to_symbol_type(typet&): Assertion `type.id()==ID_symbol' failed.
timeout: the monitored command dumped core
When this class is run in java the following output is given:
Error: A JNI error has occurred, please check your installation and try again
Exception in thread "main" java.lang.ClassFormatError: Bad class name in class file [
at java.lang.ClassLoader.defineClass1(Native Method)
at java.lang.ClassLoader.defineClass(ClassLoader.java:763)
at java.security.SecureClassLoader.defineClass(SecureClassLoader.java:142)
at java.net.URLClassLoader.defineClass(URLClassLoader.java:467)
at java.net.URLClassLoader.access$100(URLClassLoader.java:73)
at java.net.URLClassLoader$1.run(URLClassLoader.java:368)
at java.net.URLClassLoader$1.run(URLClassLoader.java:362)
at java.security.AccessController.doPrivileged(Native Method)
at java.net.URLClassLoader.findClass(URLClassLoader.java:361)
at java.lang.ClassLoader.loadClass(ClassLoader.java:424)
at sun.misc.Launcher$AppClassLoader.loadClass(Launcher.java:331)
at java.lang.ClassLoader.loadClass(ClassLoader.java:357)
at sun.launcher.LauncherHelper.checkAndLoadMain(LauncherHelper.java:495)
Based on this I expect a conversion error as the source file [.java is not valid.