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
// Comparing iterators is safe as the target must be within the same list
27
// of instructions because this is a GOTO.
28
exprt
tmp(from_l->guard);
29
30
goto_programt::const_targett
next=from_l;
31
next++;
32
if
(next==to_l)
33
tmp.
make_not
();
34
35
simplify
(tmp, ns);
36
invariant_set
.
strengthen
(tmp);
37
}
38
break
;
39
40
case
ASSERT
:
41
case
ASSUME
:
42
{
43
exprt
tmp(from_l->guard);
44
simplify
(tmp, ns);
45
invariant_set
.
strengthen
(tmp);
46
}
47
break
;
48
49
case
RETURN
:
50
// ignore
51
break
;
52
53
case
ASSIGN
:
54
{
55
const
code_assignt
&assignment=
to_code_assign
(from_l->code);
56
invariant_set
.
assignment
(assignment.
lhs
(), assignment.
rhs
());
57
}
58
break
;
59
60
case
OTHER
:
61
if
(from_l->code.is_not_nil())
62
invariant_set
.
apply_code
(from_l->code);
63
break
;
64
65
case
DECL
:
66
invariant_set
.
apply_code
(from_l->code);
67
break
;
68
69
case
FUNCTION_CALL
:
70
invariant_set
.
apply_code
(from_l->code);
71
break
;
72
73
case
START_THREAD
:
74
invariant_set
.
make_threaded
();
75
break
;
76
77
default
:
78
{
79
// do nothing
80
}
81
}
82
}
invariant_set_domain.h
Value Set.
ASSUME
Definition:
goto_program.h:33
simplify_expr.h
invariant_sett::strengthen
void strengthen(const exprt &expr)
Definition:
invariant_set.cpp:390
invariant_sett::assignment
void assignment(const exprt &lhs, const exprt &rhs)
Definition:
invariant_set.cpp:1051
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition:
std_code.h:239
code_assignt::lhs
exprt & lhs()
Definition:
std_code.h:208
invariant_sett::make_threaded
void make_threaded()
Definition:
invariant_set.h:132
RETURN
Definition:
goto_program.h:43
code_assignt::rhs
exprt & rhs()
Definition:
std_code.h:213
invariant_sett::apply_code
void apply_code(const codet &code)
Definition:
invariant_set.cpp:1070
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition:
goto_program.h:398
namespacet
TO_BE_DOCUMENTED.
Definition:
namespace.h:74
invariant_set_domaint::invariant_set
invariant_sett invariant_set
Definition:
invariant_set_domain.h:28
START_THREAD
Definition:
goto_program.h:37
invariant_set_domaint::transform
virtual void transform(locationt from_l, locationt to_l, ai_baset &ai, const namespacet &ns) final override
Definition:
invariant_set_domain.cpp:16
ASSERT
Definition:
goto_program.h:34
ASSIGN
Definition:
goto_program.h:44
FUNCTION_CALL
Definition:
goto_program.h:47
exprt::make_not
void make_not()
Definition:
expr.cpp:91
ai_baset
Definition:
ai.h:128
exprt
Base class for all expressions.
Definition:
expr.h:42
ai_domain_baset::locationt
goto_programt::const_targett locationt
Definition:
ai.h:44
OTHER
Definition:
goto_program.h:35
DECL
Definition:
goto_program.h:45
GOTO
Definition:
goto_program.h:32
code_assignt
Assignment.
Definition:
std_code.h:195
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition:
simplify_expr.cpp:2424
analyses
invariant_set_domain.cpp
Generated by
1.8.14