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, goto_programt::target_less_than>
98 worklist.push_back(instructions.begin());
100 while(!worklist.empty())
103 worklist.pop_front();
105 if(it==instructions.end() ||
106 seen.find(it)!=seen.end())
continue;
108 std::stringstream tmp;
111 if(it->condition().is_true())
115 std::string t =
from_expr(ns, function_id, it->condition());
116 while(t[ t.size()-1 ]==
'\n')
117 t = t.substr(0, t.size()-1);
121 else if(it->is_assume())
123 std::string t =
from_expr(ns, function_id, it->condition());
124 while(t[ t.size()-1 ]==
'\n')
125 t = t.substr(0, t.size()-1);
126 tmp <<
"Assume\\n(" <<
escape(t) <<
")";
128 else if(it->is_assert())
130 std::string t =
from_expr(ns, function_id, it->condition());
131 while(t[ t.size()-1 ]==
'\n')
132 t = t.substr(0, t.size()-1);
133 tmp <<
"Assert\\n(" <<
escape(t) <<
")";
135 else if(it->is_skip())
137 else if(it->is_end_function())
138 tmp.str(
"End of Function");
139 else if(it->is_location())
141 else if(it->is_dead())
143 else if(it->is_atomic_begin())
144 tmp.str(
"Atomic Begin");
145 else if(it->is_atomic_end())
146 tmp.str(
"Atomic End");
147 else if(it->is_function_call())
150 it->call_lhs(), it->call_function(), it->call_arguments());
151 std::string t =
from_expr(ns, function_id, function_call);
152 while(t[ t.size()-1 ]==
'\n')
153 t = t.substr(0, t.size()-1);
156 std::stringstream ss;
159 std::pair<std::string, exprt>(ss.str(), it->call_function()));
162 it->is_assign() || it->is_decl() || it->is_set_return_value() ||
165 std::string t =
from_expr(ns, function_id, 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->condition().is_constant())
187 out <<
",fontsize=22,label=\"";
191 std::set<goto_programt::const_targett, goto_programt::target_less_than>
193 std::set<goto_programt::const_targett, goto_programt::target_less_than>
199 if(!fres.empty() && !tres.empty())
206 set<goto_programt::const_targett, goto_programt::target_less_than>
209 for(t::iterator trit=tres.begin();
213 for(t::iterator frit=fres.begin();
220 worklist.insert(worklist.end(), temp.begin(), temp.end());
233 std::list<exprt>::const_iterator cit=
clusters.begin();
235 if(cit->get(
"name") == call.second.get(ID_identifier))
243 << cit->get(
"nr") <<
"_0"
244 <<
" [lhead=\"cluster_" << call.second.get(ID_identifier) <<
"\","
249 out <<
"subgraph \"cluster_" << call.second.get(ID_identifier)
251 out <<
"rank=sink;\n";
252 out <<
"label=\"" << call.second.get(ID_identifier) <<
"\";\n";
254 "[shape=Mrecord,fontsize=22,label=\"?\"];\n";
257 clusters.back().set(
"name", call.second.get(ID_identifier));
263 <<
" [lhead=\"cluster_" << call.second.get(
"identifier") <<
"\","
320 std::set<goto_programt::const_targett, goto_programt::target_less_than> &tres,
321 std::set<goto_programt::const_targett, goto_programt::target_less_than> &fres)
323 if(it->is_goto() && !it->condition().is_false())
325 for(
const auto &target : it->targets)
329 if(it->is_goto() && it->condition().is_true())
333 if(next!=instructions.end())
void find_next(const goto_programt::instructionst &, const goto_programt::const_targett &, std::set< goto_programt::const_targett, goto_programt::target_less_than > &, std::set< goto_programt::const_targett, goto_programt::target_less_than > &)
finds an instructions successors (for goto graphs)
void write_dot_subgraph(std::ostream &, const irep_idt &, const goto_programt &)
Write the dot graph that corresponds to the goto program to the output stream.
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...