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);
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);
266 return program.instructions.begin();
270 return --program.instructions.end();
274 return program.instructions.empty();
314template<
class T,
typename P,
typename I>
325 this->add_edge(entry, entry_map[next_PC]);
328 this->add_edge(entry, entry_map[instruction.
get_target()]);
331template<
class T,
typename P,
typename I>
339 this->add_edge(entry, entry_map[next_PC]);
344 for(
const auto &t : instruction.
targets)
346 this->add_edge(entry, entry_map[t]);
349template<
class T,
typename P,
typename I>
359template<
class T,
typename P,
typename I>
367 this->add_edge(entry, entry_map[next_PC]);
370template<
class T,
typename P,
typename I>
383 this->add_edge(entry, this->entry_map[instruction.
get_target()]);
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();
420 this->add_edge(entry, entry_map[i_it]);
424 this->add_edge(entry_map[last_it], entry_map[next_PC]);
429 this->add_edge(entry, entry_map[next_PC]);
433 this->add_edge(entry, entry_map[next_PC]);
436template<
class T,
typename P,
typename I>
446 if(function.
id()!=ID_symbol)
450 this->add_edge(entry, this->entry_map[next_PC]);
453template<
class T,
typename P,
typename I>
460 entryt entry=entry_map[PC];
461 (*this)[entry].PC=PC;
466 switch(instruction.
type())
469 compute_edges_goto(goto_program, instruction, next_PC, entry);
473 compute_edges_catch(goto_program, instruction, next_PC, entry);
477 compute_edges_throw(goto_program, instruction, next_PC, entry);
481 compute_edges_start_thread(
489 compute_edges_function_call(
518 this->add_edge(entry, entry_map[next_PC]);
528template<
class T,
typename P,
typename I>
534 it!=goto_program.instructions.end();
536 compute_edges(goto_functions, goto_program, it);
539template<
class T,
typename P,
typename I>
545 if(gf_entry.second.body_available())
546 compute_edges(goto_functions, gf_entry.second.body);
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)
data_typet::iterator iterator
entryt & at(const goto_programt::const_targett &t)
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
A multi-procedural control flow graph (CFG) whose nodes store references to instructions in a GOTO pr...
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)
virtual void compute_edges_catch(const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, entryt &entry)
base_grapht::node_indext entryt
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)
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)
grapht< cfg_base_nodet< T, I > > base_grapht
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)
std::size_t operator()(const goto_programt::const_targett &t) const
Functor to convert cfg nodes into dense integers, used by cfg_baset.
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
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
cfg_base_nodet< T, I > nodet
node_indext add_node(arguments &&... values)
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