-/* Need to compute the relationship between labels before hand */
-switch (interface_num) {
- case 0:
- // Commit point 3 <=> potentialCP 4
- if (COMMIT_POINT3_CONDITION && potential_cp_satisfied(3, 4)) {
- 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 = 3;
- cp_define.call_sequence_num = call_sequence_num;
- spec_annotation annotation_cp_define;
- annotation_cp_define.type = CP_DEFINE;
- annotation_cp_define.annotation = &cp_define;
- cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
- }
- break;
- case 1:
- // Commit point 5 <=> potentialCP 6
- if (COMMIT_POINT5_CONDITION && potential_cp_satisfied(5, 6)) {
- if (INTERFACE1_CHECK_CONDITION) {
- check_passed = true;
- }
- // ...
- // Same as the above case
- }
- break;
- default:
- break;
+// Commit point 3 <=> potentialCP 4
+if (COMMIT_POINT3_CONDITION) {
+ anno_cp_define cp_define;
+ cp_define.label_num = 3;
+ cp_define.potential_cp_label_num = 1;
+ spec_annotation annotation_cp_define;
+ annotation_cp_define.type = CP_DEFINE;
+ annotation_cp_define.annotation = &cp_define;
+ cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
+}
+// More if there are any
+