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 
19 {
20 public:
21  bool reachable;
23 
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;
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 }
void make_entry() final
Definition: is_threaded.cpp:78
Over-approximate Concurrency for Threaded Goto Programs.
void make_top() final
Definition: is_threaded.cpp:72
void compute(const goto_functionst &goto_functions)
Definition: is_threaded.cpp:85
Definition: ai.h:342
void make_bottom() final
Definition: is_threaded.cpp:66
is_threaded_sett is_threaded_set
Definition: is_threaded.h:42
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
bool merge(const is_threaded_domaint &src, locationt from, locationt to)
Definition: is_threaded.cpp:31
Abstract Interpretation.
Definition: ai.h:108
goto_programt::const_targett locationt
Definition: ai.h:42
void transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns) final
Definition: is_threaded.cpp:51
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:68