From b8536a7552f446720d5007c5ccb213a2710e547f Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Fri, 11 Feb 2022 17:49:26 +0100
Subject: [PATCH] [eacsl] Update Logic_normalizer to visit global annotations
---
src/plugins/e-acsl/src/analyses/logic_normalizer.ml | 1 +
1 file changed, 1 insertion(+)
diff --git a/src/plugins/e-acsl/src/analyses/logic_normalizer.ml b/src/plugins/e-acsl/src/analyses/logic_normalizer.ml
index bc2b125769d..02868eb133a 100644
--- a/src/plugins/e-acsl/src/analyses/logic_normalizer.ml
+++ b/src/plugins/e-acsl/src/analyses/logic_normalizer.ml
@@ -128,6 +128,7 @@ let preprocessor = object
(* Only logic functions and logic predicates are handled.
E-acsl simply ignores all the other global annotations *)
+ method !glob_annot _ = Cil.DoChildren
method !vannotation annot =
match annot with
| Dfun_or_pred _ -> Cil.DoChildren
--
GitLab