Merge pull request #172 from goblint/attr-enumerator

Add enumerator attributes

src/check.ml

@@ -390,7 +390,7 @@ and checkEnumInfo (isadef: defuse) enum =
     (* Add it to the map before we go on *)
     H.add enumUsed enum.ename (enum, ref isadef);
     checkAttributes enum.eattr;
-    List.iter (fun (tn, _, _) -> defineName tn) enum.eitems;
+    List.iter (fun (tn, attrs, _, _) -> defineName tn; checkAttributes attrs) enum.eitems;
   end
 
 and checkTypeInfo (isadef: defuse) ti =

src/cil.ml

@@ -399,7 +399,7 @@ and fieldinfo = {
     enumeration. Make sure you have a [GEnumTag] for each of of these.   *)
 and enuminfo = {
     mutable ename: string;              (** The name. Always non-empty *)
-    mutable eitems: (string * exp * location) list; (** Items with names
+    mutable eitems: (string * attributes * exp * location) list; (** Items with names
                                                       and values. This list
                                                       should be
                                                       non-empty. The item
@@ -4014,8 +4014,10 @@ class defaultCilPrinterClass : cilPrinter = object (self)
           text "enum" ++ align ++ text (" " ^ enum.ename) ++
           text " {" ++ line
           ++ (docList ~sep:(chr ',' ++ line)
-                (fun (n,i, loc) ->
-                  text (n ^ " = ")
+                (fun (n, attrs, i, loc) ->
+                  text n
+                    ++ self#pAttrs () attrs
+                    ++ text (n ^ " = ")
                     ++ self#pExp () i)
                 () enum.eitems)
           ++ unalign ++ line ++ text "} "
@@ -5622,7 +5624,7 @@ and childrenGlobal (vis: cilVisitor) (g: global) : global =
   | GEnumTag (enum, _) ->
       (* (trace "visit" (dprintf "visiting global enum %s\n" enum.ename)); *)
       (* Do the values and attributes of the enumerated items *)
-      let itemVisit (name, exp, loc) = (name, visitCilExpr vis exp, loc) in
+      let itemVisit (name, attrs, exp, loc) = (name, visitCilAttributes vis attrs, visitCilExpr vis exp, loc) in
       enum.eitems <- mapNoCopy itemVisit enum.eitems;
       enum.eattr <- visitCilAttributes vis enum.eattr;
       g

src/cil.mli

@@ -423,7 +423,7 @@ and fieldinfo = {
 and enuminfo = {
     mutable ename: string;
     (** The name. Always non-empty. *)
-    mutable eitems: (string * exp * location) list;
+    mutable eitems: (string * attributes * exp * location) list;
     (** Items with names and values. This list should be non-empty. The item
        values must be compile-time constants. *)
     mutable eattr: attributes;

src/ext/zrapp/zrapp.ml

@@ -412,8 +412,10 @@ class zraCilPrinterClass : cilPrinter = object (self)
           text "enum" ++ align ++ text (" " ^ enum.ename) ++
           self#pAttrs () enum.eattr ++ text " {" ++ line
           ++ (docList ~sep:(chr ',' ++ line)
-                (fun (n,i, loc) ->
-                  text (n ^ " = ")
+                (fun (n, attrs, i, loc) ->
+                  text n
+                    ++ self#pAttrs () attrs
+                    ++ text (n ^ " = ")
                     ++ self#pExp () i)
                 () enum.eitems)
           ++ unalign ++ line ++ text "};\n"

src/frontc/cabs.ml

@@ -168,7 +168,7 @@ and init_name = name * init_expression
 and single_name = specifier * name
 
 
-and enum_item = string * expression * cabsloc
+and enum_item = string * attribute list * expression * cabsloc
 
 (*
 ** Declaration definition (at toplevel)

src/frontc/cabs2cil.ml

@@ -2675,7 +2675,7 @@ let rec doSpecList (suggestedAnonName: string) (* This string will be part of
     | [A.Tenum (n, Some eil, extraAttrs)] -> (* A definition of an enum *)
         let rec justNames eil = match eil with
             [] -> []
-          | (str, expr, loc) :: eis -> str :: justNames eis
+          | (str, attrs, expr, loc) :: eis -> str :: justNames eis
         in
         let names = justNames eil in
         let n' =
@@ -2721,7 +2721,7 @@ let rec doSpecList (suggestedAnonName: string) (* This string will be part of
           else IULongLong (* assume there can be not enum constants that don't fit in long long since there can only be 128bit constants if long long is also 128bit *)
         in
         (* as each name,value pair is determined, this is called *)
-        let rec processName kname (i: exp) loc rest = begin
+        let rec processName kname attrs (i: exp) loc rest = begin
           (* add the name to the environment, but with a faked 'typ' field;
              we don't know the full type yet (since that includes all of the
              tag values), but we won't need them in here  *)
@@ -2731,16 +2731,16 @@ let rec doSpecList (suggestedAnonName: string) (* This string will be part of
             environment when we're finished  *)
           let newname, _  = newAlphaName true "" kname in
 
-          (kname, (newname, i, loc)) :: loop (increm i 1) rest
+          (kname, (newname, doAttributes attrs, i, loc)) :: loop (increm i 1) rest
         end
 
         and loop i = function
             [] -> []
-          | (kname, A.NOTHING, cloc) :: rest ->
+          | (kname, attrs, A.NOTHING, cloc) :: rest ->
               (* use the passed-in 'i' as the value, since none specified *)
-              processName kname i (convLoc cloc) rest
+              processName kname attrs i (convLoc cloc) rest
 
-          | (kname, e, cloc) :: rest ->
+          | (kname, attrs, e, cloc) :: rest ->
               (* constant-eval 'e' to determine tag value *)
               let e' = getIntConstExp e in
               let e'' =
@@ -2750,7 +2750,7 @@ let rec doSpecList (suggestedAnonName: string) (* This string will be part of
 		                if !lowerConstants then kintegerCilint ik n else e'
                 | _ -> E.s (error "Constant initializer %a not an integer" d_exp e')
               in
-              processName kname e'' (convLoc cloc) rest
+              processName kname attrs e'' (convLoc cloc) rest
         in
 
         let fields = loop zero eil in

src/frontc/cabsvisit.ml

@@ -198,9 +198,10 @@ and childrenTypeSpecifier vis ts =
       let fg' = mapNoCopy childrenFieldGroup fg in
       if fg' != fg then Tunion( n, Some fg', extraAttrs) else ts
   | Tenum (n, Some ei, extraAttrs) ->
-      let doOneEnumItem ((s, e, loc) as ei) =
+      let doOneEnumItem ((s, attrs, e, loc) as ei) =
+        let attrs' = visitCabsAttributes vis attrs in
         let e' = visitCabsExpression vis e in
-        if e' != e then (s, e', loc) else ei
+        if attrs' != attrs || e' != e then (s, attrs', e', loc) else ei
       in
       vis#vEnterScope ();
       let ei' = mapNoCopy doOneEnumItem ei in

src/frontc/cparser.mly

@@ -1188,8 +1188,8 @@ enum_list: /* (* ISO 6.7.2.2 *) */
 |   enum_list COMMA error               { $1 }
 ;
 enumerator:
-    IDENT			{(fst $1, NOTHING, snd $1)}
-|   IDENT EQ expression		{(fst $1, fst $3, snd $1)}
+    IDENT attributes			{(fst $1, $2, NOTHING, snd $1)}
+|   IDENT attributes EQ expression		{(fst $1, $2, fst $4, snd $1)}
 ;
 
 

src/frontc/cprint.ml

@@ -262,10 +262,11 @@ and print_enum_items items =
     indent ();
     print_commas
       true
-      (fun (id, exp, loc) -> print id;
+      (fun (id, attrs, exp, loc) -> print id;
 	if exp = NOTHING then ()
 	else begin
 	  space ();
+    print_attributes attrs;
 	  print "= ";
 	  print_expression exp
 	end)

src/mergecil.ml

@@ -701,9 +701,11 @@
        (* We check that they are defined in the same way. This is a fairly
             conservative check. *)
        List.iter2
-         (fun (old_iname, old_iv, _) (iname, iv, _) ->
+         (fun (old_iname, old_attrs, old_iv, _) (iname, attrs, iv, _) ->
            if old_iname <> iname then
              raise (Failure "(different names for enumeration items)");
+           if old_attrs <> attrs then
+             raise (Failure "(different enumerator attributes)");
            let samev =
              match (constFold true old_iv, constFold true iv) with
              | Const (CInt (oldi, _, _)), Const (CInt (i, _, _)) ->
@@ -1545,12 +1547,12 @@
                     as the variables *)
                  ei.eitems <-
                    Util.list_map
-                     (fun (n, i, loc) ->
+                     (fun (n, attrs, i, loc) ->
                        let newname, _ =
                          A.newAlphaName ~alphaTable:vtAlpha ~undolist:None
                            ~lookupname:n ~data:!currentLoc
                        in
-                       (newname, i, loc))
+                       (newname, attrs, i, loc))
                      ei.eitems;
                  mergePushGlobals (visitCilGlobal renameVisitor g)
              | Some (ei', _) ->

test/small1/attr-enumerator.c

@@ -0,0 +1,8 @@
+// From some new MacOS headers
+
+enum {
+    A,
+    B __attribute__((availability(macos,introduced=10.15))),
+    C = 5,
+    D __attribute__((availability(macos,introduced=10.15))) = 7
+} E;

test/testcil.pl

@@ -223,6 +223,7 @@ sub addToGroup {
 addTest("test/attr12 _GNUCC=1");
 addTest("test/attr13 _GNUCC=1");
 # addTest("test/attr-assign"); # TODO: only on OSX, Linux GCC errors on introduced
+# addTest("test/attr-enumerator"); # TODO: only on OSX, Linux GCC errors on introduced
 addTest("testrun/packed _GNUCC=1 WARNINGS_ARE_ERRORS=1");
 addTest("test/packed2 _GNUCC=1");
 addTest("test/bitfield");