From f5793dfdc7b35d2258b9dd90703c9c5914cb7951 Mon Sep 17 00:00:00 2001
From: Julien Girard <julien.girard2@cea.fr>
Date: Tue, 5 Apr 2022 10:36:01 +0200
Subject: [PATCH] [SAVer] Optional argument for dataset-csv.
---
src/main.ml | 2 +-
src/verification.ml | 8 +++++---
src/verification.mli | 2 +-
3 files changed, 7 insertions(+), 5 deletions(-)
diff --git a/src/main.ml b/src/main.ml
index 60b7c26f..214f8df4 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -73,7 +73,7 @@ let verify format loadpath memlimit timeout prover dataset_csv files =
List.iter
~f:
(Verification.verify ~debug format loadpath ?memlimit ?timeout prover
- ~dataset_csv)
+ ?dataset_csv)
files
let exec_cmd cmdname cmd =
diff --git a/src/verification.ml b/src/verification.ml
index 3a7bacdb..ee54efab 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -60,8 +60,8 @@ let answer_saver limit config task env prover dataset_csv =
let handle_task_saver task env dataset_csv command =
let dataset_filename =
match dataset_csv with
- | Some s -> s
- | None -> failwith "Error, no dataset provided for SAVer."
+ | "" -> failwith "Error, no dataset provided for SAVer."
+ | s -> s
in
let goal = Task.task_goal_fmla task in
let eps, svm_filename =
@@ -186,11 +186,13 @@ let call_prover ~limit config (prover : Why3.Whyconf.config_prover) driver env
Call_provers.print_prover_answer prover_answer
let verify ?(debug = false) format loadpath ?memlimit ?timeout prover
- ~dataset_csv file =
+ ?dataset_csv file =
+ let open Why3 in
if debug then Debug.set_flag (Debug.lookup_flag "call_prover");
let env, config = create_env loadpath in
let steplimit = None in
let steps = match steplimit with Some 0 -> None | _ -> steplimit in
+ let dataset_csv = Option.value dataset_csv ~default:"" in
let limit =
let memlimit =
Option.value memlimit ~default:Whyconf.(memlimit (get_main config))
diff --git a/src/verification.mli b/src/verification.mli
index 5f8f7ae2..270048cd 100644
--- a/src/verification.mli
+++ b/src/verification.mli
@@ -18,7 +18,7 @@ val verify :
?memlimit:int ->
?timeout:int ->
Prover.t ->
- dataset_csv:string option ->
+ ?dataset_csv:string ->
File.t ->
unit
(** [verify debug format loadpath memlimit timeout prover file] launches a
--
GitLab