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(cfgt::entry_mapt::iterator
70  e_it=cfg.entry_map.begin();
71  e_it!=cfg.entry_map.end();
72  e_it++)
73  {
74  if(criterion(e_it->first))
75  add_to_queue(queue, e_it->second, e_it->first);
76  else if(implicit(e_it->first))
77  add_to_queue(queue, e_it->second, e_it->first);
78  else if((e_it->first->is_goto() && e_it->first->guard.is_true()) ||
79  e_it->first->is_throw())
80  jumps.push_back(e_it->second);
81  else if(e_it->first->is_decl())
82  {
83  const exprt &s=to_code_decl(e_it->first->code).symbol();
84  decl_dead[to_symbol_expr(s).get_identifier()].push(e_it->second);
85  }
86  else if(e_it->first->is_dead())
87  {
88  const exprt &s=to_code_dead(e_it->first->code).symbol();
89  decl_dead[to_symbol_expr(s).get_identifier()].push(e_it->second);
90  }
91  }
92 
93  // compute program dependence graph (and post-dominators)
94  dependence_grapht dep_graph(ns);
95  dep_graph(goto_functions, ns);
96 
97  // compute the fixedpoint
98  fixedpoint(goto_functions, queue, jumps, decl_dead, dep_graph);
99 
100  // now replace those instructions that are not needed
101  // by skips
102 
103  Forall_goto_functions(f_it, goto_functions)
104  if(f_it->second.body_available())
105  {
106  Forall_goto_program_instructions(i_it, f_it->second.body)
107  {
108  const cfgt::entryt &e=cfg.entry_map[i_it];
109  if(!i_it->is_end_function() && // always retained
110  !cfg[e].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=cfg[e].required_by.begin();
119  req_it!=cfg[e].required_by.end();
120  ++req_it)
121  {
122  if(req_it!=cfg[e].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  // remove the skips
134  remove_skip(goto_functions);
135  goto_functions.update();
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  for(unsigned i=0; i<dep_graph.size(); ++i)
149  {
150  cfgt::entry_mapt::const_iterator entry=
151  cfg.entry_map.find(dep_graph[i].PC);
152  assert(entry!=cfg.entry_map.end());
153 
154  dep_node_to_cfg.push_back(entry->second);
155  }
156 
157  // process queue until empty
158  while(!queue.empty())
159  {
160  while(!queue.empty())
161  {
162  cfgt::entryt e=queue.top();
163  cfgt::nodet &node=cfg[e];
164  queue.pop();
165 
166  // already done by some earlier iteration?
167  if(node.node_required)
168  continue;
169 
170  // node is required
171  node.node_required=true;
172 
173  // add data and control dependencies of node
174  add_dependencies(node, queue, dep_graph, dep_node_to_cfg);
175 
176  // retain all calls of the containing function
177  add_function_calls(node, queue, goto_functions);
178 
179  // find all the symbols it uses to add declarations
180  add_decl_dead(node, queue, decl_dead);
181  }
182 
183  // add any required jumps
184  add_jumps(queue, jumps, dep_graph.cfg_post_dominators());
185  }
186 }
187 
188 
190  const cfgt::nodet &node,
191  queuet &queue,
192  const dependence_grapht &dep_graph,
193  const dep_node_to_cfgt &dep_node_to_cfg)
194 {
195  const dependence_grapht::nodet &d_node=
196  dep_graph[dep_graph[node.PC].get_node_id()];
197 
198  for(dependence_grapht::edgest::const_iterator
199  it=d_node.in.begin();
200  it!=d_node.in.end();
201  ++it)
202  add_to_queue(queue, dep_node_to_cfg[it->first], node.PC);
203 }
204 #endif
205 
207 {
208 public:
210  const goto_modelt &model_old,
211  const goto_modelt &model_new,
213  bool compact_output);
214 
215  void operator()();
216 
217 protected:
220 
225 
227 
230 
232  {
233  SAME=0,
234  NEW=1<<0,
235  DELETED=1<<1,
240  };
241 
242  typedef std::map<goto_programt::const_targett, unsigned>
244  typedef std::map<irep_idt, goto_program_change_impactt>
246 
248 
249  void change_impact(const irep_idt &function);
250 
251  void change_impact(
252  const goto_programt &old_goto_program,
253  const goto_programt &new_goto_program,
255  goto_program_change_impactt &old_impact,
256  goto_program_change_impactt &new_impact);
257 
258  void propogate_dep_back(
259  const dependence_grapht::nodet &d_node,
260  const dependence_grapht &dep_graph,
262  bool del);
264  const dependence_grapht::nodet &d_node,
265  const dependence_grapht &dep_graph,
267  bool del);
268 
270  const irep_idt &function,
271  const goto_program_change_impactt &c_i,
272  const goto_functionst &goto_functions,
273  const namespacet &ns) const;
275  const irep_idt &function,
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(char prefix,
284  const goto_programt &goto_program,
285  const namespacet &ns,
286  const irep_idt &function,
287  goto_programt::const_targett &target) const;
288 };
289 
291  const goto_modelt &model_old,
292  const goto_modelt &model_new,
293  impact_modet _impact_mode,
294  bool _compact_output):
295  impact_mode(_impact_mode),
296  compact_output(_compact_output),
297  old_goto_functions(model_old.goto_functions),
298  ns_old(model_old.symbol_table),
299  new_goto_functions(model_new.goto_functions),
300  ns_new(model_new.symbol_table),
301  unified_diff(model_old, model_new),
302  old_dep_graph(ns_old),
303  new_dep_graph(ns_new)
304 {
305  // syntactic difference?
306  if(!unified_diff())
307  return;
308 
309  // compute program dependence graph of old code
311 
312  // compute program dependence graph of new code
314 }
315 
317 {
319  unified_diff.get_diff(function, diff);
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);
326  goto_functionst::function_mapt::const_iterator new_fit=
327  new_goto_functions.function_map.find(function);
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  old_goto_program,
342  new_goto_program,
343  diff,
344  old_change_impact[function],
345  new_change_impact[function]);
346 }
347 
349  const goto_programt &old_goto_program,
350  const goto_programt &new_goto_program,
352  goto_program_change_impactt &old_impact,
353  goto_program_change_impactt &new_impact)
354 {
356  old_goto_program.instructions.begin();
358  new_goto_program.instructions.begin();
359 
360  for(const auto &d : diff)
361  {
362  switch(d.second)
363  {
365  assert(o_it!=old_goto_program.instructions.end());
366  assert(n_it!=new_goto_program.instructions.end());
367  old_impact[o_it]|=SAME;
368  ++o_it;
369  assert(n_it==d.first);
370  new_impact[n_it]|=SAME;
371  ++n_it;
372  break;
374  assert(o_it!=old_goto_program.instructions.end());
375  assert(o_it==d.first);
376  {
377  const dependence_grapht::nodet &d_node=
378  old_dep_graph[old_dep_graph[o_it].get_node_id()];
379 
383  d_node,
386  true);
390  d_node,
393  true);
394  }
395  old_impact[o_it]|=DELETED;
396  ++o_it;
397  break;
399  assert(n_it!=new_goto_program.instructions.end());
400  assert(n_it==d.first);
401  {
402  const dependence_grapht::nodet &d_node=
403  new_dep_graph[new_dep_graph[n_it].get_node_id()];
404 
408  d_node,
411  false);
415  d_node,
418  false);
419  }
420  new_impact[n_it]|=NEW;
421  ++n_it;
422  break;
423  }
424  }
425 }
426 
427 
429  const dependence_grapht::nodet &d_node,
430  const dependence_grapht &dep_graph,
432  bool del)
433 {
434  for(dependence_grapht::edgest::const_iterator it = d_node.out.begin();
435  it != d_node.out.end(); ++it)
436  {
437  goto_programt::const_targett src = dep_graph[it->first].PC;
438 
439  mod_flagt data_flag = del ? DEL_DATA_DEP : NEW_DATA_DEP;
440  mod_flagt ctrl_flag = del ? DEL_CTRL_DEP : NEW_CTRL_DEP;
441 
442  if((change_impact[src->function][src] &data_flag)
443  || (change_impact[src->function][src] &ctrl_flag))
444  continue;
445  if(it->second.get() == dep_edget::kindt::DATA
446  || it->second.get() == dep_edget::kindt::BOTH)
447  change_impact[src->function][src] |= data_flag;
448  else
449  change_impact[src->function][src] |= ctrl_flag;
450  propogate_dep_forward(dep_graph[dep_graph[src].get_node_id()], dep_graph,
451  change_impact, del);
452  }
453 }
454 
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((change_impact[src->function][src] &data_flag)
470  || (change_impact[src->function][src] &ctrl_flag))
471  {
472  continue;
473  }
474  if(it->second.get() == dep_edget::kindt::DATA
475  || it->second.get() == dep_edget::kindt::BOTH)
476  change_impact[src->function][src] |= data_flag;
477  else
478  change_impact[src->function][src] |= ctrl_flag;
479 
480  propogate_dep_back(dep_graph[dep_graph[src].get_node_id()], dep_graph,
481  change_impact, del);
482  }
483 }
484 
486 {
487  // sorted iteration over intersection(old functions, new functions)
488  typedef std::map<irep_idt,
489  goto_functionst::function_mapt::const_iterator>
490  function_mapt;
491 
492  function_mapt old_funcs, new_funcs;
493 
495  old_funcs.insert(std::make_pair(it->first, it));
497  new_funcs.insert(std::make_pair(it->first, it));
498 
499  function_mapt::const_iterator ito=old_funcs.begin();
500  for(function_mapt::const_iterator itn=new_funcs.begin();
501  itn!=new_funcs.end();
502  ++itn)
503  {
504  while(ito!=old_funcs.end() && ito->first<itn->first)
505  ++ito;
506 
507  if(ito!=old_funcs.end() && itn->first==ito->first)
508  {
509  change_impact(itn->first);
510 
511  ++ito;
512  }
513  }
514 
515  goto_functions_change_impactt::const_iterator oc_it=
516  old_change_impact.begin();
517  for(goto_functions_change_impactt::const_iterator
518  nc_it=new_change_impact.begin();
519  nc_it!=new_change_impact.end();
520  ++nc_it)
521  {
522  for( ;
523  oc_it!=old_change_impact.end() && oc_it->first<nc_it->first;
524  ++oc_it)
526  oc_it->first,
527  oc_it->second,
529  ns_old);
530 
531  if(oc_it==old_change_impact.end() || nc_it->first<oc_it->first)
533  nc_it->first,
534  nc_it->second,
536  ns_new);
537  else
538  {
539  assert(oc_it->first==nc_it->first);
540 
542  nc_it->first,
543  oc_it->second,
545  ns_old,
546  nc_it->second,
548  ns_new);
549 
550  ++oc_it;
551  }
552  }
553 }
554 
556  const irep_idt &function,
557  const goto_program_change_impactt &c_i,
558  const goto_functionst &goto_functions,
559  const namespacet &ns) const
560 {
561  goto_functionst::function_mapt::const_iterator f_it=
562  goto_functions.function_map.find(function);
563  assert(f_it!=goto_functions.function_map.end());
564  const goto_programt &goto_program=f_it->second.body;
565 
566  if(!compact_output)
567  std::cout << "/** " << function << " **/\n";
568 
569  forall_goto_program_instructions(target, goto_program)
570  {
571  goto_program_change_impactt::const_iterator c_entry=
572  c_i.find(target);
573  const unsigned mod_flags=
574  c_entry==c_i.end() ? SAME : c_entry->second;
575 
576  char prefix;
577  // syntactic changes are preferred over data/control-dependence
578  // modifications
579  if(mod_flags==SAME)
580  prefix=' ';
581  else if(mod_flags&DELETED)
582  prefix='-';
583  else if(mod_flags&NEW)
584  prefix='+';
585  else if(mod_flags&NEW_DATA_DEP)
586  prefix='D';
587  else if(mod_flags&NEW_CTRL_DEP)
588  prefix='C';
589  else if(mod_flags&DEL_DATA_DEP)
590  prefix='d';
591  else if(mod_flags&DEL_CTRL_DEP)
592  prefix='c';
593  else
594  assert(false);
595 
596  output_instruction(prefix, goto_program, ns, function, target);
597  }
598 }
599 
601  const irep_idt &function,
602  const goto_program_change_impactt &o_c_i,
603  const goto_functionst &o_goto_functions,
604  const namespacet &o_ns,
605  const goto_program_change_impactt &n_c_i,
606  const goto_functionst &n_goto_functions,
607  const namespacet &n_ns) const
608 {
609  goto_functionst::function_mapt::const_iterator o_f_it=
610  o_goto_functions.function_map.find(function);
611  assert(o_f_it!=o_goto_functions.function_map.end());
612  const goto_programt &old_goto_program=o_f_it->second.body;
613 
614  goto_functionst::function_mapt::const_iterator f_it=
615  n_goto_functions.function_map.find(function);
616  assert(f_it!=n_goto_functions.function_map.end());
617  const goto_programt &goto_program=f_it->second.body;
618 
619  if(!compact_output)
620  std::cout << "/** " << function << " **/\n";
621 
623  old_goto_program.instructions.begin();
624  forall_goto_program_instructions(target, goto_program)
625  {
626  goto_program_change_impactt::const_iterator o_c_entry=
627  o_c_i.find(o_target);
628  const unsigned old_mod_flags=
629  o_c_entry==o_c_i.end() ? SAME : o_c_entry->second;
630 
631  if(old_mod_flags&DELETED)
632  {
633  output_instruction('-', goto_program, o_ns, function, o_target);
634  ++o_target;
635  --target;
636  continue;
637  }
638 
639  goto_program_change_impactt::const_iterator c_entry=
640  n_c_i.find(target);
641  const unsigned mod_flags=
642  c_entry==n_c_i.end() ? SAME : c_entry->second;
643 
644  char prefix;
645  // syntactic changes are preferred over data/control-dependence
646  // modifications
647  if(mod_flags==SAME)
648  {
649  if(old_mod_flags==SAME)
650  prefix=' ';
651  else if(old_mod_flags&DEL_DATA_DEP)
652  prefix='d';
653  else if(old_mod_flags&DEL_CTRL_DEP)
654  prefix='c';
655  else
656  assert(false);
657 
658  ++o_target;
659  }
660  else if(mod_flags&DELETED)
661  assert(false);
662  else if(mod_flags&NEW)
663  prefix='+';
664  else if(mod_flags&NEW_DATA_DEP)
665  {
666  prefix='D';
667 
668  assert(old_mod_flags==SAME ||
669  old_mod_flags&DEL_DATA_DEP ||
670  old_mod_flags&DEL_CTRL_DEP);
671  ++o_target;
672  }
673  else if(mod_flags&NEW_CTRL_DEP)
674  {
675  prefix='C';
676 
677  assert(old_mod_flags==SAME ||
678  old_mod_flags&DEL_DATA_DEP ||
679  old_mod_flags&DEL_CTRL_DEP);
680  ++o_target;
681  }
682  else
683  assert(false);
684 
685  output_instruction(prefix, goto_program, n_ns, function, target);
686  }
687  for( ;
688  o_target!=old_goto_program.instructions.end();
689  ++o_target)
690  {
691  goto_program_change_impactt::const_iterator o_c_entry=
692  o_c_i.find(o_target);
693  const unsigned old_mod_flags=
694  o_c_entry==o_c_i.end() ? SAME : o_c_entry->second;
695 
696  char prefix;
697  // syntactic changes are preferred over data/control-dependence
698  // modifications
699  if(old_mod_flags==SAME)
700  assert(false);
701  else if(old_mod_flags&DELETED)
702  prefix='-';
703  else if(old_mod_flags&NEW)
704  assert(false);
705  else if(old_mod_flags&DEL_DATA_DEP)
706  prefix='d';
707  else if(old_mod_flags&DEL_CTRL_DEP)
708  prefix='c';
709  else
710  assert(false);
711 
712  output_instruction(prefix, goto_program, o_ns, function, o_target);
713  }
714 }
715 
717  const goto_programt &goto_program,
718  const namespacet &ns,
719  const irep_idt &function,
720  goto_programt::const_targett &target) const
721 {
722  if(compact_output)
723  {
724  if(prefix == ' ')
725  return;
726  const irep_idt &file=target->source_location.get_file();
727  const irep_idt &line=target->source_location.get_line();
728  if(!file.empty() && !line.empty())
729  std::cout << prefix << " " << id2string(file)
730  << " " << id2string(line) << '\n';
731  }
732  else
733  {
734  std::cout << prefix;
735  goto_program.output_instruction(ns, function, std::cout, target);
736  }
737 }
738 
740  const goto_modelt &model_old,
741  const goto_modelt &model_new,
742  impact_modet impact_mode,
743  bool compact_output)
744 {
745  change_impactt c(model_old, model_new, impact_mode, compact_output);
746  c();
747 }
impact_modet impact_mode
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:218
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:22
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
const namespacet ns_old
void output_change_impact(const irep_idt &function, const goto_program_change_impactt &c_i, const goto_functionst &goto_functions, const namespacet &ns) const
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:260
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
entry_mapt entry_map
Definition: cfg.h:87
exprt & symbol()
Definition: std_code.h:205
impact_modet
Definition: change_impact.h:18
instructionst instructions
The list of instructions in the goto program.
const irep_idt & get_identifier() const
Definition: std_expr.h:120
Data and control-dependencies of syntactic diff.
const namespacet ns_new
static bool implicit(goto_programt::const_targett target)
void change_impact(const irep_idt &function)
std::map< goto_programt::const_targett, unsigned > goto_program_change_impactt
std::size_t entryt
Definition: cfg.h:65
edgest in
Definition: graph.h:41
void propogate_dep_back(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
Symbol Table + CFG.
instructionst::const_iterator const_targett
std::stack< cfgt::entryt > queuet
dependence_grapht old_dep_graph
void propogate_dep_forward(const dependence_grapht::nodet &d_node, const dependence_grapht &dep_graph, goto_functions_change_impactt &change_impact, bool del)
cfg_base_nodet< cfg_nodet, goto_programt::const_targett > nodet
Definition: graph.h:135
void fixedpoint(goto_functionst &goto_functions, queuet &queue, jumpst &jumps, decl_deadt &decl_dead, const dependence_grapht &dep_graph)
TO_BE_DOCUMENTED.
Definition: namespace.h:62
std::list< cfgt::entryt > jumpst
const post_dominators_mapt & cfg_post_dominators() const
std::size_t size() const
Definition: graph.h:177
change_impactt(const goto_modelt &model_old, const goto_modelt &model_new, impact_modet impact_mode, bool compact_output)
void add_decl_dead(const cfgt::nodet &node, queuet &queue, decl_deadt &decl_dead)
Definition: full_slicer.cpp:62
const goto_functionst & old_goto_functions
void add_function_calls(const cfgt::nodet &node, queuet &queue, const goto_functionst &goto_functions)
Definition: full_slicer.cpp:38
exprt & symbol()
Definition: std_code.h:247
goto_functions_change_impactt new_change_impact
std::unordered_map< irep_idt, queuet, irep_id_hash > decl_deadt
Unified diff (using LCSS) of goto functions.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
void add_to_queue(queuet &queue, const cfgt::entryt &entry, goto_programt::const_targett reason)
void remove_skip(goto_programt &goto_program)
remove unnecessary skip statements
Definition: remove_skip.cpp:71
void output_instruction(char prefix, const goto_programt &goto_program, const namespacet &ns, const irep_idt &function, goto_programt::const_targett &target) const
dependence_grapht new_dep_graph
Base class for all expressions.
Definition: expr.h:46
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
#define Forall_goto_functions(it, functions)
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
std::map< irep_idt, goto_program_change_impactt > goto_functions_change_impactt
dstringt irep_idt
Definition: irep.h:32
std::list< std::pair< goto_programt::const_targett, differencet > > goto_program_difft
Definition: unified_diff.h:50
void get_diff(const irep_idt &function, goto_program_difft &dest) const
void operator()(goto_functionst &goto_functions, const namespacet &ns, slicing_criteriont &criterion)
#define forall_goto_functions(it, functions)
std::ostream & output_instruction(const class namespacet &ns, const irep_idt &identifier, std::ostream &out, instructionst::const_iterator it) const
See below.
void add_jumps(queuet &queue, jumpst &jumps, const dependence_grapht::post_dominators_mapt &post_dominators)
Definition: full_slicer.cpp:93
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:68
void change_impact(const goto_modelt &model_old, const goto_modelt &model_new, impact_modet impact_mode, bool compact_output)
unified_difft unified_diff
bool empty() const
Definition: dstring.h:61
goto_functions_change_impactt old_change_impact
Definition: kdev_t.h:19