20typedef std::map<std::string, graphmlt::node_indext>
name_mapt;
23 const std::string &name,
27 std::pair<name_mapt::iterator, bool> entry=
30 entry.first->second=graph.
add_node();
32 return entry.first->second;
38 std::map<std::string, std::map<std::string, std::string> > &
defaults,
54 for(xmlt::elementst::const_iterator
61 if(
e_it->get_attribute(
"key")==
"violation" &&
64 else if(
e_it->get_attribute(
"key")==
"entry" &&
81 for(std::map<std::string, std::string>::const_iterator
87 for(xmlt::elementst::const_iterator
91 found=
e_it->get_attribute(
"key")==it->first;
107 for(xmlt::elementst::const_iterator
122 for(xmlt::elementst::const_iterator
126 if(
e_it->name==
"default")
151 std::map<std::string, std::map<std::string, std::string> >
defaults;
162 for(std::size_t
i=0; !
err &&
i<
dest.size(); ++
i)
166 INVARIANT(!
n.node_name.empty(),
"node should be named");
192 const std::string &filename,
207 xmlt graphml(
"graphml");
210 "http://www.w3.org/2001/XMLSchema-instance");
213 "http://graphml.graphdrawing.org/xmlns");
221 key.set_attribute(
"attr.name",
"originFileName");
222 key.set_attribute(
"attr.type",
"string");
223 key.set_attribute(
"for",
"edge");
224 key.set_attribute(
"id",
"originfile");
227 key.new_element(
"default").data=src.
key_values.at(
"programfile");
229 key.new_element(
"default").data=
"<command-line>";
235 key.set_attribute(
"attr.name",
"invariant");
236 key.set_attribute(
"attr.type",
"string");
237 key.set_attribute(
"for",
"node");
238 key.set_attribute(
"id",
"invariant");
245 key.set_attribute(
"attr.name",
"invariant.scope");
246 key.set_attribute(
"attr.type",
"string");
247 key.set_attribute(
"for",
"node");
248 key.set_attribute(
"id",
"invariant.scope");
257 key.set_attribute(
"attr.name",
"isViolationNode");
258 key.set_attribute(
"attr.type",
"boolean");
259 key.set_attribute(
"for",
"node");
260 key.set_attribute(
"id",
"violation");
262 key.new_element(
"default").data=
"false";
270 key.set_attribute(
"attr.name",
"isEntryNode");
271 key.set_attribute(
"attr.type",
"boolean");
272 key.set_attribute(
"for",
"node");
273 key.set_attribute(
"id",
"entry");
275 key.new_element(
"default").data=
"false";
283 key.set_attribute(
"attr.name",
"isSinkNode");
284 key.set_attribute(
"attr.type",
"boolean");
285 key.set_attribute(
"for",
"node");
286 key.set_attribute(
"id",
"sink");
288 key.new_element(
"default").data=
"false";
297 key.set_attribute(
"attr.name",
"enterLoopHead");
298 key.set_attribute(
"attr.type",
"boolean");
299 key.set_attribute(
"for",
"edge");
300 key.set_attribute(
"id",
"enterLoopHead");
302 key.new_element(
"default").data=
"false";
311 key.set_attribute(
"attr.name",
"cyclehead");
312 key.set_attribute(
"attr.type",
"boolean");
313 key.set_attribute(
"for",
"node");
314 key.set_attribute(
"id",
"cyclehead");
316 key.new_element(
"default").data =
"false";
322 key.set_attribute(
"attr.name",
"threadId");
323 key.set_attribute(
"attr.type",
"int");
324 key.set_attribute(
"for",
"edge");
325 key.set_attribute(
"id",
"threadId");
327 key.new_element(
"default").data =
"0";
334 key.set_attribute(
"attr.name",
"createThread");
335 key.set_attribute(
"attr.type",
"int");
336 key.set_attribute(
"for",
"edge");
337 key.set_attribute(
"id",
"createThread");
339 key.new_element(
"default").data=
"0";
346 key.set_attribute(
"attr.name",
"sourcecodeLanguage");
347 key.set_attribute(
"attr.type",
"string");
348 key.set_attribute(
"for",
"graph");
349 key.set_attribute(
"id",
"sourcecodelang");
356 key.set_attribute(
"attr.name",
"programFile");
357 key.set_attribute(
"attr.type",
"string");
358 key.set_attribute(
"for",
"graph");
359 key.set_attribute(
"id",
"programfile");
366 key.set_attribute(
"attr.name",
"programHash");
367 key.set_attribute(
"attr.type",
"string");
368 key.set_attribute(
"for",
"graph");
369 key.set_attribute(
"id",
"programhash");
376 key.set_attribute(
"attr.name",
"specification");
377 key.set_attribute(
"attr.type",
"string");
378 key.set_attribute(
"for",
"graph");
379 key.set_attribute(
"id",
"specification");
386 key.set_attribute(
"attr.name",
"architecture");
387 key.set_attribute(
"attr.type",
"string");
388 key.set_attribute(
"for",
"graph");
389 key.set_attribute(
"id",
"architecture");
396 key.set_attribute(
"attr.name",
"producer");
397 key.set_attribute(
"attr.type",
"string");
398 key.set_attribute(
"for",
"graph");
399 key.set_attribute(
"id",
"producer");
406 key.set_attribute(
"attr.name",
"creationtime");
407 key.set_attribute(
"attr.type",
"string");
408 key.set_attribute(
"for",
"graph");
409 key.set_attribute(
"id",
"creationtime");
415 key.set_attribute(
"attr.name",
"startline");
416 key.set_attribute(
"attr.type",
"int");
417 key.set_attribute(
"for",
"edge");
418 key.set_attribute(
"id",
"startline");
424 key.set_attribute(
"attr.name",
"control");
425 key.set_attribute(
"attr.type",
"string");
426 key.set_attribute(
"for",
"edge");
427 key.set_attribute(
"id",
"control");
433 key.set_attribute(
"attr.name",
"assumption");
434 key.set_attribute(
"attr.type",
"string");
435 key.set_attribute(
"for",
"edge");
436 key.set_attribute(
"id",
"assumption");
443 key.set_attribute(
"attr.name",
"assumption.resultfunction");
444 key.set_attribute(
"attr.type",
"string");
445 key.set_attribute(
"for",
"edge");
446 key.set_attribute(
"id",
"assumption.resultfunction");
453 key.set_attribute(
"attr.name",
"assumption.scope");
454 key.set_attribute(
"attr.type",
"string");
455 key.set_attribute(
"for",
"edge");
456 key.set_attribute(
"id",
"assumption.scope");
463 key.set_attribute(
"attr.name",
"enterFunction");
464 key.set_attribute(
"attr.type",
"string");
465 key.set_attribute(
"for",
"edge");
466 key.set_attribute(
"id",
"enterFunction");
473 key.set_attribute(
"attr.name",
"returnFromFunction");
474 key.set_attribute(
"attr.type",
"string");
475 key.set_attribute(
"for",
"edge");
476 key.set_attribute(
"id",
"returnFrom");
483 key.set_attribute(
"attr.name",
"witness-type");
484 key.set_attribute(
"attr.type",
"string");
485 key.set_attribute(
"for",
"graph");
486 key.set_attribute(
"id",
"witness-type");
495 data.set_attribute(
"key",
kv.first);
533 val.set_attribute(
"key",
"invariant");
534 val.data=
n.invariant;
537 val_s.set_attribute(
"key",
"invariant.scope");
538 val_s.data=
n.invariant_scope;
541 for(graphmlt::edgest::const_iterator
548 os <<
"<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n";
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
nodet::node_indext node_indext
node_indext add_node(arguments &&... values)
std::string get_attribute(const std::string &attribute) const
xmlt & new_element(const std::string &key)
void set_attribute(const std::string &attribute, unsigned value)
static graphmlt::node_indext add_node(const std::string &name, name_mapt &name_to_node, graphmlt &graph)
bool write_graphml(const graphmlt &src, std::ostream &os)
std::map< std::string, graphmlt::node_indext > name_mapt
static bool build_graph(const xmlt &xml, graphmlt &dest, graphmlt::node_indext &entry)
static bool build_graph_rec(const xmlt &xml, name_mapt &name_to_node, std::map< std::string, std::map< std::string, std::string > > &defaults, graphmlt &dest, std::string &entrynode)
bool read_graphml(std::istream &is, graphmlt &dest, graphmlt::node_indext &entry)
Read/write graphs as GraphML.
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
#define UNREACHABLE
This should be used to mark dead code.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
bool parse_xml(std::istream &in, const std::string &filename, message_handlert &message_handler, xmlt &dest)