12#ifndef CPROVER_GOTO_PROGRAMS_CFG_H
13#define CPROVER_GOTO_PROGRAMS_CFG_H
26template<
class T,
typename I>
54 return t->location_number;
111 template <
typename U>
129 auto e=
data.insert(std::make_pair(t, 0));
134 return e.first->second;
146 template <
class Iter>
210 std::vector<goto_programt::const_targett> possible_keys;
211 for(
const auto &id_and_function : goto_functions.
function_map)
213 const auto &instructions = id_and_function.second.body.instructions;
214 possible_keys.reserve(possible_keys.size() + instructions.size());
215 for(
auto it = instructions.begin(); it != instructions.end(); ++it)
216 possible_keys.push_back(it);
218 entry_map.setup_for_keys(possible_keys.begin(), possible_keys.end());
225 std::vector<goto_programt::const_targett> possible_keys;
226 const auto &instructions = goto_program.instructions;
227 possible_keys.reserve(instructions.size());
228 for(
auto it = instructions.begin(); it != instructions.end(); ++it)
229 possible_keys.push_back(it);
230 entry_map.setup_for_keys(possible_keys.begin(), possible_keys.end());
266 return program.instructions.begin();
270 return --program.instructions.end();
274 return program.instructions.empty();
314template<
class T,
typename P,
typename I>
331template<
class T,
typename P,
typename I>
344 for(
const auto &t : instruction.
targets)
349template<
class T,
typename P,
typename I>
359template<
class T,
typename P,
typename I>
370template<
class T,
typename P,
typename I>
386template<
class T,
typename P,
typename I>
396 if(function.
id()!=ID_symbol)
402 goto_functionst::function_mapt::const_iterator f_it=
406 f_it->second.body_available())
410 f_it->second.body.instructions.begin();
413 f_it->second.body.instructions.end();
436template<
class T,
typename P,
typename I>
446 if(function.
id()!=ID_symbol)
453template<
class T,
typename P,
typename I>
461 (*this)[entry].PC=PC;
466 switch(instruction.
type())
528template<
class T,
typename P,
typename I>
534 it!=goto_program.instructions.end();
539template<
class T,
typename P,
typename I>
545 if(gf_entry.second.body_available())
const_iterator cend() const
const_iterator find(U &&u) const
grapht< cfg_base_nodet< T, I > > & container
entry_mapt(grapht< cfg_base_nodet< T, I > > &_container)
dense_integer_mapt< goto_programt::const_targett, entryt, cfg_instruction_to_dense_integert< goto_programt::const_targett > > data_typet
void setup_for_keys(Iter begin, Iter end)
entryt & operator[](const goto_programt::const_targett &t)
entryt & at(const goto_programt::const_targett &t)
data_typet::iterator iterator
data_typet::const_iterator const_iterator
const_iterator begin() const
const entryt & at(const goto_programt::const_targett &t) const
const_iterator cbegin() const
const_iterator end() const
const entry_mapt & entries() const
Get a map from program points to their corresponding node indices.
void compute_edges(const goto_functionst &goto_functions, P &goto_program)
base_grapht::node_indext entryt
virtual void compute_edges_catch(const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, entryt &entry)
static I get_first_node(P &program)
static I get_last_node(P &program)
virtual void compute_edges_function_call(const goto_functionst &goto_functions, const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, entryt &entry)
void compute_edges(const goto_functionst &goto_functions)
virtual void compute_edges_start_thread(const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, entryt &entry)
nodet & get_node(const goto_programt::const_targett &program_point)
Get the CFG graph node relating to program_point.
void operator()(P &goto_program)
entryt get_node_index(const goto_programt::const_targett &program_point) const
Get the graph node index for program_point.
void operator()(const goto_functionst &goto_functions)
grapht< cfg_base_nodet< cfg_nodet, goto_programt::const_targett > > base_grapht
void compute_edges(const goto_functionst &goto_functions, const goto_programt &goto_program, I PC)
const nodet & get_node(const goto_programt::const_targett &program_point) const
Get the CFG graph node relating to program_point.
virtual void compute_edges_throw(const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, entryt &entry)
virtual void compute_edges_goto(const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, entryt &entry)
static bool nodes_empty(P &program)
Functor to convert cfg nodes into dense integers, used by cfg_baset.
std::size_t operator()(const goto_programt::const_targett &t) const
std::size_t operator()(T &&t) const
virtual void compute_edges_start_thread(const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, typename cfg_baset< T, P, I >::entryt &entry)
A map type that is backed by a vector, which relies on the ability to (a) see the keys that might be ...
iterator_templatet< typename backing_storet::const_iterator, const typename backing_storet::value_type > const_iterator
iterator_templatet< typename backing_storet::iterator, typename backing_storet::value_type > iterator
Base class for all expressions.
bool is_true() const
Return whether the expression is a constant representing true.
bool is_false() const
Return whether the expression is a constant representing false.
A collection of goto functions.
function_mapt function_map
This class represents an instruction in the GOTO intermediate representation.
targetst targets
The list of successor instructions.
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
const exprt & condition() const
Get the condition of gotos, assume, assert.
const_targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
goto_program_instruction_typet type() const
What kind of instruction?
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
instructionst::const_iterator const_targett
This class represents a node in a directed graph.
std::map< node_indext, edget > edgest
A generic directed graph with a parametric node type.
nodet::node_indext node_indext
void add_edge(node_indext a, node_indext b)
Identity functor. When we use C++20 this can be replaced with std::identity.
const irep_idt & id() const
virtual void compute_edges_function_call(const goto_functionst &goto_functions, const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, typename cfg_baset< T, P, I >::entryt &entry)
const irep_idt & get_identifier() const
Goto Programs with Functions.
A Template Class for Graphs.
#define UNREACHABLE
This should be used to mark dead code.
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
graph_nodet< empty_edget >::edgest edgest
graph_nodet< empty_edget >::edget edget