Fix snapshot code
[model-checker.git] / scfence / sc_annotation.h
1 #ifndef _SC_ANNOTATION_H
2 #define _SC_ANNOTATION_H
3
4 #include "cdsannotate.h"
5 #include "action.h"
6
7 #define SC_ANNOTATION 2
8
9 #define BEGIN 1
10 #define END 2
11 #define KEEP 3
12
13
14 inline bool IS_SC_ANNO(ModelAction *act) {
15         return act != NULL && act->is_annotation() &&
16                 act->get_value() == SC_ANNOTATION;
17 }
18
19 inline bool IS_ANNO_BEGIN(ModelAction *act) {
20         return (void*) BEGIN == act->get_location();
21 }
22
23 inline bool IS_ANNO_END(ModelAction *act) {
24         return (void*) END == act->get_location();
25 }
26
27 inline bool IS_ANNO_KEEP(ModelAction *act) {
28         return (void*) KEEP == act->get_location();
29 }
30
31 inline void SC_BEGIN() {
32         void *loc = (void*) BEGIN;
33         cdsannotate(SC_ANNOTATION, loc);
34 }
35
36 inline void SC_END() {
37         void *loc = (void*) END;
38         cdsannotate(SC_ANNOTATION, loc);
39 }
40
41 inline void SC_KEEP() {
42         void *loc = (void*) KEEP;
43         cdsannotate(SC_ANNOTATION, loc);
44 }
45
46
47 #endif