From 2365633e87248db53da94795452c392ca81c8538 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 2 Dec 2022 14:00:49 +0100
Subject: [PATCH] [wp] detect multiple goals with the same identifier
---
src/plugins/wp/cfgWP.ml | 3 +++
1 file changed, 3 insertions(+)
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index 2e20c87f609..e1a4d022b51 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -481,6 +481,9 @@ struct
let add_vc
target ?(warn=Warning.Set.empty) ?(deps=Property.Set.empty) pred vcs =
let xs , hs , goal = introduction pred in
+ if Gmap.mem target vcs then
+ Wp_parameters.failure
+ "Multiple goals for the same target (%a)" TARGET.pretty target ;
let hyps = Conditions.intros hs Conditions.nil in
let vc = { empty_vc with goal ; vars=xs ; hyps ; warn ; deps } in
Gmap.add target (Splitter.singleton vc) vcs
--
GitLab