From 1c81259aba1bd620d612d07452012d74658dd376 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 16 Dec 2024 11:28:17 +0100
Subject: [PATCH] [wp] Upgrade to Why3 1.8
---
nix/sources.json | 4 ++--
opam | 2 +-
reference-configuration.md | 4 ++--
src/plugins/wp/ProverWhy3.ml | 20 +++++--------------
.../wp_plugin/oracle_qualif/config.res.oracle | 2 +-
5 files changed, 11 insertions(+), 21 deletions(-)
diff --git a/nix/sources.json b/nix/sources.json
index c11198b6e2f..cee5b8ffbcf 100644
--- a/nix/sources.json
+++ b/nix/sources.json
@@ -45,8 +45,8 @@
"why3": {
"branch": "master",
"repo": "https://gitlab.inria.fr/why3/why3.git",
- "rev": "1343338d3bb1941c0d4f134283bb0790816113c4",
+ "rev": "187fd52100329200d102e27f9ada7b25541e98f4",
"type": "git",
- "version": "1.7.2"
+ "version": "1.8.0"
}
}
diff --git a/opam b/opam
index 6f571573ec6..93d8881e4e2 100644
--- a/opam
+++ b/opam
@@ -137,7 +137,7 @@ depends: [
"ocp-indent" { with-dev-setup & >= "1.8.1" }
"odoc" { with-doc }
"unionFind" { >= "20220107" }
- "why3" { >= "1.7.1" & (< "1.8.0" | !with-test) }
+ "why3" { >= "1.8.0" & < "1.9.0" }
"yaml" { >= "3.0.0" }
"yojson" {>= "1.6.0" & (>= "2.0.1" | !with-test)}
"zarith" { >= "1.9" }
diff --git a/reference-configuration.md b/reference-configuration.md
index 9c9285676b8..3a2aa0d035f 100644
--- a/reference-configuration.md
+++ b/reference-configuration.md
@@ -2,7 +2,6 @@ The following set of packages is known to be a working configuration for
compiling Frama-C 30.0.
- OCaml 4.14.2
-- alt-ergo.2.5.4 (for wp, optional)
- dune.3.16.1
- dune-configurator.3.16.1
- dune-site.3.16.1
@@ -14,6 +13,7 @@ compiling Frama-C 30.0.
- ppx_deriving_yaml.0.3.0
- ppx_deriving_yojson.3.9.0
- unionFind.20220122
-- why3.1.7.2
+- why3.1.8.0 (for wp)
+- alt-ergo.2.5.4 (for wp, optional)
- yojson.2.2.2
- zarith.1.14
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 276394d7fe0..fab53a5ecf4 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1200,8 +1200,6 @@ let prover_task env prover task =
(* --- Prover Call --- *)
(* -------------------------------------------------------------------------- *)
-let altergo_step_limit = Str.regexp "^Steps limit reached:"
-
type prover_call = {
prover : Why3Provers.t ;
call : Why3.Call_provers.prover_call ;
@@ -1226,8 +1224,7 @@ let debug_model (res:Why3.Call_provers.prover_result) =
begin fun (res,model) ->
Format.fprintf fmt "@[<hov 2>model %a: %a@]@\n"
Why3.Call_provers.print_prover_answer res
- (Why3.Model_parser.print_model_human
- ~filter_similar:false
+ (Why3.Model_parser.print_model
~print_attrs:true) model
end
res.pr_models
@@ -1297,14 +1294,7 @@ let ping_prover_call ~config ~probes p =
debug_model pr;
VCS.result ~model:(get_model probes pr) VCS.Unknown
| _ when p.interrupted -> VCS.timeout p.timeout
- | Failure s -> VCS.failed s
- | HighFailure ->
- let alt_ergo_hack =
- p.prover.prover_name = "Alt-Ergo" &&
- Str.string_match altergo_step_limit pr.pr_output 0
- in
- if alt_ergo_hack then VCS.result ?steps:p.steps VCS.Stepout
- else VCS.failed "Unknown error"
+ | Failure msg | HighFailure msg -> VCS.failed msg
in
Wp_parameters.debug ~dkey
"@[@[Why3 result for %a:@] @[%a@] and @[%a@]@."
@@ -1374,11 +1364,11 @@ let run_batch pconf driver ~config
?(probes=Probe.Map.empty)
prover task =
let steps = match steplimit with Some 0 -> None | _ -> steplimit in
- let limit =
+ let limits =
let config = Why3.Whyconf.get_main @@ Why3Provers.config () in
let config_mem = Why3.Whyconf.memlimit config in
let config_time = Why3.Whyconf.timelimit config in
- let config_steps = Why3.Call_provers.empty_limit.limit_steps in
+ let config_steps = Why3.Call_provers.empty_limits.limit_steps in
Why3.Call_provers.{
limit_time = Option.value ~default:config_time timeout;
limit_steps = Option.value ~default:config_steps steps;
@@ -1398,7 +1388,7 @@ let run_batch pconf driver ~config
let inplace = if script <> None then Some true else None in
let call =
Why3.Driver.prove_task_prepared ?old:(script :> string option) ?inplace
- ~command ~limit ~config driver task in
+ ~command ~limits ~config driver task in
call_prover_task ~config ~timeout ~steps ~probes prover call
(* -------------------------------------------------------------------------- *)
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 00ab6f9978e..fc7eca0d054 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,7 +2,7 @@
WP Requirements for Qualif Tests
----------------------------------------------------------
1. The Alt-Ergo theorem prover, version v2.5.4
-2. The Why3 platform, version 1.7.2
+2. The Why3 platform, version 1.8.0
3. The environment variable FRAMAC_WP_CACHEDIR is defined
4. The environment variable FRAMAC_WP_CACHE is defined
----------------------------------------------------------
--
GitLab