Add PointerConversion castkind

Author: sim642

src/cil.ml

@@ -621,6 +621,7 @@ and castkind =
   | DefaultArgumentPromotion
   | ArithmeticConversion
   | ConditionalConversion (* non-standard terminology *)
+  | PointerConversion (* non-standard terminology *)
   | Unknown (* TODO: eventually remove *)
 
 (** An lvalue denotes the contents of a range of memory addresses. This range
@@ -2887,6 +2888,7 @@ let d_castkind () k =
   | DefaultArgumentPromotion -> text "DefaultArgumentPromotion"
   | ArithmeticConversion -> text "ArithmeticConversion"
   | ConditionalConversion -> text "ConditionalConversion"
+  | PointerConversion -> text "PointerConversion"
   | Unknown -> text "Unknown"
 
 let invalidStmt = mkStmt (Instr [])

src/cil.mli

@@ -730,6 +730,7 @@ and castkind =
   | DefaultArgumentPromotion
   | ArithmeticConversion
   | ConditionalConversion (* non-standard terminology *)
+  | PointerConversion (* non-standard terminology *)
   | Unknown (* TODO: eventually remove *)
 
 (** {b Lvalues.} Lvalues are the sublanguage of expressions that can appear at the left of an assignment or as operand to the address-of operator.

src/expcompare.ml

@@ -238,7 +238,7 @@ let rec stripCastsDeepForPtrArith (e:exp): exp =
       let e2 = stripCastsDeepForPtrArith e2 in
       if not(compareTypesNoAttributes ~ignoreSign:false
 	       (typeOf e1) (typeOf e2))
-      then BinOp(MinusPP, mkCast ~kind:Unknown ~e:e1 ~newt:(typeOf e2), e2, t)
+      then BinOp(MinusPP, mkCast ~kind:PointerConversion ~e:e1 ~newt:(typeOf e2), e2, t)
       else BinOp(MinusPP, e1, e2, t)
   | BinOp(op,e1,e2,t) ->
       let e1 = stripCastsDeepForPtrArith e1 in

src/frontc/cabs2cil.ml

@@ -1471,6 +1471,7 @@ let rec castTo ~kind
     | DefaultArgumentPromotion
     | ArithmeticConversion
     | ConditionalConversion
+    | PointerConversion
     | Unknown -> false
   in
   let debugCast = false in
@@ -5072,8 +5073,8 @@ and doBinOp (bop: binop) (e1: exp) (t1: typ) (e2: exp) (t2: typ) : typ * exp =
     (* Cast both sides to an integer *)
     let commontype = !upointType in
     intType,
-    optConstFoldBinOp false bop (makeCastT ~kind:Unknown ~e:e1 ~oldt:t1 ~newt:commontype)
-      (makeCastT ~kind:Unknown ~e:e2 ~oldt:t2 ~newt:commontype) intType
+    optConstFoldBinOp false bop (makeCastT ~kind:PointerConversion ~e:e1 ~oldt:t1 ~newt:commontype)
+      (makeCastT ~kind:PointerConversion ~e:e2 ~oldt:t2 ~newt:commontype) intType
   in
 
   match bop with
@@ -5106,32 +5107,32 @@ and doBinOp (bop: binop) (e1: exp) (t1: typ) (e2: exp) (t2: typ) : typ * exp =
   | MinusA when isPointerType t1 && isPointerType t2 ->
       let commontype = t1 in
       !ptrdiffType,
-      optConstFoldBinOp false MinusPP (makeCastT ~kind:Unknown ~e:e1 ~oldt:t1 ~newt:commontype)
-                                      (makeCastT ~kind:Unknown ~e:e2 ~oldt:t2 ~newt:commontype) !ptrdiffType
+      optConstFoldBinOp false MinusPP (makeCastT ~kind:PointerConversion ~e:e1 ~oldt:t1 ~newt:commontype)
+                                      (makeCastT ~kind:PointerConversion ~e:e2 ~oldt:t2 ~newt:commontype) !ptrdiffType
   | (Le|Lt|Ge|Gt|Eq|Ne) when isPointerType t1 && isPointerType t2 ->
       pointerComparison e1 t1 e2 t2
   | (Eq|Ne) when isPointerType t1 && isZero e2 ->
-      pointerComparison e1 t1 (makeCastT ~kind:Unknown ~e:zero ~oldt:!upointType ~newt:t1) t1
+      pointerComparison e1 t1 (makeCastT ~kind:PointerConversion ~e:zero ~oldt:!upointType ~newt:t1) t1
   | (Eq|Ne) when isPointerType t2 && isZero e1 ->
-      pointerComparison (makeCastT ~kind:Unknown ~e:zero ~oldt:!upointType ~newt:t2) t2 e2 t2
+      pointerComparison (makeCastT ~kind:PointerConversion ~e:zero ~oldt:!upointType ~newt:t2) t2 e2 t2
 
   | (Eq|Ne) when isVariadicListType t1 && isZero e2 ->
       ignore (warnOpt "Comparison of va_list and zero");
-      pointerComparison e1 t1 (makeCastT ~kind:Unknown ~e:zero ~oldt:!upointType ~newt:t1) t1
+      pointerComparison e1 t1 (makeCastT ~kind:PointerConversion ~e:zero ~oldt:!upointType ~newt:t1) t1
   | (Eq|Ne) when isVariadicListType t2 && isZero e1 ->
       ignore (warnOpt "Comparison of zero and va_list");
-      pointerComparison (makeCastT ~kind:Unknown ~e:zero ~oldt:!upointType ~newt:t2) t2 e2 t2
+      pointerComparison (makeCastT ~kind:PointerConversion ~e:zero ~oldt:!upointType ~newt:t2) t2 e2 t2
 
   | (Eq|Ne|Le|Lt|Ge|Gt) when isPointerType t1 && isArithmeticType t2 ->
       ignore (warnOpt "Comparison of pointer and non-pointer");
       (* Cast both values to upointType *)
-      doBinOp bop (makeCastT ~kind:Unknown ~e:e1 ~oldt:t1 ~newt:!upointType) !upointType
-                  (makeCastT ~kind:Unknown ~e:e2 ~oldt:t2 ~newt:!upointType) !upointType
+      doBinOp bop (makeCastT ~kind:PointerConversion ~e:e1 ~oldt:t1 ~newt:!upointType) !upointType
+                  (makeCastT ~kind:PointerConversion ~e:e2 ~oldt:t2 ~newt:!upointType) !upointType
   | (Eq|Ne|Le|Lt|Ge|Gt) when isArithmeticType t1 && isPointerType t2 ->
       ignore (warnOpt "Comparison of pointer and non-pointer");
       (* Cast both values to upointType *)
-      doBinOp bop (makeCastT ~kind:Unknown ~e:e1 ~oldt:t1 ~newt:!upointType) !upointType
-                  (makeCastT ~kind:Unknown ~e:e2 ~oldt:t2 ~newt:!upointType) !upointType
+      doBinOp bop (makeCastT ~kind:PointerConversion ~e:e1 ~oldt:t1 ~newt:!upointType) !upointType
+                  (makeCastT ~kind:PointerConversion ~e:e2 ~oldt:t2 ~newt:!upointType) !upointType
 
   | _ -> E.s (error "Invalid operands to binary operator: %a" d_plainexp (BinOp(bop,e1,e2,intType)))