Skip to content

Commit 2c99550

Browse files
committed
Remove ghost_ prefix from ghost_instrumentation update entries
1 parent 431b34d commit 2c99550

File tree

3 files changed

+11
-11
lines changed

3 files changed

+11
-11
lines changed

src/witness/yamlWitness.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -169,7 +169,7 @@ struct
169169
}
170170

171171
let ghost_update' ~variable ~(expression): GhostInstrumentation.Update.t = {
172-
ghost_variable = variable;
172+
variable;
173173
expression;
174174
}
175175

src/witness/yamlWitnessType.ml

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -518,22 +518,22 @@ struct
518518
module Update =
519519
struct
520520
type t = {
521-
ghost_variable: string;
521+
variable: string;
522522
expression: string;
523523
}
524524
[@@deriving eq, ord, hash]
525525

526-
let to_yaml {ghost_variable; expression} =
526+
let to_yaml {variable; expression} =
527527
`O [
528-
("ghost_variable", `String ghost_variable);
528+
("variable", `String variable);
529529
("expression", `String expression);
530530
]
531531

532532
let of_yaml y =
533533
let open GobYaml in
534-
let+ ghost_variable = y |> find "ghost_variable" >>= to_string
534+
let+ variable = y |> find "variable" >>= to_string
535535
and+ expression = y |> find "expression" >>= to_string in
536-
{ghost_variable; expression}
536+
{variable; expression}
537537
end
538538

539539
module LocationUpdate =

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

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -186,7 +186,7 @@ Same with ghost_instrumentation and invariant_set entries.
186186
column: 5
187187
function: producer
188188
updates:
189-
- ghost_variable: m_locked
189+
- variable: m_locked
190190
expression: "1"
191191
- location:
192192
file_name: 74-mutex.c
@@ -195,7 +195,7 @@ Same with ghost_instrumentation and invariant_set entries.
195195
column: 5
196196
function: producer
197197
updates:
198-
- ghost_variable: m_locked
198+
- variable: m_locked
199199
expression: "0"
200200
- location:
201201
file_name: 74-mutex.c
@@ -204,7 +204,7 @@ Same with ghost_instrumentation and invariant_set entries.
204204
column: 3
205205
function: main
206206
updates:
207-
- ghost_variable: multithreaded
207+
- variable: multithreaded
208208
expression: "1"
209209
- location:
210210
file_name: 74-mutex.c
@@ -213,7 +213,7 @@ Same with ghost_instrumentation and invariant_set entries.
213213
column: 3
214214
function: main
215215
updates:
216-
- ghost_variable: m_locked
216+
- variable: m_locked
217217
expression: "1"
218218
- location:
219219
file_name: 74-mutex.c
@@ -222,7 +222,7 @@ Same with ghost_instrumentation and invariant_set entries.
222222
column: 3
223223
function: main
224224
updates:
225-
- ghost_variable: m_locked
225+
- variable: m_locked
226226
expression: "0"
227227
- entry_type: invariant_set
228228
content:

0 commit comments

Comments
 (0)