diff --git a/regression/cbmc-java/lambda2/SymStream.class b/regression/cbmc-java/lambda2/SymStream.class new file mode 100644 index 00000000000..a473c854861 Binary files /dev/null and b/regression/cbmc-java/lambda2/SymStream.class differ diff --git a/regression/cbmc-java/lambda2/readme.txt b/regression/cbmc-java/lambda2/readme.txt new file mode 100644 index 00000000000..38647bdebb1 --- /dev/null +++ b/regression/cbmc-java/lambda2/readme.txt @@ -0,0 +1 @@ +from https://github.com/symphonyoss/symphony-java-client/ diff --git a/regression/cbmc-java/lambda2/test.desc b/regression/cbmc-java/lambda2/test.desc new file mode 100644 index 00000000000..2127f00ead7 --- /dev/null +++ b/regression/cbmc-java/lambda2/test.desc @@ -0,0 +1,9 @@ +KNOWNBUG +SymStream.class +--verbosity 10 --show-goto-functions +lambda function reference org/symphonyoss/symphony/clients/model/SymUser\.toSymUser in class \"SymStream\" +^EXIT=0 +^SIGNAL=0 +-- +-- +lambda functions without "lambda$" prefix aren't recognized currently TG-2691 diff --git a/regression/cbmc-java/lambda2/test_no_crash.desc b/regression/cbmc-java/lambda2/test_no_crash.desc new file mode 100644 index 00000000000..933732babea --- /dev/null +++ b/regression/cbmc-java/lambda2/test_no_crash.desc @@ -0,0 +1,8 @@ +CORE +SymStream.class +--verbosity 10 --show-goto-functions +^EXIT=0 +^SIGNAL=0 +-- +-- +just to test that it doesn't crash in this situation, cf. TG-2684