Add value and format to ghost_instrumentation

Author: sim642

src/witness/yamlWitness.ml

@@ -165,12 +165,16 @@ struct
     name = variable;
     scope = "global";
     type_;
-    initial;
+    initial = {
+      value = initial;
+      format = "c_expression";
+    };
   }
 
   let ghost_update' ~variable ~(expression): GhostInstrumentation.Update.t = {
     variable;
-    expression;
+    value = expression;
+    format = "c_expression";
   }
 
   let ghost_location_update' ~location ~(updates): GhostInstrumentation.LocationUpdate.t = {

src/witness/yamlWitnessType.ml

@@ -488,13 +488,34 @@ end
 module GhostInstrumentation =
 struct
 
+  module Initial =
+  struct
+    type t = {
+      value: string;
+      format: string;
+    }
+    [@@deriving eq, ord, hash]
+
+    let to_yaml {value; format} =
+      `O [
+        ("value", `String value);
+        ("format", `String format);
+      ]
+
+    let of_yaml y =
+      let open GobYaml in
+      let+ value = y |> find "value" >>= to_string
+      and+ format = y |> find "format" >>= to_string in
+      {value; format}
+  end
+
   module Variable =
   struct
     type t = {
       name: string;
       scope: string;
       type_: string;
-      initial: string;
+      initial: Initial.t;
     }
     [@@deriving eq, ord, hash]
 
@@ -503,37 +524,40 @@ struct
         ("name", `String name);
         ("scope", `String scope);
         ("type", `String type_);
-        ("initial", `String initial);
+        ("initial", Initial.to_yaml initial);
       ]
 
     let of_yaml y =
       let open GobYaml in
       let+ name = y |> find "name" >>= to_string
       and+ scope = y |> find "scope" >>= to_string
       and+ type_ = y |> find "type" >>= to_string
-      and+ initial = y |> find "initial" >>= to_string in
+      and+ initial = y |> find "initial" >>= Initial.of_yaml in
       {name; scope; type_; initial}
   end
 
   module Update =
   struct
     type t = {
       variable: string;
-      expression: string;
+      value: string;
+      format: string;
     }
     [@@deriving eq, ord, hash]
 
-    let to_yaml {variable; expression} =
+    let to_yaml {variable; value; format} =
       `O [
         ("variable", `String variable);
-        ("expression", `String expression);
+        ("value", `String value);
+        ("format", `String format);
       ]
 
     let of_yaml y =
       let open GobYaml in
       let+ variable = y |> find "variable" >>= to_string
-      and+ expression = y |> find "expression" >>= to_string in
-      {variable; expression}
+      and+ value = y |> find "value" >>= to_string
+      and+ format = y |> find "format" >>= to_string in
+      {variable; value; format}
   end
 
   module LocationUpdate =

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

@@ -174,11 +174,15 @@ Same with ghost_instrumentation and invariant_set entries.
       - name: m_locked
         scope: global
         type: int
-        initial: "0"
+        initial:
+          value: "0"
+          format: c_expression
       - name: multithreaded
         scope: global
         type: int
-        initial: "0"
+        initial:
+          value: "0"
+          format: c_expression
       ghost_updates:
       - location:
           file_name: 74-mutex.c
@@ -188,7 +192,8 @@ Same with ghost_instrumentation and invariant_set entries.
           function: producer
         updates:
         - variable: m_locked
-          expression: "1"
+          value: "1"
+          format: c_expression
       - location:
           file_name: 74-mutex.c
           file_hash: $FILE_HASH
@@ -197,7 +202,8 @@ Same with ghost_instrumentation and invariant_set entries.
           function: producer
         updates:
         - variable: m_locked
-          expression: "0"
+          value: "0"
+          format: c_expression
       - location:
           file_name: 74-mutex.c
           file_hash: $FILE_HASH
@@ -206,7 +212,8 @@ Same with ghost_instrumentation and invariant_set entries.
           function: main
         updates:
         - variable: multithreaded
-          expression: "1"
+          value: "1"
+          format: c_expression
       - location:
           file_name: 74-mutex.c
           file_hash: $FILE_HASH
@@ -215,7 +222,8 @@ Same with ghost_instrumentation and invariant_set entries.
           function: main
         updates:
         - variable: m_locked
-          expression: "1"
+          value: "1"
+          format: c_expression
       - location:
           file_name: 74-mutex.c
           file_hash: $FILE_HASH
@@ -224,7 +232,8 @@ Same with ghost_instrumentation and invariant_set entries.
           function: main
         updates:
         - variable: m_locked
-          expression: "0"
+          value: "0"
+          format: c_expression
   - entry_type: invariant_set
     content:
     - invariant: