From 65312ded6c15b871d06fb7d015d7447782d1d1d7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Fri, 21 May 2021 15:29:12 +0200
Subject: [PATCH] [WP] Side step mis-documentation in Why3 by always setting a
memlimit
---
src/plugins/wp/ProverWhy3.ml | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 96090a60d09..c38cd16fcaf 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1249,10 +1249,11 @@ let digest wpo drv prover task =
let batch pconf driver ?script ~timeout ~steplimit prover task =
let steps = match steplimit with Some 0 -> None | _ -> steplimit in
let limit =
+ let memlimit = Why3.Whyconf.memlimit (Why3.Whyconf.get_main (Why3Provers.config ())) in
let def = Why3.Call_provers.empty_limit in
- { def with
- Why3.Call_provers.limit_time = Why3.Opt.get_def def.limit_time timeout;
+ { Why3.Call_provers.limit_time = Why3.Opt.get_def def.limit_time timeout;
Why3.Call_provers.limit_steps = Why3.Opt.get_def def.limit_time steps;
+ Why3.Call_provers.limit_mem = memlimit;
} in
let with_steps = match steps, pconf.Why3.Whyconf.command_steps with
| None, _ -> false
--
GitLab