projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
scanalysis: fixup spacing
[model-checker.git]
/
scanalysis.h
diff --git
a/scanalysis.h
b/scanalysis.h
index e8afc18949aaa1b25b931bcfd46f42a5225fde72..047793045e63c954b03b775fd433738aaf8d08d7 100644
(file)
--- a/
scanalysis.h
+++ b/
scanalysis.h
@@
-18,11
+18,15
@@
class SCAnalysis : public TraceAnalysis {
action_list_t * generateSC(action_list_t *);
bool processRead(ModelAction *read, ClockVector *cv);
ModelAction * getNextAction();
action_list_t * generateSC(action_list_t *);
bool processRead(ModelAction *read, ClockVector *cv);
ModelAction * getNextAction();
- bool merge(ClockVector *cv, const ModelAction *act, ClockVector *cv2);
+ bool merge(ClockVector *cv, const ModelAction *act, const ModelAction *act2);
+ void check_rf(action_list_t *list);
+
int maxthreads;
HashTable<const ModelAction *, ClockVector *, uintptr_t, 4 > cvmap;
int maxthreads;
HashTable<const ModelAction *, ClockVector *, uintptr_t, 4 > cvmap;
- HashTable<const ModelAction *, const ModelAction *, uintptr_t, 4 > cycleset;
+ bool cyclic;
+ HashTable<const ModelAction *, const ModelAction *, uintptr_t, 4 > badrfset;
+ HashTable<void *, const ModelAction *, uintptr_t, 4 > lastwrmap;
SnapVector<action_list_t> threadlists;
const ModelExecution *execution;
};
SnapVector<action_list_t> threadlists;
const ModelExecution *execution;
};