28 std::stringstream tmp;
35 if(!inst.location.is_nil())
40 if(!inst.labels.empty())
43 for(goto_programt::instructiont::labelst::const_iterator
44 l_it=inst.labels.begin();
45 l_it!=inst.labels.end();
53 if(inst.target_number!=0)
57 tmp << inst.target_number;
66 if(!inst.guard.is_true())
72 for(goto_programt::instructiont::targetst::const_iterator
73 gt_it=inst.targets.begin();
74 gt_it!=inst.targets.end();
78 tmp << (*gt_it)->target_number;
116 ins.
name=
"end_function";
128 ins.
name=
"atomic_begin";
132 ins.
name=
"atomic_end";
145 ins.
name=
"instruction";
161 ins.
name=
"functioncall";
169 ins.
name=
"thread_start";
171 if(inst.targets.size()==1)
174 tmp << inst.targets.front()->target_number;
181 ins.
name=
"thread_end";
189 if(inst.function!=
"")
204 goto_program.
clear();
207 xmlt::elementst::const_iterator it =
xml.
elements.begin();
211 inst->targets.clear();
217 else if(it->name==
"assume")
221 else if(it->name==
"assert")
225 else if(it->name==
"skip")
229 else if(it->name==
"end_function")
233 else if(it->name==
"location")
237 else if(it->name==
"dead")
241 else if(it->name==
"atomic_begin")
245 else if(it->name==
"atomic_end")
249 else if(it->name==
"return")
253 else if(it->name==
"instruction")
257 else if(it->name==
"assign")
262 else if(it->name==
"functioncall")
267 else if(it->name==
"thread_start")
271 else if(it->name==
"thread_end")
277 std::cout <<
"Unknown instruction type encountered (" << it->name
282 xmlt::elementst::const_iterator eit = it->elements.begin();
283 for(; eit != it->elements.end(); eit++)
285 if(eit->name==
"location")
289 else if(eit->name==
"variables")
292 else if(eit->name==
"labels")
294 xmlt::elementst::const_iterator lit = eit->elements.begin();
295 for(; lit != eit->elements.end(); lit++)
297 if(lit->name==
"label")
299 std::string ls = lit->get_attribute(
"name");
300 inst->labels.push_back(ls);
304 std::cout <<
"Unknown node in labels section.\n";
309 else if(eit->name==
"guard")
311 inst->guard.remove(
"value");
314 else if(eit->name==
"code")
318 else if(eit->name==
"targets")
322 else if(eit->name==
"comment")
324 inst->location.set(
"comment", eit->data);
326 else if(eit->name==
"function")
328 inst->function = eit->data;
339 for(; it !=
xml.
elements.end() && ins_it!=instructions.end(); it++)
341 xmlt::elementst::const_iterator eit = it->elements.begin();
342 for(; eit != it->elements.end(); eit++)
344 if(eit->name==
"targets")
346 xmlt::elementst::const_iterator tit = eit->elements.begin();
347 for(; tit != eit->elements.end(); tit++)
349 if(tit->name==
"target")
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";
394 xmlt::elementst::const_iterator it=
xml.
elements.begin();
396 for(; it !=
xml.
elements.end() && ins_it!=instructions.end(); it++)
398 if(label==it->get_attribute(
"targetlabel"))
404 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.
xmlt xml(const source_locationt &location)
void set_attribute(const std::string &attribute, unsigned value)
goto_programt::targett find_instruction(const xmlt &xml, goto_programt::instructionst &instructions, const irep_idt &label)
finds the index of the instruction labelled with the given target label in the given xml-program ...
Convert goto programs into xml structures and back.
xmlt & new_element(const std::string &name)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
void convert(const goto_programt &goto_program, xmlt &xml)
constructs the xml structure according to the goto program and the namespace into the given xml objec...
instructionst::iterator targett