20 #define DOTGRAPHSETTINGS "color=black;" \
21 "orientation=portrait;" \
37 void output(std::ostream &out);
54 std::string &
escape(std::string &str);
63 std::set<goto_programt::const_targett> &,
64 std::set<goto_programt::const_targett> &);
73 const std::string &name,
80 out <<
"subgraph \"cluster_" << name <<
"\" {\n";
81 out <<
"label=\"" << name <<
"\";\n";
86 if(instructions.empty())
89 "[shape=Mrecord,fontsize=22,label=\"?\"];\n";
95 std::set<goto_programt::const_targett> seen;
97 worklist.push_back(instructions.begin());
99 while(!worklist.empty())
102 worklist.pop_front();
104 if(it==instructions.end() ||
105 seen.find(it)!=seen.end())
continue;
107 std::stringstream tmp(
"");
110 if(it->guard.is_true())
114 std::string t =
from_expr(ns, it->function, it->guard);
115 while(t[ t.size()-1 ]==
'\n')
116 t = t.substr(0, t.size()-1);
120 else if(it->is_assume())
122 std::string t =
from_expr(ns, it->function, it->guard);
123 while(t[ t.size()-1 ]==
'\n')
124 t = t.substr(0, t.size()-1);
125 tmp <<
"Assume\\n(" <<
escape(t) <<
")";
127 else if(it->is_assert())
129 std::string t =
from_expr(ns, it->function, it->guard);
130 while(t[ t.size()-1 ]==
'\n')
131 t = t.substr(0, t.size()-1);
132 tmp <<
"Assert\\n(" <<
escape(t) <<
")";
134 else if(it->is_skip())
136 else if(it->is_end_function())
137 tmp.str(
"End of Function");
138 else if(it->is_location())
140 else if(it->is_dead())
142 else if(it->is_atomic_begin())
143 tmp.str(
"Atomic Begin");
144 else if(it->is_atomic_end())
145 tmp.str(
"Atomic End");
146 else if(it->is_function_call())
148 std::string t =
from_expr(ns, it->function, it->code);
149 while(t[ t.size()-1 ]==
'\n')
150 t = t.substr(0, t.size()-1);
154 std::stringstream ss;
157 fc.
operands().push_back(it->code.op1());
160 else if(it->is_assign() ||
165 std::string t =
from_expr(ns, it->function, it->code);
166 while(t[ t.size()-1 ]==
'\n')
167 t = t.substr(0, t.size()-1);
170 else if(it->is_start_thread())
171 tmp.str(
"Start of Thread");
172 else if(it->is_end_thread())
173 tmp.str(
"End of Thread");
174 else if(it->is_throw())
176 else if(it->is_catch())
183 if(it->is_goto() && !it->guard.is_true() && !it->guard.is_false())
187 out <<
",fontsize=22,label=\"";
191 std::set<goto_programt::const_targett> tres;
192 std::set<goto_programt::const_targett> fres;
195 std::string tlabel=
"true";
196 std::string flabel=
"false";
197 if(fres.empty() || tres.empty())
203 typedef std::set<goto_programt::const_targett> t;
205 for(t::iterator trit=tres.begin();
209 for(t::iterator frit=fres.begin();
216 worklist.insert(worklist.end(), temp.begin(), temp.end());
229 std::list<exprt>::const_iterator cit=
clusters.begin();
231 if(cit->get(
"name")==expr.op1().get(ID_identifier))
236 out << expr.op0().id() <<
237 " -> " "Node_" << cit->get(
"nr") <<
"_0" <<
238 " [lhead=\"cluster_" << expr.op1().get(ID_identifier) <<
"\"," <<
243 out <<
"subgraph \"cluster_" << expr.op1().get(ID_identifier) <<
245 out <<
"rank=sink;\n";
246 out <<
"label=\"" << expr.op1().get(ID_identifier) <<
"\";\n";
248 "[shape=Mrecord,fontsize=22,label=\"?\"];\n";
251 clusters.back().set(
"name", expr.op1().get(ID_identifier));
253 out << expr.op0().id() <<
255 " [lhead=\"cluster_" << expr.op1().get(
"identifier") <<
"\"," <<
264 out <<
"digraph G {\n";
268 if(it->second.body_available())
288 else if(str[i]==
'\"' ||
311 std::set<goto_programt::const_targett> &tres,
312 std::set<goto_programt::const_targett> &fres)
314 if(it->is_goto() && !it->guard.is_false())
316 for(
const auto &target : it->targets)
320 if(it->is_goto() && it->guard.is_true())
324 if(next!=instructions.end())
336 const std::string &label)
343 out <<
"[fontsize=20,label=\"" << label <<
"\"";