diff --git a/src/check.ml b/src/check.ml index 1fc37396f..d8ff57f4f 100644 --- a/src/check.ml +++ b/src/check.ml @@ -601,7 +601,8 @@ and checkExp (isconst: bool) (e: exp) : typ = | _ -> E.s (bug "StartOf on a non-array") end - | CastE (tres, e) -> begin + | CastE (_, tres, e) -> begin + (* TODO: check castkind w.r.t. tres? *) let et = checkExp isconst e in checkType tres CTExp; (* Not all types can be cast *) diff --git a/src/cil.ml b/src/cil.ml index cb49cca8f..d1d3edc78 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -535,7 +535,7 @@ and exp = | Question of exp * exp * exp * typ (** (a ? b : c) operation. Includes the type of the result *) - | CastE of typ * exp (** Use {!mkCast} to make casts *) + | CastE of castkind * typ * exp (** Use {!mkCast} to make casts *) | AddrOf of lval (** Always use {!mkAddrOf} to construct one of these. Apply to an @@ -615,8 +615,15 @@ and binop = | LAnd (** logical and *) | LOr (** logical or *) - - +and castkind = + | Explicit (** Explicit conversion. @see C11 6.3.1. *) + | IntegerPromotion (** Integer promotion. @see C11 6.3.1.1.2. *) + | DefaultArgumentPromotion (** Default argument promotion. @see C11 6.5.2.2.6. *) + | ArithmeticConversion (** Usual arithmetic conversion. @see C11 6.3.1.8. *) + | ConditionalConversion (** Conditional conversion (non-standard terminology). @see C11 6.5.15.5 and 6.5.15.6. *) + | PointerConversion (** Pointer conversion (non-standard). @see C11 6.5.6.8, 6.5.8.5 and 6.5.9.5. *) + | Implicit (** Implicit conversion. @see C11 6.3.1, 6.5.2.2.7, 6.5.2.4.2, 6.5.16.1.2, 6.5.16.2.3, 6.7.9.11, 6.8.4.2.5 and 6.8.6.4.3. *) + | Internal (** CIL-internal conversion (non-standard). *) (** An lvalue denotes the contents of a range of memory addresses. This range is denoted as a host object along with an offset within the object. The @@ -1729,7 +1736,7 @@ let mkForIncr ~(iter : varinfo) ~(first: exp) ~stopat:(past: exp) ~(incr: exp) let rec stripCasts (e: exp) = - match e with CastE(_, e') -> stripCasts e' | _ -> e + match e with CastE(_, _, e') -> stripCasts e' | _ -> e @@ -1909,7 +1916,7 @@ let getParenthLevel (e: exp) = (* Unary *) | Real _ -> 30 | Imag _ -> 30 - | CastE(_,_) -> 30 + | CastE(_,_,_) -> 30 | AddrOf(_) -> 30 | AddrOfLabel(_) -> 30 | StartOf(_) -> 30 @@ -1991,7 +1998,7 @@ let rec typeOf (e: exp) : typ = | UnOp (_, _, t) | BinOp (_, _, _, t) | Question (_, _, _, t) - | CastE (t, _) -> t + | CastE (_, t, _) -> t | AddrOf (lv) -> TPtr(typeOfLval lv, []) | AddrOfLabel (lv) -> voidPtrType | StartOf (lv) -> begin @@ -2215,7 +2222,7 @@ let rec getInteger (e:exp) : cilint option = | Const(CInt (n, ik, _)) -> Some (mkCilintIk ik n) | Const(CChr c) -> getInteger (Const (charConstToInt c)) | Const(CEnum(v, _, _)) -> getInteger v - | CastE(t, e) -> begin + | CastE(_, t, e) -> begin (* Handle any truncation due to cast. We optimistically ignore loss-of-precision due to floating-point casts. *) let mkInt ik n = Some (fst (truncateCilint ik n)) in @@ -2622,19 +2629,19 @@ and constFold (machdep: bool) (e: exp) : exp = | _ -> constFold machdep (AlignOf (typeOf e)) end - | CastE(it, - AddrOf (Mem (CastE(TPtr(bt, _), z)), off)) + | CastE (k, it, + AddrOf (Mem (CastE(_, TPtr(bt, _), z)), off)) when machdep && isZero z -> begin try let start, width = bitsOffset bt off in if start mod 8 <> 0 then E.s (error "Using offset of bitfield"); - constFold machdep (CastE(it, (kinteger !kindOfSizeOf (start / 8)))) + constFold machdep (CastE(k, it, (kinteger !kindOfSizeOf (start / 8)))) with SizeOfError _ -> e end - | CastE (t, e) -> begin + | CastE (k, t, e) -> begin match constFold machdep e, unrollType t with (* Might truncate silently *) | Const(CInt(i,k,_)), TInt(nk,a) @@ -2643,7 +2650,7 @@ and constFold (machdep: bool) (e: exp) : exp = when (dropAttributes ["const"; "pconst"] a) = [] -> let i', _ = truncateCilint nk (mkCilintIk k i) in Const(CInt(i', nk, None)) - | e', _ -> CastE (t, e') + | e', _ -> CastE (k, t, e') end | Lval lv -> Lval (constFoldLval machdep lv) | AddrOf lv -> AddrOf (constFoldLval machdep lv) @@ -2765,7 +2772,7 @@ let isArrayType t = An integer constant expr with value 0, or such an expr cast to void *, is called a null pointer constant. *) let isNullPtrConstant e = let rec isNullPtrConstant = function - | CastE (TPtr (TVoid [], []), e) -> isNullPtrConstant e (* no qualifiers allowed on void or ptr *) + | CastE (_, TPtr (TVoid [], []), e) -> isNullPtrConstant e (* no qualifiers allowed on void or ptr *) | e -> isZero e in isNullPtrConstant (constFold true e) @@ -2781,7 +2788,7 @@ let rec isConstant = function | Real e -> isConstant e | Imag e -> isConstant e | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ -> true - | CastE (_, e) -> isConstant e + | CastE (_, _, e) -> isConstant e | AddrOf (Var vi, off) | StartOf (Var vi, off) -> vi.vglob && isConstantOffset off | AddrOf (Mem e, off) | StartOf(Mem e, off) @@ -2875,6 +2882,17 @@ let d_binop () b = | LAnd -> text "&&" | LOr -> text "||" +let d_castkind () k = + match k with + | Explicit -> text "Explicit" + | IntegerPromotion -> text "IntegerPromotion" + | DefaultArgumentPromotion -> text "DefaultArgumentPromotion" + | ArithmeticConversion -> text "ArithmeticConversion" + | ConditionalConversion -> text "ConditionalConversion" + | PointerConversion -> text "PointerConversion" + | Implicit -> text "Implicit" + | Internal -> text "Internal" + let invalidStmt = mkStmt (Instr []) (** Construct a hash with the builtins *) @@ -3405,9 +3423,12 @@ class defaultCilPrinterClass : cilPrinter = object (self) ++ text " : " ++ (self#pExpPrec level () e3) - | CastE(t,e) -> + | CastE(k,t,e) -> text "(" - ++ self#pType None () t + ++ self#pType None () t (* TODO: option to not print implicit casts? *) + (* ++ text "/*" + ++ d_castkind () k (* convenient for debugging castkinds *) + ++ text "*/" *) ++ text ")" ++ self#pExpPrec level () e @@ -3698,7 +3719,7 @@ class defaultCilPrinterClass : cilPrinter = object (self) in let patchArgNotUseVLACast exp = match exp with - | CastE(t, e) -> CastE(patchTypeNotVLA t, e) + | CastE(k, t, e) -> CastE(k, patchTypeNotVLA t, e) | e -> e in self#pLineDirective l @@ -4698,7 +4719,7 @@ class plainCilPrinterClass = ++ unalign) ++ text ")" - | CastE(t,e) -> dprintf "CastE(@[%a,@?%a@])" self#pOnlyType t self#pExp e + | CastE(k,t,e) -> dprintf "CastE(@[%a,@?%a,@?%a@])" d_castkind k self#pOnlyType t self#pExp e | UnOp(u,e1,_) -> dprintf "UnOp(@[%a,@?%a@])" @@ -5242,9 +5263,9 @@ and childrenExp (vis: cilVisitor) (e: exp) : exp = | Question (e1, e2, e3, t) -> let e1' = vExp e1 in let e2' = vExp e2 in let e3' = vExp e3 in let t' = vTyp t in if e1' != e1 || e2' != e2 || e3' != e3 || t' != t then Question(e1',e2',e3',t') else e - | CastE (t, e1) -> + | CastE (k, t, e1) -> let t' = vTyp t in let e1' = vExp e1 in - if t' != t || e1' != e1 then CastE(t', e1') else e + if t' != t || e1' != e1 then CastE(k, t', e1') else e | AddrOf lv -> let lv' = vLval lv in if lv' != lv then AddrOf lv' else e @@ -6097,7 +6118,7 @@ let getCompField (cinfo:compinfo) (fieldName:string) : fieldinfo = (List.find (fun fi -> fi.fname = fieldName) cinfo.cfields) -let mkCastT ~(e: exp) ~(oldt: typ) ~(newt: typ) = +let mkCastT ~(kind: castkind) ~(e: exp) ~(oldt: typ) ~(newt: typ) = (* Do not remove old casts because they are conversions !!! *) if Util.equals (typeSig oldt) (typeSig newt) then begin e @@ -6109,11 +6130,11 @@ let mkCastT ~(e: exp) ~(oldt: typ) ~(newt: typ) = let v = if compare i zero_cilint = 0 then zero_cilint else one_cilint in Const (CInt(v, IBool, None)) | TInt(newik, []), Const(CInt(i, _, _)) -> kintegerCilint newik i - | _ -> CastE(newt,e) + | _ -> CastE(kind,newt,e) end -let mkCast ~(e: exp) ~(newt: typ) = - mkCastT ~e:e ~oldt:(typeOf e) ~newt:newt +let mkCast ~kind ~(e: exp) ~(newt: typ) = + mkCastT ~kind ~e:e ~oldt:(typeOf e) ~newt:newt type existsAction = ExistsTrue (* We have found it *) @@ -6230,7 +6251,7 @@ let rec makeZeroInit (t: typ) : init = CompoundInit (t', []) | TPtr _ as t -> - SingleInit(if !insertImplicitCasts then mkCast ~e:zero ~newt:t else zero) + SingleInit(if !insertImplicitCasts then mkCast ~kind:Internal ~e:zero ~newt:t else zero) | x -> E.s (unimp "Cannot initialize type: %a" d_type x) diff --git a/src/cil.mli b/src/cil.mli index edbb092d3..ae19de994 100644 --- a/src/cil.mli +++ b/src/cil.mli @@ -617,7 +617,7 @@ and exp = | Question of exp * exp * exp * typ (** (a ? b : c) operation. Includes the type of the result *) - | CastE of typ * exp + | CastE of castkind * typ * exp (** Use {!mkCast} to make casts. *) | AddrOf of lval @@ -724,6 +724,16 @@ and binop = you want to use these, you must set {!useLogicalOperators}. *) +and castkind = + | Explicit (** Explicit conversion. @see C11 6.3.1. *) + | IntegerPromotion (** Integer promotion. @see C11 6.3.1.1.2. *) + | DefaultArgumentPromotion (** Default argument promotion. @see C11 6.5.2.2.6. *) + | ArithmeticConversion (** Usual arithmetic conversion. @see C11 6.3.1.8. *) + | ConditionalConversion (** Conditional conversion (non-standard terminology). @see C11 6.5.15.5 and 6.5.15.6. *) + | PointerConversion (** Pointer conversion (non-standard). @see C11 6.5.6.8, 6.5.8.5 and 6.5.9.5. *) + | Implicit (** Implicit conversion. @see C11 6.3.1, 6.5.2.2.7, 6.5.2.4.2, 6.5.16.1.2, 6.5.16.2.3, 6.7.9.11, 6.8.4.2.5 and 6.8.6.4.3. *) + | Internal (** CIL-internal conversion (non-standard). *) + (** {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. In C the syntax for lvalues is not always a good indication of the meaning of the lvalue. For example the C value @@ -1717,10 +1727,10 @@ val mkString: string -> exp (** Construct a cast when having the old type of the expression. If the new type is the same as the old type, then no cast is added. *) -val mkCastT: e:exp -> oldt:typ -> newt:typ -> exp +val mkCastT: kind:castkind -> e:exp -> oldt:typ -> newt:typ -> exp (** Like {!mkCastT} but uses typeOf to get [oldt] *) -val mkCast: e:exp -> newt:typ -> exp +val mkCast: kind:castkind -> e:exp -> newt:typ -> exp (** Removes casts from this expression, but ignores casts within other expression constructs. So we delete the (A) and (B) casts from @@ -2386,6 +2396,9 @@ val d_binop: unit -> binop -> Pretty.doc (** Pretty-print a unary operator *) val d_unop: unit -> unop -> Pretty.doc +(** Pretty-print a cast kind *) +val d_castkind: unit -> castkind -> Pretty.doc + (** Pretty-print an attribute using {!defaultCilPrinter} *) val d_attr: unit -> attribute -> Pretty.doc diff --git a/src/expcompare.ml b/src/expcompare.ml index 02b156202..6bc0cbd78 100644 --- a/src/expcompare.ml +++ b/src/expcompare.ml @@ -57,8 +57,8 @@ let rec compareExp (e1: exp) (e2: exp) : bool = | AddrOf lv1, AddrOf lv2 -> compareLval lv1 lv2 | BinOp(bop1, l1, r1, _), BinOp(bop2, l2, r2, _) -> bop1 = bop2 && compareExp l1 l2 && compareExp r1 r2 - | CastE(t1, e1), CastE(t2, e2) -> - t1 == t2 && compareExp e1 e2 + | CastE(k1, t1, e1), CastE(k2, t2, e2) -> + k1 = k2 && t1 == t2 && compareExp e1 e2 | _ -> begin match getInteger (constFold true e1), getInteger (constFold true e2) with Some i1, Some i2 -> compare_cilint i1 i2 = 0 @@ -95,7 +95,7 @@ and compareLval (lv1: lval) (lv2: lval) : bool = since they actually change the value of the expression. *) let rec stripNopCasts (e:exp): exp = match e with - CastE(t, e') -> begin + CastE(_, t, e') -> begin match unrollType (typeOf e'), unrollType t with TPtr (bt1, a1), TPtr (bt2, a2) when isConstType bt1 = isConstType bt2 -> @@ -127,7 +127,7 @@ let compareExpStripCasts (e1: exp) (e2: exp) : bool = of pointer arithmetic shouldn't change the resulting value. *) let rec stripCastsForPtrArith (e:exp): exp = match e with - | CastE(t, e') -> begin + | CastE(_, t, e') -> begin match unrollType (typeOf e'), unrollType t with (* Keep casts from void to something else. Among other things, we keep casts from void* to char* that would otherwise be @@ -209,7 +209,7 @@ let isTypeVolatile t = (* strip every cast between equal pointer types *) let rec stripCastsDeepForPtrArith (e:exp): exp = match e with - | CastE(t, e') when not(isTypeVolatile t) -> begin + | CastE(k, t, e') when not(isTypeVolatile t) -> begin let e' = stripCastsDeepForPtrArith e' in match unrollType (typeOf e'), unrollType t with (* Keep casts from void to something else. Among other things, @@ -224,11 +224,11 @@ let rec stripCastsDeepForPtrArith (e:exp): exp = isConstType bt1 = isConstType bt2 then e' else - CastE(t,e') + CastE(k,t,e') with SizeOfError _ -> (* bt1 or bt2 is abstract; don't strip. *) - CastE(t,e') + CastE(k,t,e') end - | _, _ -> CastE(t,e') + | _, _ -> CastE(k,t,e') end | UnOp(op,e,t) -> let e = stripCastsDeepForPtrArith e in @@ -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 ~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 diff --git a/src/ext/dataslicing/dataslicing.ml b/src/ext/dataslicing/dataslicing.ml index 3d9da12fd..2559e09fa 100644 --- a/src/ext/dataslicing/dataslicing.ml +++ b/src/ext/dataslicing/dataslicing.ml @@ -234,13 +234,13 @@ and sliceExp (i : int) (e : exp) : exp = | UnOp (op, e1, t) -> UnOp (op, sliceExp i e1, sliceType i t) | BinOp (op, e1, e2, t) -> BinOp (op, sliceExp i e1, sliceExp i e2, sliceType i t) - | CastE (t, e) -> sliceCast i t e + | CastE (k, t, e) -> sliceCast i k t e | AddrOf lv -> AddrOf (sliceLval i lv) | StartOf lv -> StartOf (sliceLval i lv) | SizeOf t -> SizeOf (sliceTypeAll t) | _ -> E.s (unimp "exp %a" d_exp e) -and sliceCast (i : int) (t : typ) (e : exp) : exp = +and sliceCast (i : int) (k : castkind) (t : typ) (e : exp) : exp = let te = typeOf e in match t, te with | TInt (k1, _), TInt (k2, attrs2) when k1 = k2 -> @@ -250,9 +250,9 @@ and sliceCast (i : int) (t : typ) (e : exp) : exp = (* Note: We strip off integer cast operations. *) sliceExp i e | TPtr _, _ when isZero e -> - CastE (sliceType i t, sliceExp i e) + CastE (k, sliceType i t, sliceExp i e) | TPtr (bt1, _), TPtr (bt2, _) when (typeSig bt1) = (typeSig bt2) -> - CastE (sliceType i t, sliceExp i e) + CastE (k, sliceType i t, sliceExp i e) | _ -> E.s (unimp "sketchy cast (%a) -> (%a)\n" d_type te d_type t) diff --git a/src/ext/pta/ptranal.ml b/src/ext/pta/ptranal.ml index cb9df89d3..8c6c40024 100644 --- a/src/ext/pta/ptranal.ml +++ b/src/ext/pta/ptranal.ml @@ -244,7 +244,7 @@ and analyze_expr (e : exp ) : A.tau = | UnOp (op, e, t) -> analyze_expr e | BinOp (op, e, e', t) -> A.join (analyze_expr e) (analyze_expr e') | Question (_, e, e', _) -> A.join (analyze_expr e) (analyze_expr e') - | CastE (t, e) -> analyze_expr e + | CastE (_, t, e) -> analyze_expr e | AddrOf l -> if !fun_ptrs_as_funs && isFunctionType (typeOfLval l) then A.rvalue (analyze_lval l) diff --git a/src/ext/zrapp/rmciltmps.ml b/src/ext/zrapp/rmciltmps.ml index dad6dce77..1c512d7cc 100644 --- a/src/ext/zrapp/rmciltmps.ml +++ b/src/ext/zrapp/rmciltmps.ml @@ -429,7 +429,7 @@ let varXformClass action data sid fd nofrm = object(self) None -> DoChildren | Some e' -> (* Cast e' to the correct type. *) - let e'' = mkCast ~e:e' ~newt:vi.vtype in + let e'' = mkCast ~kind:Internal ~e:e' ~newt:vi.vtype in ChangeTo e'') | Lval(Mem e', off) -> (* don't substitute constants in memory lvals *) @@ -468,7 +468,7 @@ let lvalXformClass action data sid fd nofrm = object(self) in ChangeDoChildrenPost(Lval(Mem e', off), post) | Some e' -> - let e'' = mkCast ~e:e' ~newt:(typeOf(Lval lv)) in + let e'' = mkCast ~kind:Internal ~e:e' ~newt:(typeOf(Lval lv)) in ChangeDoChildrenPost(e'', castrm) end | Lval lv -> begin @@ -476,7 +476,7 @@ let lvalXformClass action data sid fd nofrm = object(self) | None -> DoChildren | Some e' -> begin (* Cast e' to the correct type. *) - let e'' = mkCast ~e:e' ~newt:(typeOf(Lval lv)) in + let e'' = mkCast ~kind:Internal ~e:e' ~newt:(typeOf(Lval lv)) in ChangeDoChildrenPost(e'', castrm) end end @@ -494,7 +494,7 @@ let iosh_get_useful_def iosh vi = match ido with None -> true | Some(id) -> match time "getDefRhs" getDefRhs id with Some(RD.RDExp(Lval(Var vi',NoOffset)),_,_) - | Some(RD.RDExp(CastE(_,Lval(Var vi',NoOffset))),_,_) -> + | Some(RD.RDExp(CastE(_,_,Lval(Var vi',NoOffset))),_,_) -> not(vi.vid = vi'.vid) (* false if they are the same *) | _ -> true) ios in diff --git a/src/formatcil.ml b/src/formatcil.ml index 70a36173e..444f5b83e 100644 --- a/src/formatcil.ml +++ b/src/formatcil.ml @@ -157,7 +157,7 @@ let test () = (* Construct an instruction *) let makeInstr () = Call(Some (var res), - Lval (Mem (CastE(TPtr(TFun(TPtr(intType, []), + Lval (Mem (CastE(Explicit, TPtr(TFun(TPtr(intType, []), Some [ ("", intType, []); ("a2", TPtr(intType, []), []); ("a3", TPtr(TPtr(intType, []), diff --git a/src/formatparse.mly b/src/formatparse.mly index 494c7f4e9..d4d795190 100644 --- a/src/formatparse.mly +++ b/src/formatparse.mly @@ -504,12 +504,12 @@ expression: { ((fun args -> let t = (fst $2) args in let e = (fst $4) args in - mkCast ~e:e ~newt:t), + mkCast ~kind:Explicit ~e:e ~newt:t), (* C11 6.3.1 *) (fun e -> let t', e' = match e with - CastE (t', e') -> t', e' + CastE (_, t', e') -> t', e' | _ -> typeOf e, e in match (snd $2) t', (snd $4 e') with @@ -1354,7 +1354,7 @@ stmt: let e = (fst $3) args in let e = if isPointerType(typeOf e) then - mkCast ~e:e ~newt:!upointType + mkCast ~kind:Internal ~e:e ~newt:!upointType (* TODO: why this cast here? not done for other ifs/loops *) else e in mkStmt diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index a15eec932..23c22db96 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -1174,7 +1174,7 @@ module BlockChunk = let t = typeOf e in (* If needed, convert e to type t, and check in case the label was too big *) let checkRange e = - let e' = makeCast ~e ~newt:t in + let e' = makeCast ~kind:Implicit ~e ~newt:t in (* C11 6.8.4.2.5 *) let constFold = constFold false in let e'' = if !lowerConstants then constFold e' else e' in begin match (constFold e), (constFold e'') with @@ -1462,8 +1462,19 @@ let arithmeticConversion (* c.f. ISO 6.3.1.8 *) (* Specify whether the cast is from the source code *) -let rec castTo ?(fromsource=false) +let rec castTo ~kind (ot : typ) (nt : typ) (e : exp) : (typ * exp ) = + let fromsource = + match kind with + | Explicit -> true + | IntegerPromotion + | DefaultArgumentPromotion + | ArithmeticConversion + | ConditionalConversion + | PointerConversion + | Implicit + | Internal -> false + in let debugCast = false in if debugCast then ignore (E.log "%t: castTo:%s %a->%a\n" @@ -1478,7 +1489,7 @@ let rec castTo ?(fromsource=false) else begin let nt' = if fromsource then nt else !typeForInsertedCast nt in let result = (nt', - if !insertImplicitCasts || fromsource then Cil.mkCastT ~e:e ~oldt:ot ~newt:nt' else e) in + if !insertImplicitCasts || fromsource then Cil.mkCastT ~kind ~e:e ~oldt:ot ~newt:nt' else e) in if debugCast then ignore (E.log "castTo: ot=%a nt=%a\n result is %a\n" @@ -1558,7 +1569,7 @@ let rec castTo ?(fromsource=false) | _ -> E.s (unimp "castTo: transparent union expression is not an lval: %a\n" d_exp e) in (* Continue casting *) - castTo ~fromsource:fromsource fstfield.ftype nt' e' + castTo ~kind fstfield.ftype nt' e' end end | _ -> @@ -1586,7 +1597,7 @@ let rec isConstTrue (e:exp): bool = | Const(CChr c) -> 0 <> Char.code c | Const(CStr _ | CWStr _) -> true | Const(CReal(f, _, _)) -> f <> 0.0; - | CastE(_, e) -> isConstTrue e + | CastE(_, _, e) -> isConstTrue e | _ -> false (* Given an expression that is being coerced to bool, is it zero? @@ -1597,7 +1608,7 @@ let rec isConstFalse (e:exp): bool = | Const(CInt (n,_,_)) -> is_zero_cilint n | Const(CChr c) -> 0 = Char.code c | Const(CReal(f, _, _)) -> f = 0.0; - | CastE(_, e) -> isConstFalse e + | CastE(_, _, e) -> isConstFalse e | _ -> false @@ -1830,7 +1841,7 @@ let rec combineTypes (what: combineWhat) (oldt: typ) (t: typ) : typ = (* cast both to the same type. This prevents complaints such as "((int)1) <> ((char)1)" *) if machdep then - mkCast ~e:oldsz' ~newt:!typeOfSizeOf, mkCast ~e:sz' ~newt:!typeOfSizeOf + mkCast ~kind:Internal ~e:oldsz' ~newt:!typeOfSizeOf, mkCast ~kind:Internal ~e:sz' ~newt:!typeOfSizeOf else oldsz', sz' in @@ -2399,7 +2410,7 @@ let afterConversion (c: chunk) : chunk = is important to have the cast at the same place as the call *) let collapseCallCast = function Call(Some(Var vi, NoOffset), f, args, l, el), - Set(destlv, CastE (newt, Lval(Var vi', NoOffset)), _, _) + Set(destlv, CastE (_, newt, Lval(Var vi', NoOffset)), _, _) when (not vi.vglob && String.length vi.vname >= 3 && (* Watch out for the possibility that we have an implied cast in @@ -3461,9 +3472,9 @@ and doExp (asconst: bool) (* This expression is used as a constant *) essentially doExp should never return things of type TFun or TArray *) let processArrayFun e t = match e, unrollType t with - (Lval(lv) | CastE(_, Lval lv)), TArray(tbase, _, a) -> + (Lval(lv) | CastE(_, _, Lval lv)), TArray(tbase, _, a) -> mkStartOfAndMark lv, TPtr(tbase, a) - | (Lval(lv) | CastE(_, Lval lv)), TFun _ -> + | (Lval(lv) | CastE(_, _, Lval lv)), TFun _ -> mkAddrOfAndMark lv, TPtr(t, []) | _, (TArray _ | TFun _) -> E.s (error "Array or function expression is not lval: %a@!" @@ -3495,7 +3506,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *) (SynthetizeLoc.doChunkTail se, e, t) | _ -> let (e', t') = processArrayFun e t in - let (t'', e'') = castTo t' lvt e' in + let (t'', e'') = castTo ~kind:Implicit t' lvt e' in (* C11 6.5.16.1.2 *) (* ignore (E.log "finishExp: e = %a\n e'' = %a\n" d_plainexp e d_plainexp e''); *) @@ -3615,7 +3626,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *) let lv = match e' with Lval x -> x - | CastE(_, Lval x) -> x + | CastE(_, _, Lval x) -> x | _ -> E.s (error "Expected an lval in MEMBEROF (field %s)" str) in let field_offset = @@ -3986,7 +3997,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *) need the check. *) let newtyp, newexp = if needcast then - castTo ~fromsource:true t' typ e' + castTo ~kind:Explicit t' typ e' (* C11 6.3.1 *) else t', e' in @@ -3998,7 +4009,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *) let (se, e', t) = doExp asconst e (AExp None) in if isIntegralType t then let tres = integralPromotion t in - let fallback = UnOp(Neg, makeCastT ~e:e' ~oldt:t ~newt:tres, tres) in + let fallback = UnOp(Neg, makeCastT ~kind:IntegerPromotion ~e:e' ~oldt:t ~newt:tres, tres) in let e'' = match e', tres with | Const(CInt(i, _, _)), TInt(ik, _) -> const_if_not_overflow fallback ik (neg_cilint i) @@ -4015,7 +4026,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *) let (se, e', t) = doExp asconst e (AExp None) in if isIntegralType t then let tres = integralPromotion t in - let e'' = UnOp(BNot, makeCastT ~e:e' ~oldt:t ~newt:tres, tres) in + let e'' = UnOp(BNot, makeCastT ~kind:IntegerPromotion ~e:e' ~oldt:t ~newt:tres, tres) in finishExp se e'' tres else E.s (error "Unary ~ on a non-integral type") @@ -4060,7 +4071,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *) (* ignore (E.log "ADDROF on %a : %a\n" d_plainexp e' d_plaintype t); *) match e' with - ( Lval x | CastE(_, Lval x)) -> + ( Lval x | CastE(_, _, Lval x)) -> finishExp se (mkAddrOfAndMark x) (TPtr(t, [])) | StartOf (lv) -> @@ -4105,13 +4116,13 @@ and doExp (asconst: bool) (* This expression is used as a constant *) let lv = match e' with Lval x -> x - | CastE (_, Lval x) -> x (* A GCC extension. The operation is + | CastE (_, _, Lval x) -> x (* A GCC extension. The operation is done at the cast type. The result is also of the cast type *) | _ -> E.s (error "Expected lval for ++ or --") in let tresult, result = doBinOp uop' e' t one intType in - finishExp (se +++ (Set(lv, makeCastT ~e:result ~oldt:tresult ~newt:t, + finishExp (se +++ (Set(lv, makeCastT ~kind:Implicit ~e:result ~oldt:tresult ~newt:t, (* C11 6.5.2.4.2 *) !currentLoc, !currentExpLoc))) e' t @@ -4142,7 +4153,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *) let lv = match e' with Lval x -> x - | CastE (_, Lval x) -> x (* GCC extension. The addition must + | CastE (_, _, Lval x) -> x (* GCC extension. The addition must be be done at the cast type. The result of this is also of the cast type *) @@ -4159,7 +4170,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *) se, e' in finishExp - (se' +++ (Set(lv, makeCastT ~e:opresult ~oldt:tresult ~newt:(typeOfLval lv), + (se' +++ (Set(lv, makeCastT ~kind:Implicit ~e:opresult ~oldt:tresult ~newt:(typeOfLval lv), (* C11 6.5.2.4.2 *) !currentLoc, !currentExpLoc))) result t @@ -4267,7 +4278,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *) let lv1 = match e1' with Lval x -> x - | CastE (_, Lval x) -> x (* GCC extension. The operation and + | CastE (_, _, Lval x) -> x (* GCC extension. The operation and the result are at the cast type *) | _ -> E.s (error "Expected lval for assignment with arith") in @@ -4275,7 +4286,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *) let tresult, result = doBinOp bop' e1' t1 e2' t2 in (* We must cast the result to the type of the lv1, which may be different than t1 if lv1 was a Cast *) - let tresult', result' = castTo tresult (typeOfLval lv1) result in + let tresult', result' = castTo ~kind:Implicit tresult (typeOfLval lv1) result in (* C11 6.5.16.2.3 *) (* Catch the case of an lval that might depend on itself, e.g. p[p[0]] when p[0] == 0. We need to use a temporary here if the result of the expression will be used: @@ -4317,7 +4328,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *) | CEExp (se, e) -> let e' = let te = typeOf e in - let _, zte = castTo intType te zero in + let _, zte = castTo ~kind:Internal intType te zero in (* TODO: is this even reachable? *) BinOp(Ne, e, zte, intType) in finishExp se e' intType @@ -4406,7 +4417,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *) if isBuiltinNan && asconst then (* Replace call to builtin nan with computation yielding NaN *) let onef = Const(CReal(0.0,FDouble,None)) in - let zerodivzero = mkCast ~e:(BinOp(Div,onef,onef,doubleType)) ~newt:resType in + let zerodivzero = mkCast ~kind:Internal ~e:(BinOp(Div,onef,onef,doubleType)) ~newt:resType in (empty,zerodivzero,resType) else ( (* If the "--forceRLArgEval" flag was used, make sure @@ -4440,7 +4451,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *) test/small1/union5, in which a transparent union is passed as an argument *) let (sa, a', att) = force_right_to_left_evaluation (doExp false a (AExp None)) in - let (_, a'') = castTo att at a' in + let (_, a'') = castTo ~kind:Implicit att at a' in (* C11 6.5.2.2.7 *) (sa :: ss, a'' :: args') | ([], args) -> (* No more types *) (* Do not give a warning for functions without a prototype*) @@ -4458,7 +4469,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *) (sa :: ss, a' :: args') else let promoted_type = defaultArgumentPromotion at in - let _, a'' = castTo at promoted_type a' in + let _, a'' = castTo ~kind:DefaultArgumentPromotion at promoted_type a' in (sa :: ss, a'' :: args') in loop args @@ -4479,7 +4490,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *) let pres: exp ref = ref zero in (* If we do not have a call, this is the result *) let prestype: typ ref = ref intType in - let rec dropCasts = function CastE (_, e) -> dropCasts e | e -> e in + let rec dropCasts = function CastE (_, _, e) -> dropCasts e | e -> e in (* Get the name of the last formal *) let getNameLastFormal () = match !currentFunctionFDEC.svar.vtype with @@ -4746,7 +4757,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *) (* Make an exception here for __builtin_va_arg: hide calldest as a third parameter. *) match calldest with - | Some destlv -> None, !pargs @ [CastE(voidPtrType, AddrOf destlv)] + | Some destlv -> None, !pargs @ [CastE(Internal, voidPtrType, AddrOf destlv)] | None -> E.s (E.bug "__builtin_va_arg should have calldest always set") else calldest, !pargs @@ -4833,31 +4844,34 @@ and doExp (asconst: bool) (* This expression is used as a constant *) let tresult = conditionalConversion t2 t3 e_of_t2 e3' in match ce1 with CEExp (se1, e1') when isConstFalse e1' && canDrop se2 && (!Cil.removeBranchingOnConstants || asconst) -> - finishExp (se1 @@ se3) (snd (castTo t3 tresult e3')) tresult + finishExp (se1 @@ se3) (snd (castTo ~kind:ConditionalConversion t3 tresult e3')) tresult | CEExp (se1, e1') when isConstTrue e1' && canDrop se3 && (!Cil.removeBranchingOnConstants || asconst) -> begin match e2'o with None -> (* use e1' *) - finishExp (se1 @@ se2) (snd (castTo t2 tresult e1')) tresult + finishExp (se1 @@ se2) (snd (castTo ~kind:ConditionalConversion t2 tresult e1')) tresult | Some e2' -> - finishExp (se1 @@ se2) (snd (castTo t2 tresult e2')) tresult + finishExp (se1 @@ se2) (snd (castTo ~kind:ConditionalConversion t2 tresult e2')) tresult end | CEExp (se1, e1') when !useLogicalOperators && isEmpty se2 && isEmpty se3 -> let e2' = match e2'o with None -> (* use e1' *) - snd (castTo t2 tresult e1') + snd (castTo ~kind:ConditionalConversion t2 tresult e1') | Some e2' -> - snd (castTo t2 tresult e2') + snd (castTo ~kind:ConditionalConversion t2 tresult e2') in - let e3' = snd (castTo t3 tresult e3') in + let e3' = snd (castTo ~kind:ConditionalConversion t3 tresult e3') in finishExp se1 (Question (e1', e2', e3', tresult)) tresult | _ -> (* Use a conditional *) begin match e2'o with None -> (* has form "e1 ? : e3" *) let tmp = var (newTempVar nil true tresult) in - let (se1, _, _) = doExp asconst e1 (ASet(tmp, tresult)) in + let (se1, e1', t1) = doExp asconst e1 (AExp None) in + let (se1, _, _) = finishExp ~newWhat:(ASet(tmp, tresult)) + se1 (snd (castTo ~kind:ConditionalConversion t1 tresult e1')) tresult in let (se3, _, _) = finishExp ~newWhat:(ASet(tmp, tresult)) - se3 e3' t3 in + se3 (snd (castTo ~kind:ConditionalConversion t3 tresult e3')) tresult in + (* TODO: technically, it might be more accurate to branch on the value of e1' before ConditionalConversion *) finishExp (se1 @@ ifChunk (Lval(tmp)) !currentLoc !currentExpLoc skipChunk se3) (Lval(tmp)) @@ -4872,9 +4886,9 @@ and doExp (asconst: bool) (* This expression is used as a constant *) in (* Now add the stmts lv:=e2 and lv:=e3 to se2 and se3 *) let (se2, _, _) = finishExp ~newWhat:(ASet(lv,lvt)) - se2 e2' t2 in + se2 (snd (castTo ~kind:ConditionalConversion t2 tresult e2')) tresult in let (se3, _, _) = finishExp ~newWhat:(ASet(lv,lvt)) - se3 e3' t3 in + se3 (snd (castTo ~kind:ConditionalConversion t3 tresult e3')) tresult in finishExp (doCondition asconst e1 se2 se3) (Lval(lv)) tresult end @@ -4992,7 +5006,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *) res end in - finishExp empty (makeCast ~e:(integer addrval) ~newt:voidPtrType) voidPtrType + finishExp empty (makeCast ~kind:Internal ~e:(integer addrval) ~newt:voidPtrType) voidPtrType end | A.EXPR_PATTERN _ -> E.s (E.bug "EXPR_PATTERN in cabs2cil input") @@ -5040,14 +5054,14 @@ and doBinOp (bop: binop) (e1: exp) (t1: typ) (e2: exp) (t2: typ) : typ * exp = let tres = arithmeticConversion t1 t2 in (* Keep the operator since it is arithmetic *) tres, - optConstFoldBinOp false bop (makeCastT ~e:e1 ~oldt:t1 ~newt:tres) (makeCastT ~e:e2 ~oldt:t2 ~newt:tres) tres + optConstFoldBinOp false bop (makeCastT ~kind:ArithmeticConversion ~e:e1 ~oldt:t1 ~newt:tres) (makeCastT ~kind:ArithmeticConversion ~e:e2 ~oldt:t2 ~newt:tres) tres in let doArithmeticComp () = let tres = arithmeticConversion t1 t2 in (* Keep the operator since it is arithmetic *) intType, optConstFoldBinOp false bop - (makeCastT ~e:e1 ~oldt:t1 ~newt:tres) (makeCastT ~e:e2 ~oldt:t2 ~newt:tres) intType + (makeCastT ~kind:ArithmeticConversion ~e:e1 ~oldt:t1 ~newt:tres) (makeCastT ~kind:ArithmeticConversion ~e:e2 ~oldt:t2 ~newt:tres) intType in let doIntegralArithmetic () = let tres = unrollType (arithmeticConversion t1 t2) in @@ -5055,15 +5069,15 @@ and doBinOp (bop: binop) (e1: exp) (t1: typ) (e2: exp) (t2: typ) : typ * exp = TInt _ -> tres, optConstFoldBinOp false bop - (makeCastT ~e:e1 ~oldt:t1 ~newt:tres) (makeCastT ~e:e2 ~oldt:t2 ~newt:tres) tres + (makeCastT ~kind:ArithmeticConversion ~e:e1 ~oldt:t1 ~newt:tres) (makeCastT ~kind:ArithmeticConversion ~e:e2 ~oldt:t2 ~newt:tres) tres | _ -> E.s (error "%a operator on a non-integer type" d_binop bop) in let pointerComparison e1 t1 e2 t2 = (* Cast both sides to an integer *) let commontype = !upointType in intType, - optConstFoldBinOp false bop (makeCastT ~e:e1 ~oldt:t1 ~newt:commontype) - (makeCastT ~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 @@ -5074,7 +5088,7 @@ and doBinOp (bop: binop) (e1: exp) (t1: typ) (e2: exp) (t2: typ) : typ * exp = let t1' = integralPromotion t1 in let t2' = integralPromotion t2 in t1', - optConstFoldBinOp false bop (makeCastT ~e:e1 ~oldt:t1 ~newt:t1') (makeCastT ~e:e2 ~oldt:t2 ~newt:t2') t1' + optConstFoldBinOp false bop (makeCastT ~kind:IntegerPromotion ~e:e1 ~oldt:t1 ~newt:t1') (makeCastT ~kind:IntegerPromotion ~e:e2 ~oldt:t2 ~newt:t2') t1' | (PlusA|MinusA) when isArithmeticType t1 && isArithmeticType t2 -> doArithmetic () @@ -5084,44 +5098,44 @@ and doBinOp (bop: binop) (e1: exp) (t1: typ) (e2: exp) (t2: typ) : typ * exp = | PlusA when isPointerType t1 && isIntegralType t2 -> t1, optConstFoldBinOp false PlusPI e1 - (makeCastT ~e:e2 ~oldt:t2 ~newt:(integralPromotion t2)) t1 + (makeCastT ~kind:IntegerPromotion ~e:e2 ~oldt:t2 ~newt:(integralPromotion t2)) t1 | PlusA when isIntegralType t1 && isPointerType t2 -> t2, optConstFoldBinOp false PlusPI e2 - (makeCastT ~e:e1 ~oldt:t1 ~newt:(integralPromotion t1)) t2 + (makeCastT ~kind:IntegerPromotion ~e:e1 ~oldt:t1 ~newt:(integralPromotion t1)) t2 | MinusA when isPointerType t1 && isIntegralType t2 -> t1, optConstFoldBinOp false MinusPI e1 - (makeCastT ~e:e2 ~oldt:t2 ~newt:(integralPromotion t2)) t1 + (makeCastT ~kind:IntegerPromotion ~e:e2 ~oldt:t2 ~newt:(integralPromotion t2)) t1 | MinusA when isPointerType t1 && isPointerType t2 -> let commontype = t1 in !ptrdiffType, - optConstFoldBinOp false MinusPP (makeCastT ~e:e1 ~oldt:t1 ~newt:commontype) - (makeCastT ~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 ~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 ~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 ~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 ~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 ~e:e1 ~oldt:t1 ~newt:!upointType) !upointType - (makeCastT ~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 ~e:e1 ~oldt:t1 ~newt:!upointType) !upointType - (makeCastT ~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))) @@ -5508,7 +5522,7 @@ and doInit d_exp oneinit' d_type t' d_type so.soTyp); *) setone so.soOff (if !insertImplicitCasts then - makeCastT ~e:oneinit' ~oldt:t' ~newt:so.soTyp + makeCastT ~kind:Implicit ~e:oneinit' ~oldt:t' ~newt:so.soTyp (* C11 6.7.9.11 *) else oneinit'); (* Move on *) advanceSubobj so; @@ -5592,7 +5606,7 @@ and doInit | _, (A.NEXT_INIT, A.COMPOUND_INIT [(A.NEXT_INIT, A.SINGLE_INIT oneinit)]) :: restil -> let se, oneinit', t' = doExp isconst oneinit (AExp(Some so.soTyp)) in - setone so.soOff (makeCastT ~e:oneinit' ~oldt:t' ~newt:so.soTyp); + setone so.soOff (makeCastT ~kind:Implicit ~e:oneinit' ~oldt:t' ~newt:so.soTyp); (* C11 6.7.9.11 *) (* Move on *) advanceSubobj so; doInit isconst setone so (acc @@ se) restil @@ -6348,7 +6362,7 @@ and doDecl (isglobal: bool) (isstmt: bool) : A.definition -> chunk = function let default = defaultChunk l el - (i2c (Set ((Mem (makeCast ~e:(integer 0) ~newt:intPtrType), + (i2c (Set ((Mem (makeCast ~kind:Internal ~e:(integer 0) ~newt:intPtrType), NoOffset), integer 0, l, el))) in @@ -6546,7 +6560,7 @@ and doDecl (isglobal: bool) (isstmt: bool) : A.definition -> chunk = function TVoid _ -> None | (TInt _ | TEnum _ | TFloat _ | TPtr _) as rt -> ignore (warnOpt "Body of function %s falls-through. Adding a return statement" !currentFunctionFDEC.svar.vname); - Some (makeCastT ~e:zero ~oldt:intType ~newt:rt) + Some (makeCastT ~kind:Implicit ~e:zero ~oldt:intType ~newt:rt) (* C11 6.8.6.4.3 *) | _ -> ignore (warn "Body of function %s falls-through and cannot find an appropriate return value" !currentFunctionFDEC.svar.vname); None @@ -6670,7 +6684,7 @@ and assignInit (lv: lval) (acc: chunk) : chunk = match ie with SingleInit e -> - let (_, e'') = castTo iet (typeOfLval lv) e in + let (_, e'') = castTo ~kind:Implicit iet (typeOfLval lv) e in (* 6.5.16.1.2 *) acc +++ (Set(lv, e'', !currentLoc, !currentExpLoc)) | CompoundInit (t, initl) -> begin match unrollType t with @@ -6887,7 +6901,7 @@ and doStatement (s : A.statement) : chunk = typeRemoveAttributes ["warn_unused_result"] !currentReturnType in let (se, e', et) = doExp false e (AExp (Some rt)) in - let (et'', e'') = castTo et rt e' in + let (et'', e'') = castTo ~kind:Implicit et rt e' in (* C11 6.8.6.4.3 *) se @@ (returnChunk (Some e'') loc' eloc') end @@ -6900,7 +6914,7 @@ and doStatement (s : A.statement) : chunk = if not (Cil.isIntegralType et) then E.s (error "Switch on a non-integer expression."); let et' = integralPromotion et in - let e' = makeCastT ~e:e' ~oldt:et ~newt:et' in + let e' = makeCastT ~kind:IntegerPromotion ~e:e' ~oldt:et ~newt:et' in enter_break_env (); let s' = doStatement s in exit_break_env (); @@ -6968,7 +6982,7 @@ and doStatement (s : A.statement) : chunk = match !gotoTargetData with Some (switchv, switch) -> (* We have already generated this one *) se - @@ i2c(Set (var switchv, makeCast ~e:e' ~newt:!upointType, loc', locUnknown)) (* TODO: eloc for COMPGOTO *) + @@ i2c(Set (var switchv, makeCast ~kind:Internal ~e:e' ~newt:!upointType, loc', locUnknown)) (* TODO: eloc for COMPGOTO *) @@ s2c(mkStmt(Goto (ref switch, loc'))) | None -> begin @@ -6991,7 +7005,7 @@ and doStatement (s : A.statement) : chunk = (* And make a label for it since we'll goto it *) switch.labels <- [Label ("__docompgoto", loc', false)]; gotoTargetData := Some (switchv, switch); - se @@ i2c (Set(var switchv, makeCast ~e:e' ~newt:!upointType, loc', locUnknown)) @@ (* TODO: eloc for COMPGOTO *) + se @@ i2c (Set(var switchv, makeCast ~kind:Internal ~e:e' ~newt:!upointType, loc', locUnknown)) @@ (* TODO: eloc for COMPGOTO *) s2c switch end end diff --git a/src/mergecil.ml b/src/mergecil.ml index 6de3abc4a..8362a36c9 100644 --- a/src/mergecil.ml +++ b/src/mergecil.ml @@ -1246,15 +1246,15 @@ | BinOp (xop, xe1, xe2, xt), BinOp (yop, ye1, ye2, yt) -> xop = yop && equalExps xe1 ye1 && equalExps xe2 ye2 && true (*INC: xt == yt*) - | CastE (xt, xe), CastE (yt, ye) -> + | CastE (_, xt, xe), CastE (_, yt, ye) -> (*INC: xt == yt &&*) equalExps xe ye | AddrOf xl, AddrOf yl -> equalLvals xl yl | StartOf xl, StartOf yl -> equalLvals xl yl (* initializers that go through CIL multiple times sometimes lose casts they had the first time; so allow a different of a cast *) - | CastE (xt, xe), ye -> equalExps xe ye - | xe, CastE (yt, ye) -> equalExps xe ye + | CastE (_, xt, xe), ye -> equalExps xe ye + | xe, CastE (_, yt, ye) -> equalExps xe ye | _, _ -> false and equalLvals (x : lval) (y : lval) : bool =