Merge pull request #2679 from tautschnig/version-string

Refine test patterns to avoid spurious matches

Author: Daniel Kroening

jbmc/regression/jbmc/reachability-slice/test.desc

@@ -1,11 +1,11 @@
 CORE symex-driven-lazy-loading-expected-failure
 A.class
 --reachability-slice --show-goto-functions --property 'java::A.foo:(I)V.coverage.3' --cover location
-1001
+= \(int\)\(short\)1001
 --
-1003
-1004
-1005
+= \(int\)\(short\)1003
+= \(int\)\(short\)1004
+= \(int\)\(short\)1005
 --
 Note: 1002 might and might not be removed, based on where the assertion for coverage resides.
 At the time of writing of this test, 1002 is removed.

jbmc/regression/jbmc/reachability-slice/test2.desc

@@ -1,11 +1,11 @@
 CORE symex-driven-lazy-loading-expected-failure
 A.class
 --reachability-slice-fb --show-goto-functions --property 'java::A.foo:(I)V.coverage.4' --cover location
-1001
-1002
-1003
-1005
+= \(int\)\(short\)1001
+= \(int\)\(short\)1002
+= \(int\)\(short\)1003
+= \(int\)\(short\)1005
 --
-1004
+= \(int\)\(short\)1004
 --
 Doesn't work with symex-driven lazy loading because the reachability slicer is a whole-program pass.

jbmc/regression/jbmc/reachability-slice/test3.desc

@@ -1,11 +1,11 @@
 CORE symex-driven-lazy-loading-expected-failure
 A.class
 --reachability-slice --show-goto-functions --cover location
-1001
-1002
-1003
-1004
-1005
+= \(int\)\(short\)1001
+= \(int\)\(short\)1002
+= \(int\)\(short\)1003
+= \(int\)\(short\)1004
+= \(int\)\(short\)1005
 --
 --
 Doesn't work with symex-driven lazy loading because the reachability slicer is a whole-program pass.

regression/cbmc/reachability-slice/test.desc

@@ -1,9 +1,9 @@
 CORE
 test.c
 --reachability-slice --show-goto-functions --cover location --property foo.coverage.2
-1001
+= 1001
 --
-1004
-1005
+= 1004
+= 1005
 --
 We do not include 1002 and 1003, whether this is hit depends on where assertion is put

regression/cbmc/reachability-slice/test2.desc

@@ -1,9 +1,9 @@
 CORE
 test.c
 --reachability-slice-fb --show-goto-functions --cover location --property foo.coverage.2
-1001
-1002
-1003
-1005
+= 1001
+= 1002
+= 1003
+= 1005
 --
-1004
+= 1004

regression/cbmc/reachability-slice/test3.desc

@@ -1,10 +1,10 @@
 CORE
 test.c
 --reachability-slice --show-goto-functions --cover location
-1001
-1002
-1003
-1004
+= 1001
+= 1002
+= 1003
+= 1004
 --
 --
 We do not include 1005 since it might or might not be present based on where the assertion is in the block.