Merge pull request #171 from goblint/attr-assign

Add assignment and floating-point constant attributes

src/cil.ml

@@ -344,6 +344,7 @@ and attrparam =
   | AAddrOf of attrparam                 (** & a **)
   | AIndex of attrparam * attrparam      (** a1[a2] *)
   | AQuestion of attrparam * attrparam * attrparam (** a1 ? a2 : a3 **)
+  | AAssign of attrparam * attrparam     (** a1 = a2 *)
 
 
 (** Information about a composite type (a struct or a union). Use
@@ -1874,6 +1875,7 @@ let additiveLevel = 60
 let comparativeLevel = 70
 let bitwiseLevel = 75
 let questionLevel = 100
+let assignLevel = 110
 let getParenthLevel (e: exp) =
   match e with
   | Question _ -> questionLevel
@@ -1924,6 +1926,7 @@ let getParenthLevelAttrParam (a: attrparam) =
   | AAddrOf _ -> 30
   | ADot _ | AIndex _ | AStar _ -> 20
   | AQuestion _ -> questionLevel
+  | AAssign _ -> assignLevel
 
 
 let isIntegralType t =
@@ -4423,6 +4426,9 @@ class defaultCilPrinterClass : cilPrinter = object (self)
           self#pAttrParam () a1 ++ text " ? " ++
           self#pAttrParam () a2 ++ text " : " ++
           self#pAttrParam () a3
+    | AAssign (a1, a2) ->
+          self#pAttrParam () a1 ++ text "=" ++
+          self#pAttrParam () a2
 
 
   (* A general way of printing lists of attributes *)
@@ -5561,6 +5567,10 @@ and childrenAttrparam (vis: cilVisitor) (aa: attrparam) : attrparam =
         let e3' = fAttrP e3 in
         if e1' != e1 || e2' != e2 || e3' != e3
         then AQuestion (e1', e2', e3') else aa
+    | AAssign (e1, e2) ->
+      let e1' = fAttrP e1 in
+      let e2' = fAttrP e2 in
+      if e1' != e1 || e2' != e2 then AAssign (e1', e2') else aa
 
 
 let rec visitCilFunction (vis : cilVisitor) (f : fundec) : fundec =

src/cil.mli

@@ -338,6 +338,7 @@ and attrparam =
   | AAddrOf of attrparam                 (** & a **)
   | AIndex of attrparam * attrparam      (** a1[a2] *)
   | AQuestion of attrparam * attrparam * attrparam (** a1 ? a2 : a3 **)
+  | AAssign of attrparam * attrparam     (** a1 = a2 *)
 
 (** {b Structures.} The {!compinfo} describes the definition of a
    structure or union type. Each such {!compinfo} must be defined at the

src/frontc/cabs2cil.ml

@@ -2927,6 +2927,7 @@ and doAttr (a: A.attribute) : attribute list =
             | _ ->
                 E.s (error "Invalid attribute constant: %s")
           end
+        | A.CONSTANT (A.CONST_FLOAT str) -> ACons (str, [])
         | A.CALL(A.VARIABLE n, args) -> begin
             let n' = if strip then stripUnderscore n else n in
             let ae' = Util.list_map ae args in
@@ -2940,6 +2941,8 @@ and doAttr (a: A.attribute) : attribute list =
             ABinOp(LAnd, ae aa1, ae aa2)
         | A.BINARY(A.OR, aa1, aa2) ->
             ABinOp(LOr, ae aa1, ae aa2)
+        | A.BINARY(A.ASSIGN, aa1, aa2) ->
+            AAssign(ae aa1, ae aa2)
         | A.BINARY(abop, aa1, aa2) ->
             ABinOp (convBinOp abop, ae aa1, ae aa2)
         | A.UNARY(A.PLUS, aa) -> ae aa

src/frontc/cparser.mly

@@ -1494,6 +1494,8 @@ primary_attr:
 |   LPAREN attr RPAREN                  { $2 }
 |   IDENT IDENT                          { CALL(VARIABLE (fst $1), [VARIABLE (fst $2)]) }
 |   CST_INT                              { CONSTANT(CONST_INT (fst $1)) }
+|   CST_FLOAT                            { CONSTANT(CONST_FLOAT (fst $1)) }
+|   CST_FLOAT CST_FLOAT                  { CONSTANT(CONST_FLOAT (fst $1 ^ fst $2)) } /* Clang-like hack to parse version numbers like "10.13.4" (https://github.com/goblint/cil/pull/171#issuecomment-2250670652). We lex them as "10.13" and ".4". */
 |   const_string_or_wstring                 { CONSTANT(fst $1) }
                                            /*(* Const when it appears in
                                               attribute lists, is translated
@@ -1619,8 +1621,12 @@ conditional_attr:
 |   logical_or_attr QUEST conditional_attr COLON conditional_attr
                                           { QUESTION($1, $3, $5) }
 
+assignment_attr:
+    conditional_attr              { $1 }
+|   unary_attr EQ assignment_attr { BINARY(ASSIGN, $1, $3) }
 
-attr: conditional_attr                    { $1 }
+
+attr: assignment_attr                    { $1 }
 ;
 
 attr_list_ne:

test/Makefile

@@ -127,6 +127,9 @@ ifdef SEPARATE
   CILLY+= --nomerge
 endif
 
+# Disable GCC 14 new warnings as errors because some tests contain them
+CFLAGS += -Wno-error=implicit-int -Wno-error=implicit-function-declaration -Wno-error=int-conversion -Wno-error=incompatible-pointer-types
+
 # sm: this will make gcc warnings into errors; it's almost never
 # what we want, but for a particular testcase (combine_copyptrs)
 # I need it to show the difference between something which works

test/small1/attr-assign.c

@@ -0,0 +1,14 @@
+// From some new MacOS headers: https://github.com/goblint/cil/issues/168
+
+void foo(void) __attribute__((availability(macos,introduced=10.15)));
+
+void foo(void) {
+    return;
+}
+
+// Version numbers may have multiple dots: https://github.com/goblint/cil/pull/171#issuecomment-2250670652
+void bar(void) __attribute__((availability(macos,introduced=10.13.4)));
+
+void bar(void) {
+    return;
+}

test/small2/kernel1.c

@@ -1,4 +1,4 @@
-
+// This test is nonsense: DECLARE_WAIT_QUEUE_HEAD is a macro in Linux kernel
 DECLARE_WAIT_QUEUE_HEAD(log_wait);
 
 

test/testcil.pl

@@ -222,6 +222,7 @@ sub addToGroup {
 addTest("test/attr11 _GNUCC=1");
 addTest("test/attr12 _GNUCC=1");
 addTest("test/attr13 _GNUCC=1");
+# addTest("test/attr-assign"); # 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");
@@ -657,7 +658,7 @@ sub addToGroup {
 addBadComment("scott/globalprob", "Notbug. Not a bug if fails on a non-Linux machine ;-)");
 addTest("scott/bisonerror $gcc");
 addTest("scott/cmpzero");
-addTest("scott/kernel1 $gcc");
+# addTest("scott/kernel1 $gcc");
 addTest("scott/kernel2 $gcc");
 addTest("scott/xcheckers $gcc");
 addTest("scott/memberofptr $gcc");