cprover
is_threaded.h
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 #ifndef CPROVER_ANALYSES_IS_THREADED_H
15 #define CPROVER_ANALYSES_IS_THREADED_H
16 
17 #include <set>
18 
20 
22 {
23 public:
24  explicit is_threadedt(
25  const goto_functionst &goto_functions)
26  {
27  compute(goto_functions);
28  }
29 
31  {
32  return is_threaded_set.find(t)!=is_threaded_set.end();
33  }
34 
35  bool operator()(void) const
36  {
37  return !is_threaded_set.empty();
38  }
39 
40 protected:
41  typedef std::set<goto_programt::const_targett> is_threaded_sett;
43 
44  void compute(
45  const goto_functionst &goto_functions);
46 };
47 
48 #endif // CPROVER_ANALYSES_IS_THREADED_H
bool operator()(const goto_programt::const_targett t) const
Definition: is_threaded.h:30
bool operator()(void) const
Definition: is_threaded.h:35
void compute(const goto_functionst &goto_functions)
Definition: is_threaded.cpp:85
Goto Programs with Functions.
std::set< goto_programt::const_targett > is_threaded_sett
Definition: is_threaded.h:41
instructionst::const_iterator const_targett
is_threaded_sett is_threaded_set
Definition: is_threaded.h:42
is_threadedt(const goto_functionst &goto_functions)
Definition: is_threaded.h:24