tiny changes

litmus/skel.ml

@@ -371,9 +371,9 @@ module Make
         | Symbolic _|Tag _|PteVal _|Frozen _|ConcreteRecord _ -> assert false
         | Label (p,lab) ->
           if do_self then
-            sprintf "_a->P%d_%s[_i]" p lab
+            sprintf "_a->%s[_i]" (OutUtils.fmt_lbl_var p lab)
           else
-            sprintf "_a->P%d_%s" p lab
+            sprintf "_a->%s" (OutUtils.fmt_lbl_var p lab)
         | Instruction i -> A.GetInstr.instr_name i
 
 (* Dump left & right values when context is available *)
@@ -769,7 +769,6 @@ module Make
             | Indirect,_,_->
                 O.fi "%s%s *%s;" pp_t indirect_star s)
           test.T.globals ;
-        (* TODO *)
         begin match memory with
         | Direct -> []
         | Indirect ->
@@ -1552,8 +1551,7 @@ module Make
             test.T.code;
             Label.Full.Set.iter
             (fun (p,lab) ->
-              let lblname = sprintf "P%d_%s" p lab in
-              O.fi "_a->%s = malloc_check(size_of_test*sizeof(*(_a->%s)));" lblname lblname;
+              malloc indent (fmt_lbl_var p lab);
             )
             CfgLoc.label_init;
         end else begin