|
| dependence_grapht (const namespacet &_ns) |
|
void | initialize (const goto_functionst &goto_functions) |
| Initialize all the abstract states for a whole program. More...
|
|
void | initialize (const goto_programt &goto_program) |
| Initialize all the abstract states for a single function. More...
|
|
void | finalize () |
| Override this to add a cleanup or post-processing step after fixedpoint has run. More...
|
|
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) |
| Get the state for the given location, creating it in a default way if it doesn't exist. More...
|
|
| ait () |
|
dep_graph_domaint & | operator[] (locationt l) |
|
const dep_graph_domaint & | operator[] (locationt l) const |
|
std::unique_ptr< statet > | abstract_state_before (locationt t) const override |
| Get a copy of the abstract state before the given instruction, without needing to know what kind of domain or history is used. More...
|
|
void | clear () override |
| Reset the abstract state. More...
|
|
| ai_baset () |
|
virtual | ~ai_baset () |
|
void | operator() (const irep_idt &function_identifier, const goto_programt &goto_program, const namespacet &ns) |
| Run abstract interpretation on a single function. More...
|
|
void | operator() (const goto_functionst &goto_functions, const namespacet &ns) |
| Run abstract interpretation on a whole program. More...
|
|
void | operator() (const goto_modelt &goto_model) |
| Run abstract interpretation on a whole program. More...
|
|
void | operator() (const irep_idt &function_identifier, const goto_functionst::goto_functiont &goto_function, const namespacet &ns) |
| Run abstract interpretation on a single function. More...
|
|
virtual std::unique_ptr< statet > | abstract_state_after (locationt l) const |
| Get a copy of the abstract state after the given instruction, without needing to know what kind of domain or history is used. More...
|
|
virtual void | output (const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const |
| Output the abstract states for a whole program. More...
|
|
void | output (const goto_modelt &goto_model, std::ostream &out) const |
| Output the abstract states for a whole program. More...
|
|
void | output (const namespacet &ns, const goto_programt &goto_program, std::ostream &out) const |
| Output the abstract states for a function. More...
|
|
void | output (const namespacet &ns, const goto_functionst::goto_functiont &goto_function, std::ostream &out) const |
| Output the abstract states for a function. More...
|
|
virtual jsont | output_json (const namespacet &ns, const goto_functionst &goto_functions) const |
| Output the abstract states for the whole program as JSON. More...
|
|
jsont | output_json (const goto_modelt &goto_model) const |
| Output the abstract states for a whole program as JSON. More...
|
|
jsont | output_json (const namespacet &ns, const goto_programt &goto_program) const |
| Output the abstract states for a single function as JSON. More...
|
|
jsont | output_json (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const |
| Output the abstract states for a single function as JSON. More...
|
|
virtual xmlt | output_xml (const namespacet &ns, const goto_functionst &goto_functions) const |
| Output the abstract states for the whole program as XML. More...
|
|
xmlt | output_xml (const goto_modelt &goto_model) const |
| Output the abstract states for the whole program as XML. More...
|
|
xmlt | output_xml (const namespacet &ns, const goto_programt &goto_program) const |
| Output the abstract states for a single function as XML. More...
|
|
xmlt | output_xml (const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const |
| Output the abstract states for a single function as XML. More...
|
|
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) |
|
std::vector< node_indext > | get_reachable (node_indext src, bool forwards) const |
| Run depth-first search on the graph, starting from a single source node. More...
|
|
std::vector< node_indext > | get_reachable (const std::vector< node_indext > &src, bool forwards) const |
| Run depth-first search on the graph, starting from multiple source nodes. More...
|
|
void | disconnect_unreachable (node_indext src) |
| Removes any edges between nodes in a graph that are unreachable from a given start node. More...
|
|
void | disconnect_unreachable (const std::vector< node_indext > &src) |
| Removes any edges between nodes in a graph that are unreachable from a vector of start nodes. More...
|
|
std::vector< typename dep_nodet ::node_indext > | depth_limited_search (typename dep_nodet ::node_indext src, std::size_t limit) const |
| Run recursive depth-limited search on the graph, starting from multiple source nodes, to find the nodes reachable within n steps. More...
|
|
std::vector< typename dep_nodet ::node_indext > | depth_limited_search (std::vector< typename dep_nodet ::node_indext > &src, std::size_t limit) const |
| Run recursive depth-limited search on the graph, starting from multiple source nodes, to find the nodes reachable within n steps. More...
|
|
void | make_chordal () |
| Ensure a graph is chordal (contains no 4+-cycles without an edge crossing the cycle) by adding extra edges. More...
|
|
std::size_t | connected_subgraphs (std::vector< node_indext > &subgraph_nr) |
| Find connected subgraphs in an undirected graph. More...
|
|
std::size_t | SCCs (std::vector< node_indext > &subgraph_nr) const |
| Computes strongly-connected components of a graph and yields a vector expressing a mapping from nodes to components indices. More...
|
|
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...
|
|
std::vector< node_indext > | get_successors (const node_indext &n) const |
|
void | output_dot (std::ostream &out) const |
|
void | for_each_successor (const node_indext &n, std::function< void(const node_indext &)> f) const |
|
|
typedef std::unordered_map< locationt, dep_graph_domaint, const_target_hash, pointee_address_equalt > | state_mapt |
|
typedef std::map< unsigned, locationt > | working_sett |
| The work queue, sorted by location number. More...
|
|
const statet & | find_state (locationt l) const override |
| Get the state for the given location if it already exists; throw an exception if it doesn't. More...
|
|
bool | merge (const statet &src, locationt from, locationt to) override |
|
std::unique_ptr< statet > | make_temporary_state (const statet &s) override |
| Make a copy of a state. More...
|
|
void | fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) override |
|
virtual void | initialize (const goto_functionst::goto_functiont &goto_function) |
| Initialize all the abstract states for a single function. More...
|
|
void | entry_state (const goto_programt &goto_program) |
| Set the abstract state of the entry location of a single function to the entry state required by the analysis. More...
|
|
void | entry_state (const goto_functionst &goto_functions) |
| Set the abstract state of the entry location of a whole program to the entry state required by the analysis. More...
|
|
virtual void | output (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier, std::ostream &out) const |
| Output the abstract states for a single function. More...
|
|
virtual jsont | output_json (const namespacet &ns, const goto_programt &goto_program, const irep_idt &identifier) const |
| Output the abstract states 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 abstract states for a single function as XML. More...
|
|
locationt | get_next (working_sett &working_set) |
| Get the next location from the work queue. More...
|
|
void | put_in_working_set (working_sett &working_set, locationt l) |
|
bool | fixedpoint (const irep_idt &function_identifier, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns) |
| Run the fixedpoint algorithm until it reaches a fixed point. More...
|
|
void | sequential_fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) |
|
void | concurrent_fixedpoint (const goto_functionst &goto_functions, const namespacet &ns) |
|
bool | visit (const irep_idt &function_identifier, locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns) |
| Perform one step of abstract interpretation from location l Depending on the instruction type it may compute a number of "edges" or applications of the abstract transformer. More...
|
|
bool | do_function_call_rec (const irep_idt &calling_function_identifier, 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 (const irep_idt &calling_function_identifier, 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 |
|
std::vector< typename dep_nodet ::node_indext > | depth_limited_search (std::vector< typename dep_nodet ::node_indext > &src, std::size_t limit, std::vector< bool > &visited) const |
| Run recursive depth-limited search on the graph, starting. More...
|
|
void | tarjan (class tarjant &t, node_indext v) const |
|