diff --git a/src/plugins/e-acsl/src/analyses/logic_normalizer.ml b/src/plugins/e-acsl/src/analyses/logic_normalizer.ml index bc2b125769d3f2132e603764a329775e06911caf..02868eb133a9a2e3475557bcc183fa8368ec270f 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