|
| dependence_grapht (const namespacet &_ns) |
|
void | initialize (const goto_functionst &goto_functions) |
|
void | initialize (const goto_programt &goto_program) |
|
void | add_dep (dep_edget::kindt kind, goto_programt::const_targett from, goto_programt::const_targett to) |
|
const post_dominators_mapt & | cfg_post_dominators () const |
|
const reaching_definitions_analysist & | reaching_definitions () const |
|
virtual statet & | get_state (goto_programt::const_targett l) |
|
| ait () |
|
dep_graph_domaint & | operator[] (locationt l) |
|
const dep_graph_domaint & | operator[] (locationt l) const |
|
void | clear () override |
|
| ai_baset () |
|
virtual | ~ai_baset () |
|
void | operator() (const goto_programt &goto_program, const namespacet &ns) |
|
void | operator() (const goto_functionst &goto_functions, const namespacet &ns) |
|
void | operator() (const goto_modelt &goto_model) |
|
void | operator() (const goto_functionst::goto_functiont &goto_function, const namespacet &ns) |
|
virtual void | output (const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const |
|
void | output (const goto_modelt &goto_model, std::ostream &out) const |
|
void | output (const namespacet &ns, const goto_programt &goto_program, std::ostream &out) const |
|
void | output (const namespacet &ns, const goto_functionst::goto_functiont &goto_function, std::ostream &out) const |
|
virtual jsont | output_json (const namespacet &ns, const goto_functionst &goto_functions) const |
| Output the domains for the whole program as JSON. More...
|
|
jsont | output_json (const goto_modelt &goto_model) const |
|
jsont | output_json (const namespacet &ns, const goto_programt &goto_program) const |
|
jsont | output_json (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const |
|
virtual xmlt | output_xml (const namespacet &ns, const goto_functionst &goto_functions) const |
| Output the domains for the whole program as XML. More...
|
|
xmlt | output_xml (const goto_modelt &goto_model) const |
|
xmlt | output_xml (const namespacet &ns, const goto_programt &goto_program) const |
|
xmlt | output_xml (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const |
|
node_indext | add_node () |
|
void | swap (grapht &other) |
|
bool | has_edge (node_indext i, node_indext j) const |
|
const nodet & | operator[] (node_indext n) const |
|
nodet & | operator[] (node_indext n) |
|
void | resize (node_indext s) |
|
std::size_t | size () const |
|
bool | empty () const |
|
const edgest & | in (node_indext n) const |
|
const edgest & | out (node_indext n) const |
|
void | add_edge (node_indext a, node_indext b) |
|
void | remove_edge (node_indext a, node_indext b) |
|
edget & | edge (node_indext a, node_indext b) |
|
void | add_undirected_edge (node_indext a, node_indext b) |
|
void | remove_undirected_edge (node_indext a, node_indext b) |
|
void | remove_in_edges (node_indext n) |
|
void | remove_out_edges (node_indext n) |
|
void | remove_edges (node_indext n) |
|
void | clear () |
|
void | shortest_path (node_indext src, node_indext dest, patht &path) const |
|
void | shortest_loop (node_indext node, patht &path) const |
|
void | visit_reachable (node_indext src) |
|
void | make_chordal () |
|
std::size_t | connected_subgraphs (std::vector< node_indext > &subgraph_nr) |
|
std::size_t | SCCs (std::vector< node_indext > &subgraph_nr) |
|
bool | is_dag () const |
|
std::list< node_indext > | topsort () const |
| Find a topological order of the nodes if graph is DAG, return empty list for non-DAG or empty graph. More...
|
|
void | output_dot (std::ostream &out) const |
|
void | output_dot_node (std::ostream &out, node_indext n) const |
|
|
typedef std::unordered_map< locationt, dep_graph_domaint, const_target_hash > | state_mapt |
|
typedef std::map< unsigned, locationt > | working_sett |
|
typedef std::set< irep_idt > | recursion_sett |
|
const statet & | find_state (locationt l) const override |
|
bool | merge (const statet &src, locationt from, locationt to) override |
|
statet * | make_temporary_state (const statet &s) override |
|
void | fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) override |
|
virtual void | initialize (const goto_functionst::goto_functiont &) |
|
void | entry_state (const goto_programt &) |
|
void | entry_state (const goto_functionst &) |
|
virtual void | output (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier, std::ostream &out) const |
|
virtual jsont | output_json (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier) const |
| Output the domains for a single function as JSON. More...
|
|
virtual xmlt | output_xml (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier) const |
| Output the domains for a single function as XML. More...
|
|
locationt | get_next (working_sett &working_set) |
|
void | put_in_working_set (working_sett &working_set, locationt l) |
|
bool | fixedpoint (const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns) |
|
void | sequential_fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) |
|
void | concurrent_fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) |
|
bool | visit (locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns) |
|
bool | do_function_call_rec (locationt l_call, locationt l_return, const exprt &function, const exprt::operandst &arguments, const goto_functionst &goto_functions, const namespacet &ns) |
|
bool | do_function_call (locationt l_call, locationt l_return, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, const namespacet &ns) |
|
void | shortest_path (node_indext src, node_indext dest, patht &path, bool non_trivial) const |
|
void | tarjan (class tarjant &t, node_indext v) |
|
Definition at line 150 of file dependence_graph.h.