cdsannotate(SPEC_ANALYSIS, &annoation_interface_begin);
TypeReturn __RET__ = __wrapper_interfaceName(arg1, arg2);
- bool __COND__ = get(&__cond, tid);
- uint64_t id = get(&__id, tid);
+ int __COND__ = get(&__sequential.cond, tid);
+ uint64_t __ID__ = get(&__sequential.id, tid);
+
+ /* Post_check action, define macros for all DefineVars */
+ #define _Old_Val (get(&__sequential.put__Old_Val, tid))
+ // And more...
+ bool post_check_passed = INTERFACE_POST_CHECK_CONDITION;
+ #undef _Old_Val
+ // And more...
+
+ anno_post_check post_check;
+ post_check.check_passed = post_check_passed;
+ post_check.interface_num = interface_num;
+ post_check.call_sequence_num = call_sequence_num;
+ spec_annotation annotation_post_check;
+ annotation_post_check.type = POST_CHECK;
+ annotation_post_check.annotation = &post_check;
+ cdsannotate(SPEC_ANALYSIS, &annotation_post_check);
+
+ // Post Action (if any)
+ POST_ACTION_CODE // Unfolded in place
// HB conditions (if any)
if (HB_CONDITION1) {
// And more (if any)
}
- // Post check (if any)
- bool post_check_passed = POST_CHECK_CONDITION;
- anno_post_check post_check;
- post_check.check_passed = post_check_passed;
- post_check.interface_num = interface_num;
- post_check.call_sequence_num = call_sequence_num;
- spec_annotation annotation_post_check;
- annotation_post_check.type = POST_CHECK;
- annotation_post_check.annotation = &post_check;
- cdsannotate(SPEC_ANALYSIS, &annotation_post_check);
-
- // Post Action (if any)
- POST_ACTION_CODE // Unfolded in place
-
// Interface ends
spec_annotation annotation_interface_end;
annotation_interface_end.type = INTERFACE_END;
if (INTERFACE0_CHECK_CONDITION) {
check_passed = true;
}
- /* For all DefineVar of INTERFACE0 (Type id = Expr) */
- FIXME: Type res0 = Expr;
- put(__sequential.put_id, tid,
- #define _Old_Val __sequential.put_id
+ /* For all DefineVar of INTERFACE0 (Type id = Expr) (Type must be a
+ * pointer) */
+ /* Unfold all if there are multiple DefineVars */
+ Type res0 = Expr;
+ put(&__sequential.put__Old_Val, tid, (uint64_t) res0);
+ // And more...
+
+ /* Compute id; If not defined, assign the default ID */
+ int id = INTERFACE0_ID_EXPRESSION;
+ put(__sequential.id, tid, id);
+
+ /* Execute actions if there's any */
+ #define _Old_Val res0;
INTERFACE0_ACTION; // Unfolded right in place
+ #undef _Old_Val
+ // And more...
anno_cp_define cp_define;
uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
if (INTERFACE1_CHECK_CONDITION) {
check_passed = true;
}
- INTERFACE1_ACTION; // Unfolded right in place
+ // ...
+ // Same as the above case
+ }
+ break;
+ default:
+ break;
+}
+
+
+***** Example6: ******
+Commit Point Define Check
+
+
+#include <threads.h>
+#include <cdstrace.h>
+#include <cdsannotate.h>
+#include <spec_private_hashtable.h>
+#include <CDSName.h>
+
+
+thrd_t __tid = thrd_current();
+int interface_num = get(&__sequential.interface, tid);
+/* For all the interface check at this commit point (if there is multiple
+ * checks here) */
+/* Need to compute the relationship between labels before hand */
+switch (interface_num) {
+ case 0:
+ if (COMMIT_POINT3_CONDITION) {
+ if (INTERFACE0_CHECK_CONDITION) {
+ check_passed = true;
+ }
+ /* For all DefineVar of INTERFACE0 (Type id = Expr) (Type must be a
+ * pointer) */
+ /* Unfold all if there are multiple DefineVars */
+ Type res0 = Expr;
+ put(&__sequential.put__Old_Val, tid, (uint64_t) res0);
+ // And more...
+
+ /* Compute id; If not defined, assign the default ID */
+ int id = INTERFACE0_ID_EXPRESSION;
+ put(__sequential.id, tid, id);
+
+ /* Execute actions if there's any */
+ #define _Old_Val res0;
+ INTERFACE0_ACTION; // Unfolded right in place
+ #undef _Old_Val
+ // And more...
anno_cp_define cp_define;
uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
bool check_passed = false;
cp_define.check_passed = check_passed;
cp_define.interface_num = interface_num;
- cp_define.label_num = 5;
+ cp_define.label_num = 3;
cp_define.call_sequence_num = call_sequence_num;
spec_annotation annotation_cp_define;
annotation_cp_define.type = CP_DEFINE;
cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
}
break;
+ case 1:
+ if (COMMIT_POINT5_CONDITION) {
+ if (INTERFACE1_CHECK_CONDITION) {
+ check_passed = true;
+ }
+ // ...
+ // Same as the above case
+ }
+ break;
default:
break;
}
-
-
-***** Example6: ******
-Commit Point Define Check
-