Merge pull request #5129 from JohnDumbell/jd/feature/constant_string_functions

Constant propagate string-solver function results

Author: JohnDumbell

jbmc/regression/jbmc-strings/ConstantEvaluationContains/Main.class

@@ -0,0 +1,31 @@
+public class Main {
+    public void contains() {
+        String str = "abcde";
+        assert str.contains("cd");
+    }
+
+    public void doesntContain() {
+        String str = "abcde";
+        assert !str.contains("cda");
+    }
+
+    public void noprop(String str) {
+        assert str.contains("cd");
+    }
+
+    public void nondetArg(String str) {
+        assert "dave".contains(str);
+    }
+
+    public void noPi() {
+        assert !"dave".contains("π");
+    }
+
+    public void pi() {
+        assert "dave_loves_π".contains("π");
+    }
+
+    public void alphanumeric() {
+        assert "ad672naksd3".contains("72n");
+    }
+}

jbmc/regression/jbmc-strings/ConstantEvaluationContains/Main.java

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.alphanumeric --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationContains/alphanumeric.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.contains --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationContains/contains.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.doesntContain --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationContains/doesntContain.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.noPi --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationContains/noPi.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.nondetArg --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationContains/nondetArg.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.noprop --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationContains/noprop.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.pi --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--