CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
show_value_sets.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Show Value Sets
4
5Author: 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
18class goto_modelt;
19
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.