18 #define DOTGRAPHSETTINGS "color=black;" \ 19 "orientation=portrait;" \ 37 void output(std::ostream &out);
55 std::string &
escape(std::string &str);
58 const goto_programt::instructiont &,
59 const goto_programt::instructiont &,
64 std::set<goto_programt::const_targett> &,
65 std::set<goto_programt::const_targett> &);
74 const std::string &name,
81 out <<
"subgraph \"cluster_" << name <<
"\" {\n";
82 out <<
"label=\"" << name <<
"\";\n";
87 if(instructions.empty())
90 "[shape=Mrecord,fontsize=22,label=\"?\"];\n";
94 std::set<goto_programt::const_targett> seen;
96 worklist.push_back(instructions.begin());
98 while(!worklist.empty())
101 worklist.pop_front();
103 if(it==instructions.end() ||
104 seen.find(it)!=seen.end())
continue;
106 std::stringstream tmp(
"");
109 if(it->guard.is_true())
114 while(t[ t.size()-1 ]==
'\n')
115 t = t.substr(0, t.size()-1);
119 else if(it->is_assume())
122 while(t[ t.size()-1 ]==
'\n')
123 t = t.substr(0, t.size()-1);
124 tmp <<
"Assume\\n(" <<
escape(t) <<
")";
126 else if(it->is_assert())
129 while(t[ t.size()-1 ]==
'\n')
130 t = t.substr(0, t.size()-1);
131 tmp <<
"Assert\\n(" <<
escape(t) <<
")";
133 else if(it->is_skip())
135 else if(it->is_end_function())
136 tmp.str(
"End of Function");
137 else if(it->is_location())
139 else if(it->is_dead())
141 else if(it->is_atomic_begin())
142 tmp.str(
"Atomic Begin");
143 else if(it->is_atomic_end())
144 tmp.str(
"Atomic End");
145 else if(it->is_function_call())
148 while(t[ t.size()-1 ]==
'\n')
149 t = t.substr(0, t.size()-1);
153 std::stringstream ss;
156 fc.
operands().push_back(it->code.op1());
159 else if(it->is_assign() ||
165 while(t[ t.size()-1 ]==
'\n')
166 t = t.substr(0, t.size()-1);
169 else if(it->is_start_thread())
170 tmp.str(
"Start of Thread");
171 else if(it->is_end_thread())
172 tmp.str(
"End of Thread");
173 else if(it->is_throw())
175 else if(it->is_catch())
182 if(it->is_goto() && !it->guard.is_true() && !it->guard.is_false())
186 out <<
",fontsize=22,label=\"";
190 std::set<goto_programt::const_targett> tres;
191 std::set<goto_programt::const_targett> fres;
194 std::string tlabel=
"true";
195 std::string flabel=
"false";
196 if(fres.empty() || tres.empty())
202 typedef std::set<goto_programt::const_targett> t;
204 for(t::iterator trit=tres.begin();
208 for(t::iterator frit=fres.begin();
215 worklist.insert(worklist.end(), temp.begin(), temp.end());
228 std::list<exprt>::const_iterator cit=
clusters.begin();
230 if(cit->get(
"name")==expr.op1().get(ID_identifier))
235 out << expr.op0().id() <<
236 " -> " "Node_" << cit->get(
"nr") <<
"_0" <<
237 " [lhead=\"cluster_" << expr.op1().get(ID_identifier) <<
"\"," <<
242 out <<
"subgraph \"cluster_" << expr.op1().get(ID_identifier) <<
244 out <<
"rank=sink;\n";
245 out <<
"label=\"" << expr.op1().get(ID_identifier) <<
"\";\n";
247 "[shape=Mrecord,fontsize=22,label=\"?\"];\n";
250 clusters.back().set(
"name", expr.op1().get(ID_identifier));
251 clusters.back().set(
"nr", subgraphscount);
252 out << expr.op0().id() <<
253 " -> " "Node_" << subgraphscount <<
"_0" <<
254 " [lhead=\"cluster_" << expr.op1().get(
"identifier") <<
"\"," <<
263 out <<
"digraph G {\n";
269 if(it->second.body_available())
289 else if(str[i]==
'\"' ||
312 std::set<goto_programt::const_targett> &tres,
313 std::set<goto_programt::const_targett> &fres)
315 if(it->is_goto() && !it->guard.is_false())
317 for(
const auto &target : it->targets)
321 if(it->is_goto() && it->guard.is_true())
325 if(next!=instructions.end())
335 const goto_programt::instructiont &from,
336 const goto_programt::instructiont &to,
337 const std::string &label)
341 out <<
"Node_" <<
subgraphscount <<
"_" << to.location_number <<
" ";
344 out <<
"[fontsize=20,label=\"" << label <<
"\"";
345 if(from.is_backwards_goto() &&
346 from.location_number > to.location_number)
const std::string & id2string(const irep_idt &d)
std::list< instructiont > instructionst
instructionst instructions
The list of instructions in the goto program.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::list< exprt > clusters
unsignedbv_typet size_type()
const goto_functionst & goto_functions
void output(std::ostream &out)
std::list< Target > get_successors(Target target) const
instructionst::const_iterator const_targett
std::list< exprt > function_calls
std::string & escape(std::string &str)
escapes a string.
void do_dot_function_calls(std::ostream &)
Dump Goto-Program as DOT Graph.
dott(const goto_functionst &_goto_functions, const namespacet &_ns)
void find_next(const goto_programt::instructionst &, const goto_programt::const_targett &, std::set< goto_programt::const_targett > &, std::set< goto_programt::const_targett > &)
finds an instructions successors (for goto graphs)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
void write_edge(std::ostream &, const goto_programt::instructiont &, const goto_programt::instructiont &, const std::string &)
writes an edge from the from node to the to node and with the given label to the output stream (dot f...
Base class for all expressions.
void dot(const goto_functionst &src, const namespacet &ns, std::ostream &out)
#define forall_goto_functions(it, functions)
std::list< const_targett > const_targetst
void write_dot_subgraph(std::ostream &, const std::string &, const goto_programt &)
writes the dot graph that corresponds to the goto program to the output stream.