Documentation to existing code + fixes parameter detection on bytecode->goto translation

regression/cbmc-java/lvt-unexpected/Makefile

@@ -0,0 +1,7 @@
+
+T=unexpected
+
+all : $T.class
+
+%.class : %.j
+	jasmin $<

regression/cbmc-java/lvt-unexpected/test.desc

@@ -0,0 +1,12 @@
+KNOWNBUG
+unexpected.class
+--verbosity 10 --show-symbol-table
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+The LVT in the only method in unexpected.class does not satisfy the constraints
+expected by the bytecode to goto conversion algorithms. Namely, the live range
+of parameter x in that method is not preceeded by a store_i instruction, which
+is perfectly possibly as per the JVM specs but currently additionally required
+in CBMC.

regression/cbmc-java/lvt-unexpected/unexpected.j

@@ -0,0 +1,34 @@
+.class public unexpected
+.super java/lang/Object
+
+.method public static test1(I)I
+  .limit stack 10
+  .limit locals 20
+
+  ; unexpected in previous code, as arg is the argument of the method and its
+  ; start_pc is != 0
+  .var 0 is arg I from Label1 to Label2
+  .var 1 is x   I from Label1 to Label2
+
+  ; say hello
+  getstatic      java/lang/System/out Ljava/io/PrintStream;
+  ldc            "Starting test1!"
+  invokevirtual  java/io/PrintStream/println(Ljava/lang/String;)V
+
+Label1:
+  ; x = arg + 3
+  iload_0
+  iconst_3
+  iadd
+  istore_1
+
+  ; say bye
+  getstatic      java/lang/System/out Ljava/io/PrintStream;
+  ldc            "Returning from test1!"
+  invokevirtual  java/io/PrintStream/println(Ljava/lang/String;)V
+
+  ; return x
+  iload_1
+  ireturn
+Label2:
+.end method

regression/cbmc-java/method_parmeters1/method_parameters.java

@@ -0,0 +1,129 @@
+class method_parameters
+{
+  void test1()
+  {}
+
+  void test2(boolean b)
+  {}
+
+  void test3(byte b)
+  {}
+
+  void test3a(char c)
+  {}
+
+  void test4(int i)
+  {}
+
+  void test5(float f)
+  {}
+
+  void test6(String s)
+  {}
+
+  void test7(long l)
+  {}
+
+  void test8(double l)
+  {}
+
+  void test9(int i, long l)
+  {
+    int local = 123;
+  }
+
+  void test10(double i, String s)
+  {
+    int local = 123;
+  }
+
+  void test11(int a[][])
+  {}
+
+  double test12(double a[][], double d)
+  {
+    if (a.length < 1) return 0;
+    if (a[0].length < 1) return 0;
+    return d + a[0][0];
+  }
+
+  void test12a(double a[][][], int i, double d)
+  {}
+
+  double test12b(double a[][], double d)
+  {
+    return 123.123;
+  }
+
+  void test12c(double a[][][], double d)
+  {
+  }
+
+  void test13(double d, int i, byte b, char c)
+  {}
+
+  // Same as above but now static
+
+  static void ttest1()
+  {}
+
+  static void ttest2(boolean b)
+  {}
+
+  static void ttest3(byte b)
+  {}
+
+  static void ttest3a(char c)
+  {}
+
+  static void ttest4(int i)
+  {}
+
+  static void ttest5(float f)
+  {}
+
+  static void ttest6(String s)
+  {}
+
+  static void ttest7(long l)
+  {}
+
+  static void ttest8(double l)
+  {}
+
+  static void ttest9(int i, long l)
+  {
+    int local = 123;
+  }
+
+  static void ttest10(double i, String s)
+  {
+    int local = 123;
+  }
+
+  static void ttest11(int a[][])
+  {}
+
+  static double ttest12(double a[][], double d)
+  {
+    if (a.length < 1) return 0;
+    if (a[0].length < 1) return 0;
+    return d + a[0][0];
+  }
+
+  static void ttest12a(double a[][][], int i, double d)
+  {}
+
+  static double ttest12b(double a[][], double d)
+  {
+    return 123.123;
+  }
+
+  static void ttest12c(double a[][][], double d)
+  {
+  }
+
+  static void ttest13(double d, int i, byte b, char c)
+  {}
+
+}

regression/cbmc-java/method_parmeters1/test.desc

@@ -0,0 +1,9 @@
+CORE
+method_parameters.class
+--verbosity 10 --show-symbol-table
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+The purpose of the test is ensuring that the bytecode -> symbol table AST
+generation happens correctly. The generated .class file does not contain LVTs.

regression/cbmc-java/method_parmeters2/method_parameters.java

@@ -0,0 +1,129 @@
+class method_parameters
+{
+  void test1()
+  {}
+
+  void test2(boolean b)
+  {}
+
+  void test3(byte b)
+  {}
+
+  void test3a(char c)
+  {}
+
+  void test4(int i)
+  {}
+
+  void test5(float f)
+  {}
+
+  void test6(String s)
+  {}
+
+  void test7(long l)
+  {}
+
+  void test8(double l)
+  {}
+
+  void test9(int i, long l)
+  {
+    int local = 123;
+  }
+
+  void test10(double i, String s)
+  {
+    int local = 123;
+  }
+
+  void test11(int a[][])
+  {}
+
+  double test12(double a[][], double d)
+  {
+    if (a.length < 1) return 0;
+    if (a[0].length < 1) return 0;
+    return d + a[0][0];
+  }
+
+  void test12a(double a[][][], int i, double d)
+  {}
+
+  double test12b(double a[][], double d)
+  {
+    return 123.123;
+  }
+
+  void test12c(double a[][][], double d)
+  {
+  }
+
+  void test13(double d, int i, byte b, char c)
+  {}
+
+  // Same as above but now static
+
+  static void ttest1()
+  {}
+
+  static void ttest2(boolean b)
+  {}
+
+  static void ttest3(byte b)
+  {}
+
+  static void ttest3a(char c)
+  {}
+
+  static void ttest4(int i)
+  {}
+
+  static void ttest5(float f)
+  {}
+
+  static void ttest6(String s)
+  {}
+
+  static void ttest7(long l)
+  {}
+
+  static void ttest8(double l)
+  {}
+
+  static void ttest9(int i, long l)
+  {
+    int local = 123;
+  }
+
+  static void ttest10(double i, String s)
+  {
+    int local = 123;
+  }
+
+  static void ttest11(int a[][])
+  {}
+
+  static double ttest12(double a[][], double d)
+  {
+    if (a.length < 1) return 0;
+    if (a[0].length < 1) return 0;
+    return d + a[0][0];
+  }
+
+  static void ttest12a(double a[][][], int i, double d)
+  {}
+
+  static double ttest12b(double a[][], double d)
+  {
+    return 123.123;
+  }
+
+  static void ttest12c(double a[][][], double d)
+  {
+  }
+
+  static void ttest13(double d, int i, byte b, char c)
+  {}
+
+}

regression/cbmc-java/method_parmeters2/test.desc

@@ -0,0 +1,10 @@
+CORE
+method_parameters.class
+--verbosity 10 --show-symbol-table
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+The purpose of the test is ensuring that the bytecode -> symbol table AST
+generation happens correctly. The generated .class file DOES contain LVTs, i.e.,
+it has been compiled with with "javac -g".