Wrap ghost_instrumentation in content

Author: sim642

src/witness/yamlWitnessType.ml

@@ -566,15 +566,18 @@ struct
   let entry_type = "ghost_instrumentation"
 
   let to_yaml' {ghost_variables; ghost_updates} =
-    [
-      ("ghost_variables", `A (List.map Variable.to_yaml ghost_variables));
-      ("ghost_updates", `A (List.map LocationUpdate.to_yaml ghost_updates));
+    [("content",
+      `O [
+        ("ghost_variables", `A (List.map Variable.to_yaml ghost_variables));
+        ("ghost_updates", `A (List.map LocationUpdate.to_yaml ghost_updates));
+      ])
     ]
 
   let of_yaml y =
     let open GobYaml in
-    let+ ghost_variables = y |> find "ghost_variables" >>= list >>= list_map Variable.of_yaml
-    and+ ghost_updates = y |> find "ghost_updates" >>= list >>= list_map LocationUpdate.of_yaml in
+    let* content = y |> find "content" in
+    let+ ghost_variables = content |> find "ghost_variables" >>= list >>= list_map Variable.of_yaml
+    and+ ghost_updates = content |> find "ghost_updates" >>= list >>= list_map LocationUpdate.of_yaml in
     {ghost_variables; ghost_updates}
 end
 

tests/regression/13-privatized/74-mutex.t

@@ -169,61 +169,62 @@ Same with ghost_instrumentation and invariant_set entries.
 
   $ yamlWitnessStrip < witness.yml
   - entry_type: ghost_instrumentation
-    ghost_variables:
-    - name: m_locked
-      scope: global
-      type: int
-      initial: "0"
-    - name: multithreaded
-      scope: global
-      type: int
-      initial: "0"
-    ghost_updates:
-    - location:
-        file_name: 74-mutex.c
-        file_hash: $FILE_HASH
-        line: 20
-        column: 5
-        function: producer
-      updates:
-      - variable: m_locked
-        expression: "1"
-    - location:
-        file_name: 74-mutex.c
-        file_hash: $FILE_HASH
-        line: 23
-        column: 5
-        function: producer
-      updates:
-      - variable: m_locked
-        expression: "0"
-    - location:
-        file_name: 74-mutex.c
-        file_hash: $FILE_HASH
-        line: 34
-        column: 3
-        function: main
-      updates:
-      - variable: multithreaded
-        expression: "1"
-    - location:
-        file_name: 74-mutex.c
-        file_hash: $FILE_HASH
-        line: 36
-        column: 3
-        function: main
-      updates:
-      - variable: m_locked
-        expression: "1"
-    - location:
-        file_name: 74-mutex.c
-        file_hash: $FILE_HASH
-        line: 38
-        column: 3
-        function: main
-      updates:
-      - variable: m_locked
-        expression: "0"
+    content:
+      ghost_variables:
+      - name: m_locked
+        scope: global
+        type: int
+        initial: "0"
+      - name: multithreaded
+        scope: global
+        type: int
+        initial: "0"
+      ghost_updates:
+      - location:
+          file_name: 74-mutex.c
+          file_hash: $FILE_HASH
+          line: 20
+          column: 5
+          function: producer
+        updates:
+        - variable: m_locked
+          expression: "1"
+      - location:
+          file_name: 74-mutex.c
+          file_hash: $FILE_HASH
+          line: 23
+          column: 5
+          function: producer
+        updates:
+        - variable: m_locked
+          expression: "0"
+      - location:
+          file_name: 74-mutex.c
+          file_hash: $FILE_HASH
+          line: 34
+          column: 3
+          function: main
+        updates:
+        - variable: multithreaded
+          expression: "1"
+      - location:
+          file_name: 74-mutex.c
+          file_hash: $FILE_HASH
+          line: 36
+          column: 3
+          function: main
+        updates:
+        - variable: m_locked
+          expression: "1"
+      - location:
+          file_name: 74-mutex.c
+          file_hash: $FILE_HASH
+          line: 38
+          column: 3
+          function: main
+        updates:
+        - variable: m_locked
+          expression: "0"
   - entry_type: invariant_set
     content:
     - invariant: