cprover
Loading...
Searching...
No Matches
show_value_sets.cpp
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#include "show_value_sets.h"
13#include "value_set_analysis.h"
14
16
17#include <util/invariant.h>
18#include <util/xml.h>
19
20#include <iostream>
21
24 const goto_modelt &goto_model,
25 const value_set_analysist &value_set_analysis)
26{
27 switch(ui)
28 {
30 {
31 xmlt xml;
32 convert(goto_model.goto_functions, value_set_analysis, xml);
33 std::cout << xml << '\n';
34 }
35 break;
36
38 value_set_analysis.output(goto_model.goto_functions, std::cout);
39 break;
40
43 }
44}
45
48 const goto_programt &goto_program,
49 const value_set_analysist &value_set_analysis)
50{
51 switch(ui)
52 {
54 {
55 xmlt xml;
56 convert(goto_program, value_set_analysis, xml);
57 std::cout << xml << '\n';
58 }
59 break;
60
62 value_set_analysis.output(goto_program, std::cout);
63 break;
64
67 }
68}
static bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_tablet &symbol_table, message_handlert &message_handler)
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
virtual void output(const goto_functionst &goto_functions, std::ostream &out) const
This template class implements a data-flow analysis which keeps track of what values different variab...
Definition: xml.h:21
Symbol Table + CFG.
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:108
void show_value_sets(ui_message_handlert::uit ui, const goto_modelt &goto_model, const value_set_analysist &value_set_analysis)
Show Value Sets.
#define UNIMPLEMENTED
Definition: invariant.h:525
Value Set Propagation.