From 3308bff50aba334e31cce7b81364c94eaea51a54 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 4 Jan 2025 17:25:39 +0100 Subject: [PATCH] Compile jbmc/class-literals test sources Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. --- .../class-literals/ExampleAnnotation.class | Bin 154 -> 0 bytes .../jbmc/class-literals/ExampleEnum.class | Bin 668 -> 0 bytes .../class-literals/ExampleInterface.class | Bin 113 -> 0 bytes .../class-literals/ExampleSynthetic.class | Bin 110 -> 0 bytes .../regression/jbmc/class-literals/Test.class | Bin 1646 -> 0 bytes .../jbmc/class-literals/java/lang/Class.class | Bin 1404 -> 0 bytes .../class-literals/org/cprover/CProver.class | Bin 536 -> 0 bytes .../class-literals/org/cprover/CProver.java | 15 ------- .../org/cprover/MustNotThrow.class | Bin 156 -> 0 bytes .../org/cprover/MustNotThrow.java | 8 ---- jbmc/regression/jbmc/class-literals/pom.xml | 41 ++++++++++++++++++ .../main/java}/ExampleAnnotation.java | 0 .../{ => src/main/java}/ExampleEnum.java | 0 .../{ => src/main/java}/ExampleInterface.java | 0 .../{ => src/main/java}/ExampleSynthetic.j | 0 .../{ => src/main/java}/Test.java | 0 .../{ => src/main/java}/java/lang/Class.java | 4 +- jbmc/regression/jbmc/class-literals/test.desc | 2 +- .../jbmc/class-literals/test_lazy.desc | 2 +- jbmc/regression/jbmc/pom.xml | 1 + 20 files changed, 47 insertions(+), 26 deletions(-) delete mode 100644 jbmc/regression/jbmc/class-literals/ExampleAnnotation.class delete mode 100644 jbmc/regression/jbmc/class-literals/ExampleEnum.class delete mode 100644 jbmc/regression/jbmc/class-literals/ExampleInterface.class delete mode 100644 jbmc/regression/jbmc/class-literals/ExampleSynthetic.class delete mode 100644 jbmc/regression/jbmc/class-literals/Test.class delete mode 100644 jbmc/regression/jbmc/class-literals/java/lang/Class.class delete mode 100644 jbmc/regression/jbmc/class-literals/org/cprover/CProver.class delete mode 100644 jbmc/regression/jbmc/class-literals/org/cprover/CProver.java delete mode 100644 jbmc/regression/jbmc/class-literals/org/cprover/MustNotThrow.class delete mode 100644 jbmc/regression/jbmc/class-literals/org/cprover/MustNotThrow.java create mode 100644 jbmc/regression/jbmc/class-literals/pom.xml rename jbmc/regression/jbmc/class-literals/{ => src/main/java}/ExampleAnnotation.java (100%) rename jbmc/regression/jbmc/class-literals/{ => src/main/java}/ExampleEnum.java (100%) rename jbmc/regression/jbmc/class-literals/{ => src/main/java}/ExampleInterface.java (100%) rename jbmc/regression/jbmc/class-literals/{ => src/main/java}/ExampleSynthetic.j (100%) rename jbmc/regression/jbmc/class-literals/{ => src/main/java}/Test.java (100%) rename jbmc/regression/jbmc/class-literals/{ => src/main/java}/java/lang/Class.java (93%) diff --git a/jbmc/regression/jbmc/class-literals/ExampleAnnotation.class b/jbmc/regression/jbmc/class-literals/ExampleAnnotation.class deleted file mode 100644 index ab1a979353344d43509e2474ef3ed0e848504b81..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 154 zcmX^0Z`VEs1_l!bPId-1b_RBK1`b9BuHgLAqU2P!%$!t41~J!)#N2|MRL8u${F20y z%=|pPti-ZJMg~C)2}TA1kd%H-VqUtwe^ORzatR}YJVGcDZiGIYwP)~{!Vh~6^SibZ$*OJMcp-%d<`T-R|;d6gf zbiWxkwGHm}-Fxo2=iKk>`~4HZ5wZb@*p#t_goJ>EZ5a}hJnTr=Wsvq-r}e8^lOc3n zuidM?J5#S&cCW^SV=HEtO)xq4R} zt3^|_I>qK_U|5|}esM(Eu#8cKA^s2eJl|pnG>wj>j_d((dvZMEFKgy+SIRYki!RU6 zSIC3h?ArrPKQp+th|Avr*QUVFcM?#LLYg7ysw)T~qacD++RUF1K83-nnSF~0W4XLb zL8IN(wGjTp4 z=YdWPD-?ZBO(1*-;Tc|VvT{@`yumwxxQrLLLkJFk3Lbg^sj#1Xh3|2RJW3e>Ya}j4 aaVje9i~#(e4~WlT%UuGded~xj{Tn~}+=My+ diff --git a/jbmc/regression/jbmc/class-literals/ExampleInterface.class b/jbmc/regression/jbmc/class-literals/ExampleInterface.class deleted file mode 100644 index 3669f3afa5c7c995b597616cd25ef0beeef84b91..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 113 zcmX^0Z`VEs1_l!bc6J6@1{MG|fgE1| diff --git a/jbmc/regression/jbmc/class-literals/ExampleSynthetic.class b/jbmc/regression/jbmc/class-literals/ExampleSynthetic.class deleted file mode 100644 index 3be8707e65e122d1407cb9531d586c87d67f3726..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 110 zcmX^0Z`VEsW(Hjbc6J69b_P~P1|ipq#N2|M)Zogzl8n@n%w)YRMh1bb#Ii*FoW#6z segCAa)Z`MN5V|@>2Cm@z(xT*4x6GVW0YwHT21W)5U}RteGME^c0p431p8x;= diff --git a/jbmc/regression/jbmc/class-literals/Test.class b/jbmc/regression/jbmc/class-literals/Test.class deleted file mode 100644 index c6ca2351f0ddd9e81137e371e1bf82e94187ca4d..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 1646 zcmZ{lOHUI~6vzMfws5EI0PPe?kvF39eu+;Ic`FFGC^0GsegdK! z6XVuLQj8`VH!fWG30(RKT)Hrxi$xlGoyC7Tzd1dxdrs!-@An@83}Y#bW^{+ph#rAn zfj)u$Fv`#^Fd#4}FeGqRU|8Usza>3Npx+d0RZwmow-W34f;yA0){wqyHa41tc$TMWUe+?vHuwO~8e z(pGlWa+jqsy~vuj!%&g(&Gf@XbF+Z8(R8NZAe_o=xoKl%k%p-%xzOg8&2wI zK`TRS=8>7*%vckSlk-iP4TX|M{Tb6)@1M$0mJG=wGI5yojO*rHhG@aToa0;WeKSpw zA_X+#Y-NuOQag_S!1C=h17Devl9DnfWnRjx6zU9Lp(eyv7LH=xT-~tJ{s=?$iURAH z!K{vJQm#vxlQJ*m1{SDKvTz-Xpa9Y1P8oFDD=wazPT?cAS5#2B?ftEVa8Vh8{^`2r z4ue>?{3SC>wO4m^7A2nYUE5iw#1m_lXS>$gzwXhY`CA@ZY37<~23a&I&x3viz~u3e zw$oE1-5K4>y7s|dOGBI@EkA%9A)G!m4Wz*74fwM+;CqN0fzJr;A@TubclJ^KsX&F2 zYDyYX(y)?7lvG#J3MH*n(kdm5Drrnf4J8fa5m$64kLpsY}Xo!0d#v~%R4IK_Du!~CUp$e}M#TUfz9R_|P&NNiBCM4J}YS}!J>>ldaHtN|E zG_dDrWbe?#zM+}@KnweYRvtwgrv>4o=;h1k;~DhxT@3K27{VFKqyfgc5S`73ouqElkC>07h4RrRaoYqWZXhI7fmA6iQd{*>py>g{sMq!@U#MRuvvx*GznS+ZGwPci(s2z zhoIv^*M%nn3R;dr0n5D$c`3U?sR!L76DvJgYnjf&J~I;U7MWsaqzYN$2htS<2_VYa;QFs z{HCXHUO5!7+PX%X9`|(e&>W4!u{LTH?&(XFD0G~qfQI#66c4&nhwlD3F$a-3K98eM z=S7gGi@^^N-}tk;hz@V&p^m*b`2ZTQiYvSpxQFIM{*ASawG(WmkPB8*$OmgF z6av4HqM~0+!3lgP1vl{B6iR_#N})V+*<^Mdil|*d^(t!nsNR74c;IztBJRK=p5ooa zX*vaZatt(jhl9v*M^WUtqc95GQ5;3?C=iD`ip1rPLMfr&1-d>&{6C)Wko$@+ zb1;i%!y3;54t$fG|B@j$t>i^3xsWBdtmGvtxtJxlt>k4Z*~yXvD|y9AcC+LyE4gMR Wm$Kw-E7`Y_%USY{mHe3RWaA%(mAcOW diff --git a/jbmc/regression/jbmc/class-literals/org/cprover/CProver.class b/jbmc/regression/jbmc/class-literals/org/cprover/CProver.class deleted file mode 100644 index cd291032b8d3ff78f6e578287586342b9835eecf..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 536 zcmZvZOH0E*6ot<;=_|HAs`XJHblHj+1a}odimrl+O2O`?aY#qn8A&I#f6G-tLHGVB z@lLGNg^SFYdvoqLXOhpa*LMKN*vn(XLk^pHY!y)R;9xtC9fp!nyf+YMqfs&x46Msg zZfi9%T$v6ZB*LM2#*jOaN}5v!r_t;%xNZGF_N727ahVKzBEGX2hDxAAKIrgR+IrS> zO<#@}s)3FpKYWVySj2w&I@K1j`RsJJ(Y5emsMUisQY!}URwr>NE~JH*W;2J6e9ReE z|G|~8fD%K^I{X1wk$;mYBZuOA5{joE=0Te)rA=K-M3@*+r$AB6hxKP^`t{!JO^I&9z|&AI*nl7yfv{@QLEX(5$HztqhSkq6iACyW#G}nY&u%Y)bU9fX?A~# z%u8xnq&1f|9W2q_TFHQAtdJH_!76p^@G<>B`_6lVb6;_%$bL|j!JM%0hu~q2g4jsa H)V2N%hrMv7 diff --git a/jbmc/regression/jbmc/class-literals/org/cprover/CProver.java b/jbmc/regression/jbmc/class-literals/org/cprover/CProver.java deleted file mode 100644 index fe21dd16ad4..00000000000 --- a/jbmc/regression/jbmc/class-literals/org/cprover/CProver.java +++ /dev/null @@ -1,15 +0,0 @@ -package org.cprover; - -public final class CProver -{ - public static final boolean enableAssume=true; - - public static void assume(boolean condition) - { - if(enableAssume) - { - throw new RuntimeException( - "Cannot execute program with CProver.assume()"); - } - } -} diff --git a/jbmc/regression/jbmc/class-literals/org/cprover/MustNotThrow.class b/jbmc/regression/jbmc/class-literals/org/cprover/MustNotThrow.class deleted file mode 100644 index ca862caecb9182b58caa09db993c27375f295171..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 156 zcmX^0Z`VEs1_l!bPId-1b_RBK1`b9BuHgLAqU2P!%$!t420`D_;u637l8}s|{Bpgl z#Ii(228sNlbp7OlqWrSdB7J0eMg{?p3jLhKymWp4q^#8B5=I7jgivB$UVcepNoIbY bz9XEe#>l|Pzy!q1K$kE8X%-;K#J~yw8s{pl diff --git a/jbmc/regression/jbmc/class-literals/org/cprover/MustNotThrow.java b/jbmc/regression/jbmc/class-literals/org/cprover/MustNotThrow.java deleted file mode 100644 index 7be14b181d7..00000000000 --- a/jbmc/regression/jbmc/class-literals/org/cprover/MustNotThrow.java +++ /dev/null @@ -1,8 +0,0 @@ -package org.cprover; - -/** - * This can be added to methods to indicate they aren't allowed to throw - * exceptions. JBMC and related tools will truncate any execution path on which - * they do with an ASSUME FALSE instruction. - */ -public @interface MustNotThrow { } diff --git a/jbmc/regression/jbmc/class-literals/pom.xml b/jbmc/regression/jbmc/class-literals/pom.xml new file mode 100644 index 00000000000..7398a7121cb --- /dev/null +++ b/jbmc/regression/jbmc/class-literals/pom.xml @@ -0,0 +1,41 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.class-literals + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + org.cprover.util + cprover-api + + + + + + + maven-jar-plugin + + + default-jar + none + + + + + com.github.abextm + jasmin-maven-plugin + + + + + diff --git a/jbmc/regression/jbmc/class-literals/ExampleAnnotation.java b/jbmc/regression/jbmc/class-literals/src/main/java/ExampleAnnotation.java similarity index 100% rename from jbmc/regression/jbmc/class-literals/ExampleAnnotation.java rename to jbmc/regression/jbmc/class-literals/src/main/java/ExampleAnnotation.java diff --git a/jbmc/regression/jbmc/class-literals/ExampleEnum.java b/jbmc/regression/jbmc/class-literals/src/main/java/ExampleEnum.java similarity index 100% rename from jbmc/regression/jbmc/class-literals/ExampleEnum.java rename to jbmc/regression/jbmc/class-literals/src/main/java/ExampleEnum.java diff --git a/jbmc/regression/jbmc/class-literals/ExampleInterface.java b/jbmc/regression/jbmc/class-literals/src/main/java/ExampleInterface.java similarity index 100% rename from jbmc/regression/jbmc/class-literals/ExampleInterface.java rename to jbmc/regression/jbmc/class-literals/src/main/java/ExampleInterface.java diff --git a/jbmc/regression/jbmc/class-literals/ExampleSynthetic.j b/jbmc/regression/jbmc/class-literals/src/main/java/ExampleSynthetic.j similarity index 100% rename from jbmc/regression/jbmc/class-literals/ExampleSynthetic.j rename to jbmc/regression/jbmc/class-literals/src/main/java/ExampleSynthetic.j diff --git a/jbmc/regression/jbmc/class-literals/Test.java b/jbmc/regression/jbmc/class-literals/src/main/java/Test.java similarity index 100% rename from jbmc/regression/jbmc/class-literals/Test.java rename to jbmc/regression/jbmc/class-literals/src/main/java/Test.java diff --git a/jbmc/regression/jbmc/class-literals/java/lang/Class.java b/jbmc/regression/jbmc/class-literals/src/main/java/java/lang/Class.java similarity index 93% rename from jbmc/regression/jbmc/class-literals/java/lang/Class.java rename to jbmc/regression/jbmc/class-literals/src/main/java/java/lang/Class.java index c39aedf97cb..162a8b70515 100644 --- a/jbmc/regression/jbmc/class-literals/java/lang/Class.java +++ b/jbmc/regression/jbmc/class-literals/src/main/java/java/lang/Class.java @@ -1,6 +1,6 @@ package java.lang; -public class Class { +public class Class { private String name; @@ -43,4 +43,6 @@ public void cproverInitializeClassLiteral( public boolean isLocalClass() { return isLocalClass; } public boolean isMemberClass() { return isMemberClass; } public boolean isEnum() { return isEnum; } + + public boolean desiredAssertionStatus() { return true; } } diff --git a/jbmc/regression/jbmc/class-literals/test.desc b/jbmc/regression/jbmc/class-literals/test.desc index 513924f665e..3ac8b38eb62 100644 --- a/jbmc/regression/jbmc/class-literals/test.desc +++ b/jbmc/regression/jbmc/class-literals/test.desc @@ -1,6 +1,6 @@ CORE bdd-expected-timeout Test ---function Test.main +--function Test.main -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/class-literals/test_lazy.desc b/jbmc/regression/jbmc/class-literals/test_lazy.desc index 76b0dd8b13e..e0bd3dcc723 100644 --- a/jbmc/regression/jbmc/class-literals/test_lazy.desc +++ b/jbmc/regression/jbmc/class-literals/test_lazy.desc @@ -1,6 +1,6 @@ CORE symex-driven-lazy-loading-expected-failure Test ---function Test.main +--function Test.main -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 034e4b9ae1e..374981ad7ee 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -68,6 +68,7 @@ catch1 char1 class-fields + class-literals classpath-jar-load-whole-jar