Skip to content
Snippets Groups Projects
Commit fd15af2e authored by Michele Alberti's avatar Michele Alberti
Browse files

Add mli files for autodetection and verification.

parent d4f02558
No related branches found
No related tags found
No related merge requests found
...@@ -3,3 +3,4 @@ exp-grouping=parens ...@@ -3,3 +3,4 @@ exp-grouping=parens
if-then-else=keyword-first if-then-else=keyword-first
max-indent=2 max-indent=2
wrap-comments=true wrap-comments=true
parse-docstrings=true
(**************************************************************************)
(* *)
(* This file is part of CAISAR. *)
(* *)
(**************************************************************************)
val autodetect : debug:bool -> unit -> Why3.Whyconf.config
(** Perform the autodetection of provers.
@param debug activates debug information. *)
(**************************************************************************)
(* *)
(* 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. *)
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment