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 exprt guard
Guard for gotos, assume, assert.
I get_last_node(P &program) const
void compute_edges(const goto_functionst &goto_functions, const goto_programt &goto_program, I PC)
A generic directed graph with a parametric node type.
data_typet::iterator iterator
goto_program_instruction_typet type
What kind of instruction?
A multi-procedural control flow graph (CFG) whose nodes store references to instructions in a GOTO pr...
const irep_idt & get_identifier() const
Goto Programs with Functions.
grapht< cfg_base_nodet< T, I > > & container
bool is_false() const
Return whether the expression is a constant representing false.
virtual void compute_edges_goto(const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, entryt &entry)
bool is_true() const
Return whether the expression is a constant representing true.
function_mapt function_map
bool nodes_empty(P &program) const
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
const_iterator cbegin() const
targetst targets
The list of successor instructions.
virtual void compute_edges_catch(const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, entryt &entry)
This class represents an instruction in the GOTO intermediate representation.
const_iterator find(U &&u) const
void operator()(const goto_functionst &goto_functions)
instructionst instructions
The list of instructions in the goto program.
API to expression classes.
graph_nodet< empty_edget >::edgest edgest
void operator()(P &goto_program)
instructionst::const_iterator const_targett
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 collection of goto functions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
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)
data_typet::const_iterator const_iterator
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
entryt & operator[](const goto_programt::const_targett &t)
A generic container class for the GOTO intermediate representation of one function.
virtual void compute_edges_throw(const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, entryt &entry)
A Template Class for Graphs.
graph_nodet< empty_edget >::edget edget
Base class for all expressions.
entry_mapt(grapht< cfg_base_nodet< T, I > > &_container)
#define UNREACHABLE
This should be used to mark dead code.
std::map< goto_programt::const_targett, entryt > data_typet
I get_first_node(P &program) 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, entryt &entry)
#define forall_goto_functions(it, functions)
const_iterator end() const
This class represents a node in a directed graph.
virtual void compute_edges_start_thread(const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, entryt &entry)
const_iterator cend() const
const code_function_callt & to_code_function_call(const codet &code)
const_iterator begin() const