cprover
invariant_set_domain.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Invariant Set Domain
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#include "
invariant_set_domain.h
"
13
14
#include <
util/simplify_expr.h
>
15
16
void
invariant_set_domaint::transform
(
17
locationt
from_l,
18
locationt
to_l,
19
ai_baset
&ai,
20
const
namespacet
&ns)
21
{
22
switch
(from_l->type)
23
{
24
case
GOTO
:
25
{
26
exprt
tmp(from_l->guard);
27
28
goto_programt::const_targett
next=from_l;
29
next++;
30
if
(next==to_l)
31
tmp.
make_not
();
32
33
simplify
(tmp, ns);
34
invariant_set
.
strengthen
(tmp);
35
}
36
break
;
37
38
case
ASSERT
:
39
case
ASSUME
:
40
{
41
exprt
tmp(from_l->guard);
42
simplify
(tmp, ns);
43
invariant_set
.
strengthen
(tmp);
44
}
45
break
;
46
47
case
RETURN
:
48
// ignore
49
break
;
50
51
case
ASSIGN
:
52
{
53
const
code_assignt
&assignment=
to_code_assign
(from_l->code);
54
invariant_set
.
assignment
(assignment.
lhs
(), assignment.
rhs
());
55
}
56
break
;
57
58
case
OTHER
:
59
if
(from_l->code.is_not_nil())
60
invariant_set
.
apply_code
(from_l->code);
61
break
;
62
63
case
DECL
:
64
invariant_set
.
apply_code
(from_l->code);
65
break
;
66
67
case
FUNCTION_CALL
:
68
invariant_set
.
apply_code
(from_l->code);
69
break
;
70
71
case
START_THREAD
:
72
invariant_set
.
make_threaded
();
73
break
;
74
75
default
:
76
{
77
// do nothing
78
}
79
}
80
}
invariant_set_domain.h
Value Set.
simplify_expr.h
FUNCTION_CALL
Definition:
goto_program_template.h:46
START_THREAD
Definition:
goto_program_template.h:36
ASSUME
Definition:
goto_program_template.h:32
invariant_sett::strengthen
void strengthen(const exprt &expr)
Definition:
invariant_set.cpp:383
RETURN
Definition:
goto_program_template.h:42
invariant_sett::assignment
void assignment(const exprt &lhs, const exprt &rhs)
Definition:
invariant_set.cpp:1059
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition:
std_code.h:178
code_assignt::lhs
exprt & lhs()
Definition:
std_code.h:157
goto_program_templatet< codet, exprt >::const_targett
instructionst::const_iterator const_targett
Definition:
goto_program_template.h:347
invariant_sett::make_threaded
void make_threaded()
Definition:
invariant_set.h:132
code_assignt::rhs
exprt & rhs()
Definition:
std_code.h:162
invariant_sett::apply_code
void apply_code(const codet &code)
Definition:
invariant_set.cpp:1078
namespacet
TO_BE_DOCUMENTED.
Definition:
namespace.h:62
invariant_set_domaint::invariant_set
invariant_sett invariant_set
Definition:
invariant_set_domain.h:28
GOTO
Definition:
goto_program_template.h:31
invariant_set_domaint::transform
virtual void transform(locationt from_l, locationt to_l, ai_baset &ai, const namespacet &ns) final
Definition:
invariant_set_domain.cpp:16
DECL
Definition:
goto_program_template.h:44
exprt::make_not
void make_not()
Definition:
expr.cpp:100
ai_baset
Definition:
ai.h:108
exprt
Base class for all expressions.
Definition:
expr.h:46
ASSERT
Definition:
goto_program_template.h:33
ai_domain_baset::locationt
goto_programt::const_targett locationt
Definition:
ai.h:42
OTHER
Definition:
goto_program_template.h:34
ASSIGN
Definition:
goto_program_template.h:43
code_assignt
Assignment.
Definition:
std_code.h:144
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition:
simplify_expr.cpp:2384
analyses
invariant_set_domain.cpp
Generated by
1.8.14