20 #define DOTGRAPHSETTINGS "color=black;" \
21 "orientation=portrait;" \
37 void output(std::ostream &out);
52 std::string &
escape(std::string &str);
61 std::set<goto_programt::const_targett> &,
62 std::set<goto_programt::const_targett> &);
77 clusters.back().set(
"name", function_id);
80 out <<
"subgraph \"cluster_" << function_id <<
"\" {\n";
81 out <<
"label=\"" << function_id <<
"\";\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->get_condition().is_true())
114 std::string t =
from_expr(ns, function_id, it->get_condition());
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, function_id, it->get_condition());
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, function_id, it->get_condition());
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 const auto &function_call = it->get_function_call();
149 std::string t =
from_expr(ns, function_id, function_call);
150 while(t[ t.size()-1 ]==
'\n')
151 t = t.substr(0, t.size()-1);
154 std::stringstream ss;
157 std::pair<std::string, exprt>(ss.str(), function_call.function()));
159 else if(it->is_assign() ||
164 std::string t =
from_expr(ns, function_id, it->code);
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->get_condition().is_constant())
186 out <<
",fontsize=22,label=\"";
190 std::set<goto_programt::const_targett> tres;
191 std::set<goto_programt::const_targett> fres;
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") == call.second.get(ID_identifier))
238 << cit->get(
"nr") <<
"_0"
239 <<
" [lhead=\"cluster_" << call.second.get(ID_identifier) <<
"\","
244 out <<
"subgraph \"cluster_" << call.second.get(ID_identifier)
246 out <<
"rank=sink;\n";
247 out <<
"label=\"" << call.second.get(ID_identifier) <<
"\";\n";
249 "[shape=Mrecord,fontsize=22,label=\"?\"];\n";
252 clusters.back().set(
"name", call.second.get(ID_identifier));
258 <<
" [lhead=\"cluster_" << call.second.get(
"identifier") <<
"\","
267 out <<
"digraph G {\n";
271 if(it->second.body_available())
291 else if(str[i]==
'\"' ||
314 std::set<goto_programt::const_targett> &tres,
315 std::set<goto_programt::const_targett> &fres)
317 if(it->is_goto() && !it->get_condition().is_false())
319 for(
const auto &target : it->targets)
323 if(it->is_goto() && it->get_condition().is_true())
327 if(next!=instructions.end())
339 const std::string &label)
346 out <<
"[fontsize=20,label=\"" << label <<
"\"";