diff --git a/CHANGELOG b/CHANGELOG index 14fd89ae52c..1718d32243d 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,6 +1,8 @@ 5.8 === +* GOTO-INSTRUMENT: --reachability-slice can be used with --property to slice + down to a single property only. * GOTO-INSTRUMENT: New option --list-calls-args * GOTO-INSTRUMENT: New option --print-path-lenghts * GOTO-ANALYZER: New option --unreachable-functions, --reachable-functions diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp index f7b42a0af3c..887805ad80a 100644 --- a/src/goto-instrument/full_slicer.cpp +++ b/src/goto-instrument/full_slicer.cpp @@ -13,9 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include - -#include "full_slicer.h" #include "full_slicer_class.h" /*******************************************************************\ diff --git a/src/goto-instrument/full_slicer_class.h b/src/goto-instrument/full_slicer_class.h index 4495fa95246..93894513f57 100644 --- a/src/goto-instrument/full_slicer_class.h +++ b/src/goto-instrument/full_slicer_class.h @@ -16,7 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include + +#include "full_slicer.h" // #define DEBUG_FULL_SLICERT #if 0 @@ -30,8 +32,6 @@ echo 'digraph g {' > c.dot ; cat c.goto | \ dot -Tpdf -oc-red.pdf c-red.dot #endif -class dependence_grapht; - /*******************************************************************\ Class: full_slicert diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 401916069bd..66421b2e1e1 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1502,7 +1502,10 @@ void goto_instrument_parse_optionst::instrument_goto_program() if(cmdline.isset("reachability-slice")) { status() << "Performing a reachability slice" << eom; - reachability_slicer(goto_functions); + if(cmdline.isset("property")) + reachability_slicer(goto_functions, cmdline.get_values("property")); + else + reachability_slicer(goto_functions); } // full slice? diff --git a/src/goto-instrument/reachability_slicer.cpp b/src/goto-instrument/reachability_slicer.cpp index 231ae40cde9..073f9284add 100644 --- a/src/goto-instrument/reachability_slicer.cpp +++ b/src/goto-instrument/reachability_slicer.cpp @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include "full_slicer_class.h" #include "reachability_slicer.h" #include "reachability_slicer_class.h" @@ -29,7 +30,8 @@ Function: reachability_slicert::fixedpoint_assertions \*******************************************************************/ void reachability_slicert::fixedpoint_assertions( - const is_threadedt &is_threaded) + const is_threadedt &is_threaded, + slicing_criteriont &criterion) { queuet queue; @@ -37,7 +39,7 @@ void reachability_slicert::fixedpoint_assertions( e_it=cfg.entry_map.begin(); e_it!=cfg.entry_map.end(); e_it++) - if(e_it->first->is_assert() || + if(criterion(e_it->first) || is_threaded(e_it->first)) queue.push(e_it->second); @@ -77,7 +79,7 @@ Function: reachability_slicert::slice void reachability_slicert::slice(goto_functionst &goto_functions) { // now replace those instructions that do not reach any assertions - // by self-loops + // by assume(false) Forall_goto_functions(f_it, goto_functions) if(f_it->second.body_available()) @@ -87,7 +89,7 @@ void reachability_slicert::slice(goto_functionst &goto_functions) const cfgt::nodet &e=cfg[cfg.entry_map[i_it]]; if(!e.reaches_assertion && !i_it->is_end_function()) - i_it->make_goto(i_it); + i_it->make_assumption(false_exprt()); } // replace unreachable code by skip @@ -113,5 +115,28 @@ Function: reachability_slicer void reachability_slicer(goto_functionst &goto_functions) { - reachability_slicert()(goto_functions); + reachability_slicert s; + assert_criteriont a; + s(goto_functions, a); +} + +/*******************************************************************\ + +Function: reachability_slicer + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void reachability_slicer( + goto_functionst &goto_functions, + const std::list &properties) +{ + reachability_slicert s; + properties_criteriont p(properties); + s(goto_functions, p); } diff --git a/src/goto-instrument/reachability_slicer.h b/src/goto-instrument/reachability_slicer.h index 7ce03a1d612..e45aa81f27e 100644 --- a/src/goto-instrument/reachability_slicer.h +++ b/src/goto-instrument/reachability_slicer.h @@ -13,4 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com void reachability_slicer(goto_functionst &goto_functions); +void reachability_slicer( + goto_functionst &goto_functions, + const std::list &properties); + #endif // CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_H diff --git a/src/goto-instrument/reachability_slicer_class.h b/src/goto-instrument/reachability_slicer_class.h index 85f1e62a345..224259b57cd 100644 --- a/src/goto-instrument/reachability_slicer_class.h +++ b/src/goto-instrument/reachability_slicer_class.h @@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +class slicing_criteriont; + /*******************************************************************\ Class: reachability_slicert @@ -25,11 +27,13 @@ Author: Daniel Kroening, kroening@kroening.com class reachability_slicert { public: - void operator()(goto_functionst &goto_functions) + void operator()( + goto_functionst &goto_functions, + slicing_criteriont &criterion) { cfg(goto_functions); is_threadedt is_threaded(goto_functions); - fixedpoint_assertions(is_threaded); + fixedpoint_assertions(is_threaded, criterion); slice(goto_functions); } @@ -48,7 +52,9 @@ class reachability_slicert typedef std::stack queuet; - void fixedpoint_assertions(const is_threadedt &is_threaded); + void fixedpoint_assertions( + const is_threadedt &is_threaded, + slicing_criteriont &criterion); void slice(goto_functionst &goto_functions); };