cprover
is_threaded.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Over-approximate Concurrency for Threaded Goto Programs
4
5
Author: Daniel Kroening
6
7
Date: October 2012
8
9
\*******************************************************************/
10
13
14
#include "
is_threaded.h
"
15
16
#include "
ai.h
"
17
18
class
is_threaded_domaint
:
public
ai_domain_baset
19
{
20
public
:
21
bool
reachable
;
22
bool
is_threaded
;
23
24
is_threaded_domaint
():
25
reachable(false),
26
is_threaded(false)
27
{
28
// this is bottom
29
}
30
31
bool
merge
(
32
const
is_threaded_domaint
&src,
33
locationt
from,
34
locationt
to)
35
{
36
// assert(src.reachable);
37
38
if
(!src.
reachable
)
39
return
false
;
40
41
bool
old_reachable=
reachable
;
42
bool
old_is_threaded=
is_threaded
;
43
44
reachable=
true
;
45
is_threaded|=src.
is_threaded
;
46
47
return
old_reachable!=reachable ||
48
old_is_threaded!=
is_threaded
;
49
}
50
51
void
transform
(
52
locationt
from,
53
locationt
to,
54
ai_baset
&ai,
55
const
namespacet
&ns)
final
56
{
57
// assert(reachable);
58
59
if
(!reachable)
60
return
;
61
62
if
(from->is_start_thread())
63
is_threaded=
true
;
64
}
65
66
void
make_bottom
() final
67
{
68
reachable=
false
;
69
is_threaded=
false
;
70
}
71
72
void
make_top
() final
73
{
74
reachable=
true
;
75
is_threaded=
true
;
76
}
77
78
void
make_entry
() final
79
{
80
reachable=
true
;
81
is_threaded=
false
;
82
}
83
};
84
85
void
is_threadedt::compute
(
const
goto_functionst
&goto_functions)
86
{
87
// the analysis doesn't actually use the namespace, fake one
88
symbol_tablet
symbol_table;
89
const
namespacet
ns(symbol_table);
90
91
ait<is_threaded_domaint>
is_threaded_analysis;
92
93
is_threaded_analysis(goto_functions, ns);
94
95
forall_goto_functions
(f_it, goto_functions)
96
forall_goto_program_instructions
(i_it, f_it->second.body)
97
if
(is_threaded_analysis[i_it].
is_threaded
)
98
is_threaded_set.insert(i_it);
99
}
is_threaded_domaint::make_entry
void make_entry() final
Definition:
is_threaded.cpp:78
is_threaded.h
Over-approximate Concurrency for Threaded Goto Programs.
is_threaded_domaint::make_top
void make_top() final
Definition:
is_threaded.cpp:72
is_threadedt::compute
void compute(const goto_functionst &goto_functions)
Definition:
is_threaded.cpp:85
ait
Definition:
ai.h:342
is_threaded_domaint::make_bottom
void make_bottom() final
Definition:
is_threaded.cpp:66
ai_domain_baset
Definition:
ai.h:29
is_threaded_domaint
Definition:
is_threaded.cpp:18
symbol_tablet
The symbol table.
Definition:
symbol_table.h:52
namespacet
TO_BE_DOCUMENTED.
Definition:
namespace.h:62
is_threaded_domaint::reachable
bool reachable
Definition:
is_threaded.cpp:21
goto_functionst
Definition:
goto_functions.h:20
is_threaded_domaint::merge
bool merge(const is_threaded_domaint &src, locationt from, locationt to)
Definition:
is_threaded.cpp:31
is_threaded_domaint::is_threaded
bool is_threaded
Definition:
is_threaded.cpp:22
ai.h
Abstract Interpretation.
ai_baset
Definition:
ai.h:108
is_threaded_domaint::is_threaded_domaint
is_threaded_domaint()
Definition:
is_threaded.cpp:24
ai_domain_baset::locationt
goto_programt::const_targett locationt
Definition:
ai.h:42
is_threaded_domaint::transform
void transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns) final
Definition:
is_threaded.cpp:51
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition:
goto_functions.h:53
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition:
goto_program.h:68
analyses
is_threaded.cpp
Generated by
1.8.12