diff --git a/src/plugins/rte/rte.ml b/src/plugins/rte/rte.ml
index ad09f17f5533787fd4579322c2bd0d2d88e1560c..4d77766b988eea59d5549224cf79f63637d645c0 100644
--- a/src/plugins/rte/rte.ml
+++ b/src/plugins/rte/rte.ml
@@ -357,88 +357,38 @@ let shift_overflow_assertion ~signed ~remove_trivial ~on_alarm (exp, op, lexp, r
end
else overflow_alarm ()
-(* assertion for downcasting an integer to an unsigned integer type
- without requiring modification of value to reach target domain
- (well-defined behavior though) *)
-let unsigned_downcast_assertion ~remove_trivial ~on_alarm (ty, exp) =
- let e_typ = Cil.unrollType (Cil.typeOf exp) in
- match e_typ with
- | TInt (kind,_) ->
- let szTo = Cil.bitsSizeOfBitfield ty in
- let szFrom = Cil.bitsSizeOf e_typ in
- (if szTo < szFrom || Cil.isSigned kind then
- (* case signed to unsigned:
- requires signed to be >= 0 and also <= max of unsigned size *)
- (* cast unsigned to unsigned:
- ok is same bit size ;
- if target is <, requires <= max target *)
- let max_ty = Cil.max_unsigned_number szTo in
- let alarm ?(invalid=false) bk =
- let b = match bk with
- | Lower_bound -> Integer.zero
- | Upper_bound -> max_ty
- in
- let a = Alarms.Overflow (Alarms.Unsigned_downcast, exp, b, bk) in
- on_alarm ~invalid a;
- in
- let alarms () =
- if Cil.isSigned kind then begin (* signed to unsigned *)
- alarm Upper_bound;
- alarm Lower_bound;
- end else (* unsigned to unsigned; cannot overflow in the negative *)
- alarm Upper_bound;
- in
- if remove_trivial then begin
- match get_expr_val exp with
- | None -> alarms ()
- | Some a64 ->
- if Integer.lt a64 Integer.zero then
- alarm ~invalid:true Lower_bound
- else if Integer.gt a64 max_ty then
- alarm ~invalid:true Upper_bound
- end
- else alarms ())
- | _ -> ()
-
-(* assertion for downcasting an integer to a signed integer type
- which can raise an implementation defined behavior *)
-let signed_downcast_assertion ~remove_trivial ~on_alarm (ty, exp) =
- let e_typ = Cil.unrollType (Cil.typeOf exp) in
- match e_typ with
- | TInt (kind,_) ->
- (let szTo = Cil.bitsSizeOfBitfield ty in
- let szFrom = Cil.bitsSizeOf e_typ in
- if szTo < szFrom || (szTo == szFrom && not (Cil.isSigned kind)) then
- (* downcast: the expression result should fit on szTo bits *)
- let min_ty = Cil.min_signed_number szTo in
- let max_ty = Cil.max_signed_number szTo in
- let alarm ?(invalid=false) bk =
- let b = match bk with
- | Lower_bound -> min_ty
- | Upper_bound -> max_ty
- in
- let a = Alarms.Overflow (Alarms.Signed_downcast, exp, b, bk) in
- on_alarm ~invalid a;
- in
- let alarms () =
- if Cil.isSigned kind then begin
- (* signed to signed *)
- alarm Upper_bound;
- alarm Lower_bound
- end else (* (unsigned to signed; cannot overflow in the negative *)
- alarm Upper_bound
- in
- if remove_trivial then begin
- match get_expr_val exp with
- | None -> alarms ()
- | Some a64 ->
- (if Integer.lt a64 min_ty then
- alarm ~invalid:true Lower_bound
- else if Integer.gt a64 max_ty then
- alarm ~invalid:true Upper_bound)
- end
- else alarms ())
- | _ -> ()
+(* Assertion for downcasts. *)
+let downcast_assertion ~remove_trivial ~on_alarm (dst_type, exp) =
+ let src_type = Cil.typeOf exp in
+ let src_signed = Cil.isSignedInteger src_type in
+ let dst_signed = Cil.isSignedInteger dst_type in
+ let src_size = Cil.bitsSizeOf src_type in
+ let dst_size = Cil.bitsSizeOfBitfield dst_type in
+ if dst_size < src_size || dst_size == src_size && dst_signed <> src_signed
+ then
+ let dst_min, dst_max =
+ if dst_signed
+ then Cil.min_signed_number dst_size, Cil.max_signed_number dst_size
+ else Integer.zero, Cil.max_unsigned_number dst_size
+ in
+ let overflow_kind =
+ if dst_signed then Alarms.Signed_downcast else Alarms.Unsigned_downcast
+ in
+ let alarm ?(invalid=false) bound bound_kind =
+ let a = Alarms.Overflow (overflow_kind, exp, bound, bound_kind) in
+ on_alarm ~invalid a;
+ in
+ let alarms () =
+ alarm dst_max Upper_bound;
+ (* unsigned values cannot overflow in the negative *)
+ if src_signed then alarm dst_min Lower_bound;
+ in
+ match remove_trivial, get_expr_val exp with
+ | true, Some a64 ->
+ let invalid = true in
+ if Integer.lt a64 dst_min then alarm ~invalid dst_min Lower_bound
+ else if Integer.gt a64 dst_max then alarm ~invalid dst_max Upper_bound
+ | _ -> alarms ()
(* assertion for casting a floating-point value to an integer *)
let float_to_int_assertion ~remove_trivial ~on_alarm (ty, exp) =
diff --git a/src/plugins/rte/rte.mli b/src/plugins/rte/rte.mli
index 766fa82c8568a3ee0a48717c8664e32fd5f7ac61..7c787c279a81d18e1eae71b1683d411036e8874d 100644
--- a/src/plugins/rte/rte.mli
+++ b/src/plugins/rte/rte.mli
@@ -40,8 +40,7 @@ val shift_negative_assertion: exp alarm_gen
val shift_overflow_assertion: signed:bool -> (exp * binop * exp * exp) alarm_gen
val mult_sub_add_assertion: signed:bool -> (exp * binop * exp * exp) alarm_gen
val uminus_assertion: exp alarm_gen
-val signed_downcast_assertion: (typ * exp) alarm_gen
-val unsigned_downcast_assertion: (typ * exp) alarm_gen
+val downcast_assertion: (typ * exp) alarm_gen
val float_to_int_assertion: (typ * exp) alarm_gen
val finite_float_assertion: (fkind * exp) alarm_gen
val pointer_call: (exp * exp list) alarm_gen
diff --git a/src/plugins/rte/visit.ml b/src/plugins/rte/visit.ml
index 2592651085e9ff2cdbdfb3c001d3190e7503343a..4919cfdef8106b34ae4cc4b5ecefcb24009da2db 100644
--- a/src/plugins/rte/visit.ml
+++ b/src/plugins/rte/visit.ml
@@ -308,14 +308,12 @@ class annot_visitor kf flags on_alarm = object (self)
(match Cil.unrollType ty, Cil.unrollType (Cil.typeOf e) with
(* to , from *)
| TInt(kind,_), TInt (_, _) ->
- if Cil.isSigned kind then begin
- if self#do_signed_downcast () then begin
- self#generate_assertion Rte.signed_downcast_assertion (ty, e);
- self#mark_to_skip e;
- end
- end
- else if self#do_unsigned_downcast () then
- self#generate_assertion Rte.unsigned_downcast_assertion (ty, e)
+ let signed = Cil.isSigned kind in
+ if signed && self#do_signed_downcast ()
+ || not signed && self#do_unsigned_downcast ()
+ then self#generate_assertion Rte.downcast_assertion (ty, e);
+ if signed && self#do_signed_downcast ()
+ then self#mark_to_skip e;
| TInt _, TFloat _ ->
if self#do_float_to_int () then