+ printf("#define OFFSET_CurrentTSO %d\n", OFFSET_CurrentTSO);
+ printf("#define OFFSET_CurrentNursery %d\n", OFFSET_CurrentNursery);
+ printf("#define OFFSET_HpAlloc %d\n", OFFSET_HpAlloc);
+
+ printf("#define OFFSET_stgChk0 (%d)\n", OFFSET_stgChk0);
+ printf("#define OFFSET_stgChk1 (%d)\n", OFFSET_stgChk1);
+ printf("#define OFFSET_stgGCEnter1 (%d)\n", OFFSET_stgGCEnter1);
+ printf("#define OFFSET_stgUpdatePAP (%d)\n", OFFSET_stgUpdatePAP);