From 76f4f08fb3b452f9e431d1a914f345f8b494b186 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 26 Jul 2019 17:59:01 +0200
Subject: [PATCH] [kernel] retrieve all global annotations attributes
---
src/kernel_services/ast_queries/cil.ml | 10 +++++-----
1 file changed, 5 insertions(+), 5 deletions(-)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 064e9ae727c..0184c5caff7 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -6647,14 +6647,14 @@ let mapGlobals (fl: file)
end)
let global_annotation_attributes = function
- | Dfun_or_pred _ -> []
+ | Dfun_or_pred ({l_var_info = { lv_attr }}, _) -> lv_attr
| Dvolatile (_,_,_,attrs,_) -> attrs
| Daxiomatic (_,_,attrs,_) -> attrs
- | Dtype _ -> []
+ | Dtype ({ lt_attr }, _) -> lt_attr
| Dlemma (_,_,_,_,_,attrs,_) -> attrs
- | Dinvariant _ -> []
- | Dtype_annot _ -> []
- | Dmodel_annot _ -> []
+ | Dinvariant ({l_var_info = { lv_attr }}, _) -> lv_attr
+ | Dtype_annot ({l_var_info = { lv_attr }}, _) -> lv_attr
+ | Dmodel_annot ({ mi_attr }, _) -> mi_attr
| Dextended (_,attrs,_) -> attrs
| Dcustom_annot (_,_,attrs,_) -> attrs
--
GitLab