Commit c77a1a86 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

New option --extra-expl-prefix to specify other prefixes for VC explanations

parent ad518fe0
* marks an incompatible change
library
Tools
* add a command-line option --extra-expl-prefix to specify
additional possible prefixes for VC explanations. (Available for
why3 commands "prove" and "ide".)
Library
* improved bitvectors theories
Encodings
......@@ -9,7 +14,7 @@ Encodings
cases of equality and maps) then the translation to SMT-LIB
format is direct
provers
Provers
o discarded support for Alt-Ergo versions older than 0.95.2
o support for Coq 8.4pl6 (released Apr 9, 2015)
o support for Gappa 1.2.0 (released May 19, 2015)
......
......@@ -185,7 +185,7 @@ The \texttt{prove} command executes the following steps:
%\texttt{why3} calls the provers sequentially, use \texttt{why3bench} if *)
%you want to call the provers concurrently. *)
\noindent
\subsection{Prover Results}
The provers can give the following output:
\begin{description}
\item[Valid] The goal is proved in the given context.
......@@ -212,6 +212,17 @@ The provers can give the following output:
%then written in the prover syntax into a file located in the directory
%given to the \verb|-o/--output| option.
\subsection{Additional Options}
\label{sec:proveoptions}
\begin{description}
\item[\texttt{-{}-get-ce}] activates the generation of a potential counter-example when a proof does not succeed (experimental).
\item[\texttt{-{}-extra-expl-prefix \textsl{<s>}}] specifies
\textsl{s} as an additional prefix for labels that denotes VC
explanations. The option can be used several times to specify
several prefixes.
\end{description}
\section{The \texttt{ide} Command}
\label{sec:ideref}
......@@ -439,6 +450,13 @@ are grouped together under several tabs.
decision by clicking on it.
\end{description}
\subsection{Additional Command-Line Options}
The \texttt{ide} command also accepts the following options described for the command \texttt{prove} in Section~\ref{sec:proveoptions}.
\begin{description}
\item[\texttt{-{}-extra-expl-prefix \textsl{<s>}}]
\end{description}
\section{The \texttt{bench} Command}
......
......@@ -50,6 +50,7 @@ let spec = Arg.align [
Arg.String (fun s -> input_files := s :: !input_files),
"<file> add file to the project (ignored if it is already there)";
*)
Termcode.arg_extra_expl_prefix
]
let usage_str = sprintf
......
......@@ -15,14 +15,25 @@ open Term
(* explanations *)
(*******************************)
let expl_prefixes = ref ["expl:"]
let arg_extra_expl_prefix =
("--extra-expl-prefix",
Arg.String (fun s -> expl_prefixes := s :: !expl_prefixes),
"<s> register s as an additional prefix for VC explanations")
let collect_expls lab =
Ident.Slab.fold
(fun lab acc ->
let lab = lab.Ident.lab_string in
try
let s = Strings.remove_prefix "expl:" lab in s :: acc
with Not_found -> acc)
let rec aux l =
match l with
| [] -> acc
| p :: r ->
try
let s = Strings.remove_prefix p lab in s :: acc
with Not_found -> aux r
in aux !expl_prefixes)
lab
[]
......
......@@ -11,6 +11,8 @@
(** Explanations *)
val arg_extra_expl_prefix : string * Arg.spec * string
val goal_expl_task:
root:bool -> Task.task -> Ident.ident * string option * Task.task
......
......@@ -139,11 +139,12 @@ let option_list = [
"--print-theory", Arg.Set opt_print_theory,
" print selected theories";
"--print-namespace", Arg.Set opt_print_namespace,
" print namespaces of selected theories";
" print namespaces of selected theories";
Debug.Args.desc_shortcut
"parse_only" "--parse-only" " stop after parsing";
Debug.Args.desc_shortcut
"type_only" "--type-only" " stop after type checking";
Termcode.arg_extra_expl_prefix;
"--get-ce", Arg.Set opt_cntexmp,
" gets the counter-example model" ]
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment