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;
65 typedef std::unordered_map<irep_idt, queuet, irep_id_hash>
decl_deadt;
71 decl_deadt &decl_dead,
78 const dep_node_to_cfgt &dep_node_to_cfg);
88 decl_deadt &decl_dead);
100 #ifdef DEBUG_FULL_SLICERT 101 cfg[entry].required_by.insert(reason->location_number);
112 return target->is_assert();
120 const std::list<std::string> &properties):
121 property_ids(properties)
127 if(!target->is_assert())
130 const std::string &p_id=
131 id2string(target->source_location.get_property_id());
133 for(std::list<std::string>::const_iterator
134 it=property_ids.begin();
135 it!=property_ids.end();
147 #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.
virtual bool operator()(goto_programt::const_targett target)
properties_criteriont(const std::list< std::string > &properties)
instructionst::const_iterator const_targett
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
void fixedpoint(goto_functionst &goto_functions, queuet &queue, jumpst &jumps, decl_deadt &decl_dead, const dependence_grapht &dep_graph)
std::list< cfgt::entryt > jumpst
void add_decl_dead(const cfgt::nodet &node, queuet &queue, decl_deadt &decl_dead)
void add_function_calls(const cfgt::nodet &node, queuet &queue, const goto_functionst &goto_functions)
std::unordered_map< irep_idt, queuet, irep_id_hash > decl_deadt
void add_to_queue(queuet &queue, const cfgt::entryt &entry, goto_programt::const_targett reason)
cfg_baset< cfg_nodet > cfgt
void operator()(goto_functionst &goto_functions, const namespacet &ns, slicing_criteriont &criterion)
virtual bool operator()(goto_programt::const_targett target)
void add_jumps(queuet &queue, jumpst &jumps, const dependence_grapht::post_dominators_mapt &post_dominators)
std::vector< cfgt::entryt > dep_node_to_cfgt