Skip to content

Commit f71786d

Browse files
committed
Remove primes from YAML invariant_set element construction functions
1 parent 459bd21 commit f71786d

File tree

1 file changed

+7
-8
lines changed

1 file changed

+7
-8
lines changed

src/witness/yamlWitness.ml

Lines changed: 7 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -58,16 +58,15 @@ struct
5858
function_ = Some location_function;
5959
}
6060

61-
(* TODO: remove primes from name *)
62-
let location_invariant' ~location ~(invariant): InvariantSet.Invariant.t = {
61+
let location_invariant ~location ~(invariant): InvariantSet.Invariant.t = {
6362
invariant_type = LocationInvariant {
6463
location;
6564
value = invariant;
6665
format = "c_expression";
6766
};
6867
}
6968

70-
let loop_invariant' ~location ~(invariant): InvariantSet.Invariant.t = {
69+
let loop_invariant ~location ~(invariant): InvariantSet.Invariant.t = {
7170
invariant_type = LoopInvariant {
7271
location;
7372
value = invariant;
@@ -76,7 +75,7 @@ struct
7675
}
7776

7877
(* non-standard extension *)
79-
let flow_insensitive_invariant' ~(invariant): InvariantSet.Invariant.t = {
78+
let flow_insensitive_invariant ~(invariant): InvariantSet.Invariant.t = {
8079
invariant_type = FlowInsensitiveInvariant {
8180
value = invariant;
8281
format = "c_expression";
@@ -293,7 +292,7 @@ struct
293292
let invs = WitnessUtil.InvariantExp.process_exp inv in
294293
List.fold_left (fun acc inv ->
295294
let invariant = CilType.Exp.show inv in
296-
let invariant = Entry.location_invariant' ~location ~invariant in
295+
let invariant = Entry.location_invariant ~location ~invariant in
297296
incr cnt_location_invariant;
298297
invariant :: acc
299298
) acc invs
@@ -323,7 +322,7 @@ struct
323322
let invs = WitnessUtil.InvariantExp.process_exp inv in
324323
List.fold_left (fun acc inv ->
325324
let invariant = CilType.Exp.show inv in
326-
let invariant = Entry.loop_invariant' ~location ~invariant in
325+
let invariant = Entry.loop_invariant ~location ~invariant in
327326
incr cnt_loop_invariant;
328327
invariant :: acc
329328
) acc invs
@@ -349,15 +348,15 @@ struct
349348
let invs = WitnessUtil.InvariantExp.process_exp inv in
350349
List.fold_left (fun acc inv ->
351350
let invariant = CilType.Exp.show inv in
352-
let invariant = Entry.flow_insensitive_invariant' ~invariant in
351+
let invariant = Entry.flow_insensitive_invariant ~invariant in
353352
incr cnt_flow_insensitive_invariant;
354353
invariant :: acc
355354
) acc invs
356355
| `Lifted inv, "invariant_set-location_invariant" ->
357356
(* TODO: fold_flow_insensitive_as_location is now only used here, inline/move? *)
358357
fold_flow_insensitive_as_location ~inv (fun ~location ~inv acc ->
359358
let invariant = CilType.Exp.show inv in
360-
let invariant = Entry.location_invariant' ~location ~invariant in
359+
let invariant = Entry.location_invariant ~location ~invariant in
361360
incr cnt_location_invariant;
362361
invariant :: acc
363362
) acc

0 commit comments

Comments
 (0)