From c6d61b96a28272d33bd01ddc95f616eb818b94f0 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 1 Feb 2021 16:12:37 +0100
Subject: [PATCH] [wp] Prove main requires
---
src/plugins/wp/cfgCalculus.ml | 6 ++++++
1 file changed, 6 insertions(+)
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 5ff18776dae..77b150a71b9 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -363,6 +363,11 @@ struct
let req = default_requires mode kf in
let bhv = CfgAnnot.get_behavior kf Kglobal has_exit ~active:[] mode.bhv in
+ let prove_if_main env ps =
+ if not @@ WpStrategy.is_main_init kf then Extlib.id
+ else List.fold_right (prove_property env) ps
+ in
+
env.we ,
(* global init *)
W.close env.we @@
@@ -372,6 +377,7 @@ struct
W.label env.we None Clabels.pre @@
List.fold_right (use_property env) req @@
List.fold_right (use_property env) bhv.bhv_assumes @@
+ prove_if_main env bhv.bhv_requires @@
List.fold_right (use_property env) bhv.bhv_requires @@
List.fold_right (use_property env) (behaviors kf) @@
List.fold_right (prove_property env) (complete mode kf) @@
--
GitLab