From 474aecaeaf9dd3aa962f3a3eb41e1fc732afc62d Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Thu, 1 Sep 2022 10:32:52 +0200
Subject: [PATCH] [SAVer] Use more robust realpath rather than prefixing the
cwd path.
---
src/verification.ml | 11 ++++++-----
1 file changed, 6 insertions(+), 5 deletions(-)
diff --git a/src/verification.ml b/src/verification.ml
index 044f7b78..dfac916f 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -112,8 +112,8 @@ let answer_saver limit config task env prover dataset_csv =
| _ -> failwith "Unsupported by SAVer.")
| _ -> failwith "Unsupported by SAVer."
in
- let svm_file = Filename.concat (Caml.Sys.getcwd ()) svm_filename in
- let dataset_file = Filename.concat (Caml.Sys.getcwd ()) dataset_filename in
+ let svm_file = Unix.realpath svm_filename in
+ let dataset_file = Unix.realpath dataset_filename in
let command = Re__Core.replace_string svm ~by:svm_file command in
let command = Re__Core.replace_string dataset ~by:dataset_file command in
let command = Re__Core.replace_string epsilon ~by:eps command in
@@ -154,10 +154,11 @@ let answer_saver limit config task env prover dataset_csv =
= Int.of_string (Re__Core.Group.get g 2)
then Call_provers.Valid
else Call_provers.Invalid
- | None -> Call_provers.HighFailure
+ | None -> Call_provers.HighFailure)
+ | _ ->
(* Any other answer than HighFailure should never happen as we do not
- define anything in SAVer's driver. *))
- | _ -> assert false
+ define anything in SAVer's driver. *)
+ assert false
in
answer
--
GitLab