cprover
change_impact.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Data and control-dependencies of syntactic diff
4 
5 Author: Michael Tautschnig
6 
7 Date: 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 {
205 public:
207  const goto_modelt &model_old,
208  const goto_modelt &model_new,
210  bool compact_output);
211 
212  void operator()();
213 
214 protected:
217 
222 
224 
227 
229  {
230  SAME=0,
231  NEW=1<<0,
232  DELETED=1<<1,
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 
256  void propogate_dep_back(
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,
271  const goto_program_change_impactt &c_i,
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 
283  void output_instruction(
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 
317 void change_impactt::change_impact(const irep_idt &function_id)
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();
500  it != old_goto_functions.function_map.end();
501  ++it)
502  {
503  old_funcs.insert(std::make_pair(it->first, it));
504  }
505  for(auto it = new_goto_functions.function_map.begin();
506  it != new_goto_functions.function_map.end();
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,
570  const goto_program_change_impactt &c_i,
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
607  UNREACHABLE;
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
670  UNREACHABLE;
671 
672  ++o_target;
673  }
674  else if(mod_flags&DELETED)
675  UNREACHABLE;
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
697  UNREACHABLE;
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)
715  UNREACHABLE;
716  else if(old_mod_flags&DELETED)
717  prefix='-';
718  else if(old_mod_flags&NEW)
719  UNREACHABLE;
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
725  UNREACHABLE;
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 {
738  if(compact_output)
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
base_grapht::node_indext entryt
Definition: cfg.h:91
const entry_mapt & entries() const
Get a map from program points to their corresponding node indices.
Definition: cfg.h:259
base_grapht::nodet nodet
Definition: cfg.h:92
entryt get_node_index(const goto_programt::const_targett &program_point) const
Get the graph node index for program_point.
Definition: cfg.h:239
nodet & get_node(const goto_programt::const_targett &program_point)
Get the CFG graph node relating to program_point.
Definition: cfg.h:245
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:71
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:652
instructionst::const_iterator const_targett
Definition: goto_program.h:647
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:49
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
#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.