From d44a0f491308b2782acf2a8fa612864ddd870899 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Tue, 4 Jan 2022 11:54:22 +0100
Subject: [PATCH] Add debug switch to verification process.
---
src/autodetection.ml | 2 +-
src/autodetection.mli | 2 +-
src/main.ml | 9 ++++++---
src/verification.ml | 10 +++++-----
src/verification.mli | 6 ++++--
5 files changed, 17 insertions(+), 12 deletions(-)
diff --git a/src/autodetection.ml b/src/autodetection.ml
index ff79daa9..d23bd403 100644
--- a/src/autodetection.ml
+++ b/src/autodetection.ml
@@ -16,7 +16,7 @@ let rec lookup_file dirs filename =
let file = Caml.Filename.concat dir filename in
if Sys.file_exists file then file else lookup_file dirs filename
-let autodetect ~debug () =
+let autodetect ?(debug = false) () =
let open Why3 in
if debug then Debug.set_flag Autodetection.debug;
let caisar_conf =
diff --git a/src/autodetection.mli b/src/autodetection.mli
index 42842afe..65e97b26 100644
--- a/src/autodetection.mli
+++ b/src/autodetection.mli
@@ -4,7 +4,7 @@
(* *)
(**************************************************************************)
-val autodetect : debug:bool -> unit -> Why3.Whyconf.config
+val autodetect : ?debug:bool -> unit -> Why3.Whyconf.config
(** Perform the autodetection of provers.
@param debug activates debug information. *)
diff --git a/src/main.ml b/src/main.ml
index a86c5a94..34ec82cd 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -66,7 +66,10 @@ let config detect () =
provers))
let verify format loadpath memlimit prover files =
- List.iter ~f:(Verification.verify format loadpath ?memlimit ~prover) files
+ let debug = match Logs.level () with Some Debug -> true | _ -> false in
+ List.iter
+ ~f:(Verification.verify ~debug format loadpath ?memlimit ~prover)
+ files
let exec_cmd cmdname cmd =
Logs.debug (fun m -> m "Command `%s'." cmdname);
@@ -141,11 +144,11 @@ let verify_cmd =
let man = [ `S Manpage.s_description; `P doc ] in
( Term.(
ret
- (const (fun format loadpath memlimit prover files ->
+ (const (fun format loadpath memlimit prover files _ ->
`Ok
(exec_cmd cmdname (fun () ->
verify format loadpath memlimit prover files)))
- $ format $ loadpath $ memlimit $ prover $ files)),
+ $ format $ loadpath $ memlimit $ prover $ files $ setup_logs)),
Term.info cmdname ~sdocs:Manpage.s_common_options ~exits ~doc ~man )
let default_cmd =
diff --git a/src/verification.ml b/src/verification.ml
index c7507c5b..5bfa184c 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -7,9 +7,9 @@
open Base
module Filename = Caml.Filename
-let () = Language.register_nnet_support ()
-
-let () = Language.register_onnx_support ()
+let () =
+ Language.register_nnet_support ();
+ Language.register_onnx_support ()
let create_env loadpath =
let config = Autodetection.autodetect ~debug:true () in
@@ -73,9 +73,9 @@ let call_prover ~limit (prover : Why3.Whyconf.config_prover) driver task =
Fmt.pr "Goal %a: %a@." Pretty.print_pr (Task.task_goal task)
Call_provers.print_prover_answer answer
-let verify format loadpath ?memlimit ~prover file =
+let verify ?(debug = false) format loadpath ?memlimit ~prover file =
let open Why3 in
- (* Debug.(set_flag (lookup_flag "call_prover")); *)
+ if debug then Debug.set_flag (Debug.lookup_flag "call_prover");
let env, config = create_env loadpath in
let steplimit = None in
let timeout = None in
diff --git a/src/verification.mli b/src/verification.mli
index 95432d09..fd4c7635 100644
--- a/src/verification.mli
+++ b/src/verification.mli
@@ -5,15 +5,17 @@
(**************************************************************************)
val verify :
+ ?debug:bool ->
string option ->
string list ->
?memlimit:int ->
prover:string ->
string ->
unit
-(** [verify format loadpath memlimit prover file] launches a verification of the
- given [file] with the provided [prover].
+(** [verify debug format loadpath memlimit prover file] launches a verification
+ of the given [file] with the provided [prover].
+ @param debug when set, enables debug information.
@param format is the [file] format.
@param loadpath is the additional loadpath.
@param memlimit
--
GitLab