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";
272 if(gf_entry.second.body_available())
293 else if(str[i]==
'\"' ||
316 std::set<goto_programt::const_targett> &tres,
317 std::set<goto_programt::const_targett> &fres)
319 if(it->is_goto() && !it->get_condition().is_false())
321 for(
const auto &target : it->targets)
325 if(it->is_goto() && it->get_condition().is_true())
329 if(next!=instructions.end())
341 const std::string &label)
348 out <<
"[fontsize=20,label=\"" << label <<
"\"";
unsignedbv_typet size_type()
std::list< std::pair< std::string, exprt > > function_calls
std::list< exprt > clusters
std::string & escape(std::string &str)
escapes a string.
void do_dot_function_calls(std::ostream &)
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.
const goto_modelt & goto_model
dott(const goto_modelt &_goto_model)
void output(std::ostream &out)
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)
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...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
This class represents an instruction in the GOTO intermediate representation.
unsigned location_number
A globally unique number to identify a program location.
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
instructionst::const_iterator const_targett
std::list< instructiont > instructionst
std::list< const_targett > const_targetst
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void dot(const goto_modelt &src, std::ostream &out)
Dump Goto-Program as DOT Graph.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)