diff --git a/CodeHawk/CHB/bchcil/bCHCilToCBasic.ml b/CodeHawk/CHB/bchcil/bCHCilToCBasic.ml
index 2dbd319c..1a0adca7 100644
--- a/CodeHawk/CHB/bchcil/bCHCilToCBasic.ml
+++ b/CodeHawk/CHB/bchcil/bCHCilToCBasic.ml
@@ -200,9 +200,16 @@ and cil_fieldinfo_to_bfieldinfo (f: GoblintCil.fieldinfo): bfieldinfo_t = {
   }
 
 
-and cil_eitem_to_beitem (i: (string * GoblintCil.exp * GoblintCil.location)): beitem_t =
-  let (ename, eexp, eloc) = i in
-  (ename, cil_exp_to_bexp eexp, cil_location_to_b_location eloc)
+and cil_eitem_to_beitem
+(i: (string
+     * GoblintCil.attributes
+     * GoblintCil.exp
+     * GoblintCil.location)): beitem_t =
+  let (ename, attrs, eexp, eloc) = i in
+  (ename,
+   cil_attributes_to_b_attributes attrs,
+   cil_exp_to_bexp eexp,
+   cil_location_to_b_location eloc)
 
 
 and cil_enuminfo_to_benuminfo (e: GoblintCil.enuminfo): benuminfo_t = {
diff --git a/CodeHawk/CHB/bchlib/bCHBCDictionary.ml b/CodeHawk/CHB/bchlib/bCHBCDictionary.ml
index 9c9b9e9e..4937c612 100644
--- a/CodeHawk/CHB/bchlib/bCHBCDictionary.ml
+++ b/CodeHawk/CHB/bchlib/bCHBCDictionary.ml
@@ -720,16 +720,17 @@ object (self)
     }
 
   method index_enumitem (eitem: beitem_t) =
-    let (name, exp, loc) = eitem in
+    let (name, attrs, exp, loc) = eitem in
     let tags = [name] in
-    let args = [self#index_exp exp; self#index_location loc] in
+    let args =
+      [self#index_exp exp; self#index_location loc; self#index_attributes attrs] in
     enumitem_table#add (tags, args)
 
   method get_enumitem (index: int): beitem_t =
     let (tags, args) = enumitem_table#retrieve index in
     let t = t "beitem_t" tags in
     let a = a "beitem_t" args in
-    (t 0, self#get_exp (a 0), self#get_location (a 1))
+    (t 0, self#get_attributes (a 2), self#get_exp (a 0), self#get_location (a 1))
 
   method index_enuminfo (einfo: benuminfo_t) =
     let tags = [einfo.bename; ikind_mfts#ts einfo.bekind] in
diff --git a/CodeHawk/CHB/bchlib/bCHBCTypes.mli b/CodeHawk/CHB/bchlib/bCHBCTypes.mli
index 21b2ed5c..088761e1 100644
--- a/CodeHawk/CHB/bchlib/bCHBCTypes.mli
+++ b/CodeHawk/CHB/bchlib/bCHBCTypes.mli
@@ -246,7 +246,7 @@ and bfieldinfo_t = {
   bfieldlayout: fieldlayout_t option
 }
 
-and beitem_t = string * bexp_t * b_location_t
+and beitem_t = string * b_attributes_t * bexp_t * b_location_t
 
 and benuminfo_t = {
   bename: string;
diff --git a/CodeHawk/CHC/cchcil/cHCilDeclarations.ml b/CodeHawk/CHC/cchcil/cHCilDeclarations.ml
index ce3d8e6d..f13e89a9 100644
--- a/CodeHawk/CHC/cchcil/cHCilDeclarations.ml
+++ b/CodeHawk/CHC/cchcil/cHCilDeclarations.ml
@@ -175,12 +175,12 @@ object (self)
     compinfo_table#add (tags, args)
 
   method index_enumitem (eitem: enumitem) =
-    let (name, exp, loc) = eitem in
+    let (name, attrs, exp, loc) = eitem in
     let tags = [name] in
     let locix_r = self#index_location loc in
     match locix_r with
     | Ok locix ->
-       let args = [cd#index_exp exp; locix] in
+       let args = [cd#index_exp exp; locix; cd#index_attributes attrs] in
        enumitem_table#add (tags, args)
     | Error e ->
        begin
diff --git a/CodeHawk/CHC/cchcil/cHCilTypes.ml b/CodeHawk/CHC/cchcil/cHCilTypes.ml
index e4ae745a..44d0c3a3 100644
--- a/CodeHawk/CHC/cchcil/cHCilTypes.ml
+++ b/CodeHawk/CHC/cchcil/cHCilTypes.ml
@@ -35,7 +35,7 @@ open CHTraceResult
 open CHXmlDocument
 
 type funarg = string * typ * attributes
-type enumitem = string * exp * location
+type enumitem = string * attributes * exp * location
             
 class type cildictionary_int =
   object
diff --git a/CodeHawk/CHC/cchcil/cHCilTypes.mli b/CodeHawk/CHC/cchcil/cHCilTypes.mli
index 213d1219..dcac166a 100644
--- a/CodeHawk/CHC/cchcil/cHCilTypes.mli
+++ b/CodeHawk/CHC/cchcil/cHCilTypes.mli
@@ -36,7 +36,7 @@ open CHXmlDocument
 
 
 type funarg = string * typ * attributes
-type enumitem = string * exp * location
+type enumitem = string * attributes * exp * location
 
 
 class type cildictionary_int =
diff --git a/CodeHawk/CHC/cchlib/cCHBasicTypes.mli b/CodeHawk/CHC/cchlib/cCHBasicTypes.mli
index c5adbe83..c483c120 100644
--- a/CodeHawk/CHC/cchlib/cCHBasicTypes.mli
+++ b/CodeHawk/CHC/cchlib/cCHBasicTypes.mli
@@ -157,7 +157,7 @@ and fieldinfo = {
   floc     : location
 }
 
-and eitem = string * exp * location
+and eitem = string * attributes * exp * location
 
 and enuminfo = {
   ename    : string ;
diff --git a/CodeHawk/CHC/cchlib/cCHDeclarations.ml b/CodeHawk/CHC/cchlib/cCHDeclarations.ml
index f100780d..92e45713 100644
--- a/CodeHawk/CHC/cchlib/cCHDeclarations.ml
+++ b/CodeHawk/CHC/cchlib/cCHDeclarations.ml
@@ -237,17 +237,20 @@ object (self)
       cattr = cd#get_attributes (a 2);
       cfields = List.map self#get_fieldinfo (get_list_suffix args 3) }
 
-  method index_enumitem (eitem:enumitem) =
-    let (name,exp,loc) = eitem in
+  method index_enumitem (eitem: enumitem) =
+    let (name, attrs, exp, loc) = eitem in
     let tags = [name] in
-    let args = [cd#index_exp exp; self#index_location loc] in
-    enumitem_table#add (tags,args)
+    let args = [
+        cd#index_exp exp;
+        self#index_location loc;
+        cd#index_attributes attrs] in
+    enumitem_table#add (tags, args)
 
   method get_enumitem (index:int):enumitem =
     let (tags,args) = enumitem_table#retrieve index in
     let t = t "enumitem" tags in
     let a = a "enumitem" args in
-    (t 0, cd#get_exp (a 0), self#get_location (a 1))
+    (t 0, cd#get_attributes (a 2), cd#get_exp (a 0), self#get_location (a 1))
 
   method index_enuminfo (einfo:enuminfo) =
     let tags = [einfo.ename; ikind_mfts#ts einfo.ekind] in
diff --git a/CodeHawk/CHC/cchlib/cCHLibTypes.mli b/CodeHawk/CHC/cchlib/cCHLibTypes.mli
index 0714e37d..4ffae738 100644
--- a/CodeHawk/CHC/cchlib/cCHLibTypes.mli
+++ b/CodeHawk/CHC/cchlib/cCHLibTypes.mli
@@ -186,7 +186,7 @@ class type cdictionary_int =
 
 (** {1 Declarations} *)
 
-type enumitem = string * exp * location
+type enumitem = string * attributes * exp * location
 
 class type cdeclarations_int =
   object
diff --git a/CodeHawk/CHC/cchlib/cCHTypesCompare.ml b/CodeHawk/CHC/cchlib/cCHTypesCompare.ml
index dceeb83b..ad2ca587 100644
--- a/CodeHawk/CHC/cchlib/cCHTypesCompare.ml
+++ b/CodeHawk/CHC/cchlib/cCHTypesCompare.ml
@@ -310,9 +310,9 @@ and exp_compare (e1:exp) (e2:exp) =
       l0
 
 
-and eitem_compare (eitem1:eitem) (eitem2:eitem) =
-  let (iname1,iexp1,_) = eitem1 in
-  let (iname2,iexp2,_) = eitem2 in
+and eitem_compare (eitem1: eitem) (eitem2: eitem) =
+  let (iname1,_, iexp1, _) = eitem1 in
+  let (iname2,_, iexp2, _) = eitem2 in
   let l0 = Stdlib.compare iname1 iname2 in
   if l0 = 0 then
     exp_compare iexp1 iexp2
diff --git a/CodeHawk/CHC/cchlib/cCHTypesUtil.ml b/CodeHawk/CHC/cchlib/cCHTypesUtil.ml
index 735cff33..35b08824 100644
--- a/CodeHawk/CHC/cchlib/cCHTypesUtil.ml
+++ b/CodeHawk/CHC/cchlib/cCHTypesUtil.ml
@@ -159,7 +159,7 @@ let get_typ_attributes (t:typ) =
 
 let is_enum_constant (ename:string) (exp:exp) =
   let einfo = fenv#get_enum ename in
-  let eexps = List.map (fun (_,e,_) -> e) einfo.eitems in
+  let eexps = List.map (fun (_, _, e, _) -> e) einfo.eitems in
   List.exists (fun e -> (exp_compare e exp) = 0) eexps
 
 
@@ -537,9 +537,9 @@ let const_fits_kind (c:constant) (target_ik:ikind) =
   | _ -> false
 
 
-let enum_fits_kind (ename:string) (target_ik:ikind) =
+let enum_fits_kind (ename: string) (target_ik:ikind) =
   let einfo = fenv#get_enum ename in
-  List.for_all (fun (_, e, _) ->
+  List.for_all (fun (_, _, e, _) ->
       match e with
       | Const c -> const_fits_kind c target_ik
       | _ -> false) einfo.eitems