From 92654857572ebc16d35ddbae3ddeb3bbd975330b Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@cea.fr>
Date: Mon, 8 Nov 2021 15:56:38 +0100
Subject: [PATCH] [e-acsl] bugfix: unguarded quantifications
---
src/plugins/e-acsl/src/analyses/bound_variables.ml | 10 ++++++++--
1 file changed, 8 insertions(+), 2 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml
index f6fa2398373..447a396a399 100644
--- a/src/plugins/e-acsl/src/analyses/bound_variables.ml
+++ b/src/plugins/e-acsl/src/analyses/bound_variables.ml
@@ -684,8 +684,14 @@ end
compute_guards loc ~is_forall:true p bound_vars goal
| Pexists(bound_vars, ({ pred_content = Pand(_, _) } as goal)) ->
compute_guards loc ~is_forall:false p bound_vars goal
- | Pforall _ -> Error.not_yet "unguarded \\forall quantification"
- | Pexists _ -> Error.not_yet "unguarded \\exists quantification"
+ | Pforall _ ->
+ Quantifier.add
+ p
+ (Err (Error.Not_yet "unguarded \\forall quantification"))
+ | Pexists _ ->
+ Quantifier.add
+ p
+ (Err (Error.Not_yet "unguarded \\exists quantification"))
| _ -> ()
let gannot a =
--
GitLab