diff --git a/nix/default.nix b/nix/default.nix
index bf61a1b3287b163d90aa7329e1d59c082d89c136..8ce82489000bf017f7eb68fcfe10648b9cd72e59 100644
--- a/nix/default.nix
+++ b/nix/default.nix
@@ -7,10 +7,8 @@ let mk_buildInputs = { opamPackages ? [], nixPackages ? [] } :
"ppx_deriving" "ppx_deriving_yojson"
{ name = "coq"; constraint = "=8.12.0"; }
{ name = "alt-ergo" ; constraint = "=2.2.0"; }
- { name = "why3" ; constraint = "=1.3.3"; }
- { name = "why3-coq" ; constraint = "=1.3.3"; }
- { name = "menhir"; constraint = "=20200624"; }
- { name = "dune"; constraint = "=2.7.1"; }
+ { name = "why3" ; constraint = "=1.4.0"; }
+ { name = "why3-coq" ; constraint = "=1.4.0"; }
] ++ opamPackages
);
ocamlAttr = ocaml_version;
@@ -186,7 +184,7 @@ pkgs.lib.makeExtensible
make create_share_link
mkdir home
HOME=$(pwd)/home
- why3 config --detect
+ why3 config detect
make src/plugins/wp/tests/test_config_qualif
export FRAMAC_WP_CACHE=replay
export FRAMAC_WP_CACHEDIR=${plugins.wp-cache.src}
@@ -215,7 +213,7 @@ pkgs.lib.makeExtensible
make create_share_link
mkdir home
HOME=$(pwd)/home
- why3 config --detect
+ why3 config detect
make src/plugins/aorai/tests/ptests_config
make PTESTS_OPTS="-config prove -error-code" Aorai_TESTS
'';
@@ -310,7 +308,7 @@ pkgs.lib.makeExtensible
# Setup Why3
mkdir home
HOME=$(pwd)/home
- why3 config --detect
+ why3 config detect
# Setup WP related
export CAVEAT_IMPORTER_NIX_MODE=yes
export FRAMAC_WP_CACHE=replay
diff --git a/nix/frama-ci.nix b/nix/frama-ci.nix
index 0dc2337bb51f28e5e8d99196fc542f26a699e745..65141e9684de9637e600df87397aeb97366afdbf 100644
--- a/nix/frama-ci.nix
+++ b/nix/frama-ci.nix
@@ -5,8 +5,8 @@ let
src = builtins.fetchGit {
"url" = "https://bobot:${password}@git.frama-c.com/frama-c/Frama-CI.git";
"name" = "Frama-CI";
- "rev" = "22961f3356c3eb1279d817772b4f19c352d055a7";
- "ref" = "master";
+ "rev" = "f86e807d6f440ac4479b78f8419dfd817803419d";
+ "ref" = "feature/wp/versions-bump";
};
in
{
diff --git a/opam/opam b/opam/opam
index 2ce4efbb5ddb8ec49da811f7047d633a86568380..b00e5233da31a96c84114079e18496dc9182001e 100644
--- a/opam/opam
+++ b/opam/opam
@@ -117,7 +117,7 @@ depends: [
"ocaml" { >= "4.08.1" }
"ocamlfind" # needed beyond build stage, used by -load-module
"ocamlgraph" { >= "1.8.8" }
- "why3" { >= "1.3.3" & < "1.4~" }
+ "why3" { >= "1.4.0" & < "1.5~" }
"yojson"
"zarith"
]
@@ -142,5 +142,5 @@ messages: [
]
post-messages: [
- "Why3 provers setup: rm -f ~/.why3.conf ; why3 config --detect"
+ "Why3 provers setup: rm -f ~/.why3.conf ; why3 config detect"
]
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index adb7fd3e831b90bc20e8cdb0d4acdd56eb84ac60..96090a60d09449d9f4874ff10b7f5b29f9d13540 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1122,7 +1122,7 @@ let prover_task env prover task =
let config = Why3Provers.config () in
let prover_config = Why3.Whyconf.get_prover_config config prover in
let drv = Why3.Whyconf.load_driver (Why3.Whyconf.get_main config)
- env prover_config.driver prover_config.extra_drivers in
+ env prover_config in
let remove_for_prover =
if prover.prover_name = "Alt-Ergo"
then Filter_axioms.remove_for_altergo
@@ -1204,7 +1204,7 @@ let ping_prover_call p =
Wp_parameters.debug ~dkey
"@[@[Why3 result for %a:@] @[%a@] and @[%a@]@."
Why3.Whyconf.print_prover p.prover
- (Why3.Call_provers.print_prover_result ~json_model:false) pr
+ (Why3.Call_provers.print_prover_result ~json:false) pr
VCS.pp_result r;
Task.Return (Task.Result r)
diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml
index 8c7ffc09a9b9c47a6ff053e526c4846603782ca9..190b02c4d8ee09511a1b55f6d490a3a0a25b2781 100644
--- a/src/plugins/wp/Why3Provers.ml
+++ b/src/plugins/wp/Why3Provers.ml
@@ -26,10 +26,7 @@
let cfg = lazy
begin
- try
- let config = Why3.Whyconf.read_config None in
- let config = Why3.Whyconf.load_default_config_if_needed config in
- config
+ try Why3.Whyconf.init_config None
with exn ->
Wp_parameters.abort "%a" Why3.Exn_printer.exn_printer exn
end
@@ -46,10 +43,10 @@ let configure =
begin
let args = Array.of_list ("why3"::Wp_parameters.Why3Flags.get ()) in
begin try
- Arg.parse_argv ~current:(ref 0) args
+ Why3.Getopt.parse_all
(Why3.Debug.Args.[desc_debug;desc_debug_all;desc_debug_list])
(fun opt -> raise (Arg.Bad ("unknown option: " ^ opt)))
- "Why3 options"
+ args
with Arg.Bad s | Arg.Help s -> Wp_parameters.abort "%s" s
end;
ignore (Why3.Debug.Args.option_list ());
diff --git a/src/plugins/wp/configure.ac b/src/plugins/wp/configure.ac
index 90dcf3ec7df136174aa18560a6bbaaf099839616..7a16150db15ae19ab1228a7cd66b4b8919e262b4 100644
--- a/src/plugins/wp/configure.ac
+++ b/src/plugins/wp/configure.ac
@@ -63,15 +63,15 @@ case $WHY3VERSION in
AC_MSG_RESULT([not found!])
plugin_disable(wp,[why3 not found])
;;
- 0.* | 1.[[012]].* | 1.3.0 | 1.3.1 | 1.3.2)
- AC_MSG_RESULT([found $WHY3VERSION: requires 1.3.3+])
+ 0.* | 1.[[0123]].*)
+ AC_MSG_RESULT([found $WHY3VERSION: requires 1.4.0+])
plugin_disable(wp,[non-supported why3 $WHY3VERSION])
;;
- 1.3.*)
+ 1.4.*)
AC_MSG_RESULT([found $WHY3VERSION: ok])
;;
*)
- AC_MSG_RESULT([found $WHY3VERSION: might work (should be 1.3.3+)])
+ AC_MSG_RESULT([found $WHY3VERSION: might work (should be 1.4.0+)])
;;
esac
fi
diff --git a/src/plugins/wp/doc/manual/wp_intro.tex b/src/plugins/wp/doc/manual/wp_intro.tex
index 03468d5a7b3d0d04a535f8561b616f213b7c5fc7..0daf729a37f81929f86afc2df5bf8fa3d21ed2a3 100644
--- a/src/plugins/wp/doc/manual/wp_intro.tex
+++ b/src/plugins/wp/doc/manual/wp_intro.tex
@@ -59,6 +59,14 @@ order to fulfill proof obligations. An easy choice is to install the
\textsc{inria} and now by \textsc{OcamlPro}\footnote{\textsf{Alt-Ergo}:
\url{https://alt-ergo.ocamlpro.com/}}. When using the \textsf{Opam} package
manager, these tools are automatically installed with \textsf{Frama-C}.
+
+When updating or installing \textsf{Why-3}, the following command should be
+run to detect available provers:
+
+\begin{lstlisting}[basicstyle=\ttfamily]
+rm -f ~/.why3.conf ; why3 config detect
+\end{lstlisting}
+
See the documentation of \textsf{Why-3} to install other provers.
@@ -170,10 +178,10 @@ weakest precondition $W$; we can then conclude that $P$ precondition
of $f$ always entails its postcondition $Q$. This proof can be summarized by
the following diagram:
-$$
+$$
\frac%
{\quad(P \Longrightarrow W) \quad\quad \{W\}\,f\,\{Q\} \quad}%
-{\{P\}\,f\,\{Q\}}
+{\{P\}\,f\,\{Q\}}
$$
This is the main idea of how to prove a property by weakest
@@ -247,7 +255,7 @@ plug-in, which makes \textsf{WP} complementary to \textsf{Jessie}.
\item[\texttt{Hoare} model.] A very efficient model that generates
concise proof obligations. It simply maps each \textsf{C} variable to one
pure logical variable.\par
-
+
However, the heap cannot be represented in this model, and
expressions such as \texttt{*p} cannot be translated at all. You
can still represent pointer values, but you cannot read or write
@@ -262,7 +270,7 @@ plug-in, which makes \textsf{WP} complementary to \textsf{Jessie}.
In order to generate reasonable proof obligations, the values stored
in the global array are not the machine ones, but the logical
ones. Hence, all \textsf{C} integer types are represented by
- mathematical integers and each pointer type to a given type is represented
+ mathematical integers and each pointer type to a given type is represented
by a specific logical abstract datatype.\par
A consequence of having separated arrays is that heterogeneous casts
@@ -271,7 +279,7 @@ plug-in, which makes \textsf{WP} complementary to \textsf{Jessie}.
pointer to \texttt{char}, and then access the internal
representation of the original \texttt{int} value into memory.
- However, variants of the \texttt{Typed} model enable limited forms of casts.
+ However, variants of the \texttt{Typed} model enable limited forms of casts.
See chapter~\ref{wp-models} for details.
\item[\texttt{Bytes} model. (Not Implemented Yet).] This is a
diff --git a/src/plugins/wp/tests/why3/oracle_qualif/spec_memory.res.oracle b/src/plugins/wp/tests/why3/oracle_qualif/spec_memory.res.oracle
index 84dd9791cd3af005144c2029d1af4995b496b25b..c4a9e9694ac7bc02afa400d170568b7cfd1db643 100644
--- a/src/plugins/wp/tests/why3/oracle_qualif/spec_memory.res.oracle
+++ b/src/plugins/wp/tests/why3/oracle_qualif/spec_memory.res.oracle
@@ -1,15 +1,60 @@
-tests/why3/spec_memory.why Spec_memory check_valid_rd: Valid
-tests/why3/spec_memory.why Spec_memory check_valid: Valid
-tests/why3/spec_memory.why Spec_memory invalid_spec: Valid
-tests/why3/spec_memory.why Spec_memory invalid_null_spec: Valid
-tests/why3/spec_memory.why Spec_memory invalid_null: Valid
-tests/why3/spec_memory.why Spec_memory invalid_empty: Valid
-tests/why3/spec_memory.why Spec_memory valid_rd_null: Valid
-tests/why3/spec_memory.why Spec_memory valid_rw_null: Valid
-tests/why3/spec_memory.why Spec_memory valid_obj_null: Valid
-tests/why3/spec_memory.why Spec_memory INC_P: Valid
-tests/why3/spec_memory.why Spec_memory INC_A: Valid
-tests/why3/spec_memory.why Spec_memory INC_1: Valid
-tests/why3/spec_memory.why Spec_memory INC_2: Valid
-tests/why3/spec_memory.why Spec_memory INC_3: Valid
-tests/why3/spec_memory.why Spec_memory INC_4: Valid
+File "tests/why3/spec_memory.why", line 24, characters 4-56:
+Verification condition check_valid_rd.
+Prover result is: Valid.
+
+File "tests/why3/spec_memory.why", line 27, characters 4-56:
+Verification condition check_valid.
+Prover result is: Valid.
+
+File "tests/why3/spec_memory.why", line 30, characters 4-62:
+Verification condition invalid_spec.
+Prover result is: Valid.
+
+File "tests/why3/spec_memory.why", line 34, characters 4-76:
+Verification condition invalid_null_spec.
+Prover result is: Valid.
+
+File "tests/why3/spec_memory.why", line 38, characters 4-51:
+Verification condition invalid_null.
+Prover result is: Valid.
+
+File "tests/why3/spec_memory.why", line 42, characters 4-79:
+Verification condition invalid_empty.
+Prover result is: Valid.
+
+File "tests/why3/spec_memory.why", line 46, characters 4-59:
+Verification condition valid_rd_null.
+Prover result is: Valid.
+
+File "tests/why3/spec_memory.why", line 49, characters 4-59:
+Verification condition valid_rw_null.
+Prover result is: Valid.
+
+File "tests/why3/spec_memory.why", line 52, characters 4-34:
+Verification condition valid_obj_null.
+Prover result is: Valid.
+
+File "tests/why3/spec_memory.why", line 56, characters 4-77:
+Verification condition INC_P.
+Prover result is: Valid.
+
+File "tests/why3/spec_memory.why", line 60, characters 4-169:
+Verification condition INC_A.
+Prover result is: Valid.
+
+File "tests/why3/spec_memory.why", line 67, characters 4-63:
+Verification condition INC_1.
+Prover result is: Valid.
+
+File "tests/why3/spec_memory.why", line 71, characters 4-64:
+Verification condition INC_2.
+Prover result is: Valid.
+
+File "tests/why3/spec_memory.why", line 75, characters 4-161:
+Verification condition INC_3.
+Prover result is: Valid.
+
+File "tests/why3/spec_memory.why", line 82, characters 4-178:
+Verification condition INC_4.
+Prover result is: Valid.
+
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle
index bb756593da2a38fa0f139b26a820aac8f23aa66f..d1903f4234f1308657d5768f5132525318f1bb6d 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle
@@ -2,6 +2,6 @@
WP Requirements for Qualif Tests (3)
----------------------------------------------------------
1. The Alt-Ergo theorem prover, version 2.2.0
-2. The Why3 platform, version 1.3.3
+2. The Why3 platform, version 1.4.0
3. The Coq Proof Assistant, version 8.12.0
----------------------------------------------------------