Add tests for the use of string dependencies

romainbrenguier · romainbrenguier · commit a45c64f5edc6 · 2018-03-25T11:15:06.000+01:00
This tests, check that only constraints for the string operation that
matters are added to the list of axioms of the string solver.
In the example added here, the solver would previously consider 11
constraints, but now only 3, and still finds the correct result.
diff --git a/regression/jbmc-strings/StringDependencies/Test.class b/regression/jbmc-strings/StringDependencies/Test.class
diff --git a/regression/jbmc-strings/StringDependencies/Test.java b/regression/jbmc-strings/StringDependencies/Test.java
@@ -0,0 +1,22 @@
+class Test {
+    void test(String s) {
+        // Filter
+        if(s == null)
+            return;
+
+        // Act
+
+        // this matters for the final test
+        String t = s.concat("_foo");
+
+        // these should be ignored by the solver as they
+        // do not matter for the final test
+        String u = s.concat("_bar");
+        String v = s.concat("_baz");
+        String w = s.concat("_fiz");
+        String x = s.concat("_buz");
+
+        // Assert
+        assert t.endsWith("foo");
+    }
+}
diff --git a/regression/jbmc-strings/StringDependencies/test.desc b/regression/jbmc-strings/StringDependencies/test.desc
@@ -0,0 +1,12 @@
+CORE
+Test.class
+--refine-strings --string-max-length 1000 --string-max-input-length 100 --verbosity 10 Test.class --function Test.test
+^EXIT=0$
+^SIGNAL=0$
+assertion at file Test.java line 20 .*: SUCCESS
+string_refinement::check_axioms: 3 universal axioms
+--
+--
+We check there are exactly 3 universal formulas considered by the solver (2 for
+`t = s.concat("_foo")` and 1 for `t.endsWith("foo")`).
+The other concatenations should be ignored.
