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
void add_dependencies(const cfgt::nodet &node, queuet &queue, const dependence_grapht &dep_graph, const dep_node_to_cfgt &dep_node_to_cfg)
void slice(symex_target_equationt &equation)
const std::string & id2string(const irep_idt &d)
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
Goto Programs with Functions.
std::unordered_map< irep_idt, queuet > decl_deadt
properties_criteriont(const std::list< std::string > &properties)
const irep_idt target_function
std::stack< cfgt::entryt > queuet
const std::list< std::string > & property_ids
cfg_base_nodet< cfg_nodet, goto_programt::const_targett > nodet
std::map< irep_idt, cfg_post_dominatorst > post_dominators_mapt
instructionst::const_iterator const_targett
void fixedpoint(goto_functionst &goto_functions, queuet &queue, jumpst &jumps, decl_deadt &decl_dead, const dependence_grapht &dep_graph)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
std::list< cfgt::entryt > jumpst
A collection of goto functions.
virtual bool operator()(goto_programt::const_targett target) const
void add_decl_dead(const cfgt::nodet &node, queuet &queue, decl_deadt &decl_dead)
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
in_function_criteriont(const std::string &function_name)
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_baset< cfg_nodet > cfgt
void add_jumps(queuet &queue, jumpst &jumps, const dependence_grapht::post_dominators_mapt &post_dominators)
std::vector< cfgt::entryt > dep_node_to_cfgt
void operator()(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
virtual bool operator()(goto_programt::const_targett target) const