Java class literals: init using a library hook when possible

The Java library definition of java.lang.Class, when nondet initialized, can be quite time
consuming due to the enumeration constant dictionary's internal array. Instead, let's give
the library a chance to set Class constants (literals like MyClass.class) itself.

While we're at it we might as well gain the ability to prove some properties of the literals.
We currently supply those class attributes that are easy to come by in the parse tree; with a
little more effort in the parser IsLocalClass and IsMemberClass could be determined.

Author: smowton

jbmc/regression/jbmc/class-literals/ExampleAnnotation.class

@@ -0,0 +1,4 @@
+
+public @interface ExampleAnnotation {
+
+}

jbmc/regression/jbmc/class-literals/ExampleAnnotation.java

@@ -0,0 +1,5 @@
+
+public enum ExampleEnum {
+
+}
+

jbmc/regression/jbmc/class-literals/ExampleEnum.class

@@ -0,0 +1,4 @@
+
+interface ExampleInterface {
+
+}

jbmc/regression/jbmc/class-literals/ExampleEnum.java

@@ -0,0 +1,4 @@
+; Compile me with Jasmin 2.1+ (https://sourceforge.net/projects/jasmin/)
+
+.class public synthetic ExampleSynthetic
+.super java/lang/Object

jbmc/regression/jbmc/class-literals/ExampleInterface.class

@@ -0,0 +1,35 @@
+
+public class Test {
+
+  public static void main() {
+
+    assert ExampleAnnotation.class.isAnnotation();
+    assert ExampleInterface.class.isInterface();
+    assert ExampleEnum.class.isEnum();
+    assert ExampleSynthetic.class.isSynthetic();
+
+    assert char[].class.isArray();
+    assert short[].class.isArray();
+    assert int[].class.isArray();
+    assert long[].class.isArray();
+    assert float[].class.isArray();
+    assert double[].class.isArray();
+    assert boolean[].class.isArray();
+    assert Object[].class.isArray();
+    assert Object[][].class.isArray();
+
+    // Note use of '==' not '.equals', as we expect the same exact literal,
+    // which in jbmc always have the same address.
+    // Note names of array classes are not tested yet, as arrays' types are
+    // printed as their raw signature, to be addressed separately.
+    // Note also primitive types (e.g. int.class) are not addresses here, as
+    // they are created through box types' static initializers (e.g. Integer
+    // has a static member TYPE that holds the Class for `int.class`)
+
+    assert ExampleAnnotation.class.getName() == "ExampleAnnotation";
+    assert ExampleInterface.class.getName() == "ExampleInterface";
+    assert ExampleEnum.class.getName() == "ExampleEnum";
+
+  }
+
+}