From a4cb465d843a2445bda034a795b9020cd7e0cfbd Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 4 Mar 2022 17:28:17 +0100
Subject: [PATCH] [e-acsl] fix post-merge crash
---
src/plugins/e-acsl/src/analyses/analyses.ml | 2 +-
src/plugins/e-acsl/src/analyses/labels.ml | 3 +++
2 files changed, 4 insertions(+), 1 deletion(-)
diff --git a/src/plugins/e-acsl/src/analyses/analyses.ml b/src/plugins/e-acsl/src/analyses/analyses.ml
index 1e208d44317..eeaa2dc9da4 100644
--- a/src/plugins/e-acsl/src/analyses/analyses.ml
+++ b/src/plugins/e-acsl/src/analyses/analyses.ml
@@ -32,7 +32,7 @@ let preprocess () =
analyses_feedback "typing annotations";
Typing.type_program ast;
analyses_feedback
- "computing translation locations of labeled predicates and terms";
+ "computing future locations of labeled predicates and terms";
Labels.preprocess ast
let reset () =
diff --git a/src/plugins/e-acsl/src/analyses/labels.ml b/src/plugins/e-acsl/src/analyses/labels.ml
index a47db3d0cf0..423e630b1ab 100644
--- a/src/plugins/e-acsl/src/analyses/labels.ml
+++ b/src/plugins/e-acsl/src/analyses/labels.ml
@@ -517,6 +517,8 @@ class vis_at_labels () = object (self)
inherit E_acsl_visitor.visitor dkey
+ method! glob_annot _ = Cil.SkipChildren
+
(** Launch the analysis on the given predicate. *)
method! vpredicate p =
let kf = Option.get self#current_kf in
@@ -549,6 +551,7 @@ let reset () =
Stmt.Hashtbl.clear at_data_for_stmts
let _debug () =
+ Options.feedback ~level:2 "Labels preprocessing";
Options.feedback ~level:2 "|Locations:";
Stmt.Hashtbl.iter
(fun stmt ats_ref ->
--
GitLab