Conversion Error with PKCS11Test.java from openjdk regression suite

[jgwilson42]

Observed Behaviour

Here is the output from CBMC:

CBMC version 5.7 64-bit x86_64 linux
Parsing PKCS11Test.class
Java main class: PKCS11Test
failed to load class `java.util.HashMap'
failed to load class `java.lang.reflect.Array'
failed to load class `java.io.IOException'
failed to load class `java.io.StringReader'
failed to load class `java.io.ByteArrayOutputStream'
failed to load class `java.lang.StringBuffer'
failed to load class `java.util.Iterator'
failed to load class `java.security.spec.ECGenParameterSpec'
failed to load class `java.security.AlgorithmParameters'
failed to load class `java.security.InvalidAlgorithmParameterException'
failed to load class `java.lang.Throwable'
failed to load class `java.security.ProviderException'
failed to load class `java.security.KeyPair'
failed to load class `java.security.spec.AlgorithmParameterSpec'
failed to load class `java.security.KeyPairGenerator'
failed to load class `java.security.spec.ECParameterSpec'
failed to load class `java.lang.RuntimeException'
failed to load class `java.util.Vector'
failed to load class `java.lang.NumberFormatException'
failed to load class `java.lang.Double'
failed to load class `java.io.FileInputStream'
failed to load class `java.lang.CharSequence'
failed to load class `java.lang.UnsatisfiedLinkError'
failed to load class `java.util.Map'
failed to load class `java.util.Properties'
failed to load class `java.lang.Exception'
failed to load class `java.io.File'
failed to load class `java.security.Security'
failed to load class `java.lang.StringBuilder'
failed to load class `java.io.PrintStream'
failed to load class `java.lang.System'
failed to load class `java.security.Provider'
failed to load class `java.lang.reflect.Constructor'
failed to load class `java.lang.Enum'
failed to load class `java.lang.Class'
failed to load class `java.lang.String'
failed to load class `java.lang.Object'
Converting
main method in `PKCS11Test' is ambiguous
CONVERSION ERROR

For the file http://hg.openjdk.java.net/jdk8/jdk8/jdk/file/687fd7c7986d/test/sun/security/pkcs11/PKCS11Test.java

Expected Behaviour

We should not get a CONVERSION ERROR as java will not error (other than missing main).

Version

cbmc compiled from commit a7663cb.

Steps to reproduce

./cbmc PKCS11Test.class