Merge pull request #1804 from mgudemann/feature/parse_bootstrapmethods_attribute

[TG-2365] Parse `BootstrapMethods` attribute

Author: Thomas Kiley

regression/cbmc-java/lambda1/B.class

@@ -0,0 +1,9 @@
+public class B {
+    public int y;
+
+    public static java.util.function.Function<Double, Double> dmul = x -> x * 3.1415;
+
+    public void set(int x) {
+        y = x;
+    }
+}

regression/cbmc-java/lambda1/B.java

@@ -0,0 +1,4 @@
+@FunctionalInterface
+interface CustomLambda<T> {
+    boolean is_ok(T t);
+}

regression/cbmc-java/lambda1/C.class

@@ -0,0 +1,84 @@
+import java.util.function.*;
+
+public class Lambdatest {
+
+    class A {
+        int x;
+    }
+
+    CustomLambda<Integer> custom = x -> true;
+    BiFunction<Float, Integer, Integer> add = (x0, y0) -> x0.intValue() + y0;
+    int z = 10;
+
+    A a;
+    B b = new B();
+
+    public Integer g(Float x, Integer y, BiFunction<Float, Integer, Integer> fun) {
+        return fun.apply(x, y);
+    }
+
+    public int f(Float x, Integer y, Integer z) {
+        Integer tmp = add.apply(x, y);
+        Function<Integer, Integer> mul = (a) -> a * tmp;
+        return mul.apply(z);
+    }
+
+    public int i(int x) {
+        int z = 5;
+        Function<Integer, Integer> foo = (a) -> a * z;
+        return foo.apply(x);
+    }
+
+    public int j(int x) {
+        Function<Integer, Integer> foo = (a) -> a * z;
+        return foo.apply(x);
+    }
+
+    public int k(int x) {
+        a.x = 10;
+        
+        Function<Integer, Integer> foo = (y) -> y * a.x;
+        return foo.apply(x);
+    }
+    
+    public int l(int x) {
+        b.y = 10;
+        Function<Integer, Integer> foo = (y) -> {
+            int r = y * b.y;
+            b.set(r);
+            return r;
+        };
+        b = new B();
+        b.y = 14;
+        return foo.apply(x);
+    }
+
+    public int m(int x) {
+        b.y = 10;
+        Function<Integer, Integer> foo = (y) -> {
+            int r = y * b.y;
+            b.y = r;
+            return r;
+        };
+        return foo.apply(x);
+    }
+
+    // test static field of different class
+    public double d(Double x) {
+        return B.dmul.apply(x);
+    }
+
+    public int capture2(Float a) {
+        return add.apply(a, 1);
+    }
+
+    public boolean custom(Integer i) {
+        return custom.is_ok(i);
+    }
+}
+
+class C implements CustomLambda<Integer> {
+    public boolean is_ok(Integer i) {
+        return true;
+    }
+}

regression/cbmc-java/lambda1/CustomLambda.class

@@ -0,0 +1,12 @@
+CORE
+Lambdatest.class
+--verbosity 10 --show-goto-functions
+lambda function reference lambda\$new\$0 in class \"Lambdatest\"
+lambda function reference lambda\$new\$1 in class \"Lambdatest\"
+lambda function reference lambda\$f\$2 in class \"Lambdatest\"
+lambda function reference lambda\$i\$3 in class \"Lambdatest\"
+lambda function reference lambda\$j\$4 in class \"Lambdatest\"
+lambda function reference lambda\$k\$5 in class \"Lambdatest\"
+lambda function reference lambda\$l\$6 in class \"Lambdatest\"
+lambda function reference lambda\$m\$7 in class \"Lambdatest\"
+lambda function reference lambda\$static\$0 in class \"B\"

regression/cbmc-java/lambda1/CustomLambda.java

@@ -33,6 +33,9 @@ void java_bytecode_parse_treet::classt::swap(
   other.fields.swap(fields);
   other.methods.swap(methods);
   other.annotations.swap(annotations);
+  std::swap(
+    other.attribute_bootstrapmethods_read, attribute_bootstrapmethods_read);
+  std::swap(other.lambda_method_handle_map, lambda_method_handle_map);
 }
 
 void java_bytecode_parse_treet::output(std::ostream &out) const