is_threaded.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Over-approximate Concurrency for Threaded Goto Programs
 
Author: Daniel Kroening
 
Date: October 2012
 
\*******************************************************************/
 
 
#ifndef CPROVER_ANALYSES_IS_THREADED_H
#define CPROVER_ANALYSES_IS_THREADED_H
 
#include <set>
 
#include <goto-programs/goto_model.h>
 
class is_threadedt
{
public:
  explicit is_threadedt(
    const goto_functionst &goto_functions)
  {
    compute(goto_functions);
  }
  explicit is_threadedt( {…}
 
  explicit is_threadedt(
    const goto_modelt &goto_model)
  {
    compute(goto_model.goto_functions);
  }
  explicit is_threadedt( {…}
 
  bool operator()(const goto_programt::const_targett t) const
  {
    return is_threaded_set.find(t)!=is_threaded_set.end();
  }
  bool operator()(const goto_programt::const_targett t) const {…}
 
  bool operator()(void) const
  {
    return !is_threaded_set.empty();
  }
  bool operator()(void) const {…}
 
protected:
  typedef std::
    set<goto_programt::const_targett, goto_programt::target_less_than>
      is_threaded_sett;
  is_threaded_sett is_threaded_set;
 
  void compute(
    const goto_functionst &goto_functions);
};
class is_threadedt {…};
 
#endif // CPROVER_ANALYSES_IS_THREADED_H