Go to the documentation of this file.
12 #ifndef CPROVER_GOTO_PROGRAMS_CFG_H
13 #define CPROVER_GOTO_PROGRAMS_CFG_H
25 template<
class T,
typename I>
69 typedef std::map<goto_programt::const_targett, entryt>
data_typet;
98 auto e=
data.insert(std::make_pair(t, 0));
103 return e.first->second;
175 bool nodes_empty(P &program)
const {
return program.instructions.empty(); }
214 template<
class T,
typename P,
typename I>
223 this->add_edge(entry, entry_map[next_PC]);
225 this->add_edge(entry, entry_map[instruction.
get_target()]);
228 template<
class T,
typename P,
typename I>
236 this->add_edge(entry, entry_map[next_PC]);
241 for(
const auto &t : instruction.
targets)
243 this->add_edge(entry, entry_map[t]);
246 template<
class T,
typename P,
typename I>
256 template<
class T,
typename P,
typename I>
264 this->add_edge(entry, entry_map[next_PC]);
267 template<
class T,
typename P,
typename I>
280 this->add_edge(entry, this->entry_map[instruction.
get_target()]);
283 template<
class T,
typename P,
typename I>
291 const exprt &
function=
294 if(
function.
id()!=ID_symbol)
300 goto_functionst::function_mapt::const_iterator f_it=
304 f_it->second.body_available())
308 f_it->second.body.instructions.begin();
311 f_it->second.body.instructions.end();
318 this->add_edge(entry, entry_map[i_it]);
322 this->add_edge(entry_map[last_it], entry_map[next_PC]);
327 this->add_edge(entry, entry_map[next_PC]);
331 this->add_edge(entry, entry_map[next_PC]);
334 template<
class T,
typename P,
typename I>
342 const exprt &
function=
345 if(
function.
id()!=ID_symbol)
349 this->add_edge(entry, this->entry_map[next_PC]);
352 template<
class T,
typename P,
typename I>
359 entryt entry=entry_map[PC];
360 (*this)[entry].PC=PC;
365 switch(instruction.
type)
368 compute_edges_goto(goto_program, instruction, next_PC, entry);
372 compute_edges_catch(goto_program, instruction, next_PC, entry);
376 compute_edges_throw(goto_program, instruction, next_PC, entry);
380 compute_edges_start_thread(
388 compute_edges_function_call(
417 this->add_edge(entry, entry_map[next_PC]);
427 template<
class T,
typename P,
typename I>
433 it!=goto_program.instructions.end();
435 compute_edges(goto_functions, goto_program, it);
438 template<
class T,
typename P,
typename I>
443 if(it->second.body_available())
444 compute_edges(goto_functions, it->second.body);
447 #endif // CPROVER_GOTO_PROGRAMS_CFG_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const_iterator find(U &&u) 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)
void operator()(P &goto_program)
goto_program_instruction_typet type
What kind of instruction?
A generic directed graph with a parametric node type.
grapht< cfg_base_nodet< T, I > > & container
Base class for all expressions.
entryt & operator[](const goto_programt::const_targett &t)
targetst targets
The list of successor instructions.
bool is_true() const
Return whether the expression is a constant representing true.
virtual void compute_edges_throw(const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, entryt &entry)
function_mapt function_map
virtual void compute_edges_start_thread(const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, entryt &entry)
#define UNREACHABLE
This should be used to mark dead code.
bool is_false() const
Return whether the expression is a constant representing false.
I get_first_node(P &program) const
graph_nodet< empty_edget >::edgest edgest
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)
const irep_idt & get_identifier() const
I get_last_node(P &program) const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
void compute_edges(const goto_functionst &goto_functions, const goto_programt &goto_program, I PC)
const code_function_callt & to_code_function_call(const codet &code)
const_iterator end() const
entry_mapt(grapht< cfg_base_nodet< T, I > > &_container)
const_iterator cbegin() const
A multi-procedural control flow graph (CFG) whose nodes store references to instructions in a GOTO pr...
instructionst instructions
The list of instructions in the goto program.
bool nodes_empty(P &program) const
A collection of goto functions.
data_typet::const_iterator const_iterator
std::map< goto_programt::const_targett, entryt > data_typet
This class represents a node in a directed graph.
virtual void compute_edges_goto(const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, entryt &entry)
graph_nodet< empty_edget >::edget edget
exprt guard
Guard for gotos, assume, assert.
A generic container class for the GOTO intermediate representation of one function.
#define forall_goto_functions(it, functions)
instructionst::const_iterator const_targett
virtual void compute_edges_catch(const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, entryt &entry)
void operator()(const goto_functionst &goto_functions)
This class represents an instruction in the GOTO intermediate representation.
const_iterator cend() const
const_iterator begin() 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)
data_typet::iterator iterator
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.