diff --git a/jbmc/regression/jbmc/lambda4/LambdaBasic$If.class b/jbmc/regression/jbmc/lambda4/LambdaBasic$If.class new file mode 100644 index 00000000000..6603c84e1d2 Binary files /dev/null and b/jbmc/regression/jbmc/lambda4/LambdaBasic$If.class differ diff --git a/jbmc/regression/jbmc/lambda4/LambdaBasic.class b/jbmc/regression/jbmc/lambda4/LambdaBasic.class new file mode 100644 index 00000000000..90eec9996e4 Binary files /dev/null and b/jbmc/regression/jbmc/lambda4/LambdaBasic.class differ diff --git a/jbmc/regression/jbmc/lambda4/LambdaBasic.java b/jbmc/regression/jbmc/lambda4/LambdaBasic.java new file mode 100644 index 00000000000..7a13d6873e7 --- /dev/null +++ b/jbmc/regression/jbmc/lambda4/LambdaBasic.java @@ -0,0 +1,37 @@ +public class LambdaBasic { + + private boolean endOnSuccess = true; + + public void testThis(int branch) { + boolean endOnSuccess; + endOnSuccess = this.endOnSuccess; + If boo = () -> { + if (endOnSuccess) { + return 1; + } + return 0; + }; + + int x0 = boo.xInt(); + // assert successful + if (branch == 1) { + if (endOnSuccess) { + assert x0 == 1; + } else { + assert x0 == 0; + } + // assert failed + } else { + if (endOnSuccess) { + assert x0 != 1; + } else { + assert x0 != 0; + } + } + } + + interface If { + + int xInt(); + } +} diff --git a/jbmc/regression/jbmc/lambda4/test.desc b/jbmc/regression/jbmc/lambda4/test.desc new file mode 100644 index 00000000000..f9050e5f3ee --- /dev/null +++ b/jbmc/regression/jbmc/lambda4/test.desc @@ -0,0 +1,13 @@ +CORE +LambdaBasic.class +--function LambdaBasic.testThis --property 'java::LambdaBasic.testThis:(I)V.assertion.1' --property 'java::LambdaBasic.testThis:(I)V.assertion.2' --property 'java::LambdaBasic.testThis:(I)V.assertion.3' --property 'java::LambdaBasic.testThis:(I)V.assertion.4' +line 19 assertion.*SUCCESS$ +line 21 assertion.*SUCCESS$ +line 26 assertion.*FAILURE$ +line 28 assertion.*FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +This test is a minimised example reported in TG-2479 and fixed during lambda +development.