X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=libannotate.cc;fp=libannotate.cc;h=b1fad8afeadb28d993f32de79e9b1d76884ee6aa;hp=0000000000000000000000000000000000000000;hb=2d0d4ac38e05905a6633b3f2d5112ccadd45c27f;hpb=5c4efe5cd8bdfe1e85138396109876a121ca61d1

diff --git a/libannotate.cc b/libannotate.cc
new file mode 100644
index 0000000..b1fad8a
--- /dev/null
+++ b/libannotate.cc
@@ -0,0 +1,14 @@
+#include <cdsannotate.h>
+#include "common.h"
+#include "action.h"
+#include "model.h"
+
+/** Pass in an annotation that a trace analysis will use.  The
+ *  analysis type is a unique number that specifies which trace
+ *  analysis needs the annotation.  The reference is to a data
+ *  structure that the trace understands. */
+
+void cdsannotate(uint64_t analysistype, void *annotation) {
+	/* seq_cst is just a 'don't care' parameter */
+	model->switch_to_master(new ModelAction(ATOMIC_ANNOTATION, std::memory_order_seq_cst, annotation, analysistype));
+}