Add tests of unicode character support in Java class file names

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

jbmc/regression/jbmc/unicode-class-filename/ЮЛ.java

@@ -0,0 +1,12 @@
+public class ЮЛ
+{
+  static void f()
+  {
+    assert false;
+  }
+
+  public static void main(String[] args)
+  {
+    ЮЛ.f();
+  }
+}

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

jbmc/regression/jbmc/unicode-class-name/ЮЛ.java

@@ -0,0 +1,13 @@
+public class ЮЛ
+{
+  void f()
+  {
+    assert false;
+  }
+
+  public static void main(String[] args)
+  {
+    ЮЛ obj = new ЮЛ();
+    obj.f();
+  }
+}

jbmc/regression/jbmc/unicode-method-name/f.java

@@ -0,0 +1,13 @@
+public class f
+{
+  void ЮЛ()
+  {
+    assert false;
+  }
+
+  public static void main(String[] args)
+  {
+    f obj = new f();
+    obj.ЮЛ();
+  }
+}

jbmc/regression/jbmc/unicode-method-name/test.desc

@@ -0,0 +1,8 @@
+CORE
+f
+--
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+Test Unicode characters in Java method names (should already work)

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/exit_codes.h>
 #include <util/help_formatter.h>
 #include <util/options.h>
+#include <util/suffix.h>
 #include <util/version.h>
 
 #include <goto-programs/goto_check.h>
@@ -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;

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/exit_codes.h>
 #include <util/help_formatter.h>
 #include <util/invariant.h>
+#include <util/suffix.h>
 #include <util/version.h>
 #include <util/xml.h>
 
@@ -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;