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

romainbrenguier · web-flow · commit 8db6b2255e13 · 2018-05-04T11:50:48.000+01:00
[TG-3368] Make annotations comments in irep_idt
diff --git a/regression/cbmc-java/annotations2/FieldAnnotation.class b/regression/cbmc-java/annotations2/FieldAnnotation.class
diff --git a/regression/cbmc-java/annotations2/Test.class b/regression/cbmc-java/annotations2/Test.class
diff --git a/regression/cbmc-java/annotations2/Test.java b/regression/cbmc-java/annotations2/Test.java
@@ -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);
+    }
+}
diff --git a/regression/cbmc-java/annotations2/test.desc b/regression/cbmc-java/annotations2/test.desc
@@ -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
+--
+--
diff --git a/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h
@@ -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());
   }
 };
 
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
@@ -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

Original file line number	Diff line number	Diff line change
`@@ -71,14 +71,14 @@ class annotated_typet : public typet`
`71`	`71`	`{`
`72`	`72`	`// This cast should be safe as java_annotationt doesn't add data to irept`
`73`	`73`	`return reinterpret_cast<const std::vector<java_annotationt> &>(`
`74`		`- find(ID_annotations).get_sub());`
	`74`	`+ find(ID_C_annotations).get_sub());`
`75`	`75`	`}`
`76`	`76`
`77`	`77`	`std::vector<java_annotationt> &get_annotations()`
`78`	`78`	`{`
`79`	`79`	`// This cast should be safe as java_annotationt doesn't add data to irept`
`80`	`80`	`return reinterpret_cast<std::vector<java_annotationt> &>(`
`81`		`- add(ID_annotations).get_sub());`
	`81`	`+ add(ID_C_annotations).get_sub());`
`82`	`82`	`}`
`83`	`83`	`};`
`84`	`84`