12 Each construct should be embraced by /DOUBLE_STAR ... STAR/ annotation.
13 Within there, any line beginning with a "#" is a comment of the annotation.
14 Each constrcut should begin with @Begin and end with @End. Otherwise, the
15 annotation would be considered as normal comments of the source.
27 b) Interface construct
32 @Condition: ... (Optional)
33 @ID: ... (Optional, use default ID)
38 @Post_action: (Optional)
39 @Post_check: (Optional)
42 c) Potential commit construct
44 @Potential_commit_point_define: ...
48 d) Commit point define construct
50 @Commit_point_define_check: ...
57 @Commit_point_define: ...
58 @Potential_commit_point_label: ...
64 Key notes for interpreting the spec into the model checking process:
65 1. In the "include/cdsannotate.h" file, it declares a "void
66 cdsannotate(uinit64_t analysistype, void *annotation)" function to register
67 for an atomic annotation for the purpose trace analysis.
69 2. All the @Check, @Action, @Post_action, @Post_check can be wrapped into an
70 annotation of the model checker, and it has registered for an
71 AnnotationAction which does the internal checks and actions in the trace
79 // Forward declaration
80 class FunctionDeclaration;
81 class SpecInterpreter;
83 // A function pointer that abstracts the checks and actions to be done by the
84 // model checker internally
85 typedef (void*) (*annotation_action_t)();
89 class FunctionDeclaration {
91 The following is an example to illustrate how to use this class.
93 ReturnType functionName(ArgType1 arg1, ArgType2 arg2, ... ArgTypeN argN)
99 FunctionDeclaration();
100 // Will get "ReturnType" exactly
101 string getReturnType();
102 // Will get "functionName(arg1, arg2, ... argN)
103 string getFunctionCallStatement();
105 int getArgumentNum();
106 // argIndex ranges from 0 -- (N - 1). if argIndex == 1, you will get
108 string getNthArgType(int argIndex);
109 // argIndex ranges from 0 -- (N - 1). if argIndex == 1, you will get
111 string getNthArg(int argIndex);
113 // "ReturnType functionName(ArgType1 arg1, ArgType2 arg2, ... ArgTypeN
115 string originalFunctionDefinition();
122 class SpecInterpreter {
125 SpecInterpreter(const char* dirname);
127 void interpretSpec();
130 // Private fields necessary to interpret the spec
131 map<string, FunctionDeclaration> _interface2Decl;
134 void generateFiles();