Skip to content

Commit 459bd21

Browse files
committed
Remove TODOs with unused YAML witness 0.1 code
1 parent 3d23e8e commit 459bd21

File tree

2 files changed

+0
-33
lines changed

2 files changed

+0
-33
lines changed

src/witness/yamlWitness.ml

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

61-
let invariant invariant: Invariant.t = {
62-
string = invariant;
63-
type_ = "assertion";
64-
format = "C";
65-
}
66-
(* TODO: remove above? *)
67-
6861
(* TODO: remove primes from name *)
6962
let location_invariant' ~location ~(invariant): InvariantSet.Invariant.t = {
7063
invariant_type = LocationInvariant {
@@ -229,7 +222,6 @@ struct
229222
let cnt_loop_invariant = ref 0 in
230223
let cnt_location_invariant = ref 0 in
231224
let cnt_flow_insensitive_invariant = ref 0 in
232-
(* TODO: precondition invariants? *)
233225

234226
let invariant_global_nodes = lazy (R.ask_global InvariantGlobalNodes) in
235227

src/witness/yamlWitnessType.ml

Lines changed: 0 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -151,31 +151,6 @@ struct
151151
{file_name; file_hash; line; column; function_}
152152
end
153153

154-
module Invariant =
155-
struct
156-
type t = {
157-
string: string;
158-
type_: string;
159-
format: string;
160-
}
161-
[@@deriving eq, ord, hash]
162-
163-
let to_yaml {string; type_; format} =
164-
`O [
165-
("string", `String string);
166-
("type", `String type_);
167-
("format", `String format);
168-
]
169-
170-
let of_yaml y =
171-
let open GobYaml in
172-
let+ string = y |> find "string" >>= to_string
173-
and+ type_ = y |> find "type" >>= to_string
174-
and+ format = y |> find "format" >>= to_string in
175-
{string; type_; format}
176-
end
177-
(* TODO: remove above things? *)
178-
179154
module InvariantSet =
180155
struct
181156
module LoopInvariant =

0 commit comments

Comments
 (0)