From 7e85e55aa89f6652e18e7c3780f1686d0414896f Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Thu, 16 Jan 2020 10:58:50 +0100
Subject: [PATCH] Ensure complex  have the correct fkind rather than having the
 "complex" attribute

And also check this in check.ml
---
 src/check.ml           |  5 ++++-
 src/cil.ml             |  9 +++++++++
 src/cil.mli            |  3 +++
 src/frontc/cabs2cil.ml | 27 ++++++++++++++++-----------
 4 files changed, 32 insertions(+), 12 deletions(-)

diff --git a/src/check.ml b/src/check.ml
index 050eecd4f..12eba9005 100644
--- a/src/check.ml
+++ b/src/check.ml
@@ -237,7 +237,10 @@ let rec checkType (t: typ) (ctx: ctxType) =
   match t with
     (TVoid a | TBuiltin_va_list a) -> checkAttributes a
   | TInt (ik, a) -> checkAttributes a
-  | TFloat (_, a) -> checkAttributes a
+  | TFloat (_, a) ->
+      checkAttributes a;
+      if hasAttribute "complex" a then
+        E.s (E.bug "float type has attribute complex, this should never be the case as there are fkinds for this");
   | TPtr (t, a) -> checkAttributes a;  checkType t CTPtr
 
   | TNamed (ti, a) ->
diff --git a/src/cil.ml b/src/cil.ml
index db6641646..7009d66fb 100755
--- a/src/cil.ml
+++ b/src/cil.ml
@@ -1614,6 +1614,15 @@ let typeOfReal t =
     TFloat (newfkind fkind, newattrs)
   | _ -> E.s (E.bug "unexpected non-numerical type for argument to __real__")
 
+(** for an fkind, return the corresponding complex fkind *)
+let getComplexFkind = function
+  | FFloat -> FComplexFloat
+  | FDouble -> FComplexDouble
+  | FLongDouble -> FComplexLongDouble
+  | FComplexFloat -> FComplexFloat
+  | FComplexDouble -> FComplexDouble
+  | FComplexLongDouble -> FComplexLongDouble
+
 let var vi : lval = (Var vi, NoOffset)
 (* let assign vi e = Instrs(Set (var vi, e), lu) *)
 
diff --git a/src/cil.mli b/src/cil.mli
index c332b220c..b7a1aa7ee 100644
--- a/src/cil.mli
+++ b/src/cil.mli
@@ -1327,6 +1327,9 @@ val isVoidPtrType: typ -> bool
 (** for numerical __complex types return type of corresponding real part *)
 val typeOfReal: typ -> typ
 
+(** for an fkind, return the corresponding complex fkind *)
+val getComplexFkind: fkind -> fkind
+
 (** int *)
 val intType: typ
 
diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml
index 90f420087..829d9796f 100644
--- a/src/frontc/cabs2cil.ml
+++ b/src/frontc/cabs2cil.ml
@@ -1496,9 +1496,9 @@ let cabsTypeAddAttributes a0 t =
           t
     | _ ->
         (* anything else: add a0 to existing attributes *)
-          let add (a: attributes) = cabsAddAttributes a0 a in
+          let addA0To (a: attributes) = cabsAddAttributes a0 a in
           match t with
-            TVoid a -> TVoid (add a)
+            TVoid a -> TVoid (addA0To a)
           | TInt (ik, a) ->
               (* Here we have to watch for the mode attribute *)
 (* sm: This stuff is to handle a GCC extension where you can request integers*)
@@ -1512,7 +1512,7 @@ let cabsTypeAddAttributes a0 t =
 (* A consequence of this handling is that we throw away the mode          *)
 (* attribute, which we used to go out of our way to avoid printing anyway.*)
 (* DG: Use machine model to pick correct type                             *)
-              let ik', a0' =
+              let ik', a0' = begin
                 (* Go over the list of new attributes and come back with a
                  * filtered list and a new integer kind *)
                 List.fold_left
@@ -1544,17 +1544,22 @@ let cabsTypeAddAttributes a0 t =
                     | _ -> (ik', a0one :: a0'))
                   (ik, [])
                   a0
+      end
               in
               TInt (ik', cabsAddAttributes a0' a)
 
-          | TFloat (fk, a) -> TFloat (fk, add a)
-          | TEnum (enum, a) -> TEnum (enum, add a)
-          | TPtr (t, a) -> TPtr (t, add a)
-          | TArray (t, l, a) -> TArray (t, l, add a)
-          | TFun (t, args, isva, a) -> TFun(t, args, isva, add a)
-          | TComp (comp, a) -> TComp (comp, add a)
-          | TNamed (t, a) -> TNamed (t, add a)
-          | TBuiltin_va_list a -> TBuiltin_va_list (add a)
+          | TFloat (fk, a) ->
+            if Cil.hasAttribute "complex" a0 then
+              TFloat (Cil.getComplexFkind fk, cabsAddAttributes (Cil.dropAttribute "complex" a0) a)
+            else
+              TFloat (fk, addA0To a)
+          | TEnum (enum, a) -> TEnum (enum, addA0To a)
+          | TPtr (t, a) -> TPtr (t, addA0To a)
+          | TArray (t, l, a) -> TArray (t, l, addA0To a)
+          | TFun (t, args, isva, a) -> TFun(t, args, isva, addA0To a)
+          | TComp (comp, a) -> TComp (comp, addA0To a)
+          | TNamed (t, a) -> TNamed (t, addA0To a)
+          | TBuiltin_va_list a -> TBuiltin_va_list (addA0To a)
   end