cprover
change_impact.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Data and control-dependencies of syntactic diff
4
5Author: Michael Tautschnig
6
7Date: April 2016
8
9\*******************************************************************/
10
13
14#include "change_impact.h"
15
16#include <iostream>
17
19
21
22#include "unified_diff.h"
23
24#if 0
25 struct cfg_nodet
26 {
27 cfg_nodet():node_required(false)
28 {
29 }
30
31 bool node_required;
32#ifdef DEBUG_FULL_SLICERT
33 std::set<unsigned> required_by;
34#endif
35 };
36
37 typedef cfg_baset<cfg_nodet> cfgt;
38 cfgt cfg;
39
40 typedef std::vector<cfgt::entryt> dep_node_to_cfgt;
41 typedef std::stack<cfgt::entryt> queuet;
42
43 inline void add_to_queue(
44 queuet &queue,
45 const cfgt::entryt &entry,
47 {
48#ifdef DEBUG_FULL_SLICERT
49 cfg[entry].required_by.insert(reason->location_number);
50#endif
51 queue.push(entry);
52 }
53
55 goto_functionst &goto_functions,
56 const namespacet &ns,
57 slicing_criteriont &criterion)
58{
59 // build the CFG data structure
60 cfg(goto_functions);
61
62 // fill queue with according to slicing criterion
63 queuet queue;
64 // gather all unconditional jumps as they may need to be included
65 jumpst jumps;
66 // declarations or dead instructions may be necessary as well
67 decl_deadt decl_dead;
68
69 for(const auto &entry : cfg.entries())
70 {
71 const auto &instruction = instruction_and_index.first;
72 const auto instruction_node_index = instruction_and_index.second;
73 if(criterion(instruction))
74 add_to_queue(queue, instruction_node_index, instruction);
75 else if(implicit(instruction))
76 add_to_queue(queue, instruction_node_index, instruction);
77 else if((instruction->is_goto() && instruction->guard.is_true()) ||
78 instruction->is_throw())
79 jumps.push_back(instruction_node_index);
80 else if(instruction->is_decl())
81 {
82 const auto &s=instruction->decl_symbol();
83 decl_dead[s.get_identifier()].push(instruction_node_index);
84 }
85 else if(instruction->is_dead())
86 {
87 const auto &s=instruction->dead_symbol();
88 decl_dead[s.get_identifier()].push(instruction_node_index);
89 }
90 }
91
92 // compute program dependence graph (and post-dominators)
93 dependence_grapht dep_graph(ns);
94 dep_graph(goto_functions, ns);
95
96 // compute the fixedpoint
97 fixedpoint(goto_functions, queue, jumps, decl_dead, dep_graph);
98
99 // now replace those instructions that are not needed
100 // by skips
101
102 for(auto &gf_entry : goto_functions.function_map)
103 {
104 if(gf_entry.second.body_available())
105 {
106 Forall_goto_program_instructions(i_it, gf_entry.second.body)
107 {
108 const auto &node = cfg.get_node(i_it);
109 if(!i_it->is_end_function() && // always retained
110 !node.node_required)
111 i_it->make_skip();
112#ifdef DEBUG_FULL_SLICERT
113 else
114 {
115 std::string c="ins:"+std::to_string(i_it->location_number);
116 c+=" req by:";
117 for(std::set<unsigned>::const_iterator
118 req_it=node.required_by.begin();
119 req_it!=node.required_by.end();
120 ++req_it)
121 {
122 if(req_it!=node.required_by.begin())
123 c+=",";
124 c+=std::to_string(*req_it);
125 }
126 i_it->source_location.set_column(c); // for show-goto-functions
127 i_it->source_location.set_comment(c); // for dump-c
128 }
129#endif
130 }
131 }
132 }
133
134 // remove the skips
135 remove_skip(goto_functions);
136}
137
138
140 goto_functionst &goto_functions,
141 queuet &queue,
142 jumpst &jumps,
143 decl_deadt &decl_dead,
144 const dependence_grapht &dep_graph)
145{
146 std::vector<cfgt::entryt> dep_node_to_cfg;
147 dep_node_to_cfg.reserve(dep_graph.size());
148
149 for(unsigned i=0; i<dep_graph.size(); ++i)
150 {
151 dep_node_to_cfg.push_back(cfg.get_node_index(dep_graph[i].PC));
152 }
153
154 // process queue until empty
155 while(!queue.empty())
156 {
157 while(!queue.empty())
158 {
159 cfgt::entryt e=queue.top();
160 cfgt::nodet &node=cfg[e];
161 queue.pop();
162
163 // already done by some earlier iteration?
164 if(node.node_required)
165 continue;
166
167 // node is required
168 node.node_required=true;
169
170 // add data and control dependencies of node
171 add_dependencies(node, queue, dep_graph, dep_node_to_cfg);
172
173 // retain all calls of the containing function
174 add_function_calls(node, queue, goto_functions);
175
176 // find all the symbols it uses to add declarations
177 add_decl_dead(node, queue, decl_dead);
178 }
179
180 // add any required jumps
181 add_jumps(queue, jumps, dep_graph.cfg_post_dominators());
182 }
183}
184
185
187 const cfgt::nodet &node,
188 queuet &queue,
189 const dependence_grapht &dep_graph,
190 const dep_node_to_cfgt &dep_node_to_cfg)
191{
192 const dependence_grapht::nodet &d_node=
193 dep_graph[dep_graph[node.PC].get_node_id()];
194
195 for(dependence_grapht::edgest::const_iterator
196 it=d_node.in.begin();
197 it!=d_node.in.end();
198 ++it)
199 add_to_queue(queue, dep_node_to_cfg[it->first], node.PC);
200}
201#endif
202
204{
205public:
207 const goto_modelt &model_old,
208 const goto_modelt &model_new,
210 bool compact_output);
211
212 void operator()();
213
214protected:
217
222
224
227
229 {
231 NEW=1<<0,
236 DEL_CTRL_DEP=1<<5
237 };
238
239 typedef std::map<goto_programt::const_targett, unsigned>
241 typedef std::map<irep_idt, goto_program_change_impactt>
243
245
246 void change_impact(const irep_idt &function_id);
247
248 void change_impact(
249 const irep_idt &function_id,
250 const goto_programt &old_goto_program,
251 const goto_programt &new_goto_program,
253 goto_program_change_impactt &old_impact,
254 goto_program_change_impactt &new_impact);
255
257 const irep_idt &function_id,
258 const dependence_grapht::nodet &d_node,
259 const dependence_grapht &dep_graph,
261 bool del);
263 const irep_idt &function_id,
264 const dependence_grapht::nodet &d_node,
265 const dependence_grapht &dep_graph,
267 bool del);
268
270 const irep_idt &function_id,
272 const goto_functionst &goto_functions,
273 const namespacet &ns) const;
275 const irep_idt &function_id,
276 const goto_program_change_impactt &o_c_i,
277 const goto_functionst &o_goto_functions,
278 const namespacet &o_ns,
279 const goto_program_change_impactt &n_c_i,
280 const goto_functionst &n_goto_functions,
281 const namespacet &n_ns) const;
282
284 char prefix,
285 const goto_programt &goto_program,
286 const namespacet &ns,
287 const irep_idt &function_id,
288 goto_programt::const_targett &target) const;
289};
290
292 const goto_modelt &model_old,
293 const goto_modelt &model_new,
294 impact_modet _impact_mode,
295 bool _compact_output):
296 impact_mode(_impact_mode),
297 compact_output(_compact_output),
298 old_goto_functions(model_old.goto_functions),
299 ns_old(model_old.symbol_table),
300 new_goto_functions(model_new.goto_functions),
301 ns_new(model_new.symbol_table),
302 unified_diff(model_old, model_new),
303 old_dep_graph(ns_old),
304 new_dep_graph(ns_new)
305{
306 // syntactic difference?
307 if(!unified_diff())
308 return;
309
310 // compute program dependence graph of old code
312
313 // compute program dependence graph of new code
315}
316
318{
320
321 if(diff.empty())
322 return;
323
324 goto_functionst::function_mapt::const_iterator old_fit =
325 old_goto_functions.function_map.find(function_id);
326 goto_functionst::function_mapt::const_iterator new_fit =
327 new_goto_functions.function_map.find(function_id);
328
329 goto_programt empty;
330
331 const goto_programt &old_goto_program=
332 old_fit==old_goto_functions.function_map.end() ?
333 empty :
334 old_fit->second.body;
335 const goto_programt &new_goto_program=
336 new_fit==new_goto_functions.function_map.end() ?
337 empty :
338 new_fit->second.body;
339
341 function_id,
342 old_goto_program,
343 new_goto_program,
344 diff,
345 old_change_impact[function_id],
346 new_change_impact[function_id]);
347}
348
350 const irep_idt &function_id,
351 const goto_programt &old_goto_program,
352 const goto_programt &new_goto_program,
354 goto_program_change_impactt &old_impact,
355 goto_program_change_impactt &new_impact)
356{
358 old_goto_program.instructions.begin();
360 new_goto_program.instructions.begin();
361
362 for(const auto &d : diff)
363 {
364 switch(d.second)
365 {
367 assert(o_it!=old_goto_program.instructions.end());
368 assert(n_it!=new_goto_program.instructions.end());
369 old_impact[o_it]|=SAME;
370 ++o_it;
371 assert(n_it==d.first);
372 new_impact[n_it]|=SAME;
373 ++n_it;
374 break;
376 assert(o_it!=old_goto_program.instructions.end());
377 assert(o_it==d.first);
378 {
379 const dependence_grapht::nodet &d_node=
380 old_dep_graph[old_dep_graph[o_it].get_node_id()];
381
385 function_id, d_node, old_dep_graph, old_change_impact, true);
389 function_id, d_node, old_dep_graph, old_change_impact, true);
390 }
391 old_impact[o_it]|=DELETED;
392 ++o_it;
393 break;
395 assert(n_it!=new_goto_program.instructions.end());
396 assert(n_it==d.first);
397 {
398 const dependence_grapht::nodet &d_node=
399 new_dep_graph[new_dep_graph[n_it].get_node_id()];
400
403 {
405 function_id, d_node, new_dep_graph, new_change_impact, false);
406 }
409 {
411 function_id, d_node, new_dep_graph, new_change_impact, false);
412 }
413 }
414 new_impact[n_it]|=NEW;
415 ++n_it;
416 break;
417 }
418 }
419}
420
422 const irep_idt &function_id,
423 const dependence_grapht::nodet &d_node,
424 const dependence_grapht &dep_graph,
426 bool del)
427{
428 for(dependence_grapht::edgest::const_iterator it = d_node.out.begin();
429 it != d_node.out.end(); ++it)
430 {
431 goto_programt::const_targett src = dep_graph[it->first].PC;
432
433 mod_flagt data_flag = del ? DEL_DATA_DEP : NEW_DATA_DEP;
434 mod_flagt ctrl_flag = del ? DEL_CTRL_DEP : NEW_CTRL_DEP;
435
436 if(
437 (change_impact[function_id][src] & data_flag) ||
438 (change_impact[function_id][src] & ctrl_flag))
439 continue;
440 if(it->second.get() == dep_edget::kindt::DATA
441 || it->second.get() == dep_edget::kindt::BOTH)
442 change_impact[function_id][src] |= data_flag;
443 else
444 change_impact[function_id][src] |= ctrl_flag;
446 function_id,
447 dep_graph[dep_graph[src].get_node_id()],
448 dep_graph,
450 del);
451 }
452}
453
455 const irep_idt &function_id,
456 const dependence_grapht::nodet &d_node,
457 const dependence_grapht &dep_graph,
459 bool del)
460{
461 for(dependence_grapht::edgest::const_iterator it = d_node.in.begin();
462 it != d_node.in.end(); ++it)
463 {
464 goto_programt::const_targett src = dep_graph[it->first].PC;
465
466 mod_flagt data_flag = del ? DEL_DATA_DEP : NEW_DATA_DEP;
467 mod_flagt ctrl_flag = del ? DEL_CTRL_DEP : NEW_CTRL_DEP;
468
469 if(
470 (change_impact[function_id][src] & data_flag) ||
471 (change_impact[function_id][src] & ctrl_flag))
472 {
473 continue;
474 }
475 if(it->second.get() == dep_edget::kindt::DATA
476 || it->second.get() == dep_edget::kindt::BOTH)
477 change_impact[function_id][src] |= data_flag;
478 else
479 change_impact[function_id][src] |= ctrl_flag;
480
482 function_id,
483 dep_graph[dep_graph[src].get_node_id()],
484 dep_graph,
486 del);
487 }
488}
489
491{
492 // sorted iteration over intersection(old functions, new functions)
493 typedef std::map<irep_idt,
494 goto_functionst::function_mapt::const_iterator>
495 function_mapt;
496
497 function_mapt old_funcs, new_funcs;
498
499 for(auto it = old_goto_functions.function_map.begin();
501 ++it)
502 {
503 old_funcs.insert(std::make_pair(it->first, it));
504 }
505 for(auto it = new_goto_functions.function_map.begin();
507 ++it)
508 {
509 new_funcs.insert(std::make_pair(it->first, it));
510 }
511
512 function_mapt::const_iterator ito=old_funcs.begin();
513 for(function_mapt::const_iterator itn=new_funcs.begin();
514 itn!=new_funcs.end();
515 ++itn)
516 {
517 while(ito!=old_funcs.end() && ito->first<itn->first)
518 ++ito;
519
520 if(ito!=old_funcs.end() && itn->first==ito->first)
521 {
522 change_impact(itn->first);
523
524 ++ito;
525 }
526 }
527
528 goto_functions_change_impactt::const_iterator oc_it=
529 old_change_impact.begin();
530 for(goto_functions_change_impactt::const_iterator
531 nc_it=new_change_impact.begin();
532 nc_it!=new_change_impact.end();
533 ++nc_it)
534 {
535 for( ;
536 oc_it!=old_change_impact.end() && oc_it->first<nc_it->first;
537 ++oc_it)
539 oc_it->first,
540 oc_it->second,
542 ns_old);
543
544 if(oc_it==old_change_impact.end() || nc_it->first<oc_it->first)
546 nc_it->first,
547 nc_it->second,
549 ns_new);
550 else
551 {
552 assert(oc_it->first==nc_it->first);
553
555 nc_it->first,
556 oc_it->second,
558 ns_old,
559 nc_it->second,
561 ns_new);
562
563 ++oc_it;
564 }
565 }
566}
567
569 const irep_idt &function_id,
571 const goto_functionst &goto_functions,
572 const namespacet &ns) const
573{
574 goto_functionst::function_mapt::const_iterator f_it =
575 goto_functions.function_map.find(function_id);
576 assert(f_it!=goto_functions.function_map.end());
577 const goto_programt &goto_program=f_it->second.body;
578
579 if(!compact_output)
580 std::cout << "/** " << function_id << " **/\n";
581
582 forall_goto_program_instructions(target, goto_program)
583 {
584 goto_program_change_impactt::const_iterator c_entry=
585 c_i.find(target);
586 const unsigned mod_flags =
587 c_entry == c_i.end() ? static_cast<unsigned>(SAME) : c_entry->second;
588
589 char prefix = ' ';
590 // syntactic changes are preferred over data/control-dependence
591 // modifications
592 if(mod_flags==SAME)
593 prefix=' ';
594 else if(mod_flags&DELETED)
595 prefix='-';
596 else if(mod_flags&NEW)
597 prefix='+';
598 else if(mod_flags&NEW_DATA_DEP)
599 prefix='D';
600 else if(mod_flags&NEW_CTRL_DEP)
601 prefix='C';
602 else if(mod_flags&DEL_DATA_DEP)
603 prefix='d';
604 else if(mod_flags&DEL_CTRL_DEP)
605 prefix='c';
606 else
608
609 output_instruction(prefix, goto_program, ns, function_id, target);
610 }
611}
612
614 const irep_idt &function_id,
615 const goto_program_change_impactt &o_c_i,
616 const goto_functionst &o_goto_functions,
617 const namespacet &o_ns,
618 const goto_program_change_impactt &n_c_i,
619 const goto_functionst &n_goto_functions,
620 const namespacet &n_ns) const
621{
622 goto_functionst::function_mapt::const_iterator o_f_it =
623 o_goto_functions.function_map.find(function_id);
624 assert(o_f_it!=o_goto_functions.function_map.end());
625 const goto_programt &old_goto_program=o_f_it->second.body;
626
627 goto_functionst::function_mapt::const_iterator f_it =
628 n_goto_functions.function_map.find(function_id);
629 assert(f_it!=n_goto_functions.function_map.end());
630 const goto_programt &goto_program=f_it->second.body;
631
632 if(!compact_output)
633 std::cout << "/** " << function_id << " **/\n";
634
636 old_goto_program.instructions.begin();
637 forall_goto_program_instructions(target, goto_program)
638 {
639 goto_program_change_impactt::const_iterator o_c_entry=
640 o_c_i.find(o_target);
641 const unsigned old_mod_flags = o_c_entry == o_c_i.end()
642 ? static_cast<unsigned>(SAME)
643 : o_c_entry->second;
644
645 if(old_mod_flags&DELETED)
646 {
647 output_instruction('-', goto_program, o_ns, function_id, o_target);
648 ++o_target;
649 --target;
650 continue;
651 }
652
653 goto_program_change_impactt::const_iterator c_entry=
654 n_c_i.find(target);
655 const unsigned mod_flags =
656 c_entry == n_c_i.end() ? static_cast<unsigned>(SAME) : c_entry->second;
657
658 char prefix = ' ';
659 // syntactic changes are preferred over data/control-dependence
660 // modifications
661 if(mod_flags==SAME)
662 {
663 if(old_mod_flags==SAME)
664 prefix=' ';
665 else if(old_mod_flags&DEL_DATA_DEP)
666 prefix='d';
667 else if(old_mod_flags&DEL_CTRL_DEP)
668 prefix='c';
669 else
671
672 ++o_target;
673 }
674 else if(mod_flags&DELETED)
676 else if(mod_flags&NEW)
677 prefix='+';
678 else if(mod_flags&NEW_DATA_DEP)
679 {
680 prefix='D';
681
682 assert(old_mod_flags==SAME ||
683 old_mod_flags&DEL_DATA_DEP ||
684 old_mod_flags&DEL_CTRL_DEP);
685 ++o_target;
686 }
687 else if(mod_flags&NEW_CTRL_DEP)
688 {
689 prefix='C';
690
691 assert(old_mod_flags==SAME ||
692 old_mod_flags&DEL_DATA_DEP ||
693 old_mod_flags&DEL_CTRL_DEP);
694 ++o_target;
695 }
696 else
698
699 output_instruction(prefix, goto_program, n_ns, function_id, target);
700 }
701 for( ;
702 o_target!=old_goto_program.instructions.end();
703 ++o_target)
704 {
705 goto_program_change_impactt::const_iterator o_c_entry=
706 o_c_i.find(o_target);
707 const unsigned old_mod_flags = o_c_entry == o_c_i.end()
708 ? static_cast<unsigned>(SAME)
709 : o_c_entry->second;
710
711 char prefix = ' ';
712 // syntactic changes are preferred over data/control-dependence
713 // modifications
714 if(old_mod_flags==SAME)
716 else if(old_mod_flags&DELETED)
717 prefix='-';
718 else if(old_mod_flags&NEW)
720 else if(old_mod_flags&DEL_DATA_DEP)
721 prefix='d';
722 else if(old_mod_flags&DEL_CTRL_DEP)
723 prefix='c';
724 else
726
727 output_instruction(prefix, goto_program, o_ns, function_id, o_target);
728 }
729}
730
732 char prefix,
733 const goto_programt &goto_program,
734 const namespacet &ns,
735 const irep_idt &function_id,
736 goto_programt::const_targett &target) const
737{
739 {
740 if(prefix == ' ')
741 return;
742 const irep_idt &file = target->source_location().get_file();
743 const irep_idt &line = target->source_location().get_line();
744 if(!file.empty() && !line.empty())
745 std::cout << prefix << " " << id2string(file)
746 << " " << id2string(line) << '\n';
747 }
748 else
749 {
750 std::cout << prefix;
751 goto_program.output_instruction(ns, function_id, std::cout, *target);
752 }
753}
754
756 const goto_modelt &model_old,
757 const goto_modelt &model_new,
758 impact_modet impact_mode,
759 bool compact_output)
760{
761 change_impactt c(model_old, model_new, impact_mode, compact_output);
762 c();
763}
void change_impact(const goto_modelt &model_old, const goto_modelt &model_new, impact_modet impact_mode, bool compact_output)
Data and control-dependencies of syntactic diff.
impact_modet
Definition: change_impact.h:18
const entry_mapt & entries() const
Get a map from program points to their corresponding node indices.
Definition: cfg.h:259
base_grapht::node_indext entryt
Definition: cfg.h:91
base_grapht::nodet nodet
Definition: cfg.h:92
nodet & get_node(const goto_programt::const_targett &program_point)
Get the CFG graph node relating to program_point.
Definition: cfg.h:245
entryt get_node_index(const goto_programt::const_targett &program_point) const
Get the graph node index for program_point.
Definition: cfg.h:239
goto_functions_change_impactt old_change_impact
void output_instruction(char prefix, const goto_programt &goto_program, const namespacet &ns, const irep_idt &function_id, goto_programt::const_targett &target) const
unified_difft unified_diff
void change_impact(const irep_idt &function_id)
change_impactt(const goto_modelt &model_old, const goto_modelt &model_new, impact_modet impact_mode, bool compact_output)
dependence_grapht new_dep_graph
void propogate_dep_back(const irep_idt &function_id, const dependence_grapht::nodet &d_node, const dependence_grapht &dep_graph, goto_functions_change_impactt &change_impact, bool del)
std::map< goto_programt::const_targett, unsigned > goto_program_change_impactt
std::map< irep_idt, goto_program_change_impactt > goto_functions_change_impactt
const goto_functionst & old_goto_functions
const namespacet ns_old
goto_functions_change_impactt new_change_impact
void output_change_impact(const irep_idt &function_id, const goto_program_change_impactt &c_i, const goto_functionst &goto_functions, const namespacet &ns) const
dependence_grapht old_dep_graph
void propogate_dep_forward(const irep_idt &function_id, const dependence_grapht::nodet &d_node, const dependence_grapht &dep_graph, goto_functions_change_impactt &change_impact, bool del)
const goto_functionst & new_goto_functions
const namespacet ns_new
impact_modet impact_mode
const post_dominators_mapt & cfg_post_dominators() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
std::string::const_iterator begin() const
Definition: dstring.h:176
void add_function_calls(const cfgt::nodet &node, queuet &queue, const goto_functionst &goto_functions)
Definition: full_slicer.cpp:37
std::list< cfgt::entryt > jumpst
void add_to_queue(queuet &queue, const cfgt::entryt &entry, goto_programt::const_targett reason)
std::unordered_map< irep_idt, queuet > decl_deadt
void add_dependencies(const cfgt::nodet &node, queuet &queue, const dependence_grapht &dep_graph, const dep_node_to_cfgt &dep_node_to_cfg)
Definition: full_slicer.cpp:21
void fixedpoint(goto_functionst &goto_functions, queuet &queue, jumpst &jumps, decl_deadt &decl_dead, const dependence_grapht &dep_graph)
void add_decl_dead(const cfgt::nodet &node, queuet &queue, decl_deadt &decl_dead)
Definition: full_slicer.cpp:55
void operator()(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
std::stack< cfgt::entryt > queuet
void add_jumps(queuet &queue, jumpst &jumps, const dependence_grapht::post_dominators_mapt &post_dominators)
Definition: full_slicer.cpp:86
A collection of goto functions.
function_mapt function_map
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
instructionst::const_iterator const_targett
Definition: goto_program.h:593
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
edgest in
Definition: graph.h:42
dep_nodet nodet
Definition: graph.h:169
std::size_t size() const
Definition: graph.h:212
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
std::list< std::pair< goto_programt::const_targett, differencet > > goto_program_difft
Definition: unified_diff.h:46
goto_program_difft get_diff(const irep_idt &function) const
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
static bool implicit(goto_programt::const_targett target)
Symbol Table + CFG.
#define forall_goto_program_instructions(it, program)
#define Forall_goto_program_instructions(it, program)
dstringt irep_idt
Definition: irep.h:37
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:88
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: kdev_t.h:19
Unified diff (using LCSS) of goto functions.