From fd15af2ee55d62fecb3c87b5a7ef943b50fe41ed Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Tue, 9 Nov 2021 18:07:58 +0100
Subject: [PATCH] Add mli files for autodetection and verification.

---
 .ocamlformat          |  1 +
 src/autodetection.mli | 10 ++++++++++
 src/verification.mli  | 20 ++++++++++++++++++++
 3 files changed, 31 insertions(+)
 create mode 100644 src/autodetection.mli
 create mode 100644 src/verification.mli

diff --git a/.ocamlformat b/.ocamlformat
index 7523471a..b883181e 100644
--- a/.ocamlformat
+++ b/.ocamlformat
@@ -3,3 +3,4 @@ exp-grouping=parens
 if-then-else=keyword-first
 max-indent=2
 wrap-comments=true
+parse-docstrings=true
diff --git a/src/autodetection.mli b/src/autodetection.mli
new file mode 100644
index 00000000..42842afe
--- /dev/null
+++ b/src/autodetection.mli
@@ -0,0 +1,10 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of CAISAR.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
+val autodetect : debug:bool -> unit -> Why3.Whyconf.config
+(** Perform the autodetection of provers.
+
+    @param debug activates debug information. *)
diff --git a/src/verification.mli b/src/verification.mli
new file mode 100644
index 00000000..95432d09
--- /dev/null
+++ b/src/verification.mli
@@ -0,0 +1,20 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of CAISAR.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
+val verify :
+  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].
+
+    @param format is the [file] format.
+    @param loadpath is the additional loadpath.
+    @param memlimit
+      is the memory limit (in megabytes) granted to the verification. *)
-- 
GitLab