12 #ifndef CPROVER_GOTO_PROGRAMS_CFG_H 13 #define CPROVER_GOTO_PROGRAMS_CFG_H 25 template<
class T,
typename I>
68 public std::map<goto_programt::const_targett, entryt>
79 std::pair<iterator, bool> e=insert(std::make_pair(t, 0));
84 return e.first->second;
92 const goto_programt::instructiont &instruction,
98 const goto_programt::instructiont &instruction,
104 const goto_programt::instructiont &instruction,
110 const goto_programt::instructiont &instruction,
117 const goto_programt::instructiont &instruction,
156 bool nodes_empty(P &program)
const {
return program.instructions.empty(); }
167 const goto_programt::instructiont &instruction,
181 const goto_programt::instructiont &instruction,
195 template<
class T,
typename P,
typename I>
198 const goto_programt::instructiont &instruction,
203 !instruction.guard.is_true())
204 this->add_edge(entry, entry_map[next_PC]);
206 for(
const auto &t : instruction.targets)
208 this->add_edge(entry, entry_map[t]);
211 template<
class T,
typename P,
typename I>
214 const goto_programt::instructiont &instruction,
219 this->add_edge(entry, entry_map[next_PC]);
224 for(
const auto &t : instruction.targets)
226 this->add_edge(entry, entry_map[t]);
229 template<
class T,
typename P,
typename I>
232 const goto_programt::instructiont &instruction,
239 template<
class T,
typename P,
typename I>
242 const goto_programt::instructiont &instruction,
247 this->add_edge(entry, entry_map[next_PC]);
250 template<
class T,
typename P,
typename I>
253 const goto_programt::instructiont &instruction,
263 for(
const auto &t : instruction.targets)
265 this->add_edge(entry, this->entry_map[t]);
268 template<
class T,
typename P,
typename I>
272 const goto_programt::instructiont &instruction,
276 const exprt &
function=
279 if(
function.
id()!=ID_symbol)
285 goto_functionst::function_mapt::const_iterator f_it=
289 f_it->second.body_available())
293 f_it->second.body.instructions.begin();
296 f_it->second.body.instructions.end();
303 this->add_edge(entry, entry_map[i_it]);
307 this->add_edge(entry_map[last_it], entry_map[next_PC]);
312 this->add_edge(entry, entry_map[next_PC]);
316 this->add_edge(entry, entry_map[next_PC]);
319 template<
class T,
typename P,
typename I>
323 const goto_programt::instructiont &instruction,
327 const exprt &
function=
330 if(
function.
id()!=ID_symbol)
334 this->add_edge(entry, this->entry_map[next_PC]);
337 template<
class T,
typename P,
typename I>
343 const goto_programt::instructiont &instruction=*PC;
344 entryt entry=entry_map[PC];
345 (*this)[entry].PC=PC;
350 switch(instruction.type)
353 compute_edges_goto(goto_program, instruction, next_PC, entry);
357 compute_edges_catch(goto_program, instruction, next_PC, entry);
361 compute_edges_throw(goto_program, instruction, next_PC, entry);
365 compute_edges_start_thread(
373 compute_edges_function_call(
388 if(instruction.guard.is_false())
402 this->add_edge(entry, entry_map[next_PC]);
411 template<
class T,
typename P,
typename I>
417 it!=goto_program.instructions.end();
419 compute_edges(goto_functions, goto_program, it);
422 template<
class T,
typename P,
typename I>
427 if(it->second.body_available())
428 compute_edges(goto_functions, it->second.body);
431 #endif // CPROVER_GOTO_PROGRAMS_CFG_H 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.
instructionst instructions
The list of instructions in the goto program.
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.
virtual void compute_edges_goto(const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, entryt &entry)
bool nodes_empty(P &program) const
virtual void compute_edges_catch(const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, entryt &entry)
grapht< cfg_base_nodet< T, I > > & container
instructionst::const_iterator const_targett
void operator()(const goto_functionst &goto_functions)
API to expression classes.
graph_nodet< empty_edget >::edgest edgest
void operator()(P &goto_program)
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)
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)
function_mapt function_map
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
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.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
I get_first_node(P &program) const
entry_mapt(grapht< cfg_base_nodet< T, I > > &_container)
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)
entryt & operator[](const goto_programt::const_targett &t)
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 code_function_callt & to_code_function_call(const codet &code)