cprover
is_threaded.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Over-approximate Concurrency for Threaded Goto Programs
4
5Author: Daniel Kroening
6
7Date: 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{
23public:
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
46protected:
47 typedef std::set<goto_programt::const_targett> is_threaded_sett;
49
50 void compute(
51 const goto_functionst &goto_functions);
52};
53
54#endif // CPROVER_ANALYSES_IS_THREADED_H
A collection of goto functions.
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
instructionst::const_iterator const_targett
Definition: goto_program.h:593
is_threadedt(const goto_functionst &goto_functions)
Definition: is_threaded.h:24
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
std::set< goto_programt::const_targett > is_threaded_sett
Definition: is_threaded.h:47
is_threaded_sett is_threaded_set
Definition: is_threaded.h:48
Symbol Table + CFG.