Add support for Java annotations with Class value

Java annotations can store element-value pairs, where each value is of
type String, Enum, Class, annotation, array or a primitive type.
The Class case was among the cases that did not have support in the java
bytecode parser before. For minimal support (without storing any
reference to java.lang.Class), we can just store the name of the type as
retrieved from the constant pool in a symbol_exprt.

Author: antlechner

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -1509,6 +1509,9 @@ void java_bytecode_parsert::relement_value_pairs(
   }
 }
 
+/// Corresponds to the element_value structure
+/// Described in Java 8 specification 4.7.16.1
+/// https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html#jvms-4.7.16.1
 void java_bytecode_parsert::relement_value_pair(
   annotationt::element_value_pairt &element_value_pair)
 {
@@ -1526,8 +1529,8 @@ void java_bytecode_parsert::relement_value_pair(
 
   case 'c':
     {
-      UNUSED u2 class_info_index=read_u2();
-      // todo: class
+      u2 class_info_index = read_u2();
+      element_value_pair.value = symbol_exprt(pool_entry(class_info_index).s);
     }
     break;
 

jbmc/unit/java_bytecode/java_bytecode_parser/AnnotationWithClassType.class

@@ -0,0 +1,3 @@
+public @interface AnnotationWithClassType {
+    Class<?> value();
+}

jbmc/unit/java_bytecode/java_bytecode_parser/AnnotationWithClassType.java

@@ -0,0 +1,3 @@
+@AnnotationWithClassType(java.lang.String.class)
+public class ClassWithClassTypeAnnotation {
+}

jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithClassTypeAnnotation.class

@@ -0,0 +1,3 @@
+@AnnotationWithClassType(byte.class)
+public class ClassWithPrimitiveTypeAnnotation {
+}

jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithClassTypeAnnotation.java

@@ -0,0 +1,3 @@
+@AnnotationWithClassType(void.class)
+public class ClassWithVoidTypeAnnotation {
+}

jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithPrimitiveTypeAnnotation.class

@@ -0,0 +1,3 @@
+java-testing-utils
+testing-utils
+java_bytecode