From e25a7ac32b684fcd794cd580966dfe4195de36c2 Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Fri, 23 Mar 2018 10:26:37 +0000
Subject: [PATCH] Mark the new reachability-slicer incompatible with
 symex-driven loading

The new slicer is structured as a whole-program pass, so it can't operate when functions
are being produced one at a time as symex explores the target program.
---
 regression/cbmc-java/reachability-slice/test.desc  | 4 +++-
 regression/cbmc-java/reachability-slice/test2.desc | 4 +++-
 regression/cbmc-java/reachability-slice/test3.desc | 5 ++++-
 src/jbmc/jbmc_parse_options.cpp                    | 4 +++-
 4 files changed, 13 insertions(+), 4 deletions(-)

diff --git a/regression/cbmc-java/reachability-slice/test.desc b/regression/cbmc-java/reachability-slice/test.desc
index 972f34bca71..a5f7064d5f9 100644
--- a/regression/cbmc-java/reachability-slice/test.desc
+++ b/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.
diff --git a/regression/cbmc-java/reachability-slice/test2.desc b/regression/cbmc-java/reachability-slice/test2.desc
index 7bb351660bc..d8eea80d626 100644
--- a/regression/cbmc-java/reachability-slice/test2.desc
+++ b/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.
diff --git a/regression/cbmc-java/reachability-slice/test3.desc b/regression/cbmc-java/reachability-slice/test3.desc
index 271adbc2f0b..8c84468ecc0 100644
--- a/regression/cbmc-java/reachability-slice/test3.desc
+++ b/regression/cbmc-java/reachability-slice/test3.desc
@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 A.class
 --reachability-slice --show-goto-functions --cover location
 1001
@@ -6,3 +6,6 @@ A.class
 1003
 1004
 1005
+--
+--
+Doesn't work with symex-driven lazy loading because the reachability slicer is a whole-program pass.
diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp
index 42ef9afee20..0cd241a8cad 100644
--- a/src/jbmc/jbmc_parse_options.cpp
+++ b/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))
       {