Merge pull request diffblue#1965 from smowton/smowton/fix/reachability-slicer-incompatible-with-symex-driven-loading

Mark the new reachability-slicer incompatible with symex-driven loading

Author: smowton

regression/cbmc-java/reachability-slice/test.desc

@@ -1,4 +1,4 @@
-CORE
+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
@@ -9,3 +9,5 @@ A.class
 --
 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.
+
+Doesn't work with symex-driven lazy loading because the reachability slicer is a whole-program pass.

regression/cbmc-java/reachability-slice/test2.desc

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

regression/cbmc-java/reachability-slice/test3.desc

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

src/jbmc/jbmc_parse_options.cpp

@@ -385,7 +385,9 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
     for(const char *opt :
       { "nondet-static",
         "full-slice",
-        "lazy-methods" })
+        "lazy-methods",
+        "reachability-slice",
+        "reachability-slice-fb" })
     {
       if(cmdline.isset(opt))
       {