diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index ae7a41fd5008aace906238f7035fda8352b7dab1..5d267f9428f6d0848eb021cdf293489b2a87ffd9 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -125,20 +125,8 @@ let () = Cil_printer.register_shallow_attribute frama_c_destructor
types of cabs2cil-introduced temp variables. *)
let typeForInsertedVar: (Cil_types.typ -> Cil_types.typ) ref = ref (fun t -> t)
-(** Like [typeForInsertedVar], but for casts.
- * Casts in the source code are exempt from this hook. *)
-let typeForInsertedCast:
- (Cil_types.exp -> Cil_types.typ -> Cil_types.typ -> Cil_types.typ) ref =
- ref (fun _ _ t -> t)
-
-
let cabs_exp loc node = { expr_loc = loc; expr_node = node }
-let bigger_length_args l1 l2 =
- match l1, l2 with
- | None, _ | _, None -> false
- | Some l1, Some l2 -> List.length l1 > List.length l2
-
let abort_context msg =
let pos = fst (Cil.CurrentLoc.get ()) in
let append fmt =
@@ -708,23 +696,6 @@ let gotoTargetHash: (string, int) H.t = H.create 13
let gotoTargetNextAddr: int ref = ref 0
-(********** TRANSPARENT UNION ******)
-(* Check if a type is a transparent union, and return the first field if it
- * is *)
-let isTransparentUnion (t: typ) : fieldinfo option =
- match unrollType t with
- | TComp (comp, _) when not comp.cstruct ->
- (* Turn transparent unions into the type of their first field *)
- if typeHasAttribute "transparent_union" t then begin
- match comp.cfields with
- | Some [] | None ->
- abort_context
- "Empty transparent union: %s" (compFullName comp)
- | Some (f :: _) -> Some f
- end else
- None
- | _ -> None
-
(* When we process an argument list, remember the argument index which has a
* transparent union type, along with the original type. We need this to
* process function definitions *)
@@ -1439,33 +1410,6 @@ let integralPromotion = Cil.integralPromotion
exceptions, also listed in 6.3.2.1:2 *)
let dropQualifiers = Cil.type_remove_qualifier_attributes
-(* true if the expression is known to be a boolean result, i.e. 0 or 1. *)
-let rec is_boolean_result e =
- Cil.(isBoolType (typeOf e)) ||
- match e.enode with
- | Const _ ->
- (match Cil.isInteger e with
- | Some i ->
- Integer.equal i Integer.zero || Integer.equal i Integer.one
- | None -> false)
- | CastE (_,e) -> is_boolean_result e
- | BinOp((Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr),_,_,_) -> true
- | BinOp((PlusA | PlusPI | MinusA | MinusPI | MinusPP | Mult
- | Div | Mod | Shiftlt | Shiftrt | BAnd | BXor | BOr),_,_,_) -> false
- | UnOp(LNot,_,_) -> true
- | UnOp ((Neg | BNot),_,_) -> false
- | Lval _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _
- | AlignOfE _ | AddrOf _ | StartOf _ -> false
-
-(* Like Cil.mkCastT, but it calls typeForInsertedCast *)
-let makeCastT ~(e: exp) ~(oldt: typ) ~(newt: typ) =
- if need_cast oldt newt then
- Cil.mkCastT ~oldt ~newt:(!typeForInsertedCast e oldt newt) e
- else e
-
-let makeCast ~(e: exp) ~(newt: typ) =
- makeCastT ~e ~oldt:(typeOf e) ~newt
-
let is_scalar_type t =
match unrollType t with
| TInt _
@@ -2182,7 +2126,7 @@ struct
| Case (e, loc) ->
(* If needed, convert e to type t, and check in case the label
was too big *)
- let e' = makeCast ~e ~newt:t in
+ let e' = mkCast ~newt:t e in
let constFold = constFold true in
let e'' = if theMachine.lowerConstants then constFold e' else e' in
(match constFoldToInt e, constFoldToInt e'' with
@@ -2661,208 +2605,9 @@ let cabsTypeAddAttributes =
let get_qualifiers t = Cil.filter_qualifier_attributes (Cil.typeAttrs t)
-(* Specify whether the cast is from the source code *)
-let rec castTo ?context ?(fromsource=false)
- (ot : typ) (nt : typ) (e : exp) : (typ * exp ) =
- let dkey = Kernel.dkey_typing_cast in
- Kernel.debug ~dkey "@[%t: castTo:%s %a->%a@\n@]"
- Cil.pp_thisloc (if fromsource then "(source)" else "")
- Cil_datatype.Typ.pretty ot Cil_datatype.Typ.pretty nt;
- if not fromsource && not (need_cast ot nt) then begin
- (* Do not put the cast if it is not necessary, unless it is from the
- * source. *)
- Kernel.debug ~dkey "no cast to perform";
- (ot, e)
- end else begin
- let nt = if fromsource then nt else !typeForInsertedCast e ot nt in
- let result = (nt, if theMachine.insertImplicitCasts || fromsource then
- Cil.mkCastT ~force:true ~oldt:ot ~newt:nt e else e)
- in
- let origin_error =
- if fromsource then "explicit cast:" else " implicit cast:"
- in
- (* [BM] uncomment the following line to enable attributes static typing
- ignore (check_strict_attributes true ot nt && check_strict_attributes false nt ot);*)
- Kernel.debug ~dkey "@[castTo: ot=%a nt=%a\n result is %a@\n@]"
- Cil_datatype.Typ.pretty ot Cil_datatype.Typ.pretty nt
- Cil_printer.pp_exp (snd result);
- (* Now see if we can have a cast here *)
- match Cil.unrollType ot, Cil.unrollType nt with
- | TNamed _, _
- | _, TNamed _ -> Kernel.fatal ~current:true "unrollType failed in castTo"
- | t, TInt(IBool,_) when is_scalar_type t ->
- if is_boolean_result e then begin
- Kernel.debug ~dkey "Explicit cast to Boolean: %a" Cil_printer.pp_exp e;
- result
- end else begin
- Kernel.debug ~dkey
- "bool conversion by checking !=0: %a" Cil_printer.pp_exp e;
- let cmp = Cil.mkBinOp ~loc:e.eloc Ne e (Cil.integer ~loc:e.eloc 0) in
- let oldt = Cil.typeOf cmp in
- nt, Cil.mkCastT ~oldt ~newt:nt cmp
- end
- | TInt(_,_), TInt(_,_) ->
- (* We used to ignore attributes on integer-integer casts. Not anymore *)
- (* if ikindo = ikindn then (nt, e) else *)
- result
- | TPtr (TFun (_,args,va,_),_), TPtr(TFun (_,args',va',_),_) ->
- (* Checks on casting from a function type into another one.
- We enforce at least the same number of arguments, and emit a warning
- if types do not match. Note that empty argument lists are always
- compatible. *)
- if (va <> va' || bigger_length_args args args') &&
- (args <> None && args' <> None)
- then
- abort_context
- "%s conversion between function types with \
- different number of arguments:@ %a@ and@ %a"
- origin_error
- Cil_datatype.Typ.pretty ot Cil_datatype.Typ.pretty nt;
- if not (areCompatibleTypes ?context ot nt) then
- Kernel.warning
- ~wkey:Kernel.wkey_incompatible_types_call
- ~current:true
- "implicit conversion between incompatible function types:@ \
- %a@ and@ %a"
- Cil_datatype.Typ.pretty ot Cil_datatype.Typ.pretty nt;
- result
-
- | TFun _, TPtr(TFun _, _) ->
- let clean_e =
- match e.enode with
- | Lval lv -> Cil.mkAddrOf ~loc:e.eloc lv
- | _ -> e (* function decay into pointer anyway *)
- in
- castTo ?context ~fromsource (TPtr (ot, [])) nt clean_e
-
- (* accept converting a ptr to function to/from a ptr to void, even though
- not really accepted by the standard. gcc supports it. though
- *)
- | TPtr (TFun _,_), TPtr (TVoid _, _) -> result
- | TPtr (TVoid _, _), TPtr (TFun _,_) -> result
- (* Taking numerical address or calling an absolute location. Also
- accepted by gcc albeit with a warning. *)
- | TInt _, TPtr (TFun _, _) -> result
-
- (* pointer to potential function type. Note that we do not
- use unrollTypeDeep above in order to avoid needless divergence with
- original type in the sources.
- *)
- | TPtr(TFun _,_), TPtr(TNamed(ti,nattr),pattr) ->
- castTo ?context
- ~fromsource ot (TPtr (Cil.typeAddAttributes nattr ti.ttype, pattr)) e
- | TPtr(TNamed(ti,nattr),pattr), TPtr(TFun _,_) ->
- castTo ?context
- ~fromsource (TPtr (Cil.typeAddAttributes nattr ti.ttype, pattr)) nt e
-
- (* No other conversion implying a pointer to function
- and a pointer to object are supported. *)
- | TPtr (TFun _,_), TPtr _ ->
- Kernel.warning
- ~wkey:Kernel.wkey_incompatible_pointer_types
- ~current:true
- "casting function to %a" Cil_datatype.Typ.pretty nt;
- result
- | TPtr _, TPtr (TFun _,_) ->
- Kernel.warning
- ~wkey:Kernel.wkey_incompatible_pointer_types
- ~current:true
- "casting function from %a" Cil_datatype.Typ.pretty ot;
- result
- | _, TPtr (TFun _, _) ->
- abort_context "%s cannot cast %a to function type"
- origin_error Cil_datatype.Typ.pretty ot
- | TPtr _, TPtr _ -> result
-
- | TInt _, TPtr _ -> result
-
- | TPtr _, TInt _ ->
- if not fromsource
- then
- Kernel.warning
- ~wkey:Kernel.wkey_int_conversion
- ~current:true
- "Conversion from a pointer to an integer without an explicit cast";
- result
-
- | TArray _, TPtr _ -> result
-
- | TArray(t1,_,_), TArray(t2,None,_)
- when Cil_datatype.Typ.equal t1 t2 -> (nt, e)
-
- | TPtr _, TArray(_,_,_) ->
- abort_context "%s cast over a non-scalar type %a"
- origin_error Cil_datatype.Typ.pretty nt;
-
- | TEnum _, TInt _ -> result
- | TFloat _, (TInt _|TEnum _) -> result
- | (TInt _|TEnum _), TFloat _ -> result
- | TFloat _, TFloat _ -> result
- | TInt (ik,_), TEnum (ei,_) ->
- (match e.enode with
- | Const (CEnum { eihost = ei'})
- when ei.ename = ei'.ename && not fromsource &&
- Cil.bytesSizeOfInt ik = Cil.bytesSizeOfInt ei'.ekind
- -> (nt,e)
- | _ -> result)
- | TEnum _, TEnum _ -> result
-
- | TEnum _, TPtr _ -> result
- | TBuiltin_va_list _, (TInt _ | TPtr _) ->
- result
-
- | (TInt _ | TPtr _), TBuiltin_va_list _ ->
- Kernel.debug ~dkey ~current:true
- "Casting %a to __builtin_va_list" Cil_datatype.Typ.pretty ot ;
- result
-
- | TPtr _, TEnum _ ->
- Kernel.debug ~dkey ~current:true
- "Casting a pointer into an enumeration type" ;
- result
-
- (* The expression is evaluated for its effects *)
- | (TInt _ | TEnum _ | TPtr _ ), TVoid _ ->
- Kernel.debug ~level:3
- "Casting a value into void: expr is evaluated for side effects";
- result
-
- (* Even casts between structs are allowed when we are only
- * modifying some attributes *)
- | TComp (comp1, _), TComp (comp2, _) when comp1.ckey = comp2.ckey ->
- result
-
- (* If we try to pass a transparent union value to a function
- * expecting a transparent union argument, the argument type would
- * have been changed to the type of the first argument, and we'll
- * see a cast from a union to the type of the first argument. Turn
- * that into a field access *)
- | TComp(_, _), _ -> begin
- match isTransparentUnion ot with
- | None ->
- abort_context "%s %a -> %a"
- origin_error Cil_datatype.Typ.pretty ot Cil_datatype.Typ.pretty nt
- | Some fstfield -> begin
- (* We do it now only if the expression is an lval *)
- let e' =
- match e.enode with
- | Lval lv ->
- new_exp ~loc:e.eloc
- (Lval (addOffsetLval (Field(fstfield, NoOffset)) lv))
- | _ ->
- abort_context
- "%s transparent union expression is not an lval: %a\n"
- origin_error
- Cil_printer.pp_exp e
- in
- (* Continue casting *)
- castTo ?context ~fromsource:fromsource fstfield.ftype nt e'
- end
- end
- | _ ->
- abort_context "%s cannot cast from %a to %a@\n"
- origin_error Cil_datatype.Typ.pretty ot Cil_datatype.Typ.pretty nt
- end
+let castTo ?context ?(fromsource=false)
+ (oldt : typ) (newt : typ) (e : exp) : (typ * exp) =
+ mkCastTGen ?context ~force:fromsource ~fromsource ~oldt ~newt e
(* Create and cache varinfo's for globals. Starts with a varinfo but if the
* global has been declared already it might come back with another varinfo.
@@ -3057,7 +2802,6 @@ let setupBuiltin ?(force_keep=false) name ?spec (resTyp, args_or_argtypes, isva)
if force_keep then
v.vattr <- Cil.addAttribute (Attr ("FC_BUILTIN",[])) v.vattr;
v
-;;
(* builtin is never ghost *)
let memoBuiltin ?force_keep ?spec name proto =
@@ -6045,7 +5789,7 @@ and doExp local_env
if isIntegralType t then
let tres = integralPromotion t in
let e'' =
- new_exp ~loc (UnOp(Neg, makeCastT ~e:e' ~oldt:t ~newt:tres, tres))
+ new_exp ~loc (UnOp(Neg, mkCastT ~oldt:t ~newt:tres e', tres))
in
finishExp r se e'' tres
else
@@ -6061,7 +5805,7 @@ and doExp local_env
if isIntegralType t then
let tres = integralPromotion t in
let e'' =
- new_exp ~loc (UnOp(BNot, makeCastT ~e:e' ~oldt:t ~newt:tres, tres))
+ new_exp ~loc (UnOp(BNot, mkCastT ~oldt:t ~newt:tres e', tres))
in
finishExp r se e'' tres
else
@@ -6071,7 +5815,7 @@ and doExp local_env
let (r, se, e, t as v) = doExp (no_paren_local_env local_env) asconst e what in
if isIntegralType t then
let newt = integralPromotion t in
- let e' = makeCastT ~e ~oldt:t ~newt in
+ let e' = mkCastT ~oldt:t ~newt e in
finishExp r se e' newt
else
if isArithmeticType t then
@@ -7511,7 +7255,7 @@ and doExp local_env
end
in
finishExp [] (unspecified_chunk empty)
- (makeCast ~e:(integer ~loc addrval) ~newt:voidPtrType) voidPtrType
+ (mkCast ~newt:voidPtrType (integer ~loc addrval)) voidPtrType
end
| Cabs.EXPR_PATTERN _ ->
@@ -7689,8 +7433,8 @@ and doBinOp loc (bop: binop) (e1: exp) (t1: typ) (e2: exp) (t2: typ) =
(* Keep the operator since it is arithmetic *)
tres,
optConstFoldBinOp loc false bop
- (makeCastT ~e:e1 ~oldt:t1 ~newt:tres)
- (makeCastT ~e:e2 ~oldt:t2 ~newt:tres)
+ (mkCastT ~oldt:t1 ~newt:tres e1)
+ (mkCastT ~oldt:t2 ~newt:tres e2)
tres
end else
abort_context
@@ -7702,8 +7446,8 @@ and doBinOp loc (bop: binop) (e1: exp) (t1: typ) (e2: exp) (t2: typ) =
(* Keep the operator since it is arithmetic *)
intType,
optConstFoldBinOp loc false bop
- (makeCastT ~e:e1 ~oldt:t1 ~newt:tres)
- (makeCastT ~e:e2 ~oldt:t2 ~newt:tres)
+ (mkCastT ~oldt:t1 ~newt:tres e1)
+ (mkCastT ~oldt:t2 ~newt:tres e2)
intType
in
let doIntegralArithmetic () =
@@ -7713,8 +7457,8 @@ and doBinOp loc (bop: binop) (e1: exp) (t1: typ) (e2: exp) (t2: typ) =
| TInt _ ->
tres,
optConstFoldBinOp loc false bop
- (makeCastT ~e:e1 ~oldt:t1 ~newt:tres)
- (makeCastT ~e:e2 ~oldt:t2 ~newt:tres)
+ (mkCastT ~oldt:t1 ~newt:tres e1)
+ (mkCastT ~oldt:t2 ~newt:tres e2)
tres
| _ ->
Kernel.fatal
@@ -7735,8 +7479,8 @@ and doBinOp loc (bop: binop) (e1: exp) (t1: typ) (e2: exp) (t2: typ) =
arguments with incompatible types to a common type *)
let e1', e2' =
if not (areCompatibleTypes t1p t2p) then
- makeCastT ~e:e1 ~oldt:t1 ~newt:Cil.voidPtrType,
- makeCastT ~e:e2 ~oldt:t2 ~newt:Cil.voidPtrType
+ mkCastT ~oldt:t1 ~newt:Cil.voidPtrType e1,
+ mkCastT ~oldt:t2 ~newt:Cil.voidPtrType e2
else e1, e2
in
intType,
@@ -7748,7 +7492,7 @@ and doBinOp loc (bop: binop) (e1: exp) (t1: typ) (e2: exp) (t2: typ) =
{ e1 with enode = AddrOf (addOffsetLval (Index (e2,NoOffset)) lv) }
| _ ->
optConstFoldBinOp loc false PlusPI e1
- (makeCastT ~e:e2 ~oldt:t2 ~newt:(integralPromotion t2)) t1
+ (mkCastT ~oldt:t2 ~newt:(integralPromotion t2) e2) t1
in
match bop with
| (Mult|Div) -> doArithmetic ()
@@ -7763,8 +7507,8 @@ and doBinOp loc (bop: binop) (e1: exp) (t1: typ) (e2: exp) (t2: typ) =
let t2' = integralPromotion t2 in
t1',
optConstFoldBinOp loc false bop
- (makeCastT ~e:e1 ~oldt:t1 ~newt:t1')
- (makeCastT ~e:e2 ~oldt:t2 ~newt:t2')
+ (mkCastT ~oldt:t1 ~newt:t1' e1)
+ (mkCastT ~oldt:t2 ~newt:t2' e2)
t1'
| (PlusA|MinusA)
when isArithmeticType t1 && isArithmeticType t2 -> doArithmetic ()
@@ -7778,7 +7522,7 @@ and doBinOp loc (bop: binop) (e1: exp) (t1: typ) (e2: exp) (t2: typ) =
| MinusA when isPointerType t1 && isIntegralType t2 ->
t1,
optConstFoldBinOp loc false MinusPI e1
- (makeCastT ~e:e2 ~oldt:t2 ~newt:(integralPromotion t2)) t1
+ (mkCastT ~oldt:t2 ~newt:(integralPromotion t2) e2) t1
| MinusA when isPointerType t1 && isPointerType t2 ->
if areCompatibleTypes (* C99 6.5.6:3 *)
(Cil.type_remove_qualifier_attributes_deep t1)
@@ -7791,9 +7535,9 @@ and doBinOp loc (bop: binop) (e1: exp) (t1: typ) (e2: exp) (t2: typ) =
(* Two special cases for comparisons with the NULL pointer. We are a bit
more permissive. *)
| (Le|Lt|Ge|Gt|Eq|Ne) when isPointerType t1 && isZero e2 ->
- pointerComparison e1 t1 (makeCast ~e:e2 ~newt:t1) t1
+ pointerComparison e1 t1 (mkCast ~newt:t1 e2) t1
| (Le|Lt|Ge|Gt|Eq|Ne) when isPointerType t2 && isZero e1 ->
- pointerComparison (makeCast ~e:e1 ~newt:t2) t2 e2 t2
+ pointerComparison (mkCast ~newt:t2 e1) t2 e2 t2
| (Le|Lt|Ge|Gt|Eq|Ne) when isPointerType t1 && isPointerType t2 ->
pointerComparison e1 t1 e2 t2
@@ -8449,7 +8193,7 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
asconst oneinit (AExp(Some so.soTyp))
in
let r = Cil_datatype.Lval.Set.of_list r in
- let init_expr = makeCastT ~e:oneinit' ~oldt:t' ~newt:so.soTyp in
+ let init_expr = mkCastT ~oldt:t' ~newt:so.soTyp oneinit' in
let preinit' = setOneInit preinit so.soOff (SinglePre (init_expr, r)) in
(* Move on *)
advanceSubobj so;
@@ -9024,7 +8768,7 @@ and createLocal ghost ((_, sto, _, _) as specs)
in
let setlen = se0 +++
(mkStmtOneInstr ~ghost ~valid_sid
- (Set(var savelen, makeCast ~e:len ~newt:savelen.vtype,
+ (Set(var savelen, mkCast ~newt:savelen.vtype len,
CurrentLoc.get ())),
[],[],[])
in
@@ -9054,8 +8798,7 @@ and createLocal ghost ((_, sto, _, _) as specs)
(Local_init
(vi,AssignInit
(SingleInit
- (makeCast ~e:(new_exp ~loc (Lval(var tmp)))
- ~newt:vi.vtype)),
+ (mkCast ~newt:vi.vtype (new_exp ~loc (Lval(var tmp))))),
CurrentLoc.get ())),
[],[var vi],[var tmp])
end
@@ -9491,8 +9234,7 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
defaultChunk ~ghost
loc
(i2c (mkStmtOneInstr ~ghost:local_env.is_ghost ~valid_sid
- (Set ((Mem (makeCast ~e:(integer ~loc 0)
- ~newt:intPtrType),
+ (Set ((Mem (mkCast ~newt:intPtrType (integer ~loc 0)),
NoOffset),
integer ~loc 0, loc)),[],[],[]))
in
@@ -9580,7 +9322,7 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
match unrollType !currentReturnType with
| TVoid _ -> [], None
| (TInt _ | TEnum _ | TFloat _ | TPtr _) as rt ->
- let res = Some (makeCastT ~e:(zero ~loc) ~oldt:intType ~newt:rt) in
+ let res = Some (mkCastT ~oldt:intType ~newt:rt (zero ~loc)) in
if !currentFunctionFDEC.svar.vname = "main" then
[],res
else begin
@@ -9595,7 +9337,7 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
On the other hand, *( T* )0 is. We're not supposed
to get there anyway. *)
let null_ptr =
- makeCastT ~e:(zero ~loc) ~oldt:intType ~newt:(TPtr(rt,[]))
+ mkCastT ~oldt:intType ~newt:(TPtr(rt,[])) (zero ~loc)
in
let res =
Some (new_exp ~loc (Lval (mkMem ~addr:null_ptr ~off:NoOffset)))
@@ -10104,7 +9846,7 @@ and doStatement local_env (s : Cabs.statement) : chunk =
if not (Cil.isIntegralType et) then
Kernel.error ~once:true ~current:true "Switch on a non-integer expression.";
let et' = Cil.integralPromotion et in
- let e' = makeCastT ~e:e' ~oldt:et ~newt:et' in
+ let e' = mkCastT ~oldt:et ~newt:et' e' in
enter_break_env ();
let s' = doStatement local_env s in
exit_break_env ();
@@ -10182,7 +9924,7 @@ and doStatement local_env (s : Cabs.statement) : chunk =
| Some (switchv, switch) -> (* We have already generated this one *)
(se
@@@ (i2c(mkStmtOneInstr ~ghost ~valid_sid
- (Set (var switchv, makeCast ~e:e' ~newt:intType, loc')),
+ (Set (var switchv, mkCast ~newt:intType e', loc')),
[],[],[]), ghost))
@@@ (s2c(mkStmt ~ghost ~valid_sid (Goto (ref switch, loc'))), ghost)
@@ -10213,7 +9955,7 @@ and doStatement local_env (s : Cabs.statement) : chunk =
(se @@@
(i2c
(mkStmtOneInstr ~ghost ~valid_sid
- (Set (var switchv, makeCast ~e:e' ~newt:intType, loc')),
+ (Set (var switchv, mkCast ~newt:intType e', loc')),
[],[],[]),
ghost))
@@@ (s2c switch, ghost)
diff --git a/src/kernel_internals/typing/cabs2cil.mli b/src/kernel_internals/typing/cabs2cil.mli
index 21b1100134556d614dd3af4d174aae60852eb592..13d8b9107f4f18b5d2a082173bfa14482d7459fa 100644
--- a/src/kernel_internals/typing/cabs2cil.mli
+++ b/src/kernel_internals/typing/cabs2cil.mli
@@ -160,18 +160,6 @@ val fc_local_static: string
types of cabs2cil-introduced temp variables. *)
val typeForInsertedVar: (Cil_types.typ -> Cil_types.typ) ref
-(** Like [typeForInsertedVar], but for casts.
- [typeForInsertedCast expr original_type destination_type]
- returns the type into which [expr], which has type [original_type] and
- whose type must be converted into [destination_type], must be casted.
-
- By default, returns [destination_type].
-
- This applies only to implicit casts. Casts already present
- in the source code are exempt from this hook. *)
-val typeForInsertedCast:
- (Cil_types.exp -> Cil_types.typ -> Cil_types.typ -> Cil_types.typ) ref
-
(** [fresh_global prefix] creates a variable name not clashing with any other
globals and starting with [prefix] *)
val fresh_global : string -> string
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 17d4701d6fd10e0a505892ab4d5a9ac49046a1fb..94be68f46f229218626cd984f50d41fd1bad28f6 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -70,6 +70,14 @@ let () = Log.set_current_source (fun () -> fst (CurrentLoc.get ()))
let pp_thisloc fmt = Location.pretty fmt (CurrentLoc.get ())
+let abort_context msg =
+ let pos = fst (CurrentLoc.get ()) in
+ let append fmt =
+ Format.pp_print_newline fmt ();
+ Errorloc.pp_context_from_file fmt pos
+ in
+ Kernel.abort ~current:true ~append msg
+
let voidType = Cil_const.voidType
let intType = TInt(IInt,[])
let uintType = TInt(IUInt,[])
@@ -3587,6 +3595,7 @@ let rec isLogicRealType t =
isLogicRealType (unroll_ltdef ty)
| Lvar _ | Ltype _ | Larrow _ -> false
+(* ISO 6.2.5.18 *)
let isArithmeticType t =
match unrollTypeSkel t with
(TInt _ | TEnum _ | TFloat _) -> true
@@ -3597,13 +3606,6 @@ let isLongDoubleType t =
| TFloat(FLongDouble,_) -> true
| _ -> false
-let isScalarType t=
- match unrollTypeSkel t with
- | TInt _ | TEnum _ | TFloat _ | TPtr _ -> true
- | _ -> false
-
-let isArithmeticOrPointerType = isScalarType
-
let rec isLogicArithmeticType t =
match t with
| Ctype t -> isArithmeticType t
@@ -3617,6 +3619,10 @@ let isFunctionType t =
| TFun _ -> true
| _ -> false
+(* ISO 6.2.5.1 *)
+let isObjectType t =
+ not (isFunctionType t)
+
let isLogicFunctionType t = Logic_const.isLogicCType isFunctionType t
let isFunPtrType t =
@@ -3631,6 +3637,28 @@ let isPointerType t =
| TPtr _ -> true
| _ -> false
+(* ISO 6.2.5.21 *)
+let isScalarType t = isArithmeticType t || isPointerType t
+
+let isArithmeticOrPointerType = isScalarType
+
+
+(********** TRANSPARENT UNION ******)
+(* Check if a type is a transparent union, and return the first field if it
+ * is *)
+let isTransparentUnion (t: typ) : fieldinfo option =
+ match unrollType t with
+ | TComp (comp, _) when not comp.cstruct ->
+ (* Turn transparent unions into the type of their first field *)
+ if typeHasAttribute "transparent_union" t then begin
+ match comp.cfields with
+ | Some [] | None ->
+ abort_context "Empty transparent union: %s" (compFullName comp)
+ | Some (f :: _) -> Some f
+ end else
+ None
+ | _ -> None
+
let rec isTypeTagType t =
match t with
| Ltype ({lt_name = "typetag"},[]) -> true
@@ -3698,15 +3726,15 @@ let rec typeOf (e: exp) : typ =
| Const(CEnum {eival=v}) -> typeOf v
(* l-values used as r-values lose their qualifiers (C99 6.3.2.1:2) *)
- | Lval(lv) -> type_remove_qualifier_attributes (typeOfLval lv)
+ | Lval lv -> type_remove_qualifier_attributes (typeOfLval lv)
| SizeOf _ | SizeOfE _ | SizeOfStr _ -> theMachine.typeOfSizeOf
| AlignOf _ | AlignOfE _ -> theMachine.typeOfSizeOf
| UnOp (_, _, t) -> t
| BinOp (_, _, _, t) -> t
| CastE (t, _) -> t
- | AddrOf (lv) -> TPtr(typeOfLval lv, [])
- | StartOf (lv) ->
+ | AddrOf lv -> TPtr(typeOfLval lv, [])
+ | StartOf lv ->
match unrollType (typeOfLval lv) with
| TArray (t,_,attrs) -> TPtr(t, attrs)
| _ -> Kernel.fatal ~current:true "typeOf: StartOf on a non-array"
@@ -5896,42 +5924,101 @@ let same_int64 ?(machdep=true) e1 e2 =
| Some i, Some i' -> Integer.equal i i'
| _ -> false
+(* how type qualifiers must be checked *)
+type qualifier_check_context =
+ | Identical (* identical qualifiers. *)
+ | IdenticalToplevel (* ignore at toplevel, use Identical when going under a
+ pointer. *)
+ | Covariant (* first type can have const-qualifications
+ the second doesn't have. *)
+ | CovariantToplevel
+ (* accepts everything for current type, use Covariant when going under a
+ pointer. *)
+ | Contravariant (* second type can have const-qualifications
+ the first doesn't have. *)
+ | ContravariantToplevel
+ (* accepts everything for current type, use Contravariant when going under
+ a pointer. *)
-let mkCastT ?(force=false) ~(oldt: typ) ~(newt: typ) e =
- let loc = e.eloc in
- (* Issue #!1546
- let force = force ||
- (* see warning of need_cast function:
- [false] as default value for that option is not safe... *)
- (match e.enode with | Const(CEnum _) -> false | _ -> true)
- in *)
- if need_cast ~force oldt newt then begin
- let mk_cast exp = (* to new type [newt] *)
- new_exp ~loc (CastE(type_remove_qualifier_attributes newt,exp))
- in
- let normalized_type = type_remove_attributes_for_c_cast (unrollType newt) in
- (* Watch out for constants and cast of cast to pointer *)
- match normalized_type, e.enode with
- (* In the case were we have a representation for the literal,
- explicitly add the cast. *)
- | TInt(newik, []), Const(CInt64(i, _, None)) ->
- kinteger64 ~loc ~kind:newik i
- | TPtr _, CastE (_, e') ->
- (match unrollType (typeOf e'), e'.enode with
- | (TPtr _ as typ''), _ ->
- (* Old cast can be removed...*)
- if need_cast ~force newt typ'' then mk_cast e'
- else (* In fact, both casts can be removed. *) e'
- | _, Const(CInt64 (i, _, _)) when Integer.is_zero i -> mk_cast e'
- | _ -> mk_cast e)
- | _ ->
- (* Do not remove old casts because they are conversions !!! *)
- mk_cast e
- end else
- e
+let qualifier_context_fun_arg = function
+ | Identical | IdenticalToplevel -> IdenticalToplevel
+ | Covariant | CovariantToplevel -> ContravariantToplevel
+ | Contravariant | ContravariantToplevel -> CovariantToplevel
+
+let qualifier_context_fun_ret = function
+ | Identical | IdenticalToplevel -> IdenticalToplevel
+ | Covariant | CovariantToplevel -> CovariantToplevel
+ | Contravariant | ContravariantToplevel -> ContravariantToplevel
+
+let qualifier_context_ptr = function
+ | Identical | IdenticalToplevel -> Identical
+ | Covariant | CovariantToplevel -> Covariant
+ | Contravariant | ContravariantToplevel -> Contravariant
+
+let included_qualifiers ?(context=Identical) a1 a2 =
+ let a1 = filter_qualifier_attributes a1 in
+ let a2 = filter_qualifier_attributes a2 in
+ let a1 = dropAttribute "restrict" a1 in
+ let a2 = dropAttribute "restrict" a2 in
+ let a1_no_cv = dropAttributes ["const"; "volatile"] a1 in
+ let a2_no_cv = dropAttributes ["const"; "volatile"] a2 in
+ let is_equal = Cil_datatype.Attributes.equal a1 a2 in
+ if is_equal then true
+ else begin
+ match context with
+ | Identical -> false
+ | Covariant -> Cil_datatype.Attributes.equal a1_no_cv a2
+ | Contravariant -> Cil_datatype.Attributes.equal a1 a2_no_cv
+ | CovariantToplevel | ContravariantToplevel | IdenticalToplevel -> true
+ end
+
+(* precondition: t1 and t2 must be "compatible" as per combineTypes, i.e.
+ you must have called [combineTypes t1 t2] before calling this function. *)
+let rec have_compatible_qualifiers_deep ?(context=Identical) t1 t2 =
+ match unrollType t1, unrollType t2 with
+ | TFun (tres1, Some args1, _, _), TFun (tres2, Some args2, _, _) ->
+ have_compatible_qualifiers_deep
+ ~context:(qualifier_context_fun_ret context) tres1 tres2 &&
+ let context = qualifier_context_fun_arg context in
+ List.for_all2 (fun (_, t1', a1) (_, t2', a2) ->
+ have_compatible_qualifiers_deep ~context t1' t2' &&
+ included_qualifiers ~context a1 a2)
+ args1 args2
+ | TPtr (t1', a1), TPtr (t2', a2)
+ | TArray (t1', _, a1), TArray (t2', _, a2) ->
+ (included_qualifiers ~context a1 a2) &&
+ let context = qualifier_context_ptr context in
+ have_compatible_qualifiers_deep ~context t1' t2'
+ | _, _ -> included_qualifiers ~context (typeAttrs t1) (typeAttrs t2)
+
+
+(* true if the expression is known to be a boolean result, i.e. 0 or 1. *)
+let rec is_boolean_result e =
+ (isBoolType (typeOf e)) ||
+ match e.enode with
+ | Const _ ->
+ (match isInteger e with
+ | Some i ->
+ Integer.equal i Integer.zero || Integer.equal i Integer.one
+ | None -> false)
+ | CastE (_, e) -> is_boolean_result e
+ | BinOp ((Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr), _, _, _) -> true
+ | BinOp
+ ((PlusA | PlusPI | MinusA | MinusPI | MinusPP | Mult
+ | Div | Mod | Shiftlt | Shiftrt | BAnd | BXor | BOr), _, _, _) -> false
+ | UnOp (LNot, _, _) -> true
+ | UnOp ((Neg | BNot), _, _) -> false
+ | Lval _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _
+ | AlignOfE _ | AddrOf _ | StartOf _ -> false
+
+
+(** A hook into the code that creates casts. By default this
+ returns the new type.
+ Casts in the source code are exempt from this hook. *)
+let typeForInsertedCast:
+ (Cil_types.exp -> Cil_types.typ -> Cil_types.typ -> Cil_types.typ) ref =
+ ref (fun _ _ t -> t)
-let mkCast ?force ~(newt: typ) e =
- mkCastT ?force ~oldt:(typeOf e) ~newt e
exception Cannot_combine of string
@@ -6072,12 +6159,9 @@ let combineTypesGen ?emitwith (combF : combineFunction)
(* They are not structurally equal. But perhaps they are equal if we
evaluate them. Check first machine independent comparison. *)
let checkEqualSize (machdep: bool) =
- let size_t = theMachine.typeOfSizeOf in
- let size_t_oldsz' = mkCast ~force:false ~newt:size_t oldsz' in
- let size_t_sz' = mkCast ~force:false ~newt:size_t sz' in
- ExpStructEqSized.equal
- (constFold machdep size_t_oldsz')
- (constFold machdep size_t_sz')
+ match constFoldToInt ~machdep oldsz', constFoldToInt ~machdep sz' with
+ | Some m, Some n -> m = n
+ | _ -> ExpStructEqSized.equal oldsz' sz'
in
if checkEqualSize false then
oldsz
@@ -6201,74 +6285,6 @@ let combineTypes ?(strictReturnTypes=false) what (oldt: typ) (t: typ) : typ =
(***************** Compatibility ******)
-
-(* how type qualifiers must be checked *)
-type qualifier_check_context =
- | Identical (* identical qualifiers. *)
- | IdenticalToplevel (* ignore at toplevel, use Identical when going under a
- pointer. *)
- | Covariant (* first type can have const-qualifications
- the second doesn't have. *)
- | CovariantToplevel
- (* accepts everything for current type, use Covariant when going under a
- pointer. *)
- | Contravariant (* second type can have const-qualifications
- the first doesn't have. *)
- | ContravariantToplevel
- (* accepts everything for current type, use Contravariant when going under
- a pointer. *)
-
-let qualifier_context_fun_arg = function
- | Identical | IdenticalToplevel -> IdenticalToplevel
- | Covariant | CovariantToplevel -> ContravariantToplevel
- | Contravariant | ContravariantToplevel -> CovariantToplevel
-
-let qualifier_context_fun_ret = function
- | Identical | IdenticalToplevel -> IdenticalToplevel
- | Covariant | CovariantToplevel -> CovariantToplevel
- | Contravariant | ContravariantToplevel -> ContravariantToplevel
-
-let qualifier_context_ptr = function
- | Identical | IdenticalToplevel -> Identical
- | Covariant | CovariantToplevel -> Covariant
- | Contravariant | ContravariantToplevel -> Contravariant
-
-let included_qualifiers ?(context=Identical) a1 a2 =
- let a1 = filter_qualifier_attributes a1 in
- let a2 = filter_qualifier_attributes a2 in
- let a1 = dropAttribute "restrict" a1 in
- let a2 = dropAttribute "restrict" a2 in
- let a1_no_cv = dropAttributes ["const"; "volatile"] a1 in
- let a2_no_cv = dropAttributes ["const"; "volatile"] a2 in
- let is_equal = Cil_datatype.Attributes.equal a1 a2 in
- if is_equal then true
- else begin
- match context with
- | Identical -> false
- | Covariant -> Cil_datatype.Attributes.equal a1_no_cv a2
- | Contravariant -> Cil_datatype.Attributes.equal a1 a2_no_cv
- | CovariantToplevel | ContravariantToplevel | IdenticalToplevel -> true
- end
-
-(* precondition: t1 and t2 must be "compatible" as per combineTypes, i.e.
- you must have called [combineTypes t1 t2] before calling this function. *)
-let rec have_compatible_qualifiers_deep ?(context=Identical) t1 t2 =
- match unrollType t1, unrollType t2 with
- | TFun (tres1, Some args1, _, _), TFun (tres2, Some args2, _, _) ->
- have_compatible_qualifiers_deep
- ~context:(qualifier_context_fun_ret context) tres1 tres2 &&
- let context = qualifier_context_fun_arg context in
- List.for_all2 (fun (_, t1', a1) (_, t2', a2) ->
- have_compatible_qualifiers_deep ~context t1' t2' &&
- included_qualifiers ~context a1 a2)
- args1 args2
- | TPtr (t1', a1), TPtr (t2', a2)
- | TArray (t1', _, a1), TArray (t2', _, a2) ->
- (included_qualifiers ~context a1 a2) &&
- let context = qualifier_context_ptr context in
- have_compatible_qualifiers_deep ~context t1' t2'
- | _, _ -> included_qualifiers ~context (typeAttrs t1) (typeAttrs t2)
-
let compatibleTypes ?strictReturnTypes ?context t1 t2 =
let r = combineTypes ?strictReturnTypes CombineOther t1 t2 in
(* C99, 6.7.3 §9: "... to be compatible, both shall have the identically
@@ -6283,9 +6299,258 @@ let areCompatibleTypes ?strictReturnTypes ?context t1 t2 =
ignore (compatibleTypes ?strictReturnTypes ?context t1 t2); true
with Cannot_combine _ -> false
+(******************** CASTING *****)
+
+
+let checkCast ?context ?(fromsource=false) =
+ let rec default_rec oldt newt =
+ let dkey = Kernel.dkey_typing_cast in
+ let error s =
+ if fromsource
+ then abort_context s
+ else Kernel.fatal ~current:true s
+ in
+ match unrollType oldt, unrollType newt with
+ | TNamed _, _
+ | _, TNamed _ -> Kernel.fatal ~current:true "unrollType failed in checkCast"
+ | t, TInt (IBool, _) when isScalarType t -> ()
+ | TInt _, TInt _ -> ()
+ | TFloat _, TInt _ -> (* ISO 6.3.1.4.1 *) ()
+ | TInt _, TFloat _ -> (* ISO 6.3.1.4.2 *) ()
+ | TFloat _, TFloat _ -> (* ISO 6.3.1.5.1 *) ()
+
+ (* ISO 6.4.4.3 is only about enum constant but ccomp is more permissive. *)
+ | TEnum _, (TInt _ | TFloat _ | TPtr _ | TEnum _)
+ | TFloat _ , TEnum _ -> ()
+ | TPtr _, TEnum _ ->
+ Kernel.debug ~dkey ~current:true
+ "Casting a pointer into an enumeration type"
+ | TInt _, TEnum _ -> ()
+
+ | _, TVoid _ ->
+ (* ISO 6.3.2.2 *)
+ Kernel.debug ~level:3
+ "Casting a value into void: expr is evaluated for side effects"
+ | TPtr (t, _), TPtr (TVoid _, _) when isObjectType t ->
+ (* ISO 6.3.2.3.1 *) ()
+ | TPtr (TVoid _, _), TPtr (t, _) when isObjectType t ->
+ (* ISO 6.3.2.3.1 *) ()
+ | TInt _, TPtr _ -> (* ISO 6.3.2.3.5 *) ()
+ | TPtr _, TInt _ -> (* ISO 6.3.2.3.6 *)
+ if not fromsource && newt != theMachine.upointType
+ then
+ Kernel.warning
+ ~wkey:Kernel.wkey_int_conversion
+ ~current:true
+ "Conversion from a pointer to an integer without an explicit cast"
+ | TPtr (t1, _), TPtr (t2, _) when isObjectType t1 && isObjectType t2 ->
+ (* ISO 6.3.2.3.7 *) ()
+ | TPtr (t1, _), TPtr (t2, _) when isFunctionType t1 && isFunctionType t2 ->
+ (* ISO 6.3.2.3.8 *)
+ if not (areCompatibleTypes ?context oldt newt)
+ then
+ Kernel.warning
+ ~wkey:Kernel.wkey_incompatible_types_call
+ ~current:true
+ "implicit conversion between incompatible function types:@ \
+ %a@ and@ %a"
+ Cil_datatype.Typ.pretty oldt Cil_datatype.Typ.pretty newt
+
+ (* accept converting a ptr to function to/from a ptr to void, even though
+ not really accepted by the standard.
+ Main compilers supports it. *)
+ | TPtr (TFun _, _), TPtr (TVoid _, _) -> ()
+ | TPtr (TVoid _, _), TPtr (TFun _, _) -> ()
+
+ | TFun _, TPtr (TFun _, _) -> (* ISO 6.3.2.1.4 *) ()
+
+ | TArray (t1, _, _), TPtr (t2, _) ->
+ (* ISO 6.3.2.1.3 *)
+ if not (areCompatibleTypes ?context t1 t2)
+ then
+ Kernel.warning
+ ~wkey:Kernel.wkey_incompatible_types_call
+ ~current:true
+ "conversion between incompatible from array type to pointer type:@ \
+ %a@ and@ %a"
+ Cil_datatype.Typ.pretty oldt Cil_datatype.Typ.pretty newt
+
+ | TArray (t1, _, _), TArray (t2, _, _) ->
+ if not (areCompatibleTypes ?context t1 t2)
+ then
+ Kernel.warning
+ ~wkey:Kernel.wkey_incompatible_types_call
+ ~current:true
+ "conversion between incompatible array types :@ \
+ %a@ and@ %a"
+ Cil_datatype.Typ.pretty oldt Cil_datatype.Typ.pretty newt
+
+ (* pointer to potential function type. Note that we do not
+ use unrollTypeDeep above in order to avoid needless divergence with
+ original type in the sources.
+ *)
+ | TPtr (TFun _, _), TPtr (TNamed (ti, nattr), pattr) ->
+ default_rec oldt (TPtr (typeAddAttributes nattr ti.ttype, pattr))
+ | TPtr (TNamed (ti, nattr), pattr), TPtr (TFun _, _) ->
+ default_rec (TPtr (typeAddAttributes nattr ti.ttype, pattr)) newt
+
+ | TFloat _, TPtr _
+ | TPtr _, TFloat _ ->
+ (* ISO 6.5.4.4 *)
+ error "illegal conversion between float and pointers"
+
+ (* No other conversion implying a pointer to function
+ and a pointer to object are supported. *)
+ | TPtr (t1, _), TPtr (t2, _) when isFunctionType t1 && isObjectType t2 ->
+ Kernel.warning
+ ~wkey:Kernel.wkey_incompatible_pointer_types
+ ~current:true
+ "casting function to %a" Cil_datatype.Typ.pretty newt
+ | TPtr (t1, _), TPtr (t2, _) when isFunctionType t2 && isObjectType t1 ->
+ Kernel.warning
+ ~wkey:Kernel.wkey_incompatible_pointer_types
+ ~current:true
+ "casting function from %a" Cil_datatype.Typ.pretty oldt
+
+
+ | _, TPtr (t1, _) when isFunctionType t1 ->
+ error "cannot cast %a to function type"
+ Cil_datatype.Typ.pretty oldt
+
+ | t1, t2 when isArithmeticType t1 && isArithmeticType t2 ->
+ (* ISO 6.5.16.1.1#1 *) ()
+
+
+ | TComp _, TComp _ when areCompatibleTypes oldt newt ->
+ (* ISO 6.5.16.1.1#2*) ()
+
+ (* If we try to pass a transparent union value to a function
+ expecting a transparent union argument, the argument type would
+ have been changed to the type of the first argument, and we'll
+ see a cast from a union to the type of the first argument. Turn
+ that into a field access *)
+ | TComp (_, _), _ ->
+ begin
+ match isTransparentUnion oldt with
+ | None ->
+ abort_context "cast from %a to %a"
+ Cil_datatype.Typ.pretty oldt Cil_datatype.Typ.pretty newt
+ | Some _ -> ()
+ end
+
+ | TBuiltin_va_list _, (TInt _ | TPtr _) -> ()
+
+ | (TInt _ | TPtr _), TBuiltin_va_list _ ->
+ Kernel.debug ~dkey ~current:true
+ "Casting %a to __builtin_va_list" Cil_datatype.Typ.pretty oldt
+
+ | _, t1 when fromsource && not (isScalarType t1) ->
+ (* ISO 6.5.4.2 *)
+ error "Cast over a non-scalar type %a"
+ Cil_datatype.Typ.pretty newt
+
+ | _ ->
+ error "cannot cast from %a to %a@\n"
+ Cil_datatype.Typ.pretty oldt Cil_datatype.Typ.pretty newt
+ in default_rec
+
+let rec castReduce fromsource force =
+ let dkey = Kernel.dkey_typing_cast in
+ let rec rec_default oldt newt e =
+ let loc = e.eloc in
+ let normalized_newt = type_remove_attributes_for_c_cast (unrollType newt) in
+ let res e = new_exp ~loc (CastE (type_remove_qualifier_attributes newt, e)) in
+ match unrollType oldt, normalized_newt, e.enode with
+ (* In the case were we have a representation for the literal,
+ explicitly add the cast. *)
+ | _, TInt (newik, []), Const (CInt64 (i, _, None)) ->
+ (* ISO 6.3.1.3.2 *) kinteger64 ~loc ~kind:newik i
+
+ | _, TPtr _, CastE (_, e') ->
+ begin
+ match unrollType (typeOf e'), e'.enode with
+ | (TPtr _ as typ''), _ ->
+ (* Old cast can be removed...*)
+ if need_cast ~force newt typ'' then res e'
+ else (* In fact, both casts can be removed. *) e'
+ | _, Const (CInt64 (i, _, _)) when Integer.is_zero i -> res e'
+ | _ -> res e
+ end
+
+ | TInt (ik, _), TEnum (ei, _), Const (CEnum { eihost = ei'}) when
+ ei.ename = ei'.ename && not fromsource &&
+ bytesSizeOfInt ik = bytesSizeOfInt ei'.ekind -> e
+
+ | TFun _, TPtr (TFun _, _), Lval lv -> mkAddrOf ~loc lv
+
+ | t, TInt (IBool, _), _ when isScalarType t ->
+ if is_boolean_result e then begin
+ Kernel.debug ~dkey "Explicit cast to Boolean: %a" !pp_exp_ref e;
+ res e
+ end else begin
+ Kernel.debug ~dkey
+ "bool conversion by checking !=0: %a" !pp_exp_ref e;
+ let cmp = mkBinOp ~loc Ne e (integer ~loc 0) in
+ let oldt = typeOf cmp in
+ rec_default oldt newt cmp
+ end
+
+ | TComp _, _, _ ->
+ begin
+ match isTransparentUnion oldt with
+ | None ->
+ abort_context "cast from %a to %a"
+ Cil_datatype.Typ.pretty oldt Cil_datatype.Typ.pretty newt
+ | Some fstfield ->
+ (* We do it now only if the expression is an lval *)
+ let e' =
+ match e.enode with
+ | Lval lv ->
+ new_exp ~loc:e.eloc
+ (Lval (addOffsetLval (Field (fstfield, NoOffset)) lv))
+ | _ ->
+ Kernel.fatal ~current:true
+ "castTo: transparent union expression is not an lval: %a\n"
+ Cil_datatype.Exp.pretty e
+
+ in
+ (* Continue casting *)
+ rec_default fstfield.ftype newt e'
+ end
+
+ | _ -> res e
+ in rec_default
+
+and mkCastTGen ?(check=true) ?context ?(fromsource=false) ?(force=false)
+ ~(oldt: typ) ~(newt: typ) e =
+ let dkey = Kernel.dkey_typing_cast in
+ if
+ (if fromsource
+ then not (need_cast ~force oldt newt)
+ else not (need_cast ~force:false oldt newt))
+ then
+ begin
+ Kernel.debug ~dkey "no cast to perform";
+ let returned_type =
+ match newt with
+ | TNamed _ -> newt
+ | _ -> oldt
+ in
+ (returned_type, e)
+ end
+ else
+ let newt = if fromsource then newt else !typeForInsertedCast e oldt newt in
+ if check then checkCast ?context ~fromsource oldt newt;
+ (newt, castReduce fromsource force oldt newt e)
+
+and mkCastT ?(check=true) ?(force=false) ~(oldt: typ) ~(newt: typ) e =
+ snd (mkCastTGen ~check ~context:Identical ~force ~oldt ~newt e)
+
+and mkCast ?(check=true) ?force ~(newt: typ) e =
+ mkCastT ~check ?force ~oldt:(typeOf e) ~newt e
(* TODO: unify this with doBinOp in Cabs2cil. *)
-let mkBinOp ~loc op e1 e2 =
+and mkBinOp ~loc op e1 e2 =
let t1 = typeOf e1 in
let t2 = typeOf e2 in
let machdep = false in
@@ -6317,7 +6582,7 @@ let mkBinOp ~loc op e1 e2 =
let compare_pointer op ?cast1 ?cast2 e1 e2 =
let do_cast e = function
| None -> e
- | Some t' -> mkCastT ~force:false ~oldt:(typeOf e) ~newt:t' e
+ | Some t' -> mkCast ~force:false ~newt:t' e
in
let e1, e2 =
if need_cast ~force:true (typeOf e1) (typeOf e2) then
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index ed7a2d90c3bacd176d6bfedd45e46a4b0f203ea8..202240172646694cf72d8211023f7a858620703c 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -587,6 +587,11 @@ val isFunPtrType: typ -> bool
@since 18.0-Argon *)
val isLogicFunPtrType: logic_type -> bool
+(** Check if a type is a transparent union, and return the first field
+
+ @since Frama-C+dev *)
+val isTransparentUnion : typ -> fieldinfo option
+
(** True if the argument is the type for reified C types. *)
val isTypeTagType: logic_type -> bool
@@ -1150,17 +1155,67 @@ val mkString: loc:location -> string -> exp
*)
val need_cast: ?force:bool -> typ -> typ -> bool
+(** [typeForInsertedCast expr original_type destination_type]
+ returns the type into which [expr], which has type [original_type] and
+ whose type must be converted into [destination_type], must be casted.
+
+ By default, returns [destination_type].
+
+ This applies only to implicit casts. Casts already present
+ in the source code are exempt from this hook.
+
+ @since Frama-C+dev*)
+val typeForInsertedCast: (exp -> typ -> typ -> typ) ref
+
+(** [checkCast context fromsource oldt newt] emits a warning or an error
+ if the cast from [oldt] to [newt] is invalid.
+ Otherwise, doesn't make anything.
+ [fromsource] is [false] (default) if the cast is not from the source.
+ Check [areCompatibleTypes] documentation for [context].
+
+ Suspicious cases that only emits a warning :
+ - Implicit cast from a pointer to an integer.
+ - Cast from a pointer to a function type to another pointer to a function
+ type when the function types are not compatible.
+ - Cast from an array to a pointer/array when types are not compatible.
+ - Cast, in both directions, between pointer to an object type and pointer
+ to a function type.
+
+ @since Frama-C+dev*)
+val checkCast:
+ ?context:qualifier_check_context -> ?fromsource:bool -> typ -> typ -> unit
+
+
+(** Generic version of {!Cil.mkCastT}.
+ Construct a cast when having the old type of the expression.
+ [fromsource] is [false] (default) if the cast is not from the source.
+ If [check] is [true] (default), we check that the cast is valid,
+ fail if the cast is invalid.
+ If the new type is the same as the old type, then no cast is added,
+ unless [force] is [true] (default is [false]).
+ Casting from [oldt] to [newt].
+ Take the expression as argument and can modify it.
+ Return the new type and the new expression.
+
+ @since Frama-C+dev
+*)
+val mkCastTGen: ?check:bool -> ?context:qualifier_check_context ->
+ ?fromsource:bool -> ?force:bool -> oldt:typ -> newt:typ -> exp -> typ * 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, unless [force]
- is [true] (default is [false])
+ is [true] (default is [false]).
+ Fail if the cast is invalid.
@before 23.0-Vanadium different order of arguments.
+ @before Frama-C+dev no [check] argument, it was always [false].
*)
-val mkCastT: ?force:bool -> oldt:typ -> newt:typ -> exp -> exp
+val mkCastT: ?check:bool -> ?force:bool -> oldt:typ -> newt:typ -> exp -> exp
(** Like {!Cil.mkCastT} but uses typeOf to get [oldt]
@before 23.0-Vanadium different order of arguments.
+ @before Frama-C+dev no [check] argument, it was always [false].
*)
-val mkCast: ?force:bool -> newt:typ -> exp -> exp
+val mkCast: ?check:bool -> ?force:bool -> newt:typ -> exp -> exp
(** Equivalent to [stripCasts] for terms. *)
val stripTermCasts: term -> term
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 13ea19b232fa3826cfcc3e388b49a4c67132d3a5..4cfddc62f891ddba3b715a74d7d4d96e67a2cd96 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -1351,53 +1351,21 @@ struct
end
- let rec c_cast_to ot nt e =
+ let c_cast_to ot nt e =
if is_same_c_type ot nt then (ot, e)
- else begin
- let result = (nt, mk_cast e (Ctype nt)) in
- match ot, nt with
- | TNamed(r, _), _ -> c_cast_to r.ttype nt e
- | _, TNamed(r, _) -> c_cast_to ot r.ttype e
- | TInt(_ikindo,_), TInt(_ikindn,_) ->
- result
- | TInt _, TPtr _ -> result
- | TPtr _, TInt _ -> result
- | ((TArray (told,_,_) | TPtr (told,_)),
- (TPtr (tnew,_) | TArray(tnew,_,_)))
- when is_same_c_type told tnew -> result
- | (TPtr _ | TArray _), (TPtr _ | TArray _)
- when isLogicNull e -> result
- | TPtr _, TPtr _ when isVoidPtrType nt -> (nt, e)
- | TPtr (t1,_), TPtr (t2,_) when
- Cil.isFunctionType t1 &&
- Cil.isFunctionType t2 &&
- is_compatible_funtype t1 t2 -> result
- | TEnum _, TInt _ -> result
- | TFloat _, (TInt _|TEnum _) -> result
- | (TInt _|TEnum _), TFloat _ -> result
- | TFloat _, TFloat _ -> result
- | TInt _, TEnum _ -> result
- | TEnum _, TEnum _ -> result
- | TEnum _, TPtr _ -> result
- | TBuiltin_va_list _, (TInt _ | TPtr _) ->
- result
- | (TInt _ | TPtr _), TBuiltin_va_list _ ->
- Kernel.debug ~level:3 "Casting %a to __builtin_va_list"
- Cil_printer.pp_typ ot;
- result
- | TPtr _, TEnum _ ->
- Kernel.debug ~level:3 "Casting a pointer into an enumeration type";
- result
- | (TInt _ | TEnum _ | TPtr _ ), TVoid _ ->
- (ot, e)
- | TComp (comp1, _), TComp (comp2, _)
- when comp1.ckey = comp2.ckey ->
- nt, e
- | _ ->
- Kernel.fatal ~current:true
- "Logic_typing.c_cast_to: %a -> %a@."
- Cil_printer.pp_typ ot Cil_printer.pp_typ nt
- end
+ else
+ begin
+ Cil.checkCast ot nt;
+ match Cil.unrollType ot, Cil.unrollType nt with
+ | TPtr _, TPtr _ when isVoidPtrType nt ->
+ nt, e
+ | (TInt _ | TEnum _ | TPtr _ ), TVoid _ ->
+ ot, e
+ | TComp (comp1, _), TComp (comp2, _) when comp1.ckey = comp2.ckey ->
+ nt, e
+ | _ -> nt, mk_cast e (Ctype nt)
+ end
+
(* for overloading: raised when an arguments list does not fit a
formal parameter list *)
diff --git a/src/plugins/variadic/standard.ml b/src/plugins/variadic/standard.ml
index 16c4a9e8c6bc82d96fc80b0af123a0ec641ab783..98eefe0444d8a2b8313c137f22f55668bff17537 100644
--- a/src/plugins/variadic/standard.ml
+++ b/src/plugins/variadic/standard.ml
@@ -138,7 +138,7 @@ let cast_arg i paramtyp exp =
(i + 1)
pretty_typ argtyp pretty_typ paramtyp
end;
- Cil.mkCast ~force:false ~newt:paramtyp exp
+ Cil.mkCast ~check:false ~force:false ~newt:paramtyp exp
(* cast a list of args to the tparams list of types and remove unused args *)
diff --git a/tests/syntax/Enum_repr.ml b/tests/syntax/Enum_repr.ml
index 907d611a59531e83826bbde6cf7e45831311cc4d..3346cb44b0cf42d98bf275a8489e244f30513bf6 100644
--- a/tests/syntax/Enum_repr.ml
+++ b/tests/syntax/Enum_repr.ml
@@ -1,13 +1,13 @@
open Cil_types
let warn_cast =
- let typeForInsertedCast = !Cabs2cil.typeForInsertedCast in
+ let typeForInsertedCast = !Cil.typeForInsertedCast in
fun e t1 t2 ->
Kernel.feedback ~source:(fst e.eloc) "Inserted implicit cast from %a to %a"
Printer.pp_typ t1 Printer.pp_typ t2;
typeForInsertedCast e t1 t2
-let () = Cabs2cil.typeForInsertedCast := warn_cast
+let () = Cil.typeForInsertedCast := warn_cast
let run () =
let f = Ast.get () in
diff --git a/tests/syntax/inserted_casts.ml b/tests/syntax/inserted_casts.ml
index ebd466c230473c94bf6623deb3dffb01e1017fea..87e83b394c134b127227ba1b3d14565b5fd1aa19 100644
--- a/tests/syntax/inserted_casts.ml
+++ b/tests/syntax/inserted_casts.ml
@@ -11,4 +11,4 @@ let print_warning e ot nt =
nt
;;
-Cabs2cil.typeForInsertedCast := print_warning
+Cil.typeForInsertedCast := print_warning
diff --git a/tests/syntax/oracle/array_cast_bts1099.res.oracle b/tests/syntax/oracle/array_cast_bts1099.res.oracle
index 09ba17a47e269d5a40446c613f67d7d35cd6f4fd..4d39dbf0d7d154c649c738f8b024cd5518ecde1d 100644
--- a/tests/syntax/oracle/array_cast_bts1099.res.oracle
+++ b/tests/syntax/oracle/array_cast_bts1099.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing array_cast_bts1099.i (no preprocessing)
[kernel] array_cast_bts1099.i:12: User Error:
- explicit cast: cast over a non-scalar type t
+ Cast over a non-scalar type t
10 int tab1[4];
11 u* p = &tab1;
12 t* p2 = (t) p;
diff --git a/tests/syntax/oracle/wrong-assignment.res.oracle b/tests/syntax/oracle/wrong-assignment.res.oracle
index 85766b5401ffebf7cee24786897212ae7241fedc..e3ed14ddfe7d6fbd0482c6d74157fd906d72f0a4 100644
--- a/tests/syntax/oracle/wrong-assignment.res.oracle
+++ b/tests/syntax/oracle/wrong-assignment.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing wrong-assignment.i (no preprocessing)
[kernel] wrong-assignment.i:13: User Error:
- implicit cast: ebool -> _Bool
+ cast from ebool to _Bool
11 void d() {
12 // this assignment should be rejected
13 c.a = b;