Go to the documentation of this file.
12 #ifndef CPROVER_GOTO_INSTRUMENT_FULL_SLICER_CLASS_H
13 #define CPROVER_GOTO_INSTRUMENT_FULL_SLICER_CLASS_H
28 useful
for debugging (remove NOLINT)
29 goto-instrument --full-
slice a.out c.out
30 goto-instrument --show-
goto-functions c.out > c.goto
31 echo
'digraph g {' > c.dot ; cat c.goto | \
32 NOLINT(*) grep 'ins:[[:digit:]]\+ req by' | grep '^[[:space:]]*
54 #ifdef DEBUG_FULL_SLICERT
55 std::set<unsigned> required_by;
63 typedef std::stack<cfgt::entryt>
queuet;
64 typedef std::list<cfgt::entryt>
jumpst;
100 #ifdef DEBUG_FULL_SLICERT
101 cfg[entry].required_by.insert(reason->location_number);
114 return target->is_assert();
139 const std::list<std::string> &properties):
146 if(!target->is_assert())
149 const std::string &p_id=
150 id2string(target->source_location.get_property_id());
152 for(std::list<std::string>::const_iterator
166 #endif // CPROVER_GOTO_INSTRUMENT_FULL_SLICER_CLASS_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
virtual bool operator()(goto_programt::const_targett target) const
std::stack< cfgt::entryt > queuet
virtual bool operator()(goto_programt::const_targett target) const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void add_dependencies(const cfgt::nodet &node, queuet &queue, const dependence_grapht &dep_graph, const dep_node_to_cfgt &dep_node_to_cfg)
const std::string & id2string(const irep_idt &d)
properties_criteriont(const std::list< std::string > &properties)
std::map< irep_idt, cfg_post_dominatorst > post_dominators_mapt
std::vector< cfgt::entryt > dep_node_to_cfgt
void add_decl_dead(const cfgt::nodet &node, queuet &queue, decl_deadt &decl_dead)
cfg_baset< cfg_nodet > cfgt
void operator()(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
void add_jumps(queuet &queue, jumpst &jumps, const dependence_grapht::post_dominators_mapt &post_dominators)
A collection of goto functions.
in_function_criteriont(const std::string &function_name)
virtual bool operator()(goto_programt::const_targett target) const
void fixedpoint(goto_functionst &goto_functions, queuet &queue, jumpst &jumps, decl_deadt &decl_dead, const dependence_grapht &dep_graph)
const irep_idt target_function
const std::list< std::string > & property_ids
instructionst::const_iterator const_targett
std::list< cfgt::entryt > jumpst
std::unordered_map< irep_idt, queuet > decl_deadt
void add_function_calls(const cfgt::nodet &node, queuet &queue, const goto_functionst &goto_functions)
void add_to_queue(queuet &queue, const cfgt::entryt &entry, goto_programt::const_targett reason)
cfg_base_nodet< cfg_nodet, goto_programt::const_targett > nodet
void slice(symex_target_equationt &equation)