cprover
value_set_domain.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Value Set
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#include "
value_set_domain.h
"
13
14
#include <
util/std_code.h
>
15
16
void
value_set_domaint::transform
(
17
const
namespacet
&ns,
18
locationt
from_l,
19
locationt
to_l)
20
{
21
switch
(from_l->type)
22
{
23
case
GOTO
:
24
// ignore for now
25
break
;
26
27
case
END_FUNCTION
:
28
value_set
.
do_end_function
(
static_analysis_baset::get_return_lhs
(to_l), ns);
29
break
;
30
31
case
RETURN
:
32
case
OTHER
:
33
case
ASSIGN
:
34
case
DECL
:
35
value_set
.
apply_code
(from_l->code, ns);
36
break
;
37
38
case
ASSUME
:
39
value_set
.
guard
(from_l->guard, ns);
40
break
;
41
42
case
FUNCTION_CALL
:
43
{
44
const
code_function_callt
&code=
45
to_code_function_call
(from_l->code);
46
47
value_set
.
do_function_call
(to_l->function, code.
arguments
(), ns);
48
}
49
break
;
50
51
default
:
52
{
53
// do nothing
54
}
55
}
56
}
FUNCTION_CALL
Definition:
goto_program_template.h:46
ASSUME
Definition:
goto_program_template.h:32
RETURN
Definition:
goto_program_template.h:42
static_analysis_baset::get_return_lhs
static exprt get_return_lhs(locationt to)
Definition:
static_analysis.cpp:43
domain_baset::locationt
goto_programt::const_targett locationt
Definition:
static_analysis.h:38
std_code.h
code_function_callt::arguments
argumentst & arguments()
Definition:
std_code.h:689
value_set_domaint::value_set
value_sett value_set
Definition:
value_set_domain.h:23
value_sett::do_function_call
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
Definition:
value_set.cpp:1423
namespacet
TO_BE_DOCUMENTED.
Definition:
namespace.h:62
code_function_callt
A function call.
Definition:
std_code.h:657
value_set_domain.h
Value Set.
GOTO
Definition:
goto_program_template.h:31
DECL
Definition:
goto_program_template.h:44
value_sett::do_end_function
void do_end_function(const exprt &lhs, const namespacet &ns)
Definition:
value_set.cpp:1469
value_set_domaint::transform
virtual void transform(const namespacet &ns, locationt from_l, locationt to_l)
Definition:
value_set_domain.cpp:16
value_sett::guard
void guard(const exprt &expr, const namespacet &ns)
Definition:
value_set.cpp:1616
END_FUNCTION
Definition:
goto_program_template.h:39
OTHER
Definition:
goto_program_template.h:34
value_sett::apply_code
void apply_code(const codet &code, const namespacet &ns)
Definition:
value_set.cpp:1481
ASSIGN
Definition:
goto_program_template.h:43
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition:
std_code.h:700
pointer-analysis
value_set_domain.cpp
Generated by
1.8.14