#include <spec_lib.h>
/* All other user-defined functions */
-ALL_USER_DEFINED_FUNCTIONS
+ALL_USER_DEFINED_FUNCTIONS // Make them static
/* Definition of interface info struct (per interface) */
typedef struct Put_info {
/* ID functions of interface */
static id_t Put_id() {
- id_t id = PUT_ID;
+ id_t id = PUT_ID; // Default ID == 0;
return id;
}
}
/* End of ID functions */
-/* Initialization of interface<->function_ptr table */
-#define INTERFACE_SIZE 2
-void* func_ptr_table[INTERFACE_SIZE * 2] = {
- CLASS
+
/* Check_action function of interfaces */
bool Put_check_action(void *info, id_t __ID__) {
}
/* End of check_action function definitions */
+/* Initialization of interface<->function_ptr table */
+#define INTERFACE_SIZE 2
+void** func_ptr_table;
/* Beginning of other user-defined variables */
bool lock_acquired;
/* Define function for sequential code initialization */
void __sequential_init() {
+ /* Init func_ptr_table */
+ func_ptr_table = (void**) malloc(sizeof(void*) * 2);
+ func_ptr_table[0] = (void*) &Put_id;
+ func_ptr_table[1] = (void*) &Put_check_action;
+ func_ptr_table[2] = (void*) &Get_id;
+ func_ptr_table[3] = (void*) &Get_check_action;
+
/* Init user-defined variables */
lock_acquired = false;
reader_lock_cnt = 0;
+ /* Pass function table info */
+ anno_func_table_init func_table;
+ func_table.size = INTERFACE_SIZE;
+ func_table.table = func_ptr_table;
+ spec_annotation func_init;
+ func_init.type = FUNC_TABLE_INIT;
+ func_init.annotation = &anno_func_table_init;
+ cdsannotate(SPEC_ANALYSIS, &func_init);
+
/* Pass the happens-before initialization here */
/* PutIfAbsent (putIfAbsent_Succ) -> Get (true) */
anno_hb_init hbConditionInit0;
// And more (if any)
// Interface ends
- spec_annotation annotation_interface_end;
INTERFACE_LABEL_info info = (INTERFACE_LABEL_info*) malloc(sizeof(INTERFACE_LABEL_info));
info->__RET__ = __RET__;
info->arg1 = arg1;
anno_interface_end interface_end;
interface_end.interface_num = 0; // Interface number
interface_end.info = info; // Info
+ spec_annotation annotation_interface_end;
annotation_interface_end.type = INTERFACE_END;
annotation_interface_end.annotation = &interface_end;
cdsannotate(SPEC_ANALYSIS, &annoation_interface_end);