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:]]*
56 #ifdef DEBUG_FULL_SLICERT
57 std::set<unsigned> required_by;
65 typedef std::stack<cfgt::entryt>
queuet;
66 typedef std::list<cfgt::entryt>
jumpst;
102 #ifdef DEBUG_FULL_SLICERT
103 cfg[entry].required_by.insert(reason->location_number);
117 return target->is_assert();
143 const std::list<std::string> &properties):
151 if(!target->is_assert())
154 const std::string &p_id =
155 id2string(target->source_location().get_property_id());
157 for(std::list<std::string>::const_iterator
void slice(symex_bmct &symex, symex_target_equationt &symex_target_equation, const namespacet &ns, const optionst &options, ui_message_handlert &ui_message_handler)
virtual bool operator()(const irep_idt &, goto_programt::const_targett target) const
base_grapht::node_indext entryt
std::map< irep_idt, cfg_post_dominatorst > post_dominators_mapt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void add_function_calls(const cfgt::nodet &node, queuet &queue, const goto_functionst &goto_functions)
std::list< cfgt::entryt > jumpst
void add_to_queue(queuet &queue, const cfgt::entryt &entry, goto_programt::const_targett reason)
std::unordered_map< irep_idt, queuet > decl_deadt
void add_dependencies(const cfgt::nodet &node, queuet &queue, const dependence_grapht &dep_graph, const dep_node_to_cfgt &dep_node_to_cfg)
cfg_baset< cfg_nodet > cfgt
void fixedpoint(goto_functionst &goto_functions, queuet &queue, jumpst &jumps, decl_deadt &decl_dead, const dependence_grapht &dep_graph)
void add_decl_dead(const cfgt::nodet &node, queuet &queue, decl_deadt &decl_dead)
void operator()(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion, message_handlert &message_handler)
std::stack< cfgt::entryt > queuet
std::vector< cfgt::entryt > dep_node_to_cfgt
void add_jumps(queuet &queue, jumpst &jumps, const dependence_grapht::post_dominators_mapt &post_dominators)
A collection of goto functions.
instructionst::const_iterator const_targett
virtual bool operator()(const irep_idt &function_id, goto_programt::const_targett) const
const irep_idt target_function
in_function_criteriont(const std::string &function_name)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
properties_criteriont(const std::list< std::string > &properties)
const std::list< std::string > & property_ids
virtual bool operator()(const irep_idt &, goto_programt::const_targett target) const
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
Goto Programs with Functions.
const std::string & id2string(const irep_idt &d)