X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=datarace.h;h=737a6d6e99a915a06d2f21d9f6a521a5ad126e03;hb=d17fbaf88464f1a9e8fe2b7df96631652ee17122;hp=78903d336832bb7439d4a8ab61799dd48f2ceed5;hpb=c123ef2c7d98d23474d2d2b121b56b502d75665b;p=model-checker.git diff --git a/datarace.h b/datarace.h index 78903d3..737a6d6 100644 --- a/datarace.h +++ b/datarace.h @@ -2,14 +2,14 @@ * @brief Data race detection code. */ -#ifndef DATARACE_H +#ifndef __DATARACE_H__ +#define __DATARACE_H__ + #include "config.h" #include #include "modeltypes.h" -#include "stl-model.h" /* Forward declaration */ -class ClockVector; class ModelAction; struct ShadowTable { @@ -46,8 +46,7 @@ void raceCheckWrite(thread_id_t thread, void *location); void raceCheckRead(thread_id_t thread, const void *location); bool checkDataRaces(); void assert_race(struct DataRace *race); - -extern SnapVector unrealizedraces; +bool haveUnrealizedRaces(); /** * @brief A record of information for detecting data races @@ -91,4 +90,5 @@ struct RaceRecord { #define MAXTHREADID (THREADMASK-1) #define MAXREADVECTOR (READMASK-1) #define MAXWRITEVECTOR (WRITEMASK-1) -#endif + +#endif /* __DATARACE_H__ */