cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
show_value_sets.cpp
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
#include "
show_value_sets.h
"
13
#include "
value_set_analysis.h
"
14
15
#include <
util/xml.h
>
16
17
#include <iostream>
18
19
void
show_value_sets
(
20
ui_message_handlert::uit
ui,
21
const
goto_modelt
&goto_model,
22
const
value_set_analysist
&value_set_analysis)
23
{
24
switch
(ui)
25
{
26
case
ui_message_handlert::uit::XML_UI
:
27
std::cout << value_set_analysis.
output_xml
(goto_model);
28
break
;
29
30
case
ui_message_handlert::uit::PLAIN
:
31
value_set_analysis.
output
(goto_model, std::cout);
32
break
;
33
34
case
ui_message_handlert::uit::JSON_UI
:
35
std::cout << value_set_analysis.
output_json
(goto_model);
36
break
;
37
}
38
}
39
40
void
show_value_sets
(
41
ui_message_handlert::uit
ui,
42
const
namespacet
&ns,
43
const
irep_idt
&function_name,
44
const
goto_programt
&goto_program,
45
const
value_set_analysist
&value_set_analysis)
46
{
47
switch
(ui)
48
{
49
case
ui_message_handlert::uit::XML_UI
:
50
std::cout << value_set_analysis.
output_xml
(ns, function_name, goto_program);
51
break
;
52
53
case
ui_message_handlert::uit::PLAIN
:
54
value_set_analysis.
output
(ns, function_name, goto_program, std::cout);
55
break
;
56
57
case
ui_message_handlert::uit::JSON_UI
:
58
std::cout << value_set_analysis.
output_json
(
59
ns, function_name, goto_program);
60
break
;
61
}
62
}
ai_baset::output
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
Definition
ai.cpp:39
ai_baset::output_xml
virtual xmlt output_xml(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program) const
Output the abstract states for a single function as XML.
Definition
ai.cpp:136
ai_baset::output_json
virtual jsont output_json(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program) const
Output the abstract states for a single function as JSON.
Definition
ai.cpp:83
goto_modelt
Definition
goto_model.h:27
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition
goto_program.h:72
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition
namespace.h:91
ui_message_handlert::uit
uit
Definition
ui_message.h:24
ui_message_handlert::uit::JSON_UI
@ JSON_UI
Definition
ui_message.h:24
ui_message_handlert::uit::XML_UI
@ XML_UI
Definition
ui_message.h:24
ui_message_handlert::uit::PLAIN
@ PLAIN
Definition
ui_message.h:24
show_value_sets
void show_value_sets(ui_message_handlert::uit ui, const goto_modelt &goto_model, const value_set_analysist &value_set_analysis)
Definition
show_value_sets.cpp:19
show_value_sets.h
Show Value Sets.
value_set_analysis.h
Value Set Propagation.
value_set_analysist
value_set_analysis_templatet< value_set_domain_templatet< value_sett > > value_set_analysist
Definition
value_set_analysis.h:53
irep_idt
dstringt irep_idt
Definition
verification_result.h:16
xml.h
pointer-analysis
show_value_sets.cpp
Generated by
1.17.0