* remove unnecessary 'class' keyword
* add ASSERT() in the 'thread_current()' function
* move #include into .cc file
* remove more end-of-line spaces
-typedef std::list<class ModelAction *> action_list_t;
+typedef std::list<ModelAction *> action_list_t;
#endif /* __ACTION_H__ */
#endif /* __ACTION_H__ */
CycleGraph::CycleGraph() {
hasCycles=false;
CycleGraph::CycleGraph() {
hasCycles=false;
}
bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) {
}
bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) {
- std::vector<class CycleNode *> queue;
- HashTable<class CycleNode *, class CycleNode *, uintptr_t, 4> discovered;
-
+ std::vector<CycleNode *> queue;
+ HashTable<CycleNode *, CycleNode *, uintptr_t, 4> discovered;
+
queue.push_back(from);
discovered.put(from, from);
while(!queue.empty()) {
queue.push_back(from);
discovered.put(from, from);
while(!queue.empty()) {
- class CycleNode * node=queue.back();
+ CycleNode * node=queue.back();
queue.pop_back();
if (node==to)
return true;
queue.pop_back();
if (node==to)
return true;
for(unsigned int i=0;i<node->getEdges()->size();i++) {
CycleNode *next=(*node->getEdges())[i];
if (!discovered.contains(next)) {
for(unsigned int i=0;i<node->getEdges()->size();i++) {
CycleNode *next=(*node->getEdges())[i];
if (!discovered.contains(next)) {
-std::vector<class CycleNode *> * CycleNode::getEdges() {
+std::vector<CycleNode *> * CycleNode::getEdges() {
#define CYCLEGRAPH_H
#include "hashtable.h"
#define CYCLEGRAPH_H
#include "hashtable.h"
#include <vector>
#include <inttypes.h>
class CycleNode;
#include <vector>
#include <inttypes.h>
class CycleNode;
/** @brief A graph of Model Actions for tracking cycles. */
class CycleGraph {
/** @brief A graph of Model Actions for tracking cycles. */
class CycleGraph {
private:
CycleNode * getNode(ModelAction *);
private:
CycleNode * getNode(ModelAction *);
- HashTable<class ModelAction *, class CycleNode *, uintptr_t, 4> actionToNode;
+ HashTable<ModelAction *, CycleNode *, uintptr_t, 4> actionToNode;
bool checkReachable(CycleNode *from, CycleNode *to);
bool checkReachable(CycleNode *from, CycleNode *to);
public:
CycleNode(ModelAction *action);
void addEdge(CycleNode * node);
public:
CycleNode(ModelAction *action);
void addEdge(CycleNode * node);
- std::vector<class CycleNode *> * getEdges();
+ std::vector<CycleNode *> * getEdges();
private:
ModelAction *action;
private:
ModelAction *action;
- std::vector<class CycleNode *> edges;
+ std::vector<CycleNode *> edges;
diverge(NULL),
nextThread(THREAD_ID_T_NONE),
action_trace(new action_list_t()),
diverge(NULL),
nextThread(THREAD_ID_T_NONE),
action_trace(new action_list_t()),
- thread_map(new std::map<int, class Thread *>),
+ thread_map(new std::map<int, Thread *>),
obj_thrd_map(new std::map<void *, std::vector<action_list_t> >()),
thrd_last_action(new std::vector<ModelAction *>(1)),
node_stack(new NodeStack()),
obj_thrd_map(new std::map<void *, std::vector<action_list_t> >()),
thrd_last_action(new std::vector<ModelAction *>(1)),
node_stack(new NodeStack()),
/** @brief Destructor */
ModelChecker::~ModelChecker()
{
/** @brief Destructor */
ModelChecker::~ModelChecker()
{
- std::map<int, class Thread *>::iterator it;
+ std::map<int, Thread *>::iterator it;
for (it = thread_map->begin(); it != thread_map->end(); it++)
delete (*it).second;
delete thread_map;
for (it = thread_map->begin(); it != thread_map->end(); it++)
delete (*it).second;
delete thread_map;
~ModelChecker();
/** The scheduler to use: tracks the running/ready Threads */
~ModelChecker();
/** The scheduler to use: tracks the running/ready Threads */
- class Scheduler *scheduler;
/** Stores the context for the main model-checking system thread (call
* once)
/** Stores the context for the main model-checking system thread (call
* once)
ucontext_t *system_context;
action_list_t *action_trace;
ucontext_t *system_context;
action_list_t *action_trace;
- std::map<int, class Thread *> *thread_map;
+ std::map<int, Thread *> *thread_map;
std::map<void *, std::vector<action_list_t> > *obj_thrd_map;
std::vector<ModelAction *> *thrd_last_action;
std::map<void *, std::vector<action_list_t> > *obj_thrd_map;
std::vector<ModelAction *> *thrd_last_action;
- class NodeStack *node_stack;
ModelAction *next_backtrack;
};
ModelAction *next_backtrack;
};
action_set_t may_read_from;
};
action_set_t may_read_from;
};
-typedef std::list<class Node *, MyAlloc< class Node * > > node_list_t;
+typedef std::list< Node *, MyAlloc< Node * > > node_list_t;
/**
* @brief A stack of nodes
/**
* @brief A stack of nodes
Thread * thread_current(void)
{
Thread * thread_current(void)
{
return model->scheduler->get_current_thread();
}
return model->scheduler->get_current_thread();
}