From 45cb0b31dfa3f97dd9336494be6848e10f2b53b5 Mon Sep 17 00:00:00 2001 From: Michele Alberti <michele.alberti@cea.fr> Date: Mon, 3 Oct 2022 12:14:59 +0200 Subject: [PATCH] [SAVer] Rename module. --- src/{saver.ml => SAVer.ml} | 0 src/{saver.mli => SAVer.mli} | 4 ++-- src/verification.ml | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) rename src/{saver.ml => SAVer.ml} (100%) rename src/{saver.mli => SAVer.mli} (93%) diff --git a/src/saver.ml b/src/SAVer.ml similarity index 100% rename from src/saver.ml rename to src/SAVer.ml diff --git a/src/saver.mli b/src/SAVer.mli similarity index 93% rename from src/saver.mli rename to src/SAVer.mli index 2bec2d2..2119b52 100644 --- a/src/saver.mli +++ b/src/SAVer.mli @@ -24,8 +24,8 @@ open Why3 type answer = { prover_answer : Call_provers.prover_answer; - nb_total : int; (* Total number of data points. *) - nb_proved : int; (* Number of data points verifying the property. *) + nb_total : int; (** Total number of data points. *) + nb_proved : int; (** Number of data points verifying the property. *) } val call : diff --git a/src/verification.ml b/src/verification.ml index 2d12c9d..836ff1b 100644 --- a/src/verification.ml +++ b/src/verification.ml @@ -74,7 +74,7 @@ let answer_saver limit config env config_prover dataset_csv task = | None -> invalid_arg "No dataset provided for SAVer" | Some filename -> filename in - let answer = Saver.call limit config env config_prover ~dataset task in + let answer = SAVer.call limit config env config_prover ~dataset task in let prover_answer = answer.prover_answer in let additional_info = Fmt.str "(%d/%d)" answer.nb_proved answer.nb_total in (prover_answer, Some additional_info) -- GitLab