From ebec1d4260f3ec4336421261aa0e24f3a18f2fa9 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Tue, 12 Apr 2022 15:14:25 +0200
Subject: [PATCH] [cmdline] Use custom input file parser and printer in order
to accept - for stdin.
---
src/main.ml | 3 ++-
src/verification.ml | 19 +++++++++++++++++--
src/verification.mli | 9 ++++++++-
3 files changed, 27 insertions(+), 4 deletions(-)
diff --git a/src/main.ml b/src/main.ml
index 0a45a707..4aea0394 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -122,7 +122,8 @@ let verify_cmd =
let cmdname = "verify" in
let files =
let doc = "Files to verify." in
- Arg.(value & pos_all string [] & info [] ~doc)
+ let file_or_stdin = Verification.File.(of_string, pretty) in
+ Arg.(value & pos_all file_or_stdin [] & info [] ~doc)
in
let format =
let doc = "File format." in
diff --git a/src/verification.ml b/src/verification.ml
index 863155b3..51dd4f56 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -8,6 +8,21 @@ open Why3
open Base
module Filename = Caml.Filename
+module File = struct
+ type t = Stdin | File of string
+
+ let of_string s =
+ if String.equal s "-"
+ then `Ok Stdin
+ else if Caml.Sys.file_exists s
+ then `Ok (File s)
+ else `Error (Fmt.str "no '%s' file or directory" s)
+
+ let pretty fmt = function
+ | Stdin -> Fmt.string fmt "-"
+ | File f -> Fmt.string fmt f
+end
+
let () =
Language.register_nnet_support ();
Language.register_onnx_support ()
@@ -84,9 +99,9 @@ let verify ?(debug = false) format loadpath ?memlimit ?timeout prover file =
in
let _, mstr_theory =
match file with
- | "-" ->
+ | File.Stdin ->
("stdin", Env.(read_channel ?format base_language env "stdin" Caml.stdin))
- | file ->
+ | File file ->
let mlw_files, _ = Env.(read_file ?format base_language env file) in
(file, mlw_files)
in
diff --git a/src/verification.mli b/src/verification.mli
index 117f64ca..36ba72e0 100644
--- a/src/verification.mli
+++ b/src/verification.mli
@@ -4,6 +4,13 @@
(* *)
(**************************************************************************)
+module File : sig
+ type t
+
+ val of_string : string -> [ `Ok of t | `Error of string ]
+ val pretty : Format.formatter -> t -> unit
+end
+
val verify :
?debug:bool ->
string option ->
@@ -11,7 +18,7 @@ val verify :
?memlimit:int ->
?timeout:int ->
Prover.t ->
- string ->
+ File.t ->
unit
(** [verify debug format loadpath memlimit timeout prover file] launches a
verification of the given [file] with the provided [prover].
--
GitLab