diff --git a/src/plugins/e-acsl/src/analyses/analyses.ml b/src/plugins/e-acsl/src/analyses/analyses.ml index 1e208d4431797c4e87984f21ba94036b2bb6a453..eeaa2dc9da43da2b12e3c869d07b65738c80e633 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 a47db3d0cf0a6a287666a6f82c876636db1db31e..423e630b1ab8de860350f50d9d6ba3cce30075c3 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 ->