From: Brian Norris <banorris@uci.edu>
Date: Mon, 21 May 2012 18:07:44 +0000 (-0700)
Subject: Merge commit: branch 'work'
X-Git-Tag: pldi2013~409
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=10de861d3a9908e75b6f94283cc67b3f1b4d93ab

Merge commit: branch 'work'

tree.{cc,h} were replaced with NodeStack. (Will need to update them)

Other trivial conflicts in Makefile and model.h

Conflicts:
	Makefile
	model.h
	tree.cc
	tree.h
---

10de861d3a9908e75b6f94283cc67b3f1b4d93ab
diff --cc Makefile
index f91f4fd,22a1c64..ef89c5a
--- a/Makefile
+++ b/Makefile
@@@ -8,16 -8,12 +8,16 @@@ LIB_SO=lib$(LIB_NAME).s
  USER_O=userprog.o
  USER_H=libthreads.h libatomic.h
  
- MODEL_CC=libthreads.cc schedule.cc libatomic.cc model.cc threads.cc tree.cc librace.cc action.cc nodestack.cc clockvector.cc main.cc snapshot-interface.cc
- MODEL_O=libthreads.o schedule.o libatomic.o model.o threads.o tree.o librace.o action.o nodestack.o clockvector.o main.o snapshot-interface.o
- MODEL_H=libthreads.h schedule.h common.h libatomic.h model.h threads.h tree.h librace.h action.h nodestack.h clockvector.h snapshot-interface.h
 -MODEL_CC=libthreads.cc schedule.cc libatomic.cc model.cc malloc.c threads.cc librace.cc action.cc nodestack.cc clockvector.cc main.cc
 -MODEL_O=libthreads.o schedule.o libatomic.o model.o malloc.o threads.o librace.o action.o nodestack.o clockvector.o main.o
 -MODEL_H=libthreads.h schedule.h common.h libatomic.h model.h threads.h librace.h action.h nodestack.h clockvector.h
++MODEL_CC=libthreads.cc schedule.cc libatomic.cc model.cc threads.cc librace.cc action.cc nodestack.cc clockvector.cc main.cc snapshot-interface.cc
++MODEL_O=libthreads.o schedule.o libatomic.o model.o threads.o librace.o action.o nodestack.o clockvector.o main.o snapshot-interface.o
++MODEL_H=libthreads.h schedule.h common.h libatomic.h model.h threads.h librace.h action.h nodestack.h clockvector.h snapshot-interface.h
 +
 +SHMEM_CC=snapshot.cc malloc.c mymemory.cc
 +SHMEM_O=snapshot.o malloc.o mymemory.o
 +SHMEM_H=snapshot.h snapshotimp.h mymemory.h
  
  CPPFLAGS=-Wall -g
 -LDFLAGS=-ldl
 +LDFLAGS=-ldl -lrt
  
  all: $(BIN)
  
diff --cc model.cc
index e068a08,90dcdc7..8da05aa
--- a/model.cc
+++ b/model.cc
@@@ -2,10 -2,8 +2,10 @@@
  
  #include "model.h"
  #include "action.h"
- #include "tree.h"
+ #include "nodestack.h"
  #include "schedule.h"
 +#include "snapshot-interface.h"
 +#undef DEBUG
  #include "common.h"
  
  #define INITIAL_THREAD_ID	0
diff --cc model.h
index 1dc6a15,e8a8c5e..4718c50
--- a/model.h
+++ b/model.h
@@@ -63,9 -58,9 +62,9 @@@ private
  
  	ucontext_t *system_context;
  	action_list_t *action_trace;
 -	std::map<int, class Thread *> thread_map;
 +	std::map<int, class Thread *, std::less< int >, MyAlloc< std::pair< const int, class Thread * > > > thread_map;
- 	class TreeNode *rootNode, *currentNode;
- 	std::list<class Backtrack *, MyAlloc< class Backtrack * > > backtrack_list;
+ 	class NodeStack *node_stack;
+ 	ModelAction *next_backtrack;
  };
  
  extern ModelChecker *model;