Skip to content
Snippets Groups Projects
Commit d12ab074 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

Merge branch 'feature/wp/versions-bump' into 'master' 

WP tools versions

Closes #2548, #41, #40, and #1020

See merge request frama-c/frama-c!3117
parents 18879ee1 569423fa
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 92 additions and 44 deletions
nix/default.nix
+ 5
− 7
View file @ d12ab074
......@@ -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
......
nix/frama-ci.nix
+ 2
− 2
View file @ d12ab074
......@@ -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
{
......
opam/opam
+ 2
− 2
View file @ d12ab074
......@@ -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"
]
src/plugins/wp/ProverWhy3.ml
+ 2
− 2
View file @ d12ab074
......@@ -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)
......
src/plugins/wp/Why3Provers.ml
+ 3
− 6
View file @ d12ab074
......@@ -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 ());
......
src/plugins/wp/configure.ac
+ 4
− 4
View file @ d12ab074
......@@ -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
......
src/plugins/wp/doc/manual/wp_intro.tex
+ 13
− 5
View file @ d12ab074
......@@ -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
......
src/plugins/wp/tests/why3/oracle_qualif/spec_memory.res.oracle
+ 60
− 15
View file @ d12ab074
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.
src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle
+ 1
− 1
View file @ d12ab074
......@@ -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
----------------------------------------------------------
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