Add separate pconst attribute for tracking whether to print const

Normal const attribute will be preseved (not stripped from locals), such that type compatibility (e.g. for generic) is still correct.
Must print some consts because otherwise the whole testing framework fails since it assumes CIL will keep some consts for GCC.

Author: sim642

src/check.ml

@@ -208,6 +208,7 @@ let typeSigIgnoreConst (t : typ) : typsig =
   let attrFilter (attr : attribute) : bool =
     match attr with
       | Attr ("const", []) -> false
+      | Attr ("pconst", []) -> false
       | _ -> true
   in
   typeSigWithAttrs (List.filter attrFilter) t

src/cil.ml

@@ -1275,7 +1275,7 @@ let charType = TInt(IChar, [])
 let boolType = TInt(IBool, [])
 
 let charPtrType = TPtr(charType,[])
-let charConstPtrType = TPtr(TInt(IChar, [Attr("const", [])]),[])
+let charConstPtrType = TPtr(TInt(IChar, [Attr("const", []); Attr("pconst", [])]),[])
 let stringLiteralType = charPtrType
 
 let voidPtrType = TPtr(voidType, [])
@@ -2989,7 +2989,7 @@ let initGccBuiltins () : unit =
   let ulongLongType = TInt(IULongLong, []) in
   let floatType = TFloat(FFloat, []) in
   let longDoubleType = TFloat (FLongDouble, []) in
-  let voidConstPtrType = TPtr(TVoid [Attr ("const", [])], []) in
+  let voidConstPtrType = TPtr(TVoid [Attr ("const", []); Attr ("pconst", [])], []) in
   let sizeType = !typeOfSizeOf in
   let v4sfType = TFloat (FFloat,[Attr("__vector_size__", [AInt 16])]) in
 
@@ -4428,7 +4428,7 @@ class defaultCilPrinterClass : cilPrinter = object (self)
 
     | TArray (elemt, lo, a) ->
         (* ignore the const attribute for arrays *)
-        let a' = dropAttributes [ "const" ] a in
+        let a' = dropAttributes [ "pconst" ] a in
         let name' =
           if a' == [] then name else
           if nameOpt == None then printAttributes a' else
@@ -4496,7 +4496,8 @@ class defaultCilPrinterClass : cilPrinter = object (self)
   method pAttr (Attr(an, args): attribute) : doc * bool =
     (* Recognize and take care of some known cases *)
     match an, args with
-      "const", [] -> text "const", false
+      "const", [] -> nil, false (* don't print const directly, because of split local declarations *)
+    | "pconst", [] -> text "const", false (* pconst means print const *)
           (* Put the aconst inside the attribute list *)
     | "complex", [] when !c99Mode -> text "_Complex", false
     | "complex", [] when not !msvcMode -> text "__complex__", false
@@ -5068,7 +5069,7 @@ let makeVarinfo global name ?init typ =
     { vname = name;
       vid   = newVID ();
       vglob = global;
-      vtype = if global then typ else typeRemoveAttributes ["const"] typ;
+      vtype = if global then typ else typeRemoveAttributes ["pconst"] typ;
       vdecl = lu;
       vinit = {init=init};
       vinline = false;

src/frontc/cabs2cil.ml

@@ -616,8 +616,8 @@ let alphaConvertVarAndAddToEnv (addtoenv: bool) (vi: varinfo) : varinfo =
  * elements. *)
 let rec stripConstLocalType (t: typ) : typ =
   let dc a =
-    if hasAttribute "const" a then
-      dropAttribute "const" a
+    if hasAttribute "pconst" a then
+      dropAttribute "pconst" a
     else a
   in
   match t with
@@ -2670,7 +2670,7 @@ let rec doSpecList (suggestedAnonName: string) (* This string will be part of
 and convertCVtoAttr (src: A.cvspec list) : A.attribute list =
   match src with
   | [] -> []
-  | CV_CONST    :: tl -> ("const",[])    :: (convertCVtoAttr tl)
+  | CV_CONST    :: tl -> ("const",[]) :: ("pconst",[])    :: (convertCVtoAttr tl)
   | CV_VOLATILE :: tl -> ("volatile",[]) :: (convertCVtoAttr tl)
   | CV_RESTRICT :: tl -> ("restrict",[]) :: (convertCVtoAttr tl)
   | CV_COMPLEX  :: tl -> ("complex",[]) ::  (convertCVtoAttr tl)

src/mergecil.ml

@@ -820,8 +820,10 @@ let oneFilePass1 (f:file) : unit =
        * can happen if one file declares the variable a non-const while
        * others declare it as "const". *)
       if hasAttribute "const" (typeAttrs vi.vtype) !=
-         hasAttribute "const" (typeAttrs oldvi.vtype) then begin
-        newrep.ndata.vtype <- typeRemoveAttributes ["const"] newtype;
+         hasAttribute "const" (typeAttrs oldvi.vtype) ||
+         hasAttribute "pconst" (typeAttrs vi.vtype) !=
+         hasAttribute "pconst" (typeAttrs oldvi.vtype) then begin
+        newrep.ndata.vtype <- typeRemoveAttributes ["const"; "pconst"] newtype;
       end else begin
         newrep.ndata.vtype <- newtype;
       end;