CBMC
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 
30  explicit is_threadedt(
31  const goto_modelt &goto_model)
32  {
33  compute(goto_model.goto_functions);
34  }
35 
37  {
38  return is_threaded_set.find(t)!=is_threaded_set.end();
39  }
40 
41  bool operator()(void) const
42  {
43  return !is_threaded_set.empty();
44  }
45 
46 protected:
47  typedef std::
48  set<goto_programt::const_targett, goto_programt::target_less_than>
51 
52  void compute(
53  const goto_functionst &goto_functions);
54 };
55 
56 #endif // CPROVER_ANALYSES_IS_THREADED_H
A collection of goto functions.
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:34
instructionst::const_iterator const_targett
Definition: goto_program.h:615
is_threadedt(const goto_functionst &goto_functions)
Definition: is_threaded.h:24
std::set< goto_programt::const_targett, goto_programt::target_less_than > is_threaded_sett
Definition: is_threaded.h:49
bool operator()(const goto_programt::const_targett t) const
Definition: is_threaded.h:36
is_threadedt(const goto_modelt &goto_model)
Definition: is_threaded.h:30
void compute(const goto_functionst &goto_functions)
Definition: is_threaded.cpp:95
bool operator()(void) const
Definition: is_threaded.h:41
is_threaded_sett is_threaded_set
Definition: is_threaded.h:50
Symbol Table + CFG.