Skip to content

Commit f953b8f

Browse files
committed
Add witness missing verdict to YAML witness validation
Better than "EXCEPTION (Failure)" as verdict.
1 parent 06086c6 commit f953b8f

File tree

1 file changed

+8
-3
lines changed

1 file changed

+8
-3
lines changed

src/witness/yamlWitness.ml

+8-3
Original file line numberDiff line numberDiff line change
@@ -565,6 +565,8 @@ struct
565565
}
566566

567567
let validate () =
568+
let open GobResult.Syntax in
569+
568570
let location_locator = Locator.create () in
569571
let loop_locator = Locator.create () in
570572
(* TODO: add all CFG nodes, not just live ones from lh, like UnassumeAnalysis *)
@@ -579,9 +581,12 @@ struct
579581

580582
let inv_parser = InvariantParser.create FileCfg.file in
581583

582-
let yaml = match Yaml_unix.of_file (Fpath.v (GobConfig.get_string "witness.yaml.validate")) with
583-
| Ok yaml -> yaml
584-
| Error (`Msg m) -> failwith ("Yaml_unix.of_file: " ^ m)
584+
let* yaml =
585+
Yaml_unix.of_file (Fpath.v (GobConfig.get_string "witness.yaml.validate"))
586+
|> Result.map_error (fun (`Msg m) ->
587+
Logs.error "Yaml_unix.of_file: %s" m;
588+
"witness missing"
589+
)
585590
in
586591
let yaml_entries = yaml |> GobYaml.list |> BatResult.get_ok in
587592

0 commit comments

Comments
 (0)