From c2b0a9940e7d85aaba1b8a443248c38bb2a27542 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 29 Nov 2025 18:51:23 +0100 Subject: [PATCH] Add tests of unicode character support in Java class file names Add regression tests for unicode class and method names. Fixes: #628 --- .../jbmc/unicode-class-filename/test.desc | 8 ++++++++ .../\320\256\320\233.class" | Bin 0 -> 574 bytes .../unicode-class-filename/\320\256\320\233.java" | 12 ++++++++++++ jbmc/regression/jbmc/unicode-class-name/test.desc | 8 ++++++++ .../unicode-class-name/\320\256\320\233.class" | Bin 0 -> 592 bytes .../unicode-class-name/\320\256\320\233.java" | 13 +++++++++++++ jbmc/regression/jbmc/unicode-method-name/f.class | Bin 0 -> 589 bytes jbmc/regression/jbmc/unicode-method-name/f.java | 13 +++++++++++++ .../regression/jbmc/unicode-method-name/test.desc | 8 ++++++++ jbmc/src/janalyzer/janalyzer_parse_options.cpp | 6 ++++++ jbmc/src/jbmc/jbmc_parse_options.cpp | 6 ++++++ 11 files changed, 74 insertions(+) create mode 100644 jbmc/regression/jbmc/unicode-class-filename/test.desc create mode 100644 "jbmc/regression/jbmc/unicode-class-filename/\320\256\320\233.class" create mode 100644 "jbmc/regression/jbmc/unicode-class-filename/\320\256\320\233.java" create mode 100644 jbmc/regression/jbmc/unicode-class-name/test.desc create mode 100644 "jbmc/regression/jbmc/unicode-class-name/\320\256\320\233.class" create mode 100644 "jbmc/regression/jbmc/unicode-class-name/\320\256\320\233.java" create mode 100644 jbmc/regression/jbmc/unicode-method-name/f.class create mode 100644 jbmc/regression/jbmc/unicode-method-name/f.java create mode 100644 jbmc/regression/jbmc/unicode-method-name/test.desc diff --git a/jbmc/regression/jbmc/unicode-class-filename/test.desc b/jbmc/regression/jbmc/unicode-class-filename/test.desc new file mode 100644 index 00000000000..3bc410091b9 --- /dev/null +++ b/jbmc/regression/jbmc/unicode-class-filename/test.desc @@ -0,0 +1,8 @@ +CORE +ЮЛ +-- +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +Test that .class suffix is properly stripped for Unicode class names \ No newline at end of file diff --git "a/jbmc/regression/jbmc/unicode-class-filename/\320\256\320\233.class" "b/jbmc/regression/jbmc/unicode-class-filename/\320\256\320\233.class" new file mode 100644 index 0000000000000000000000000000000000000000..1b4f30f4770b2a2934f01bb2d154fd6ba4ba6140 GIT binary patch literal 574 zcmYjOOD_Xa6#mZ4)U?y-%cJV8iG^CQu_Ho?mB*qY!D`xGa;v5?GxcNm0d^832nl;D zzet=@kFmJ-oRj-K&N=t}^Z6CP8p;j~m^LgI3G@;2E$_lxXnX$2!fw5#8WEvyS^GL# zA(*q3{S=Z&*>GH>;S#Kmn~y8Pz>F7$Du{H)57%|*)!V8`phFv3LMfJ9`$cU8K__sK zf$6Yd!9~BA)3Jj=4B05U7)FVZi>cK%TM&v(73x4W|CDNx7j^l8n>*xws-31{-j?>& zPWP;?f<0-5kYQZoblW@ssjV|l`z$wmv=w{QqCop6OO<^>a=Fp|8QZCKxunL9UliIgwNGB~q9vPHf}xSHTd920Yopj!cAly7;KJSj7C6zF142*};RzC`*3 znS)2<-h^cINb*apge+6WI5R<6q%hty5rt_!qH8@NAA5b%9EPXaZ}Oj?V1Yt^@&N;v bu&rxY<~{7#@wZKJOTchfWtb^03`~Ck50Ya@ literal 0 HcmV?d00001 diff --git "a/jbmc/regression/jbmc/unicode-class-filename/\320\256\320\233.java" "b/jbmc/regression/jbmc/unicode-class-filename/\320\256\320\233.java" new file mode 100644 index 00000000000..4b92533b12c --- /dev/null +++ "b/jbmc/regression/jbmc/unicode-class-filename/\320\256\320\233.java" @@ -0,0 +1,12 @@ +public class ЮЛ +{ + static void f() + { + assert false; + } + + public static void main(String[] args) + { + ЮЛ.f(); + } +} \ No newline at end of file diff --git a/jbmc/regression/jbmc/unicode-class-name/test.desc b/jbmc/regression/jbmc/unicode-class-name/test.desc new file mode 100644 index 00000000000..9581d9f964e --- /dev/null +++ b/jbmc/regression/jbmc/unicode-class-name/test.desc @@ -0,0 +1,8 @@ +CORE +ЮЛ +-- +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +Test Unicode characters in Java class names diff --git "a/jbmc/regression/jbmc/unicode-class-name/\320\256\320\233.class" "b/jbmc/regression/jbmc/unicode-class-name/\320\256\320\233.class" new file mode 100644 index 0000000000000000000000000000000000000000..1d50a7d016caccca04d4d9c569c204c005c7f395 GIT binary patch literal 592 zcmYjOOD_Xa6#mZ4)U;#z@UFLtg-5WlBSJh@#iAm?YT91St(wZr)Q{l@*h!GI2?={E zzet=TWo*u4?)e_)%*WTu8-Q)hIxt|`uv{e2L&(*=8*jDY`L)%fa$Qv-LeGZwb+kz^ z=NC>=NFrs!anTExV0}J(-Vp}oyf9Qjq?>-Yt3$8cP*nn**~k#`G3EB})LsxY0|#lC z4io-_eisAcfG!*iVc5oqi#$dN*%-gmU>(A6RfRfG)jzsYC+Cf?*cM@K=P}Y2^oe=aAkrrNU_9JmtmO)WF-BHBx7^Mr8fFv(F`L1Ik-4=IZyu+ j7iplcKiS6MEo|!^miY`jmjCrE(g_&umTWe|je){9zVc=R literal 0 HcmV?d00001 diff --git "a/jbmc/regression/jbmc/unicode-class-name/\320\256\320\233.java" "b/jbmc/regression/jbmc/unicode-class-name/\320\256\320\233.java" new file mode 100644 index 00000000000..e77f72fb4d3 --- /dev/null +++ "b/jbmc/regression/jbmc/unicode-class-name/\320\256\320\233.java" @@ -0,0 +1,13 @@ +public class ЮЛ +{ + void f() + { + assert false; + } + + public static void main(String[] args) + { + ЮЛ obj = new ЮЛ(); + obj.f(); + } +} diff --git a/jbmc/regression/jbmc/unicode-method-name/f.class b/jbmc/regression/jbmc/unicode-method-name/f.class new file mode 100644 index 0000000000000000000000000000000000000000..89ece316f8f4ba886b5fab2b9b5f94396415c68f GIT binary patch literal 589 zcmYjOO)mps5Psg>ZMWTSKeSYRt2nd-7dIlB;#3?e5}dZ}TY0Ii>~8%Set??<2?+^z zr~V=_)0B02XJ+U5n3?_he)|AW!GZ-1x(UNZ1W|#^g>&PqbsYD6?XYnnn}I-dQ@JYG z63|QK<2Yi7o3LyoU<-)0KyK0Tedz_N>-sy&cN!hpqRy#_lt3ZWtNfyNJ+JFoNJ6(r zZSZ7m zl?T16hV+hjD1jv5nwR^|^{_Us9OaT+>8uud)B{hs=Nsi?f!JoVGu+*(cY9t_?kU!Z zwpSUCB8{)n8AYbR=b+4h;5*VgN!1KRK{2xQ3h~H5Owr42&cQoVWav5x@t5=y%v&Vh zkvw@t`jbi8fW-fal#n9IG-WzO3URWS9V)C4fFa3u#E6@zEx%wSG))l$;Dhs|HpRJr k=4=g&WMeNFy@hGq!_c2$hW5WRvvmZTz0I4=Q=y^w1CRb=eE #include #include +#include #include #include @@ -355,6 +356,11 @@ int janalyzer_parse_optionst::doit() if((cmdline.args.size() == 1) && !cmdline.isset("show-parse-tree")) { std::string main_class = cmdline.args[0]; + + // Strip .class suffix if present (to support filenames like "ClassName.class") + if(has_suffix(main_class, ".class")) + main_class.resize(main_class.size() - 6); + // `java` accepts slashes and dots as package separators std::replace(main_class.begin(), main_class.end(), '/', '.'); config.java.main_class = main_class; diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 7ed4105af63..a16a3aa0172 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -433,6 +434,11 @@ int jbmc_parse_optionst::doit() if((cmdline.args.size() == 1) && !cmdline.isset("show-parse-tree")) { std::string main_class = cmdline.args[0]; + + // Strip .class suffix if present (to support filenames like "ClassName.class") + if(has_suffix(main_class, ".class")) + main_class.resize(main_class.size() - 6); + // `java` accepts slashes and dots as package separators std::replace(main_class.begin(), main_class.end(), '/', '.'); config.java.main_class = main_class;