trivial changes

* remove unnecessary 'class' keyword
* add ASSERT() in the 'thread_current()' function
* move #include into .cc file
* remove more end-of-line spaces

diff --git a/action.h b/action.h
index c84381dcff935e0689afa5dac314f589cdb7fae2..4903f37b7720c4116943f5c542bcfa06ae92c8a8 100644 (file)
--- a/action.h
+++ b/action.h
@@ -101,6 +101,6 @@ private:
        ClockVector *cv;
 };
 
-typedef std::list<class ModelAction *> action_list_t;
+typedef std::list<ModelAction *> action_list_t;
 
 #endif /* __ACTION_H__ */

diff --git a/cyclegraph.cc b/cyclegraph.cc
index c1fea4f3d0a96f14de433b6aac8b61e6f6479131..8788bfeba6c33140c0544a4ed39f8475864f3e8c 100644 (file)
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -1,4 +1,5 @@
 #include "cyclegraph.h"
+#include "action.h"
 
 CycleGraph::CycleGraph() {
        hasCycles=false;
@@ -24,17 +25,17 @@ void CycleGraph::addEdge(ModelAction *from, ModelAction *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()) {
-               class CycleNode * node=queue.back();
+               CycleNode * node=queue.back();
                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)) {
@@ -50,7 +51,7 @@ CycleNode::CycleNode(ModelAction *modelaction) {
        action=modelaction;
 }
 
-std::vector<class CycleNode *> * CycleNode::getEdges() {
+std::vector<CycleNode *> * CycleNode::getEdges() {
        return &edges;
 }
 

diff --git a/cyclegraph.h b/cyclegraph.h
index 818a3e88f3afca519cbff27e8d4310f485e130ff..df9d46c17d108c51af33862cb1777a6b150ab515 100644 (file)
--- a/cyclegraph.h
+++ b/cyclegraph.h
@@ -2,11 +2,11 @@
 #define CYCLEGRAPH_H
 
 #include "hashtable.h"
-#include "action.h"
 #include <vector>
 #include <inttypes.h>
 
 class CycleNode;
+class ModelAction;
 
 /** @brief A graph of Model Actions for tracking cycles. */
 class CycleGraph {
@@ -17,9 +17,9 @@ class CycleGraph {
 
  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 hasCycles;
 
 };
@@ -28,11 +28,11 @@ class CycleNode {
  public:
        CycleNode(ModelAction *action);
        void addEdge(CycleNode * node);
-       std::vector<class CycleNode *> * getEdges();
+       std::vector<CycleNode *> * getEdges();
 
  private:
        ModelAction *action;
-       std::vector<class CycleNode *> edges;
+       std::vector<CycleNode *> edges;
 };
 
 #endif

diff --git a/model.cc b/model.cc
index 4e2bb0250f05480ca3ccde1f6b99c26afe344a8b..3e25dc6f0171d5efce0480504ec4c4ba14190c4b 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -26,7 +26,7 @@ ModelChecker::ModelChecker()
        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()),
@@ -37,7 +37,7 @@ 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;

diff --git a/model.h b/model.h
index 4ea55903dde4ae3b595ca5a653c22415b50f320a..fbf1b3f0909ff3fd67fbb10e905d1c0b7ff9003b 100644 (file)
--- a/model.h
+++ b/model.h
@@ -30,7 +30,7 @@ public:
        ~ModelChecker();
 
        /** The scheduler to use: tracks the running/ready Threads */
-       class Scheduler *scheduler;
+       Scheduler *scheduler;
 
        /** Stores the context for the main model-checking system thread (call
         * once)
@@ -88,10 +88,10 @@ private:
 
        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;
-       class NodeStack *node_stack;
+       NodeStack *node_stack;
        ModelAction *next_backtrack;
 };
 

diff --git a/nodestack.h b/nodestack.h
index 37f9261149bc49a9d0a99182e21102be39e1161a..59e545783a4f570ff852105f5d08792d562d2b03 100644 (file)
--- a/nodestack.h
+++ b/nodestack.h
@@ -64,7 +64,7 @@ private:
        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

diff --git a/threads.cc b/threads.cc
index 37b0f1a87ee6fb9ac975a84c8df9adf018d808c5..6d290a94f9f2131b5ca9e7d47b8bae457dd02857 100644 (file)
--- a/threads.cc
+++ b/threads.cc
@@ -19,6 +19,7 @@ static void stack_free(void *stack)
 
 Thread * thread_current(void)
 {
+       ASSERT(model);
        return model->scheduler->get_current_thread();
 }