From fb89e5aa3bf29b6dd8d408494dd60f9e71c3161b Mon Sep 17 00:00:00 2001 From: Cristina Date: Mon, 22 May 2017 20:51:54 +0100 Subject: [PATCH] Regression test for ArithmeticException --- .../ArithmeticExceptionTest.class | Bin 0 -> 818 bytes .../ArithmeticExceptionTest.java | 11 +++++++++++ .../cbmc-java/ArithmeticException1/test.desc | 9 +++++++++ .../ArithmeticExceptionTest.class | Bin 0 -> 646 bytes .../ArithmeticExceptionTest.java | 12 ++++++++++++ .../cbmc-java/ArithmeticException2/test.desc | 9 +++++++++ .../ArithmeticExceptionTest.class | Bin 0 -> 629 bytes .../ArithmeticExceptionTest.java | 11 +++++++++++ .../cbmc-java/ArithmeticException3/test.desc | 9 +++++++++ .../ArithmeticExceptionTest.class | Bin 0 -> 646 bytes .../ArithmeticExceptionTest.java | 12 ++++++++++++ .../cbmc-java/ArithmeticException4/test.desc | 9 +++++++++ .../ArithmeticExceptionTest.class | Bin 0 -> 639 bytes .../ArithmeticExceptionTest.java | 11 +++++++++++ .../cbmc-java/ArithmeticException5/test.desc | 8 ++++++++ .../ArithmeticExceptionTest.class | Bin 0 -> 605 bytes .../ArithmeticExceptionTest.java | 10 ++++++++++ .../cbmc-java/ArithmeticException6/test.desc | 9 +++++++++ 18 files changed, 120 insertions(+) create mode 100644 regression/cbmc-java/ArithmeticException1/ArithmeticExceptionTest.class create mode 100644 regression/cbmc-java/ArithmeticException1/ArithmeticExceptionTest.java create mode 100644 regression/cbmc-java/ArithmeticException1/test.desc create mode 100644 regression/cbmc-java/ArithmeticException2/ArithmeticExceptionTest.class create mode 100644 regression/cbmc-java/ArithmeticException2/ArithmeticExceptionTest.java create mode 100644 regression/cbmc-java/ArithmeticException2/test.desc create mode 100644 regression/cbmc-java/ArithmeticException3/ArithmeticExceptionTest.class create mode 100644 regression/cbmc-java/ArithmeticException3/ArithmeticExceptionTest.java create mode 100644 regression/cbmc-java/ArithmeticException3/test.desc create mode 100644 regression/cbmc-java/ArithmeticException4/ArithmeticExceptionTest.class create mode 100644 regression/cbmc-java/ArithmeticException4/ArithmeticExceptionTest.java create mode 100644 regression/cbmc-java/ArithmeticException4/test.desc create mode 100644 regression/cbmc-java/ArithmeticException5/ArithmeticExceptionTest.class create mode 100644 regression/cbmc-java/ArithmeticException5/ArithmeticExceptionTest.java create mode 100644 regression/cbmc-java/ArithmeticException5/test.desc create mode 100644 regression/cbmc-java/ArithmeticException6/ArithmeticExceptionTest.class create mode 100644 regression/cbmc-java/ArithmeticException6/ArithmeticExceptionTest.java create mode 100644 regression/cbmc-java/ArithmeticException6/test.desc diff --git a/regression/cbmc-java/ArithmeticException1/ArithmeticExceptionTest.class b/regression/cbmc-java/ArithmeticException1/ArithmeticExceptionTest.class new file mode 100644 index 0000000000000000000000000000000000000000..3ad4e6ebe86e52587843990ffa9af01256fb2197 GIT binary patch literal 818 zcmZuvPfrs;6#u>Mw%cwCmR6w@5Kz#fwp0nF!GSUnVYczHeWE_8W~icmvy)g8 z^|!^441aIfUY`eqsGHerGtcfqreI zpT!CCQt~sYvVk|wcj7&}c@4Va zLk82l=F%kF@mZh@Kp8W<7f?Z!GeZ8%XovT@(<=K5;qyy=2VdY^p!fss;We_qu2QbY z#)1^(I%|VpV1^aFv?Pzq$zz@|;(ybE~lC0yq#od5e0jVv;ym(u+b2N^v43vqX+?f?J) literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/ArithmeticException1/ArithmeticExceptionTest.java b/regression/cbmc-java/ArithmeticException1/ArithmeticExceptionTest.java new file mode 100644 index 00000000000..7988e85700e --- /dev/null +++ b/regression/cbmc-java/ArithmeticException1/ArithmeticExceptionTest.java @@ -0,0 +1,11 @@ +public class ArithmeticExceptionTest { + public static void main(String args[]) { + try { + int i=0; + int j=10/i; + } + catch(ArithmeticException exc) { + assert false; + } + } +} diff --git a/regression/cbmc-java/ArithmeticException1/test.desc b/regression/cbmc-java/ArithmeticException1/test.desc new file mode 100644 index 00000000000..e8f7c941fd4 --- /dev/null +++ b/regression/cbmc-java/ArithmeticException1/test.desc @@ -0,0 +1,9 @@ +CORE +ArithmeticExceptionTest.class +--java-throw-runtime-exceptions +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file ArithmeticExceptionTest.java line 8 function.*: FAILURE$ +^VERIFICATION FAILED +-- +^warning: ignoring diff --git a/regression/cbmc-java/ArithmeticException2/ArithmeticExceptionTest.class b/regression/cbmc-java/ArithmeticException2/ArithmeticExceptionTest.class new file mode 100644 index 0000000000000000000000000000000000000000..3ac62d1ede54f090f97492e6620371a6529a2426 GIT binary patch literal 646 zcmZvZ&rcIU6vw}>-QC&UF3=W)DzsSjfF9&R!okLXfTs$F5)<*X-A?M%c1vcb#=nJs zfHRQLL=(OHM;YI&)OuhKGjHCH&-=c&zkYxF0bmDDLxiZgY}+psco@LPBZ2i09%=#` zA?j!dY!a5A#aSk`QR6f_R9V~|${vBv2wqF2%Dg5Nx1PTzI0xgNBrLU6Dvu|luGFVC znFFI(rG(Y3kL^MHCEgy!X@9$8v`YK0Y~e!3#L4G(@p+!lVhDaK8Q#Ie&Um5|`Bquf z#=chO(?}YX9DPmXxm9&4GxO4dBP?K%P@gxsCp$t35ux^9(rmmVt;d?Mc2AY~jovTainI1qd{g1r?K-ZVEyyY3~b?Q6IfD1C?bVG8l{ zDz7YY0|$ki)yS*t%Vn;|GD42}%nZ1F3CqkBC>#r{Soec}+IDgjP^tR22reL;OE|?F WxK`(1_DrW`xF|$>cAC{Zy!HoF7ky*^ literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/ArithmeticException2/ArithmeticExceptionTest.java b/regression/cbmc-java/ArithmeticException2/ArithmeticExceptionTest.java new file mode 100644 index 00000000000..0c83bf9a409 --- /dev/null +++ b/regression/cbmc-java/ArithmeticException2/ArithmeticExceptionTest.java @@ -0,0 +1,12 @@ +public class ArithmeticExceptionTest { + public static void main(String args[]) { + try { + long denom=0; + long num=10; + long j=num/denom; + } + catch(ArithmeticException exc) { + assert false; + } + } +} diff --git a/regression/cbmc-java/ArithmeticException2/test.desc b/regression/cbmc-java/ArithmeticException2/test.desc new file mode 100644 index 00000000000..00820d86c6e --- /dev/null +++ b/regression/cbmc-java/ArithmeticException2/test.desc @@ -0,0 +1,9 @@ +CORE +ArithmeticExceptionTest.class +--java-throw-runtime-exceptions +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file ArithmeticExceptionTest.java line 9 function.*: FAILURE$ +^VERIFICATION FAILED +-- +^warning: ignoring diff --git a/regression/cbmc-java/ArithmeticException3/ArithmeticExceptionTest.class b/regression/cbmc-java/ArithmeticException3/ArithmeticExceptionTest.class new file mode 100644 index 0000000000000000000000000000000000000000..21c451e02f32de87391382dd30ce9f5daacffdf4 GIT binary patch literal 629 zcmZuuJx?1!5PfrZ_S(k*#w5lV9D+mv6wuINA`l@3a+1O*QlL7YS7gCHTYGE7Z{ZJ6 zJ4jdp33`4M%Itw-3bfLG%)IyJ&Fs_j-2;FvEc?izBrump7G;5XAD(?zd@Nv5ph}os z36n%>qq=eORV87wEn5USCS+?WR^|)AU0wS{@bbS@|=m2^6gz_8EsJ#QNyP7cf4$IaM_!M9Xp9zIA`DgP? zMuxi{hxXe%FmAUc6QyNqZzRuMnm#9ZTE|%CdFS{Gs8F_s_~wGFf8HngRppcT%&ZSV z0}I3y@7Xj+OqoW3?-qIjhsi+2trh%*-p)0O^}lehFmVs>_Yj%KLCO+b#^GgkDy#(l zY6lsJ)PUgPIm|O=hBE@rp+IqpL$m)qZKX26Ofh>4aRuRB!*g%oT7NIPBY##S11H$E KU3^H>AO8WIDtt!( literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/ArithmeticException3/ArithmeticExceptionTest.java b/regression/cbmc-java/ArithmeticException3/ArithmeticExceptionTest.java new file mode 100644 index 00000000000..dfe7b031288 --- /dev/null +++ b/regression/cbmc-java/ArithmeticException3/ArithmeticExceptionTest.java @@ -0,0 +1,11 @@ +public class ArithmeticExceptionTest { + public static void main(String args[]) { + try { + int i=0; + int j=10%i; + } + catch(ArithmeticException exc) { + assert false; + } + } +} diff --git a/regression/cbmc-java/ArithmeticException3/test.desc b/regression/cbmc-java/ArithmeticException3/test.desc new file mode 100644 index 00000000000..e8f7c941fd4 --- /dev/null +++ b/regression/cbmc-java/ArithmeticException3/test.desc @@ -0,0 +1,9 @@ +CORE +ArithmeticExceptionTest.class +--java-throw-runtime-exceptions +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file ArithmeticExceptionTest.java line 8 function.*: FAILURE$ +^VERIFICATION FAILED +-- +^warning: ignoring diff --git a/regression/cbmc-java/ArithmeticException4/ArithmeticExceptionTest.class b/regression/cbmc-java/ArithmeticException4/ArithmeticExceptionTest.class new file mode 100644 index 0000000000000000000000000000000000000000..a4723d1d652bd59d4cc9043e4a0654a2abb3aa7d GIT binary patch literal 646 zcmZvZO;6iE5Qg7LY_IJY2;nQGBq=Qi=%HMYI20j1N>70vf+`hGjOY9)H_k3!6vrs)A6c4z0~nRmv29)8{fSi_qTA*wFh_6r4G1n@C0@G^vls=z{s z8tMWK!qifnWl|f}PqPmyi`!k%4dSJ+wVxiL{p{mV9;wzeQ1+8 z(2G?{m|Z?@p2pwe)oz@gthS6+>B)OrIMy<8a<(6z=lLv#;BO?|zwoftALvAWR2H?c zt(E!OlSUZnf V*Xn#?4|Q6Gi$b(zrL>hEXQe2Th(qhZsUgsQm}(kGG?BstHriRM{Q^uS2}S zTS8?}{H1jwW5ZJqLR%eP7?0bQnbNYo*{A0zO^*}2tpn!q`4<3GsaZjMD}pzHGM^*t z)!7nTcj*>%Wr3*h>E%H}38Sd;-9nGxz-2pA{y2`peER7U)y6g43k>~+_w5$q{wgo? zxs!uJPBhI_$UT>plsF?;1-}7SHO3i%!mhx0nL`u*M6KpDz-ZO~iP8mxa|x$-1J?@t T!`l~VIb0ON4LinUo}PLF!N`3} literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/ArithmeticException5/ArithmeticExceptionTest.java b/regression/cbmc-java/ArithmeticException5/ArithmeticExceptionTest.java new file mode 100644 index 00000000000..d32299a427f --- /dev/null +++ b/regression/cbmc-java/ArithmeticException5/ArithmeticExceptionTest.java @@ -0,0 +1,11 @@ +public class ArithmeticExceptionTest { + public static void main(String args[]) { + try { + double i=0; + double j=10/i; + } + catch(ArithmeticException exc) { + assert false; + } + } +} diff --git a/regression/cbmc-java/ArithmeticException5/test.desc b/regression/cbmc-java/ArithmeticException5/test.desc new file mode 100644 index 00000000000..d57ec32a9a9 --- /dev/null +++ b/regression/cbmc-java/ArithmeticException5/test.desc @@ -0,0 +1,8 @@ +CORE +ArithmeticExceptionTest.class +--java-throw-runtime-exceptions +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL +-- +^warning: ignoring diff --git a/regression/cbmc-java/ArithmeticException6/ArithmeticExceptionTest.class b/regression/cbmc-java/ArithmeticException6/ArithmeticExceptionTest.class new file mode 100644 index 0000000000000000000000000000000000000000..fdcb29ad2522533d0fdb0d5fb7d08fe1d7d592ca GIT binary patch literal 605 zcmZutO;5r=5Pd^Si?s@(0-~rS9@K+gI1(d4j3#~@P!qkCveCs-Ok0e<#XrCqO*GL& z@BS#`EQ)wAo6OA4ym|9xK0aUG0F+R)kU+*nb_@n`Cgv>Y>YukTj|CG2!t{z0h9Zb$ z#}9X8=rlahB+v!HC`(^PTLf)&?TnyTJ551I9!Ostb=wUQoG36C+K%+ut?nz>L_Koc z>qF;eQ038tMA`LzsH}RY8@OUus>X#%Afv0ch@@M)bH$C)a3aEJqvhN>HpXES3M$_8 z9RG6jAGD1zScKdk&~TYr5Oe}U_Ma{_!^EPEB`gzCqvqpAOSlp5I7(GLJ`W+&6rl`6 zvofUTEu$_M_%;_P@^uq@a7yKrAdWPU($98+e+Bl$KED18>MI~7*&2f+aZ3^@jurG2 zF@8WUW#zqc59xykX!jU@g?|2w_}{ogW>B8}0?o>G7XSbN literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/ArithmeticException6/ArithmeticExceptionTest.java b/regression/cbmc-java/ArithmeticException6/ArithmeticExceptionTest.java new file mode 100644 index 00000000000..281f868b3e6 --- /dev/null +++ b/regression/cbmc-java/ArithmeticException6/ArithmeticExceptionTest.java @@ -0,0 +1,10 @@ +public class ArithmeticExceptionTest { + public static void main(int denom) { + try { + int j=10/denom; + } + catch(ArithmeticException exc) { + assert false; + } + } +} diff --git a/regression/cbmc-java/ArithmeticException6/test.desc b/regression/cbmc-java/ArithmeticException6/test.desc new file mode 100644 index 00000000000..8cab5f69869 --- /dev/null +++ b/regression/cbmc-java/ArithmeticException6/test.desc @@ -0,0 +1,9 @@ +CORE +ArithmeticExceptionTest.class +--java-throw-runtime-exceptions +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file ArithmeticExceptionTest.java line 7 function.*: FAILURE$ +^VERIFICATION FAILED +-- +^warning: ignoring