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);
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);
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())
148 it->call_lhs(), it->call_function(), it->call_arguments());
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(), it->call_function()));
160 it->is_assign() || it->is_decl() || it->is_set_return_value() ||
163 std::string t =
from_expr(ns, function_id, it->get_code());
164 while(t[ t.size()-1 ]==
'\n')
165 t = t.substr(0, t.size()-1);
168 else if(it->is_start_thread())
169 tmp.str(
"Start of Thread");
170 else if(it->is_end_thread())
171 tmp.str(
"End of Thread");
172 else if(it->is_throw())
174 else if(it->is_catch())
181 if(it->is_goto() && !it->get_condition().is_constant())
185 out <<
",fontsize=22,label=\"";
189 std::set<goto_programt::const_targett>
tres;
190 std::set<goto_programt::const_targett>
fres;
201 typedef std::set<goto_programt::const_targett> t;
214 worklist.insert(worklist.end(),
temp.begin(),
temp.end());
227 std::list<exprt>::const_iterator cit=
clusters.begin();
237 << cit->get(
"nr") <<
"_0"
245 out <<
"rank=sink;\n";
248 "[shape=Mrecord,fontsize=22,label=\"?\"];\n";
257 <<
" [lhead=\"cluster_" <<
call.second.get(
"identifier") <<
"\","
266 out <<
"digraph G {\n";
271 if(
gf_entry.second.body_available())
285 for(std::string::size_type
i=0;
i<str.size();
i++)
292 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())
338 const std::string &label)
345 out <<
"[fontsize=20,label=\"" << label <<
"\"";
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
codet representation of a function call statement.
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)