diffblue · mgudemann · Feb 27, 2018 · Feb 5, 2018 · Feb 5, 2018 · Feb 6, 2018
diff --git a/regression/cbmc-java/lots_local_variables_manual/ManyLocalVariables.class b/regression/cbmc-java/lots_local_variables_manual/ManyLocalVariables.class
diff --git a/regression/cbmc-java/lots_local_variables_manual/ManyLocalVariables.j b/regression/cbmc-java/lots_local_variables_manual/ManyLocalVariables.j
@@ -0,0 +1,36 @@
+; This generates a class file that attempts to access local variables indexed
+; at 255, 256 and 65534
+; The class file is generated from this file using the following command:
+; java -jar jasmin.jar ManyLocalVariables.j
+; The jasmin jar file can be obtained from: http://jasmin.sourceforge.net/
+
+.class public ManyLocalVariables
+.super java/lang/Object
+
+.method public static test()I
+  .limit stack 10
+  .limit locals 65535
+  .line 1
+   iconst_1
+   istore 1
+
+   iconst_1
+   istore 255
+
+   iconst_1
+   istore_w 256
+
+   iconst_1
+   istore_w 65534
+
+   iload 1
+   iload 255
+   iload_w 256
+   iload_w 65534
+
+   iadd
+   iadd
+   iadd
+
+   ireturn
+.end method
diff --git a/regression/cbmc-java/lots_local_variables_manual/test.desc b/regression/cbmc-java/lots_local_variables_manual/test.desc
@@ -0,0 +1,4 @@
+CORE
+ManyLocalVariables.class
+--function ManyLocalVariables.test
+VERIFICATION SUCCESSFUL
diff --git a/regression/cbmc-java/lots_of_local_variables/TooManyLocals.class b/regression/cbmc-java/lots_of_local_variables/TooManyLocals.class