X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=scfence%2Fsc_annotation.h;fp=scfence%2Fsc_annotation.h;h=1f3710727453c16491aff3c717500724b5559f81;hp=0000000000000000000000000000000000000000;hb=a65e234b607444355eb6e34097ee55ba93d4c01b;hpb=7c510878f9679da10de79c289df402356b092396

diff --git a/scfence/sc_annotation.h b/scfence/sc_annotation.h
new file mode 100644
index 0000000..1f37107
--- /dev/null
+++ b/scfence/sc_annotation.h
@@ -0,0 +1,47 @@
+#ifndef _SC_ANNOTATION_H
+#define _SC_ANNOTATION_H
+
+#include "cdsannotate.h"
+#include "action.h"
+
+#define SC_ANNOTATION 2
+
+#define BEGIN 1
+#define END 2
+#define KEEP 3
+
+
+inline bool IS_SC_ANNO(ModelAction *act) {
+	return act != NULL && act->is_annotation() &&
+		act->get_value() == SC_ANNOTATION;
+}
+
+inline bool IS_ANNO_BEGIN(ModelAction *act) {
+	return (void*) BEGIN == act->get_location();
+}
+
+inline bool IS_ANNO_END(ModelAction *act) {
+	return (void*) END == act->get_location();
+}
+
+inline bool IS_ANNO_KEEP(ModelAction *act) {
+	return (void*) KEEP == act->get_location();
+}
+
+inline void SC_BEGIN() {
+	void *loc = (void*) BEGIN;
+	cdsannotate(SC_ANNOTATION, loc);
+}
+
+inline void SC_END() {
+	void *loc = (void*) END;
+	cdsannotate(SC_ANNOTATION, loc);
+}
+
+inline void SC_KEEP() {
+	void *loc = (void*) KEEP;
+	cdsannotate(SC_ANNOTATION, loc);
+}
+
+
+#endif