CBMC
show_value_sets.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Show Value Sets
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_POINTER_ANALYSIS_SHOW_VALUE_SETS_H
13 #define CPROVER_POINTER_ANALYSIS_SHOW_VALUE_SETS_H
14 
16 #include <util/ui_message.h>
17 
18 class goto_modelt;
19 
20 void show_value_sets(
22  const goto_modelt &,
23  const value_set_analysist &);
24 
25 #endif // CPROVER_POINTER_ANALYSIS_SHOW_VALUE_SETS_H
This template class implements a data-flow analysis which keeps track of what values different variab...
void show_value_sets(ui_message_handlert::uit, const goto_modelt &, const value_set_analysist &)
Value Set Propagation.