From 3258f618c294beeac66147a9333d084fede581b0 Mon Sep 17 00:00:00 2001
From: Artem Khyzha <artem.khyzha@arm.com>
Date: Tue, 19 Mar 2024 16:19:58 +0000
Subject: [PATCH] tiny changes

---
 litmus/skel.ml | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/litmus/skel.ml b/litmus/skel.ml
index 25ec36e19..e46d1eb8d 100644
--- a/litmus/skel.ml
+++ b/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