Merge pull request diffblue#2139 from romainbrenguier/bugfix/annotations-as-comments

[TG-3368] Make annotations comments in irep_idt

Author: romainbrenguier

regression/cbmc-java/annotations2/FieldAnnotation.class

@@ -0,0 +1,13 @@
+@interface FieldAnnotation {
+}
+
+public class Test {
+    @FieldAnnotation
+    public static double d;
+
+    public void check() {
+        double f = d;
+        assert(f == d);
+        assert(f != d);
+    }
+}

regression/cbmc-java/annotations2/Test.class

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.check
+^EXIT=10$
+^SIGNAL=0$
+assertion at file Test.java line 10 .* SUCCESS
+assertion at file Test.java line 11 .* FAILURE
+--
+--

regression/cbmc-java/annotations2/Test.java

@@ -71,14 +71,14 @@ class annotated_typet : public typet
   {
     // This cast should be safe as java_annotationt doesn't add data to irept
     return reinterpret_cast<const std::vector<java_annotationt> &>(
-      find(ID_annotations).get_sub());
+      find(ID_C_annotations).get_sub());
   }
 
   std::vector<java_annotationt> &get_annotations()
   {
     // This cast should be safe as java_annotationt doesn't add data to irept
     return reinterpret_cast<std::vector<java_annotationt> &>(
-      add(ID_annotations).get_sub());
+      add(ID_C_annotations).get_sub());
   }
 };
 

regression/cbmc-java/annotations2/test.desc

@@ -670,7 +670,7 @@ IREP_ID_TWO(overflow_shl, overflow-shl)
 IREP_ID_TWO(C_no_initialization_required, #no_initialization_required)
 IREP_ID_TWO(overlay_class, java::com.diffblue.OverlayClassImplementation)
 IREP_ID_TWO(overlay_method, java::com.diffblue.OverlayMethodImplementation)
-IREP_ID_ONE(annotations)
+IREP_ID_TWO(C_annotations, #annotations)
 
 // Projects depending on this code base that wish to extend the list of
 // available ids should provide a file local_irep_ids.h in their source tree and