annotation_interface_begin.annotation = &interface_boundary;
cdsannotate(SPEC_ANALYSIS, &annoation_interface_begin);
- // FIXME:
TypeReturn __RET__ = __wrapper_interfaceName(arg1, arg2);
- int __COND__ = get(&__sequential.condition, 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;
-
- 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
- #undef _Old_Val
- // And more...
// HB conditions (if any)
if (HB_CONDITION1) {
#include <spec_private_hashtable.h>
#include <_sepc_sequential_genenrated.h>
+// FIXME
+/* Define MACRO */
+#define CAS (__ATOMIC_RET__ = CAS)
+#define LOAD (__ATOMIC_RET__ = LOAD)
+#define RMW (__ATOMIC_RET__ = RMW)
+
thrd_t tid = thrd_current();
-uint64_t __ATOMIC_RET__ = get_prev_value(tid);
if (POTENTIAL_CP_DEFINE_CONDITION) {
uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
annotation_potential_cp_define.annotation = &potential_cp_define;
cdsannotate(SPEC_ANALYSIS, &annotation_potential_cp_define);
}
+/* Undefine MACRO */
+#undef CAS
+#undef LOAD
+#undef RMW
****** Example4: ******
Commit Point Define