Merge pull request #2914 from polgreen/check_slicer_has_property

Throw error if reachability slicer has no slicing criteria

Author: tautschnig

regression/goto-instrument/slicing_criterion1/main.c

@@ -0,0 +1,8 @@
+void a()
+{
+}
+
+int main()
+{
+  a();
+}

regression/goto-instrument/slicing_criterion1/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+--reachability-slice
+^Reason: no slicing criterion found$
+^EXIT=1$
+^SIGNAL=0$

regression/goto-instrument/slicing_criterion2/main.c

@@ -0,0 +1,9 @@
+void a()
+{
+  __CPROVER_assert(0, "");
+}
+
+int main()
+{
+  a();
+}

regression/goto-instrument/slicing_criterion2/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+--reachability-slice --property property-name-with-typo
+^Reason: no slicing criterion found$
+^EXIT=1$
+^SIGNAL=0$

src/goto-instrument/reachability_slicer.cpp

@@ -22,7 +22,8 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/remove_skip.h>
 #include <goto-programs/remove_unreachable.h>
 
-#include "util/message.h"
+#include <util/exception_utils.h>
+#include <util/message.h>
 
 #include "full_slicer_class.h"
 #include "reachability_slicer_class.h"
@@ -46,6 +47,14 @@ reachability_slicert::get_sources(
       sources.push_back(e_it.second);
   }
 
+  if(sources.empty())
+  {
+    throw invalid_command_line_argument_exceptiont{
+      "no slicing criterion found",
+      "--property",
+      "provide at least one property using --property <property>"};
+  }
+
   return sources;
 }