unicode support for java class files

[mgudemann]

java identifiers (and therefore also class files can contain unicode characters (cf. http://docs.oracle.com/javase/specs/jls/se7/html/jls-3.html#jls-3.8), CBMC/Java does not seem to support unicode in file names currently, e.g.

public class ЮЛ
{
  void f()
  {
  }
}

results in main symbol 'ЮЛ.f' not found

public class f
{
  void ЮЛ()
  {
  }
}

succeeds with the following in coverage analysis:

** coverage results:
[java::f.<init>:()V.coverage.1] file f.java line 1 function java::f.<init>:()V bytecode_index 1 block 1: FAILED
[java::f.<init>:()V.coverage.2] file f.java line 1 function java::f.<init>:()V bytecode_index 2 block 2: FAILED
[java::f.ЮЛ:()V.coverage.1] file f.java line 5 function java::f.ЮЛ:()V bytecode_index 0 block 1: SATISFIED