Merge pull request #2260 from antlechner/antonia/annotation-class-value

Add support for Java annotations with Class value

Author: romainbrenguier

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -1514,6 +1514,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)
 {
@@ -1531,8 +1534,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