diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index ae9503e76ad6f3103eb254f1c1ef9ada04b085c8..2faab4979f1ef4dc46ae06fff1b2c4bf2fe77d1f 100644
--- a/src/kernel_services/ast_data/alarms.ml
+++ b/src/kernel_services/ast_data/alarms.ml
@@ -23,7 +23,8 @@
open Cil_types
open Cil_datatype
-type overflow_kind = Signed | Unsigned | Signed_downcast | Unsigned_downcast
+type overflow_kind =
+ Signed | Unsigned | Signed_downcast | Unsigned_downcast | Pointer_downcast
type access_kind = For_reading | For_writing
type bound_kind = Lower_bound | Upper_bound
@@ -32,6 +33,7 @@ let string_of_overflow_kind = function
| Unsigned -> "unsigned_overflow"
| Signed_downcast -> "signed_downcast"
| Unsigned_downcast -> "unsigned_downcast"
+ | Pointer_downcast -> "pointer_downcast"
type alarm =
| Division_by_zero of exp
@@ -549,6 +551,9 @@ let create_predicate ?(loc=Location.unknown) alarm =
(* n <= e or e <= n according to bound *)
let loc = best_loc ~loc e.eloc in
let t = match kind with
+ | Pointer_downcast ->
+ let t = Logic_utils.expr_to_term ~cast:true e in
+ Logic_const.tcast ~loc t Cil.theMachine.upointType
| Signed_downcast | Unsigned_downcast ->
Logic_utils.expr_to_term ~cast:true e
| _ ->
diff --git a/src/kernel_services/ast_data/alarms.mli b/src/kernel_services/ast_data/alarms.mli
index c301b2e797c6de7ed2675f805bfb997c7edecf29..a369dc60f2b76309b0ac2fed63a1474550724a4d 100644
--- a/src/kernel_services/ast_data/alarms.mli
+++ b/src/kernel_services/ast_data/alarms.mli
@@ -25,9 +25,10 @@
open Cil_types
-(** Only signed overflows int are really RTEs. The other kinds may be
- meaningful nevertheless. *)
-type overflow_kind = Signed | Unsigned | Signed_downcast | Unsigned_downcast
+(** Only signed overflows and pointer downcasts are really RTEs.
+ The other kinds may be meaningful nevertheless. *)
+type overflow_kind =
+ Signed | Unsigned | Signed_downcast | Unsigned_downcast | Pointer_downcast
type access_kind = For_reading | For_writing
type bound_kind = Lower_bound | Upper_bound
diff --git a/src/kernel_services/ast_queries/logic_const.ml b/src/kernel_services/ast_queries/logic_const.ml
index 8da10c3cf6910de2ce69ffa4b223bd79679c70ca..e9417dd0256ab638e8fe3f476d30be8edbac6c0f 100644
--- a/src/kernel_services/ast_queries/logic_const.ml
+++ b/src/kernel_services/ast_queries/logic_const.ml
@@ -305,6 +305,9 @@ let tat ?(loc=Cil_datatype.Location.unknown) (t,label) =
let told ?(loc=Cil_datatype.Location.unknown) t = tat ~loc (t,old_label)
+let tcast ?(loc=Cil_datatype.Location.unknown) t ct =
+ term ~loc (TCastE (ct, t)) (Ctype ct)
+
let tlogic_coerce ?(loc=Cil_datatype.Location.unknown) t lt =
term ~loc (TLogic_coerce (lt, t)) lt
diff --git a/src/kernel_services/ast_queries/logic_const.mli b/src/kernel_services/ast_queries/logic_const.mli
index c3be4194f94c20ce9dafc1719ca405b9397f19ca..280661c522f5e0027260323c72bf8ba1eb32da41 100644
--- a/src/kernel_services/ast_queries/logic_const.mli
+++ b/src/kernel_services/ast_queries/logic_const.mli
@@ -321,6 +321,9 @@ val tvar: ?loc:Location.t -> logic_var -> term
(** \result *)
val tresult: ?loc:Location.t -> typ -> term
+(** cast to the given C type *)
+val tcast: ?loc:Location.t -> term -> typ -> term
+
(** coercion to the given logic type *)
val tlogic_coerce: ?loc:Location.t -> term -> logic_type -> term
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index e5ea4748e6b3950a654a49ab29c868d7d79db2c9..2453bded6360dc01a4109b3724d32b37fb135586 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -1018,6 +1018,7 @@ module RteGen = struct
let get_pointerCall_status = mk_fun "RteGen.get_pointerCall_status"
let get_unsignedOv_status = mk_fun "RteGen.get_unsignedOv_status"
let get_unsignedDownCast_status = mk_fun "RteGen.get_unsignedDownCast_status"
+ let get_pointer_downcast_status = mk_fun "RteGen.get_pointer_downcast_status"
let get_float_to_int_status = mk_fun "RteGen.get_float_to_int_status"
let get_finite_float_status = mk_fun "RteGen.get_finite_float_status"
let get_bool_value_status = mk_fun "RteGen.get_bool_value_status"
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 565c20806a04f78a636ff9dca8a062f9e6af3b87..a54ae74932d0942ba3df7aa1508675e0dda9c5a8 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -900,6 +900,7 @@ module RteGen : sig
val get_signed_downCast_status : (unit -> status_accessor) ref
val get_unsignedOv_status : (unit -> status_accessor) ref
val get_unsignedDownCast_status : (unit -> status_accessor) ref
+ val get_pointer_downcast_status : (unit -> status_accessor) ref
val get_float_to_int_status : (unit -> status_accessor) ref
val get_finite_float_status : (unit -> status_accessor) ref
val get_bool_value_status : (unit -> status_accessor) ref
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 4dca12b991c27963dddde65a1dce642c4c9e3016..a7ffdfeb73030844ef69826fe1814b3bdced74c7 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -1440,6 +1440,17 @@ module UnsignedDowncast =
destination range"
end)
+(* Pointer downcasts are undefined behaviors. *)
+let () = Parameter_customize.set_group analysis_options
+let () = Parameter_customize.do_not_reset_on_copy ()
+module PointerDowncast =
+ True
+ (struct
+ let module_name = "PointerDowncast"
+ let option_name = "-warn-pointer-downcast"
+ let help = "generate alarms when a pointer is converted into an integer \
+ but may not be in the range of the destination type."
+ end)
(* Not finite floats are ok, but might not always be a behavior the programmer
wants. *)
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 87ffd853c1c5593cfb4b3ae4153ea6f521e000f2..04ef6317f0c2e63a44f15a244e79a31947ae9b1c 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -540,6 +540,9 @@ module SignedDowncast: Parameter_sig.Bool
module UnsignedDowncast: Parameter_sig.Bool
(** Behavior of option "-warn-unsigned-downcast" *)
+module PointerDowncast: Parameter_sig.Bool
+(** Behavior of option "-warn-pointer-downcast" *)
+
module SpecialFloat: Parameter_sig.String
(** Behavior of option "-warn-special-float" *)
diff --git a/src/plugins/rte/flags.ml b/src/plugins/rte/flags.ml
index 5a5efb9c60c333de0bf18346135e72ea20f3f04d..7d17b15a3a9577579b409c2396f89060023f48a8 100644
--- a/src/plugins/rte/flags.ml
+++ b/src/plugins/rte/flags.ml
@@ -36,6 +36,7 @@ type t = {
unsigned_overflow: bool;
signed_downcast: bool;
unsigned_downcast: bool;
+ pointer_downcast: bool;
float_to_int: bool;
finite_float: bool;
pointer_call: bool;
@@ -54,6 +55,7 @@ let all = {
unsigned_overflow = true;
signed_downcast = true;
unsigned_downcast = true;
+ pointer_downcast = true;
float_to_int = true;
finite_float = true;
pointer_call = true;
@@ -72,6 +74,7 @@ let none = {
unsigned_overflow = false;
signed_downcast = false;
unsigned_downcast = false;
+ pointer_downcast = false;
float_to_int = false;
finite_float = false;
pointer_call = false;
@@ -95,6 +98,7 @@ let default
?unsigned_overflow
?signed_downcast
?unsigned_downcast
+ ?pointer_downcast
?float_to_int
?finite_float
?pointer_call
@@ -112,6 +116,7 @@ let default
unsigned_overflow = option Kernel.UnsignedOverflow.get unsigned_overflow ;
signed_downcast = option Kernel.SignedDowncast.get signed_downcast ;
unsigned_downcast = option Kernel.UnsignedDowncast.get unsigned_downcast ;
+ pointer_downcast = option Kernel.PointerDowncast.get pointer_downcast ;
float_to_int = option Options.DoFloatToInt.get float_to_int ;
finite_float = option (fun () -> Kernel.SpecialFloat.get () <> "none") finite_float ;
pointer_call = option Options.DoPointerCall.get pointer_call ;
diff --git a/src/plugins/rte/flags.mli b/src/plugins/rte/flags.mli
index f90a63a3afa4e02c1b7bb15b94c0a68857ae633a..3ea19d53f367e367c1a0e414871403d5bef54d1b 100644
--- a/src/plugins/rte/flags.mli
+++ b/src/plugins/rte/flags.mli
@@ -38,6 +38,7 @@ type t = {
unsigned_overflow: bool;
signed_downcast: bool;
unsigned_downcast: bool;
+ pointer_downcast: bool;
float_to_int: bool;
finite_float: bool;
pointer_call: bool;
@@ -57,6 +58,7 @@ val default :
?unsigned_overflow:bool ->
?signed_downcast:bool ->
?unsigned_downcast:bool ->
+ ?pointer_downcast:bool ->
?float_to_int:bool ->
?finite_float:bool ->
?pointer_call:bool ->
diff --git a/src/plugins/rte/generator.ml b/src/plugins/rte/generator.ml
index 67214fae804fe5ab58da7821c3507b3f8aebb3cd..8c8e697d4dcf846db06cb7c6062fc9b5fd9847a1 100644
--- a/src/plugins/rte/generator.ml
+++ b/src/plugins/rte/generator.ml
@@ -155,6 +155,14 @@ module Unsigned_downcast =
let additional_parameters = []
end)
+module Pointer_downcast =
+ Make
+ (struct
+ let name = "pointer_downcast"
+ let parameter = Kernel.PointerDowncast.parameter
+ let additional_parameters = []
+ end)
+
module Float_to_int =
Make
(struct
diff --git a/src/plugins/rte/generator.mli b/src/plugins/rte/generator.mli
index 1e1c61ccd3a87124d5ef785ef2ef72e73f23d123..1518a0acc67f22908320d834bb54b1f99c22eec4 100644
--- a/src/plugins/rte/generator.mli
+++ b/src/plugins/rte/generator.mli
@@ -39,6 +39,7 @@ module Signed_overflow: S
module Signed_downcast: S
module Unsigned_overflow: S
module Unsigned_downcast: S
+module Pointer_downcast: S
module Float_to_int: S
module Finite_float: S
module Bool_value: S
diff --git a/src/plugins/rte/register.ml b/src/plugins/rte/register.ml
index ed9296659abc8dc7463e90a2c1ec372b45cd1c8e..8b5afe27c054f83e273da685237efc10d5899d2d 100644
--- a/src/plugins/rte/register.ml
+++ b/src/plugins/rte/register.ml
@@ -93,6 +93,7 @@ let () =
nojournal_register get_pointerCall_status Pointer_call.accessor;
nojournal_register get_unsignedOv_status Unsigned_overflow.accessor;
nojournal_register get_unsignedDownCast_status Unsigned_downcast.accessor;
+ nojournal_register get_pointer_downcast_status Pointer_downcast.accessor;
nojournal_register get_float_to_int_status Float_to_int.accessor;
nojournal_register get_finite_float_status Finite_float.accessor;
nojournal_register get_bool_value_status Bool_value.accessor ;
diff --git a/src/plugins/rte/rte.ml b/src/plugins/rte/rte.ml
index ad09f17f5533787fd4579322c2bd0d2d88e1560c..467d65f1ffd919d19c5ef4f4784c8cef98e9b490 100644
--- a/src/plugins/rte/rte.ml
+++ b/src/plugins/rte/rte.ml
@@ -357,88 +357,42 @@ 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 Cil.isPointerType src_type
+ then Alarms.Pointer_downcast
+ else 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..61dafe98471f4ed4f86338f62319019ef54b5c44 100644
--- a/src/plugins/rte/visit.ml
+++ b/src/plugins/rte/visit.ml
@@ -86,6 +86,10 @@ class annot_visitor kf flags on_alarm = object (self)
flags.Flags.unsigned_downcast
&& not (Generator.Unsigned_downcast.is_computed kf)
+ method private do_pointer_downcast () =
+ flags.Flags.pointer_downcast
+ && not (Generator.Pointer_downcast.is_computed kf)
+
method private do_float_to_int () =
flags.Flags.float_to_int && not (Generator.Float_to_int.is_computed kf)
@@ -307,15 +311,16 @@ class annot_visitor kf flags on_alarm = object (self)
| CastE (ty, e) ->
(match Cil.unrollType ty, Cil.unrollType (Cil.typeOf e) with
(* to , from *)
+ | TInt _, TPtr _ when self#do_pointer_downcast () ->
+ self#generate_assertion Rte.downcast_assertion (ty, e)
+
| 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
@@ -455,6 +460,7 @@ let annotate ?flags kf =
comp Signed_downcast.accessor flags.signed_downcast |||
comp Unsigned_overflow.accessor flags.unsigned_overflow |||
comp Unsigned_downcast.accessor flags.unsigned_downcast |||
+ comp Pointer_downcast.accessor flags.pointer_downcast |||
comp Float_to_int.accessor flags.float_to_int |||
comp Finite_float.accessor flags.finite_float |||
comp Bool_value.accessor flags.bool_value
diff --git a/src/plugins/value/alarmset.ml b/src/plugins/value/alarmset.ml
index fa27012f076cd1e98586412b941bcc6c1c9411b8..1738ac4a35a476f78bd46f46e5816d3361d7ef16 100644
--- a/src/plugins/value/alarmset.ml
+++ b/src/plugins/value/alarmset.ml
@@ -309,6 +309,7 @@ let emit_alarm kinstr alarm (status:status) =
| Alarms.Unsigned -> "unsigned overflow"
| Alarms.Signed_downcast -> "signed downcast"
| Alarms.Unsigned_downcast -> "unsigned downcast"
+ | Alarms.Pointer_downcast -> "pointer downcast"
in
register_alarm str
diff --git a/src/plugins/value/engine/evaluation.ml b/src/plugins/value/engine/evaluation.ml
index 43eb4404fe604f3061b01f4241b9ea65c0f87f37..ab391eb3546aa0c66ad31105fa65c3ab7156fca6 100644
--- a/src/plugins/value/engine/evaluation.ml
+++ b/src/plugins/value/engine/evaluation.ml
@@ -665,7 +665,7 @@ module Make
in
cast_integer Alarms.Signed_downcast expr ~src ~dst value
- let cast_int_to_int expr ~src ~dst value =
+ let cast_int_to_int expr ~ptr ~src ~dst value =
(* Regain some precision in case a transfer function was imprecise.
This should probably be done in the transfer function, though. *)
let value =
@@ -675,16 +675,19 @@ module Make
in
if Eval_typ.range_inclusion src dst
then return value (* Upcast, nothing to check. *)
- else if dst.i_signed then (* Signed downcast. *)
- if Kernel.SignedDowncast.get ()
- then cast_integer Alarms.Signed_downcast expr ~src ~dst value
- else if Value_parameters.WarnSignedConvertedDowncast.get ()
+ else
+ let overflow_kind, warn =
+ if ptr
+ then Alarms.Pointer_downcast, Kernel.PointerDowncast.get
+ else if dst.i_signed
+ then Alarms.Signed_downcast, Kernel.SignedDowncast.get
+ else Alarms.Unsigned_downcast, Kernel.UnsignedDowncast.get
+ in
+ if warn ()
+ then cast_integer overflow_kind expr ~src ~dst value
+ else if dst.i_signed && Value_parameters.WarnSignedConvertedDowncast.get ()
then relaxed_signed_downcast expr ~src ~dst value
else return (Value.rewrap_integer dst value)
- else (* Unsigned downcast. *)
- if Kernel.UnsignedDowncast.get ()
- then cast_integer Alarms.Unsigned_downcast expr ~src ~dst value
- else return (Value.rewrap_integer dst value)
(* Re-export type here *)
type scalar_typ = Eval_typ.scalar_typ =
@@ -728,15 +731,17 @@ module Make
| Some src_type, Some dst_type ->
let value, alarms =
match src_type, dst_type with
- | (TSInt src | TSPtr src), (TSInt dst | TSPtr dst) ->
- cast_int_to_int ~src ~dst expr value
+ | TSPtr src, TSInt dst ->
+ cast_int_to_int ~ptr:true ~src ~dst expr value
+ | TSInt src, (TSInt dst | TSPtr dst) ->
+ cast_int_to_int ~ptr:false ~src ~dst expr value
| TSFloat src, (TSInt dst | TSPtr dst) ->
restrict_float ~reduce:true ~assume_finite:true expr src value >>=
truncate_float src dst expr
| (TSInt _ | TSPtr _), TSFloat _ ->
(* Cannot overflow with 32 bits float. *)
- `Value value, Alarmset.none
- | TSFloat _, TSFloat _ -> `Value value, Alarmset.none
+ return value
+ | TSFloat _, TSFloat _ | TSPtr _, TSPtr _ -> return value
in
value >>- Value.forward_cast ~src_type ~dst_type, alarms
diff --git a/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
index ec9df06d3ed29feb21b4fef6d0321d049ac1d8aa..545c7824113ee498d7e686c7b3111bcb02302b1a 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
@@ -25,6 +25,8 @@
Assigning imprecise value to b.
The imprecision originates from Arithmetic
{tests/known/printf_garbled_mix.c:6}
+[eva:alarm] tests/known/printf_garbled_mix.c:7: Warning:
+ pointer downcast. assert (unsigned int)b ≤ 2147483647;
[eva] using specification for function printf_va_1
[eva] tests/known/printf_garbled_mix.c:8:
Frama_C_show_each_nb_printed: [-2147483648..2147483647]
@@ -67,6 +69,7 @@ void main(void)
{
int a[2] = {1, 2};
int *b = (int *)((unsigned int)(a) * (unsigned int)2);
+ /*@ assert Eva: pointer_downcast: (unsigned int)b ≤ 2147483647; */
int nb_printed = printf_va_1("%d",(int)b);
Frama_C_show_each_nb_printed(nb_printed);
b = (int *)0;
diff --git a/tests/builtins/oracle/Longinit_sequencer.res.oracle b/tests/builtins/oracle/Longinit_sequencer.res.oracle
index 2a0c3fd82a978552927c8aed7b96e5f48b92d07a..7593544dbd939e453a2870b1e76c873fc147295a 100644
--- a/tests/builtins/oracle/Longinit_sequencer.res.oracle
+++ b/tests/builtins/oracle/Longinit_sequencer.res.oracle
@@ -2,17 +2,14 @@
[kernel] Parsing tests/builtins/long_init.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
-[eva] tests/builtins/long_init.c:34:
- Assigning imprecise value to garbled_mix.
- The imprecision originates from Arithmetic {tests/builtins/long_init.c:34}
+[eva:alarm] tests/builtins/long_init.c:34: Warning:
+ pointer downcast. assert (unsigned int)"abc" ≤ 127;
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
nondet ∈ [--..--]
a1[0..9] ∈ {0}
stuff ∈ {0}
- garbled_mix ∈
- {{ garbled mix of &{"abc"}
- (origin: Arithmetic {tests/builtins/long_init.c:34}) }}
+ garbled_mix ∈ {{ "abc" }}
s ∈ {{ "abc" }}
pr ∈ {0}
pr2 ∈ {0}
@@ -73,6 +70,8 @@
[eva] tests/builtins/long_init.c:73:
Call to builtin Frama_C_malloc_fresh for function malloc
[eva] tests/builtins/long_init.c:73: allocating variable __malloc_init_inner_l73
+[eva:alarm] tests/builtins/long_init.c:74: Warning:
+ pointer downcast. assert (unsigned int)alloc1 ≤ 2147483647;
[eva] tests/builtins/long_init.c:75:
Call to builtin Frama_C_malloc_fresh for function malloc
[eva] tests/builtins/long_init.c:75: allocating variable __malloc_init_inner_l75
@@ -130,9 +129,7 @@
.d[7] ∈ {21.875}
.d[8] ∈ {25.}
.d[9] ∈ {28.125}
- garbled_mix ∈
- {{ garbled mix of &{"abc"}
- (origin: Arithmetic {tests/builtins/long_init.c:34}) }}
+ garbled_mix ∈ {{ "abc" }}
s ∈ {{ "abc" }}
pr ∈ ESCAPINGADDR
pr2 ∈ ESCAPINGADDR
@@ -170,6 +167,8 @@
[eva] tests/builtins/long_init.c:104: allocating variable __malloc_main_l104
[eva] Recording results for main
[eva] done for function main
+[eva] tests/builtins/long_init.c:34:
+ cannot evaluate ACSL term, unsupported ACSL construct: constant strings
[eva] Saving globals state after call to function: init_inner
Values at end of function dmin:
__retres ∈ [93.9166666667 .. 110.791666667]
@@ -297,17 +296,14 @@ Values at end of function main:
__retres ∈ {0}[kernel] Parsing tests/builtins/long_init2.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
-[eva] tests/builtins/long_init2.c:34:
- Assigning imprecise value to garbled_mix.
- The imprecision originates from Arithmetic {tests/builtins/long_init2.c:34}
+[eva:alarm] tests/builtins/long_init2.c:34: Warning:
+ pointer downcast. assert (unsigned int)"abc" ≤ 127;
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
nondet ∈ [--..--]
a1[0..9] ∈ {0}
stuff ∈ {0}
- garbled_mix ∈
- {{ garbled mix of &{"abc"}
- (origin: Arithmetic {tests/builtins/long_init2.c:34}) }}
+ garbled_mix ∈ {{ "abc" }}
s ∈ {{ "abc" }}
another_global ∈ {42}
pr ∈ {0}
@@ -325,7 +321,6 @@ Values at end of function main:
Call to builtin Frama_C_load_state for function init_inner
[eva] Skipping call to init_inner, loading globals state from file:
tests/builtins/result/Longinit_sequencer.sav
-[eva] Warning: importing garbled mix, locations may have changed
[eva] Warning: variable `r' is not global, possibly an escaping value; ignoring
[eva] Warning: variable `r2' is not global, possibly an escaping value; ignoring
[eva] Warning: variable `r2' is not global, possibly an escaping value; ignoring
@@ -371,9 +366,7 @@ Values at end of function main:
.d[7] ∈ {21.875}
.d[8] ∈ {25.}
.d[9] ∈ {28.125}
- garbled_mix ∈
- {{ garbled mix of &{"abc"}
- (origin: Arithmetic {tests/builtins/long_init.c:34}) }}
+ garbled_mix ∈ {{ "abc" }}
s ∈ {{ "abc" }}
another_global ∈ {42}
pr ∈ ESCAPINGADDR
@@ -446,6 +439,8 @@ Values at end of function main:
[eva] tests/builtins/long_init2.c:104: allocating variable __malloc_main_l104
[eva] Recording results for main
[eva] done for function main
+[eva] tests/builtins/long_init2.c:34:
+ cannot evaluate ACSL term, unsupported ACSL construct: constant strings
[eva] Saving globals state after call to function: init_outer
@@ -539,17 +534,14 @@ Values at end of function main:
__retres ∈ {0}[kernel] Parsing tests/builtins/long_init3.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
-[eva] tests/builtins/long_init3.c:34:
- Assigning imprecise value to garbled_mix.
- The imprecision originates from Arithmetic {tests/builtins/long_init3.c:34}
+[eva:alarm] tests/builtins/long_init3.c:34: Warning:
+ pointer downcast. assert (unsigned int)"abc" ≤ 127;
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
nondet ∈ [--..--]
a1[0..9] ∈ {0}
stuff ∈ {0}
- garbled_mix ∈
- {{ garbled mix of &{"abc"}
- (origin: Arithmetic {tests/builtins/long_init3.c:34}) }}
+ garbled_mix ∈ {{ "abc" }}
s ∈ {{ "abc" }}
another_global ∈ {42}
yet_another_global ∈ {43}
@@ -566,7 +558,6 @@ Values at end of function main:
Call to builtin Frama_C_load_state for function init_outer
[eva] Skipping call to init_outer, loading globals state from file:
tests/builtins/result/Longinit_sequencer.sav
-[eva] Warning: importing garbled mix, locations may have changed
[eva] Warning: found new global variable `yet_another_global'
[eva] tests/builtins/long_init3.c:92:
Frama_C_dump_each:
@@ -607,9 +598,7 @@ Values at end of function main:
.d[7] ∈ {21.875}
.d[8] ∈ {25.}
.d[9] ∈ {28.125}
- garbled_mix ∈
- {{ garbled mix of &{"abc"}
- (origin: Arithmetic {tests/builtins/long_init.c:34}) }}
+ garbled_mix ∈ {{ "abc" }}
s ∈ {{ "abc" }}
another_global ∈ {42}
yet_another_global ∈ {43}
@@ -683,6 +672,8 @@ Values at end of function main:
[eva] tests/builtins/long_init3.c:104: allocating variable __malloc_main_l104
[eva] Recording results for main
[eva] done for function main
+[eva] tests/builtins/long_init3.c:34:
+ cannot evaluate ACSL term, unsupported ACSL construct: constant strings
Values at end of function dmin:
diff --git a/tests/builtins/oracle/alloc.0.res.oracle b/tests/builtins/oracle/alloc.0.res.oracle
index 257776baaff09cd5091b410914f02fdfcbe6fadc..b124e2220d17a6d8a85d3bb9dc74b91e716d5a75 100644
--- a/tests/builtins/oracle/alloc.0.res.oracle
+++ b/tests/builtins/oracle/alloc.0.res.oracle
@@ -34,6 +34,8 @@
all target addresses were invalid. This path is assumed to be dead.
[eva] tests/builtins/alloc.c:25: Call to builtin Frama_C_malloc_fresh
[eva] tests/builtins/alloc.c:25: allocating variable __malloc_main_l25
+[eva:alarm] tests/builtins/alloc.c:26: Warning:
+ pointer downcast. assert (unsigned int)q ≤ 2147483647;
[eva:alarm] tests/builtins/alloc.c:26: Warning:
signed overflow. assert -2147483648 ≤ -((int)q);
[eva:alarm] tests/builtins/alloc.c:26: Warning:
diff --git a/tests/builtins/oracle/alloc.1.res.oracle b/tests/builtins/oracle/alloc.1.res.oracle
index b4990cc4a79455a5bf971a573423df33d4f1d5fb..48c4356d116b6568051f121123841c9f5b03d047 100644
--- a/tests/builtins/oracle/alloc.1.res.oracle
+++ b/tests/builtins/oracle/alloc.1.res.oracle
@@ -15,6 +15,8 @@
ch ∈ {44}
[eva] tests/builtins/alloc.c:50: Call to builtin Frama_C_malloc_fresh
[eva] tests/builtins/alloc.c:50: allocating variable __malloc_main_abs_l50
+[eva:alarm] tests/builtins/alloc.c:51: Warning:
+ pointer downcast. assert (unsigned int)q ≤ 2147483647;
[eva:alarm] tests/builtins/alloc.c:51: Warning:
signed overflow. assert -2147483648 ≤ -((int)q);
[eva:alarm] tests/builtins/alloc.c:51: Warning:
@@ -24,6 +26,8 @@
The imprecision originates from Arithmetic {tests/builtins/alloc.c:51}
[eva:alarm] tests/builtins/alloc.c:54: Warning:
out of bounds write. assert \valid(r);
+[eva:alarm] tests/builtins/alloc.c:54: Warning:
+ pointer downcast. assert (unsigned int)r ≤ 2147483647;
[eva:alarm] tests/builtins/alloc.c:56: Warning:
signed overflow. assert -2147483648 ≤ *q + 1;
[eva:alarm] tests/builtins/alloc.c:56: Warning:
diff --git a/tests/builtins/oracle/alloc_weak.res.oracle b/tests/builtins/oracle/alloc_weak.res.oracle
index 5a584e372684c98e4aa9b566bf7ddcda96c4ca45..7705984008d4c08d656c18cda171bb1d1adb99e5 100644
--- a/tests/builtins/oracle/alloc_weak.res.oracle
+++ b/tests/builtins/oracle/alloc_weak.res.oracle
@@ -41,6 +41,10 @@
Called from tests/builtins/alloc_weak.c:73.
[eva] tests/builtins/alloc_weak.c:37: Call to builtin malloc
[eva] tests/builtins/alloc_weak.c:37: allocating variable __malloc_main2_l37
+[eva:alarm] tests/builtins/alloc_weak.c:37: Warning:
+ pointer downcast.
+ assert (unsigned int)tmp ≤ 2147483647;
+ (tmp from malloc(sizeof(int)))
[eva] tests/builtins/alloc_weak.c:40:
Trace partitioning superposing up to 100 states
[eva] tests/builtins/alloc_weak.c:40:
diff --git a/tests/builtins/oracle/imprecise-malloc-free.res.oracle b/tests/builtins/oracle/imprecise-malloc-free.res.oracle
index 82e150fd29421edf85c87ee0fc822d57ea050e75..4d7ac635f76867055ff5101b207043750e18500c 100644
--- a/tests/builtins/oracle/imprecise-malloc-free.res.oracle
+++ b/tests/builtins/oracle/imprecise-malloc-free.res.oracle
@@ -4,6 +4,10 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
i ∈ [--..--]
+[eva:alarm] tests/builtins/imprecise-malloc-free.c:12: Warning:
+ pointer downcast. assert (unsigned int)(&size1 + i) ≤ 2147483647;
+[eva:alarm] tests/builtins/imprecise-malloc-free.c:13: Warning:
+ pointer downcast. assert (unsigned int)(&size2) ≤ 2147483647;
[eva:alarm] tests/builtins/imprecise-malloc-free.c:13: Warning:
signed overflow. assert -2147483648 ≤ i + (int)((int)(&size2) >> 1);
[eva:alarm] tests/builtins/imprecise-malloc-free.c:13: Warning:
@@ -12,6 +16,8 @@
Assigning imprecise value to size2.
The imprecision originates from Arithmetic
{tests/builtins/imprecise-malloc-free.c:13}
+[eva:alarm] tests/builtins/imprecise-malloc-free.c:14: Warning:
+ pointer downcast. assert (unsigned int)(&i) ≤ 2147483647;
[eva] tests/builtins/imprecise-malloc-free.c:14: Call to builtin malloc
[eva] tests/builtins/imprecise-malloc-free.c:14:
allocating variable __malloc_main_l14
@@ -30,15 +36,25 @@
(origin: Arithmetic {tests/builtins/imprecise-malloc-free.c:19}) }}
[eva:alarm] tests/builtins/imprecise-malloc-free.c:21: Warning:
out of bounds write. assert \valid(p);
+[eva:alarm] tests/builtins/imprecise-malloc-free.c:21: Warning:
+ pointer downcast. assert (unsigned int)(p + 1) ≤ 2147483647;
[eva:alarm] tests/builtins/imprecise-malloc-free.c:22: Warning:
out of bounds write. assert \valid(q);
+[eva:alarm] tests/builtins/imprecise-malloc-free.c:22: Warning:
+ pointer downcast. assert (unsigned int)(q + 2) ≤ 2147483647;
[eva:alarm] tests/builtins/imprecise-malloc-free.c:23: Warning:
out of bounds write. assert \valid(r);
+[eva:alarm] tests/builtins/imprecise-malloc-free.c:23: Warning:
+ pointer downcast. assert (unsigned int)(r + 3) ≤ 2147483647;
+[eva:alarm] tests/builtins/imprecise-malloc-free.c:25: Warning:
+ pointer downcast. assert (unsigned int)p ≤ 2147483647;
[eva] tests/builtins/imprecise-malloc-free.c:25: Call to builtin free
[eva:alarm] tests/builtins/imprecise-malloc-free.c:25: Warning:
function free: precondition 'freeable' got status unknown.
[eva:malloc] tests/builtins/imprecise-malloc-free.c:25:
weak free on bases: {__malloc_main_l14}
+[eva:alarm] tests/builtins/imprecise-malloc-free.c:26: Warning:
+ pointer downcast. assert (unsigned int)r ≤ 2147483647;
[eva] tests/builtins/imprecise-malloc-free.c:26: Call to builtin free
[eva:alarm] tests/builtins/imprecise-malloc-free.c:26: Warning:
function free: precondition 'freeable' got status unknown.
diff --git a/tests/builtins/oracle/imprecise.res.oracle b/tests/builtins/oracle/imprecise.res.oracle
index 35235461d13ed2ecd8659d12fcde6992bb47ce76..f93b938207e84054d6ecd4daf5c6a9740816884a 100644
--- a/tests/builtins/oracle/imprecise.res.oracle
+++ b/tests/builtins/oracle/imprecise.res.oracle
@@ -48,6 +48,8 @@
[eva] Done for function invalid_assigns_imprecise
[eva] computing for function write_garbled <- main.
Called from tests/builtins/imprecise.c:145.
+[eva:alarm] tests/builtins/imprecise.c:19: Warning:
+ pointer downcast. assert (unsigned int)(&k) ≤ 2147483647;
[eva] tests/builtins/imprecise.c:19:
Assigning imprecise value to p.
The imprecision originates from Arithmetic {tests/builtins/imprecise.c:19}
@@ -78,6 +80,8 @@
s1.[bits 0 to ..] ∈ {0} or UNINITIALIZED
s2.[bits 0 to ..] ∈ {0} or UNINITIALIZED
==END OF DUMP==
+[eva:alarm] tests/builtins/imprecise.c:22: Warning:
+ pointer downcast. assert (unsigned int)p ≤ 2147483647;
[eva] Recording results for write_garbled
[from] Computing for function write_garbled
[from] Done for function write_garbled
@@ -105,6 +109,8 @@
cannot evaluate ACSL term, unsupported ACSL construct: logic function memset
[eva:alarm] tests/builtins/imprecise.c:53: Warning:
out of bounds write. assert \valid(p2);
+[eva:alarm] tests/builtins/imprecise.c:53: Warning:
+ pointer downcast. assert (unsigned int)(&addr) ≤ 2147483647;
[eva:alarm] tests/builtins/imprecise.c:56: Warning:
out of bounds write. assert \valid(p4);
[eva:alarm] tests/builtins/imprecise.c:58: Warning:
@@ -117,9 +123,8 @@
[eva] Done for function abstract_structs
[eva] computing for function cast_address <- main.
Called from tests/builtins/imprecise.c:147.
-[eva] tests/builtins/imprecise.c:66:
- Assigning imprecise value to c1.
- The imprecision originates from Arithmetic {tests/builtins/imprecise.c:66}
+[eva:alarm] tests/builtins/imprecise.c:66: Warning:
+ pointer downcast. assert (unsigned int)p ≤ 127;
[eva:alarm] tests/builtins/imprecise.c:68: Warning:
signed overflow. assert -2147483648 ≤ (int)*((char *)(&p)) + 0;
[eva:alarm] tests/builtins/imprecise.c:68: Warning:
@@ -276,9 +281,7 @@
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function cast_address:
p ∈ {{ &x }}
- c1 ∈
- {{ garbled mix of &{x}
- (origin: Arithmetic {tests/builtins/imprecise.c:66}) }}
+ c1 ∈ {{ (char)&x }}
c2# ∈ {{ (? *)&x }}%32, bits 0 to 7
c3 ∈
{{ garbled mix of &{x}
@@ -621,6 +624,8 @@
[eva] Done for function invalid_assigns_imprecise
[eva] computing for function write_garbled <- main.
Called from tests/builtins/imprecise.c:145.
+[eva:alarm] tests/builtins/imprecise.c:19: Warning:
+ pointer downcast. assert (unsigned int)(&k) ≤ 2147483647;
[eva:alarm] tests/builtins/imprecise.c:20: Warning:
out of bounds write. assert \valid(p);
[eva] tests/builtins/imprecise.c:21:
@@ -657,6 +662,8 @@
S_0_S_p_gm_null[0..1] ∈ [--..--]
S_1_S_p_gm_null[0..1] ∈ [--..--]
==END OF DUMP==
+[eva:alarm] tests/builtins/imprecise.c:22: Warning:
+ pointer downcast. assert (unsigned int)p ≤ 2147483647;
[eva] Recording results for write_garbled
[from] Computing for function write_garbled
[from] Done for function write_garbled
@@ -678,6 +685,8 @@
[eva] tests/builtins/imprecise.c:51: Call to builtin memset
[eva:alarm] tests/builtins/imprecise.c:53: Warning:
out of bounds write. assert \valid(p2);
+[eva:alarm] tests/builtins/imprecise.c:53: Warning:
+ pointer downcast. assert (unsigned int)(&addr) ≤ 2147483647;
[eva:alarm] tests/builtins/imprecise.c:56: Warning:
out of bounds write. assert \valid(p4);
[eva:alarm] tests/builtins/imprecise.c:58: Warning:
@@ -690,6 +699,8 @@
[eva] Done for function abstract_structs
[eva] computing for function cast_address <- main.
Called from tests/builtins/imprecise.c:147.
+[eva:alarm] tests/builtins/imprecise.c:66: Warning:
+ pointer downcast. assert (unsigned int)p ≤ 127;
[eva:alarm] tests/builtins/imprecise.c:68: Warning:
signed overflow. assert -2147483648 ≤ (int)*((char *)(&p)) + 0;
[eva:alarm] tests/builtins/imprecise.c:68: Warning:
@@ -826,9 +837,7 @@
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function cast_address:
p ∈ {{ &x }}
- c1 ∈
- {{ garbled mix of &{x}
- (origin: Arithmetic {tests/builtins/imprecise.c:66}) }}
+ c1 ∈ {{ (char)&x }}
c2# ∈ {{ (? *)&x }}%32, bits 0 to 7
c3 ∈
{{ garbled mix of &{x}
diff --git a/tests/builtins/oracle/memchr.res.oracle b/tests/builtins/oracle/memchr.res.oracle
index 228d7406ba2bb1a8b76ab084431e8a9005743923..4fbe20f941e39805a6270ea36816a8f5df791524 100644
--- a/tests/builtins/oracle/memchr.res.oracle
+++ b/tests/builtins/oracle/memchr.res.oracle
@@ -477,6 +477,8 @@
[eva] Done for function memchr_bitfields2
[eva] computing for function memchr_escaping <- main.
Called from tests/builtins/memchr.c:662.
+[eva:alarm] tests/builtins/memchr.c:264: Warning:
+ pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva:locals-escaping] tests/builtins/memchr.c:264: Warning:
locals {x} escaping the scope of a block of memchr_escaping through s
[eva] tests/builtins/memchr.c:267: Call to builtin memchr
diff --git a/tests/builtins/oracle/memcpy.res.oracle b/tests/builtins/oracle/memcpy.res.oracle
index 8e73401933cf18244067ab5c84f7b50c269d724f..68da16922725ebdd4a044ba722aef0cc200d86fe 100644
--- a/tests/builtins/oracle/memcpy.res.oracle
+++ b/tests/builtins/oracle/memcpy.res.oracle
@@ -128,6 +128,8 @@
function memcpy: precondition 'valid_src' got status valid.
[eva] tests/builtins/memcpy.c:85:
function memcpy: precondition 'separation' got status valid.
+[eva:alarm] tests/builtins/memcpy.c:87: Warning:
+ pointer downcast. assert (unsigned int)((struct t1 *)t) ≤ 2147483647;
[eva] tests/builtins/memcpy.c:87: Call to builtin memcpy
[eva] tests/builtins/memcpy.c:87:
function memcpy: precondition 'valid_dest' got status valid.
@@ -135,6 +137,8 @@
function memcpy: precondition 'valid_src' got status unknown.
[eva] tests/builtins/memcpy.c:87:
function memcpy: precondition 'separation' got status valid.
+[eva:alarm] tests/builtins/memcpy.c:89: Warning:
+ pointer downcast. assert (unsigned int)(&v4) ≤ 2147483647;
[eva] tests/builtins/memcpy.c:89: Call to builtin memcpy
[eva:alarm] tests/builtins/memcpy.c:89: Warning:
function memcpy: precondition 'valid_dest' got status unknown.
@@ -145,6 +149,10 @@
[kernel] tests/builtins/memcpy.c:89:
writing somewhere in {NULL; v4} because of Arithmetic
{tests/builtins/memcpy.c:89}.
+[eva:alarm] tests/builtins/memcpy.c:90: Warning:
+ pointer downcast. assert (unsigned int)((struct t1 *)t) ≤ 2147483647;
+[eva:alarm] tests/builtins/memcpy.c:91: Warning:
+ pointer downcast. assert (unsigned int)(&v5) ≤ 2147483647;
[eva] tests/builtins/memcpy.c:91: Call to builtin memcpy
[eva:alarm] tests/builtins/memcpy.c:91: Warning:
function memcpy: precondition 'valid_dest' got status unknown.
@@ -452,6 +460,7 @@
[from] Non-terminating function main_all (no dependencies)
[from] Done for function main_all
[eva] done for function main_all
+[scope:rm_asserts] removing 1 assertion(s)
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function init:
src[0] ∈ {1}
@@ -1871,6 +1880,15 @@
tried with Eva.
[ - ] Assertion (file tests/builtins/memcpy.c, line 152)
tried with Eva.
+[ - ] Assertion 'Eva,pointer_downcast' (file tests/builtins/memcpy.c, line 87)
+ tried with Eva.
+[ - ] Assertion 'Eva,pointer_downcast' (file tests/builtins/memcpy.c, line 89)
+ tried with Eva.
+[ Partial ] Assertion 'Eva,pointer_downcast' (file tests/builtins/memcpy.c, line 90)
+ By RedundantAlarms, with pending:
+ - Assertion 'Eva,pointer_downcast' (file tests/builtins/memcpy.c, line 87)
+[ - ] Assertion 'Eva,pointer_downcast' (file tests/builtins/memcpy.c, line 91)
+ tried with Eva.
[ Valid ] Instance of 'Pre-condition 'valid_dest'' at call 'memcpy' (file tests/builtins/memcpy.c, line 68)
by Eva.
@@ -2221,8 +2239,9 @@
--- Status Report Summary
--------------------------------------------------------------------------------
162 Completely validated
+ 1 Locally validated
239 Considered valid
- 29 To be validated
+ 32 To be validated
4 Alarms emitted
- 434 Total
+ 438 Total
--------------------------------------------------------------------------------
diff --git a/tests/builtins/oracle/memset.res.oracle b/tests/builtins/oracle/memset.res.oracle
index c53d0987526cc622b257198546a75defbd30cf08..e2c146788658bd30ae5e489e1134b1800830daf9 100644
--- a/tests/builtins/oracle/memset.res.oracle
+++ b/tests/builtins/oracle/memset.res.oracle
@@ -25,6 +25,8 @@
function memset: precondition 'valid_s' got status valid.
[eva] share/libc/string.h:118:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memset
+[eva:alarm] tests/builtins/memset.c:34: Warning:
+ pointer downcast. assert (unsigned int)((int *)t2) ≤ 2147483647;
[eva] tests/builtins/memset.c:34: Call to builtin memset
[eva:alarm] tests/builtins/memset.c:34: Warning:
function memset: precondition 'valid_s' got status unknown.
@@ -42,6 +44,8 @@
[eva] tests/builtins/memset.c:38: Call to builtin memset
[eva:alarm] tests/builtins/memset.c:38: Warning:
function memset: precondition 'valid_s' got status invalid.
+[eva:alarm] tests/builtins/memset.c:41: Warning:
+ pointer downcast. assert (unsigned int)((int *)t1) ≤ 2147483647;
[eva] tests/builtins/memset.c:41: Call to builtin memset
[eva] tests/builtins/memset.c:41:
function memset: precondition 'valid_s' got status valid.
diff --git a/tests/builtins/oracle/strchr.res.oracle b/tests/builtins/oracle/strchr.res.oracle
index 8a69adef2398b5bbf8d7160b7d1a3e684b8d0e90..21fd920919affc8afd1710f3d43042b975c924b3 100644
--- a/tests/builtins/oracle/strchr.res.oracle
+++ b/tests/builtins/oracle/strchr.res.oracle
@@ -316,6 +316,8 @@
[eva] Done for function strchr_bitfields2
[eva] computing for function strchr_escaping <- main.
Called from tests/builtins/strchr.c:556.
+[eva:alarm] tests/builtins/strchr.c:258: Warning:
+ pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva:locals-escaping] tests/builtins/strchr.c:258: Warning:
locals {x} escaping the scope of a block of strchr_escaping through s
[eva] tests/builtins/strchr.c:261: Call to builtin strchr
@@ -669,9 +671,13 @@
[eva] Done for function strchr_invalid
[eva] computing for function strchr_garbled_mix_in_char <- main.
Called from tests/builtins/strchr.c:562.
+[eva:alarm] tests/builtins/strchr.c:541: Warning:
+ pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva] tests/builtins/strchr.c:541:
Assigning imprecise value to garbled.
The imprecision originates from Arithmetic {tests/builtins/strchr.c:541}
+[eva:alarm] tests/builtins/strchr.c:542: Warning:
+ pointer downcast. assert (unsigned int)garbled ≤ 2147483647;
[eva] tests/builtins/strchr.c:542: Call to builtin strchr
[eva:alarm] tests/builtins/strchr.c:542: Warning:
function strchr: precondition 'valid_string_s' got status invalid.
diff --git a/tests/builtins/oracle/strlen.res.oracle b/tests/builtins/oracle/strlen.res.oracle
index 7d20e2bba7eacaab18db9c9debc5ceeb2f032fbe..dcc09a3de5d1cf947b9d8f050733884324be3c76 100644
--- a/tests/builtins/oracle/strlen.res.oracle
+++ b/tests/builtins/oracle/strlen.res.oracle
@@ -261,6 +261,8 @@
[eva] Done for function bitfields2
[eva] computing for function escaping <- main.
Called from tests/builtins/strlen.c:342.
+[eva:alarm] tests/builtins/strlen.c:222: Warning:
+ pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva:locals-escaping] tests/builtins/strlen.c:222: Warning:
locals {x} escaping the scope of a block of escaping through s
[eva] tests/builtins/strlen.c:225: Call to builtin strlen
diff --git a/tests/builtins/oracle/strnlen2.res.oracle b/tests/builtins/oracle/strnlen2.res.oracle
index 903c30f5d3a4cffb4f6aae6f5439d141e2fed5a3..392940b6cb6e3312cb5941f61892dfa13cb007c0 100644
--- a/tests/builtins/oracle/strnlen2.res.oracle
+++ b/tests/builtins/oracle/strnlen2.res.oracle
@@ -261,6 +261,8 @@
[eva] Done for function bitfields2
[eva] computing for function escaping <- main.
Called from tests/builtins/strnlen2.c:522.
+[eva:alarm] tests/builtins/strnlen2.c:196: Warning:
+ pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva:locals-escaping] tests/builtins/strnlen2.c:196: Warning:
locals {x} escaping the scope of a block of escaping through s
[eva] tests/builtins/strnlen2.c:199: Call to builtin strnlen
diff --git a/tests/builtins/oracle/wcslen.res.oracle b/tests/builtins/oracle/wcslen.res.oracle
index f5a97cc85744af051d76551bd0250596ac7f074f..784bf02c5cf4f24b9aa67db81b8cf442ed7c0e06 100644
--- a/tests/builtins/oracle/wcslen.res.oracle
+++ b/tests/builtins/oracle/wcslen.res.oracle
@@ -261,6 +261,14 @@
[eva] Done for function bitfields2
[eva] computing for function escaping <- main.
Called from tests/builtins/wcslen.c:347.
+[eva:alarm] tests/builtins/wcslen.c:222: Warning:
+ pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
+[eva:alarm] tests/builtins/wcslen.c:222: Warning:
+ pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
+[eva:alarm] tests/builtins/wcslen.c:222: Warning:
+ pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
+[eva:alarm] tests/builtins/wcslen.c:222: Warning:
+ pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva:locals-escaping] tests/builtins/wcslen.c:222: Warning:
locals {x} escaping the scope of a block of escaping through s
[eva] tests/builtins/wcslen.c:225: Call to builtin wcslen
@@ -358,6 +366,7 @@
[eva] Done for function negative_offsets
[eva] Recording results for main
[eva] done for function main
+[scope:rm_asserts] removing 3 assertion(s)
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function init_array_nondet:
from ∈ {-1}
diff --git a/tests/float/oracle/builtins.res.oracle b/tests/float/oracle/builtins.res.oracle
index 0bfa3b88df28af5763d4da2e18e3a395ffb58887..66f30707d3259e2969df47d8e280f469eb3f74b4 100644
--- a/tests/float/oracle/builtins.res.oracle
+++ b/tests/float/oracle/builtins.res.oracle
@@ -134,6 +134,8 @@
function exp: precondition 'finite_arg' got status valid.
[eva] tests/float/builtins.c:104:
function exp: precondition 'finite_domain' got status valid.
+[eva:alarm] tests/float/builtins.c:107: Warning:
+ pointer downcast. assert (unsigned int)(&d) ≤ 2147483647;
[eva:alarm] tests/float/builtins.c:107: Warning:
non-finite double value. assert \is_finite((double)((int)(&d)));
[eva] tests/float/builtins.c:107: Call to builtin log
diff --git a/tests/float/oracle/nonlin.0.res.oracle b/tests/float/oracle/nonlin.0.res.oracle
index 648a1ae9af5f33b985dcd3411249ebe3e07a77c4..5e60b7a32e5ff2014f7a279f2b314b5969f31798 100644
--- a/tests/float/oracle/nonlin.0.res.oracle
+++ b/tests/float/oracle/nonlin.0.res.oracle
@@ -230,6 +230,10 @@
[eva] Done for function norm
[eva] computing for function garbled <- main.
Called from tests/float/nonlin.c:148.
+[eva:alarm] tests/float/nonlin.c:98: Warning:
+ pointer downcast. assert (unsigned int)(&x_0) ≤ 2147483647;
+[eva:alarm] tests/float/nonlin.c:98: Warning:
+ pointer downcast. assert (unsigned int)(&x_0 + (int)(&x_0)) ≤ 2147483647;
[eva:alarm] tests/float/nonlin.c:98: Warning:
non-finite float value.
assert \is_finite((float)((int)(&x_0 + (int)(&x_0))));
diff --git a/tests/float/oracle/nonlin.1.res.oracle b/tests/float/oracle/nonlin.1.res.oracle
index 3ddef66ef496f7061b9f8444af849b2b4bd1bafb..036f8d26e43e182434e95dcde6ced28107a6d3bb 100644
--- a/tests/float/oracle/nonlin.1.res.oracle
+++ b/tests/float/oracle/nonlin.1.res.oracle
@@ -253,6 +253,10 @@
[eva] Done for function norm
[eva] computing for function garbled <- main.
Called from tests/float/nonlin.c:148.
+[eva:alarm] tests/float/nonlin.c:98: Warning:
+ pointer downcast. assert (unsigned int)(&x_0) ≤ 2147483647;
+[eva:alarm] tests/float/nonlin.c:98: Warning:
+ pointer downcast. assert (unsigned int)(&x_0 + (int)(&x_0)) ≤ 2147483647;
[eva:alarm] tests/float/nonlin.c:98: Warning:
non-finite float value.
assert \is_finite((float)((int)(&x_0 + (int)(&x_0))));
diff --git a/tests/float/oracle/nonlin.2.res.oracle b/tests/float/oracle/nonlin.2.res.oracle
index ba81c19d44c306730614d89d500ccdb7fde507a5..112f643e8810a8acfb5c96421196df65e43d7fe5 100644
--- a/tests/float/oracle/nonlin.2.res.oracle
+++ b/tests/float/oracle/nonlin.2.res.oracle
@@ -240,6 +240,10 @@
[eva] Done for function norm
[eva] computing for function garbled <- main.
Called from tests/float/nonlin.c:148.
+[eva:alarm] tests/float/nonlin.c:98: Warning:
+ pointer downcast. assert (unsigned int)(&x_0) ≤ 2147483647;
+[eva:alarm] tests/float/nonlin.c:98: Warning:
+ pointer downcast. assert (unsigned int)(&x_0 + (int)(&x_0)) ≤ 2147483647;
[eva] tests/float/nonlin.c:98:
Assigning imprecise value to a_0.
The imprecision originates from Arithmetic {tests/float/nonlin.c:98}
diff --git a/tests/float/oracle/nonlin.3.res.oracle b/tests/float/oracle/nonlin.3.res.oracle
index c3e1e9cdb8b72a6f1a433932db7cf78cbfcc82bc..f791b980831bd6f9e0c61b1febfb6e83cba17dda 100644
--- a/tests/float/oracle/nonlin.3.res.oracle
+++ b/tests/float/oracle/nonlin.3.res.oracle
@@ -230,6 +230,10 @@
[eva] Done for function norm
[eva] computing for function garbled <- main.
Called from tests/float/nonlin.c:148.
+[eva:alarm] tests/float/nonlin.c:98: Warning:
+ pointer downcast. assert (unsigned int)(&x_0) ≤ 2147483647;
+[eva:alarm] tests/float/nonlin.c:98: Warning:
+ pointer downcast. assert (unsigned int)(&x_0 + (int)(&x_0)) ≤ 2147483647;
[eva:alarm] tests/float/nonlin.c:98: Warning:
non-finite float value.
assert \is_finite((float)((int)(&x_0 + (int)(&x_0))));
diff --git a/tests/float/oracle/nonlin.4.res.oracle b/tests/float/oracle/nonlin.4.res.oracle
index 2f06c2710cf66d8592b8fdae363e0a41589b4481..ba58150afafceddb7303e4ef4f35b0d438a7b2b4 100644
--- a/tests/float/oracle/nonlin.4.res.oracle
+++ b/tests/float/oracle/nonlin.4.res.oracle
@@ -253,6 +253,10 @@
[eva] Done for function norm
[eva] computing for function garbled <- main.
Called from tests/float/nonlin.c:148.
+[eva:alarm] tests/float/nonlin.c:98: Warning:
+ pointer downcast. assert (unsigned int)(&x_0) ≤ 2147483647;
+[eva:alarm] tests/float/nonlin.c:98: Warning:
+ pointer downcast. assert (unsigned int)(&x_0 + (int)(&x_0)) ≤ 2147483647;
[eva:alarm] tests/float/nonlin.c:98: Warning:
non-finite float value.
assert \is_finite((float)((int)(&x_0 + (int)(&x_0))));
diff --git a/tests/float/oracle/nonlin.5.res.oracle b/tests/float/oracle/nonlin.5.res.oracle
index a26018dc5a7b1e8f6e79c7f951bc2d4b1e746db0..36e1a671ef649728d5f1a3b4b1ba0f00f12488ea 100644
--- a/tests/float/oracle/nonlin.5.res.oracle
+++ b/tests/float/oracle/nonlin.5.res.oracle
@@ -240,6 +240,10 @@
[eva] Done for function norm
[eva] computing for function garbled <- main.
Called from tests/float/nonlin.c:148.
+[eva:alarm] tests/float/nonlin.c:98: Warning:
+ pointer downcast. assert (unsigned int)(&x_0) ≤ 2147483647;
+[eva:alarm] tests/float/nonlin.c:98: Warning:
+ pointer downcast. assert (unsigned int)(&x_0 + (int)(&x_0)) ≤ 2147483647;
[eva] tests/float/nonlin.c:98:
Assigning imprecise value to a_0.
The imprecision originates from Arithmetic {tests/float/nonlin.c:98}
diff --git a/tests/rte/oracle/castoncall.0.res.oracle b/tests/rte/oracle/castoncall.0.res.oracle
index 430827699b37879782d59e6e4e9c4193b0079fc3..5bee127b54a1cdc4bc55cc45abba81fd07275144 100644
--- a/tests/rte/oracle/castoncall.0.res.oracle
+++ b/tests/rte/oracle/castoncall.0.res.oracle
@@ -16,6 +16,8 @@ void *nondet_ptr(void *a, void *b)
{
void *__retres;
int tmp;
+ /*@ assert rte: pointer_downcast: (unsigned int)a ≤ 2147483647; */
+ /*@ assert rte: pointer_downcast: (unsigned int)b ≤ 2147483647; */
tmp = nondet((int)a,(int)b);
__retres = (void *)tmp;
return __retres;
diff --git a/tests/rte/oracle/castoncall.1.res.oracle b/tests/rte/oracle/castoncall.1.res.oracle
index 430827699b37879782d59e6e4e9c4193b0079fc3..5bee127b54a1cdc4bc55cc45abba81fd07275144 100644
--- a/tests/rte/oracle/castoncall.1.res.oracle
+++ b/tests/rte/oracle/castoncall.1.res.oracle
@@ -16,6 +16,8 @@ void *nondet_ptr(void *a, void *b)
{
void *__retres;
int tmp;
+ /*@ assert rte: pointer_downcast: (unsigned int)a ≤ 2147483647; */
+ /*@ assert rte: pointer_downcast: (unsigned int)b ≤ 2147483647; */
tmp = nondet((int)a,(int)b);
__retres = (void *)tmp;
return __retres;
diff --git a/tests/rte/oracle/twofunc.res.oracle b/tests/rte/oracle/twofunc.res.oracle
index 58f6280ce2a0652e9d51261289831067a286bf40..5d0a80d5f3847f4511ec8b4104f59014643e42ae 100644
--- a/tests/rte/oracle/twofunc.res.oracle
+++ b/tests/rte/oracle/twofunc.res.oracle
@@ -133,6 +133,7 @@ int main(void)
[kernel] - bool_value = true
[kernel] - finite_float = true
[kernel] - float_to_int = true
+[kernel] - pointer_downcast = true
[kernel] - unsigned_downcast = false
[kernel] - unsigned_overflow = false
[kernel] - downcast = true
@@ -148,6 +149,7 @@ int main(void)
[kernel] - bool_value = true
[kernel] - finite_float = true
[kernel] - float_to_int = true
+[kernel] - pointer_downcast = true
[kernel] - unsigned_downcast = false
[kernel] - unsigned_overflow = false
[kernel] - downcast = true
@@ -225,6 +227,7 @@ int main(void)
[kernel] - bool_value = true
[kernel] - finite_float = true
[kernel] - float_to_int = true
+[kernel] - pointer_downcast = true
[kernel] - unsigned_downcast = false
[kernel] - unsigned_overflow = false
[kernel] - downcast = true
@@ -240,6 +243,7 @@ int main(void)
[kernel] - bool_value = true
[kernel] - finite_float = true
[kernel] - float_to_int = true
+[kernel] - pointer_downcast = true
[kernel] - unsigned_downcast = false
[kernel] - unsigned_overflow = false
[kernel] - downcast = true
diff --git a/tests/slicing/oracle/slice_no_body.res.oracle b/tests/slicing/oracle/slice_no_body.res.oracle
index 2960de9c498aacd917cb2454c4e52994569f0ced..dcba3c11fcc1a7d1050389ca74ec54aa489549e7 100644
--- a/tests/slicing/oracle/slice_no_body.res.oracle
+++ b/tests/slicing/oracle/slice_no_body.res.oracle
@@ -102,7 +102,6 @@ Print slice = h_slice_1:
/**/int h(void)
{
- /* <[---], [---]> */ int __retres;
/* invisible call */ /* <[---], [---]> */
/* <[---], [---]> */ int a = f(1);
/* invisible call */ /* <[---], [---]> */
@@ -117,9 +116,7 @@ Print slice = h_slice_1:
G = g(c);
}
/* <[---], [---]> */
- __retres = (int)(& g);
- /* <[---], [---]> */
- return __retres;
+ return G;
}
Slicing project worklist [default] =
@@ -223,7 +220,6 @@ Print slice = h_slice_1: (InCtrl: <[---], [ S ]>)
/**/int h(void)
{
- /* <[---], [---]> */ int __retres;
/* sig call:
(InCtrl: <[---], [ S ]>)
(In1: <[---], [ S ]>)
@@ -262,9 +258,7 @@ Print slice = h_slice_1: (InCtrl: <[---], [ S ]>)
G = g(c);
}
/* <[---], [---]> */
- __retres = (int)(& g);
- /* <[---], [---]> */
- return __retres;
+ return G;
}
Slicing project worklist [default] =
diff --git a/tests/slicing/slice_no_body.i b/tests/slicing/slice_no_body.i
index 8e97f4c920a7f4f6972d25a7be69257b90dd1adf..e2be30cc3c617fc32f374986687e8bfa8d4d8f79 100644
--- a/tests/slicing/slice_no_body.i
+++ b/tests/slicing/slice_no_body.i
@@ -24,5 +24,5 @@ int h (void) {
G = f (4);
if (G > 0)
G = g (c);
- return (int)g;
+ return G;
}
diff --git a/tests/syntax/oracle/ghost_else_bad.1.err.oracle b/tests/syntax/oracle/ghost_else_bad.1.err.oracle
deleted file mode 100644
index b7f5dc572a00637862d9948bffdcdd1ccea254e5..0000000000000000000000000000000000000000
--- a/tests/syntax/oracle/ghost_else_bad.1.err.oracle
+++ /dev/null
@@ -1 +0,0 @@
-Warning: tests/syntax/ghost_else_bad.c:32: Invalid ghost else ignored
diff --git a/tests/value/downcast.i b/tests/value/downcast.i
index e979236ea122b6149c761eb12b5af28192441efa..6c01c21fd74573af61c929d6257ffaa1f1526bfc 100644
--- a/tests/value/downcast.i
+++ b/tests/value/downcast.i
@@ -1,5 +1,9 @@
/* run.config*
- STDOPT: +"-load-module report -report -warn-signed-downcast -lib-entry -print -then -no-warn-signed-downcast -warn-unsigned-downcast -then -no-warn-unsigned-downcast -eva-warn-signed-converted-downcast -then -main main5_wrap_signed -slevel 2 -no-print"
+ STDOPT: +"-lib-entry -no-warn-signed-downcast -no-warn-unsigned-downcast -warn-pointer-downcast -eva-slevel-function main5_wrap_signed:2"
+ STDOPT: +"-lib-entry -warn-signed-downcast -no-warn-unsigned-downcast -warn-pointer-downcast"
+ STDOPT: +"-lib-entry -no-warn-signed-downcast -warn-unsigned-downcast -warn-pointer-downcast"
+ STDOPT: +"-lib-entry -no-warn-signed-downcast -no-warn-unsigned-downcast -warn-pointer-downcast -eva-warn-signed-converted-downcast"
+ STDOPT: +"-lib-entry -no-warn-signed-downcast -no-warn-unsigned-downcast -no-warn-pointer-downcast"
*/
signed char sx,sy,sz;
diff --git a/tests/value/oracle/addition.res.oracle b/tests/value/oracle/addition.res.oracle
index f601e53058bff5ba8712b59c7b0ce069bfa7a1b4..1fe41a6755acb70d209f28f6fe3f44444cfd61d9 100644
--- a/tests/value/oracle/addition.res.oracle
+++ b/tests/value/oracle/addition.res.oracle
@@ -59,27 +59,56 @@
[eva] tests/value/addition.i:34:
Assigning imprecise value to p1.
The imprecision originates from Arithmetic {tests/value/addition.i:34}
+[eva:alarm] tests/value/addition.i:36: Warning:
+ pointer downcast. assert (unsigned int)(&p1) ≤ 2147483647;
[eva] tests/value/addition.i:36:
Assigning imprecise value to p2.
The imprecision originates from Arithmetic {tests/value/addition.i:36}
+[eva:alarm] tests/value/addition.i:38: Warning:
+ pointer downcast. assert (unsigned int)(&p1) ≤ 127;
+[eva:alarm] tests/value/addition.i:38: Warning:
+ pointer downcast. assert (unsigned int)(&t[(char)(&p1)]) ≤ 2147483647;
[eva] tests/value/addition.i:38:
Assigning imprecise value to p3.
The imprecision originates from Arithmetic {tests/value/addition.i:38}
+[eva:alarm] tests/value/addition.i:40: Warning:
+ pointer downcast. assert (unsigned int)(&p1) ≤ 127;
+[eva:alarm] tests/value/addition.i:40: Warning:
+ pointer downcast. assert (unsigned int)(&tt[(char)(&p1)].a) ≤ 2147483647;
[eva] tests/value/addition.i:40:
Assigning imprecise value to p4.
The imprecision originates from Arithmetic {tests/value/addition.i:40}
+[eva:alarm] tests/value/addition.i:42: Warning:
+ pointer downcast. assert (unsigned int)(&p1) ≤ 127;
+[eva:alarm] tests/value/addition.i:42: Warning:
+ pointer downcast. assert (unsigned int)(&p2) ≤ 127;
+[eva:alarm] tests/value/addition.i:42: Warning:
+ pointer downcast.
+ assert (unsigned int)(&ttt[(char)(&p1)][(char)(&p2)]) ≤ 2147483647;
[eva] tests/value/addition.i:42:
Assigning imprecise value to p5.
The imprecision originates from Arithmetic {tests/value/addition.i:42}
+[eva:alarm] tests/value/addition.i:44: Warning:
+ pointer downcast. assert (unsigned int)(&p1) ≤ 127;
+[eva:alarm] tests/value/addition.i:44: Warning:
+ pointer downcast.
+ assert (unsigned int)(&ttt[(char)(&p1)][u2]) ≤ 2147483647;
[eva] tests/value/addition.i:44:
Assigning imprecise value to p6.
The imprecision originates from Arithmetic {tests/value/addition.i:44}
+[eva:alarm] tests/value/addition.i:46: Warning:
+ pointer downcast. assert (unsigned int)(&p2) ≤ 127;
+[eva:alarm] tests/value/addition.i:46: Warning:
+ pointer downcast.
+ assert (unsigned int)(&ttt[u2][(char)(&p2)]) ≤ 2147483647;
[eva] tests/value/addition.i:46:
Assigning imprecise value to p7.
The imprecision originates from Arithmetic {tests/value/addition.i:46}
[eva:alarm] tests/value/addition.i:48: Warning:
pointer comparison.
assert \pointer_comparable((void *)(&p1 + 1), (void *)(&p2));
+[eva:alarm] tests/value/addition.i:50: Warning:
+ pointer downcast. assert (unsigned int)(&p1) ≤ 2147483647;
[eva:alarm] tests/value/addition.i:50: Warning:
signed overflow. assert -2147483648 ≤ (int)(&p1) / 2;
[eva:alarm] tests/value/addition.i:50: Warning:
@@ -87,9 +116,15 @@
[eva] tests/value/addition.i:50:
Assigning imprecise value to p9.
The imprecision originates from Arithmetic {tests/value/addition.i:50}
+[eva:alarm] tests/value/addition.i:52: Warning:
+ pointer downcast. assert (unsigned int)(&p1) ≤ 2147483647;
[eva] tests/value/addition.i:52:
Assigning imprecise value to p10.
The imprecision originates from Arithmetic {tests/value/addition.i:52}
+[eva:alarm] tests/value/addition.i:56: Warning:
+ pointer downcast. assert (unsigned int)(&p1) ≤ 2147483647;
+[eva:alarm] tests/value/addition.i:56: Warning:
+ pointer downcast. assert (unsigned int)(&p2) ≤ 2147483647;
[eva] tests/value/addition.i:56:
Assigning imprecise value to p12.
The imprecision originates from Arithmetic {tests/value/addition.i:56}
@@ -130,7 +165,7 @@
{{ garbled mix of &{p1} (origin: Arithmetic {tests/value/addition.i:56}) }}
{{ garbled mix of &{p1} (origin: Misaligned {tests/value/addition.i:59}) }}
{{ garbled mix of &{p1} (origin: Misaligned {tests/value/addition.i:61}) }}
-[scope:rm_asserts] removing 2 assertion(s)
+[scope:rm_asserts] removing 9 assertion(s)
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
t[0] ∈ {0}
@@ -323,13 +358,48 @@
signed overflow. assert -2147483648 ≤ &p2 - &p3;
[eva:alarm] tests/value/addition.i:34: Warning:
signed overflow. assert &p2 - &p3 ≤ 2147483647;
+[eva:alarm] tests/value/addition.i:36: Warning:
+ pointer downcast. assert (unsigned int)(&p1) ≤ 2147483647;
+[eva:alarm] tests/value/addition.i:38: Warning:
+ pointer downcast. assert (unsigned int)(&p1) ≤ 127;
+[eva:alarm] tests/value/addition.i:38: Warning:
+ pointer downcast. assert (unsigned int)(&t[(char)(&p1)]) ≤ 2147483647;
+[eva:alarm] tests/value/addition.i:40: Warning:
+ pointer downcast. assert (unsigned int)(&p1) ≤ 127;
+[eva:alarm] tests/value/addition.i:40: Warning:
+ pointer downcast. assert (unsigned int)(&tt[(char)(&p1)].a) ≤ 2147483647;
+[eva:alarm] tests/value/addition.i:42: Warning:
+ pointer downcast. assert (unsigned int)(&p1) ≤ 127;
+[eva:alarm] tests/value/addition.i:42: Warning:
+ pointer downcast. assert (unsigned int)(&p2) ≤ 127;
+[eva:alarm] tests/value/addition.i:42: Warning:
+ pointer downcast.
+ assert (unsigned int)(&ttt[(char)(&p1)][(char)(&p2)]) ≤ 2147483647;
+[eva:alarm] tests/value/addition.i:44: Warning:
+ pointer downcast. assert (unsigned int)(&p1) ≤ 127;
+[eva:alarm] tests/value/addition.i:44: Warning:
+ pointer downcast.
+ assert (unsigned int)(&ttt[(char)(&p1)][u2]) ≤ 2147483647;
+[eva:alarm] tests/value/addition.i:46: Warning:
+ pointer downcast. assert (unsigned int)(&p2) ≤ 127;
+[eva:alarm] tests/value/addition.i:46: Warning:
+ pointer downcast.
+ assert (unsigned int)(&ttt[u2][(char)(&p2)]) ≤ 2147483647;
[eva:alarm] tests/value/addition.i:48: Warning:
pointer comparison.
assert \pointer_comparable((void *)(&p1 + 1), (void *)(&p2));
+[eva:alarm] tests/value/addition.i:50: Warning:
+ pointer downcast. assert (unsigned int)(&p1) ≤ 2147483647;
[eva:alarm] tests/value/addition.i:50: Warning:
signed overflow. assert -2147483648 ≤ (int)(&p1) / 2;
[eva:alarm] tests/value/addition.i:50: Warning:
signed overflow. assert (int)(&p1) / 2 ≤ 2147483647;
+[eva:alarm] tests/value/addition.i:52: Warning:
+ pointer downcast. assert (unsigned int)(&p1) ≤ 2147483647;
+[eva:alarm] tests/value/addition.i:56: Warning:
+ pointer downcast. assert (unsigned int)(&p1) ≤ 2147483647;
+[eva:alarm] tests/value/addition.i:56: Warning:
+ pointer downcast. assert (unsigned int)(&p2) ≤ 2147483647;
[eva:alarm] tests/value/addition.i:59: Warning:
signed overflow. assert -2147483648 ≤ (int)*((char *)(&q1)) + 2;
[eva:alarm] tests/value/addition.i:59: Warning:
@@ -360,7 +430,7 @@
{{ garbled mix of &{p1} (origin: Arithmetic {tests/value/addition.i:56}) }}
{{ garbled mix of &{p1} (origin: Misaligned {tests/value/addition.i:59}) }}
{{ garbled mix of &{p1} (origin: Misaligned {tests/value/addition.i:61}) }}
-[scope:rm_asserts] removing 2 assertion(s)
+[scope:rm_asserts] removing 9 assertion(s)
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
t[0] ∈ {0}
diff --git a/tests/value/oracle/align_char_array.res.oracle b/tests/value/oracle/align_char_array.res.oracle
index 82c0a105954556053c32fb592300ec24255c11b1..3383a7f5af11c33a0b49deb33113bdbf7543ac0f 100644
--- a/tests/value/oracle/align_char_array.res.oracle
+++ b/tests/value/oracle/align_char_array.res.oracle
@@ -15,25 +15,41 @@
overlapread2 ∈ {0}
overlapread3 ∈ {0}
overlapread4 ∈ {0}
+[eva:alarm] tests/value/align_char_array.c:21: Warning:
+ pointer downcast. assert (unsigned int)(&S.a) ≤ 2147483647;
+[eva:alarm] tests/value/align_char_array.c:21: Warning:
+ pointer downcast. assert (unsigned int)(&S.c) ≤ 2147483647;
+[eva:alarm] tests/value/align_char_array.c:23: Warning:
+ pointer downcast. assert (unsigned int)(&t[2][2]) ≤ 2147483647;
+[eva:alarm] tests/value/align_char_array.c:23: Warning:
+ pointer downcast. assert (unsigned int)(&t[0][0]) ≤ 2147483647;
+[eva:alarm] tests/value/align_char_array.c:25: Warning:
+ pointer downcast. assert (unsigned int)((char (*)[10])t) ≤ 2147483647;
[eva:alarm] tests/value/align_char_array.c:25: Warning:
signed overflow. assert -2147483648 ≤ (int)((char (*)[10])t) + 3;
[eva:alarm] tests/value/align_char_array.c:25: Warning:
signed overflow. assert (int)((char (*)[10])t) + 3 ≤ 2147483647;
+[eva:alarm] tests/value/align_char_array.c:26: Warning:
+ pointer downcast. assert (unsigned int)((char (*)[10])t) ≤ 2147483647;
[eva:alarm] tests/value/align_char_array.c:26: Warning:
signed overflow. assert -2147483648 ≤ (int)((char (*)[10])t) + 3;
[eva:alarm] tests/value/align_char_array.c:26: Warning:
signed overflow. assert (int)((char (*)[10])t) + 3 ≤ 2147483647;
+[eva:alarm] tests/value/align_char_array.c:27: Warning:
+ pointer downcast. assert (unsigned int)((char (*)[10])t) ≤ 2147483647;
[eva:alarm] tests/value/align_char_array.c:27: Warning:
signed overflow. assert -2147483648 ≤ (int)((char (*)[10])t) + 2;
[eva:alarm] tests/value/align_char_array.c:27: Warning:
signed overflow. assert (int)((char (*)[10])t) + 2 ≤ 2147483647;
+[eva:alarm] tests/value/align_char_array.c:28: Warning:
+ pointer downcast. assert (unsigned int)((char (*)[10])t) ≤ 2147483647;
[eva:alarm] tests/value/align_char_array.c:28: Warning:
signed overflow. assert -2147483648 ≤ (int)((char (*)[10])t) + 2;
[eva:alarm] tests/value/align_char_array.c:28: Warning:
signed overflow. assert (int)((char (*)[10])t) + 2 ≤ 2147483647;
[eva] Recording results for main
[eva] done for function main
-[scope:rm_asserts] removing 4 assertion(s)
+[scope:rm_asserts] removing 7 assertion(s)
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
d1 ∈ {1}
diff --git a/tests/value/oracle/arith_pointer.res.oracle b/tests/value/oracle/arith_pointer.res.oracle
index 3ec14d1a31c7604387924f3f8ca5d8de5a3c1bad..a09c922b6d3924e3f74da13fa331a48dc6afe907 100644
--- a/tests/value/oracle/arith_pointer.res.oracle
+++ b/tests/value/oracle/arith_pointer.res.oracle
@@ -22,6 +22,8 @@
[eva:alarm] tests/value/arith_pointer.c:51: Warning:
pointer subtraction. assert \base_addr(p2) ≡ \base_addr(p2);
[eva] tests/value/arith_pointer.c:52: Frama_C_show_each: {0}
+[eva:alarm] tests/value/arith_pointer.c:54: Warning:
+ pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva] tests/value/arith_pointer.c:54:
Assigning imprecise value to p1.
The imprecision originates from Arithmetic {tests/value/arith_pointer.c:54}
@@ -148,6 +150,8 @@
Frama_C_show_each:
{{ garbled mix of &{x; y}
(origin: Arithmetic {tests/value/arith_pointer.c:51}) }}
+[eva:alarm] tests/value/arith_pointer.c:54: Warning:
+ pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva:alarm] tests/value/arith_pointer.c:56: Warning:
signed overflow. assert -2147483648 ≤ p2 - p1;
[eva:alarm] tests/value/arith_pointer.c:56: Warning:
diff --git a/tests/value/oracle/array_ptr.res.oracle b/tests/value/oracle/array_ptr.res.oracle
index 76ce304e41df77b747b0ad233ff3d1dc8d01b778..8599de4e4af9da144bcf4e997d7be8c9348c5b49 100644
--- a/tests/value/oracle/array_ptr.res.oracle
+++ b/tests/value/oracle/array_ptr.res.oracle
@@ -6,6 +6,8 @@
G ∈ {1}
l[0] ∈ {1}
[1..19] ∈ {0}
+[eva:alarm] tests/value/array_ptr.i:14: Warning:
+ pointer downcast. assert (unsigned int)(&l) ≤ 2147483647;
[eva] computing for function f <- main.
Called from tests/value/array_ptr.i:15.
[eva] Recording results for f
diff --git a/tests/value/oracle/assigns.res.oracle b/tests/value/oracle/assigns.res.oracle
index 0edee1de714cdb4506cf8068125b5fb063ed94e1..4cfd1aeca7a34e5f4825e3efdf9dade3a7e01e54 100644
--- a/tests/value/oracle/assigns.res.oracle
+++ b/tests/value/oracle/assigns.res.oracle
@@ -44,6 +44,8 @@
[eva] computing for function f <- main1 <- main.
Called from tests/value/assigns.i:49.
[eva] Done for function f
+[eva:alarm] tests/value/assigns.i:51: Warning:
+ pointer downcast. assert (unsigned int)(&T) ≤ 2147483647;
[eva:alarm] tests/value/assigns.i:51: Warning:
signed overflow. assert -2147483648 ≤ 2 * (int)(&T);
[eva:alarm] tests/value/assigns.i:51: Warning:
@@ -52,6 +54,8 @@
Called from tests/value/assigns.i:51.
[eva] using specification for function g
[eva] Done for function g
+[eva:alarm] tests/value/assigns.i:52: Warning:
+ pointer downcast. assert (unsigned int)(&t3) ≤ 2147483647;
[eva:alarm] tests/value/assigns.i:52: Warning:
signed overflow. assert -2147483648 ≤ 2 * (int)(&t3);
[eva:alarm] tests/value/assigns.i:52: Warning:
@@ -931,9 +935,11 @@ void main1(void)
i ++;
}
}
+ /*@ assert Eva: pointer_downcast: (unsigned int)(&T) ≤ 2147483647; */
/*@ assert Eva: signed_overflow: -2147483648 ≤ 2 * (int)(&T); */
/*@ assert Eva: signed_overflow: 2 * (int)(&T) ≤ 2147483647; */
g(2 * (int)(& T));
+ /*@ assert Eva: pointer_downcast: (unsigned int)(&t3) ≤ 2147483647; */
/*@ assert Eva: signed_overflow: -2147483648 ≤ 2 * (int)(&t3); */
/*@ assert Eva: signed_overflow: 2 * (int)(&t3) ≤ 2147483647; */
h((int *)(2 * (int)(& t3)));
diff --git a/tests/value/oracle/bitfield.res.oracle b/tests/value/oracle/bitfield.res.oracle
index 05b0967b0520a71f78f122b82d7b572800408561..0ae5f0394606e216870ff0d5c5f4fe947f103d98 100644
--- a/tests/value/oracle/bitfield.res.oracle
+++ b/tests/value/oracle/bitfield.res.oracle
@@ -28,9 +28,13 @@
Called from tests/value/bitfield.i:164.
[eva] tests/value/bitfield.i:113: Frama_C_show_each: {1}
[eva] tests/value/bitfield.i:117: Frama_C_show_each: {3}
+[eva:alarm] tests/value/bitfield.i:123: Warning:
+ pointer downcast. assert (unsigned int)(&v) ≤ 2147483647;
[eva] tests/value/bitfield.i:123:
Assigning imprecise value to v.c.
The imprecision originates from Arithmetic {tests/value/bitfield.i:123}
+[eva:alarm] tests/value/bitfield.i:124: Warning:
+ pointer downcast. assert (unsigned int)(&v + 1) ≤ 2147483647;
[eva:alarm] tests/value/bitfield.i:125: Warning:
signed overflow. assert -2147483648 ≤ (int)v.d + 1;
[eva:alarm] tests/value/bitfield.i:125: Warning:
@@ -77,6 +81,8 @@
signed overflow. assert -2147483648 ≤ foo + foo;
[eva:alarm] tests/value/bitfield.i:129: Warning:
signed overflow. assert foo + foo ≤ 2147483647;
+[eva:alarm] tests/value/bitfield.i:130: Warning:
+ pointer downcast. assert (unsigned int)(&v + 1) ≤ 2147483647;
[eva] tests/value/bitfield.i:130:
Assigning imprecise value to h.c.
The imprecision originates from Arithmetic {tests/value/bitfield.i:130}
@@ -207,6 +213,7 @@
[eva] done for function main
[eva] tests/value/bitfield.i:102:
assertion 'Eva,initialization' got final status invalid.
+[scope:rm_asserts] removing 1 assertion(s)
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function char_short:
S.c ∈ {1}
@@ -550,7 +557,9 @@ void main_old(void)
else Frama_C_show_each(3);
VV = (unsigned int)h.a;
h.a = (unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(2))))VV;
+ /*@ assert Eva: pointer_downcast: (unsigned int)(&v) ≤ 2147483647; */
v.c = (int __attribute__((__FRAMA_C_BITFIELD_SIZE__(22))))((int)(& v));
+ /*@ assert Eva: pointer_downcast: (unsigned int)(&v + 1) ≤ 2147483647; */
v.d = (int __attribute__((__FRAMA_C_BITFIELD_SIZE__(32))))((int)(& v + 1));
/*@ assert Eva: signed_overflow: -2147483648 ≤ (int)v.d + 1; */
/*@ assert Eva: signed_overflow: (int)v.d + 1 ≤ 2147483647; */
@@ -561,6 +570,7 @@ void main_old(void)
/*@ assert Eva: signed_overflow: -2147483648 ≤ foo + foo; */
/*@ assert Eva: signed_overflow: foo + foo ≤ 2147483647; */
h.b = (int __attribute__((__FRAMA_C_BITFIELD_SIZE__(4))))(((foo + foo) + (int)h.a) + (int)h.b);
+ /*@ assert Eva: pointer_downcast: (unsigned int)(&v + 1) ≤ 2147483647; */
h.c = (int __attribute__((__FRAMA_C_BITFIELD_SIZE__(22))))((int)(& v + 1));
k8.b = (int __attribute__((__FRAMA_C_BITFIELD_SIZE__(4))))8;
tmp = return_8();
diff --git a/tests/value/oracle/bitwise_pointer.res.oracle b/tests/value/oracle/bitwise_pointer.res.oracle
index c1a1f86bba18a08385a94aab5c3509196a363c36..878fa04174a2301232dcc5fab79671c8cfad0fe8 100644
--- a/tests/value/oracle/bitwise_pointer.res.oracle
+++ b/tests/value/oracle/bitwise_pointer.res.oracle
@@ -29,11 +29,15 @@
[10..99] ∈ {0}
p1 ∈ {0}
x1 ∈ {0}
+[eva:alarm] tests/value/bitwise_pointer.i:18: Warning:
+ pointer downcast. assert (unsigned int)(&t[7]) ≤ 2147483647;
[eva] tests/value/bitwise_pointer.i:18:
Assigning imprecise value to p.
The imprecision originates from Arithmetic {tests/value/bitwise_pointer.i:18}
[eva:alarm] tests/value/bitwise_pointer.i:19: Warning:
out of bounds write. assert \valid(p);
+[eva:alarm] tests/value/bitwise_pointer.i:22: Warning:
+ pointer downcast. assert (unsigned int)(&t1[mask]) ≤ 2147483647;
[eva] tests/value/bitwise_pointer.i:22:
Assigning imprecise value to p1.
The imprecision originates from Arithmetic {tests/value/bitwise_pointer.i:22}
diff --git a/tests/value/oracle/call.res.oracle b/tests/value/oracle/call.res.oracle
index bd70d1673837431b24118da8e0c2e213dbcc1357..144373249549a7098517489dc881ab42cdfcef3f 100644
--- a/tests/value/oracle/call.res.oracle
+++ b/tests/value/oracle/call.res.oracle
@@ -10,6 +10,8 @@
x ∈ {0}
[eva:alarm] tests/value/call.i:19: Warning:
out of bounds read. assert \valid_read(v + 1);
+[eva:alarm] tests/value/call.i:19: Warning:
+ pointer downcast. assert (unsigned int)*(v + 1) ≤ 2147483647;
[eva] computing for function leaf_fun_int <- main.
Called from tests/value/call.i:19.
[kernel:annot:missing-spec] tests/value/call.i:19: Warning:
diff --git a/tests/value/oracle/cmp_ptr.0.res.oracle b/tests/value/oracle/cmp_ptr.0.res.oracle
index b3a90b9fbe13a88ea88e78cc4d5f921cb937e06c..47a1035cc56d34fcfaad83bf7bfc5cd2f7b50b2d 100644
--- a/tests/value/oracle/cmp_ptr.0.res.oracle
+++ b/tests/value/oracle/cmp_ptr.0.res.oracle
@@ -45,12 +45,18 @@
invalid pointer comparison: invalid pointer(s)
[eva:alarm] tests/value/cmp_ptr.i:22: Warning:
pointer comparison. assert \pointer_comparable((void *)0, (void *)(&y + 2));
+[eva:alarm] tests/value/cmp_ptr.i:23: Warning:
+ pointer downcast. assert (unsigned int)(&y + 2) ≤ 2147483647;
[eva:pointer-comparison] tests/value/cmp_ptr.i:24:
invalid pointer comparison: invalid pointer(s)
[eva:alarm] tests/value/cmp_ptr.i:24: Warning:
non-finite float value. assert \is_finite(ff);
[eva:pointer-comparison] tests/value/cmp_ptr.i:28:
invalid pointer comparison: invalid pointer(s)
+[eva:alarm] tests/value/cmp_ptr.i:28: Warning:
+ pointer downcast.
+ assert (unsigned int)tmp_0 ≤ 2147483647;
+ (tmp_0 from u?& f:& g)
[eva:alarm] tests/value/cmp_ptr.i:28: Warning:
signed overflow.
assert -2147483648 ≤ 1 + (int)tmp_0;
diff --git a/tests/value/oracle/cmp_ptr.1.res.oracle b/tests/value/oracle/cmp_ptr.1.res.oracle
index 36b9efb6f4798d3be4013f0f8d40bed54d1f7905..182c5433339e484a9db1a6187096ab716cc325a0 100644
--- a/tests/value/oracle/cmp_ptr.1.res.oracle
+++ b/tests/value/oracle/cmp_ptr.1.res.oracle
@@ -59,12 +59,18 @@
evaluating condition to {0; 1} instead of {0} because of UPCPA
[eva:alarm] tests/value/cmp_ptr.i:22: Warning:
pointer comparison. assert \pointer_comparable((void *)0, (void *)(&y + 2));
+[eva:alarm] tests/value/cmp_ptr.i:23: Warning:
+ pointer downcast. assert (unsigned int)(&y + 2) ≤ 2147483647;
[eva:pointer-comparison] tests/value/cmp_ptr.i:24:
invalid pointer comparison: invalid pointer(s)
[eva:alarm] tests/value/cmp_ptr.i:24: Warning:
non-finite float value. assert \is_finite(ff);
[eva:pointer-comparison] tests/value/cmp_ptr.i:28:
invalid pointer comparison: invalid pointer(s)
+[eva:alarm] tests/value/cmp_ptr.i:28: Warning:
+ pointer downcast.
+ assert (unsigned int)tmp_0 ≤ 2147483647;
+ (tmp_0 from u?& f:& g)
[eva:alarm] tests/value/cmp_ptr.i:28: Warning:
signed overflow.
assert -2147483648 ≤ 1 + (int)tmp_0;
diff --git a/tests/value/oracle/context_free.res.oracle b/tests/value/oracle/context_free.res.oracle
index b244fecc83c99a27e3be9deb7ff2499573145e64..f1220992e0b2fe33b682cd14e1d308846df0d14a 100644
--- a/tests/value/oracle/context_free.res.oracle
+++ b/tests/value/oracle/context_free.res.oracle
@@ -101,10 +101,8 @@
The imprecision originates from Well
[eva:alarm] tests/value/context_free.i:61: Warning:
out of bounds write. assert \valid(pvoid);
-[eva] tests/value/context_free.i:61:
- Assigning imprecise value to *pvoid
- (pointing to S_qvoid with offsets [0..34359738360],0%8).
- The imprecision originates from Arithmetic {tests/value/context_free.i:61}
+[eva:alarm] tests/value/context_free.i:61: Warning:
+ pointer downcast. assert (unsigned int)(&pvoid) ≤ 127;
[eva:alarm] tests/value/context_free.i:62: Warning:
pointer to function with incompatible type. assert \valid_function(g);
[eva] Recording results for f
diff --git a/tests/value/oracle/conversion.res.oracle b/tests/value/oracle/conversion.res.oracle
index d9ed842d845c0b9c251ded319a56058f991f54bb..954fdab07b419cf2a12ec881c37860546384ec36 100644
--- a/tests/value/oracle/conversion.res.oracle
+++ b/tests/value/oracle/conversion.res.oracle
@@ -57,6 +57,8 @@
f ∈ [3. .. 5.]
l ∈ UNINITIALIZED
==END OF DUMP==
+[eva:alarm] tests/value/conversion.i:38: Warning:
+ pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva] tests/value/conversion.i:40:
Frama_C_dump_each:
# Cvalue domain:
@@ -161,6 +163,8 @@
f ∈ [3. .. 5.]
l ∈ UNINITIALIZED
==END OF DUMP==
+[eva:alarm] tests/value/conversion.i:38: Warning:
+ pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva:alarm] tests/value/conversion.i:39: Warning:
non-finite float value. assert \is_finite(*((float *)(&x)));
[eva] tests/value/conversion.i:39:
diff --git a/tests/value/oracle/degeneration2.res.oracle b/tests/value/oracle/degeneration2.res.oracle
index feb99e8fb7164d2b46d6f4e6802813eb4265ca6b..8ba6db66b554ace332d5b2673b0ce0b2a7fcec7d 100644
--- a/tests/value/oracle/degeneration2.res.oracle
+++ b/tests/value/oracle/degeneration2.res.oracle
@@ -6,6 +6,8 @@
v ∈ [--..--]
[eva:alarm] tests/value/degeneration2.i:14: Warning:
accessing uninitialized left-value. assert \initialized(&A);
+[eva:alarm] tests/value/degeneration2.i:14: Warning:
+ pointer downcast. assert (unsigned int)A ≤ 2147483647;
[eva:alarm] tests/value/degeneration2.i:14: Warning:
signed overflow. assert -2147483648 ≤ -((int)A);
[eva:alarm] tests/value/degeneration2.i:14: Warning:
diff --git a/tests/value/oracle/deps_addr.res.oracle b/tests/value/oracle/deps_addr.res.oracle
index 093935ed64325e2002c3ba5be0483f9edff1ea14..59f4ac5f0f9e552e08318ac54231d9674780213f 100644
--- a/tests/value/oracle/deps_addr.res.oracle
+++ b/tests/value/oracle/deps_addr.res.oracle
@@ -6,6 +6,8 @@
t ∈ {0}
a ∈ {0}
tt[0..4][0..4] ∈ {0}
+[eva:alarm] tests/value/deps_addr.i:6: Warning:
+ pointer downcast. assert (unsigned int)(&a) ≤ 2147483647;
[eva:alarm] tests/value/deps_addr.i:6: Warning:
out of bounds read. assert \valid_read(t + (int)(&a));
[eva] Recording results for main
diff --git a/tests/value/oracle/deps_mixed.res.oracle b/tests/value/oracle/deps_mixed.res.oracle
index b33c688ba947bc3efb73d0909b92254a462308c1..6631dfe4e46d5233ea557de069df72f64f96bec0 100644
--- a/tests/value/oracle/deps_mixed.res.oracle
+++ b/tests/value/oracle/deps_mixed.res.oracle
@@ -12,6 +12,8 @@
v ∈ [--..--]
t[0] ∈ {{ &f }}
[1] ∈ {{ &g }}
+[eva:alarm] tests/value/deps_mixed.i:20: Warning:
+ pointer downcast. assert (unsigned int)q ≤ 2147483647;
[eva:alarm] tests/value/deps_mixed.i:20: Warning:
out of bounds read. assert \valid_read(p + (int)q);
[eva:alarm] tests/value/deps_mixed.i:22: Warning:
@@ -26,6 +28,10 @@
Called from tests/value/deps_mixed.i:22.
[eva] Recording results for f
[eva] Done for function f
+[eva:alarm] tests/value/deps_mixed.i:24: Warning:
+ pointer downcast. assert (unsigned int)q ≤ 2147483647;
+[eva:alarm] tests/value/deps_mixed.i:24: Warning:
+ pointer downcast. assert (unsigned int)(p + (int)q) ≤ 2147483647;
[eva] tests/value/deps_mixed.i:24:
Assigning imprecise value to __retres.
The imprecision originates from Arithmetic {tests/value/deps_mixed.i:24}
diff --git a/tests/value/oracle/div.0.res.oracle b/tests/value/oracle/div.0.res.oracle
index b0c33659a01a67ad2e5e1db4f15e05217dc9dc2b..2f95483430ee68b9fb2aee65ffad1ccfd202931a 100644
--- a/tests/value/oracle/div.0.res.oracle
+++ b/tests/value/oracle/div.0.res.oracle
@@ -35,6 +35,8 @@
signed overflow. assert X + 1 ≤ 2147483647;
[eva:alarm] tests/value/div.i:32: Warning: division by zero. assert Z2 ≢ 0;
[eva:alarm] tests/value/div.i:33: Warning: division by zero. assert Z2 ≢ 0;
+[eva:alarm] tests/value/div.i:33: Warning:
+ pointer downcast. assert (unsigned int)(&Z2) ≤ 2147483647;
[eva:alarm] tests/value/div.i:33: Warning:
signed overflow. assert -2147483648 ≤ (int)(&Z2) / Z2;
[eva:alarm] tests/value/div.i:33: Warning:
@@ -42,6 +44,8 @@
[eva] tests/value/div.i:33:
Assigning imprecise value to b.
The imprecision originates from Arithmetic {tests/value/div.i:33}
+[eva:alarm] tests/value/div.i:34: Warning:
+ pointer downcast. assert (unsigned int)(&X + 2) ≤ 2147483647;
[eva:alarm] tests/value/div.i:34: Warning:
division by zero. assert (int)(&X + 2) ≢ 0;
[eva:alarm] tests/value/div.i:34: Warning:
@@ -51,6 +55,8 @@
[eva] tests/value/div.i:34:
Assigning imprecise value to d2.
The imprecision originates from Arithmetic {tests/value/div.i:34}
+[eva:alarm] tests/value/div.i:35: Warning:
+ pointer downcast. assert (unsigned int)(&X + 1) ≤ 2147483647;
[eva:alarm] tests/value/div.i:35: Warning:
signed overflow. assert -2147483648 ≤ 100 / (int)(&X + 1);
[eva:alarm] tests/value/div.i:35: Warning:
@@ -58,6 +64,8 @@
[eva] tests/value/div.i:35:
Assigning imprecise value to d1.
The imprecision originates from Arithmetic {tests/value/div.i:35}
+[eva:alarm] tests/value/div.i:36: Warning:
+ pointer downcast. assert (unsigned int)(&X) ≤ 2147483647;
[eva:alarm] tests/value/div.i:36: Warning:
signed overflow. assert -2147483648 ≤ 100 / (int)(&X);
[eva:alarm] tests/value/div.i:36: Warning:
@@ -65,6 +73,8 @@
[eva] tests/value/div.i:36:
Assigning imprecise value to d0.
The imprecision originates from Arithmetic {tests/value/div.i:36}
+[eva:alarm] tests/value/div.i:37: Warning:
+ pointer downcast. assert (unsigned int)(&X) ≤ 2147483647;
[eva:alarm] tests/value/div.i:37: Warning:
signed overflow. assert -2147483648 ≤ -((int)(&X));
[eva:alarm] tests/value/div.i:37: Warning:
@@ -74,7 +84,7 @@
The imprecision originates from Arithmetic {tests/value/div.i:37}
[eva] Recording results for main
[eva] done for function main
-[scope:rm_asserts] removing 1 assertion(s)
+[scope:rm_asserts] removing 2 assertion(s)
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
X ∈ [--..--]
diff --git a/tests/value/oracle/div.1.res.oracle b/tests/value/oracle/div.1.res.oracle
index e333aa05c132dd16c43aa7b148d98c22a25f8000..bb2cbef17535dbdbf3cef47f6757b5ac4894ff6c 100644
--- a/tests/value/oracle/div.1.res.oracle
+++ b/tests/value/oracle/div.1.res.oracle
@@ -50,11 +50,15 @@
[eva:alarm] tests/value/div.i:32: Warning:
assertion 'rte,division_by_zero' got status unknown.
[eva:alarm] tests/value/div.i:32: Warning: division by zero. assert Z2 ≢ 0;
+[eva:alarm] tests/value/div.i:33: Warning:
+ assertion 'rte,pointer_downcast' got status unknown.
[eva:alarm] tests/value/div.i:33: Warning:
assertion 'rte,division_by_zero' got status unknown.
[eva:alarm] tests/value/div.i:33: Warning:
assertion 'rte,signed_overflow' got status unknown.
[eva:alarm] tests/value/div.i:33: Warning: division by zero. assert Z2 ≢ 0;
+[eva:alarm] tests/value/div.i:33: Warning:
+ pointer downcast. assert (unsigned int)(&Z2) ≤ 2147483647;
[eva:alarm] tests/value/div.i:33: Warning:
signed overflow. assert -2147483648 ≤ (int)(&Z2) / Z2;
[eva:alarm] tests/value/div.i:33: Warning:
@@ -62,8 +66,12 @@
[eva] tests/value/div.i:33:
Assigning imprecise value to b.
The imprecision originates from Arithmetic {tests/value/div.i:33}
+[eva:alarm] tests/value/div.i:34: Warning:
+ assertion 'rte,pointer_downcast' got status unknown.
[eva:alarm] tests/value/div.i:34: Warning:
assertion 'rte,division_by_zero' got status unknown.
+[eva:alarm] tests/value/div.i:34: Warning:
+ pointer downcast. assert (unsigned int)(&X + 2) ≤ 2147483647;
[eva:alarm] tests/value/div.i:34: Warning:
division by zero. assert (int)(&X + 2) ≢ 0;
[eva:alarm] tests/value/div.i:34: Warning:
@@ -73,7 +81,11 @@
[eva] tests/value/div.i:34:
Assigning imprecise value to d2.
The imprecision originates from Arithmetic {tests/value/div.i:34}
+[eva:alarm] tests/value/div.i:35: Warning:
+ assertion 'rte,pointer_downcast' got status unknown.
[eva] tests/value/div.i:35: assertion 'rte,division_by_zero' got status valid.
+[eva:alarm] tests/value/div.i:35: Warning:
+ pointer downcast. assert (unsigned int)(&X + 1) ≤ 2147483647;
[eva:alarm] tests/value/div.i:35: Warning:
signed overflow. assert -2147483648 ≤ 100 / (int)(&X + 1);
[eva:alarm] tests/value/div.i:35: Warning:
@@ -81,7 +93,11 @@
[eva] tests/value/div.i:35:
Assigning imprecise value to d1.
The imprecision originates from Arithmetic {tests/value/div.i:35}
+[eva:alarm] tests/value/div.i:36: Warning:
+ assertion 'rte,pointer_downcast' got status unknown.
[eva] tests/value/div.i:36: assertion 'rte,division_by_zero' got status valid.
+[eva:alarm] tests/value/div.i:36: Warning:
+ pointer downcast. assert (unsigned int)(&X) ≤ 2147483647;
[eva:alarm] tests/value/div.i:36: Warning:
signed overflow. assert -2147483648 ≤ 100 / (int)(&X);
[eva:alarm] tests/value/div.i:36: Warning:
@@ -89,8 +105,12 @@
[eva] tests/value/div.i:36:
Assigning imprecise value to d0.
The imprecision originates from Arithmetic {tests/value/div.i:36}
+[eva:alarm] tests/value/div.i:37: Warning:
+ assertion 'rte,pointer_downcast' got status unknown.
[eva:alarm] tests/value/div.i:37: Warning:
assertion 'rte,signed_overflow' got status unknown.
+[eva:alarm] tests/value/div.i:37: Warning:
+ pointer downcast. assert (unsigned int)(&X) ≤ 2147483647;
[eva:alarm] tests/value/div.i:37: Warning:
signed overflow. assert -2147483648 ≤ -((int)(&X));
[eva:alarm] tests/value/div.i:37: Warning:
@@ -110,7 +130,7 @@
assertion 'rte,division_by_zero' got final status valid.
[eva] tests/value/div.i:36:
assertion 'rte,division_by_zero' got final status valid.
-[scope:rm_asserts] removing 1 assertion(s)
+[scope:rm_asserts] removing 2 assertion(s)
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
X ∈ [--..--]
diff --git a/tests/value/oracle/downcast.0.res.oracle b/tests/value/oracle/downcast.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..c27a3ff663f1e3ba23a8e2cf6cc34c19e724e10e
--- /dev/null
+++ b/tests/value/oracle/downcast.0.res.oracle
@@ -0,0 +1,231 @@
+[kernel] Parsing tests/value/downcast.i (no preprocessing)
+[eva] Analyzing an incomplete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ sx ∈ [--..--]
+ sy ∈ [--..--]
+ sz ∈ [--..--]
+ uc ∈ [--..--]
+ x ∈ [--..--]
+ ux ∈ [--..--]
+ uy ∈ [--..--]
+ uz ∈ [--..--]
+ s ∈ [--..--]
+ v ∈ [--..--]
+[eva] computing for function main1 <- main.
+ Called from tests/value/downcast.i:156.
+[eva] Recording results for main1
+[eva] Done for function main1
+[eva] computing for function main2_bitfield <- main.
+ Called from tests/value/downcast.i:157.
+[eva] Recording results for main2_bitfield
+[eva] Done for function main2_bitfield
+[eva] computing for function main3_reduction <- main.
+ Called from tests/value/downcast.i:158.
+[eva] Recording results for main3_reduction
+[eva] Done for function main3_reduction
+[eva] computing for function main4_pointer <- main.
+ Called from tests/value/downcast.i:159.
+[eva:alarm] tests/value/downcast.i:54: Warning:
+ signed overflow. assert -9223372036854775808 ≤ p + (long long)100;
+[eva:alarm] tests/value/downcast.i:54: Warning:
+ signed overflow. assert p + (long long)100 ≤ 9223372036854775807;
+[eva] Recording results for main4_pointer
+[eva] Done for function main4_pointer
+[eva] computing for function main5_wrap_signed <- main.
+ Called from tests/value/downcast.i:160.
+[eva:alarm] tests/value/downcast.i:62: Warning:
+ assertion 'ASSUME' got status unknown.
+[eva] tests/value/downcast.i:63: assertion got status valid.
+[eva] tests/value/downcast.i:67:
+ Frama_C_show_each:
+ [2147483503..2147483647],
+ [2147483648..2147483792],
+ [-2147483648..-2147483504]
+[eva] tests/value/downcast.i:67:
+ Frama_C_show_each:
+ [100000..2147483502], [100145..2147483647], [100145..2147483647]
+[eva] tests/value/downcast.i:68: assertion got status valid.
+[eva] Recording results for main5_wrap_signed
+[eva] Done for function main5_wrap_signed
+[eva] computing for function main6_val_warn_converted_signed <- main.
+ Called from tests/value/downcast.i:161.
+[eva:alarm] tests/value/downcast.i:95: Warning:
+ pointer downcast. assert (unsigned int)p ≤ 2147483647;
+[eva:alarm] tests/value/downcast.i:96: Warning:
+ pointer downcast. assert (unsigned int)p ≤ 32767;
+[eva:alarm] tests/value/downcast.i:97: Warning:
+ pointer downcast. assert (unsigned int)p ≤ 65535;
+[eva] Recording results for main6_val_warn_converted_signed
+[eva] Done for function main6_val_warn_converted_signed
+[eva] computing for function main7_signed_upcast <- main.
+ Called from tests/value/downcast.i:162.
+[eva] Recording results for main7_signed_upcast
+[eva] Done for function main7_signed_upcast
+[eva] computing for function main8_bitfields <- main.
+ Called from tests/value/downcast.i:163.
+[eva] Recording results for main8_bitfields
+[eva] Done for function main8_bitfields
+[eva] computing for function main9_bitfield <- main.
+ Called from tests/value/downcast.i:164.
+[eva] tests/value/downcast.i:138: assertion got status valid.
+[eva] Recording results for main9_bitfield
+[eva] Done for function main9_bitfield
+[eva] computing for function main10_loop <- main.
+ Called from tests/value/downcast.i:165.
+[eva] tests/value/downcast.i:149: starting to merge loop iterations
+[eva] Recording results for main10_loop
+[eva] Done for function main10_loop
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main1:
+ sz ∈ [--..--]
+ uc ∈ [--..--]
+ x ∈ [--..--]
+ ux ∈ [--..--]
+ s ∈ [--..--]
+[eva:final-states] Values at end of function main10_loop:
+ c ∈ [--..--] or UNINITIALIZED
+ bf.b ∈ [--..--] or UNINITIALIZED
+ .[bits 10 to 31] ∈ UNINITIALIZED
+ k ∈ {10}
+[eva:final-states] Values at end of function main2_bitfield:
+ i ∈ {117}
+ j ∈ {254}
+ ss.i ∈ {-11} or UNINITIALIZED
+ .j ∈ {30} or UNINITIALIZED
+ .[bits 10 to 31] ∈ UNINITIALIZED
+[eva:final-states] Values at end of function main3_reduction:
+ x_0 ∈ [--..--]
+ c ∈ [--..--]
+ y ∈ [--..--]
+ d ∈ [--..--]
+[eva:final-states] Values at end of function main4_pointer:
+ p ∈ {{ &x_0 + {100} }}
+ q ∈ {{ &x_0 + {100} }}
+ r ∈ {{ &x_0 + {100} }}
+[eva:final-states] Values at end of function main5_wrap_signed:
+ x_0 ∈ [100000..2147483647]
+ y ∈ [100145..2147483792]
+ z ∈ [--..--]
+[eva:final-states] Values at end of function main6_val_warn_converted_signed:
+
+[eva:final-states] Values at end of function main7_signed_upcast:
+ c ∈ {240}
+ i ∈ {240}
+[eva:final-states] Values at end of function main8_bitfields:
+ S.i1 ∈ {65}
+ .i2 ∈ {-1; 1} or UNINITIALIZED
+ .[bits 24 to 31] ∈ UNINITIALIZED
+ c ∈ {-1; 1; 65} or UNINITIALIZED
+[eva:final-states] Values at end of function main9_bitfield:
+ bf.a ∈ {1648}
+ .[bits 11 to 31] ∈ UNINITIALIZED
+ c ∈ {112} or UNINITIALIZED
+[eva:final-states] Values at end of function main:
+ sz ∈ [--..--]
+ uc ∈ [--..--]
+ x ∈ [--..--]
+ ux ∈ [--..--]
+ s ∈ [--..--]
+[from] Computing for function main1
+[from] Done for function main1
+[from] Computing for function main10_loop
+[from] Done for function main10_loop
+[from] Computing for function main2_bitfield
+[from] Done for function main2_bitfield
+[from] Computing for function main3_reduction
+[from] Done for function main3_reduction
+[from] Computing for function main4_pointer
+[from] Done for function main4_pointer
+[from] Computing for function main5_wrap_signed
+[from] Done for function main5_wrap_signed
+[from] Computing for function main6_val_warn_converted_signed
+[from] Done for function main6_val_warn_converted_signed
+[from] Computing for function main7_signed_upcast
+[from] Done for function main7_signed_upcast
+[from] Computing for function main8_bitfields
+[from] Done for function main8_bitfields
+[from] Computing for function main9_bitfield
+[from] Done for function main9_bitfield
+[from] Computing for function main
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function main1:
+ sz FROM sx; sy
+ uc FROM x
+ x FROM uy; uz
+ ux FROM uy; uz
+ s FROM uy; uz
+[from] Function main10_loop:
+ NO EFFECTS
+[from] Function main2_bitfield:
+ NO EFFECTS
+[from] Function main3_reduction:
+ NO EFFECTS
+[from] Function main4_pointer:
+ NO EFFECTS
+[from] Function main5_wrap_signed:
+ NO EFFECTS
+[from] Function main6_val_warn_converted_signed:
+ NO EFFECTS
+[from] Function main7_signed_upcast:
+ NO EFFECTS
+[from] Function main8_bitfields:
+ NO EFFECTS
+[from] Function main9_bitfield:
+ NO EFFECTS
+[from] Function main:
+ sz FROM sx; sy
+ uc FROM x
+ x FROM uy; uz
+ ux FROM uy; uz
+ s FROM uy; uz
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function main1:
+ sz; uc; x; ux; s
+[inout] Inputs for function main1:
+ sx; sy; x; uy; uz
+[inout] Out (internal) for function main10_loop:
+ c; bf.b; k
+[inout] Inputs for function main10_loop:
+ v
+[inout] Out (internal) for function main2_bitfield:
+ i; j; ss{.i; .j}
+[inout] Inputs for function main2_bitfield:
+ v
+[inout] Out (internal) for function main3_reduction:
+ x_0; c; y; d
+[inout] Inputs for function main3_reduction:
+ v
+[inout] Out (internal) for function main4_pointer:
+ p; q; r
+[inout] Inputs for function main4_pointer:
+ \nothing
+[inout] Out (internal) for function main5_wrap_signed:
+ x_0; y; z
+[inout] Inputs for function main5_wrap_signed:
+ v
+[inout] Out (internal) for function main6_val_warn_converted_signed:
+ s_0; u; e; b; e_0; b_0; e_1; b_1; p; x_0; y; z
+[inout] Inputs for function main6_val_warn_converted_signed:
+ v
+[inout] Out (internal) for function main7_signed_upcast:
+ c; i
+[inout] Inputs for function main7_signed_upcast:
+ \nothing
+[inout] Out (internal) for function main8_bitfields:
+ S{.i1; .i2}; c
+[inout] Inputs for function main8_bitfields:
+ v
+[inout] Out (internal) for function main9_bitfield:
+ bf.a; signed_a; c
+[inout] Inputs for function main9_bitfield:
+ v
+[inout] Out (internal) for function main:
+ sz; uc; x; ux; s
+[inout] Inputs for function main:
+ sx; sy; x; uy; uz; v
diff --git a/tests/value/oracle/downcast.1.res.oracle b/tests/value/oracle/downcast.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..4430fdae7754b7ca73df1a85b6314fffe75916ad
--- /dev/null
+++ b/tests/value/oracle/downcast.1.res.oracle
@@ -0,0 +1,286 @@
+[kernel] Parsing tests/value/downcast.i (no preprocessing)
+[eva] Analyzing an incomplete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ sx ∈ [--..--]
+ sy ∈ [--..--]
+ sz ∈ [--..--]
+ uc ∈ [--..--]
+ x ∈ [--..--]
+ ux ∈ [--..--]
+ uy ∈ [--..--]
+ uz ∈ [--..--]
+ s ∈ [--..--]
+ v ∈ [--..--]
+[eva] computing for function main1 <- main.
+ Called from tests/value/downcast.i:156.
+[eva:alarm] tests/value/downcast.i:23: Warning:
+ signed downcast. assert -128 ≤ (int)((int)sx + (int)sy);
+[eva:alarm] tests/value/downcast.i:23: Warning:
+ signed downcast. assert (int)((int)sx + (int)sy) ≤ 127;
+[eva:alarm] tests/value/downcast.i:26: Warning:
+ signed downcast. assert (unsigned int)(uy + uz) ≤ 2147483647;
+[eva] Recording results for main1
+[eva] Done for function main1
+[eva] computing for function main2_bitfield <- main.
+ Called from tests/value/downcast.i:157.
+[eva:alarm] tests/value/downcast.i:36: Warning:
+ signed downcast. assert i ≤ 15;
+[eva] Recording results for main2_bitfield
+[eva] Done for function main2_bitfield
+[eva] computing for function main3_reduction <- main.
+ Called from tests/value/downcast.i:158.
+[eva:alarm] tests/value/downcast.i:42: Warning:
+ signed downcast. assert -128 ≤ x_0;
+[eva:alarm] tests/value/downcast.i:42: Warning:
+ signed downcast. assert x_0 ≤ 127;
+[eva] Recording results for main3_reduction
+[eva] Done for function main3_reduction
+[eva] computing for function main4_pointer <- main.
+ Called from tests/value/downcast.i:159.
+[eva:alarm] tests/value/downcast.i:54: Warning:
+ signed overflow. assert -9223372036854775808 ≤ p + (long long)100;
+[eva:alarm] tests/value/downcast.i:54: Warning:
+ signed overflow. assert p + (long long)100 ≤ 9223372036854775807;
+[eva:alarm] tests/value/downcast.i:56: Warning:
+ signed downcast. assert -2147483648 ≤ p;
+[eva:alarm] tests/value/downcast.i:56: Warning:
+ signed downcast. assert p ≤ 2147483647;
+[eva] Recording results for main4_pointer
+[eva] Done for function main4_pointer
+[eva] computing for function main5_wrap_signed <- main.
+ Called from tests/value/downcast.i:160.
+[eva:alarm] tests/value/downcast.i:62: Warning:
+ assertion 'ASSUME' got status unknown.
+[eva] tests/value/downcast.i:63: assertion got status valid.
+[eva:alarm] tests/value/downcast.i:66: Warning:
+ signed downcast. assert y ≤ 2147483647;
+[eva] tests/value/downcast.i:67:
+ Frama_C_show_each:
+ [100000..2147483647], [100145..2147483647], [100145..2147483647]
+[eva] tests/value/downcast.i:68: assertion got status valid.
+[eva] Recording results for main5_wrap_signed
+[eva] Done for function main5_wrap_signed
+[eva] computing for function main6_val_warn_converted_signed <- main.
+ Called from tests/value/downcast.i:161.
+[eva:alarm] tests/value/downcast.i:75: Warning:
+ signed downcast. assert 65300u ≤ 32767;
+[eva:alarm] tests/value/downcast.i:86: Warning:
+ signed downcast. assert e_0 ≤ 32767;
+[eva:alarm] tests/value/downcast.i:91: Warning:
+ signed downcast. assert e_1 ≤ 32767;
+[eva:alarm] tests/value/downcast.i:95: Warning:
+ pointer downcast. assert (unsigned int)p ≤ 2147483647;
+[eva:alarm] tests/value/downcast.i:96: Warning:
+ pointer downcast. assert (unsigned int)p ≤ 32767;
+[eva:alarm] tests/value/downcast.i:97: Warning:
+ pointer downcast. assert (unsigned int)p ≤ 65535;
+[eva] Recording results for main6_val_warn_converted_signed
+[eva] Done for function main6_val_warn_converted_signed
+[eva] computing for function main7_signed_upcast <- main.
+ Called from tests/value/downcast.i:162.
+[eva] Recording results for main7_signed_upcast
+[eva] Done for function main7_signed_upcast
+[eva] computing for function main8_bitfields <- main.
+ Called from tests/value/downcast.i:163.
+[eva:alarm] tests/value/downcast.i:118: Warning:
+ signed downcast. assert S.i1 ≤ 31;
+[eva:alarm] tests/value/downcast.i:119: Warning:
+ signed downcast. assert S.i1 ≤ 127;
+[eva:alarm] tests/value/downcast.i:123: Warning:
+ signed downcast. assert S.i1 ≤ 31;
+[eva:alarm] tests/value/downcast.i:124: Warning:
+ signed downcast. assert S.i1 ≤ 127;
+[eva:alarm] tests/value/downcast.i:128: Warning:
+ signed downcast. assert S.i1 ≤ 31;
+[eva] Recording results for main8_bitfields
+[eva] Done for function main8_bitfields
+[eva] computing for function main9_bitfield <- main.
+ Called from tests/value/downcast.i:164.
+[eva:alarm] tests/value/downcast.i:137: Warning:
+ signed downcast. assert bf.a ≤ 1023;
+[eva:alarm] tests/value/downcast.i:141: Warning:
+ signed downcast. assert bf.a ≤ 127;
+[eva] Recording results for main9_bitfield
+[eva] Done for function main9_bitfield
+[eva] computing for function main10_loop <- main.
+ Called from tests/value/downcast.i:165.
+[eva:alarm] tests/value/downcast.i:151: Warning:
+ signed downcast. assert bf.b ≤ 127;
+[eva] tests/value/downcast.i:149: starting to merge loop iterations
+[eva] Recording results for main10_loop
+[eva] Done for function main10_loop
+[eva] Recording results for main
+[eva] done for function main
+[eva] tests/value/downcast.i:36:
+ assertion 'Eva,signed_downcast' got final status invalid.
+[eva] tests/value/downcast.i:75:
+ assertion 'Eva,signed_downcast' got final status invalid.
+[eva] tests/value/downcast.i:86:
+ assertion 'Eva,signed_downcast' got final status invalid.
+[eva] tests/value/downcast.i:91:
+ assertion 'Eva,signed_downcast' got final status invalid.
+[eva] tests/value/downcast.i:118:
+ assertion 'Eva,signed_downcast' got final status invalid.
+[eva] tests/value/downcast.i:119:
+ assertion 'Eva,signed_downcast' got final status invalid.
+[eva] tests/value/downcast.i:123:
+ assertion 'Eva,signed_downcast' got final status invalid.
+[eva] tests/value/downcast.i:124:
+ assertion 'Eva,signed_downcast' got final status invalid.
+[eva] tests/value/downcast.i:128:
+ assertion 'Eva,signed_downcast' got final status invalid.
+[eva] tests/value/downcast.i:137:
+ assertion 'Eva,signed_downcast' got final status invalid.
+[eva] tests/value/downcast.i:141:
+ assertion 'Eva,signed_downcast' got final status invalid.
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main1:
+ sz ∈ [--..--]
+ uc ∈ [--..--]
+ x ∈ [0..2147483647]
+ ux ∈ [--..--]
+ s ∈ [--..--]
+[eva:final-states] Values at end of function main10_loop:
+ c ∈ [0..127] or UNINITIALIZED
+ bf.b ∈ [--..--] or UNINITIALIZED
+ .[bits 10 to 31] ∈ UNINITIALIZED
+ k ∈ {10}
+[eva:final-states] Values at end of function main2_bitfield:
+ i ∈ {117}
+ j ∈ {254}
+ ss.i ∈ UNINITIALIZED
+ .j ∈ {30} or UNINITIALIZED
+ .[bits 10 to 31] ∈ UNINITIALIZED
+[eva:final-states] Values at end of function main3_reduction:
+ x_0 ∈ [-128..127]
+ c ∈ [--..--]
+ y ∈ [--..--]
+ d ∈ [--..--]
+[eva:final-states] Values at end of function main4_pointer:
+ p ∈ {{ &x_0 + {100} }}
+ q ∈ {{ &x_0 + {100} }}
+ r ∈ {{ &x_0 + {100} }}
+[eva:final-states] Values at end of function main5_wrap_signed:
+ x_0 ∈ [100000..2147483647]
+ y ∈ [100145..2147483647]
+ z ∈ [100145..2147483647]
+[eva:final-states] Values at end of function main6_val_warn_converted_signed:
+
+[eva:final-states] Values at end of function main7_signed_upcast:
+ c ∈ {240}
+ i ∈ {240}
+[eva:final-states] Values at end of function main8_bitfields:
+ S.i1 ∈ {65}
+ {.i2; .[bits 24 to 31]} ∈ UNINITIALIZED
+ c ∈ {65} or UNINITIALIZED
+[eva:final-states] Values at end of function main9_bitfield:
+ bf.a ∈ {1648}
+ .[bits 11 to 31] ∈ UNINITIALIZED
+ c ∈ UNINITIALIZED
+[eva:final-states] Values at end of function main:
+ sz ∈ [--..--]
+ uc ∈ [--..--]
+ x ∈ [0..2147483647]
+ ux ∈ [--..--]
+ s ∈ [--..--]
+[from] Computing for function main1
+[from] Done for function main1
+[from] Computing for function main10_loop
+[from] Done for function main10_loop
+[from] Computing for function main2_bitfield
+[from] Done for function main2_bitfield
+[from] Computing for function main3_reduction
+[from] Done for function main3_reduction
+[from] Computing for function main4_pointer
+[from] Done for function main4_pointer
+[from] Computing for function main5_wrap_signed
+[from] Done for function main5_wrap_signed
+[from] Computing for function main6_val_warn_converted_signed
+[from] Done for function main6_val_warn_converted_signed
+[from] Computing for function main7_signed_upcast
+[from] Done for function main7_signed_upcast
+[from] Computing for function main8_bitfields
+[from] Done for function main8_bitfields
+[from] Computing for function main9_bitfield
+[from] Done for function main9_bitfield
+[from] Computing for function main
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function main1:
+ sz FROM sx; sy
+ uc FROM x
+ x FROM uy; uz
+ ux FROM uy; uz
+ s FROM uy; uz
+[from] Function main10_loop:
+ NO EFFECTS
+[from] Function main2_bitfield:
+ NO EFFECTS
+[from] Function main3_reduction:
+ NO EFFECTS
+[from] Function main4_pointer:
+ NO EFFECTS
+[from] Function main5_wrap_signed:
+ NO EFFECTS
+[from] Function main6_val_warn_converted_signed:
+ NO EFFECTS
+[from] Function main7_signed_upcast:
+ NO EFFECTS
+[from] Function main8_bitfields:
+ NO EFFECTS
+[from] Function main9_bitfield:
+ NO EFFECTS
+[from] Function main:
+ sz FROM sx; sy
+ uc FROM x
+ x FROM uy; uz
+ ux FROM uy; uz
+ s FROM uy; uz
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function main1:
+ sz; uc; x; ux; s
+[inout] Inputs for function main1:
+ sx; sy; x; uy; uz
+[inout] Out (internal) for function main10_loop:
+ c; bf.b; k
+[inout] Inputs for function main10_loop:
+ v
+[inout] Out (internal) for function main2_bitfield:
+ i; j; ss{.i; .j}
+[inout] Inputs for function main2_bitfield:
+ v
+[inout] Out (internal) for function main3_reduction:
+ x_0; c; y; d
+[inout] Inputs for function main3_reduction:
+ v
+[inout] Out (internal) for function main4_pointer:
+ p; q; r
+[inout] Inputs for function main4_pointer:
+ \nothing
+[inout] Out (internal) for function main5_wrap_signed:
+ x_0; y; z
+[inout] Inputs for function main5_wrap_signed:
+ v
+[inout] Out (internal) for function main6_val_warn_converted_signed:
+ s_0; u; e; b; e_0; b_0; e_1; b_1; p; x_0; y; z
+[inout] Inputs for function main6_val_warn_converted_signed:
+ v
+[inout] Out (internal) for function main7_signed_upcast:
+ c; i
+[inout] Inputs for function main7_signed_upcast:
+ \nothing
+[inout] Out (internal) for function main8_bitfields:
+ S{.i1; .i2}; c
+[inout] Inputs for function main8_bitfields:
+ v
+[inout] Out (internal) for function main9_bitfield:
+ bf.a; signed_a; c
+[inout] Inputs for function main9_bitfield:
+ v
+[inout] Out (internal) for function main:
+ sz; uc; x; ux; s
+[inout] Inputs for function main:
+ sx; sy; x; uy; uz; v
diff --git a/tests/value/oracle/downcast.2.res.oracle b/tests/value/oracle/downcast.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..0c43f9fb2f787dbfc9aa221ef2c9387f3ed6f8c6
--- /dev/null
+++ b/tests/value/oracle/downcast.2.res.oracle
@@ -0,0 +1,257 @@
+[kernel] Parsing tests/value/downcast.i (no preprocessing)
+[eva] Analyzing an incomplete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ sx ∈ [--..--]
+ sy ∈ [--..--]
+ sz ∈ [--..--]
+ uc ∈ [--..--]
+ x ∈ [--..--]
+ ux ∈ [--..--]
+ uy ∈ [--..--]
+ uz ∈ [--..--]
+ s ∈ [--..--]
+ v ∈ [--..--]
+[eva] computing for function main1 <- main.
+ Called from tests/value/downcast.i:156.
+[eva:alarm] tests/value/downcast.i:24: Warning:
+ unsigned downcast. assert 0 ≤ (int)((int)sx + (int)sy);
+[eva:alarm] tests/value/downcast.i:25: Warning:
+ unsigned downcast. assert 0 ≤ x;
+[eva:alarm] tests/value/downcast.i:25: Warning:
+ unsigned downcast. assert x ≤ 255;
+[eva:alarm] tests/value/downcast.i:28: Warning:
+ unsigned downcast. assert (unsigned int)(uy + uz) ≤ 65535;
+[eva] Recording results for main1
+[eva] Done for function main1
+[eva] computing for function main2_bitfield <- main.
+ Called from tests/value/downcast.i:157.
+[eva:alarm] tests/value/downcast.i:37: Warning:
+ unsigned downcast. assert j ≤ 31;
+[eva] Recording results for main2_bitfield
+[eva] Done for function main2_bitfield
+[eva] computing for function main3_reduction <- main.
+ Called from tests/value/downcast.i:158.
+[eva:alarm] tests/value/downcast.i:44: Warning:
+ unsigned downcast. assert 0 ≤ v;
+[eva:alarm] tests/value/downcast.i:45: Warning:
+ unsigned downcast. assert y ≤ 255;
+[eva] Recording results for main3_reduction
+[eva] Done for function main3_reduction
+[eva] computing for function main4_pointer <- main.
+ Called from tests/value/downcast.i:159.
+[eva:alarm] tests/value/downcast.i:54: Warning:
+ signed overflow. assert -9223372036854775808 ≤ p + (long long)100;
+[eva:alarm] tests/value/downcast.i:54: Warning:
+ signed overflow. assert p + (long long)100 ≤ 9223372036854775807;
+[eva:alarm] tests/value/downcast.i:55: Warning:
+ unsigned downcast. assert 0 ≤ p;
+[eva:alarm] tests/value/downcast.i:55: Warning:
+ unsigned downcast. assert p ≤ 4294967295;
+[eva] Recording results for main4_pointer
+[eva] Done for function main4_pointer
+[eva] computing for function main5_wrap_signed <- main.
+ Called from tests/value/downcast.i:160.
+[eva:alarm] tests/value/downcast.i:62: Warning:
+ assertion 'ASSUME' got status unknown.
+[eva] tests/value/downcast.i:63: assertion got status valid.
+[eva] tests/value/downcast.i:67:
+ Frama_C_show_each:
+ [100000..2147483647], [100145..2147483792], [-2147483648..2147483647]
+[eva:alarm] tests/value/downcast.i:68: Warning: assertion got status unknown.
+[eva] Recording results for main5_wrap_signed
+[eva] Done for function main5_wrap_signed
+[eva] computing for function main6_val_warn_converted_signed <- main.
+ Called from tests/value/downcast.i:161.
+[eva:alarm] tests/value/downcast.i:85: Warning:
+ unsigned downcast. assert 0 ≤ (int)(-12);
+[eva:alarm] tests/value/downcast.i:90: Warning:
+ unsigned downcast. assert 0 ≤ (int)(-64000);
+[eva:alarm] tests/value/downcast.i:95: Warning:
+ pointer downcast. assert (unsigned int)p ≤ 2147483647;
+[eva:alarm] tests/value/downcast.i:96: Warning:
+ pointer downcast. assert (unsigned int)p ≤ 32767;
+[eva:alarm] tests/value/downcast.i:97: Warning:
+ pointer downcast. assert (unsigned int)p ≤ 65535;
+[eva] Recording results for main6_val_warn_converted_signed
+[eva] Done for function main6_val_warn_converted_signed
+[eva] computing for function main7_signed_upcast <- main.
+ Called from tests/value/downcast.i:162.
+[eva] Recording results for main7_signed_upcast
+[eva] Done for function main7_signed_upcast
+[eva] computing for function main8_bitfields <- main.
+ Called from tests/value/downcast.i:163.
+[eva] Recording results for main8_bitfields
+[eva] Done for function main8_bitfields
+[eva] computing for function main9_bitfield <- main.
+ Called from tests/value/downcast.i:164.
+[eva] tests/value/downcast.i:138: assertion got status valid.
+[eva] Recording results for main9_bitfield
+[eva] Done for function main9_bitfield
+[eva] computing for function main10_loop <- main.
+ Called from tests/value/downcast.i:165.
+[eva:alarm] tests/value/downcast.i:150: Warning:
+ unsigned downcast. assert 0 ≤ v;
+[eva:alarm] tests/value/downcast.i:150: Warning:
+ unsigned downcast. assert v ≤ 1023;
+[eva] tests/value/downcast.i:149: starting to merge loop iterations
+[eva] Recording results for main10_loop
+[eva] Done for function main10_loop
+[eva] Recording results for main
+[eva] done for function main
+[eva] tests/value/downcast.i:37:
+ assertion 'Eva,unsigned_downcast' got final status invalid.
+[eva] tests/value/downcast.i:85:
+ assertion 'Eva,unsigned_downcast' got final status invalid.
+[eva] tests/value/downcast.i:90:
+ assertion 'Eva,unsigned_downcast' got final status invalid.
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main1:
+ sz ∈ [--..--]
+ uc ∈ [--..--]
+ x ∈ [--..--]
+ ux ∈ [--..--]
+ s ∈ [--..--]
+[eva:final-states] Values at end of function main10_loop:
+ c ∈ [--..--] or UNINITIALIZED
+ bf.b ∈ [--..--] or UNINITIALIZED
+ .[bits 10 to 31] ∈ UNINITIALIZED
+ k ∈ {10}
+[eva:final-states] Values at end of function main2_bitfield:
+ i ∈ {117}
+ j ∈ {254}
+ ss.i ∈ {-11} or UNINITIALIZED
+ {.j; .[bits 10 to 31]} ∈ UNINITIALIZED
+[eva:final-states] Values at end of function main3_reduction:
+ x_0 ∈ [--..--]
+ c ∈ [--..--]
+ y ∈ [0..255]
+ d ∈ [--..--]
+[eva:final-states] Values at end of function main4_pointer:
+ p ∈ {{ &x_0 + {100} }}
+ q ∈ {{ &x_0 + {100} }}
+ r ∈ {{ &x_0 + {100} }}
+[eva:final-states] Values at end of function main5_wrap_signed:
+ x_0 ∈ [100000..2147483647]
+ y ∈ [100145..2147483792]
+ z ∈ [--..--]
+[eva:final-states] Values at end of function main6_val_warn_converted_signed:
+
+[eva:final-states] Values at end of function main7_signed_upcast:
+ c ∈ {240}
+ i ∈ {240}
+[eva:final-states] Values at end of function main8_bitfields:
+ S.i1 ∈ {65}
+ .i2 ∈ {-1; 1} or UNINITIALIZED
+ .[bits 24 to 31] ∈ UNINITIALIZED
+ c ∈ {-1; 1; 65} or UNINITIALIZED
+[eva:final-states] Values at end of function main9_bitfield:
+ bf.a ∈ {1648}
+ .[bits 11 to 31] ∈ UNINITIALIZED
+ c ∈ {112} or UNINITIALIZED
+[eva:final-states] Values at end of function main:
+ sz ∈ [--..--]
+ uc ∈ [--..--]
+ x ∈ [--..--]
+ ux ∈ [--..--]
+ s ∈ [--..--]
+[from] Computing for function main1
+[from] Done for function main1
+[from] Computing for function main10_loop
+[from] Done for function main10_loop
+[from] Computing for function main2_bitfield
+[from] Done for function main2_bitfield
+[from] Computing for function main3_reduction
+[from] Done for function main3_reduction
+[from] Computing for function main4_pointer
+[from] Done for function main4_pointer
+[from] Computing for function main5_wrap_signed
+[from] Done for function main5_wrap_signed
+[from] Computing for function main6_val_warn_converted_signed
+[from] Done for function main6_val_warn_converted_signed
+[from] Computing for function main7_signed_upcast
+[from] Done for function main7_signed_upcast
+[from] Computing for function main8_bitfields
+[from] Done for function main8_bitfields
+[from] Computing for function main9_bitfield
+[from] Done for function main9_bitfield
+[from] Computing for function main
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function main1:
+ sz FROM sx; sy
+ uc FROM x
+ x FROM uy; uz
+ ux FROM uy; uz
+ s FROM uy; uz
+[from] Function main10_loop:
+ NO EFFECTS
+[from] Function main2_bitfield:
+ NO EFFECTS
+[from] Function main3_reduction:
+ NO EFFECTS
+[from] Function main4_pointer:
+ NO EFFECTS
+[from] Function main5_wrap_signed:
+ NO EFFECTS
+[from] Function main6_val_warn_converted_signed:
+ NO EFFECTS
+[from] Function main7_signed_upcast:
+ NO EFFECTS
+[from] Function main8_bitfields:
+ NO EFFECTS
+[from] Function main9_bitfield:
+ NO EFFECTS
+[from] Function main:
+ sz FROM sx; sy
+ uc FROM x
+ x FROM uy; uz
+ ux FROM uy; uz
+ s FROM uy; uz
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function main1:
+ sz; uc; x; ux; s
+[inout] Inputs for function main1:
+ sx; sy; x; uy; uz
+[inout] Out (internal) for function main10_loop:
+ c; bf.b; k
+[inout] Inputs for function main10_loop:
+ v
+[inout] Out (internal) for function main2_bitfield:
+ i; j; ss{.i; .j}
+[inout] Inputs for function main2_bitfield:
+ v
+[inout] Out (internal) for function main3_reduction:
+ x_0; c; y; d
+[inout] Inputs for function main3_reduction:
+ v
+[inout] Out (internal) for function main4_pointer:
+ p; q; r
+[inout] Inputs for function main4_pointer:
+ \nothing
+[inout] Out (internal) for function main5_wrap_signed:
+ x_0; y; z
+[inout] Inputs for function main5_wrap_signed:
+ v
+[inout] Out (internal) for function main6_val_warn_converted_signed:
+ s_0; u; e; b; e_0; e_1; p; x_0; y; z
+[inout] Inputs for function main6_val_warn_converted_signed:
+ v
+[inout] Out (internal) for function main7_signed_upcast:
+ c; i
+[inout] Inputs for function main7_signed_upcast:
+ \nothing
+[inout] Out (internal) for function main8_bitfields:
+ S{.i1; .i2}; c
+[inout] Inputs for function main8_bitfields:
+ v
+[inout] Out (internal) for function main9_bitfield:
+ bf.a; signed_a; c
+[inout] Inputs for function main9_bitfield:
+ v
+[inout] Out (internal) for function main:
+ sz; uc; x; ux; s
+[inout] Inputs for function main:
+ sx; sy; x; uy; uz; v
diff --git a/tests/value/oracle/downcast.3.res.oracle b/tests/value/oracle/downcast.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..d25d52f4759afa0aabbfca5eb6c5cd47d4312a86
--- /dev/null
+++ b/tests/value/oracle/downcast.3.res.oracle
@@ -0,0 +1,270 @@
+[kernel] Parsing tests/value/downcast.i (no preprocessing)
+[eva] Analyzing an incomplete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ sx ∈ [--..--]
+ sy ∈ [--..--]
+ sz ∈ [--..--]
+ uc ∈ [--..--]
+ x ∈ [--..--]
+ ux ∈ [--..--]
+ uy ∈ [--..--]
+ uz ∈ [--..--]
+ s ∈ [--..--]
+ v ∈ [--..--]
+[eva] computing for function main1 <- main.
+ Called from tests/value/downcast.i:156.
+[eva:alarm] tests/value/downcast.i:23: Warning:
+ signed downcast. assert -128 ≤ (int)((int)sx + (int)sy);
+[eva:alarm] tests/value/downcast.i:23: Warning:
+ signed downcast. assert (int)((int)sx + (int)sy) ≤ 127;
+[eva] Recording results for main1
+[eva] Done for function main1
+[eva] computing for function main2_bitfield <- main.
+ Called from tests/value/downcast.i:157.
+[eva:alarm] tests/value/downcast.i:36: Warning:
+ signed downcast. assert i ≤ 15;
+[eva] Recording results for main2_bitfield
+[eva] Done for function main2_bitfield
+[eva] computing for function main3_reduction <- main.
+ Called from tests/value/downcast.i:158.
+[eva:alarm] tests/value/downcast.i:42: Warning:
+ signed downcast. assert -128 ≤ x_0;
+[eva:alarm] tests/value/downcast.i:42: Warning:
+ signed downcast. assert x_0 ≤ 127;
+[eva] Recording results for main3_reduction
+[eva] Done for function main3_reduction
+[eva] computing for function main4_pointer <- main.
+ Called from tests/value/downcast.i:159.
+[eva:alarm] tests/value/downcast.i:54: Warning:
+ signed overflow. assert -9223372036854775808 ≤ p + (long long)100;
+[eva:alarm] tests/value/downcast.i:54: Warning:
+ signed overflow. assert p + (long long)100 ≤ 9223372036854775807;
+[eva:alarm] tests/value/downcast.i:56: Warning:
+ signed downcast. assert -2147483648 ≤ p;
+[eva:alarm] tests/value/downcast.i:56: Warning:
+ signed downcast. assert p ≤ 2147483647;
+[eva] Recording results for main4_pointer
+[eva] Done for function main4_pointer
+[eva] computing for function main5_wrap_signed <- main.
+ Called from tests/value/downcast.i:160.
+[eva:alarm] tests/value/downcast.i:62: Warning:
+ assertion 'ASSUME' got status unknown.
+[eva] tests/value/downcast.i:63: assertion got status valid.
+[eva] tests/value/downcast.i:67:
+ Frama_C_show_each:
+ [100000..2147483647], [100145..2147483792], [-2147483648..2147483647]
+[eva:alarm] tests/value/downcast.i:68: Warning: assertion got status unknown.
+[eva] Recording results for main5_wrap_signed
+[eva] Done for function main5_wrap_signed
+[eva] computing for function main6_val_warn_converted_signed <- main.
+ Called from tests/value/downcast.i:161.
+[eva:alarm] tests/value/downcast.i:75: Warning:
+ signed downcast. assert (int)65300u ≤ 32767;
+[eva:alarm] tests/value/downcast.i:91: Warning:
+ signed downcast. assert -32768 ≤ (int)e_1;
+[eva:alarm] tests/value/downcast.i:95: Warning:
+ pointer downcast. assert (unsigned int)p ≤ 2147483647;
+[eva:alarm] tests/value/downcast.i:96: Warning:
+ pointer downcast. assert (unsigned int)p ≤ 32767;
+[eva:alarm] tests/value/downcast.i:97: Warning:
+ pointer downcast. assert (unsigned int)p ≤ 65535;
+[eva] Recording results for main6_val_warn_converted_signed
+[eva] Done for function main6_val_warn_converted_signed
+[eva] computing for function main7_signed_upcast <- main.
+ Called from tests/value/downcast.i:162.
+[eva] Recording results for main7_signed_upcast
+[eva] Done for function main7_signed_upcast
+[eva] computing for function main8_bitfields <- main.
+ Called from tests/value/downcast.i:163.
+[eva:alarm] tests/value/downcast.i:123: Warning:
+ signed downcast. assert (int)S.i1 ≤ 31;
+[eva:alarm] tests/value/downcast.i:124: Warning:
+ signed downcast. assert (int)S.i1 ≤ 127;
+[eva:alarm] tests/value/downcast.i:128: Warning:
+ signed downcast. assert (int)S.i1 ≤ 31;
+[eva] Recording results for main8_bitfields
+[eva] Done for function main8_bitfields
+[eva] computing for function main9_bitfield <- main.
+ Called from tests/value/downcast.i:164.
+[eva] tests/value/downcast.i:138: assertion got status valid.
+[eva:alarm] tests/value/downcast.i:141: Warning:
+ signed downcast. assert -128 ≤ (int)bf.a;
+[eva] Recording results for main9_bitfield
+[eva] Done for function main9_bitfield
+[eva] computing for function main10_loop <- main.
+ Called from tests/value/downcast.i:165.
+[eva:alarm] tests/value/downcast.i:151: Warning:
+ signed downcast. assert -128 ≤ (int)bf.b;
+[eva:alarm] tests/value/downcast.i:151: Warning:
+ signed downcast. assert (int)bf.b ≤ 127;
+[eva] tests/value/downcast.i:149: starting to merge loop iterations
+[eva] Recording results for main10_loop
+[eva] Done for function main10_loop
+[eva] Recording results for main
+[eva] done for function main
+[eva] tests/value/downcast.i:36:
+ assertion 'Eva,signed_downcast' got final status invalid.
+[eva] tests/value/downcast.i:75:
+ assertion 'Eva,signed_downcast' got final status invalid.
+[eva] tests/value/downcast.i:91:
+ assertion 'Eva,signed_downcast' got final status invalid.
+[eva] tests/value/downcast.i:123:
+ assertion 'Eva,signed_downcast' got final status invalid.
+[eva] tests/value/downcast.i:124:
+ assertion 'Eva,signed_downcast' got final status invalid.
+[eva] tests/value/downcast.i:128:
+ assertion 'Eva,signed_downcast' got final status invalid.
+[eva] tests/value/downcast.i:141:
+ assertion 'Eva,signed_downcast' got final status invalid.
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main1:
+ sz ∈ [--..--]
+ uc ∈ [--..--]
+ x ∈ [--..--]
+ ux ∈ [--..--]
+ s ∈ [--..--]
+[eva:final-states] Values at end of function main10_loop:
+ c ∈ [--..--] or UNINITIALIZED
+ bf.b ∈ [--..--] or UNINITIALIZED
+ .[bits 10 to 31] ∈ UNINITIALIZED
+ k ∈ {10}
+[eva:final-states] Values at end of function main2_bitfield:
+ i ∈ {117}
+ j ∈ {254}
+ ss.i ∈ UNINITIALIZED
+ .j ∈ {30} or UNINITIALIZED
+ .[bits 10 to 31] ∈ UNINITIALIZED
+[eva:final-states] Values at end of function main3_reduction:
+ x_0 ∈ [-128..127]
+ c ∈ [--..--]
+ y ∈ [--..--]
+ d ∈ [--..--]
+[eva:final-states] Values at end of function main4_pointer:
+ p ∈ {{ &x_0 + {100} }}
+ q ∈ {{ &x_0 + {100} }}
+ r ∈ {{ &x_0 + {100} }}
+[eva:final-states] Values at end of function main5_wrap_signed:
+ x_0 ∈ [100000..2147483647]
+ y ∈ [100145..2147483792]
+ z ∈ [--..--]
+[eva:final-states] Values at end of function main6_val_warn_converted_signed:
+
+[eva:final-states] Values at end of function main7_signed_upcast:
+ c ∈ {240}
+ i ∈ {240}
+[eva:final-states] Values at end of function main8_bitfields:
+ S.i1 ∈ {65}
+ .i2 ∈ {-1} or UNINITIALIZED
+ .[bits 24 to 31] ∈ UNINITIALIZED
+ c ∈ {-1; 65} or UNINITIALIZED
+[eva:final-states] Values at end of function main9_bitfield:
+ bf.a ∈ {1648}
+ .[bits 11 to 31] ∈ UNINITIALIZED
+ c ∈ UNINITIALIZED
+[eva:final-states] Values at end of function main:
+ sz ∈ [--..--]
+ uc ∈ [--..--]
+ x ∈ [--..--]
+ ux ∈ [--..--]
+ s ∈ [--..--]
+[from] Computing for function main1
+[from] Done for function main1
+[from] Computing for function main10_loop
+[from] Done for function main10_loop
+[from] Computing for function main2_bitfield
+[from] Done for function main2_bitfield
+[from] Computing for function main3_reduction
+[from] Done for function main3_reduction
+[from] Computing for function main4_pointer
+[from] Done for function main4_pointer
+[from] Computing for function main5_wrap_signed
+[from] Done for function main5_wrap_signed
+[from] Computing for function main6_val_warn_converted_signed
+[from] Done for function main6_val_warn_converted_signed
+[from] Computing for function main7_signed_upcast
+[from] Done for function main7_signed_upcast
+[from] Computing for function main8_bitfields
+[from] Done for function main8_bitfields
+[from] Computing for function main9_bitfield
+[from] Done for function main9_bitfield
+[from] Computing for function main
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function main1:
+ sz FROM sx; sy
+ uc FROM x
+ x FROM uy; uz
+ ux FROM uy; uz
+ s FROM uy; uz
+[from] Function main10_loop:
+ NO EFFECTS
+[from] Function main2_bitfield:
+ NO EFFECTS
+[from] Function main3_reduction:
+ NO EFFECTS
+[from] Function main4_pointer:
+ NO EFFECTS
+[from] Function main5_wrap_signed:
+ NO EFFECTS
+[from] Function main6_val_warn_converted_signed:
+ NO EFFECTS
+[from] Function main7_signed_upcast:
+ NO EFFECTS
+[from] Function main8_bitfields:
+ NO EFFECTS
+[from] Function main9_bitfield:
+ NO EFFECTS
+[from] Function main:
+ sz FROM sx; sy
+ uc FROM x
+ x FROM uy; uz
+ ux FROM uy; uz
+ s FROM uy; uz
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function main1:
+ sz; uc; x; ux; s
+[inout] Inputs for function main1:
+ sx; sy; x; uy; uz
+[inout] Out (internal) for function main10_loop:
+ c; bf.b; k
+[inout] Inputs for function main10_loop:
+ v
+[inout] Out (internal) for function main2_bitfield:
+ i; j; ss{.i; .j}
+[inout] Inputs for function main2_bitfield:
+ v
+[inout] Out (internal) for function main3_reduction:
+ x_0; c; y; d
+[inout] Inputs for function main3_reduction:
+ v
+[inout] Out (internal) for function main4_pointer:
+ p; q; r
+[inout] Inputs for function main4_pointer:
+ \nothing
+[inout] Out (internal) for function main5_wrap_signed:
+ x_0; y; z
+[inout] Inputs for function main5_wrap_signed:
+ v
+[inout] Out (internal) for function main6_val_warn_converted_signed:
+ s_0; u; e; b; e_0; b_0; e_1; b_1; p; x_0; y; z
+[inout] Inputs for function main6_val_warn_converted_signed:
+ v
+[inout] Out (internal) for function main7_signed_upcast:
+ c; i
+[inout] Inputs for function main7_signed_upcast:
+ \nothing
+[inout] Out (internal) for function main8_bitfields:
+ S{.i1; .i2}; c
+[inout] Inputs for function main8_bitfields:
+ v
+[inout] Out (internal) for function main9_bitfield:
+ bf.a; signed_a; c
+[inout] Inputs for function main9_bitfield:
+ v
+[inout] Out (internal) for function main:
+ sz; uc; x; ux; s
+[inout] Inputs for function main:
+ sx; sy; x; uy; uz; v
diff --git a/tests/value/oracle/downcast.4.res.oracle b/tests/value/oracle/downcast.4.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..d691ffe3fe111924fcefe788f39991a23f6f2f9b
--- /dev/null
+++ b/tests/value/oracle/downcast.4.res.oracle
@@ -0,0 +1,226 @@
+[kernel] Parsing tests/value/downcast.i (no preprocessing)
+[eva] Analyzing an incomplete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ sx ∈ [--..--]
+ sy ∈ [--..--]
+ sz ∈ [--..--]
+ uc ∈ [--..--]
+ x ∈ [--..--]
+ ux ∈ [--..--]
+ uy ∈ [--..--]
+ uz ∈ [--..--]
+ s ∈ [--..--]
+ v ∈ [--..--]
+[eva] computing for function main1 <- main.
+ Called from tests/value/downcast.i:156.
+[eva] Recording results for main1
+[eva] Done for function main1
+[eva] computing for function main2_bitfield <- main.
+ Called from tests/value/downcast.i:157.
+[eva] Recording results for main2_bitfield
+[eva] Done for function main2_bitfield
+[eva] computing for function main3_reduction <- main.
+ Called from tests/value/downcast.i:158.
+[eva] Recording results for main3_reduction
+[eva] Done for function main3_reduction
+[eva] computing for function main4_pointer <- main.
+ Called from tests/value/downcast.i:159.
+[eva:alarm] tests/value/downcast.i:54: Warning:
+ signed overflow. assert -9223372036854775808 ≤ p + (long long)100;
+[eva:alarm] tests/value/downcast.i:54: Warning:
+ signed overflow. assert p + (long long)100 ≤ 9223372036854775807;
+[eva] Recording results for main4_pointer
+[eva] Done for function main4_pointer
+[eva] computing for function main5_wrap_signed <- main.
+ Called from tests/value/downcast.i:160.
+[eva:alarm] tests/value/downcast.i:62: Warning:
+ assertion 'ASSUME' got status unknown.
+[eva] tests/value/downcast.i:63: assertion got status valid.
+[eva] tests/value/downcast.i:67:
+ Frama_C_show_each:
+ [100000..2147483647], [100145..2147483792], [-2147483648..2147483647]
+[eva:alarm] tests/value/downcast.i:68: Warning: assertion got status unknown.
+[eva] Recording results for main5_wrap_signed
+[eva] Done for function main5_wrap_signed
+[eva] computing for function main6_val_warn_converted_signed <- main.
+ Called from tests/value/downcast.i:161.
+[eva] tests/value/downcast.i:96:
+ Assigning imprecise value to y.
+ The imprecision originates from Arithmetic {tests/value/downcast.i:96}
+[eva] tests/value/downcast.i:97:
+ Assigning imprecise value to z.
+ The imprecision originates from Arithmetic {tests/value/downcast.i:97}
+[eva] Recording results for main6_val_warn_converted_signed
+[eva] Done for function main6_val_warn_converted_signed
+[eva] computing for function main7_signed_upcast <- main.
+ Called from tests/value/downcast.i:162.
+[eva] Recording results for main7_signed_upcast
+[eva] Done for function main7_signed_upcast
+[eva] computing for function main8_bitfields <- main.
+ Called from tests/value/downcast.i:163.
+[eva] Recording results for main8_bitfields
+[eva] Done for function main8_bitfields
+[eva] computing for function main9_bitfield <- main.
+ Called from tests/value/downcast.i:164.
+[eva] tests/value/downcast.i:138: assertion got status valid.
+[eva] Recording results for main9_bitfield
+[eva] Done for function main9_bitfield
+[eva] computing for function main10_loop <- main.
+ Called from tests/value/downcast.i:165.
+[eva] tests/value/downcast.i:149: starting to merge loop iterations
+[eva] Recording results for main10_loop
+[eva] Done for function main10_loop
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main1:
+ sz ∈ [--..--]
+ uc ∈ [--..--]
+ x ∈ [--..--]
+ ux ∈ [--..--]
+ s ∈ [--..--]
+[eva:final-states] Values at end of function main10_loop:
+ c ∈ [--..--] or UNINITIALIZED
+ bf.b ∈ [--..--] or UNINITIALIZED
+ .[bits 10 to 31] ∈ UNINITIALIZED
+ k ∈ {10}
+[eva:final-states] Values at end of function main2_bitfield:
+ i ∈ {117}
+ j ∈ {254}
+ ss.i ∈ {-11} or UNINITIALIZED
+ .j ∈ {30} or UNINITIALIZED
+ .[bits 10 to 31] ∈ UNINITIALIZED
+[eva:final-states] Values at end of function main3_reduction:
+ x_0 ∈ [--..--]
+ c ∈ [--..--]
+ y ∈ [--..--]
+ d ∈ [--..--]
+[eva:final-states] Values at end of function main4_pointer:
+ p ∈ {{ &x_0 + {100} }}
+ q ∈ {{ &x_0 + {100} }}
+ r ∈ {{ &x_0 + {100} }}
+[eva:final-states] Values at end of function main5_wrap_signed:
+ x_0 ∈ [100000..2147483647]
+ y ∈ [100145..2147483792]
+ z ∈ [--..--]
+[eva:final-states] Values at end of function main6_val_warn_converted_signed:
+
+[eva:final-states] Values at end of function main7_signed_upcast:
+ c ∈ {240}
+ i ∈ {240}
+[eva:final-states] Values at end of function main8_bitfields:
+ S.i1 ∈ {65}
+ .i2 ∈ {-1; 1} or UNINITIALIZED
+ .[bits 24 to 31] ∈ UNINITIALIZED
+ c ∈ {-1; 1; 65} or UNINITIALIZED
+[eva:final-states] Values at end of function main9_bitfield:
+ bf.a ∈ {1648}
+ .[bits 11 to 31] ∈ UNINITIALIZED
+ c ∈ {112} or UNINITIALIZED
+[eva:final-states] Values at end of function main:
+ sz ∈ [--..--]
+ uc ∈ [--..--]
+ x ∈ [--..--]
+ ux ∈ [--..--]
+ s ∈ [--..--]
+[from] Computing for function main1
+[from] Done for function main1
+[from] Computing for function main10_loop
+[from] Done for function main10_loop
+[from] Computing for function main2_bitfield
+[from] Done for function main2_bitfield
+[from] Computing for function main3_reduction
+[from] Done for function main3_reduction
+[from] Computing for function main4_pointer
+[from] Done for function main4_pointer
+[from] Computing for function main5_wrap_signed
+[from] Done for function main5_wrap_signed
+[from] Computing for function main6_val_warn_converted_signed
+[from] Done for function main6_val_warn_converted_signed
+[from] Computing for function main7_signed_upcast
+[from] Done for function main7_signed_upcast
+[from] Computing for function main8_bitfields
+[from] Done for function main8_bitfields
+[from] Computing for function main9_bitfield
+[from] Done for function main9_bitfield
+[from] Computing for function main
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function main1:
+ sz FROM sx; sy
+ uc FROM x
+ x FROM uy; uz
+ ux FROM uy; uz
+ s FROM uy; uz
+[from] Function main10_loop:
+ NO EFFECTS
+[from] Function main2_bitfield:
+ NO EFFECTS
+[from] Function main3_reduction:
+ NO EFFECTS
+[from] Function main4_pointer:
+ NO EFFECTS
+[from] Function main5_wrap_signed:
+ NO EFFECTS
+[from] Function main6_val_warn_converted_signed:
+ NO EFFECTS
+[from] Function main7_signed_upcast:
+ NO EFFECTS
+[from] Function main8_bitfields:
+ NO EFFECTS
+[from] Function main9_bitfield:
+ NO EFFECTS
+[from] Function main:
+ sz FROM sx; sy
+ uc FROM x
+ x FROM uy; uz
+ ux FROM uy; uz
+ s FROM uy; uz
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function main1:
+ sz; uc; x; ux; s
+[inout] Inputs for function main1:
+ sx; sy; x; uy; uz
+[inout] Out (internal) for function main10_loop:
+ c; bf.b; k
+[inout] Inputs for function main10_loop:
+ v
+[inout] Out (internal) for function main2_bitfield:
+ i; j; ss{.i; .j}
+[inout] Inputs for function main2_bitfield:
+ v
+[inout] Out (internal) for function main3_reduction:
+ x_0; c; y; d
+[inout] Inputs for function main3_reduction:
+ v
+[inout] Out (internal) for function main4_pointer:
+ p; q; r
+[inout] Inputs for function main4_pointer:
+ \nothing
+[inout] Out (internal) for function main5_wrap_signed:
+ x_0; y; z
+[inout] Inputs for function main5_wrap_signed:
+ v
+[inout] Out (internal) for function main6_val_warn_converted_signed:
+ s_0; u; e; b; e_0; b_0; e_1; b_1; p; x_0; y; z
+[inout] Inputs for function main6_val_warn_converted_signed:
+ v
+[inout] Out (internal) for function main7_signed_upcast:
+ c; i
+[inout] Inputs for function main7_signed_upcast:
+ \nothing
+[inout] Out (internal) for function main8_bitfields:
+ S{.i1; .i2}; c
+[inout] Inputs for function main8_bitfields:
+ v
+[inout] Out (internal) for function main9_bitfield:
+ bf.a; signed_a; c
+[inout] Inputs for function main9_bitfield:
+ v
+[inout] Out (internal) for function main:
+ sz; uc; x; ux; s
+[inout] Inputs for function main:
+ sx; sy; x; uy; uz; v
diff --git a/tests/value/oracle/downcast.res.oracle b/tests/value/oracle/downcast.res.oracle
deleted file mode 100644
index 18b563a5f18a5c227a7f0f3e1f69a537e4b39aad..0000000000000000000000000000000000000000
--- a/tests/value/oracle/downcast.res.oracle
+++ /dev/null
@@ -1,1812 +0,0 @@
-[kernel] Parsing tests/value/downcast.i (no preprocessing)
-[eva] Analyzing an incomplete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- sx ∈ [--..--]
- sy ∈ [--..--]
- sz ∈ [--..--]
- uc ∈ [--..--]
- x ∈ [--..--]
- ux ∈ [--..--]
- uy ∈ [--..--]
- uz ∈ [--..--]
- s ∈ [--..--]
- v ∈ [--..--]
-[eva] computing for function main1 <- main.
- Called from tests/value/downcast.i:152.
-[eva:alarm] tests/value/downcast.i:19: Warning:
- signed downcast. assert -128 ≤ (int)((int)sx + (int)sy);
-[eva:alarm] tests/value/downcast.i:19: Warning:
- signed downcast. assert (int)((int)sx + (int)sy) ≤ 127;
-[eva:alarm] tests/value/downcast.i:22: Warning:
- signed downcast. assert (unsigned int)(uy + uz) ≤ 2147483647;
-[eva] Recording results for main1
-[eva] Done for function main1
-[eva] computing for function main2_bitfield <- main.
- Called from tests/value/downcast.i:153.
-[eva:alarm] tests/value/downcast.i:32: Warning:
- signed downcast. assert i ≤ 15;
-[eva] Recording results for main2_bitfield
-[eva] Done for function main2_bitfield
-[eva] computing for function main3_reduction <- main.
- Called from tests/value/downcast.i:154.
-[eva:alarm] tests/value/downcast.i:38: Warning:
- signed downcast. assert -128 ≤ x_0;
-[eva:alarm] tests/value/downcast.i:38: Warning:
- signed downcast. assert x_0 ≤ 127;
-[eva] Recording results for main3_reduction
-[eva] Done for function main3_reduction
-[eva] computing for function main4_pointer <- main.
- Called from tests/value/downcast.i:155.
-[eva:alarm] tests/value/downcast.i:50: Warning:
- signed overflow. assert -9223372036854775808 ≤ p + (long long)100;
-[eva:alarm] tests/value/downcast.i:50: Warning:
- signed overflow. assert p + (long long)100 ≤ 9223372036854775807;
-[eva:alarm] tests/value/downcast.i:52: Warning:
- signed downcast. assert -2147483648 ≤ p;
-[eva:alarm] tests/value/downcast.i:52: Warning:
- signed downcast. assert p ≤ 2147483647;
-[eva] Recording results for main4_pointer
-[eva] Done for function main4_pointer
-[eva] computing for function main5_wrap_signed <- main.
- Called from tests/value/downcast.i:156.
-[eva:alarm] tests/value/downcast.i:58: Warning:
- assertion 'ASSUME' got status unknown.
-[eva] tests/value/downcast.i:59: assertion got status valid.
-[eva:alarm] tests/value/downcast.i:62: Warning:
- signed downcast. assert y ≤ 2147483647;
-[eva] tests/value/downcast.i:63:
- Frama_C_show_each:
- [100000..2147483647], [100145..2147483647], [100145..2147483647]
-[eva] tests/value/downcast.i:64: assertion got status valid.
-[eva] Recording results for main5_wrap_signed
-[eva] Done for function main5_wrap_signed
-[eva] computing for function main6_val_warn_converted_signed <- main.
- Called from tests/value/downcast.i:157.
-[eva:alarm] tests/value/downcast.i:71: Warning:
- signed downcast. assert 65300u ≤ 32767;
-[eva:alarm] tests/value/downcast.i:82: Warning:
- signed downcast. assert e_0 ≤ 32767;
-[eva:alarm] tests/value/downcast.i:87: Warning:
- signed downcast. assert e_1 ≤ 32767;
-[eva:alarm] tests/value/downcast.i:91: Warning:
- signed downcast. assert p ≤ 2147483647;
-[eva:alarm] tests/value/downcast.i:92: Warning:
- signed downcast. assert p ≤ 32767;
-[eva] tests/value/downcast.i:93:
- Assigning imprecise value to z.
- The imprecision originates from Arithmetic {tests/value/downcast.i:93}
-[eva] Recording results for main6_val_warn_converted_signed
-[eva] Done for function main6_val_warn_converted_signed
-[eva] computing for function main7_signed_upcast <- main.
- Called from tests/value/downcast.i:158.
-[eva] Recording results for main7_signed_upcast
-[eva] Done for function main7_signed_upcast
-[eva] computing for function main8_bitfields <- main.
- Called from tests/value/downcast.i:159.
-[eva:alarm] tests/value/downcast.i:114: Warning:
- signed downcast. assert S.i1 ≤ 31;
-[eva:alarm] tests/value/downcast.i:115: Warning:
- signed downcast. assert S.i1 ≤ 127;
-[eva:alarm] tests/value/downcast.i:119: Warning:
- signed downcast. assert S.i1 ≤ 31;
-[eva:alarm] tests/value/downcast.i:120: Warning:
- signed downcast. assert S.i1 ≤ 127;
-[eva:alarm] tests/value/downcast.i:124: Warning:
- signed downcast. assert S.i1 ≤ 31;
-[eva] Recording results for main8_bitfields
-[eva] Done for function main8_bitfields
-[eva] computing for function main9_bitfield <- main.
- Called from tests/value/downcast.i:160.
-[eva:alarm] tests/value/downcast.i:133: Warning:
- signed downcast. assert bf.a ≤ 1023;
-[eva:alarm] tests/value/downcast.i:137: Warning:
- signed downcast. assert bf.a ≤ 127;
-[eva] Recording results for main9_bitfield
-[eva] Done for function main9_bitfield
-[eva] computing for function main10_loop <- main.
- Called from tests/value/downcast.i:161.
-[eva:alarm] tests/value/downcast.i:147: Warning:
- signed downcast. assert bf.b ≤ 127;
-[eva] tests/value/downcast.i:145: starting to merge loop iterations
-[eva] Recording results for main10_loop
-[eva] Done for function main10_loop
-[eva] Recording results for main
-[eva] done for function main
-[eva] tests/value/downcast.i:32:
- assertion 'Eva,signed_downcast' got final status invalid.
-[eva] tests/value/downcast.i:71:
- assertion 'Eva,signed_downcast' got final status invalid.
-[eva] tests/value/downcast.i:82:
- assertion 'Eva,signed_downcast' got final status invalid.
-[eva] tests/value/downcast.i:87:
- assertion 'Eva,signed_downcast' got final status invalid.
-[eva] tests/value/downcast.i:114:
- assertion 'Eva,signed_downcast' got final status invalid.
-[eva] tests/value/downcast.i:115:
- assertion 'Eva,signed_downcast' got final status invalid.
-[eva] tests/value/downcast.i:119:
- assertion 'Eva,signed_downcast' got final status invalid.
-[eva] tests/value/downcast.i:120:
- assertion 'Eva,signed_downcast' got final status invalid.
-[eva] tests/value/downcast.i:124:
- assertion 'Eva,signed_downcast' got final status invalid.
-[eva] tests/value/downcast.i:133:
- assertion 'Eva,signed_downcast' got final status invalid.
-[eva] tests/value/downcast.i:137:
- assertion 'Eva,signed_downcast' got final status invalid.
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function main1:
- sz ∈ [--..--]
- uc ∈ [--..--]
- x ∈ [0..2147483647]
- ux ∈ [--..--]
- s ∈ [--..--]
-[eva:final-states] Values at end of function main10_loop:
- c ∈ [0..127] or UNINITIALIZED
- bf.b ∈ [--..--] or UNINITIALIZED
- .[bits 10 to 31] ∈ UNINITIALIZED
- k ∈ {10}
-[eva:final-states] Values at end of function main2_bitfield:
- i ∈ {117}
- j ∈ {254}
- ss.i ∈ UNINITIALIZED
- .j ∈ {30} or UNINITIALIZED
- .[bits 10 to 31] ∈ UNINITIALIZED
-[eva:final-states] Values at end of function main3_reduction:
- x_0 ∈ [-128..127]
- c ∈ [--..--]
- y ∈ [--..--]
- d ∈ [--..--]
-[eva:final-states] Values at end of function main4_pointer:
- p ∈ {{ &x_0 + {100} }}
- q ∈ {{ &x_0 + {100} }}
- r ∈ {{ &x_0 + {100} }}
-[eva:final-states] Values at end of function main5_wrap_signed:
- x_0 ∈ [100000..2147483647]
- y ∈ [100145..2147483647]
- z ∈ [100145..2147483647]
-[eva:final-states] Values at end of function main6_val_warn_converted_signed:
-
-[eva:final-states] Values at end of function main7_signed_upcast:
- c ∈ {240}
- i ∈ {240}
-[eva:final-states] Values at end of function main8_bitfields:
- S.i1 ∈ {65}
- {.i2; .[bits 24 to 31]} ∈ UNINITIALIZED
- c ∈ {65} or UNINITIALIZED
-[eva:final-states] Values at end of function main9_bitfield:
- bf.a ∈ {1648}
- .[bits 11 to 31] ∈ UNINITIALIZED
- c ∈ UNINITIALIZED
-[eva:final-states] Values at end of function main:
- sz ∈ [--..--]
- uc ∈ [--..--]
- x ∈ [0..2147483647]
- ux ∈ [--..--]
- s ∈ [--..--]
-[from] Computing for function main1
-[from] Done for function main1
-[from] Computing for function main10_loop
-[from] Done for function main10_loop
-[from] Computing for function main2_bitfield
-[from] Done for function main2_bitfield
-[from] Computing for function main3_reduction
-[from] Done for function main3_reduction
-[from] Computing for function main4_pointer
-[from] Done for function main4_pointer
-[from] Computing for function main5_wrap_signed
-[from] Done for function main5_wrap_signed
-[from] Computing for function main6_val_warn_converted_signed
-[from] Done for function main6_val_warn_converted_signed
-[from] Computing for function main7_signed_upcast
-[from] Done for function main7_signed_upcast
-[from] Computing for function main8_bitfields
-[from] Done for function main8_bitfields
-[from] Computing for function main9_bitfield
-[from] Done for function main9_bitfield
-[from] Computing for function main
-[from] Done for function main
-[from] ====== DEPENDENCIES COMPUTED ======
- These dependencies hold at termination for the executions that terminate:
-[from] Function main1:
- sz FROM sx; sy
- uc FROM x
- x FROM uy; uz
- ux FROM uy; uz
- s FROM uy; uz
-[from] Function main10_loop:
- NO EFFECTS
-[from] Function main2_bitfield:
- NO EFFECTS
-[from] Function main3_reduction:
- NO EFFECTS
-[from] Function main4_pointer:
- NO EFFECTS
-[from] Function main5_wrap_signed:
- NO EFFECTS
-[from] Function main6_val_warn_converted_signed:
- NO EFFECTS
-[from] Function main7_signed_upcast:
- NO EFFECTS
-[from] Function main8_bitfields:
- NO EFFECTS
-[from] Function main9_bitfield:
- NO EFFECTS
-[from] Function main:
- sz FROM sx; sy
- uc FROM x
- x FROM uy; uz
- ux FROM uy; uz
- s FROM uy; uz
-[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function main1:
- sz; uc; x; ux; s
-[inout] Inputs for function main1:
- sx; sy; x; uy; uz
-[inout] Out (internal) for function main10_loop:
- c; bf.b; k
-[inout] Inputs for function main10_loop:
- v
-[inout] Out (internal) for function main2_bitfield:
- i; j; ss{.i; .j}
-[inout] Inputs for function main2_bitfield:
- v
-[inout] Out (internal) for function main3_reduction:
- x_0; c; y; d
-[inout] Inputs for function main3_reduction:
- v
-[inout] Out (internal) for function main4_pointer:
- p; q; r
-[inout] Inputs for function main4_pointer:
- \nothing
-[inout] Out (internal) for function main5_wrap_signed:
- x_0; y; z
-[inout] Inputs for function main5_wrap_signed:
- v
-[inout] Out (internal) for function main6_val_warn_converted_signed:
- s_0; u; e; b; e_0; b_0; e_1; b_1; p; x_0; y; z
-[inout] Inputs for function main6_val_warn_converted_signed:
- v
-[inout] Out (internal) for function main7_signed_upcast:
- c; i
-[inout] Inputs for function main7_signed_upcast:
- \nothing
-[inout] Out (internal) for function main8_bitfields:
- S{.i1; .i2}; c
-[inout] Inputs for function main8_bitfields:
- v
-[inout] Out (internal) for function main9_bitfield:
- bf.a; signed_a; c
-[inout] Inputs for function main9_bitfield:
- v
-[inout] Out (internal) for function main:
- sz; uc; x; ux; s
-[inout] Inputs for function main:
- sx; sy; x; uy; uz; v
-[report] Computing properties status...
-
---------------------------------------------------------------------------------
---- Properties of Function 'main1'
---------------------------------------------------------------------------------
-
-[ - ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 19)
- tried with Eva.
-[ - ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 19)
- tried with Eva.
-[ - ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 22)
- tried with Eva.
-
---------------------------------------------------------------------------------
---- Properties of Function 'main2_bitfield'
---------------------------------------------------------------------------------
-
-[ Alarm ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 32)
- By Eva, with pending:
- - Unreachable instruction (file tests/value/downcast.i, line 32)
-
---------------------------------------------------------------------------------
---- Properties of Function 'main3_reduction'
---------------------------------------------------------------------------------
-
-[ - ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 38)
- tried with Eva.
-[ - ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 38)
- tried with Eva.
-
---------------------------------------------------------------------------------
---- Properties of Function 'main4_pointer'
---------------------------------------------------------------------------------
-
-[ - ] Assertion 'Eva,signed_overflow' (file tests/value/downcast.i, line 50)
- tried with Eva.
-[ - ] Assertion 'Eva,signed_overflow' (file tests/value/downcast.i, line 50)
- tried with Eva.
-[ - ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 52)
- tried with Eva.
-[ - ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 52)
- tried with Eva.
-
---------------------------------------------------------------------------------
---- Properties of Function 'main5_wrap_signed'
---------------------------------------------------------------------------------
-
-[ - ] Assertion 'ASSUME' (file tests/value/downcast.i, line 58)
- tried with Eva.
-[ Valid ] Assertion (file tests/value/downcast.i, line 59)
- by Eva.
-[ Valid ] Assertion (file tests/value/downcast.i, line 64)
- by Eva.
-[ - ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 62)
- tried with Eva.
-
---------------------------------------------------------------------------------
---- Properties of Function 'main6_val_warn_converted_signed'
---------------------------------------------------------------------------------
-
-[ Alarm ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 71)
- By Eva, with pending:
- - Unreachable initialization of 's_0' (file tests/value/downcast.i, line 71)
-[ Alarm ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 82)
- By Eva, with pending:
- - Unreachable initialization of 'b_0' (file tests/value/downcast.i, line 82)
-[ Alarm ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 87)
- By Eva, with pending:
- - Unreachable initialization of 'b_1' (file tests/value/downcast.i, line 87)
-[ - ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 91)
- tried with Eva.
-[ - ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 92)
- tried with Eva.
-
---------------------------------------------------------------------------------
---- Properties of Function 'main8_bitfields'
---------------------------------------------------------------------------------
-
-[ Alarm ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 114)
- By Eva, with pending:
- - Unreachable instruction (file tests/value/downcast.i, line 114)
-[ Alarm ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 115)
- By Eva, with pending:
- - Unreachable instruction (file tests/value/downcast.i, line 115)
-[ Alarm ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 119)
- By Eva, with pending:
- - Unreachable instruction (file tests/value/downcast.i, line 119)
-[ Alarm ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 120)
- By Eva, with pending:
- - Unreachable instruction (file tests/value/downcast.i, line 120)
-[ Alarm ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 124)
- By Eva, with pending:
- - Unreachable instruction (file tests/value/downcast.i, line 124)
-
---------------------------------------------------------------------------------
---- Properties of Function 'main9_bitfield'
---------------------------------------------------------------------------------
-
-[ Dead ] Assertion (file tests/value/downcast.i, line 134)
- Locally valid, but unreachable.
- By Eva because:
- - Unreachable program point (file tests/value/downcast.i, line 134)
-[ Alarm ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 133)
- By Eva, with pending:
- - Unreachable initialization of 'signed_a' (file tests/value/downcast.i, line 133)
-[ Alarm ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 137)
- By Eva, with pending:
- - Unreachable instruction (file tests/value/downcast.i, line 137)
-[Unreachable] Unreachable program point (file tests/value/downcast.i, line 134)
- by Eva.
-
---------------------------------------------------------------------------------
---- Properties of Function 'main10_loop'
---------------------------------------------------------------------------------
-
-[ - ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 147)
- tried with Eva.
-
---------------------------------------------------------------------------------
---- Status Report Summary
---------------------------------------------------------------------------------
- 2 Completely validated
- 14 To be validated
- 11 Alarms emitted
- 1 Dead property
- 1 Unreachable
- 29 Total
---------------------------------------------------------------------------------
-/* Generated by Frama-C */
-struct s {
- int i : 5 ;
- unsigned int j : 5 ;
-};
-struct bitf {
- unsigned int i1 : 18 ;
- int i2 : 6 ;
-};
-struct __anonstruct_bf_1 {
- unsigned int a : 11 ;
-};
-struct __anonstruct_bf_2 {
- unsigned int b : 10 ;
-};
-signed char sx;
-signed char sy;
-signed char sz;
-unsigned char uc;
-int x;
-unsigned int ux;
-unsigned int uy;
-unsigned int uz;
-unsigned short s;
-int volatile v;
-void main1(void)
-{
- /*@ assert Eva: signed_downcast: -128 ≤ (int)((int)sx + (int)sy); */
- /*@ assert Eva: signed_downcast: (int)((int)sx + (int)sy) ≤ 127; */
- sz = (signed char)((int)sx + (int)sy);
- uc = (unsigned char)((int)sx + (int)sy);
- uc = (unsigned char)x;
- /*@ assert Eva: signed_downcast: (unsigned int)(uy + uz) ≤ 2147483647; */
- x = (int)(uy + uz);
- ux = uy + uz;
- s = (unsigned short)(uy + uz);
- return;
-}
-
-void main2_bitfield(void)
-{
- struct s ss;
- int i = 117;
- unsigned int j = (unsigned int)254;
- if (v)
- /*@ assert Eva: signed_downcast: i ≤ 15; */
- ss.i = (int)i;
- if (v) ss.j = (unsigned int)j;
- return;
-}
-
-void main3_reduction(void)
-{
- int x_0 = v;
- /*@ assert Eva: signed_downcast: -128 ≤ x_0; */
- /*@ assert Eva: signed_downcast: x_0 ≤ 127; */
- char c = (char)x_0;
- unsigned int y = (unsigned int)v;
- unsigned char d = (unsigned char)y;
- return;
-}
-
-void main4_pointer(void)
-{
- int x_0;
- long long p = (long long)(& x_0);
- /*@ assert
- Eva: signed_overflow: -9223372036854775808 ≤ p + (long long)100;
- */
- /*@ assert
- Eva: signed_overflow: p + (long long)100 ≤ 9223372036854775807;
- */
- p += (long long)100;
- unsigned int q = (unsigned int)p;
- /*@ assert Eva: signed_downcast: -2147483648 ≤ p; */
- /*@ assert Eva: signed_downcast: p ≤ 2147483647; */
- int r = (int)p;
- return;
-}
-
-/*@ assigns \result;
- assigns \result \from \nothing; */
-extern int ( /* missing proto */ Frama_C_show_each)();
-
-void main5_wrap_signed(void)
-{
- int x_0 = v;
- /*@ assert ASSUME: x_0 ≥ 100000; */ ;
- /*@ assert x_0 > 0x7FFFFFFF - 145 ∨ x_0 ≤ 0x7FFFFFFF - 145; */ ;
- unsigned int y = (unsigned int)x_0;
- y += (unsigned int)145;
- /*@ assert Eva: signed_downcast: y ≤ 2147483647; */
- int z = (int)y;
- Frama_C_show_each(x_0,y,z);
- /*@ assert z ≥ 100000 + 145 ∨ z ≤ (int)(0x7FFFFFFF + 145); */ ;
- return;
-}
-
-void main6_val_warn_converted_signed(void)
-{
- if (v) {
- /*@ assert Eva: signed_downcast: 65300u ≤ 32767; */
- short s_0 = (short)65300u;
- }
- if (v) {
- unsigned short u = (unsigned short)65300u;
- }
- if (v) {
- unsigned long e = (unsigned long)17;
- short b = (short)e;
- }
- if (v) {
- unsigned long e_0 = (unsigned long)(-12);
- /*@ assert Eva: signed_downcast: e_0 ≤ 32767; */
- short b_0 = (short)e_0;
- }
- if (v) {
- unsigned int e_1 = (unsigned int)(-64000);
- /*@ assert Eva: signed_downcast: e_1 ≤ 32767; */
- short b_1 = (short)e_1;
- }
- if (v) {
- int *p = (int *)(& v);
- /*@ assert Eva: signed_downcast: p ≤ 2147483647; */
- int x_0 = (int)p;
- /*@ assert Eva: signed_downcast: p ≤ 32767; */
- short y = (short)p;
- unsigned short z = (unsigned short)p;
- }
- return;
-}
-
-void main7_signed_upcast(void)
-{
- unsigned char c = (unsigned char)240;
- int i = (int)c;
- return;
-}
-
-void main8_bitfields(void)
-{
- struct bitf S;
- signed char c;
- S.i1 = (unsigned int)0x3FFFF;
- if (v)
- /*@ assert Eva: signed_downcast: S.i1 ≤ 31; */
- S.i2 = (int)S.i1;
- if (v)
- /*@ assert Eva: signed_downcast: S.i1 ≤ 127; */
- c = (signed char)S.i1;
- S.i1 = (unsigned int)257u;
- if (v)
- /*@ assert Eva: signed_downcast: S.i1 ≤ 31; */
- S.i2 = (int)S.i1;
- if (v)
- /*@ assert Eva: signed_downcast: S.i1 ≤ 127; */
- c = (signed char)S.i1;
- S.i1 = (unsigned int)65u;
- if (v)
- /*@ assert Eva: signed_downcast: S.i1 ≤ 31; */
- S.i2 = (int)S.i1;
- if (v) c = (signed char)S.i1;
- return;
-}
-
-void main9_bitfield(void)
-{
- struct __anonstruct_bf_1 bf;
- signed char c;
- bf.a = (unsigned int)1648;
- if (v) {
- /*@ assert Eva: signed_downcast: bf.a ≤ 1023; */
- int signed_a = (int)((int)bf.a);
- /*@ assert signed_a ≡ -400; */ ;
- }
- if (v)
- /*@ assert Eva: signed_downcast: bf.a ≤ 127; */
- c = (signed char)bf.a;
- return;
-}
-
-void main10_loop(void)
-{
- signed char c;
- struct __anonstruct_bf_2 bf;
- int k = 0;
- while (k < 10) {
- bf.b = (unsigned int)v;
- if (v)
- /*@ assert Eva: signed_downcast: bf.b ≤ 127; */
- c = (signed char)bf.b;
- k ++;
- }
- return;
-}
-
-void main(void)
-{
- main1();
- main2_bitfield();
- main3_reduction();
- main4_pointer();
- main5_wrap_signed();
- main6_val_warn_converted_signed();
- main7_signed_upcast();
- main8_bitfields();
- main9_bitfield();
- main10_loop();
- return;
-}
-
-
-[eva] Analyzing an incomplete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- sx ∈ [--..--]
- sy ∈ [--..--]
- sz ∈ [--..--]
- uc ∈ [--..--]
- x ∈ [--..--]
- ux ∈ [--..--]
- uy ∈ [--..--]
- uz ∈ [--..--]
- s ∈ [--..--]
- v ∈ [--..--]
-[eva] computing for function main1 <- main.
- Called from tests/value/downcast.i:152.
-[eva:alarm] tests/value/downcast.i:20: Warning:
- unsigned downcast. assert 0 ≤ (int)((int)sx + (int)sy);
-[eva:alarm] tests/value/downcast.i:21: Warning:
- unsigned downcast. assert 0 ≤ x;
-[eva:alarm] tests/value/downcast.i:21: Warning:
- unsigned downcast. assert x ≤ 255;
-[eva:alarm] tests/value/downcast.i:24: Warning:
- unsigned downcast. assert (unsigned int)(uy + uz) ≤ 65535;
-[eva] Recording results for main1
-[eva] Done for function main1
-[eva] computing for function main2_bitfield <- main.
- Called from tests/value/downcast.i:153.
-[eva:alarm] tests/value/downcast.i:33: Warning:
- unsigned downcast. assert j ≤ 31;
-[eva] Recording results for main2_bitfield
-[eva] Done for function main2_bitfield
-[eva] computing for function main3_reduction <- main.
- Called from tests/value/downcast.i:154.
-[eva:alarm] tests/value/downcast.i:40: Warning:
- unsigned downcast. assert 0 ≤ v;
-[eva:alarm] tests/value/downcast.i:41: Warning:
- unsigned downcast. assert y ≤ 255;
-[eva] Recording results for main3_reduction
-[eva] Done for function main3_reduction
-[eva] computing for function main4_pointer <- main.
- Called from tests/value/downcast.i:155.
-[eva:alarm] tests/value/downcast.i:50: Warning:
- signed overflow. assert -9223372036854775808 ≤ p + (long long)100;
-[eva:alarm] tests/value/downcast.i:50: Warning:
- signed overflow. assert p + (long long)100 ≤ 9223372036854775807;
-[eva:alarm] tests/value/downcast.i:51: Warning:
- unsigned downcast. assert 0 ≤ p;
-[eva:alarm] tests/value/downcast.i:51: Warning:
- unsigned downcast. assert p ≤ 4294967295;
-[eva] Recording results for main4_pointer
-[eva] Done for function main4_pointer
-[eva] computing for function main5_wrap_signed <- main.
- Called from tests/value/downcast.i:156.
-[eva] tests/value/downcast.i:63:
- Frama_C_show_each:
- [100000..2147483647], [100145..2147483792], [-2147483648..2147483647]
-[eva:alarm] tests/value/downcast.i:64: Warning: assertion got status unknown.
-[eva] Recording results for main5_wrap_signed
-[eva] Done for function main5_wrap_signed
-[eva] computing for function main6_val_warn_converted_signed <- main.
- Called from tests/value/downcast.i:157.
-[eva:alarm] tests/value/downcast.i:81: Warning:
- unsigned downcast. assert 0 ≤ (int)(-12);
-[eva:alarm] tests/value/downcast.i:86: Warning:
- unsigned downcast. assert 0 ≤ (int)(-64000);
-[eva] tests/value/downcast.i:92:
- Assigning imprecise value to y.
- The imprecision originates from Arithmetic {tests/value/downcast.i:92}
-[eva:alarm] tests/value/downcast.i:93: Warning:
- unsigned downcast. assert p ≤ 65535;
-[eva] Recording results for main6_val_warn_converted_signed
-[eva] Done for function main6_val_warn_converted_signed
-[eva] computing for function main7_signed_upcast <- main.
- Called from tests/value/downcast.i:158.
-[eva] Recording results for main7_signed_upcast
-[eva] Done for function main7_signed_upcast
-[eva] computing for function main8_bitfields <- main.
- Called from tests/value/downcast.i:159.
-[eva] Recording results for main8_bitfields
-[eva] Done for function main8_bitfields
-[eva] computing for function main9_bitfield <- main.
- Called from tests/value/downcast.i:160.
-[eva] tests/value/downcast.i:134: assertion got status valid.
-[eva] Recording results for main9_bitfield
-[eva] Done for function main9_bitfield
-[eva] computing for function main10_loop <- main.
- Called from tests/value/downcast.i:161.
-[eva:alarm] tests/value/downcast.i:146: Warning:
- unsigned downcast. assert 0 ≤ v;
-[eva:alarm] tests/value/downcast.i:146: Warning:
- unsigned downcast. assert v ≤ 1023;
-[eva] Recording results for main10_loop
-[eva] Done for function main10_loop
-[eva] Recording results for main
-[eva] done for function main
-[eva] tests/value/downcast.i:33:
- assertion 'Eva,unsigned_downcast' got final status invalid.
-[eva] tests/value/downcast.i:81:
- assertion 'Eva,unsigned_downcast' got final status invalid.
-[eva] tests/value/downcast.i:86:
- assertion 'Eva,unsigned_downcast' got final status invalid.
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function main1:
- sz ∈ [--..--]
- uc ∈ [--..--]
- x ∈ [--..--]
- ux ∈ [--..--]
- s ∈ [--..--]
-[eva:final-states] Values at end of function main10_loop:
- c ∈ [--..--] or UNINITIALIZED
- bf.b ∈ [--..--] or UNINITIALIZED
- .[bits 10 to 31] ∈ UNINITIALIZED
- k ∈ {10}
-[eva:final-states] Values at end of function main2_bitfield:
- i ∈ {117}
- j ∈ {254}
- ss.i ∈ {-11} or UNINITIALIZED
- {.j; .[bits 10 to 31]} ∈ UNINITIALIZED
-[eva:final-states] Values at end of function main3_reduction:
- x_0 ∈ [--..--]
- c ∈ [--..--]
- y ∈ [0..255]
- d ∈ [--..--]
-[eva:final-states] Values at end of function main4_pointer:
- p ∈ {{ &x_0 + {100} }}
- q ∈ {{ &x_0 + {100} }}
- r ∈ {{ &x_0 + {100} }}
-[eva:final-states] Values at end of function main5_wrap_signed:
- x_0 ∈ [100000..2147483647]
- y ∈ [100145..2147483792]
- z ∈ [--..--]
-[eva:final-states] Values at end of function main6_val_warn_converted_signed:
-
-[eva:final-states] Values at end of function main7_signed_upcast:
- c ∈ {240}
- i ∈ {240}
-[eva:final-states] Values at end of function main8_bitfields:
- S.i1 ∈ {65}
- .i2 ∈ {-1; 1} or UNINITIALIZED
- .[bits 24 to 31] ∈ UNINITIALIZED
- c ∈ {-1; 1; 65} or UNINITIALIZED
-[eva:final-states] Values at end of function main9_bitfield:
- bf.a ∈ {1648}
- .[bits 11 to 31] ∈ UNINITIALIZED
- c ∈ {112} or UNINITIALIZED
-[eva:final-states] Values at end of function main:
- sz ∈ [--..--]
- uc ∈ [--..--]
- x ∈ [--..--]
- ux ∈ [--..--]
- s ∈ [--..--]
-[from] Computing for function main1
-[from] Done for function main1
-[from] Computing for function main10_loop
-[from] Done for function main10_loop
-[from] Computing for function main2_bitfield
-[from] Done for function main2_bitfield
-[from] Computing for function main3_reduction
-[from] Done for function main3_reduction
-[from] Computing for function main4_pointer
-[from] Done for function main4_pointer
-[from] Computing for function main5_wrap_signed
-[from] Done for function main5_wrap_signed
-[from] Computing for function main6_val_warn_converted_signed
-[from] Done for function main6_val_warn_converted_signed
-[from] Computing for function main7_signed_upcast
-[from] Done for function main7_signed_upcast
-[from] Computing for function main8_bitfields
-[from] Done for function main8_bitfields
-[from] Computing for function main9_bitfield
-[from] Done for function main9_bitfield
-[from] Computing for function main
-[from] Done for function main
-[from] ====== DEPENDENCIES COMPUTED ======
- These dependencies hold at termination for the executions that terminate:
-[from] Function main1:
- sz FROM sx; sy
- uc FROM x
- x FROM uy; uz
- ux FROM uy; uz
- s FROM uy; uz
-[from] Function main10_loop:
- NO EFFECTS
-[from] Function main2_bitfield:
- NO EFFECTS
-[from] Function main3_reduction:
- NO EFFECTS
-[from] Function main4_pointer:
- NO EFFECTS
-[from] Function main5_wrap_signed:
- NO EFFECTS
-[from] Function main6_val_warn_converted_signed:
- NO EFFECTS
-[from] Function main7_signed_upcast:
- NO EFFECTS
-[from] Function main8_bitfields:
- NO EFFECTS
-[from] Function main9_bitfield:
- NO EFFECTS
-[from] Function main:
- sz FROM sx; sy
- uc FROM x
- x FROM uy; uz
- ux FROM uy; uz
- s FROM uy; uz
-[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function main1:
- sz; uc; x; ux; s
-[inout] Inputs for function main1:
- sx; sy; x; uy; uz
-[inout] Out (internal) for function main10_loop:
- c; bf.b; k
-[inout] Inputs for function main10_loop:
- v
-[inout] Out (internal) for function main2_bitfield:
- i; j; ss{.i; .j}
-[inout] Inputs for function main2_bitfield:
- v
-[inout] Out (internal) for function main3_reduction:
- x_0; c; y; d
-[inout] Inputs for function main3_reduction:
- v
-[inout] Out (internal) for function main4_pointer:
- p; q; r
-[inout] Inputs for function main4_pointer:
- \nothing
-[inout] Out (internal) for function main5_wrap_signed:
- x_0; y; z
-[inout] Inputs for function main5_wrap_signed:
- v
-[inout] Out (internal) for function main6_val_warn_converted_signed:
- s_0; u; e; b; e_0; e_1; p; x_0; y; z
-[inout] Inputs for function main6_val_warn_converted_signed:
- v
-[inout] Out (internal) for function main7_signed_upcast:
- c; i
-[inout] Inputs for function main7_signed_upcast:
- \nothing
-[inout] Out (internal) for function main8_bitfields:
- S{.i1; .i2}; c
-[inout] Inputs for function main8_bitfields:
- v
-[inout] Out (internal) for function main9_bitfield:
- bf.a; signed_a; c
-[inout] Inputs for function main9_bitfield:
- v
-[inout] Out (internal) for function main:
- sz; uc; x; ux; s
-[inout] Inputs for function main:
- sx; sy; x; uy; uz; v
-[report] Computing properties status...
-
---------------------------------------------------------------------------------
---- Properties of Function 'main1'
---------------------------------------------------------------------------------
-
-[ - ] Assertion 'Eva,unsigned_downcast' (file tests/value/downcast.i, line 20)
- tried with Eva.
-[ - ] Assertion 'Eva,unsigned_downcast' (file tests/value/downcast.i, line 21)
- tried with Eva.
-[ - ] Assertion 'Eva,unsigned_downcast' (file tests/value/downcast.i, line 21)
- tried with Eva.
-[ - ] Assertion 'Eva,unsigned_downcast' (file tests/value/downcast.i, line 24)
- tried with Eva.
-
---------------------------------------------------------------------------------
---- Properties of Function 'main2_bitfield'
---------------------------------------------------------------------------------
-
-[ Alarm ] Assertion 'Eva,unsigned_downcast' (file tests/value/downcast.i, line 33)
- By Eva, with pending:
- - Unreachable instruction (file tests/value/downcast.i, line 33)
-
---------------------------------------------------------------------------------
---- Properties of Function 'main3_reduction'
---------------------------------------------------------------------------------
-
-[ - ] Assertion 'Eva,unsigned_downcast' (file tests/value/downcast.i, line 40)
- tried with Eva.
-[ - ] Assertion 'Eva,unsigned_downcast' (file tests/value/downcast.i, line 41)
- tried with Eva.
-
---------------------------------------------------------------------------------
---- Properties of Function 'main4_pointer'
---------------------------------------------------------------------------------
-
-[ - ] Assertion 'Eva,signed_overflow' (file tests/value/downcast.i, line 50)
- tried with Eva.
-[ - ] Assertion 'Eva,signed_overflow' (file tests/value/downcast.i, line 50)
- tried with Eva.
-[ - ] Assertion 'Eva,unsigned_downcast' (file tests/value/downcast.i, line 51)
- tried with Eva.
-[ - ] Assertion 'Eva,unsigned_downcast' (file tests/value/downcast.i, line 51)
- tried with Eva.
-
---------------------------------------------------------------------------------
---- Properties of Function 'main5_wrap_signed'
---------------------------------------------------------------------------------
-
-[ - ] Assertion 'ASSUME' (file tests/value/downcast.i, line 58)
- tried with Eva.
-[ Valid ] Assertion (file tests/value/downcast.i, line 59)
- by Eva.
-[ - ] Assertion (file tests/value/downcast.i, line 64)
- tried with Eva.
-
---------------------------------------------------------------------------------
---- Properties of Function 'main6_val_warn_converted_signed'
---------------------------------------------------------------------------------
-
-[ Alarm ] Assertion 'Eva,unsigned_downcast' (file tests/value/downcast.i, line 81)
- By Eva, with pending:
- - Unreachable initialization of 'e_0' (file tests/value/downcast.i, line 81)
-[ Alarm ] Assertion 'Eva,unsigned_downcast' (file tests/value/downcast.i, line 86)
- By Eva, with pending:
- - Unreachable initialization of 'e_1' (file tests/value/downcast.i, line 86)
-[ - ] Assertion 'Eva,unsigned_downcast' (file tests/value/downcast.i, line 93)
- tried with Eva.
-
---------------------------------------------------------------------------------
---- Properties of Function 'main9_bitfield'
---------------------------------------------------------------------------------
-
-[ Valid ] Assertion (file tests/value/downcast.i, line 134)
- by Eva.
-
---------------------------------------------------------------------------------
---- Properties of Function 'main10_loop'
---------------------------------------------------------------------------------
-
-[ - ] Assertion 'Eva,unsigned_downcast' (file tests/value/downcast.i, line 146)
- tried with Eva.
-[ - ] Assertion 'Eva,unsigned_downcast' (file tests/value/downcast.i, line 146)
- tried with Eva.
-
---------------------------------------------------------------------------------
---- Status Report Summary
---------------------------------------------------------------------------------
- 2 Completely validated
- 15 To be validated
- 3 Alarms emitted
- 20 Total
---------------------------------------------------------------------------------
-/* Generated by Frama-C */
-struct s {
- int i : 5 ;
- unsigned int j : 5 ;
-};
-struct bitf {
- unsigned int i1 : 18 ;
- int i2 : 6 ;
-};
-struct __anonstruct_bf_1 {
- unsigned int a : 11 ;
-};
-struct __anonstruct_bf_2 {
- unsigned int b : 10 ;
-};
-signed char sx;
-signed char sy;
-signed char sz;
-unsigned char uc;
-int x;
-unsigned int ux;
-unsigned int uy;
-unsigned int uz;
-unsigned short s;
-int volatile v;
-void main1(void)
-{
- sz = (signed char)((int)sx + (int)sy);
- /*@ assert Eva: unsigned_downcast: 0 ≤ (int)((int)sx + (int)sy); */
- uc = (unsigned char)((int)sx + (int)sy);
- /*@ assert Eva: unsigned_downcast: 0 ≤ x; */
- /*@ assert Eva: unsigned_downcast: x ≤ 255; */
- uc = (unsigned char)x;
- x = (int)(uy + uz);
- ux = uy + uz;
- /*@ assert Eva: unsigned_downcast: (unsigned int)(uy + uz) ≤ 65535; */
- s = (unsigned short)(uy + uz);
- return;
-}
-
-void main2_bitfield(void)
-{
- struct s ss;
- int i = 117;
- unsigned int j = (unsigned int)254;
- if (v)
- ss.i = (int)i;
- if (v)
- /*@ assert Eva: unsigned_downcast: j ≤ 31; */
- ss.j = (unsigned int)j;
- return;
-}
-
-void main3_reduction(void)
-{
- int x_0 = v;
- char c = (char)x_0;
- /*@ assert Eva: unsigned_downcast: 0 ≤ v; */
- unsigned int y = (unsigned int)v;
- /*@ assert Eva: unsigned_downcast: y ≤ 255; */
- unsigned char d = (unsigned char)y;
- return;
-}
-
-void main4_pointer(void)
-{
- int x_0;
- long long p = (long long)(& x_0);
- /*@ assert
- Eva: signed_overflow: -9223372036854775808 ≤ p + (long long)100;
- */
- /*@ assert
- Eva: signed_overflow: p + (long long)100 ≤ 9223372036854775807;
- */
- p += (long long)100;
- /*@ assert Eva: unsigned_downcast: 0 ≤ p; */
- /*@ assert Eva: unsigned_downcast: p ≤ 4294967295; */
- unsigned int q = (unsigned int)p;
- int r = (int)p;
- return;
-}
-
-/*@ assigns \result;
- assigns \result \from \nothing; */
-extern int ( /* missing proto */ Frama_C_show_each)();
-
-void main5_wrap_signed(void)
-{
- int x_0 = v;
- /*@ assert ASSUME: x_0 ≥ 100000; */ ;
- /*@ assert x_0 > 0x7FFFFFFF - 145 ∨ x_0 ≤ 0x7FFFFFFF - 145; */ ;
- unsigned int y = (unsigned int)x_0;
- y += (unsigned int)145;
- int z = (int)y;
- Frama_C_show_each(x_0,y,z);
- /*@ assert z ≥ 100000 + 145 ∨ z ≤ (int)(0x7FFFFFFF + 145); */ ;
- return;
-}
-
-void main6_val_warn_converted_signed(void)
-{
- if (v) {
- short s_0 = (short)65300u;
- }
- if (v) {
- unsigned short u = (unsigned short)65300u;
- }
- if (v) {
- unsigned long e = (unsigned long)17;
- short b = (short)e;
- }
- if (v) {
- /*@ assert Eva: unsigned_downcast: 0 ≤ (int)(-12); */
- unsigned long e_0 = (unsigned long)(-12);
- short b_0 = (short)e_0;
- }
- if (v) {
- /*@ assert Eva: unsigned_downcast: 0 ≤ (int)(-64000); */
- unsigned int e_1 = (unsigned int)(-64000);
- short b_1 = (short)e_1;
- }
- if (v) {
- int *p = (int *)(& v);
- int x_0 = (int)p;
- short y = (short)p;
- /*@ assert Eva: unsigned_downcast: p ≤ 65535; */
- unsigned short z = (unsigned short)p;
- }
- return;
-}
-
-void main7_signed_upcast(void)
-{
- unsigned char c = (unsigned char)240;
- int i = (int)c;
- return;
-}
-
-void main8_bitfields(void)
-{
- struct bitf S;
- signed char c;
- S.i1 = (unsigned int)0x3FFFF;
- if (v)
- S.i2 = (int)S.i1;
- if (v)
- c = (signed char)S.i1;
- S.i1 = (unsigned int)257u;
- if (v)
- S.i2 = (int)S.i1;
- if (v)
- c = (signed char)S.i1;
- S.i1 = (unsigned int)65u;
- if (v)
- S.i2 = (int)S.i1;
- if (v) c = (signed char)S.i1;
- return;
-}
-
-void main9_bitfield(void)
-{
- struct __anonstruct_bf_1 bf;
- signed char c;
- bf.a = (unsigned int)1648;
- if (v) {
- int signed_a = (int)((int)bf.a);
- /*@ assert signed_a ≡ -400; */ ;
- }
- if (v)
- c = (signed char)bf.a;
- return;
-}
-
-void main10_loop(void)
-{
- signed char c;
- struct __anonstruct_bf_2 bf;
- int k = 0;
- while (k < 10) {
- /*@ assert Eva: unsigned_downcast: 0 ≤ v; */
- /*@ assert Eva: unsigned_downcast: v ≤ 1023; */
- bf.b = (unsigned int)v;
- if (v)
- c = (signed char)bf.b;
- k ++;
- }
- return;
-}
-
-void main(void)
-{
- main1();
- main2_bitfield();
- main3_reduction();
- main4_pointer();
- main5_wrap_signed();
- main6_val_warn_converted_signed();
- main7_signed_upcast();
- main8_bitfields();
- main9_bitfield();
- main10_loop();
- return;
-}
-
-
-[eva] Analyzing an incomplete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- sx ∈ [--..--]
- sy ∈ [--..--]
- sz ∈ [--..--]
- uc ∈ [--..--]
- x ∈ [--..--]
- ux ∈ [--..--]
- uy ∈ [--..--]
- uz ∈ [--..--]
- s ∈ [--..--]
- v ∈ [--..--]
-[eva] computing for function main1 <- main.
- Called from tests/value/downcast.i:152.
-[eva:alarm] tests/value/downcast.i:19: Warning:
- signed downcast. assert -128 ≤ (int)((int)sx + (int)sy);
-[eva:alarm] tests/value/downcast.i:19: Warning:
- signed downcast. assert (int)((int)sx + (int)sy) ≤ 127;
-[eva] Recording results for main1
-[eva] Done for function main1
-[eva] computing for function main2_bitfield <- main.
- Called from tests/value/downcast.i:153.
-[eva:alarm] tests/value/downcast.i:32: Warning:
- signed downcast. assert i ≤ 15;
-[eva] Recording results for main2_bitfield
-[eva] Done for function main2_bitfield
-[eva] computing for function main3_reduction <- main.
- Called from tests/value/downcast.i:154.
-[eva:alarm] tests/value/downcast.i:38: Warning:
- signed downcast. assert -128 ≤ x_0;
-[eva:alarm] tests/value/downcast.i:38: Warning:
- signed downcast. assert x_0 ≤ 127;
-[eva] Recording results for main3_reduction
-[eva] Done for function main3_reduction
-[eva] computing for function main4_pointer <- main.
- Called from tests/value/downcast.i:155.
-[eva:alarm] tests/value/downcast.i:50: Warning:
- signed overflow. assert -9223372036854775808 ≤ p + (long long)100;
-[eva:alarm] tests/value/downcast.i:50: Warning:
- signed overflow. assert p + (long long)100 ≤ 9223372036854775807;
-[eva:alarm] tests/value/downcast.i:52: Warning:
- signed downcast. assert -2147483648 ≤ p;
-[eva:alarm] tests/value/downcast.i:52: Warning:
- signed downcast. assert p ≤ 2147483647;
-[eva] Recording results for main4_pointer
-[eva] Done for function main4_pointer
-[eva] computing for function main5_wrap_signed <- main.
- Called from tests/value/downcast.i:156.
-[eva] tests/value/downcast.i:63:
- Frama_C_show_each:
- [100000..2147483647], [100145..2147483792], [-2147483648..2147483647]
-[eva] Recording results for main5_wrap_signed
-[eva] Done for function main5_wrap_signed
-[eva] computing for function main6_val_warn_converted_signed <- main.
- Called from tests/value/downcast.i:157.
-[eva:alarm] tests/value/downcast.i:71: Warning:
- signed downcast. assert (int)65300u ≤ 32767;
-[eva:alarm] tests/value/downcast.i:87: Warning:
- signed downcast. assert -32768 ≤ (int)e_1;
-[eva:alarm] tests/value/downcast.i:92: Warning:
- signed downcast. assert -32768 ≤ (int)p;
-[eva:alarm] tests/value/downcast.i:92: Warning:
- signed downcast. assert (int)p ≤ 32767;
-[eva] Recording results for main6_val_warn_converted_signed
-[eva] Done for function main6_val_warn_converted_signed
-[eva] computing for function main7_signed_upcast <- main.
- Called from tests/value/downcast.i:158.
-[eva] Recording results for main7_signed_upcast
-[eva] Done for function main7_signed_upcast
-[eva] computing for function main8_bitfields <- main.
- Called from tests/value/downcast.i:159.
-[eva:alarm] tests/value/downcast.i:119: Warning:
- signed downcast. assert (int)S.i1 ≤ 31;
-[eva:alarm] tests/value/downcast.i:120: Warning:
- signed downcast. assert (int)S.i1 ≤ 127;
-[eva:alarm] tests/value/downcast.i:124: Warning:
- signed downcast. assert (int)S.i1 ≤ 31;
-[eva] Recording results for main8_bitfields
-[eva] Done for function main8_bitfields
-[eva] computing for function main9_bitfield <- main.
- Called from tests/value/downcast.i:160.
-[eva:alarm] tests/value/downcast.i:137: Warning:
- signed downcast. assert -128 ≤ (int)bf.a;
-[eva] Recording results for main9_bitfield
-[eva] Done for function main9_bitfield
-[eva] computing for function main10_loop <- main.
- Called from tests/value/downcast.i:161.
-[eva:alarm] tests/value/downcast.i:147: Warning:
- signed downcast. assert -128 ≤ (int)bf.b;
-[eva:alarm] tests/value/downcast.i:147: Warning:
- signed downcast. assert (int)bf.b ≤ 127;
-[eva] Recording results for main10_loop
-[eva] Done for function main10_loop
-[eva] Recording results for main
-[eva] done for function main
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function main1:
- sz ∈ [--..--]
- uc ∈ [--..--]
- x ∈ [--..--]
- ux ∈ [--..--]
- s ∈ [--..--]
-[eva:final-states] Values at end of function main10_loop:
- c ∈ [--..--] or UNINITIALIZED
- bf.b ∈ [--..--] or UNINITIALIZED
- .[bits 10 to 31] ∈ UNINITIALIZED
- k ∈ {10}
-[eva:final-states] Values at end of function main2_bitfield:
- i ∈ {117}
- j ∈ {254}
- ss.i ∈ UNINITIALIZED
- .j ∈ {30} or UNINITIALIZED
- .[bits 10 to 31] ∈ UNINITIALIZED
-[eva:final-states] Values at end of function main3_reduction:
- x_0 ∈ [-128..127]
- c ∈ [--..--]
- y ∈ [--..--]
- d ∈ [--..--]
-[eva:final-states] Values at end of function main4_pointer:
- p ∈ {{ &x_0 + {100} }}
- q ∈ {{ &x_0 + {100} }}
- r ∈ {{ &x_0 + {100} }}
-[eva:final-states] Values at end of function main5_wrap_signed:
- x_0 ∈ [100000..2147483647]
- y ∈ [100145..2147483792]
- z ∈ [--..--]
-[eva:final-states] Values at end of function main6_val_warn_converted_signed:
-
-[eva:final-states] Values at end of function main7_signed_upcast:
- c ∈ {240}
- i ∈ {240}
-[eva:final-states] Values at end of function main8_bitfields:
- S.i1 ∈ {65}
- .i2 ∈ {-1} or UNINITIALIZED
- .[bits 24 to 31] ∈ UNINITIALIZED
- c ∈ {-1; 65} or UNINITIALIZED
-[eva:final-states] Values at end of function main9_bitfield:
- bf.a ∈ {1648}
- .[bits 11 to 31] ∈ UNINITIALIZED
- c ∈ UNINITIALIZED
-[eva:final-states] Values at end of function main:
- sz ∈ [--..--]
- uc ∈ [--..--]
- x ∈ [--..--]
- ux ∈ [--..--]
- s ∈ [--..--]
-[from] Computing for function main1
-[from] Done for function main1
-[from] Computing for function main10_loop
-[from] Done for function main10_loop
-[from] Computing for function main2_bitfield
-[from] Done for function main2_bitfield
-[from] Computing for function main3_reduction
-[from] Done for function main3_reduction
-[from] Computing for function main4_pointer
-[from] Done for function main4_pointer
-[from] Computing for function main5_wrap_signed
-[from] Done for function main5_wrap_signed
-[from] Computing for function main6_val_warn_converted_signed
-[from] Done for function main6_val_warn_converted_signed
-[from] Computing for function main7_signed_upcast
-[from] Done for function main7_signed_upcast
-[from] Computing for function main8_bitfields
-[from] Done for function main8_bitfields
-[from] Computing for function main9_bitfield
-[from] Done for function main9_bitfield
-[from] Computing for function main
-[from] Done for function main
-[from] ====== DEPENDENCIES COMPUTED ======
- These dependencies hold at termination for the executions that terminate:
-[from] Function main1:
- sz FROM sx; sy
- uc FROM x
- x FROM uy; uz
- ux FROM uy; uz
- s FROM uy; uz
-[from] Function main10_loop:
- NO EFFECTS
-[from] Function main2_bitfield:
- NO EFFECTS
-[from] Function main3_reduction:
- NO EFFECTS
-[from] Function main4_pointer:
- NO EFFECTS
-[from] Function main5_wrap_signed:
- NO EFFECTS
-[from] Function main6_val_warn_converted_signed:
- NO EFFECTS
-[from] Function main7_signed_upcast:
- NO EFFECTS
-[from] Function main8_bitfields:
- NO EFFECTS
-[from] Function main9_bitfield:
- NO EFFECTS
-[from] Function main:
- sz FROM sx; sy
- uc FROM x
- x FROM uy; uz
- ux FROM uy; uz
- s FROM uy; uz
-[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function main1:
- sz; uc; x; ux; s
-[inout] Inputs for function main1:
- sx; sy; x; uy; uz
-[inout] Out (internal) for function main10_loop:
- c; bf.b; k
-[inout] Inputs for function main10_loop:
- v
-[inout] Out (internal) for function main2_bitfield:
- i; j; ss{.i; .j}
-[inout] Inputs for function main2_bitfield:
- v
-[inout] Out (internal) for function main3_reduction:
- x_0; c; y; d
-[inout] Inputs for function main3_reduction:
- v
-[inout] Out (internal) for function main4_pointer:
- p; q; r
-[inout] Inputs for function main4_pointer:
- \nothing
-[inout] Out (internal) for function main5_wrap_signed:
- x_0; y; z
-[inout] Inputs for function main5_wrap_signed:
- v
-[inout] Out (internal) for function main6_val_warn_converted_signed:
- s_0; u; e; b; e_0; b_0; e_1; b_1; p; x_0; y; z
-[inout] Inputs for function main6_val_warn_converted_signed:
- v
-[inout] Out (internal) for function main7_signed_upcast:
- c; i
-[inout] Inputs for function main7_signed_upcast:
- \nothing
-[inout] Out (internal) for function main8_bitfields:
- S{.i1; .i2}; c
-[inout] Inputs for function main8_bitfields:
- v
-[inout] Out (internal) for function main9_bitfield:
- bf.a; signed_a; c
-[inout] Inputs for function main9_bitfield:
- v
-[inout] Out (internal) for function main:
- sz; uc; x; ux; s
-[inout] Inputs for function main:
- sx; sy; x; uy; uz; v
-[report] Computing properties status...
-
---------------------------------------------------------------------------------
---- Properties of Function 'main1'
---------------------------------------------------------------------------------
-
-[ - ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 19)
- tried with Eva.
-[ - ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 19)
- tried with Eva.
-
---------------------------------------------------------------------------------
---- Properties of Function 'main2_bitfield'
---------------------------------------------------------------------------------
-
-[ Alarm ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 32)
- By Eva, with pending:
- - Unreachable instruction (file tests/value/downcast.i, line 32)
-
---------------------------------------------------------------------------------
---- Properties of Function 'main3_reduction'
---------------------------------------------------------------------------------
-
-[ - ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 38)
- tried with Eva.
-[ - ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 38)
- tried with Eva.
-
---------------------------------------------------------------------------------
---- Properties of Function 'main4_pointer'
---------------------------------------------------------------------------------
-
-[ - ] Assertion 'Eva,signed_overflow' (file tests/value/downcast.i, line 50)
- tried with Eva.
-[ - ] Assertion 'Eva,signed_overflow' (file tests/value/downcast.i, line 50)
- tried with Eva.
-[ - ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 52)
- tried with Eva.
-[ - ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 52)
- tried with Eva.
-
---------------------------------------------------------------------------------
---- Properties of Function 'main5_wrap_signed'
---------------------------------------------------------------------------------
-
-[ - ] Assertion 'ASSUME' (file tests/value/downcast.i, line 58)
- tried with Eva.
-[ Valid ] Assertion (file tests/value/downcast.i, line 59)
- by Eva.
-[ - ] Assertion (file tests/value/downcast.i, line 64)
- tried with Eva.
-
---------------------------------------------------------------------------------
---- Properties of Function 'main6_val_warn_converted_signed'
---------------------------------------------------------------------------------
-
-[ Alarm ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 71)
- By Eva, with pending:
- - Unreachable initialization of 's_0' (file tests/value/downcast.i, line 71)
-[ Alarm ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 87)
- By Eva, with pending:
- - Unreachable initialization of 'b_1' (file tests/value/downcast.i, line 87)
-[ - ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 92)
- tried with Eva.
-[ - ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 92)
- tried with Eva.
-
---------------------------------------------------------------------------------
---- Properties of Function 'main8_bitfields'
---------------------------------------------------------------------------------
-
-[ Alarm ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 119)
- By Eva, with pending:
- - Unreachable instruction (file tests/value/downcast.i, line 119)
-[ Alarm ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 120)
- By Eva, with pending:
- - Unreachable instruction (file tests/value/downcast.i, line 120)
-[ Alarm ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 124)
- By Eva, with pending:
- - Unreachable instruction (file tests/value/downcast.i, line 124)
-
---------------------------------------------------------------------------------
---- Properties of Function 'main9_bitfield'
---------------------------------------------------------------------------------
-
-[ Valid ] Assertion (file tests/value/downcast.i, line 134)
- by Eva.
-[ Alarm ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 137)
- By Eva, with pending:
- - Unreachable instruction (file tests/value/downcast.i, line 137)
-
---------------------------------------------------------------------------------
---- Properties of Function 'main10_loop'
---------------------------------------------------------------------------------
-
-[ - ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 147)
- tried with Eva.
-[ - ] Assertion 'Eva,signed_downcast' (file tests/value/downcast.i, line 147)
- tried with Eva.
-
---------------------------------------------------------------------------------
---- Status Report Summary
---------------------------------------------------------------------------------
- 2 Completely validated
- 14 To be validated
- 7 Alarms emitted
- 23 Total
---------------------------------------------------------------------------------
-/* Generated by Frama-C */
-struct s {
- int i : 5 ;
- unsigned int j : 5 ;
-};
-struct bitf {
- unsigned int i1 : 18 ;
- int i2 : 6 ;
-};
-struct __anonstruct_bf_1 {
- unsigned int a : 11 ;
-};
-struct __anonstruct_bf_2 {
- unsigned int b : 10 ;
-};
-signed char sx;
-signed char sy;
-signed char sz;
-unsigned char uc;
-int x;
-unsigned int ux;
-unsigned int uy;
-unsigned int uz;
-unsigned short s;
-int volatile v;
-void main1(void)
-{
- /*@ assert Eva: signed_downcast: -128 ≤ (int)((int)sx + (int)sy); */
- /*@ assert Eva: signed_downcast: (int)((int)sx + (int)sy) ≤ 127; */
- sz = (signed char)((int)sx + (int)sy);
- uc = (unsigned char)((int)sx + (int)sy);
- uc = (unsigned char)x;
- x = (int)(uy + uz);
- ux = uy + uz;
- s = (unsigned short)(uy + uz);
- return;
-}
-
-void main2_bitfield(void)
-{
- struct s ss;
- int i = 117;
- unsigned int j = (unsigned int)254;
- if (v)
- /*@ assert Eva: signed_downcast: i ≤ 15; */
- ss.i = (int)i;
- if (v)
- ss.j = (unsigned int)j;
- return;
-}
-
-void main3_reduction(void)
-{
- int x_0 = v;
- /*@ assert Eva: signed_downcast: -128 ≤ x_0; */
- /*@ assert Eva: signed_downcast: x_0 ≤ 127; */
- char c = (char)x_0;
- unsigned int y = (unsigned int)v;
- unsigned char d = (unsigned char)y;
- return;
-}
-
-void main4_pointer(void)
-{
- int x_0;
- long long p = (long long)(& x_0);
- /*@ assert
- Eva: signed_overflow: -9223372036854775808 ≤ p + (long long)100;
- */
- /*@ assert
- Eva: signed_overflow: p + (long long)100 ≤ 9223372036854775807;
- */
- p += (long long)100;
- unsigned int q = (unsigned int)p;
- /*@ assert Eva: signed_downcast: -2147483648 ≤ p; */
- /*@ assert Eva: signed_downcast: p ≤ 2147483647; */
- int r = (int)p;
- return;
-}
-
-/*@ assigns \result;
- assigns \result \from \nothing; */
-extern int ( /* missing proto */ Frama_C_show_each)();
-
-void main5_wrap_signed(void)
-{
- int x_0 = v;
- /*@ assert ASSUME: x_0 ≥ 100000; */ ;
- /*@ assert x_0 > 0x7FFFFFFF - 145 ∨ x_0 ≤ 0x7FFFFFFF - 145; */ ;
- unsigned int y = (unsigned int)x_0;
- y += (unsigned int)145;
- int z = (int)y;
- Frama_C_show_each(x_0,y,z);
- /*@ assert z ≥ 100000 + 145 ∨ z ≤ (int)(0x7FFFFFFF + 145); */ ;
- return;
-}
-
-void main6_val_warn_converted_signed(void)
-{
- if (v) {
- /*@ assert Eva: signed_downcast: (int)65300u ≤ 32767; */
- short s_0 = (short)65300u;
- }
- if (v) {
- unsigned short u = (unsigned short)65300u;
- }
- if (v) {
- unsigned long e = (unsigned long)17;
- short b = (short)e;
- }
- if (v) {
- unsigned long e_0 = (unsigned long)(-12);
- short b_0 = (short)e_0;
- }
- if (v) {
- unsigned int e_1 = (unsigned int)(-64000);
- /*@ assert Eva: signed_downcast: -32768 ≤ (int)e_1; */
- short b_1 = (short)e_1;
- }
- if (v) {
- int *p = (int *)(& v);
- int x_0 = (int)p;
- /*@ assert Eva: signed_downcast: -32768 ≤ (int)p; */
- /*@ assert Eva: signed_downcast: (int)p ≤ 32767; */
- short y = (short)p;
- unsigned short z = (unsigned short)p;
- }
- return;
-}
-
-void main7_signed_upcast(void)
-{
- unsigned char c = (unsigned char)240;
- int i = (int)c;
- return;
-}
-
-void main8_bitfields(void)
-{
- struct bitf S;
- signed char c;
- S.i1 = (unsigned int)0x3FFFF;
- if (v)
- S.i2 = (int)S.i1;
- if (v)
- c = (signed char)S.i1;
- S.i1 = (unsigned int)257u;
- if (v)
- /*@ assert Eva: signed_downcast: (int)S.i1 ≤ 31; */
- S.i2 = (int)S.i1;
- if (v)
- /*@ assert Eva: signed_downcast: (int)S.i1 ≤ 127; */
- c = (signed char)S.i1;
- S.i1 = (unsigned int)65u;
- if (v)
- /*@ assert Eva: signed_downcast: (int)S.i1 ≤ 31; */
- S.i2 = (int)S.i1;
- if (v) c = (signed char)S.i1;
- return;
-}
-
-void main9_bitfield(void)
-{
- struct __anonstruct_bf_1 bf;
- signed char c;
- bf.a = (unsigned int)1648;
- if (v) {
- int signed_a = (int)((int)bf.a);
- /*@ assert signed_a ≡ -400; */ ;
- }
- if (v)
- /*@ assert Eva: signed_downcast: -128 ≤ (int)bf.a; */
- c = (signed char)bf.a;
- return;
-}
-
-void main10_loop(void)
-{
- signed char c;
- struct __anonstruct_bf_2 bf;
- int k = 0;
- while (k < 10) {
- bf.b = (unsigned int)v;
- if (v)
- /*@ assert Eva: signed_downcast: -128 ≤ (int)bf.b; */
- /*@ assert Eva: signed_downcast: (int)bf.b ≤ 127; */
- c = (signed char)bf.b;
- k ++;
- }
- return;
-}
-
-void main(void)
-{
- main1();
- main2_bitfield();
- main3_reduction();
- main4_pointer();
- main5_wrap_signed();
- main6_val_warn_converted_signed();
- main7_signed_upcast();
- main8_bitfields();
- main9_bitfield();
- main10_loop();
- return;
-}
-
-
-[eva] Analyzing an incomplete application starting at main5_wrap_signed
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- sx ∈ [--..--]
- sy ∈ [--..--]
- sz ∈ [--..--]
- uc ∈ [--..--]
- x ∈ [--..--]
- ux ∈ [--..--]
- uy ∈ [--..--]
- uz ∈ [--..--]
- s ∈ [--..--]
- v ∈ [--..--]
-[eva] tests/value/downcast.i:63:
- Frama_C_show_each:
- [2147483503..2147483647],
- [2147483648..2147483792],
- [-2147483648..-2147483504]
-[eva] tests/value/downcast.i:63:
- Frama_C_show_each:
- [100000..2147483502], [100145..2147483647], [100145..2147483647]
-[eva] Recording results for main5_wrap_signed
-[eva] done for function main5_wrap_signed
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function main5_wrap_signed:
- x_0 ∈ [100000..2147483647]
- y ∈ [100145..2147483792]
- z ∈ [--..--]
-[from] Computing for function main5_wrap_signed
-[from] Done for function main5_wrap_signed
-[from] ====== DEPENDENCIES COMPUTED ======
- These dependencies hold at termination for the executions that terminate:
-[from] Function main5_wrap_signed:
- NO EFFECTS
-[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function main5_wrap_signed:
- x_0; y; z
-[inout] Inputs for function main5_wrap_signed:
- v
-[report] Computing properties status...
-
---------------------------------------------------------------------------------
---- Properties of Function 'main5_wrap_signed'
---------------------------------------------------------------------------------
-
-[ - ] Assertion 'ASSUME' (file tests/value/downcast.i, line 58)
- tried with Eva (v2).
-[ Valid ] Assertion (file tests/value/downcast.i, line 59)
- by Eva (v2).
-[ Valid ] Assertion (file tests/value/downcast.i, line 64)
- by Eva (v2).
-
---------------------------------------------------------------------------------
---- Properties of Function 'main9_bitfield'
---------------------------------------------------------------------------------
-
-[ Dead ] Assertion (file tests/value/downcast.i, line 134)
- Locally valid, but unreachable.
- By Eva (v2) because:
- - Unreachable program point (file tests/value/downcast.i, line 134)
-[Unreachable] Unreachable program point (file tests/value/downcast.i, line 134)
- by Eva (v2).
-
---------------------------------------------------------------------------------
---- Status Report Summary
---------------------------------------------------------------------------------
- 2 Completely validated
- 1 To be validated
- 1 Dead property
- 1 Unreachable
- 5 Total
---------------------------------------------------------------------------------
diff --git a/tests/value/oracle/eval_separated.res.oracle b/tests/value/oracle/eval_separated.res.oracle
index 0c3fea76b479bd4c8ddadcf89f365a78a7d71c30..ba49fd5aff7ed2c46847101b030c1578ba71f117 100644
--- a/tests/value/oracle/eval_separated.res.oracle
+++ b/tests/value/oracle/eval_separated.res.oracle
@@ -11,6 +11,8 @@
[eva] tests/value/eval_separated.c:6: assertion got status valid.
[eva] tests/value/eval_separated.c:8: assertion got status valid.
[eva] tests/value/eval_separated.c:9: assertion got status valid.
+[eva:alarm] tests/value/eval_separated.c:11: Warning:
+ pointer downcast. assert (unsigned int)(&q) ≤ 2147483647;
[eva:alarm] tests/value/eval_separated.c:11: Warning:
signed overflow. assert -2147483648 ≤ (int)(&q) + (int)(&q);
[eva:alarm] tests/value/eval_separated.c:11: Warning:
@@ -18,6 +20,8 @@
[eva] tests/value/eval_separated.c:11:
Assigning imprecise value to q.
The imprecision originates from Arithmetic {tests/value/eval_separated.c:11}
+[eva:alarm] tests/value/eval_separated.c:12: Warning:
+ pointer downcast. assert (unsigned int)(&r) ≤ 2147483647;
[eva:alarm] tests/value/eval_separated.c:12: Warning:
signed overflow. assert -2147483648 ≤ (int)(&r) + (int)(&r);
[eva:alarm] tests/value/eval_separated.c:12: Warning:
diff --git a/tests/value/oracle/from_call.0.res.oracle b/tests/value/oracle/from_call.0.res.oracle
index 5f8aacfb014ade7377e9998ae79661c5f3f5ce64..90af155562b9b8797ae7bcbd68e0ee6bd42434e9 100644
--- a/tests/value/oracle/from_call.0.res.oracle
+++ b/tests/value/oracle/from_call.0.res.oracle
@@ -1,6 +1,10 @@
[kernel] Parsing tests/value/from_call.i (no preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
+[eva:alarm] tests/value/from_call.i:70: Warning:
+ pointer downcast. assert (unsigned int)(&AA) ≤ 2147483647;
+[eva:alarm] tests/value/from_call.i:71: Warning:
+ pointer downcast. assert (unsigned int)(&AA) ≤ 2147483647;
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
a ∈ {0}
diff --git a/tests/value/oracle/from_call.1.res.oracle b/tests/value/oracle/from_call.1.res.oracle
index e8c864534dc5e981b7c63292a1f42e4ece799b56..eb4493ddfd3a65d3dfce413d96809353d388e0e9 100644
--- a/tests/value/oracle/from_call.1.res.oracle
+++ b/tests/value/oracle/from_call.1.res.oracle
@@ -1,6 +1,10 @@
[kernel] Parsing tests/value/from_call.i (no preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
+[eva:alarm] tests/value/from_call.i:70: Warning:
+ pointer downcast. assert (unsigned int)(&AA) ≤ 2147483647;
+[eva:alarm] tests/value/from_call.i:71: Warning:
+ pointer downcast. assert (unsigned int)(&AA) ≤ 2147483647;
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
a ∈ {0}
diff --git a/tests/value/oracle/from_ptr.0.res.oracle b/tests/value/oracle/from_ptr.0.res.oracle
index 46f997dc35f0e830f429145d190dad1388f71ea6..7261a1cb811310c62ae52d2a8bf458e0b25f6de2 100644
--- a/tests/value/oracle/from_ptr.0.res.oracle
+++ b/tests/value/oracle/from_ptr.0.res.oracle
@@ -15,6 +15,10 @@
b ∈ {0}
p[0..9][0..9][0..9] ∈ {0}
q ∈ {0}
+[eva:alarm] tests/value/from_ptr.i:12: Warning:
+ pointer downcast. assert (unsigned int)(&p[11]) ≤ 2147483647;
+[eva:alarm] tests/value/from_ptr.i:13: Warning:
+ pointer downcast. assert (unsigned int)(&p[10]) ≤ 2147483647;
[eva:alarm] tests/value/from_ptr.i:17: Warning:
out of bounds write. assert \valid((int *)i);
[kernel] tests/value/from_ptr.i:17: Warning:
diff --git a/tests/value/oracle/from_ptr.1.res.oracle b/tests/value/oracle/from_ptr.1.res.oracle
index f1dd5f2cc2c5dd152dca8817202c2c84b01dfba5..1cde862a4b6551a10c5c50fbf37f9edddcd36857 100644
--- a/tests/value/oracle/from_ptr.1.res.oracle
+++ b/tests/value/oracle/from_ptr.1.res.oracle
@@ -15,6 +15,10 @@
b ∈ {0}
p[0..9][0..9][0..9] ∈ {0}
q ∈ {0}
+[eva:alarm] tests/value/from_ptr.i:24: Warning:
+ pointer downcast. assert (unsigned int)(&p[1]) ≤ 2147483647;
+[eva:alarm] tests/value/from_ptr.i:25: Warning:
+ pointer downcast. assert (unsigned int)((int (*)[10][10])p) ≤ 2147483647;
[eva] Recording results for main1
[eva] done for function main1
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/fun_ptr.1.res.oracle b/tests/value/oracle/fun_ptr.1.res.oracle
index f8b69ef751a77b9ba0cac41417df312e4b31fc68..3e7b008426e2a3857f1506beccf02faeb6d98f7a 100644
--- a/tests/value/oracle/fun_ptr.1.res.oracle
+++ b/tests/value/oracle/fun_ptr.1.res.oracle
@@ -8,6 +8,10 @@
expected 'short *' but got argument of type 'int *': & x
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
+[eva:alarm] tests/value/fun_ptr.i:21: Warning:
+ pointer downcast. assert (unsigned __int64)(&f) ≤ 9223372036854775807;
+[eva:alarm] tests/value/fun_ptr.i:21: Warning:
+ pointer downcast. assert (unsigned __int64)(&g) ≤ 9223372036854775807;
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
t[0] ∈ {{ (__int64)&f }}
diff --git a/tests/value/oracle/gauges.res.oracle b/tests/value/oracle/gauges.res.oracle
index fa19ee9d0ef3002d43a7656080239d7a89f6a42b..7cf52beab44793b0f3ed8c99f8dc13f610b85e11 100644
--- a/tests/value/oracle/gauges.res.oracle
+++ b/tests/value/oracle/gauges.res.oracle
@@ -240,6 +240,10 @@
[eva] computing for function main9 <- main.
Called from tests/value/gauges.c:361.
[eva] tests/value/gauges.c:186: starting to merge loop iterations
+[eva:alarm] tests/value/gauges.c:188: Warning:
+ pointer downcast. assert (unsigned int)p ≤ 2147483647;
+[eva:alarm] tests/value/gauges.c:188: Warning:
+ pointer downcast. assert (unsigned int)q ≤ 2147483647;
[eva:alarm] tests/value/gauges.c:188: Warning:
signed overflow. assert -2147483648 ≤ (int)p + (int)q;
[eva:alarm] tests/value/gauges.c:188: Warning:
diff --git a/tests/value/oracle/imprecise_invalid_write.res.oracle b/tests/value/oracle/imprecise_invalid_write.res.oracle
index 3442108db92a4fbc4284112a78b6cbed78012754..338f79ddc5e562248c7d3246b45271cb2c3c3945 100644
--- a/tests/value/oracle/imprecise_invalid_write.res.oracle
+++ b/tests/value/oracle/imprecise_invalid_write.res.oracle
@@ -21,6 +21,8 @@
[eva] Done for function main1
[eva] computing for function main2 <- main.
Called from tests/value/imprecise_invalid_write.i:25.
+[eva:alarm] tests/value/imprecise_invalid_write.i:9: Warning:
+ pointer downcast. assert (unsigned int)(&main1) ≤ 2147483647;
[eva] tests/value/imprecise_invalid_write.i:9:
Assigning imprecise value to p.
The imprecision originates from Arithmetic
@@ -33,6 +35,8 @@
[eva] Done for function main2
[eva] computing for function main3 <- main.
Called from tests/value/imprecise_invalid_write.i:28.
+[eva:alarm] tests/value/imprecise_invalid_write.i:16: Warning:
+ pointer downcast. assert (unsigned int)s ≤ 2147483647;
[eva] tests/value/imprecise_invalid_write.i:16:
Assigning imprecise value to p.
The imprecision originates from Arithmetic
diff --git a/tests/value/oracle/initialized.res.oracle b/tests/value/oracle/initialized.res.oracle
index f3d1c20aa17d60f4f052fe7a489807dd3537ff5f..b57ddb23b52afcfe2fb43e41160db19dd1996f01 100644
--- a/tests/value/oracle/initialized.res.oracle
+++ b/tests/value/oracle/initialized.res.oracle
@@ -66,6 +66,8 @@
[eva] Done for function g1
[eva] computing for function g2 <- main.
Called from tests/value/initialized.c:194.
+[eva:alarm] tests/value/initialized.c:50: Warning:
+ pointer downcast. assert (unsigned int)(&b4) ≤ 2147483647;
[eva:alarm] tests/value/initialized.c:50: Warning:
signed overflow. assert -2147483648 ≤ (int)(&b4) + (int)(&b4);
[eva:alarm] tests/value/initialized.c:50: Warning:
diff --git a/tests/value/oracle/join_misaligned.res.oracle b/tests/value/oracle/join_misaligned.res.oracle
index cb31ee65e403a3dd9324e6a25644b6f3c07d6db6..111aa1c6f07269e57c40e05b830f78610e7d81e3 100644
--- a/tests/value/oracle/join_misaligned.res.oracle
+++ b/tests/value/oracle/join_misaligned.res.oracle
@@ -14,6 +14,10 @@
z[0..4] ∈ {255}
a ∈ {0}
va ∈ [--..--]
+[eva:alarm] tests/value/join_misaligned.i:23: Warning:
+ pointer downcast. assert (unsigned int)(&t) ≤ 2147483647;
+[eva:alarm] tests/value/join_misaligned.i:37: Warning:
+ pointer downcast. assert (unsigned int)(&u) ≤ 2147483647;
[eva] Recording results for main
[eva] done for function main
[eva:garbled-mix] Warning:
diff --git a/tests/value/oracle/label.res.oracle b/tests/value/oracle/label.res.oracle
index a7dfd612adb73ce8ff24f9b2a2b76936f9e33e74..a87f0773b6eb65bac1d59beedb2c2d142fd94d48 100644
--- a/tests/value/oracle/label.res.oracle
+++ b/tests/value/oracle/label.res.oracle
@@ -10,6 +10,8 @@
i ∈ {0}
p ∈ {0}
q ∈ {0}
+[eva:alarm] tests/value/label.i:14: Warning:
+ pointer downcast. assert (unsigned int)(&d + 1) ≤ 2147483647;
[eva] tests/value/label.i:18:
Assigning imprecise value to *((char *)(& p) + i)
(pointing to p with offsets {0}).
diff --git a/tests/value/oracle/leaf2.res.oracle b/tests/value/oracle/leaf2.res.oracle
index db427e105c3dc4664fced2891c968210aae2f1e9..96ab8ffd9b41e9562a73dd6afd3f244a6c403e5f 100644
--- a/tests/value/oracle/leaf2.res.oracle
+++ b/tests/value/oracle/leaf2.res.oracle
@@ -6,6 +6,8 @@
G ∈ {0}
H ∈ {0}
I ∈ {0}
+[eva:alarm] tests/value/leaf2.i:6: Warning:
+ pointer downcast. assert (unsigned int)(&I) ≤ 2147483647;
[eva] computing for function f <- main.
Called from tests/value/leaf2.i:6.
[kernel:annot:missing-spec] tests/value/leaf2.i:6: Warning:
diff --git a/tests/value/oracle/mini_pointrer.res.oracle b/tests/value/oracle/mini_pointrer.res.oracle
index 2c0b41b4d4a63a35f3d6216f247a33171a4028f4..0cc72335a3a945d507756d104f6b9f40ca26ee8f 100644
--- a/tests/value/oracle/mini_pointrer.res.oracle
+++ b/tests/value/oracle/mini_pointrer.res.oracle
@@ -11,6 +11,8 @@
accessing out of bounds index. assert 0 ≤ c1;
[eva:alarm] tests/value/mini_pointrer.i:6: Warning:
accessing out of bounds index. assert c1 < 2;
+[eva:alarm] tests/value/mini_pointrer.i:6: Warning:
+ pointer downcast. assert (unsigned int)(&T[c1]) ≤ 2147483647;
[eva:alarm] tests/value/mini_pointrer.i:8: Warning:
out of bounds read. assert \valid_read(ppp);
[eva:alarm] tests/value/mini_pointrer.i:8: Warning:
diff --git a/tests/value/oracle/nonlin.res.oracle b/tests/value/oracle/nonlin.res.oracle
index de062d28c580191ea1a8cdb6de19c2f0ac49020a..433ce49eaa0ba5fe807e8a83e3c7550bb2c62d67 100644
--- a/tests/value/oracle/nonlin.res.oracle
+++ b/tests/value/oracle/nonlin.res.oracle
@@ -63,6 +63,8 @@
[eva:nonlin] tests/value/nonlin.c:21: subdividing on i
[eva:alarm] tests/value/nonlin.c:21: Warning:
out of bounds read. assert \valid_read((p + i) - i);
+[eva:alarm] tests/value/nonlin.c:23: Warning:
+ pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva:alarm] tests/value/nonlin.c:24: Warning:
out of bounds read. assert \valid_read((p + i) - i);
[eva] Recording results for subdivide_pointer
diff --git a/tests/value/oracle/not_ct_array_arg.res.oracle b/tests/value/oracle/not_ct_array_arg.res.oracle
index b6c5638c803e6da7d593848c541fb7418e386e7b..8be78fd49c0cde02afd96f8c3a7f7345cee83b0b 100644
--- a/tests/value/oracle/not_ct_array_arg.res.oracle
+++ b/tests/value/oracle/not_ct_array_arg.res.oracle
@@ -24,6 +24,8 @@
==END OF DUMP==
[eva:alarm] tests/value/not_ct_array_arg.i:12: Warning:
out of bounds write. assert \valid(&(*(tb + 9))[100]);
+[eva:alarm] tests/value/not_ct_array_arg.i:12: Warning:
+ pointer downcast. assert (unsigned int)(&tb) ≤ 2147483647;
[eva] tests/value/not_ct_array_arg.i:13:
Frama_C_dump_each:
# Cvalue domain:
diff --git a/tests/value/oracle/offset_top.res.oracle b/tests/value/oracle/offset_top.res.oracle
index bc18f222647e0f0ff249f35ea2d4dbcff8abb73d..8dbc430d5ee96b88e1fdc11243dd643dbfaa6a2b 100644
--- a/tests/value/oracle/offset_top.res.oracle
+++ b/tests/value/oracle/offset_top.res.oracle
@@ -6,6 +6,8 @@
NULL[rbits 0 to 2047] ∈ [--..--]
T ∈ {0}
TAB[0..9] ∈ {0}
+[eva:alarm] tests/value/offset_top.i:10: Warning:
+ pointer downcast. assert (unsigned int)(&TAB[*T]) ≤ 2147483647;
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/offsetmap.0.res.oracle b/tests/value/oracle/offsetmap.0.res.oracle
index ed60e2eb7466464a7334f4896599961a48bcb892..572459f644a8f9403d5f4f5cc1231c2b6bf93b2e 100644
--- a/tests/value/oracle/offsetmap.0.res.oracle
+++ b/tests/value/oracle/offsetmap.0.res.oracle
@@ -27,6 +27,8 @@
Called from tests/value/offsetmap.i:75.
[eva] tests/value/offsetmap.i:19: starting to merge loop iterations
[eva] tests/value/offsetmap.i:29: starting to merge loop iterations
+[eva:alarm] tests/value/offsetmap.i:51: Warning:
+ pointer downcast. assert (unsigned int)(&x2) ≤ 2147483647;
[eva] Recording results for f
[eva] Done for function f
[eva] computing for function g <- main.
diff --git a/tests/value/oracle/offsetmap.1.res.oracle b/tests/value/oracle/offsetmap.1.res.oracle
index dbf10008a7f66e55292c0882ccc83a502ca8ca94..d4ac4533187b26fcde94ffc2686f55870879fca3 100644
--- a/tests/value/oracle/offsetmap.1.res.oracle
+++ b/tests/value/oracle/offsetmap.1.res.oracle
@@ -27,6 +27,8 @@
Called from tests/value/offsetmap.i:75.
[eva] tests/value/offsetmap.i:19: starting to merge loop iterations
[eva] tests/value/offsetmap.i:29: starting to merge loop iterations
+[eva:alarm] tests/value/offsetmap.i:51: Warning:
+ pointer downcast. assert (unsigned int)(&x2) ≤ 2147483647;
[eva] Recording results for f
[eva] Done for function f
[eva] computing for function g <- main.
diff --git a/tests/value/oracle/origin.0.res.oracle b/tests/value/oracle/origin.0.res.oracle
index 64ee1af662166a6561d4bf893d8f0730672cde0e..2bdd5becc39c217a92386b0eec24bb4ac9ebdd71 100644
--- a/tests/value/oracle/origin.0.res.oracle
+++ b/tests/value/oracle/origin.0.res.oracle
@@ -54,6 +54,8 @@
S_gpp[0..1] ∈ [--..--]
[eva] computing for function origin_arithmetic_1 <- main.
Called from tests/value/origin.i:94.
+[eva:alarm] tests/value/origin.i:14: Warning:
+ pointer downcast. assert (unsigned int)((int *)ta1) ≤ 2147483647;
[eva:alarm] tests/value/origin.i:14: Warning:
signed overflow. assert -2147483648 ≤ -((int)((int *)ta1));
[eva:alarm] tests/value/origin.i:14: Warning:
@@ -67,6 +69,8 @@
[eva] Done for function origin_arithmetic_1
[eva] computing for function origin_arithmetic_2 <- main.
Called from tests/value/origin.i:95.
+[eva:alarm] tests/value/origin.i:19: Warning:
+ pointer downcast. assert (unsigned int)((int *)ta2) ≤ 2147483647;
[eva:alarm] tests/value/origin.i:19: Warning:
signed overflow. assert -2147483648 ≤ -((int)((int *)ta2));
[eva:alarm] tests/value/origin.i:19: Warning:
@@ -77,6 +81,8 @@
[eva] tests/value/origin.i:20:
Assigning imprecise value to qa2.
The imprecision originates from Arithmetic {tests/value/origin.i:19}
+[eva:alarm] tests/value/origin.i:20: Warning:
+ pointer downcast. assert (unsigned int)((int *)tta2) ≤ 2147483647;
[eva:alarm] tests/value/origin.i:20: Warning:
signed overflow. assert -2147483648 ≤ -((int)((int *)tta2));
[eva:alarm] tests/value/origin.i:20: Warning:
@@ -86,10 +92,14 @@
The imprecision originates from Arithmetic {tests/value/origin.i:20}
[eva:alarm] tests/value/origin.i:21: Warning:
out of bounds write. assert \valid(qa2);
+[eva:alarm] tests/value/origin.i:21: Warning:
+ pointer downcast. assert (unsigned int)(&aa2) ≤ 2147483647;
[eva] Recording results for origin_arithmetic_2
[eva] Done for function origin_arithmetic_2
[eva] computing for function origin_arithmetic_3 <- main.
Called from tests/value/origin.i:96.
+[eva:alarm] tests/value/origin.i:25: Warning:
+ pointer downcast. assert (unsigned int)((int *)ta3) ≤ 2147483647;
[eva:alarm] tests/value/origin.i:25: Warning:
signed overflow. assert -2147483648 ≤ -((int)((int *)ta3));
[eva:alarm] tests/value/origin.i:25: Warning:
@@ -148,6 +158,8 @@
{{ garbled mix of &{a; b} (origin: Misaligned {tests/value/origin.i:54}) }}
[eva:alarm] tests/value/origin.i:56: Warning:
out of bounds write. assert \valid(qm2);
+[eva:alarm] tests/value/origin.i:56: Warning:
+ pointer downcast. assert (unsigned int)(&a) ≤ 2147483647;
[eva] Recording results for origin_misalign_2
[eva] Done for function origin_misalign_2
[eva] computing for function origin_uninitialized_1 <- main.
@@ -166,6 +178,12 @@
[eva] Done for function origin_uninitialized_2
[eva] computing for function local_escape_1 <- main.
Called from tests/value/origin.i:108.
+[eva:alarm] tests/value/origin.i:83: Warning:
+ pointer downcast. assert (unsigned int)(&arg) ≤ 2147483647;
+[eva:alarm] tests/value/origin.i:84: Warning:
+ pointer downcast. assert (unsigned int)(&local1) ≤ 2147483647;
+[eva:alarm] tests/value/origin.i:85: Warning:
+ pointer downcast. assert (unsigned int)(&arg) ≤ 2147483647;
[eva:alarm] tests/value/origin.i:85: Warning:
signed overflow. assert -2147483648 ≤ -((int)(&arg));
[eva:alarm] tests/value/origin.i:85: Warning:
@@ -173,6 +191,10 @@
[eva] tests/value/origin.i:85:
Assigning imprecise value to esc3.
The imprecision originates from Arithmetic {tests/value/origin.i:85}
+[eva:alarm] tests/value/origin.i:87: Warning:
+ pointer downcast. assert (unsigned int)(&local1) ≤ 2147483647;
+[eva:alarm] tests/value/origin.i:88: Warning:
+ pointer downcast. assert (unsigned int)(&esc1) ≤ 2147483647;
[eva] Recording results for local_escape_1
[eva] Done for function local_escape_1
[eva:locals-escaping] tests/value/origin.i:108: Warning:
@@ -187,6 +209,7 @@
[eva] done for function main
[eva] tests/value/origin.i:75:
assertion 'Eva,initialization' got final status invalid.
+[scope:rm_asserts] removing 2 assertion(s)
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function local_escape_1:
esc1 ∈ {{ (int)&arg }}
diff --git a/tests/value/oracle/origin.1.res.oracle b/tests/value/oracle/origin.1.res.oracle
index b8a6b3cb99b375317a49b248133106a0f094ed93..0b3195a5397b0126f8eed45040fafff00df4c125 100644
--- a/tests/value/oracle/origin.1.res.oracle
+++ b/tests/value/oracle/origin.1.res.oracle
@@ -64,6 +64,8 @@
[eva] tests/value/origin.i:129:
Assigning imprecise value to r.t[0].
The imprecision originates from Merge {tests/value/origin.i:129}
+[eva:alarm] tests/value/origin.i:130: Warning:
+ pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva:alarm] tests/value/origin.i:130: Warning:
signed overflow. assert -2147483648 ≤ -((int)(&x));
[eva:alarm] tests/value/origin.i:130: Warning:
diff --git a/tests/value/oracle/period.res.oracle b/tests/value/oracle/period.res.oracle
index 0283e81195e5dfb1886fd792544581c9ba206445..2af9a46bd2a738663bb66bde0768d88bc3967919 100644
--- a/tests/value/oracle/period.res.oracle
+++ b/tests/value/oracle/period.res.oracle
@@ -78,18 +78,25 @@
Gt ∈ {12}
Ht ∈ {1}
==END OF DUMP==
+[eva:alarm] tests/value/period.c:51: Warning:
+ pointer downcast. assert (unsigned int)(&g) ≤ 2147483647;
[eva] tests/value/period.c:51:
Assigning imprecise value to p.
The imprecision originates from Arithmetic {tests/value/period.c:51}
[eva:alarm] tests/value/period.c:52: Warning:
out of bounds write. assert \valid(p);
+[eva:alarm] tests/value/period.c:53: Warning:
+ pointer downcast. assert (unsigned int)(&g) ≤ 2147483647;
[eva] tests/value/period.c:53:
Assigning imprecise value to p.
The imprecision originates from Arithmetic {tests/value/period.c:53}
[eva:alarm] tests/value/period.c:54: Warning:
out of bounds read. assert \valid_read(p);
+[eva:alarm] tests/value/period.c:55: Warning:
+ pointer downcast. assert (unsigned int)(&vg) ≤ 2147483647;
[eva] Recording results for main
[eva] done for function main
+[scope:rm_asserts] removing 1 assertion(s)
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
g[0..9] ∈
diff --git a/tests/value/oracle/pointer_comparison.0.res.oracle b/tests/value/oracle/pointer_comparison.0.res.oracle
index c58a323eab8082ad0f725a204de27b2a959e86dc..6ac5900dc2e425cc69bd9317d1baadd5b41e2e7f 100644
--- a/tests/value/oracle/pointer_comparison.0.res.oracle
+++ b/tests/value/oracle/pointer_comparison.0.res.oracle
@@ -18,6 +18,10 @@
[eva] tests/value/pointer_comparison.c:14: Frama_C_show_each_4: {{ &x + {16} }}
[eva:pointer-comparison] tests/value/pointer_comparison.c:16:
invalid pointer comparison: invalid pointer(s)
+[eva:alarm] tests/value/pointer_comparison.c:16: Warning:
+ pointer downcast. assert (unsigned int)p ≤ 2147483647;
+[eva:alarm] tests/value/pointer_comparison.c:16: Warning:
+ pointer downcast. assert (unsigned int)(&y) ≤ 2147483647;
[eva] tests/value/pointer_comparison.c:16: Frama_C_show_each_5: {{ &x + {16} }}
[eva] tests/value/pointer_comparison.c:17: Frama_C_show_each_5e: {{ &x + {16} }}
[eva:pointer-comparison] tests/value/pointer_comparison.c:18:
@@ -48,8 +52,23 @@
[inout] Inputs for function main:
p
[report] Computing properties status...
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'main'
+--------------------------------------------------------------------------------
+
+[ - ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 16)
+ assert Eva: pointer_downcast: (unsigned int)p ≤ 2147483647;
+ tried with Eva.
+[ - ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 16)
+ assert Eva: pointer_downcast: (unsigned int)(&y) ≤ 2147483647;
+ tried with Eva.
+
--------------------------------------------------------------------------------
---- No status to report
+--- Status Report Summary
+--------------------------------------------------------------------------------
+ 2 To be validated
+ 2 Total
--------------------------------------------------------------------------------
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
@@ -74,6 +93,10 @@
assert \pointer_comparable((void *)tmp_2, (void *)(&y));
(tmp_2 from p++)
[eva] tests/value/pointer_comparison.c:14: Frama_C_show_each_4: {{ &x + {16} }}
+[eva:alarm] tests/value/pointer_comparison.c:16: Warning:
+ pointer downcast. assert (unsigned int)p ≤ 2147483647;
+[eva:alarm] tests/value/pointer_comparison.c:16: Warning:
+ pointer downcast. assert (unsigned int)(&y) ≤ 2147483647;
[eva] tests/value/pointer_comparison.c:16: Frama_C_show_each_5: {{ &x + {16} }}
[eva] tests/value/pointer_comparison.c:17: Frama_C_show_each_5e: {{ &x + {16} }}
[eva:alarm] tests/value/pointer_comparison.c:18: Warning:
@@ -125,6 +148,12 @@
Eva: ptr_comparison:
\pointer_comparable((void *)tmp_2, (void *)(&y));
tried with Eva.
+[ - ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 16)
+ assert Eva: pointer_downcast: (unsigned int)p ≤ 2147483647;
+ tried with Eva.
+[ - ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 16)
+ assert Eva: pointer_downcast: (unsigned int)(&y) ≤ 2147483647;
+ tried with Eva.
[ - ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 18)
assert
Eva: ptr_comparison:
@@ -134,8 +163,8 @@
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
- 4 To be validated
- 4 Total
+ 6 To be validated
+ 6 Total
--------------------------------------------------------------------------------
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
@@ -160,6 +189,10 @@
assert \pointer_comparable((void *)tmp_2, (void *)(&y));
(tmp_2 from p++)
[eva] tests/value/pointer_comparison.c:14: Frama_C_show_each_4: {{ &x + {16} }}
+[eva:alarm] tests/value/pointer_comparison.c:16: Warning:
+ pointer downcast. assert (unsigned int)p ≤ 2147483647;
+[eva:alarm] tests/value/pointer_comparison.c:16: Warning:
+ pointer downcast. assert (unsigned int)(&y) ≤ 2147483647;
[eva:alarm] tests/value/pointer_comparison.c:16: Warning:
pointer comparison. assert \pointer_comparable((void *)p, (void *)(&y));
[eva] tests/value/pointer_comparison.c:16: Frama_C_show_each_5: {{ &x + {16} }}
@@ -213,6 +246,12 @@
Eva: ptr_comparison:
\pointer_comparable((void *)tmp_2, (void *)(&y));
tried with Eva.
+[ - ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 16)
+ assert Eva: pointer_downcast: (unsigned int)p ≤ 2147483647;
+ tried with Eva.
+[ - ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 16)
+ assert Eva: pointer_downcast: (unsigned int)(&y) ≤ 2147483647;
+ tried with Eva.
[ - ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 16)
assert
Eva: ptr_comparison: \pointer_comparable((void *)p, (void *)(&y));
@@ -226,6 +265,6 @@
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
- 5 To be validated
- 5 Total
+ 7 To be validated
+ 7 Total
--------------------------------------------------------------------------------
diff --git a/tests/value/oracle/pointer_comparison.1.res.oracle b/tests/value/oracle/pointer_comparison.1.res.oracle
index 890e9690c6c1d14e06b4af1515e5dc193155e4f0..cd63714dccccd315f1b03fddceefecccc8f7ddd8 100644
--- a/tests/value/oracle/pointer_comparison.1.res.oracle
+++ b/tests/value/oracle/pointer_comparison.1.res.oracle
@@ -33,6 +33,10 @@
[eva] tests/value/pointer_comparison.c:15: Frama_C_show_each_4e: {{ &x + {16} }}
[eva:pointer-comparison] tests/value/pointer_comparison.c:16:
invalid pointer comparison: invalid pointer(s)
+[eva:alarm] tests/value/pointer_comparison.c:16: Warning:
+ pointer downcast. assert (unsigned int)p ≤ 2147483647;
+[eva:alarm] tests/value/pointer_comparison.c:16: Warning:
+ pointer downcast. assert (unsigned int)(&y) ≤ 2147483647;
[eva] tests/value/pointer_comparison.c:16: Frama_C_show_each_5: {{ &x + {16} }}
[eva] tests/value/pointer_comparison.c:17: Frama_C_show_each_5e: {{ &x + {16} }}
[eva:pointer-comparison] tests/value/pointer_comparison.c:18:
@@ -68,8 +72,23 @@
[inout] Inputs for function main:
p
[report] Computing properties status...
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'main'
+--------------------------------------------------------------------------------
+
+[ - ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 16)
+ assert Eva: pointer_downcast: (unsigned int)p ≤ 2147483647;
+ tried with Eva.
+[ - ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 16)
+ assert Eva: pointer_downcast: (unsigned int)(&y) ≤ 2147483647;
+ tried with Eva.
+
--------------------------------------------------------------------------------
---- No status to report
+--- Status Report Summary
+--------------------------------------------------------------------------------
+ 2 To be validated
+ 2 Total
--------------------------------------------------------------------------------
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
@@ -97,6 +116,10 @@
(tmp_2 from p++)
[eva] tests/value/pointer_comparison.c:14: Frama_C_show_each_4: {{ &x + {16} }}
[eva] tests/value/pointer_comparison.c:15: Frama_C_show_each_4e: {{ &x + {16} }}
+[eva:alarm] tests/value/pointer_comparison.c:16: Warning:
+ pointer downcast. assert (unsigned int)p ≤ 2147483647;
+[eva:alarm] tests/value/pointer_comparison.c:16: Warning:
+ pointer downcast. assert (unsigned int)(&y) ≤ 2147483647;
[eva] tests/value/pointer_comparison.c:16: Frama_C_show_each_5: {{ &x + {16} }}
[eva] tests/value/pointer_comparison.c:17: Frama_C_show_each_5e: {{ &x + {16} }}
[eva:alarm] tests/value/pointer_comparison.c:18: Warning:
@@ -149,6 +172,12 @@
Eva: ptr_comparison:
\pointer_comparable((void *)tmp_2, (void *)(&y));
tried with Eva.
+[ - ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 16)
+ assert Eva: pointer_downcast: (unsigned int)p ≤ 2147483647;
+ tried with Eva.
+[ - ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 16)
+ assert Eva: pointer_downcast: (unsigned int)(&y) ≤ 2147483647;
+ tried with Eva.
[ - ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 18)
assert
Eva: ptr_comparison:
@@ -158,8 +187,8 @@
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
- 4 To be validated
- 4 Total
+ 6 To be validated
+ 6 Total
--------------------------------------------------------------------------------
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
@@ -187,6 +216,10 @@
(tmp_2 from p++)
[eva] tests/value/pointer_comparison.c:14: Frama_C_show_each_4: {{ &x + {16} }}
[eva] tests/value/pointer_comparison.c:15: Frama_C_show_each_4e: {{ &x + {16} }}
+[eva:alarm] tests/value/pointer_comparison.c:16: Warning:
+ pointer downcast. assert (unsigned int)p ≤ 2147483647;
+[eva:alarm] tests/value/pointer_comparison.c:16: Warning:
+ pointer downcast. assert (unsigned int)(&y) ≤ 2147483647;
[eva:alarm] tests/value/pointer_comparison.c:16: Warning:
pointer comparison. assert \pointer_comparable((void *)p, (void *)(&y));
[eva] tests/value/pointer_comparison.c:16: Frama_C_show_each_5: {{ &x + {16} }}
@@ -241,6 +274,12 @@
Eva: ptr_comparison:
\pointer_comparable((void *)tmp_2, (void *)(&y));
tried with Eva.
+[ - ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 16)
+ assert Eva: pointer_downcast: (unsigned int)p ≤ 2147483647;
+ tried with Eva.
+[ - ] Assertion 'Eva,pointer_downcast' (file tests/value/pointer_comparison.c, line 16)
+ assert Eva: pointer_downcast: (unsigned int)(&y) ≤ 2147483647;
+ tried with Eva.
[ - ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 16)
assert
Eva: ptr_comparison: \pointer_comparable((void *)p, (void *)(&y));
@@ -254,6 +293,6 @@
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
- 5 To be validated
- 5 Total
+ 7 To be validated
+ 7 Total
--------------------------------------------------------------------------------
diff --git a/tests/value/oracle/pointer_int_cast.res.oracle b/tests/value/oracle/pointer_int_cast.res.oracle
index 078dfbbd5bee8472325f2b748799bbafe9459628..cad14cc1bd042de3a5b4ae42904551966dc6a151 100644
--- a/tests/value/oracle/pointer_int_cast.res.oracle
+++ b/tests/value/oracle/pointer_int_cast.res.oracle
@@ -8,6 +8,8 @@
q ∈ {0}
x ∈ {0}
y ∈ {0}
+[eva:alarm] tests/value/pointer_int_cast.i:9: Warning:
+ pointer downcast. assert (unsigned int)(&y) ≤ 2147483647;
[eva] Recording results for g
[eva] done for function g
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/shift.0.res.oracle b/tests/value/oracle/shift.0.res.oracle
index aa83c00acb6fec860002e54317aee5ec41e97e39..b2838250a6d5104942a7d000707c740654d060e8 100644
--- a/tests/value/oracle/shift.0.res.oracle
+++ b/tests/value/oracle/shift.0.res.oracle
@@ -44,6 +44,8 @@
[eva] tests/value/shift.i:52:
Assigning imprecise value to r.
The imprecision originates from Arithmetic {tests/value/shift.i:52}
+[eva:alarm] tests/value/shift.i:53: Warning:
+ pointer downcast. assert (unsigned int)((char *)t) ≤ 2147483647;
[eva:alarm] tests/value/shift.i:53: Warning:
invalid LHS operand for left shift. assert 0 ≤ (long)((char *)t);
[eva:alarm] tests/value/shift.i:53: Warning:
diff --git a/tests/value/oracle/shift.1.res.oracle b/tests/value/oracle/shift.1.res.oracle
index 076532ff7124c6875536b00e1051863ad9d4aa3c..9862244f180a9db29e4f8a675b3763cf0dc72b3d 100644
--- a/tests/value/oracle/shift.1.res.oracle
+++ b/tests/value/oracle/shift.1.res.oracle
@@ -38,6 +38,8 @@
[eva] tests/value/shift.i:52:
Assigning imprecise value to r.
The imprecision originates from Arithmetic {tests/value/shift.i:52}
+[eva:alarm] tests/value/shift.i:53: Warning:
+ pointer downcast. assert (unsigned int)((char *)t) ≤ 2147483647;
[eva:alarm] tests/value/shift.i:53: Warning:
signed overflow. assert -2147483648 ≤ (long)((char *)t) << 8;
[eva:alarm] tests/value/shift.i:53: Warning:
diff --git a/tests/value/oracle/sizeof.res.oracle b/tests/value/oracle/sizeof.res.oracle
index 90ea60d5201575ac44fcbe81c059e02e2632d14d..adc483ff665929f6a5ccbcac65eee15f7da03395 100644
--- a/tests/value/oracle/sizeof.res.oracle
+++ b/tests/value/oracle/sizeof.res.oracle
@@ -18,6 +18,8 @@
[eva] Done for function main1
[eva] computing for function main2 <- main.
Called from tests/value/sizeof.i:41.
+[eva:alarm] tests/value/sizeof.i:32: Warning:
+ pointer downcast. assert (unsigned int)(&s1) ≤ 2147483647;
[eva] tests/value/sizeof.i:32:
Assigning imprecise value to p.
The imprecision originates from Arithmetic {tests/value/sizeof.i:32}
@@ -124,6 +126,7 @@ struct s s1;
int volatile i;
void main2(void)
{
+ /*@ assert Eva: pointer_downcast: (unsigned int)(&s1) ≤ 2147483647; */
struct s *p = (& s1 + (int)(& s1)) - (int)(& s1);
/*@ assert
Eva: index_bound: (unsigned int)(sizeof(s1.t) - (unsigned int)i) < 10;
diff --git a/tests/value/oracle/struct3.res.oracle b/tests/value/oracle/struct3.res.oracle
index 73e5ba0ea066bc75260c87fae0c189e46048166b..4cbcaa45fece740a5d003524f97f4d0e6c3bd565 100644
--- a/tests/value/oracle/struct3.res.oracle
+++ b/tests/value/oracle/struct3.res.oracle
@@ -19,6 +19,10 @@
accessing out of bounds index. assert 10 < 10;
[kernel] tests/value/struct3.i:42: Warning:
all target addresses were invalid. This path is assumed to be dead.
+[eva:alarm] tests/value/struct3.i:46: Warning:
+ pointer downcast. assert (unsigned int)s2.c ≤ 2147483647;
+[eva:alarm] tests/value/struct3.i:46: Warning:
+ pointer downcast. assert (unsigned int)(s2.c + (int)s2.c) ≤ 2147483647;
[eva] tests/value/struct3.i:46:
Assigning imprecise value to s2.a.
The imprecision originates from Arithmetic {tests/value/struct3.i:46}
diff --git a/tests/value/oracle/struct_array.res.oracle b/tests/value/oracle/struct_array.res.oracle
index faf7f29e81bdc46b6f0a80ba6da31a3c64d8b13e..05ac2f16880175bd81d50810e8f58c82ee0a05a7 100644
--- a/tests/value/oracle/struct_array.res.oracle
+++ b/tests/value/oracle/struct_array.res.oracle
@@ -1,6 +1,12 @@
[kernel] Parsing tests/value/struct_array.i (no preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
+[eva:alarm] tests/value/struct_array.i:15: Warning:
+ pointer downcast. assert (unsigned int)(&z1) ≤ 2147483647;
+[eva:alarm] tests/value/struct_array.i:15: Warning:
+ pointer downcast. assert (unsigned int)(&z2) ≤ 2147483647;
+[eva:alarm] tests/value/struct_array.i:15: Warning:
+ pointer downcast. assert (unsigned int)(&z4) ≤ 2147483647;
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
v ∈ [--..--]
@@ -234,6 +240,12 @@
[19].p; [20].p; [21].p}; s; s1; s2; s3
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
+[eva:alarm] tests/value/struct_array.i:15: Warning:
+ pointer downcast. assert (unsigned int)(&z1) ≤ 2147483647;
+[eva:alarm] tests/value/struct_array.i:15: Warning:
+ pointer downcast. assert (unsigned int)(&z2) ≤ 2147483647;
+[eva:alarm] tests/value/struct_array.i:15: Warning:
+ pointer downcast. assert (unsigned int)(&z4) ≤ 2147483647;
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
v ∈ [--..--]
diff --git a/tests/value/oracle/struct_incl.res.oracle b/tests/value/oracle/struct_incl.res.oracle
index 7f41406ae8876196443ccfd0f061fe5c14b45722..3eb4f598ee5535e92806764dd7628d0d1bc3307c 100644
--- a/tests/value/oracle/struct_incl.res.oracle
+++ b/tests/value/oracle/struct_incl.res.oracle
@@ -22,6 +22,12 @@
z ∈ {0}
t ∈ {0}
v ∈ [--..--]
+[eva:alarm] tests/value/struct_incl.i:28: Warning:
+ pointer downcast. assert (unsigned int)(&s1.d[9]) ≤ 2147483647;
+[eva:alarm] tests/value/struct_incl.i:29: Warning:
+ pointer downcast. assert (unsigned int)(&s1.d[10]) ≤ 2147483647;
+[eva:alarm] tests/value/struct_incl.i:30: Warning:
+ pointer downcast. assert (unsigned int)(&s1.b) ≤ 2147483647;
[eva:alarm] tests/value/struct_incl.i:48: Warning:
accessing out of bounds index. assert 10 < 10;
[kernel] tests/value/struct_incl.i:48: Warning:
diff --git a/tests/value/oracle/symbolic_locs.res.oracle b/tests/value/oracle/symbolic_locs.res.oracle
index 154a7b55ae69c0322855b6ec0641415c750dac3c..eb325482dff5626613b033e1a10ed1426e77a835 100644
--- a/tests/value/oracle/symbolic_locs.res.oracle
+++ b/tests/value/oracle/symbolic_locs.res.oracle
@@ -64,6 +64,8 @@
Called from tests/value/symbolic_locs.i:121.
[eva:alarm] tests/value/symbolic_locs.i:51: Warning:
assertion got status unknown.
+[eva:alarm] tests/value/symbolic_locs.i:54: Warning:
+ pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
[eva] tests/value/symbolic_locs.i:55:
Frama_C_dump_each:
# Cvalue domain:
diff --git a/tests/value/oracle/test_arith.res.oracle b/tests/value/oracle/test_arith.res.oracle
index 8e462c9e595ce5651bccad91d3ee4d434ff1fa56..0eacce08467e7b1726285b701f49cbe4f7613b07 100644
--- a/tests/value/oracle/test_arith.res.oracle
+++ b/tests/value/oracle/test_arith.res.oracle
@@ -17,6 +17,8 @@
G ∈ {0}
[eva:alarm] tests/value/test_arith.c:16: Warning:
signed overflow. assert n + 1 ≤ 2147483647;
+[eva:alarm] tests/value/test_arith.c:18: Warning:
+ pointer downcast. assert (unsigned int)ptr ≤ 2147483647;
[eva:alarm] tests/value/test_arith.c:18: Warning:
signed overflow. assert -2147483648 ≤ (int)ptr + 1;
[eva:alarm] tests/value/test_arith.c:18: Warning:
diff --git a/tests/value/oracle/val6.0.res.oracle b/tests/value/oracle/val6.0.res.oracle
index 4e2b389231689d1033ecb2773969b962487172d1..6f55e39160535d43c76637297a29444fff5d2392 100644
--- a/tests/value/oracle/val6.0.res.oracle
+++ b/tests/value/oracle/val6.0.res.oracle
@@ -9,6 +9,8 @@
b ∈ {0}
y ∈ {0}
x ∈ {0}
+[eva:alarm] tests/value/val6.i:13: Warning:
+ pointer downcast. assert (unsigned int)c ≤ 2147483647;
[eva] Recording results for f
[eva] done for function f
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/volatile.res.oracle b/tests/value/oracle/volatile.res.oracle
index fe1efbbfceb93a5fde01d1a898afddbdc39dd98d..8cfa94fed9df507ba41a46c8921cf3b906e5eb20 100644
--- a/tests/value/oracle/volatile.res.oracle
+++ b/tests/value/oracle/volatile.res.oracle
@@ -90,6 +90,8 @@
[eva] Done for function main1
[eva] computing for function main2 <- main.
Called from tests/value/volatile.c:177.
+[eva:alarm] tests/value/volatile.c:83: Warning:
+ pointer downcast. assert (unsigned int)(&X) ≤ 2147483647;
[eva] Recording results for main2
[eva] Done for function main2
[eva] computing for function main3 <- main.
diff --git a/tests/value/oracle/volatilestruct.res.oracle b/tests/value/oracle/volatilestruct.res.oracle
index ed81eece0db93c42d0a0d23243d2c91ace28ebfa..256e74cfbacfc6a6c2b098a2703e0ef1b94d90ca 100644
--- a/tests/value/oracle/volatilestruct.res.oracle
+++ b/tests/value/oracle/volatilestruct.res.oracle
@@ -7,6 +7,8 @@
s2 ∈ {0}
x ∈ {0}
y ∈ {0}
+[eva:alarm] tests/value/volatilestruct.c:31: Warning:
+ pointer downcast. assert (unsigned int)p->f4.f2 ≤ 2147483647;
[eva:alarm] tests/value/volatilestruct.c:33: Warning:
signed overflow. assert -2147483648 ≤ &x - p->f4.f1;
[eva:alarm] tests/value/volatilestruct.c:33: Warning:
@@ -53,6 +55,8 @@
s2 ∈ {0}
x ∈ {0}
y ∈ {0}
+[eva:alarm] tests/value/volatilestruct.c:31: Warning:
+ pointer downcast. assert (unsigned int)p->f4.f2 ≤ 2147483647;
[eva:signed-overflow] tests/value/volatilestruct.c:33: Warning:
2's complement assumed for overflow
[eva:signed-overflow] tests/value/volatilestruct.c:34: Warning: