30 std::stringstream tmp;
36 if(!inst.location.is_nil())
42 if(!inst.labels.empty())
45 for(goto_programt::instructiont::labelst::const_iterator
46 l_it=inst.labels.begin();
47 l_it!=inst.labels.end();
55 if(inst.target_number!=0)
59 tmp << inst.target_number;
68 if(!inst.guard.is_true())
74 for(goto_programt::instructiont::targetst::const_iterator
75 gt_it=inst.targets.begin();
76 gt_it!=inst.targets.end();
80 tmp << (*gt_it)->target_number;
113 ins.
name=
"end_function";
125 ins.
name=
"atomic_begin";
129 ins.
name=
"atomic_end";
142 ins.
name=
"instruction";
158 ins.
name=
"functioncall";
166 ins.
name=
"thread_start";
168 if(inst.targets.size()==1)
171 tmp << inst.targets.front()->target_number;
178 ins.
name=
"thread_end";
186 if(inst.function!=
"")
202 goto_program.
clear();
205 for(
const auto &element : xml.
elements)
208 inst->targets.clear();
210 if(element.name==
"goto")
214 else if(element.name==
"assume")
218 else if(element.name==
"assert")
222 else if(element.name==
"skip")
226 else if(element.name==
"end_function")
230 else if(element.name==
"location")
234 else if(element.name==
"dead")
238 else if(element.name==
"atomic_begin")
242 else if(element.name==
"atomic_end")
246 else if(element.name==
"return")
250 else if(element.name==
"instruction")
254 else if(element.name==
"assign")
259 else if(element.name==
"functioncall")
264 else if(element.name==
"thread_start")
268 else if(element.name==
"thread_end")
274 std::cout <<
"Unknown instruction type encountered (" 275 << element.name <<
")\n";
279 xmlt::elementst::const_iterator eit=element.elements.begin();
280 for(
const auto &sub : element.elements)
282 if(sub.name==
"location")
287 else if(sub.name==
"variables")
290 else if(sub.name==
"labels")
292 xmlt::elementst::const_iterator lit=sub.elements.begin();
293 for(; lit != sub.elements.end(); lit++)
295 if(lit->name==
"label")
297 std::string ls=lit->get_attribute(
"name");
298 inst->labels.push_back(ls);
302 std::cout <<
"Unknown node in labels section.\n";
307 else if(sub.name==
"guard")
309 inst->guard.remove(
"value");
313 else if(sub.name==
"code")
318 else if(sub.name==
"targets")
322 else if(sub.name==
"comment")
324 inst->location.set(
"comment", sub.data);
326 else if(sub.name==
"function")
328 inst->function=sub.data;
338 for(
const auto &element : xml.
elements)
340 if(ins_it==instructions.end())
343 for(
const auto &sub : element.elements)
345 if(sub.name==
"targets")
347 for(
const auto &t : sub.elements)
353 if(tins!=instructions.end())
357 ins_it->targets.push_back(tins);
361 std::cout <<
"Warning: instruction not found when " 362 "resolving target links.\n";
367 std::cout <<
"Unknown node in targets section.\n";
390 const std::string &label)
393 for(
const auto &element : xml.
elements)
395 if(ins_it==instructions.end())
398 if(label==element.get_attribute(
"targetlabel"))
402 return instructions.end();
void update()
Update all indices.
targett add_instruction()
Adds an instruction at the end.
const std::string & id2string(const irep_idt &d)
std::list< instructiont > instructionst
void clear()
Clear the goto program.
std::string comment(const rw_set_baset::entryt &entry, bool write)
instructionst instructions
The list of instructions in the goto program.
void compute_location_numbers(unsigned &nr)
Compute location numbers.
void reference_convert(const irept &irep, xmlt &xml)
xmlt xml(const source_locationt &location)
void convert(const goto_programt &, xmlt &)
constructs the xml structure according to the goto program and the namespace into the given xml objec...
XML-irep conversions with hashing.
goto_programt::targett find_instruction(const xmlt &, goto_programt::instructionst &, const std::string &)
finds the index of the instruction labelled with the given target label in the given xml-program ...
void resolve_references(const irept &cur)
resolves references to ireps from an irep after reading an irep hash map into memory.
void convert(const irept &irep, xmlt &xml)
void set_attribute(const std::string &attribute, unsigned value)
xml_irep_convertt irepconverter
xmlt & new_element(const std::string &name)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Convert goto programs into xml structures and back (with irep hashing)
instructionst::iterator targett