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 <<
"\"";
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)