|
| | variable_sensitivity_dependence_grapht (const goto_functionst &goto_functions, const namespacet &_ns, variable_sensitivity_object_factory_ptrt object_factory, const vsd_configt &_configuration, message_handlert &message_handler) |
| |
| void | initialize (const irep_idt &function_id, 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 (vs_dep_edget::kindt kind, goto_programt::const_targett from, goto_programt::const_targett to) |
| |
| post_dominators_mapt & | cfg_post_dominators () |
| |
| | ai_three_way_merget (std::unique_ptr< ai_history_factory_baset > &&hf, std::unique_ptr< ai_domain_factory_baset > &&df, std::unique_ptr< ai_storage_baset > &&st, message_handlert &mh) |
| |
| | ai_recursive_interproceduralt (std::unique_ptr< ai_history_factory_baset > &&hf, std::unique_ptr< ai_domain_factory_baset > &&df, std::unique_ptr< ai_storage_baset > &&st, message_handlert &mh) |
| |
| | ai_baset (std::unique_ptr< ai_history_factory_baset > &&hf, std::unique_ptr< ai_domain_factory_baset > &&df, std::unique_ptr< ai_storage_baset > &&st, message_handlert &mh) |
| |
| virtual | ~ai_baset () |
| |
| void | operator() (const irep_idt &function_id, 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 abstract_goto_modelt &goto_model) |
| | Run abstract interpretation on a whole program. More...
|
| |
| void | operator() (const irep_idt &function_id, const goto_functionst::goto_functiont &goto_function, const namespacet &ns) |
| | Run abstract interpretation on a single function. More...
|
| |
| virtual ctrace_set_ptrt | abstract_traces_before (locationt l) const |
| | Returns all of the histories that have reached the start of the instruction. More...
|
| |
| virtual ctrace_set_ptrt | abstract_traces_after (locationt l) const |
| | Returns all of the histories that have reached the end of the instruction. More...
|
| |
| virtual cstate_ptrt | abstract_state_before (locationt l) const |
| | Get a copy of the abstract state before the given instruction, without needing to know what kind of domain or history is used. More...
|
| |
| virtual cstate_ptrt | 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 cstate_ptrt | abstract_state_before (const trace_ptrt &p) const |
| | The same interfaces but with histories. More...
|
| |
| virtual cstate_ptrt | abstract_state_after (const trace_ptrt &p) const |
| |
| virtual void | clear () |
| | Reset the abstract state. More...
|
| |
| virtual void | output (const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const |
| | Output the abstract states for a single function. More...
|
| |
| virtual jsont | output_json (const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program) const |
| | Output the abstract states for a single function as JSON. More...
|
| |
| virtual xmlt | output_xml (const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program) const |
| | Output the abstract states for a single function as XML. 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_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 (arguments &&... values) |
| |
| 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 N::node_indext > | depth_limited_search (typename N::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 N::node_indext > | depth_limited_search (std::vector< typename N::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_predecessors (const node_indext &n) const |
| |
| std::vector< node_indext > | get_successors (const node_indext &n) const |
| |
| void | output_dot (std::ostream &out) const |
| |
| void | for_each_predecessor (const node_indext &n, std::function< void(const node_indext &)> f) const |
| |
| void | for_each_successor (const node_indext &n, std::function< void(const node_indext &)> f) const |
| |
|
| virtual statet & | get_state (locationt l) |
| |
| variable_sensitivity_dependence_domaint & | operator[] (locationt l) |
| |
| virtual statet & | get_state (trace_ptrt p) |
| | Get the state for the given history, creating it with the factory if it doesn't exist. More...
|
| |
| bool | visit_edge_function_call (const irep_idt &calling_function_id, trace_ptrt p_call, locationt l_return, const irep_idt &callee_function_id, working_sett &working_set, const goto_programt &callee, const goto_functionst &goto_functions, const namespacet &ns) override |
| |
| virtual void | initialize (const irep_idt &function_id, const goto_functionst::goto_functiont &goto_function) |
| | Initialize all the abstract states for a single function. More...
|
| |
| virtual void | initialize (const goto_functionst &goto_functions) |
| | Initialize all the abstract states for a whole program. More...
|
| |
| trace_ptrt | 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...
|
| |
| trace_ptrt | 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...
|
| |
| trace_ptrt | get_next (working_sett &working_set) |
| | Get the next location from the work queue. More...
|
| |
| void | put_in_working_set (working_sett &working_set, trace_ptrt t) |
| |
| virtual bool | fixedpoint (trace_ptrt starting_trace, const irep_idt &function_id, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns) |
| | Run the fixedpoint algorithm until it reaches a fixed point. More...
|
| |
| virtual void | fixedpoint (trace_ptrt starting_trace, const goto_functionst &goto_functions, const namespacet &ns) |
| |
| virtual bool | visit (const irep_idt &function_id, trace_ptrt p, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns) |
| | Perform one step of abstract interpretation from trace t Depending on the instruction type it may compute a number of "edges" or applications of the abstract transformer. More...
|
| |
| virtual bool | visit_function_call (const irep_idt &function_id, trace_ptrt p_call, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns) |
| |
| virtual bool | visit_end_function (const irep_idt &function_id, trace_ptrt p, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns) |
| |
| bool | visit_edge (const irep_idt &function_id, trace_ptrt p, const irep_idt &to_function_id, locationt to_l, trace_ptrt caller_history, const namespacet &ns, working_sett &working_set) |
| |
| virtual bool | merge (const statet &src, trace_ptrt from, trace_ptrt to) |
| | Merge the state src, flowing from tracet from to tracet to, into the state currently stored for tracet to. More...
|
| |
| virtual std::unique_ptr< statet > | make_temporary_state (const statet &s) |
| | Make a copy of a state. More...
|
| |
| virtual statet & | get_state (trace_ptrt p) |
| | Get the state for the given history, creating it with the factory if it doesn't exist. More...
|
| |
| void | shortest_path (node_indext src, node_indext dest, patht &path, bool non_trivial) const |
| |
| std::vector< typename N::node_indext > | depth_limited_search (std::vector< typename N::node_indext > &src, std::size_t limit, std::vector< bool > &visited) const |
| | Run recursive depth-limited search on the graph, starting from multiple source nodes, to find the nodes reachable within n steps. More...
|
| |
| void | tarjan (class tarjant &t, node_indext v) const |
| |
Inheritance diagram for variable_sensitivity_dependence_grapht: