Test for assignement of annotated field

This tests that the assignement is correctly analyzed by jbmc although
the left-hand-side and right-hand-side differ in annotated type.

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
+--
+--