diff --git a/devel_tools/docker/frama-c.dev/Dockerfile b/devel_tools/docker/frama-c.dev/Dockerfile
index a1a8c63ae8bd91f412e6e4231415b4f75781ed2e..67acc324b1438531ddb3f5e66a162f9004d8e6bf 100644
--- a/devel_tools/docker/frama-c.dev/Dockerfile
+++ b/devel_tools/docker/frama-c.dev/Dockerfile
@@ -20,20 +20,20 @@ RUN opam update -y && opam install depext -y
# Install packages from reference configuration
RUN apt-get update && opam update -y && opam depext --install -y --verbose \
- alt-ergo.2.0.0 \
+ alt-ergo.2.2.0 \
apron.v0.9.12 \
conf-graphviz.0.1 \
mlgmpidl.1.2.12 \
ocamlfind.1.8.1 \
ocamlgraph.1.8.8 \
ppx_deriving_yojson.3.5.2 \
- why3.1.3.1 \
+ why3.1.3.3 \
yojson.1.7.0 \
zarith.1.9.1 \
zmq.5.1.3 \
&& rm -rf /var/lib/apt/lists/*
-RUN why3 config --full-config
+RUN why3 config --detect
# with_source: keep Frama-C sources
ARG with_source=no
@@ -50,6 +50,7 @@ RUN cd /root && \
# with_test: run Frama-C tests; requires "with_source=yes"
ARG with_test=no
+# run general tests, then test that WP can see external provers
RUN if [ "${with_test}" != "no" ]; then \
apt-get update && \
opam update -y && opam depext --install -y \
@@ -59,5 +60,8 @@ RUN if [ "${with_test}" != "no" ]; then \
&& \
rm -rf /var/lib/apt/lists/* && \
cd /root/frama-c && \
- make tests; \
+ make tests && \
+ (cd src/plugins/wp/tests/ && \
+ frama-c -wp wp_gallery/binary-multiplication-without-overflow.c \
+ -wp-prover alt-ergo,cvc4); \
fi
diff --git a/doc/release/build.tex b/doc/release/build.tex
index fc70329ed3cca10d01648f279362c723d6120d88..7d2cfc524726c384cdf7279618022a4ed25b2298 100644
--- a/doc/release/build.tex
+++ b/doc/release/build.tex
@@ -279,7 +279,7 @@ Please check that the distribution (sources and API) is OK:
\item \verb+./configure --prefix="$PWD/build"+
\item \verb+make+;
\item \verb+make install+;
- \item \verb+rm -f ~/.why3.conf; why3 config --full-config+;
+ \item \verb+rm -f ~/.why3.conf; why3 config --detect+;
\item \verb+build/bin/frama-c tests/idct/*.c -eva -wp -wp-rte+
\item If you have a GUI, replace \verb+frama-c+ above with \verb+frama-c-gui+
and click around, see if things work (e.g. no segmentation faults).
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 90d5cf66c32343299306fd0110f1b41dd815a5de..27b6beac5547cd0d203f912d37adb9724f172e37 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1740,12 +1740,12 @@ src/plugins/wp/share/coqwp/Zbits.v: CEA_WP
src/plugins/wp/share/coqwp/bool/Bool.v: UNMODIFIED_WHY3
src/plugins/wp/share/coqwp/int/Abs.v: UNMODIFIED_WHY3
src/plugins/wp/share/coqwp/int/ComputerDivision.v: UNMODIFIED_WHY3
-src/plugins/wp/share/coqwp/int/EuclideanDivision.v: UNMODIFIED_WHY3
+src/plugins/wp/share/coqwp/int/EuclideanDivision.v: MODIFIED_WHY3
src/plugins/wp/share/coqwp/int/Exponentiation.v: UNMODIFIED_WHY3
src/plugins/wp/share/coqwp/int/Int.v: UNMODIFIED_WHY3
src/plugins/wp/share/coqwp/int/MinMax.v: UNMODIFIED_WHY3
src/plugins/wp/share/coqwp/int/Power.v: UNMODIFIED_WHY3
-src/plugins/wp/share/coqwp/int/ComputerOfEuclideanDivision.v: UNMODIFIED_WHY3
+src/plugins/wp/share/coqwp/int/ComputerOfEuclideanDivision.v: MODIFIED_WHY3
src/plugins/wp/share/coqwp/map/Map.v: UNMODIFIED_WHY3
src/plugins/wp/share/coqwp/map/Const.v: UNMODIFIED_WHY3
src/plugins/wp/share/coqwp/real/Abs.v: UNMODIFIED_WHY3
diff --git a/nix/default.nix b/nix/default.nix
index 7a4cc5ffedbd16e8cc5fd638ca7131c6d5ffe7ee..39ca3878ecc176c7a8b6c8d0c9f208c737e5d74e 100644
--- a/nix/default.nix
+++ b/nix/default.nix
@@ -4,12 +4,12 @@
let mk_buildInputs = { opamPackages ? [], nixPackages ? [] } :
[ pkgs.gnugrep pkgs.gnused pkgs.autoconf pkgs.gnumake pkgs.gcc pkgs.ncurses pkgs.time pkgs.python3 pkgs.perl pkgs.file pkgs.which pkgs.dos2unix] ++ nixPackages ++ opam2nix.build {
specs = opam2nix.toSpecs ([ "ocamlfind" "zarith" "ocamlgraph" "yojson"
- { name = "coq"; constraint = "=8.11.1"; }
- { name = "why3" ; constraint = "=1.3.1"; }
- { name = "why3-coq" ; constraint = "=1.3.1"; }
- { name = "menhir"; constraint = "=20190924"; }
- { name = "dune"; constraint = "=1.11.4"; }
- { name = "camlzip"; constraint = "=1.07"; } #so that why3 is always compiled with it
+ { 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"; }
] ++ opamPackages
);
ocamlAttr = ocaml_version;
@@ -159,9 +159,7 @@ rec {
wp-qualif = mk_deriv {
name = "frama-c-wp-qualif";
- buildInputs = mk_buildInputs { opamPackages = [
- { name = "alt-ergo"; constraint = "=2.0.0"; }
- ]; };
+ buildInputs = mk_buildInputs { };
build_dir = main.build_dir;
src = main.build_dir + "/dir.tar";
sourceRoot = ".";
@@ -176,7 +174,7 @@ rec {
make create_share_link
mkdir home
HOME=$(pwd)/home
- why3 config --full-config
+ why3 config --detect
make src/plugins/wp/tests/test_config_qualif
export FRAMAC_WP_CACHE=replay
export FRAMAC_WP_CACHEDIR=${plugins.wp-cache.src}
@@ -189,9 +187,7 @@ rec {
aorai-prove = mk_deriv {
name = "frama-c-aorai-prove";
- buildInputs = mk_buildInputs { opamPackages = [
- { name = "alt-ergo"; constraint = "=2.0.0"; }
- ]; };
+ buildInputs = mk_buildInputs { };
build_dir = main.build_dir;
src = main.build_dir + "/dir.tar";
sourceRoot = ".";
@@ -207,7 +203,7 @@ rec {
make create_share_link
mkdir home
HOME=$(pwd)/home
- why3 config --full-config
+ why3 config --detect
make src/plugins/aorai/tests/ptests_config
make PTESTS_OPTS="-config prove -error-code" Aorai_TESTS
'';
diff --git a/nix/frama-ci.nix b/nix/frama-ci.nix
index 7939e05dd1161d65a13c6d4093cfff78d3f3fe81..3e705a8ac1871c85d7680324718834ba71b0fd71 100644
--- a/nix/frama-ci.nix
+++ b/nix/frama-ci.nix
@@ -5,7 +5,7 @@ let
src = builtins.fetchGit {
"url" = "https://bobot:${password}@git.frama-c.com/frama-c/Frama-CI.git";
"name" = "Frama-CI";
- "rev" = "3e8a67b19d5923c651509070eec5db646b80ec32";
+ "rev" = "01d423ae0e14b2d0d41e952d261aa859b2a3855e";
"ref" = "master";
};
in
diff --git a/opam/opam b/opam/opam
index 3ba784a791405be719eac1d105526731c8d723a4..dd9a22814ac9549d145b8d40c79de1590dc8192f 100644
--- a/opam/opam
+++ b/opam/opam
@@ -116,7 +116,7 @@ depends: [
( "alt-ergo-free" | "alt-ergo" )
"conf-graphviz" { post }
"yojson"
- "why3" { >= "1.3.1" }
+ "why3" { >= "1.3.3" }
]
depopts: [
diff --git a/reference-configuration.md b/reference-configuration.md
index 67657200acdd65fd4798d090e3865c5e88fb7d3d..ac25beb9709da653897d5dc57db41e72cb2b0aa6 100644
--- a/reference-configuration.md
+++ b/reference-configuration.md
@@ -2,14 +2,14 @@ The following set of packages is known to be a working configuration for
compiling Frama-C+dev, on a machine with gcc <= 9[^gcc-10]
- OCaml 4.08.1
-- alt-ergo.2.0.0 (for wp, optional)
+- alt-ergo.2.2.0 (for wp, optional)
- apron.v0.9.12 (for eva, optional)
- lablgtk.2.18.11 | lablgtk3.3.1.1 + lablgtk3-sourceview3.3.1.1
- mlgmpidl.1.2.12 (for eva, optional)
- ocamlfind.1.8.1
- ocamlgraph.1.8.8
- ppx_deriving_yojson.3.5.2 (for mdr, optional)
-- why3.1.3.1
+- why3.1.3.3
- yojson.1.7.0
- zarith.1.9.1
- zmq.5.1.3 (for server, optional)
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index 2771afd2721b6b1e7d17d12f21a20b0590cfc148..06edf050db3ce0ce5336420e15c4eed6971fce93 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -130,7 +130,8 @@ struct
let tree env = env.tree
- let play env res =
+ let play env prv res =
+ List.mem prv env.provers &&
if VCS.is_valid res then env.valid else env.failed
let progress env msg = env.progress (ProofEngine.main env.tree) msg
@@ -332,7 +333,7 @@ let rec crawl env on_child node = function
| Prover( prv , res ) :: alternative ->
begin
let task =
- if Env.play env res then
+ if Env.play env prv res then
let wpo = Env.goal env node in
let config = VCS.configure res in
Env.prove env wpo ~config prv
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index f6fd227bee2b163a97c03a2a83f95acd96dda4be..0b298b1af9e4e5dd69999dbf664b32752554d451 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1252,6 +1252,7 @@ let batch pconf driver ?script ~timeout ~steplimit prover task =
| Some _, Some _ -> true
| Some _, None -> false
in
+ let steps = if with_steps then steps else None in
let command = Why3.Whyconf.get_complete_command pconf ~with_steps in
let inplace = if script <> None then Some true else None in
let call = Why3.Driver.prove_task_prepared ?old:script ?inplace
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index ffa0bccf1ca04ba1ab79bb12f4e8a59868cf5bd2..3451cbacab7c6513706448e6042c195a5ef098d8 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -311,33 +311,35 @@ let cached r = if is_verdict r then { r with cached=true } else r
let kfailed ?pos msg = Pretty_utils.ksfprintf (failed ?pos) msg
-let perfo dkey = not (Wp_parameters.has_dkey dkey)
-
-let pp_perf fmt r =
+let pp_perf_forced fmt r =
begin
let t = r.solver_time in
- if t > Rformat.epsilon && perfo dkey_shell
+ if t > Rformat.epsilon
then Format.fprintf fmt " (Qed:%a)" Rformat.pp_time t ;
let t = r.prover_time in
- if t > Rformat.epsilon && perfo dkey_shell
+ if t > Rformat.epsilon
then Format.fprintf fmt " (%a)" Rformat.pp_time t ;
let s = r.prover_steps in
- if s > 0 && perfo dkey_shell
+ if s > 0
then Format.fprintf fmt " (%d)" s ;
- if r.cached && perfo dkey_shell
+ if r.cached
then Format.fprintf fmt " (cached)" ;
end
+let pp_perf_shell fmt r =
+ if not (Wp_parameters.has_dkey dkey_shell) then
+ pp_perf_forced fmt r
+
let pp_result fmt r =
match r.verdict with
| NoResult -> Format.pp_print_string fmt "No Result"
| Computing _ -> Format.pp_print_string fmt "Computing"
| Invalid -> Format.pp_print_string fmt "Invalid"
| Failed -> Format.fprintf fmt "Failed@ %s" r.prover_errmsg
- | Valid -> Format.fprintf fmt "Valid%a" pp_perf r
- | Unknown -> Format.fprintf fmt "Unknown%a" pp_perf r
- | Stepout -> Format.fprintf fmt "Step limit%a" pp_perf r
- | Timeout -> Format.fprintf fmt "Timeout%a" pp_perf r
+ | Valid -> Format.fprintf fmt "Valid%a" pp_perf_shell r
+ | Unknown -> Format.fprintf fmt "Unknown%a" pp_perf_shell r
+ | Stepout -> Format.fprintf fmt "Step limit%a" pp_perf_shell r
+ | Timeout -> Format.fprintf fmt "Timeout%a" pp_perf_shell r
let is_qualified prover result =
match prover with
@@ -350,7 +352,7 @@ let pp_cache_miss fmt st updating prover result =
&& not (is_qualified prover result)
&& Wp_parameters.has_dkey dkey_shell
then
- Format.fprintf fmt "%s%a (missing cache)" st pp_perf result
+ Format.fprintf fmt "%s%a (missing cache)" st pp_perf_forced result
else
Format.pp_print_string fmt @@
if is_valid result then "Valid" else "Unsuccess"
diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml
index 215d8912e50e7b2cbb3160540329ddd5e50e6c63..3c9a5f797a62fa1879dab6209297e3bda177d835 100644
--- a/src/plugins/wp/Why3Provers.ml
+++ b/src/plugins/wp/Why3Provers.ml
@@ -27,7 +27,9 @@
let cfg = lazy
begin
try
- Why3.Whyconf.read_config None
+ let config = Why3.Whyconf.read_config None in
+ let config = Why3.Whyconf.load_default_config_if_needed config in
+ config
with exn ->
Wp_parameters.abort "%a" Why3.Exn_printer.exn_printer exn
end
diff --git a/src/plugins/wp/configure.ac b/src/plugins/wp/configure.ac
index 0c3828b35ff2f37b6daf675d0e6670ce9639c3fc..052fd1617d8adadc08240f26a10416921815c5c1 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)
- AC_MSG_RESULT([found $WHY3VERSION: requires 1.3.1+])
+ 0.* | 1.[[012]].* | 1.3.0 | 1.3.1 | 1.3.2)
+ AC_MSG_RESULT([found $WHY3VERSION: requires 1.3.3+])
plugin_disable(wp,[non-supported why3 $WHY3VERSION])
;;
1.3.*)
AC_MSG_RESULT([found $WHY3VERSION: ok])
;;
*)
- AC_MSG_RESULT([found $WHY3VERSION: might work (should be 1.3.1+)])
+ AC_MSG_RESULT([found $WHY3VERSION: might work (should be 1.3.3+)])
;;
esac
fi
@@ -85,7 +85,7 @@ if test "$ENABLE_WP" != "no"; then
if test "$COQC" = "yes" ; then
COQVERSION=`coqc -v | sed -n -e 's|.*version* *\([[^ ]]*\) .*$|\1|p' `
case $COQVERSION in
- 8.7*|8.8*|8.9*|8.10*|8.11.*|trunk)
+ 8.7*|8.8*|8.9*|8.10*|8.11.*|8.12.*|trunk)
AC_MSG_RESULT(coqc version $COQVERSION found)
;;
*)
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index c985100d7006a38906cc7031dab443153e14b01a..24cd69441d0aa7e9539bc8bd179110417be6178a 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -759,49 +759,48 @@ let dkey_refusage = Wp_parameters.register_category "refusage"
let dkey_builtins = Wp_parameters.register_category "builtins"
let cmdline_run () =
- let wp_main fct =
- Wp_parameters.feedback ~ontty:`Feedback "Running WP plugin...";
- Ast.compute ();
- Dyncall.compute ();
- if Wp_parameters.has_dkey dkey_logicusage then
- begin
- LogicUsage.compute ();
- LogicUsage.dump ();
- end ;
- if Wp_parameters.has_dkey dkey_refusage then
- begin
- RefUsage.compute ();
- RefUsage.dump ();
- end ;
- let bhv = Wp_parameters.Behaviors.get () in
- let prop = Wp_parameters.Properties.get () in
- (** TODO entry point *)
- let computer = computer () in
- if Wp_parameters.has_dkey dkey_builtins then
- begin
- WpContext.on_context (computer#model,WpContext.Global)
- LogicBuiltins.dump ();
- end ;
- wp_compute_memory_context computer#model ;
- if Wp_parameters.CheckModelHypotheses.get () then
- wp_insert_memory_context computer#model fct ;
- Generator.compute_selection computer ~fct ~bhv ~prop ()
- in
- if Wp_parameters.CachePrint.get () then
- Kernel.feedback "Cache directory: %s" (Cache.get_dir ()) ;
- let fct = Wp_parameters.get_wp () in
- if fct <> Wp_parameters.Fct_none then
- begin
- let goals = wp_main fct in
- do_wp_proofs goals ;
+ begin
+ if Wp_parameters.CachePrint.get () then
+ Kernel.feedback "Cache directory: %s" (Cache.get_dir ()) ;
+ let fct = Wp_parameters.get_fct () in
+ if fct <> Wp_parameters.Fct_none then
begin
- if fct <> Wp_parameters.Fct_all then
- do_wp_print_for goals
- else
- do_wp_print () ;
- end ;
- do_wp_report () ;
- end
+ Wp_parameters.feedback ~ontty:`Feedback "Running WP plugin...";
+ Ast.compute ();
+ Dyncall.compute ();
+ if Wp_parameters.has_dkey dkey_logicusage then
+ begin
+ LogicUsage.compute ();
+ LogicUsage.dump ();
+ end ;
+ if Wp_parameters.has_dkey dkey_refusage then
+ begin
+ RefUsage.compute ();
+ RefUsage.dump ();
+ end ;
+ let bhv = Wp_parameters.Behaviors.get () in
+ let prop = Wp_parameters.Properties.get () in
+ (** TODO entry point *)
+ let computer = computer () in
+ if Wp_parameters.has_dkey dkey_builtins then
+ begin
+ WpContext.on_context (computer#model,WpContext.Global)
+ LogicBuiltins.dump ();
+ end ;
+ wp_compute_memory_context computer#model ;
+ if Wp_parameters.CheckModelHypotheses.get () then
+ wp_insert_memory_context computer#model fct ;
+ let goals = Generator.compute_selection computer ~fct ~bhv ~prop () in
+ do_wp_proofs goals ;
+ begin
+ if fct <> Wp_parameters.Fct_all then
+ do_wp_print_for goals
+ else
+ do_wp_print () ;
+ end ;
+ do_wp_report () ;
+ end
+ end
(* ------------------------------------------------------------------------ *)
(* --- Register external functions --- *)
diff --git a/src/plugins/wp/share/coqwp/Vlist.v b/src/plugins/wp/share/coqwp/Vlist.v
index 62ef751f99343e9fcc2d5a17bed86bc9e04e84a3..f91fabec5d1b900534a7bdd3e1abd1e6d800121d 100644
--- a/src/plugins/wp/share/coqwp/Vlist.v
+++ b/src/plugins/wp/share/coqwp/Vlist.v
@@ -40,6 +40,7 @@ Hint Rewrite List.app_assoc List.app_nil_l List.app_nil_r : list.
(* --- Classical Lists for Alt-Ergo --- *)
(* -------------------------------------------------------------------- *)
Require Import Qedlib.
+Require Import Lia.
(* Why3 goal *)
Definition list : forall (a:Type), Type.
@@ -399,11 +400,7 @@ intros p q w h1 h2. unfold vlist_eq ; simpl ; split ; auto with zarith.
rewrite length_repeat ; auto with zarith.
replace (i - p * length A) with (i + (-p) * length A).
rewrite Z.rem_add ; auto with zarith.
- apply Z.mul_nonneg_nonneg ; auto with zarith.
- replace (i + -p * length A) with (i - p * length A) ; auto with zarith.
- rewrite Z.mul_opp_l. rewrite Z.add_opp_r. auto.
- rewrite Z.mul_opp_l. rewrite Z.add_opp_r. auto.
- rewrite length_repeat ; auto with zarith.
+ lia. rewrite length_repeat. lia. auto.
Qed.
(* Why3 goal *)
diff --git a/src/plugins/wp/share/coqwp/int/ComputerOfEuclideanDivision.v b/src/plugins/wp/share/coqwp/int/ComputerOfEuclideanDivision.v
index f9fb43d91946cef92d571b22367ff35e53403425..3e41143a85f6329bdc2df183170cfab02e4de89c 100644
--- a/src/plugins/wp/share/coqwp/int/ComputerOfEuclideanDivision.v
+++ b/src/plugins/wp/share/coqwp/int/ComputerOfEuclideanDivision.v
@@ -7,6 +7,9 @@
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
+(* File modified by CEA (Commissariat à l'énergie atomique et aux *)
+(* énergies alternatives). *)
+(* *)
(**************************************************************************)
(* This file is generated by Why3's Coq-realize driver *)
@@ -29,19 +32,19 @@ case (Z_le_dec 0 (n mod (Zpos d))); intros H2.
* destruct (H2 H0).
Qed.
-
(* Why3 goal *)
-Lemma cdiv_cases : forall (n:Z) (d:Z), ((0%Z <= n)%Z -> ((0%Z < d)%Z ->
- ((ZArith.BinInt.Z.quot n d) = (int.EuclideanDivision.div n d)))) /\
- (((n <= 0%Z)%Z -> ((0%Z < d)%Z ->
- ((ZArith.BinInt.Z.quot n d) = (-(int.EuclideanDivision.div (-n)%Z
- d))%Z))) /\ (((0%Z <= n)%Z -> ((d < 0%Z)%Z ->
- ((ZArith.BinInt.Z.quot n d) = (-(int.EuclideanDivision.div n
- (-d)%Z))%Z))) /\ ((n <= 0%Z)%Z -> ((d < 0%Z)%Z ->
- ((ZArith.BinInt.Z.quot n d) = (int.EuclideanDivision.div (-n)%Z
- (-d)%Z)))))).
+Lemma cdiv_cases :
+ forall (n:Numbers.BinNums.Z) (d:Numbers.BinNums.Z),
+ ((0%Z <= n)%Z -> (0%Z < d)%Z ->
+ ((ZArith.BinInt.Z.quot n d) = (int.EuclideanDivision.div n d))) /\
+ ((n <= 0%Z)%Z -> (0%Z < d)%Z ->
+ ((ZArith.BinInt.Z.quot n d) = (-(int.EuclideanDivision.div (-n)%Z d))%Z)) /\
+ ((0%Z <= n)%Z -> (d < 0%Z)%Z ->
+ ((ZArith.BinInt.Z.quot n d) = (-(int.EuclideanDivision.div n (-d)%Z))%Z)) /\
+ ((n <= 0%Z)%Z -> (d < 0%Z)%Z ->
+ ((ZArith.BinInt.Z.quot n d) = (int.EuclideanDivision.div (-n)%Z (-d)%Z))).
intros n d.
- destruct d as [|d|d]; destruct n as [|n|n]; intuition (try contradiction; try discriminate; auto).
+ destruct d as [|d|d]; destruct n as [|n|n]; intuition (try discriminate; try contradiction).
+ assert (NZ_d:((Zpos d) <> 0)%Z) by discriminate.
rewrite (Z.quot_div (Z.pos n) (Z.pos d) NZ_d).
rewrite on_pos_euclidean_is_div.
@@ -64,15 +67,17 @@ Lemma cdiv_cases : forall (n:Z) (d:Z), ((0%Z <= n)%Z -> ((0%Z < d)%Z ->
Qed.
(* Why3 goal *)
-Lemma cmod_cases : forall (n:Z) (d:Z), ((0%Z <= n)%Z -> ((0%Z < d)%Z ->
- ((ZArith.BinInt.Z.rem n d) = (int.EuclideanDivision.mod1 n d)))) /\
- (((n <= 0%Z)%Z -> ((0%Z < d)%Z ->
- ((ZArith.BinInt.Z.rem n d) = (-(int.EuclideanDivision.mod1 (-n)%Z
- d))%Z))) /\ (((0%Z <= n)%Z -> ((d < 0%Z)%Z ->
- ((ZArith.BinInt.Z.rem n d) = (int.EuclideanDivision.mod1 n (-d)%Z)))) /\
- ((n <= 0%Z)%Z -> ((d < 0%Z)%Z ->
- ((ZArith.BinInt.Z.rem n d) = (-(int.EuclideanDivision.mod1 (-n)%Z
- (-d)%Z))%Z))))).
+Lemma cmod_cases :
+ forall (n:Numbers.BinNums.Z) (d:Numbers.BinNums.Z),
+ ((0%Z <= n)%Z -> (0%Z < d)%Z ->
+ ((ZArith.BinInt.Z.rem n d) = (int.EuclideanDivision.mod1 n d))) /\
+ ((n <= 0%Z)%Z -> (0%Z < d)%Z ->
+ ((ZArith.BinInt.Z.rem n d) = (-(int.EuclideanDivision.mod1 (-n)%Z d))%Z)) /\
+ ((0%Z <= n)%Z -> (d < 0%Z)%Z ->
+ ((ZArith.BinInt.Z.rem n d) = (int.EuclideanDivision.mod1 n (-d)%Z))) /\
+ ((n <= 0%Z)%Z -> (d < 0%Z)%Z ->
+ ((ZArith.BinInt.Z.rem n d) =
+ (-(int.EuclideanDivision.mod1 (-n)%Z (-d)%Z))%Z)).
intros n d.
unfold int.EuclideanDivision.mod1.
assert (Z.rem n d = n - (d * (Z.quot n d)))%Z.
@@ -80,7 +85,7 @@ Lemma cmod_cases : forall (n:Z) (d:Z), ((0%Z <= n)%Z -> ((0%Z < d)%Z ->
omega.
rewrite H.
assert (H2:=cdiv_cases n d).
- intuition.
+ intuition idtac.
+ rewrite H1.
reflexivity.
+ rewrite H4.
diff --git a/src/plugins/wp/share/coqwp/int/EuclideanDivision.v b/src/plugins/wp/share/coqwp/int/EuclideanDivision.v
index 45c05b8a8ab2b956d3e5c830c180da0be552ef1e..2954f05261ad48c202a2d35d500cf330b82f2c6c 100644
--- a/src/plugins/wp/share/coqwp/int/EuclideanDivision.v
+++ b/src/plugins/wp/share/coqwp/int/EuclideanDivision.v
@@ -7,6 +7,9 @@
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
+(* File modified by CEA (Commissariat à l'énergie atomique et aux *)
+(* énergies alternatives). *)
+(* *)
(**************************************************************************)
(* This file is generated by Why3's Coq-realize driver *)
@@ -17,7 +20,7 @@ Require int.Int.
Require int.Abs.
(* Why3 goal *)
-Definition div : Z -> Z -> Z.
+Definition div : Numbers.BinNums.Z -> Numbers.BinNums.Z -> Numbers.BinNums.Z.
intros x y.
case (Z_le_dec 0 (Zmod x y)) ; intros H.
exact (Z.div x y).
@@ -25,14 +28,16 @@ exact (Z.div x y + 1)%Z.
Defined.
(* Why3 goal *)
-Definition mod1 : Z -> Z -> Z.
+Definition mod1 :
+ Numbers.BinNums.Z -> Numbers.BinNums.Z -> Numbers.BinNums.Z.
intros x y.
exact (x - y * div x y)%Z.
Defined.
(* Why3 goal *)
Lemma Div_mod :
- forall (x:Z) (y:Z), ~ (y = 0%Z) -> (x = ((y * (div x y))%Z + (mod1 x y))%Z).
+ forall (x:Numbers.BinNums.Z) (y:Numbers.BinNums.Z), ~ (y = 0%Z) ->
+ (x = ((y * (div x y))%Z + (mod1 x y))%Z).
intros x y Zy.
unfold mod1, div.
case Z_le_dec ; intros H ; ring.
@@ -40,10 +45,10 @@ Qed.
(* Why3 goal *)
Lemma Mod_bound :
- forall (x:Z) (y:Z), ~ (y = 0%Z) ->
+ forall (x:Numbers.BinNums.Z) (y:Numbers.BinNums.Z), ~ (y = 0%Z) ->
(0%Z <= (mod1 x y))%Z /\ ((mod1 x y) < (ZArith.BinInt.Z.abs y))%Z.
intros x y Zy.
-zify.
+assert (H := Zabs_spec y).
assert (H1 := Z_mod_neg x y).
assert (H2 := Z_mod_lt x y).
unfold mod1, div.
@@ -57,8 +62,9 @@ Qed.
(* Why3 goal *)
Lemma Div_unique :
- forall (x:Z) (y:Z) (q:Z), (0%Z < y)%Z ->
- (((q * y)%Z <= x)%Z /\ (x < ((q * y)%Z + y)%Z)%Z) -> ((div x y) = q).
+ forall (x:Numbers.BinNums.Z) (y:Numbers.BinNums.Z) (q:Numbers.BinNums.Z),
+ (0%Z < y)%Z -> ((q * y)%Z <= x)%Z /\ (x < ((q * y)%Z + y)%Z)%Z ->
+ ((div x y) = q).
intros x y q h1 (h2,h3).
assert (h:(~(y=0))%Z) by omega.
generalize (Mod_bound x y h); intro h0.
@@ -80,8 +86,8 @@ Qed.
(* Why3 goal *)
Lemma Div_bound :
- forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
- (0%Z <= (div x y))%Z /\ ((div x y) <= x)%Z.
+ forall (x:Numbers.BinNums.Z) (y:Numbers.BinNums.Z),
+ (0%Z <= x)%Z /\ (0%Z < y)%Z -> (0%Z <= (div x y))%Z /\ ((div x y) <= x)%Z.
intros x y (Hx,Hy).
unfold div.
case Z_le_dec ; intros H.
@@ -100,7 +106,7 @@ now apply Z.lt_gt.
Qed.
(* Why3 goal *)
-Lemma Mod_1 : forall (x:Z), ((mod1 x 1%Z) = 0%Z).
+Lemma Mod_1 : forall (x:Numbers.BinNums.Z), ((mod1 x 1%Z) = 0%Z).
intros x.
unfold mod1, div.
rewrite Zmod_1_r, Zdiv_1_r, Zmult_1_l.
@@ -108,7 +114,7 @@ apply Zminus_diag.
Qed.
(* Why3 goal *)
-Lemma Div_1 : forall (x:Z), ((div x 1%Z) = x).
+Lemma Div_1 : forall (x:Numbers.BinNums.Z), ((div x 1%Z) = x).
intros x.
unfold div.
now rewrite Zmod_1_r, Zdiv_1_r.
@@ -116,7 +122,8 @@ Qed.
(* Why3 goal *)
Lemma Div_inf :
- forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> ((div x y) = 0%Z).
+ forall (x:Numbers.BinNums.Z) (y:Numbers.BinNums.Z),
+ (0%Z <= x)%Z /\ (x < y)%Z -> ((div x y) = 0%Z).
intros x y Hxy.
unfold div.
case Z_le_dec ; intros H.
@@ -127,8 +134,8 @@ Qed.
(* Why3 goal *)
Lemma Div_inf_neg :
- forall (x:Z) (y:Z), ((0%Z < x)%Z /\ (x <= y)%Z) ->
- ((div (-x)%Z y) = (-1%Z)%Z).
+ forall (x:Numbers.BinNums.Z) (y:Numbers.BinNums.Z),
+ (0%Z < x)%Z /\ (x <= y)%Z -> ((div (-x)%Z y) = (-1%Z)%Z).
intros x y Hxy.
assert (h: (x < y \/ x = y)%Z) by omega.
destruct h.
@@ -159,7 +166,8 @@ rewrite Z_div_same_full; auto with zarith.
Qed.
(* Why3 goal *)
-Lemma Mod_0 : forall (y:Z), ~ (y = 0%Z) -> ((mod1 0%Z y) = 0%Z).
+Lemma Mod_0 :
+ forall (y:Numbers.BinNums.Z), ~ (y = 0%Z) -> ((mod1 0%Z y) = 0%Z).
intros y Hy.
unfold mod1, div.
rewrite Zmod_0_l.
@@ -168,14 +176,15 @@ now rewrite Zdiv_0_l, Zmult_0_r.
Qed.
(* Why3 goal *)
-Lemma Div_1_left : forall (y:Z), (1%Z < y)%Z -> ((div 1%Z y) = 0%Z).
+Lemma Div_1_left :
+ forall (y:Numbers.BinNums.Z), (1%Z < y)%Z -> ((div 1%Z y) = 0%Z).
intros y Hy.
rewrite Div_inf; auto with zarith.
Qed.
(* Why3 goal *)
Lemma Div_minus1_left :
- forall (y:Z), (1%Z < y)%Z -> ((div (-1%Z)%Z y) = (-1%Z)%Z).
+ forall (y:Numbers.BinNums.Z), (1%Z < y)%Z -> ((div (-1%Z)%Z y) = (-1%Z)%Z).
intros y Hy.
unfold div.
assert (h1: (1 mod y = 1)%Z).
@@ -189,7 +198,8 @@ rewrite Zdiv_small; auto with zarith.
Qed.
(* Why3 goal *)
-Lemma Mod_1_left : forall (y:Z), (1%Z < y)%Z -> ((mod1 1%Z y) = 1%Z).
+Lemma Mod_1_left :
+ forall (y:Numbers.BinNums.Z), (1%Z < y)%Z -> ((mod1 1%Z y) = 1%Z).
intros y Hy.
unfold mod1.
rewrite Div_1_left; auto with zarith.
@@ -197,7 +207,8 @@ Qed.
(* Why3 goal *)
Lemma Mod_minus1_left :
- forall (y:Z), (1%Z < y)%Z -> ((mod1 (-1%Z)%Z y) = (y - 1%Z)%Z).
+ forall (y:Numbers.BinNums.Z), (1%Z < y)%Z ->
+ ((mod1 (-1%Z)%Z y) = (y - 1%Z)%Z).
intros y Hy.
unfold mod1.
rewrite Div_minus1_left; auto with zarith.
@@ -207,8 +218,8 @@ Open Scope Z_scope.
(* Why3 goal *)
Lemma Div_mult :
- forall (x:Z) (y:Z) (z:Z), (0%Z < x)%Z ->
- ((div ((x * y)%Z + z)%Z x) = (y + (div z x))%Z).
+ forall (x:Numbers.BinNums.Z) (y:Numbers.BinNums.Z) (z:Numbers.BinNums.Z),
+ (0%Z < x)%Z -> ((div ((x * y)%Z + z)%Z x) = (y + (div z x))%Z).
intros x y z h.
unfold div.
destruct (Z_le_dec 0 (z mod x)).
@@ -221,8 +232,8 @@ Qed.
(* Why3 goal *)
Lemma Mod_mult :
- forall (x:Z) (y:Z) (z:Z), (0%Z < x)%Z ->
- ((mod1 ((x * y)%Z + z)%Z x) = (mod1 z x)).
+ forall (x:Numbers.BinNums.Z) (y:Numbers.BinNums.Z) (z:Numbers.BinNums.Z),
+ (0%Z < x)%Z -> ((mod1 ((x * y)%Z + z)%Z x) = (mod1 z x)).
intros x y z h.
unfold mod1.
rewrite Div_mult.
diff --git a/src/plugins/wp/tests/wp_acsl/assigned_initialized_memvar.i b/src/plugins/wp/tests/wp_acsl/assigned_initialized_memvar.i
index 6ce93865705c61be2b35da0848b416e4ebe90a72..c320c1273b969100934bdd4de54c5557ce74fe3c 100644
--- a/src/plugins/wp/tests/wp_acsl/assigned_initialized_memvar.i
+++ b/src/plugins/wp/tests/wp_acsl/assigned_initialized_memvar.i
@@ -2,7 +2,7 @@
OPT: -wp-prop=CHECK
*/
/* run.config_qualif
- OPT: -wp-prop=CHECK
+ OPT: -wp-prop=CHECK -wp-timeout 20
*/
struct S {
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle
index 73c1299e84eef5626085f89187fbc140eae7a64b..bdd6cac2653343ae848ca9b820fc69dc15e8fdd7 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle
@@ -1,4 +1,4 @@
-# frama-c -wp [...]
+# frama-c -wp -wp-timeout 20 [...]
[kernel] Parsing tests/wp_acsl/assigned_initialized_memvar.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_gallery/binary-multiplication-without-overflow.c b/src/plugins/wp/tests/wp_gallery/binary-multiplication-without-overflow.c
index 5569384103c9eb72d8ab274b7de5658d45a279e0..9755d37151c09274a1e9cc21715cccb903967d5e 100644
--- a/src/plugins/wp/tests/wp_gallery/binary-multiplication-without-overflow.c
+++ b/src/plugins/wp/tests/wp_gallery/binary-multiplication-without-overflow.c
@@ -3,16 +3,15 @@
*/
/* run.config_qualif
- OPT: -warn-unsigned-overflow -wp-rte
+ OPT: -warn-unsigned-overflow -wp-rte -wp-timeout 20
*/
typedef unsigned uint32_t ;
typedef unsigned long long uint64_t ;
/*@ axiomatic mult {
-
- @ lemma sizeof_ok: ok: sizeof(uint64_t) == 2 * sizeof(uint32_t);
- @ lemma ax1: lack: \forall integer x, y; 0<x && 0<y ==> 0 <= 2*x*(y/2) <= x*y;
+ @ lemma size: sizeof(uint64_t) == 2 * sizeof(uint32_t);
+ @ lemma half: \forall integer x, y; 0<x && 0<y ==> 0 <= 2*x*(y/2) <= x*y;
@ }
@ */
@@ -24,7 +23,8 @@ uint64_t BinaryMultiplication (uint32_t a, uint32_t b) {
if (b != 0) {
/*@ loop assigns ok: r, x, b;
@ loop invariant inv1: ok: r+x*b == \at(a*b, LoopEntry);
- @ loop invariant inv2: ok: deductible: 2*x*(b/2) <= 18446744073709551615; // deductible from inv1, ax1, a1 and x>=0, b>0, r>=0
+ @ loop invariant inv2: ok: deductible: 2*x*(b/2) <= 18446744073709551615;
+ // deductible from inv1, half and x>=0, b>0, r>=0
@ loop variant ok: b ;
@*/
while (1) {
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication-without-overflow.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication-without-overflow.res.oracle
index 4a3a4384db14cfb12387b0265f04c6a284b3954f..d48fc137832a2d7e441b479b86b96e968db3b572 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication-without-overflow.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication-without-overflow.res.oracle
@@ -2,8 +2,8 @@
[kernel] Parsing tests/wp_gallery/binary-multiplication-without-overflow.c (with preprocessing)
[wp] Running WP plugin...
[rte] annotating function BinaryMultiplication
-[wp] Goal typed_lemma_ax1_lack : not tried
-[wp] Goal typed_lemma_sizeof_ok_ok : trivial
+[wp] Goal typed_lemma_half : not tried
+[wp] Goal typed_lemma_size : trivial
[wp] Goal typed_BinaryMultiplication_ensures_product : not tried
[wp] Goal typed_BinaryMultiplication_assert_a1_ok_deductible : not tried
[wp] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_preserved : not tried
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle
index 41402c7b8c2aef45ecafd2238c6896a462d04be1..2bf3e0ea994f79997ec9562c77d3408aac591fd3 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle
@@ -1,10 +1,10 @@
-# frama-c -wp -wp-rte -warn-unsigned-overflow [...]
+# frama-c -wp -wp-rte -wp-timeout 20 -warn-unsigned-overflow [...]
[kernel] Parsing tests/wp_gallery/binary-multiplication-without-overflow.c (with preprocessing)
[wp] Running WP plugin...
[rte] annotating function BinaryMultiplication
[wp] 16 goals scheduled
-[wp] [Alt-Ergo] Goal typed_lemma_ax1_lack : Unsuccess
-[wp] [Qed] Goal typed_lemma_sizeof_ok_ok : Valid
+[wp] [Alt-Ergo] Goal typed_lemma_half : Valid
+[wp] [Qed] Goal typed_lemma_size : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_ensures_product : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_assert_a1_ok_deductible : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_preserved : Valid
@@ -19,12 +19,12 @@
[wp] [Qed] Goal typed_BinaryMultiplication_loop_assigns : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_variant_decrease : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_variant_positive : Valid
-[wp] Proved goals: 15 / 16
+[wp] Proved goals: 16 / 16
Qed: 3
- Alt-Ergo: 12 (unsuccess: 1)
+ Alt-Ergo: 13
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
- Axiomatic mult 1 - 2 50.0%
+ Axiomatic mult 1 1 2 100%
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
BinaryMultiplication 2 12 14 100%
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/script/BinaryMultiplication_loop_invariant_inv1_ok_preserved.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/script/BinaryMultiplication_loop_invariant_inv1_ok_preserved.json
index a44e4f7a5cfe5c2654916e6178f295550553a9d3..da7a4fc7b539ebcca9a6c78e2904ca53e633e649 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/script/BinaryMultiplication_loop_invariant_inv1_ok_preserved.json
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/script/BinaryMultiplication_loop_invariant_inv1_ok_preserved.json
@@ -2,15 +2,50 @@
"params": { "inf": 0, "sup": 1 },
"select": { "select": "inside-step", "at": 17, "kind": "have",
"occur": 0, "target": "b_3 mod 2", "pattern": "%$b2" },
- "children": { "Lower 0": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0637,
- "steps": 96 } ],
- "Value 0": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0813,
- "steps": 120 } ],
- "Value 1": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.3008,
- "steps": 284 } ],
- "Upper 1": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0965,
- "steps": 99 } ] } } ]
+ "children": { "Lower 0": [ { "header": "Overflow",
+ "tactic": "Wp.overflow", "params": {},
+ "select": { "select": "inside-goal",
+ "occur": 0,
+ "target": "(to_uint64 (2*x_1))",
+ "pattern": "to_uint64.2$x" },
+ "children": { "In-Range": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid",
+ "time": 4.6879,
+ "steps": 46 } ],
+ "No-Overflow": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid",
+ "time": 4.8895,
+ "steps": 47 } ] } } ],
+ "Value 0": [ { "header": "Overflow",
+ "tactic": "Wp.overflow", "params": {},
+ "select": { "select": "inside-step",
+ "at": 3, "kind": "have",
+ "occur": 0,
+ "target": "(to_uint64 (a_1*b_1))",
+ "pattern": "to_uint64*$a$b" },
+ "children": { "In-Range": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid",
+ "time": 4.7487,
+ "steps": 40 } ],
+ "No-Overflow": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid",
+ "time": 4.7716,
+ "steps": 183 } ] } } ],
+ "Value 1": [ { "header": "Overflow",
+ "tactic": "Wp.overflow", "params": {},
+ "select": { "select": "inside-step",
+ "at": 3, "kind": "have",
+ "occur": 0,
+ "target": "(to_uint64 (a_1*b_1))",
+ "pattern": "to_uint64*$a$b" },
+ "children": { "In-Range": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid",
+ "time": 4.7262,
+ "steps": 44 } ],
+ "No-Overflow": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid",
+ "time": 4.7611,
+ "steps": 221 } ] } } ],
+ "Upper 1": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 6.2835,
+ "steps": 48 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/loop-statement.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/loop-statement.res.oracle
index 8f26f5372756daf4fdba29baeba2f1f8ad2d43eb..a86dae9951bdf6be94cf4c1213e92c65b93591a9 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/loop-statement.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/loop-statement.res.oracle
@@ -3,7 +3,7 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 15 goals scheduled
-[wp] [Alt-Ergo] Goal typed_lemma_Lb : Valid
+[wp] [Alt-Ergo] Goal typed_lemma_Lb : Unsuccess
[wp] [Qed] Goal typed_loop_statement_requires_Scond : Valid
[wp] [Qed] Goal typed_loop_statement_ensures_Sbody : Valid
[wp] [Qed] Goal typed_loop_statement_assigns : Valid
@@ -18,12 +18,12 @@
[wp] [Qed] Goal typed_loop_statement_assigns_2_exit_part2 : Valid
[wp] [Qed] Goal typed_loop_statement_assigns_2_normal_part1 : Valid
[wp] [Qed] Goal typed_loop_statement_assigns_2_normal_part2 : Valid
-[wp] Proved goals: 15 / 15
+[wp] Proved goals: 14 / 15
Qed: 11
- Alt-Ergo: 4
+ Alt-Ergo: 3 (unsuccess: 1)
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
- Axiomatic Ploop - 1 1 100%
+ Axiomatic Ploop - - 1 0.0%
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
loop_statement 11 3 14 100%
diff --git a/src/plugins/wp/tests/wp_plugin/no_step_limit.i b/src/plugins/wp/tests/wp_plugin/no_step_limit.i
index 2d5745aa584f56360e7e8ae129266313c25b514c..d1ad1d007aab8783123f81c1e3e37e9480154377 100644
--- a/src/plugins/wp/tests/wp_plugin/no_step_limit.i
+++ b/src/plugins/wp/tests/wp_plugin/no_step_limit.i
@@ -3,8 +3,9 @@
*/
/* run.config_qualif
CMD: WHY3CONFIG=@PTEST_DIR@/@PTEST_NAME@.conf @frama-c@
- OPT: -wp -wp-prover no-steps -wp-steps 10 -wp-msg-key shell
+ OPT: -wp -wp-prover no-steps -wp-steps 10 -wp-timeout 1 -wp-cache none -wp-no-cache-env -wp-msg-key shell
*/
+// cache is locally deactivated to see the option
/*@
lemma truc: \false ;
*/
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/trig.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/trig.res.oracle
index 6cad2d7458db74974f8f50369941a9117d488574..1f0699f38c6b96e6a614985d4f552db71e4c3982 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/trig.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/trig.res.oracle
@@ -6,63 +6,61 @@
Function foo
------------------------------------------------------------
-Goal Assertion 'qed_ok,S' (file tests/wp_plugin/trig.i, line 42):
-Let x = c.F1_MSG_size.
-Let a_1 = c.F1_MSG_text.
+Goal Assertion 'ok,S' (file tests/wp_plugin/trig.i, line 35):
+Let a_1 = L_concat(a, b).
+Let x = a_1.F1_MSG_size.
+Let a_2 = a_1.F1_MSG_text.
Assume {
- Type: IsS1_MSG(a) /\ IsS1_MSG(b) /\ IsS1_MSG(c) /\ is_sint32(x) /\
- is_uint8((a.F1_MSG_text)[2]) /\ is_uint8((b.F1_MSG_text)[2]) /\
- is_uint8(a_1[2]) /\ is_uint8(a_1[7]).
+ Type: IsS1_MSG(a) /\ IsS1_MSG(b) /\ is_uint8((a.F1_MSG_text)[2]) /\
+ is_uint8((b.F1_MSG_text)[2]) /\ IsS1_MSG(a_1) /\ is_sint32(x) /\
+ is_uint8(a_2[2]) /\ is_uint8(a_2[7]).
(* Pre-condition *)
Have: ((a.F1_MSG_size) = 5) /\ ((b.F1_MSG_size) = 5).
- (* Call 'fconcat' *)
- Have: EqS1_MSG(c, L_concat(a, b)).
}
Prove: x = 10.
------------------------------------------------------------
-Goal Assertion 'qed_ok,A' (file tests/wp_plugin/trig.i, line 43):
-Let a_1 = (a.F1_MSG_text)[2].
-Let a_2 = c.F1_MSG_text.
-Let a_3 = a_2[2].
+Goal Assertion 'ok,A' (file tests/wp_plugin/trig.i, line 36):
+Let a_1 = L_concat(a, b).
+Let a_2 = (a.F1_MSG_text)[2].
+Let a_3 = a_1.F1_MSG_text.
+Let a_4 = a_3[2].
Assume {
- Type: IsS1_MSG(a) /\ IsS1_MSG(b) /\ IsS1_MSG(c) /\ is_uint8(a_1) /\
- is_uint8((b.F1_MSG_text)[2]) /\ is_uint8(a_3) /\ is_uint8(a_2[7]).
+ Type: IsS1_MSG(a) /\ IsS1_MSG(b) /\ is_uint8(a_2) /\
+ is_uint8((b.F1_MSG_text)[2]) /\ IsS1_MSG(a_1) /\ is_uint8(a_4) /\
+ is_uint8(a_3[7]).
(* Pre-condition *)
Have: ((a.F1_MSG_size) = 5) /\ ((b.F1_MSG_size) = 5).
- (* Call 'fconcat' *)
- Have: EqS1_MSG(c, L_concat(a, b)).
- (* Assertion 'qed_ok,S' *)
- Have: (c.F1_MSG_size) = 10.
+ (* Assertion 'ok,S' *)
+ Have: (a_1.F1_MSG_size) = 10.
}
-Prove: a_3 = a_1.
+Prove: a_4 = a_2.
------------------------------------------------------------
-Goal Assertion 'qed_ok,B' (file tests/wp_plugin/trig.i, line 44):
-Let a_1 = c.F1_MSG_text.
-Let a_2 = a_1[2].
-Let a_3 = (a.F1_MSG_text)[2].
-Let a_4 = (b.F1_MSG_text)[2].
-Let a_5 = a_1[7].
+Goal Assertion 'ok,B' (file tests/wp_plugin/trig.i, line 37):
+Let a_1 = L_concat(a, b).
+Let a_2 = a_1.F1_MSG_text.
+Let a_3 = a_2[2].
+Let a_4 = (a.F1_MSG_text)[2].
+Let a_5 = (b.F1_MSG_text)[2].
+Let a_6 = a_2[7].
Assume {
- Type: IsS1_MSG(a) /\ IsS1_MSG(b) /\ IsS1_MSG(c) /\ is_uint8(a_3) /\
- is_uint8(a_4) /\ is_uint8(a_2) /\ is_uint8(a_5).
+ Type: IsS1_MSG(a) /\ IsS1_MSG(b) /\ is_uint8(a_4) /\ is_uint8(a_5) /\
+ IsS1_MSG(a_1) /\ is_uint8(a_3) /\ is_uint8(a_6).
(* Pre-condition *)
Have: ((a.F1_MSG_size) = 5) /\ ((b.F1_MSG_size) = 5).
- (* Call 'fconcat' *)
- Have: EqS1_MSG(c, L_concat(a, b)).
- (* Assertion 'qed_ok,S' *)
- Have: (c.F1_MSG_size) = 10.
- (* Assertion 'qed_ok,A' *)
- Have: a_2 = a_3.
+ (* Assertion 'ok,S' *)
+ Have: (a_1.F1_MSG_size) = 10.
+ (* Assertion 'ok,A' *)
+ Have: a_3 = a_4.
}
-Prove: a_5 = a_4.
+Prove: a_6 = a_5.
------------------------------------------------------------
-Goal Instance of 'Pre-condition 'qed_ok' in 'fconcat'' in 'foo' at initialization of 'c' (file tests/wp_plugin/trig.i, line 41)
+Goal Instance of 'Pre-condition 'qed_ok' in 'fconcat'' in 'foo' at initialization of 'c' (file tests/wp_plugin/trig.i, line 34)
:
Prove: true.
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 c262dc3d274019adb6a1a56a0d2125fef38d489d..bb756593da2a38fa0f139b26a820aac8f23aa66f 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
@@ -1,7 +1,7 @@
----------------------------------------------------------
WP Requirements for Qualif Tests (3)
----------------------------------------------------------
-1. The Alt-Ergo theorem prover, version 2.0.0
-2. The Why3 platform, version 1.3.1
-3. The Coq Proof Assistant, version 8.11.1
+1. The Alt-Ergo theorem prover, version 2.2.0
+2. The Why3 platform, version 1.3.3
+3. The Coq Proof Assistant, version 8.12.0
----------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
index c78a7cf65a38f32339cb534a45aaced02ad60dcf..4028fd0e199f2b378fe54f72025b011ae11391a8 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
@@ -2,7 +2,7 @@
[kernel] Parsing tests/wp_plugin/fallback.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] Warning: Prover 'Alt-Ergo:1.2.0' not found, fallback to 'Alt-Ergo:2.0.0'
+[wp] Warning: Prover 'Alt-Ergo:1.2.0' not found, fallback to 'Alt-Ergo:2.2.0'
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_job_ensures : Valid
[wp] Proved goals: 1 / 1
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/no_step_limit.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/no_step_limit.res.oracle
index ce12f14d75e508eb5d7d3aaf23c54f7322e71554..4feaeefdadad2ae6b7ed8f9b8380c50edb7f23d7 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/no_step_limit.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/no_step_limit.res.oracle
@@ -1,4 +1,4 @@
-# frama-c -wp -wp-steps 10 [...]
+# frama-c -wp -wp-timeout 1 -wp-steps 10 [...]
[kernel] Parsing tests/wp_plugin/no_step_limit.i (no preprocessing)
[wp] Running WP plugin...
[wp] 1 goal scheduled
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.res.oracle
index 1647eed4e12f9eec5d91b1c473c1899f1700a55d..57c1c46213f63ee45bec279856df93aee1788a85 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.res.oracle
@@ -4,12 +4,12 @@
[wp] 4 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_access_16_16_ok : Valid
[wp] [Alt-Ergo] Goal typed_lemma_access_4_4_ok : Valid
-[wp] [Alt-Ergo] Goal typed_lemma_access_repeat_concat_3_ok_lack : Valid
+[wp] [Alt-Ergo] Goal typed_lemma_access_repeat_concat_3_ok_lack : Unsuccess
[wp] [Qed] Goal typed_lemma_eq_repeat_concat_3_ok : Valid
-[wp] Proved goals: 4 / 4
+[wp] Proved goals: 3 / 4
Qed: 1
- Alt-Ergo: 3
+ Alt-Ergo: 2 (unsuccess: 1)
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
- Axiomatic Nth 1 3 4 100%
+ Axiomatic Nth 1 2 4 75.0%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle
index 59455952143a4d400e7a94030a7fa6c446b544ff..a58fda9c10a8b8af8c1d5221276ae445259ef2e6 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle
@@ -3,9 +3,9 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
-[wp] [Alt-Ergo] Goal typed_foo_assert_qed_ok_S : Valid
-[wp] [Alt-Ergo] Goal typed_foo_assert_qed_ok_A : Valid
-[wp] [Alt-Ergo] Goal typed_foo_assert_qed_ok_B : Unsuccess
+[wp] [Alt-Ergo] Goal typed_foo_assert_ok_S : Valid
+[wp] [Alt-Ergo] Goal typed_foo_assert_ok_A : Valid
+[wp] [Alt-Ergo] Goal typed_foo_assert_ok_B : Unsuccess
[wp] [Qed] Goal typed_foo_call_fconcat_requires_qed_ok : Valid
[wp] Proved goals: 3 / 4
Qed: 1
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/script/lemma_U32.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/script/lemma_U32.json
index b5bf8ebae8688cf7e111e29ea2f31fc33a4a91ea..77438629a177d10c967e936ebf34b1db7e8cbf09 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/script/lemma_U32.json
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.0.session/script/lemma_U32.json
@@ -8,10 +8,10 @@
"select": { "select": "clause-goal",
"target": "(0<=x_0) /\\ (0<=(land 4294967295 x_0)) /\\ (x_0<=4294967295)",
"pattern": "&<=<=<=0$x0land$x42949672954294967295" },
- "children": { "Goal 1/3": [ { "prover": "Alt-Ergo:2.0.0",
+ "children": { "Goal 1/3": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid",
- "time": 0.0101,
- "steps": 10 } ],
+ "time": 0.0095,
+ "steps": 14 } ],
"Goal 2/3": [ { "header": "Bit Range",
"tactic": "Wp.bitrange",
"params":
@@ -25,8 +25,8 @@
{ "bit-range":
[ { "prover": "qed",
"verdict": "valid" } ] } } ],
- "Goal 3/3": [ { "prover": "Alt-Ergo:2.0.0",
+ "Goal 3/3": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid",
- "time": 0.0095,
- "steps": 10 } ] } } ],
+ "time": 0.01,
+ "steps": 14 } ] } } ],
"bitwise": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle
index 4dc2d8b6cabcc2b77ac16615387e15dadd33c4a1..4e4af2c1d3de53e290bb2a962a64749a16586809 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle
@@ -2,11 +2,9 @@
[kernel] Parsing tests/wp_plugin/unsigned.i (no preprocessing)
[wp] Running WP plugin...
[wp] 1 goal scheduled
-[wp] [Script] Goal typed_lemma_U32 : Valid
-[wp] Proved goals: 1 / 1
- Qed: 0
- Script: 1
+[wp] [Script] Goal typed_lemma_U32 : Unsuccess
+[wp] Proved goals: 0 / 1
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
- Lemma - - 1 100%
+ Lemma - - 1 0.0%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/trig.i b/src/plugins/wp/tests/wp_plugin/trig.i
index c97b9d6a18614969df4d5f71a7e43a3e3c9392d6..0fdc8f2bd7f55b850e27a49637e0ba993228266a 100644
--- a/src/plugins/wp/tests/wp_plugin/trig.i
+++ b/src/plugins/wp/tests/wp_plugin/trig.i
@@ -1,10 +1,3 @@
-/* run.config
- STDOPT: +"-wp-no-extensional"
-*/
-/* run.config_qualif
- OPT: -wp -wp-par 1 -wp-no-extensional
-*/
-
typedef struct MSG {
int size ;
unsigned char text [65536] ;
@@ -12,20 +5,20 @@ typedef struct MSG {
/*@ axiomatic Messages {
@ logic message concat( message a , message b );
- @
- @ axiom cats: \forall message a,b ;
+ @
+ @ axiom cats: \forall message a,b ;
@ concat(a,b).size == a.size + b.size ;
- @
+ @
@ axiom cat1: \forall message a,b,c ; \forall integer k ;
@ c == concat(a,b) ==>
- @ 0 <= k < a.size ==>
+ @ 0 <= k < a.size ==>
@ c.text[k] == a.text[k] ;
- @
+ @
@ axiom cat2: \forall message a,b,c ; \forall integer k ;
@ (TRIGGER: c == concat(a,b)) ==>
- @ a.size <= k < a.size + b.size ==>
+ @ a.size <= k < a.size + b.size ==>
@ (TRIGGER: c.text[k]) == b.text[k - a.size] ;
- @
+ @
@ }
@ */
@@ -39,7 +32,7 @@ message fconcat(message a,message b);
void foo(message a,message b)
{
message c = fconcat(a,b);
- //@ assert qed_ok: S: c.size == 10 ;
- //@ assert qed_ok: A: c.text[2] == a.text[2] ;
- //@ assert qed_ok: B: c.text[7] == b.text[2] ;
+ //@ assert ok: S: c.size == 10 ;
+ //@ assert ok: A: c.text[2] == a.text[2] ;
+ //@ assert ok: B: c.text[7] == b.text[2] ;
}
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.res.oracle
index dbc2330142860c450016dadd3afe2cd9f5c8a828..96bb1c3037c84b0974790f377c051aa0257fd6fa 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.res.oracle
@@ -3,12 +3,12 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
-[wp] [Alt-Ergo] Goal typed_compound_assert_SEP : Valid
+[wp] [Alt-Ergo] Goal typed_compound_assert_SEP : Unsuccess
[wp] [Alt-Ergo] Goal typed_compound_assert_RES : Valid
-[wp] Proved goals: 2 / 2
+[wp] Proved goals: 1 / 2
Qed: 0
- Alt-Ergo: 2
+ Alt-Ergo: 1 (unsuccess: 1)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- compound - 2 2 100%
+ compound - 1 2 50.0%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
index 3a1b937b6ff4108b49bc33d4e58bceb54b322deb..a5f8a971b9f1229e8509d038e8f7451dafdfa9f7 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
@@ -2,9 +2,9 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_136) /\\ (i_1<=i_137) /\\ (0<=i_0) /\\ (i_136<=i_0) /\\ (i_137<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0097,
- "steps": 12 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0109,
- "steps": 16 } ] } } ]
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.017,
+ "steps": 22 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0148,
+ "steps": 22 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
index 3a1b937b6ff4108b49bc33d4e58bceb54b322deb..a5f8a971b9f1229e8509d038e8f7451dafdfa9f7 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
@@ -2,9 +2,9 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_136) /\\ (i_1<=i_137) /\\ (0<=i_0) /\\ (i_136<=i_0) /\\ (i_137<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0097,
- "steps": 12 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0109,
- "steps": 16 } ] } } ]
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.017,
+ "steps": 22 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0148,
+ "steps": 22 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
index d177a98c28b67066576c3d38a7a0eff89828cfda..1a1c4c0451c01821da44f4cd61861b8ebeee4f02 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
@@ -2,9 +2,9 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_9) /\\ (i_1<=i_10) /\\ (0<=i_0) /\\ (i_9<=i_0) /\\ (i_10<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0124,
- "steps": 22 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.009,
- "steps": 28 } ] } } ]
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0236,
+ "steps": 41 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0251,
+ "steps": 41 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
index f5c72396b7f8ddae811ebc406bbbbdc5fb40e428..398a69be748b427406223332d1c8447708dc51e1 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
@@ -2,9 +2,9 @@
"select": { "select": "clause-goal",
"target": "exists i_1,i_2:int.\n(i_1<=i_0) /\\ (i_2<=i_3) /\\ (0<=i_1) /\\ (i_0<=i_1) /\\ (i_3<=i_2) /\\ (i_1<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0133,
- "steps": 16 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0081,
- "steps": 22 } ] } } ]
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.018,
+ "steps": 29 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.022,
+ "steps": 29 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_assigns_part2.json
index 6168a77396917172956d78549bbe7dcf3219cf4d..d7d87cb0431b99609b2b733ee68bb9ac2cdc04e6 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_assigns_part2.json
@@ -2,9 +2,9 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_156) /\\ (i_1<=i_157) /\\ (0<=i_0) /\\ (i_156<=i_0) /\\ (i_157<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0076,
- "steps": 9 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0091,
- "steps": 11 } ] } } ]
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.011,
+ "steps": 16 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0092,
+ "steps": 16 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json
index 27f3c51ba83312b37f018ed69fc8d5b75b527624..9927a473006bfd0846ae22f978f724ca10e5e553 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json
@@ -2,9 +2,9 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_13) /\\ (i_1<=i_14) /\\ (0<=i_0) /\\ (i_13<=i_0) /\\ (i_14<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.017,
- "steps": 22 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0162,
- "steps": 24 } ] } } ]
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0177,
+ "steps": 40 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0177,
+ "steps": 40 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json
index 60c3f311be2351c5b45237a512d006907d24cdb1..e43bf2a0c07c931be6a637bc59d7981d08afa12f 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json
@@ -2,9 +2,9 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_2:int.\n(i_0<=i_1) /\\ (0<=i_0) /\\ (i_1<=i_0) /\\ (j_0<=i_2) /\\ (i_2<=j_0) /\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i0#1$i#1$j#0" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0105,
- "steps": 14 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0145,
- "steps": 16 } ] } } ]
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0154,
+ "steps": 24 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0157,
+ "steps": 24 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json
index 7297a4bc53302546af749a5462ef046aa7bfd5d5..8138f144480b3491b3bd4e0ba6074c5cd9988c62 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json
@@ -2,9 +2,9 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_21) /\\ (i_1<=i_22) /\\ (0<=i_0) /\\ (i_21<=i_0) /\\ (i_22<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0163,
- "steps": 18 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0156,
- "steps": 20 } ] } } ]
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0167,
+ "steps": 33 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0171,
+ "steps": 33 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json
index 4bad3f08d5e99af184014fde5dcee4bb5b90c96b..c110027873b58604a7e9b1f4add93925e424cd1f 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json
@@ -2,9 +2,9 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_8) /\\ (i_1<=i_9) /\\ (0<=i_0) /\\ (i_8<=i_0) /\\ (i_9<=i_1) /\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0163,
- "steps": 18 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0156,
- "steps": 20 } ] } } ]
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0167,
+ "steps": 33 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0171,
+ "steps": 33 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_assigns_part2.json
index 6b363edb0f779b2bde6f0df63a6319ee68cc03c8..2f0e9f12c125589ccbe9b513e6c1145d72b89497 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_assigns_part2.json
@@ -2,9 +2,9 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_148) /\\ (i_1<=i_149) /\\ (0<=i_0) /\\ (i_148<=i_0) /\\ (i_149<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0076,
- "steps": 9 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0091,
- "steps": 11 } ] } } ]
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.011,
+ "steps": 16 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0092,
+ "steps": 16 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json
index 957e4cdf73998a9b788068ebfe746895109ec89a..0f331f4933d265794ca3c72277892cdaeef876be 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json
@@ -2,9 +2,9 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_13) /\\ (i_1<=i_14) /\\ (0<=i_0) /\\ (i_13<=i_0) /\\ (i_14<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0152,
- "steps": 23 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0165,
- "steps": 27 } ] } } ]
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0196,
+ "steps": 39 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0223,
+ "steps": 39 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json
index 9a022b74ecf6f56589717f3faecc6797baf0fb58..9fc6a77f392331e6771b07d65d55ebfb62b84ae8 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json
@@ -2,9 +2,9 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_4) /\\ (i_1<=i_6) /\\ (0<=i_0) /\\ (i_4<=i_0) /\\ (i_6<=i_1) /\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0142,
- "steps": 17 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.014,
- "steps": 21 } ] } } ]
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0152,
+ "steps": 27 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0151,
+ "steps": 27 } ] } } ]
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index acc0f77cfbedb6e1c4039e3df1afac556cdfea71..94f5b8131ffe76c1ea358b39e5130bc4b1088a3f 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -155,21 +155,20 @@ let iter_fct phi = function
(fun kf -> if not (Fct.mem kf fs) then phi kf)
| Fct_list fs -> Fct.iter phi fs
-let get_kf () =
+let get_kfs () =
if Functions.is_empty() then
if SkipFunctions.is_empty () then Fct_all
else Fct_skip (SkipFunctions.get())
else
Fct_list (Fct.diff (Functions.get()) (SkipFunctions.get()))
-let get_wp () =
+let get_fct () =
if WP.get () || not (Functions.is_empty()) ||
not (Behaviors.is_empty()) || not (Properties.is_empty())
- then get_kf ()
+ then get_kfs ()
else Fct_none
-let iter_wp f = iter_fct f (get_wp ())
-let iter_kf f = iter_fct f (get_kf ())
+let iter_kf f = iter_fct f (get_fct ())
(* ------------------------------------------------------------------------ *)
(* --- Memory Models --- *)
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index 236c418e01883ea1690ca1a4961af637dd808464..a37b5e895a7470f21a738e3c69a5c15dc9566796 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -32,11 +32,9 @@ type functions =
| Fct_skip of Cil_datatype.Kf.Set.t
| Fct_list of Cil_datatype.Kf.Set.t
-val get_kf : unit -> functions
-val get_wp : unit -> functions
+val get_fct : unit -> functions
val iter_fct : (Kernel_function.t -> unit) -> functions -> unit
val iter_kf : (Kernel_function.t -> unit) -> unit
-val iter_wp : (Kernel_function.t -> unit) -> unit
(** {2 Goal Selection} *)