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> &);
76 clusters.back().set(
"name", function_id);
79 out <<
"subgraph \"cluster_" << function_id <<
"\" {\n";
80 out <<
"label=\"" << function_id <<
"\";\n";
85 if(instructions.empty())
88 "[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->get_condition().is_true())
113 std::string t =
from_expr(ns, function_id, it->get_condition());
114 while(t[ t.size()-1 ]==
'\n')
115 t = t.substr(0, t.size()-1);
119 else if(it->is_assume())
121 std::string t =
from_expr(ns, function_id, it->get_condition());
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())
128 std::string t =
from_expr(ns, function_id, it->get_condition());
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())
147 const auto &function_call = it->get_function_call();
148 std::string t =
from_expr(ns, function_id, function_call);
149 while(t[ t.size()-1 ]==
'\n')
150 t = t.substr(0, t.size()-1);
153 std::stringstream ss;
156 std::pair<std::string, exprt>(ss.str(), it->call_function()));
159 it->is_assign() || it->is_decl() || it->is_set_return_value() ||
162 std::string t =
from_expr(ns, function_id, it->get_code());
163 while(t[ t.size()-1 ]==
'\n')
164 t = t.substr(0, t.size()-1);
167 else if(it->is_start_thread())
168 tmp.str(
"Start of Thread");
169 else if(it->is_end_thread())
170 tmp.str(
"End of Thread");
171 else if(it->is_throw())
173 else if(it->is_catch())
180 if(it->is_goto() && !it->get_condition().is_constant())
184 out <<
",fontsize=22,label=\"";
188 std::set<goto_programt::const_targett> tres;
189 std::set<goto_programt::const_targett> fres;
194 if(!fres.empty() && !tres.empty())
200 typedef std::set<goto_programt::const_targett> t;
202 for(t::iterator trit=tres.begin();
206 for(t::iterator frit=fres.begin();
213 worklist.insert(worklist.end(), temp.begin(), temp.end());
226 std::list<exprt>::const_iterator cit=
clusters.begin();
228 if(cit->get(
"name") == call.second.get(ID_identifier))
236 << cit->get(
"nr") <<
"_0"
237 <<
" [lhead=\"cluster_" << call.second.get(ID_identifier) <<
"\","
242 out <<
"subgraph \"cluster_" << call.second.get(ID_identifier)
244 out <<
"rank=sink;\n";
245 out <<
"label=\"" << call.second.get(ID_identifier) <<
"\";\n";
247 "[shape=Mrecord,fontsize=22,label=\"?\"];\n";
250 clusters.back().set(
"name", call.second.get(ID_identifier));
256 <<
" [lhead=\"cluster_" << call.second.get(
"identifier") <<
"\","
265 out <<
"digraph G {\n";
270 if(gf_entry.second.body_available())
291 else if(str[i]==
'\"' ||
313 std::set<goto_programt::const_targett> &tres,
314 std::set<goto_programt::const_targett> &fres)
316 if(it->is_goto() && !it->get_condition().is_false())
318 for(
const auto &target : it->targets)
322 if(it->is_goto() && it->get_condition().is_true())
326 if(next!=instructions.end())
337 const std::string &label)
344 out <<
"[fontsize=20,label=\"" << label <<
"\"";