From 0fd648233cf796f98b12e3831ee74e87b31629c3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Mon, 5 Mar 2018 17:51:30 +0100
Subject: [PATCH] Add regression test

---
 regression/cbmc-java/lambda2/SymStream.class    | Bin 0 -> 4475 bytes
 regression/cbmc-java/lambda2/readme.txt         |   1 +
 regression/cbmc-java/lambda2/test.desc          |   9 +++++++++
 regression/cbmc-java/lambda2/test_no_crash.desc |   8 ++++++++
 4 files changed, 18 insertions(+)
 create mode 100644 regression/cbmc-java/lambda2/SymStream.class
 create mode 100644 regression/cbmc-java/lambda2/readme.txt
 create mode 100644 regression/cbmc-java/lambda2/test.desc
 create mode 100644 regression/cbmc-java/lambda2/test_no_crash.desc

diff --git a/regression/cbmc-java/lambda2/SymStream.class b/regression/cbmc-java/lambda2/SymStream.class
new file mode 100644
index 0000000000000000000000000000000000000000..a473c854861974e71e7f172ee2c178a3927c14ae
GIT binary patch
literal 4475
zcmbtX`*Raj6#h1Cvu(PR+S2kA6ezZ-5Jb>QODUA{&=e{y6|jigblZk*c4M+ds`x-r
zP!z@Y`}G&#jFi`m<BT&p<M<~zj^EkcCfhXW*z!Z}J@@Xp=X~dRZ~prC&aVKr<EIE7
z#PKRr;e-q)Wq4M_Py`j;_9@wUPQ~d6=i?DP4_&BXp%T@o$4DIoovFqI%m`AjgtAqn
zh3f_3$_SMe$`NW(sIw6?;YC@VQ!y368WCM33~TU`3@@uVub?vPWDGrZXhcC>{EU89
zkD0nP7VCF1No%ZKLB#t$FqJk`ysDsFC<WRf%Q7<Erk>3jSp^+&J2Mu`PNmZ0wl!sE
zvpG7JFq4MmWMe6N#4uz1Qz?q3LJ^bQC?l0rW^6lkSWi)~nle(uMuswLJvft2(u~EE
zS%-X8{mC&)cP2Ar+*|N@ArOvbjZAx|C^pVHM#j=j1@!^z_u95;=oT5m9Z4(cbSfxo
zZW*NY-Lyi%(s<G`4o?cu0e#ryPF>ti=;olFNy^&aEO*9}G-TU?okPXdV}|2-N<y=&
zxg`KE7o6&Bkg1`0E{}j-k`v{{u9L#<DO^i(YCVCwo9{)QKoo0_=5j#H%C92));p6F
zbu*3#rp3NFn~O?@2-W5k)%(uO>k*udv%}2n^+VlL$i4^!GmhxV<z&N*VQx+4vr-(C
z=V}bbeTK;u=GeJ<Q;?V^O8OXU)GyJ&?OxusFFZ@6V6tv`D~OfOiK5zA-RvKpYUXUe
zqbDYM^|b3>_C^J#=fPj1$;@X$+8&wdNiJeyZ!HbE2={z==CCiymyv#ZGLta&C#A#G
z<U+Yc+O&qPctpc`Y|yX~%^F&;flbWq;BL<D$z=2?>6;p&Xw|R<F$G%}TK6hm({K=n
zG(3r?H0;4%4TteMyE7BbVXXCZui=c_BiW^4T&TqxoZhU(MGbG^Z55X^T*f;p-qmmg
z?`e1+S7}Keq=#=GdNk}tn}#mz)bO}aPYBg6)Cc%b!!ED~x0FO*=x+_z<oriyBhvh>
zc4YXBk#JOetYBwJStW8Qe_<)uT=H<S)K;*1rjFgncoia7Ebqbg2tL853N{6c*u%-}
zErd?)&+z&DwJ;lkd(|x@``iNxD)e;PoKmoE7WC0cE8!$<E4JS!ST)P@;hbd|@642*
zR?rq~jdKO~Mi%i5{WeE*w{4mXp)C)DuwzU9C|ElSqYom-Nr-B~JH`SCf|<iv#Nlj9
zqZvCjsGE~4!oFaX7(jU=EyTGzQuy|%U@w;|zJk}B%sWcv)_jSn;tLI5;u{s;YWNNp
z6|B$aPSQGSPZ+Vdo*Ev}S+4r1E-qwrt5f-viXZ6HxNT2NGHQPZE%gO>m3~mSMohll
zJkIt&j`|J>?94joKK2&%(Nh^zHCJ#jcK+9H-8B1?j=V6p{C}@X0Wj+B-6^z+9~Css
z@n$h+Fcs(L<3E8a{=lbyNP0J^khE`iW(Rj?wrePO*rhk~J3BY&8t$>>bKJ(&Fv>^)
z8>2U&M3ox|$xtRkdGszSPTWNJ22@#B{_IM6l;bLdIX0o38mp+KhO+A^b1na-Z08rv
zlZhR8j4MStv9B-2S@cyze?jOvi4a6!*xhUk9InV6W(W5Vcal3K+|gD7&BKYfyB&1K
zE>}XM$K^{9>Ea?$+>Q=kRuD*8A&{=3KzMf)15#E9WFLX_lmH?z5+J;#iU27u1ahz_
z5Z-RZfRq;ki4#a~2_TXr0)#g)y(Os-^oUvrq^}4NFSEKSgcq+bq>pnhM5+KPa|7&!
zXn=r@l>p>r>wcc_vM0>v#%9X)v>YJC=L5$=sFj6Kj~9We$g{&gJS&R=N$o)#BE(ZA
zAW8wTq7kQ8Js`i+JTZ4D`X?%s>vvJbf{DaiqtmFKh9>ip+o(}+2TOt5s14y3?z@e;
z5Pn1bG?tN};SW>`W5YBWWnMmw6*8~9g;mp7-75BZPK+W#T4&h}Gp7xf-545?WGYQC
zp-dcrg(FDgBr*XDhWOAr!gDp8`&f_)p603wq3}QGQgPHZsNXlp@Z+~)#-KGc=ziCr
zwbNJ^0MkfE0p|#2ieS!D{Hp|WA)t7Lt4<V0sCvLx%zhJgRURv)GVj9&#1(n_J(ZWJ
z@-kIkq2Q}jd2N<TQRJ!2+v=(;!yrF|@C+W}Tt})2uV7QxN_>Uy@ikV`p<eEd(%oYi
GNAf=ep><gR

literal 0
HcmV?d00001

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