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,
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 }
136 
137 
139  goto_functionst &goto_functions,
140  queuet &queue,
141  jumpst &jumps,
142  decl_deadt &decl_dead,
143  const dependence_grapht &dep_graph)
144 {
145  std::vector<cfgt::entryt> dep_node_to_cfg;
146  dep_node_to_cfg.reserve(dep_graph.size());
147  for(unsigned i=0; i<dep_graph.size(); ++i)
148  {
149  cfgt::entry_mapt::const_iterator entry=
150  cfg.entry_map.find(dep_graph[i].PC);
151  assert(entry!=cfg.entry_map.end());
152 
153  dep_node_to_cfg.push_back(entry->second);
154  }
155 
156  // process queue until empty
157  while(!queue.empty())
158  {
159  while(!queue.empty())
160  {
161  cfgt::entryt e=queue.top();
162  cfgt::nodet &node=cfg[e];
163  queue.pop();
164 
165  // already done by some earlier iteration?
166  if(node.node_required)
167  continue;
168 
169  // node is required
170  node.node_required=true;
171 
172  // add data and control dependencies of node
173  add_dependencies(node, queue, dep_graph, dep_node_to_cfg);
174 
175  // retain all calls of the containing function
176  add_function_calls(node, queue, goto_functions);
177 
178  // find all the symbols it uses to add declarations
179  add_decl_dead(node, queue, decl_dead);
180  }
181 
182  // add any required jumps
183  add_jumps(queue, jumps, dep_graph.cfg_post_dominators());
184  }
185 }
186 
187 
189  const cfgt::nodet &node,
190  queuet &queue,
191  const dependence_grapht &dep_graph,
192  const dep_node_to_cfgt &dep_node_to_cfg)
193 {
194  const dependence_grapht::nodet &d_node=
195  dep_graph[dep_graph[node.PC].get_node_id()];
196 
197  for(dependence_grapht::edgest::const_iterator
198  it=d_node.in.begin();
199  it!=d_node.in.end();
200  ++it)
201  add_to_queue(queue, dep_node_to_cfg[it->first], node.PC);
202 }
203 #endif
204 
206 {
207 public:
209  const goto_modelt &model_old,
210  const goto_modelt &model_new,
212  bool compact_output);
213 
214  void operator()();
215 
216 protected:
219 
224 
226 
229 
231  {
232  SAME=0,
233  NEW=1<<0,
234  DELETED=1<<1,
239  };
240 
241  typedef std::map<goto_programt::const_targett, unsigned>
243  typedef std::map<irep_idt, goto_program_change_impactt>
245 
247 
248  void change_impact(const irep_idt &function);
249 
250  void change_impact(
251  const goto_programt &old_goto_program,
252  const goto_programt &new_goto_program,
254  goto_program_change_impactt &old_impact,
255  goto_program_change_impactt &new_impact);
256 
257  void propogate_dep_back(
258  const dependence_grapht::nodet &d_node,
259  const dependence_grapht &dep_graph,
261  bool del);
263  const dependence_grapht::nodet &d_node,
264  const dependence_grapht &dep_graph,
266  bool del);
267 
269  const irep_idt &function,
270  const goto_program_change_impactt &c_i,
271  const goto_functionst &goto_functions,
272  const namespacet &ns) const;
274  const irep_idt &function,
275  const goto_program_change_impactt &o_c_i,
276  const goto_functionst &o_goto_functions,
277  const namespacet &o_ns,
278  const goto_program_change_impactt &n_c_i,
279  const goto_functionst &n_goto_functions,
280  const namespacet &n_ns) const;
281 
282  void output_instruction(char prefix,
284  const namespacet &ns,
285  const irep_idt &function,
286  goto_programt::const_targett &target) const;
287 };
288 
290  const goto_modelt &model_old,
291  const goto_modelt &model_new,
292  impact_modet _impact_mode,
293  bool _compact_output):
294  impact_mode(_impact_mode),
295  compact_output(_compact_output),
296  old_goto_functions(model_old.goto_functions),
297  ns_old(model_old.symbol_table),
298  new_goto_functions(model_new.goto_functions),
299  ns_new(model_new.symbol_table),
300  unified_diff(model_old, model_new),
301  old_dep_graph(ns_old),
302  new_dep_graph(ns_new)
303 {
304  // syntactic difference?
305  if(!unified_diff())
306  return;
307 
308  // compute program dependence graph of old code
310 
311  // compute program dependence graph of new code
313 }
314 
316 {
318 
319  if(diff.empty())
320  return;
321 
322  goto_functionst::function_mapt::const_iterator old_fit=
323  old_goto_functions.function_map.find(function);
324  goto_functionst::function_mapt::const_iterator new_fit=
325  new_goto_functions.function_map.find(function);
326 
327  goto_programt empty;
328 
329  const goto_programt &old_goto_program=
330  old_fit==old_goto_functions.function_map.end() ?
331  empty :
332  old_fit->second.body;
333  const goto_programt &new_goto_program=
334  new_fit==new_goto_functions.function_map.end() ?
335  empty :
336  new_fit->second.body;
337 
339  old_goto_program,
340  new_goto_program,
341  diff,
342  old_change_impact[function],
343  new_change_impact[function]);
344 }
345 
347  const goto_programt &old_goto_program,
348  const goto_programt &new_goto_program,
350  goto_program_change_impactt &old_impact,
351  goto_program_change_impactt &new_impact)
352 {
354  old_goto_program.instructions.begin();
356  new_goto_program.instructions.begin();
357 
358  for(const auto &d : diff)
359  {
360  switch(d.second)
361  {
363  assert(o_it!=old_goto_program.instructions.end());
364  assert(n_it!=new_goto_program.instructions.end());
365  old_impact[o_it]|=SAME;
366  ++o_it;
367  assert(n_it==d.first);
368  new_impact[n_it]|=SAME;
369  ++n_it;
370  break;
372  assert(o_it!=old_goto_program.instructions.end());
373  assert(o_it==d.first);
374  {
375  const dependence_grapht::nodet &d_node=
376  old_dep_graph[old_dep_graph[o_it].get_node_id()];
377 
381  d_node,
384  true);
388  d_node,
391  true);
392  }
393  old_impact[o_it]|=DELETED;
394  ++o_it;
395  break;
397  assert(n_it!=new_goto_program.instructions.end());
398  assert(n_it==d.first);
399  {
400  const dependence_grapht::nodet &d_node=
401  new_dep_graph[new_dep_graph[n_it].get_node_id()];
402 
406  d_node,
409  false);
413  d_node,
416  false);
417  }
418  new_impact[n_it]|=NEW;
419  ++n_it;
420  break;
421  }
422  }
423 }
424 
425 
427  const dependence_grapht::nodet &d_node,
428  const dependence_grapht &dep_graph,
430  bool del)
431 {
432  for(dependence_grapht::edgest::const_iterator it = d_node.out.begin();
433  it != d_node.out.end(); ++it)
434  {
435  goto_programt::const_targett src = dep_graph[it->first].PC;
436 
437  mod_flagt data_flag = del ? DEL_DATA_DEP : NEW_DATA_DEP;
438  mod_flagt ctrl_flag = del ? DEL_CTRL_DEP : NEW_CTRL_DEP;
439 
440  if((change_impact[src->function][src] &data_flag)
441  || (change_impact[src->function][src] &ctrl_flag))
442  continue;
443  if(it->second.get() == dep_edget::kindt::DATA
444  || it->second.get() == dep_edget::kindt::BOTH)
445  change_impact[src->function][src] |= data_flag;
446  else
447  change_impact[src->function][src] |= ctrl_flag;
448  propogate_dep_forward(dep_graph[dep_graph[src].get_node_id()], dep_graph,
449  change_impact, del);
450  }
451 }
452 
454  const dependence_grapht::nodet &d_node,
455  const dependence_grapht &dep_graph,
457  bool del)
458 {
459  for(dependence_grapht::edgest::const_iterator it = d_node.in.begin();
460  it != d_node.in.end(); ++it)
461  {
462  goto_programt::const_targett src = dep_graph[it->first].PC;
463 
464  mod_flagt data_flag = del ? DEL_DATA_DEP : NEW_DATA_DEP;
465  mod_flagt ctrl_flag = del ? DEL_CTRL_DEP : NEW_CTRL_DEP;
466 
467  if((change_impact[src->function][src] &data_flag)
468  || (change_impact[src->function][src] &ctrl_flag))
469  {
470  continue;
471  }
472  if(it->second.get() == dep_edget::kindt::DATA
473  || it->second.get() == dep_edget::kindt::BOTH)
474  change_impact[src->function][src] |= data_flag;
475  else
476  change_impact[src->function][src] |= ctrl_flag;
477 
478  propogate_dep_back(dep_graph[dep_graph[src].get_node_id()], dep_graph,
479  change_impact, del);
480  }
481 }
482 
484 {
485  // sorted iteration over intersection(old functions, new functions)
486  typedef std::map<irep_idt,
487  goto_functionst::function_mapt::const_iterator>
488  function_mapt;
489 
490  function_mapt old_funcs, new_funcs;
491 
493  old_funcs.insert(std::make_pair(it->first, it));
495  new_funcs.insert(std::make_pair(it->first, it));
496 
497  function_mapt::const_iterator ito=old_funcs.begin();
498  for(function_mapt::const_iterator itn=new_funcs.begin();
499  itn!=new_funcs.end();
500  ++itn)
501  {
502  while(ito!=old_funcs.end() && ito->first<itn->first)
503  ++ito;
504 
505  if(ito!=old_funcs.end() && itn->first==ito->first)
506  {
507  change_impact(itn->first);
508 
509  ++ito;
510  }
511  }
512 
513  goto_functions_change_impactt::const_iterator oc_it=
514  old_change_impact.begin();
515  for(goto_functions_change_impactt::const_iterator
516  nc_it=new_change_impact.begin();
517  nc_it!=new_change_impact.end();
518  ++nc_it)
519  {
520  for( ;
521  oc_it!=old_change_impact.end() && oc_it->first<nc_it->first;
522  ++oc_it)
524  oc_it->first,
525  oc_it->second,
527  ns_old);
528 
529  if(oc_it==old_change_impact.end() || nc_it->first<oc_it->first)
531  nc_it->first,
532  nc_it->second,
534  ns_new);
535  else
536  {
537  assert(oc_it->first==nc_it->first);
538 
540  nc_it->first,
541  oc_it->second,
543  ns_old,
544  nc_it->second,
546  ns_new);
547 
548  ++oc_it;
549  }
550  }
551 }
552 
554  const irep_idt &function,
555  const goto_program_change_impactt &c_i,
556  const goto_functionst &goto_functions,
557  const namespacet &ns) const
558 {
559  goto_functionst::function_mapt::const_iterator f_it=
560  goto_functions.function_map.find(function);
561  assert(f_it!=goto_functions.function_map.end());
562  const goto_programt &goto_program=f_it->second.body;
563 
564  if(!compact_output)
565  std::cout << "/** " << function << " **/\n";
566 
568  {
569  goto_program_change_impactt::const_iterator c_entry=
570  c_i.find(target);
571  const unsigned mod_flags=
572  c_entry==c_i.end() ? SAME : c_entry->second;
573 
574  char prefix;
575  // syntactic changes are preferred over data/control-dependence
576  // modifications
577  if(mod_flags==SAME)
578  prefix=' ';
579  else if(mod_flags&DELETED)
580  prefix='-';
581  else if(mod_flags&NEW)
582  prefix='+';
583  else if(mod_flags&NEW_DATA_DEP)
584  prefix='D';
585  else if(mod_flags&NEW_CTRL_DEP)
586  prefix='C';
587  else if(mod_flags&DEL_DATA_DEP)
588  prefix='d';
589  else if(mod_flags&DEL_CTRL_DEP)
590  prefix='c';
591  else
592  UNREACHABLE;
593 
594  output_instruction(prefix, goto_program, ns, function, target);
595  }
596 }
597 
599  const irep_idt &function,
600  const goto_program_change_impactt &o_c_i,
601  const goto_functionst &o_goto_functions,
602  const namespacet &o_ns,
603  const goto_program_change_impactt &n_c_i,
604  const goto_functionst &n_goto_functions,
605  const namespacet &n_ns) const
606 {
607  goto_functionst::function_mapt::const_iterator o_f_it=
608  o_goto_functions.function_map.find(function);
609  assert(o_f_it!=o_goto_functions.function_map.end());
610  const goto_programt &old_goto_program=o_f_it->second.body;
611 
612  goto_functionst::function_mapt::const_iterator f_it=
613  n_goto_functions.function_map.find(function);
614  assert(f_it!=n_goto_functions.function_map.end());
615  const goto_programt &goto_program=f_it->second.body;
616 
617  if(!compact_output)
618  std::cout << "/** " << function << " **/\n";
619 
621  old_goto_program.instructions.begin();
623  {
624  goto_program_change_impactt::const_iterator o_c_entry=
625  o_c_i.find(o_target);
626  const unsigned old_mod_flags=
627  o_c_entry==o_c_i.end() ? SAME : o_c_entry->second;
628 
629  if(old_mod_flags&DELETED)
630  {
631  output_instruction('-', goto_program, o_ns, function, o_target);
632  ++o_target;
633  --target;
634  continue;
635  }
636 
637  goto_program_change_impactt::const_iterator c_entry=
638  n_c_i.find(target);
639  const unsigned mod_flags=
640  c_entry==n_c_i.end() ? SAME : c_entry->second;
641 
642  char prefix;
643  // syntactic changes are preferred over data/control-dependence
644  // modifications
645  if(mod_flags==SAME)
646  {
647  if(old_mod_flags==SAME)
648  prefix=' ';
649  else if(old_mod_flags&DEL_DATA_DEP)
650  prefix='d';
651  else if(old_mod_flags&DEL_CTRL_DEP)
652  prefix='c';
653  else
654  UNREACHABLE;
655 
656  ++o_target;
657  }
658  else if(mod_flags&DELETED)
659  UNREACHABLE;
660  else if(mod_flags&NEW)
661  prefix='+';
662  else if(mod_flags&NEW_DATA_DEP)
663  {
664  prefix='D';
665 
666  assert(old_mod_flags==SAME ||
667  old_mod_flags&DEL_DATA_DEP ||
668  old_mod_flags&DEL_CTRL_DEP);
669  ++o_target;
670  }
671  else if(mod_flags&NEW_CTRL_DEP)
672  {
673  prefix='C';
674 
675  assert(old_mod_flags==SAME ||
676  old_mod_flags&DEL_DATA_DEP ||
677  old_mod_flags&DEL_CTRL_DEP);
678  ++o_target;
679  }
680  else
681  UNREACHABLE;
682 
683  output_instruction(prefix, goto_program, n_ns, function, target);
684  }
685  for( ;
686  o_target!=old_goto_program.instructions.end();
687  ++o_target)
688  {
689  goto_program_change_impactt::const_iterator o_c_entry=
690  o_c_i.find(o_target);
691  const unsigned old_mod_flags=
692  o_c_entry==o_c_i.end() ? SAME : o_c_entry->second;
693 
694  char prefix;
695  // syntactic changes are preferred over data/control-dependence
696  // modifications
697  if(old_mod_flags==SAME)
698  UNREACHABLE;
699  else if(old_mod_flags&DELETED)
700  prefix='-';
701  else if(old_mod_flags&NEW)
702  UNREACHABLE;
703  else if(old_mod_flags&DEL_DATA_DEP)
704  prefix='d';
705  else if(old_mod_flags&DEL_CTRL_DEP)
706  prefix='c';
707  else
708  UNREACHABLE;
709 
710  output_instruction(prefix, goto_program, o_ns, function, o_target);
711  }
712 }
713 
716  const namespacet &ns,
717  const irep_idt &function,
718  goto_programt::const_targett &target) const
719 {
720  if(compact_output)
721  {
722  if(prefix == ' ')
723  return;
724  const irep_idt &file=target->source_location.get_file();
725  const irep_idt &line=target->source_location.get_line();
726  if(!file.empty() && !line.empty())
727  std::cout << prefix << " " << id2string(file)
728  << " " << id2string(line) << '\n';
729  }
730  else
731  {
732  std::cout << prefix;
733  goto_program.output_instruction(ns, function, std::cout, *target);
734  }
735 }
736 
738  const goto_modelt &model_old,
739  const goto_modelt &model_new,
740  impact_modet impact_mode,
741  bool compact_output)
742 {
743  change_impactt c(model_old, model_new, impact_mode, compact_output);
744  c();
745 }
impact_modet impact_mode
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:289
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:43
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:341
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
entry_mapt entry_map
Definition: cfg.h:106
exprt & symbol()
Definition: std_code.h:266
impact_modet
Definition: change_impact.h:18
const irep_idt & get_identifier() const
Definition: std_expr.h:128
Data and control-dependencies of syntactic diff.
std::unordered_map< irep_idt, queuet > decl_deadt
const namespacet ns_new
static bool implicit(goto_programt::const_targett target)
function_mapt function_map
void change_impact(const irep_idt &function)
std::map< goto_programt::const_targett, unsigned > goto_program_change_impactt
goto_program_difft get_diff(const irep_idt &function) const
std::size_t entryt
Definition: cfg.h:65
edgest in
Definition: graph.h:42
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.
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:136
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
instructionst::const_iterator const_targett
Definition: goto_program.h:398
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:74
std::list< cfgt::entryt > jumpst
const post_dominators_mapt & cfg_post_dominators() const
std::size_t size() const
Definition: graph.h:178
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
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:318
goto_functions_change_impactt new_change_impact
Unified diff (using LCSS) of goto functions.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
void add_to_queue(queuet &queue, const cfgt::entryt &entry, goto_programt::const_targett reason)
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &it) const
Output a single instruction.
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:42
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
std::string to_string(const string_constraintt &expr)
Used for debug printing.
#define Forall_goto_functions(it, functions)
#define UNREACHABLE
Definition: invariant.h:250
goto_programt coverage_criteriont criterion
Definition: cover.cpp:63
goto_programt & goto_program
Definition: cover.cpp:63
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
std::map< irep_idt, goto_program_change_impactt > goto_functions_change_impactt
dstringt irep_idt
Definition: irep.h:31
std::list< std::pair< goto_programt::const_targett, differencet > > goto_program_difft
Definition: unified_diff.h:47
void operator()(goto_functionst &goto_functions, const namespacet &ns, slicing_criteriont &criterion)
#define forall_goto_functions(it, functions)
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:735
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