@@ -1371,6 +1371,45 @@ let rec integralPromotion (t : typ) : typ = (* c.f. ISO 6.3.1.1 *)
13711371 | TEnum (ei , a ) -> integralPromotion (TInt (ei.ekind, a)) (* gcc packed enums can be < int *)
13721372 | t -> E. s (error " integralPromotion: not expecting %a" d_type t)
13731373
1374+ (* Integer promotion for bit-fields (c.f. ISO 6.3.1.1): the width of the
1375+ bit-field restricts the range of representable values, so a bit-field of
1376+ a wider type (e.g. long : 7) may still be promotable to int. *)
1377+ let rec integralPromotionBitfield (t : typ ) (width : int ) : typ =
1378+ let int_bits = bitsSizeOf (TInt (IInt , [] )) in
1379+ match unrollType t with
1380+ | TInt (IBool, a ) -> TInt (IInt , a)
1381+ | TInt (ik , a ) ->
1382+ if width < int_bits then TInt (IInt , a)
1383+ else if width = int_bits then
1384+ if isSigned ik then TInt (IInt , a) else TInt (IUInt , a)
1385+ else TInt (ik, a) (* width > int_bits: no promotion *)
1386+ | TEnum (ei , a ) -> integralPromotionBitfield (TInt (ei.ekind, a)) width
1387+ | t -> E. s (error " integralPromotionBitfield: not expecting %a" d_type t)
1388+
1389+ (* If the expression is a direct bit-field lvalue, return the bit-field width;
1390+ otherwise return None. Used to apply bit-field-aware integer promotion.
1391+ Handles nested field accesses (e.g. s.inner.bf) by examining the last
1392+ field in the offset chain. *)
1393+ let bitfieldWidthOfExp (e : exp ) : int option =
1394+ let rec lastBitfieldInOffset off =
1395+ match off with
1396+ | NoOffset -> None
1397+ | Field (fi , NoOffset) -> fi.fbitfield
1398+ | Field (_ , sub ) -> lastBitfieldInOffset sub
1399+ | Index (_ , sub ) -> lastBitfieldInOffset sub
1400+ in
1401+ match e with
1402+ | Lval (_ , off ) -> lastBitfieldInOffset off
1403+ | _ -> None
1404+
1405+ (* Apply integer promotion considering a possible bit-field restriction.
1406+ If [e] is a bit-field lvalue, uses its width; otherwise falls back to
1407+ the regular integralPromotion. *)
1408+ let integralPromotionE (e : exp ) (t : typ ) : typ =
1409+ match bitfieldWidthOfExp e with
1410+ | Some width -> integralPromotionBitfield t width
1411+ | None -> integralPromotion t
1412+
13741413let defaultArgumentPromotion (t : typ ) : typ = (* c.f. ISO 6.5.2.2:6 *)
13751414 match unrollType t with
13761415 | TFloat (FFloat, a ) -> TFloat (FDouble , a)
@@ -4008,7 +4047,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *)
40084047 | A. UNARY (A. MINUS, e ) ->
40094048 let (se, e', t) = doExp asconst e (AExp None ) in
40104049 if isIntegralType t then
4011- let tres = integralPromotion t in
4050+ let tres = integralPromotionE e' t in
40124051 let fallback = UnOp (Neg , makeCastT ~kind: IntegerPromotion ~e: e' ~oldt: t ~newt: tres, tres) in
40134052 let e'' =
40144053 match e', tres with
@@ -4025,7 +4064,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *)
40254064 | A. UNARY (A. BNOT, e ) ->
40264065 let (se, e', t) = doExp asconst e (AExp None ) in
40274066 if isIntegralType t then
4028- let tres = integralPromotion t in
4067+ let tres = integralPromotionE e' t in
40294068 let e'' = UnOp (BNot , makeCastT ~kind: IntegerPromotion ~e: e' ~oldt: t ~newt: tres, tres) in
40304069 finishExp se e'' tres
40314070 else
@@ -4034,7 +4073,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *)
40344073 | A. UNARY (A. PLUS, e ) ->
40354074 let (se, e', t) = doExp asconst e (AExp None ) in
40364075 if isIntegralType t then
4037- let tres = integralPromotion t in
4076+ let tres = integralPromotionE e' t in
40384077 let e'' = makeCastT ~kind: IntegerPromotion ~e: e' ~oldt: t ~newt: tres in
40394078 finishExp se e'' tres
40404079 else
@@ -4477,7 +4516,12 @@ and doExp (asconst: bool) (* This expression is used as a constant *)
44774516 -- gcc manual *)
44784517 (sa :: ss, a' :: args')
44794518 else
4480- let promoted_type = defaultArgumentPromotion at in
4519+ (* For bit-field arguments, apply bit-field-aware promotion
4520+ to get the correct effective type before default arg promotion. *)
4521+ let eff_at = match bitfieldWidthOfExp a' with
4522+ | Some w -> integralPromotionBitfield at w
4523+ | None -> at in
4524+ let promoted_type = defaultArgumentPromotion eff_at in
44814525 let _, a'' = castTo ~kind: DefaultArgumentPromotion at promoted_type a' in
44824526 (sa :: ss, a'' :: args')
44834527 in
@@ -5048,8 +5092,15 @@ and doExp (asconst: bool) (* This expression is used as a constant *)
50485092 | _ -> true
50495093 | exception (Failure _ ) -> false
50505094 in
5051- let (_, _ , e_typ) = doExp false e (AExp None ) in (* doExp with AExp handles array and function types for "lvalue conversions" (AType would not!) *)
5095+ let (_, e_expr , e_typ) = doExp false e (AExp None ) in (* doExp with AExp handles array and function types for "lvalue conversions" (AType would not!) *)
50525096 let e_typ = removeOuterQualifierAttributes e_typ in (* removeOuterQualifierAttributes handles qualifiers for "lvalue conversions" *)
5097+ (* ISO 6.5.1.1: if the controlling expression is a bit-field lvalue,
5098+ integer promotions are applied and the type after promotion is used
5099+ for association matching. For non-bit-field expressions, the type
5100+ is NOT subject to integer promotions here. *)
5101+ let e_typ = match bitfieldWidthOfExp e_expr with
5102+ | Some w -> integralPromotionBitfield e_typ w
5103+ | None -> e_typ in
50535104 let al_compatible = List. filter (fun ((ast , adt ), _ ) -> typ_compatible e_typ (doOnlyType ast adt)) al_nondefault in
50545105
50555106 (* TODO: error when multiple compatible associations or defaults even when unused? *)
@@ -5075,21 +5126,29 @@ and doExp (asconst: bool) (* This expression is used as a constant *)
50755126(* bop is always the arithmetic version. Change it to the appropriate pointer
50765127 version if necessary *)
50775128and doBinOp (bop : binop ) (e1 : exp ) (t1 : typ ) (e2 : exp ) (t2 : typ ) : typ * exp =
5129+ (* For bit-field lvalue expressions, the integer promotion (ISO 6.3.1.1)
5130+ must account for the bit-field width, not just the base type.
5131+ pt1/pt2 are the effectively-promoted types used for arithmetic; the
5132+ original t1/t2 are still used as oldt in casts. *)
5133+ let pt1 = match bitfieldWidthOfExp e1 with
5134+ | Some w -> integralPromotionBitfield t1 w | None -> t1 in
5135+ let pt2 = match bitfieldWidthOfExp e2 with
5136+ | Some w -> integralPromotionBitfield t2 w | None -> t2 in
50785137 let doArithmetic () =
5079- let tres = arithmeticConversion t1 t2 in
5138+ let tres = arithmeticConversion pt1 pt2 in
50805139 (* Keep the operator since it is arithmetic *)
50815140 tres,
50825141 optConstFoldBinOp false bop (makeCastT ~kind: ArithmeticConversion ~e: e1 ~oldt: t1 ~newt: tres) (makeCastT ~kind: ArithmeticConversion ~e: e2 ~oldt: t2 ~newt: tres) tres
50835142 in
50845143 let doArithmeticComp () =
5085- let tres = arithmeticConversion t1 t2 in
5144+ let tres = arithmeticConversion pt1 pt2 in
50865145 (* Keep the operator since it is arithmetic *)
50875146 intType,
50885147 optConstFoldBinOp false bop
50895148 (makeCastT ~kind: ArithmeticConversion ~e: e1 ~oldt: t1 ~newt: tres) (makeCastT ~kind: ArithmeticConversion ~e: e2 ~oldt: t2 ~newt: tres) intType
50905149 in
50915150 let doIntegralArithmetic () =
5092- let tres = unrollType (arithmeticConversion t1 t2 ) in
5151+ let tres = unrollType (arithmeticConversion pt1 pt2 ) in
50935152 match tres with
50945153 TInt _ ->
50955154 tres,
@@ -5110,8 +5169,8 @@ and doBinOp (bop: binop) (e1: exp) (t1: typ) (e2: exp) (t2: typ) : typ * exp =
51105169 | (Mod |BAnd |BOr |BXor ) -> doIntegralArithmetic ()
51115170 | (Shiftlt |Shiftrt ) -> (* ISO 6.5.7. Only integral promotions. The result
51125171 has the same type as the left hand side *)
5113- let t1' = integralPromotion t1 in
5114- let t2' = integralPromotion t2 in
5172+ let t1' = integralPromotion pt1 in
5173+ let t2' = integralPromotion pt2 in
51155174 t1',
51165175 optConstFoldBinOp false bop (makeCastT ~kind: IntegerPromotion ~e: e1 ~oldt: t1 ~newt: t1') (makeCastT ~kind: IntegerPromotion ~e: e2 ~oldt: t2 ~newt: t2') t1'
51175176
@@ -5123,15 +5182,15 @@ and doBinOp (bop: binop) (e1: exp) (t1: typ) (e2: exp) (t2: typ) : typ * exp =
51235182 | PlusA when isPointerType t1 && isIntegralType t2 ->
51245183 t1,
51255184 optConstFoldBinOp false PlusPI e1
5126- (makeCastT ~kind: IntegerPromotion ~e: e2 ~oldt: t2 ~newt: (integralPromotion t2 )) t1
5185+ (makeCastT ~kind: IntegerPromotion ~e: e2 ~oldt: t2 ~newt: (integralPromotion pt2 )) t1
51275186 | PlusA when isIntegralType t1 && isPointerType t2 ->
51285187 t2,
51295188 optConstFoldBinOp false PlusPI e2
5130- (makeCastT ~kind: IntegerPromotion ~e: e1 ~oldt: t1 ~newt: (integralPromotion t1 )) t2
5189+ (makeCastT ~kind: IntegerPromotion ~e: e1 ~oldt: t1 ~newt: (integralPromotion pt1 )) t2
51315190 | MinusA when isPointerType t1 && isIntegralType t2 ->
51325191 t1,
51335192 optConstFoldBinOp false MinusPI e1
5134- (makeCastT ~kind: IntegerPromotion ~e: e2 ~oldt: t2 ~newt: (integralPromotion t2 )) t1
5193+ (makeCastT ~kind: IntegerPromotion ~e: e2 ~oldt: t2 ~newt: (integralPromotion pt2 )) t1
51355194 | MinusA when isPointerType t1 && isPointerType t2 ->
51365195 let commontype = t1 in
51375196 ! ptrdiffType,
@@ -6945,7 +7004,7 @@ and doStatement (s : A.statement) : chunk =
69457004 let (se, e', et) = doExp false e (AExp None ) in
69467005 if not (Cil. isIntegralType et) then
69477006 E. s (error " Switch on a non-integer expression." );
6948- let et' = integralPromotion et in
7007+ let et' = integralPromotionE e' et in
69497008 let e' = makeCastT ~kind: IntegerPromotion ~e: e' ~oldt: et ~newt: et' in
69507009 enter_break_env () ;
69517010 let s' = doStatement s in
0 commit comments