Test constant propagation of array length and cells

The test would fail if the length or cells of the array was not
propagated by symex and available when deciding on which branch
of the if-then-else to analyse.

Author: romainbrenguier

jbmc/regression/jbmc/constant-propagation/Test.class

@@ -0,0 +1,37 @@
+public class Test {
+
+  public String checkPass() {
+    String string = "vVvvVvvVv";
+    int[] array = new int[4];
+    if(array.length == 4)
+    {
+      String result = string.toLowerCase();
+      assert(result.charAt(0) == 'v');
+      return result;
+    }
+    else
+    {
+      String result = string.toUpperCase();
+      assert(result.charAt(0) == 'V');
+      return result;
+    }
+  }
+
+  static public String checkPass1() {
+    int[] array = new int[1];
+    array[0] = 23;
+    if(array[0] == 92)
+    {
+      String result = "vVvvVvvVv".toLowerCase();
+      assert(result.charAt(0) == 'v');
+      return result;
+    }
+    else
+    {
+      String result = "vVvvVvvVv".toUpperCase();
+      assert(result.charAt(0) == 'V');
+      return result;
+    }
+  }
+
+}

jbmc/regression/jbmc/constant-propagation/Test.java

@@ -0,0 +1,11 @@
+CORE
+Test.class
+--function Test.checkPass --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --unwind 10 --show-vcc
+^EXIT=0$
+^SIGNAL=0$
+cprover_string_to_lower_case_func
+--
+cprover_string_to_upper_case_func
+--
+Check that to_upper_case calls are not reached by symex, because the length is
+correctly propagated