diff --git a/src/plugins/eva/domains/cvalue/builtins_memory.ml b/src/plugins/eva/domains/cvalue/builtins_memory.ml
index 85181c1a4218956a3ac6f9d36fa17d21cb6108dd..cc33f02c7db7e07a260ca99dfd49d901b6959230 100644
--- a/src/plugins/eva/domains/cvalue/builtins_memory.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_memory.ml
@@ -36,63 +36,7 @@ let rec lval_of_address exp =
| CastE (_typ, exp) -> lval_of_address exp
| _ -> Cil.mkMem ~addr:exp ~off:Cil_types.NoOffset
-let frama_C_is_base_aligned _state = function
- | [_, x; _, y] ->
- let result =
- match Ival.project_small_set (Cvalue.V.project_ival y) with
- | Some si ->
- let aligned =
- Location_Bytes.for_all
- (fun b _o -> List.for_all (Base.is_aligned_by b) si)
- x
- in
- if aligned then Cvalue.V.singleton_one else Cvalue.V.zero_or_one
- | None
- | exception Cvalue.V.Not_based_on_null -> Cvalue.V.zero_or_one
- in
- Builtins.Result [result]
- | _ -> raise (Builtins.Invalid_nb_of_args 2)
-
-let () = register_builtin "Frama_C_is_base_aligned" frama_C_is_base_aligned
-
-
-let frama_c_offset _state = function
- | [_, x] ->
- let result =
- try
- let acc = Ival.bottom in
- let offsets = Location_Bytes.fold_i (fun _b -> Ival.join) x acc in
- Cvalue.V.inject_ival offsets
- with Abstract_interp.Error_Top ->
- Self.error ~current:true
- "Builtin Frama_C_offset is applied to a value not \
- guaranteed to be an address";
- Cvalue.V.top_int
- in
- Builtins.Result [result]
- | _ -> raise (Builtins.Invalid_nb_of_args 1)
-
-let () = register_builtin "Frama_C_offset" frama_c_offset
-
-exception Memcpy_result of (Cvalue.Model.t * Assigns.t * Zone.t)
-
-exception Indeterminate of V_Or_Uninitialized.t
-
-(* Called by the [memcpy] builtin. Warns when the offsetmap contains
- an indeterminate value, when the imprecision category is enabled *)
-let memcpy_check_indeterminate_offsetmap offsm =
- if Self.is_debug_key_enabled dkey then
- try
- let aux_offset _ (v, _, _) =
- match v with
- | V_Or_Uninitialized.C_init_noesc _ -> ()
- | _ -> raise (Indeterminate v)
- in
- V_Offsetmap.iter aux_offset offsm
- with Indeterminate v ->
- Self.debug ~current:true ~dkey ~once:true
- "@[In memcpy@ builtin:@ precise@ copy of@ indeterminate@ values %a@]%t"
- V_Or_Uninitialized.pretty v Eva_utils.pp_callstack
+let plevel = Parameters.ArrayPrecisionLevel.get
(* Create a dependency [\from arg_n] where n is the nth argument of the
currently called function. *)
@@ -103,282 +47,260 @@ let deps_nth_arg n =
Deps.add_data Deps.bottom (Locations.zone_of_varinfo vi)
with Failure _ -> Kernel.fatal "%d arguments expected" n
+(* Preconditions of memcpy, memmove and memset ensures that pointer arguments
+ are valid. Reduce them accordingly. *)
+let reduce_to_valid_loc dst size access =
+ let min_size = Ival.min_int size in
+ let size = Option.fold ~none:Int_Base.zero ~some:Int_Base.inject min_size in
+ let dst_loc = Locations.make_loc dst size in
+ let valid_dst_loc = Locations.valid_part ~bitfield:false access dst_loc in
+ valid_dst_loc.Locations.loc
+
+(* -------------------------------------------------------------------------- *)
+(* Memcpy & Memmove *)
+(* -------------------------------------------------------------------------- *)
+
+(* Warns when the value is indeterminate. *)
+let warn_indeterminate_value ~name ?(precise = false) = function
+ | V_Or_Uninitialized.C_init_noesc _ -> ()
+ | _ ->
+ Self.result ~dkey ~current:true ~once:true
+ "@[In %s builtin:@ %sprecise copy@ of indeterminate values.@]%t"
+ name (if precise then "" else "im") Eva_utils.pp_callstack
+
+(* Warns when the offsetmap contains an indeterminate value. *)
+let check_indeterminate_offsetmap ~name offsm =
+ if Self.is_debug_key_enabled dkey then
+ let warn _ (v, _, _) = warn_indeterminate_value ~name ~precise:true v in
+ V_Offsetmap.iter warn offsm
+
+(* Adds \from dependency from [src_loc] to [dst_loc]. *)
+let add_deps_loc ~exact ~src_loc ~dst_loc deps_table =
+ let src_zone = Locations.(enumerate_valid_bits Read src_loc) in
+ let dst_zone = Locations.(enumerate_valid_bits Write dst_loc) in
+ let deps = Deps.(add_data bottom src_zone) in
+ Assigns.Memory.add_binding ~exact deps_table dst_zone deps
+
+(* Adds a sure \from dependency of size [size] from [src] to [dst].
+ Also returns the written zone if it is a singleton. *)
+let add_sure_deps ~size ~src ~dst (deps_table, sure_output) =
+ let size = Int_Base.inject size in
+ let src_loc = Locations.make_loc src size in
+ let dst_loc = Locations.make_loc dst size in
+ let exact = Location_Bits.cardinal_zero_or_one dst in
+ let deps_table = add_deps_loc ~exact ~src_loc ~dst_loc deps_table in
+ let dst_zone = Locations.(enumerate_valid_bits Write dst_loc) in
+ let sure_zone = if exact then dst_zone else Zone.bottom in
+ deps_table, Zone.join sure_zone sure_output
+
+(* Copy the offsetmap of size [size] from [src] to [dst] in [state]. *)
+let copy_offsetmap ~name ~exact ~size ~src ~dst ~dst_lval state =
+ match Cvalue.Model.copy_offsetmap src size state with
+ | `Bottom -> Cvalue.Model.bottom
+ | `Value offsetmap ->
+ check_indeterminate_offsetmap ~name offsetmap;
+ let prefix = "Builtin " ^ name in
+ Cvalue_transfer.warn_imprecise_offsm_write ~prefix dst_lval offsetmap;
+ Cvalue.Model.paste_offsetmap ~from:offsetmap ~dst_loc:dst ~size ~exact state
+
+(* Returns the min and max size of a copy from an Ival.t. *)
+let min_max_size size =
+ let min, max = Ival.min_and_max size in
+ let min = Option.fold min ~none:Int.zero ~some:Int.(max zero) in
+ let max_max = Bit_utils.max_bit_size () in
+ let max = Option.fold max ~none:max_max ~some:Int.(max zero) in
+ min, max
+
+(* Computes the remaining [src], [dst] and [size] to be copied after [factor]
+ bits have already been copied. *)
+let shift ~factor:i src dst size =
+ let new_size = Int.sub size i in
+ let ival = Ival.inject_singleton i in
+ let new_src = Location_Bits.shift ival src in
+ let new_dst = Location_Bits.shift ival dst in
+ new_src, new_dst, new_size
+
+(* Performs the remaining copy from [src] to [dst] for all other possible [size],
+ after the copy for the minimum size has already been done.
+ Iterates on all possible values of [size] (after the first), and does the
+ copy for [previous_size..size]. *)
+let copy_remaining_size_by_size ~name ~src ~dst ~dst_lval ~size state =
+ let exception Result of Cvalue.Model.t in
+ let do_size size (state, previous_size) =
+ (* First iteration: this copy has already been performed, skip. *)
+ if Int.(equal previous_size minus_one)
+ then state, size
+ else
+ (* Copy data between [previous_size] and [size]. *)
+ let src, dst, size = shift ~factor:previous_size src dst size in
+ (* [exact] is false as all these copies may not happen according to the
+ concrete value of [size]. *)
+ let exact = false in
+ let new_state = copy_offsetmap ~name ~exact ~size ~src ~dst ~dst_lval state in
+ (* If this copy failed, the current size is completely invalid, and so
+ will be the following ones. Stop now with the previous state. *)
+ if not (Cvalue.Model.is_reachable new_state) then raise (Result state);
+ new_state, size
+ in
+ try fst (Ival.fold_int do_size size (state, Int.minus_one))
+ with Result state -> state
+
+(* Copy the value at location [src_loc] to location [dst_loc] in [state]. *)
+let imprecise_copy ~name ~src_loc ~dst_loc ~dst_lval state =
+ Self.debug ~dkey ~once:true ~current:true
+ "In %s builtin: too many sizes to enumerate, possible loss of precision"
+ name;
+ (* conflate_bottom:false as we want to copy padding bits *)
+ let v = Model.find_indeterminate ~conflate_bottom:false state src_loc in
+ warn_indeterminate_value ~name v;
+ let value = Cvalue.V_Or_Uninitialized.get_v v in
+ let prefix = "Builtin " ^ name in
+ Cvalue_transfer.warn_imprecise_write ~prefix dst_lval dst_loc value;
+ let new_state =
+ Cvalue.Model.add_indeterminate_binding ~exact:false state dst_loc v
+ in
+ (* Beware that all sizes may be invalid, in which case [add_binding] will
+ return [bottom]. In this case, return the previously computed state *)
+ if Model.is_reachable new_state then new_state else state
+
+(* Creates the location {loc + [0..max_size-1]} of size char. *)
+let char_location loc max_size =
+ let size_char = Bit_utils.sizeofchar () in
+ let max = Int.sub max_size size_char in
+ (* Use ranges modulo char_bits to read and write byte-by-byte, which can
+ preserve some precision.*)
+ let shift =
+ Ival.inject_interval ~min:(Some Int.zero) ~max:(Some max)
+ ~rem:Int.zero ~modu:size_char
+ in
+ let loc = Location_Bits.shift shift loc in
+ make_loc loc (Int_Base.inject size_char)
+
+let compute_memcpy ~name ~dst_lval ~dst ~src ~size state =
+ let size_min, size_max = min_max_size size in
+ (* Empty \from dependencies and sure output *)
+ let empty_deps = Assigns.Memory.empty, Zone.bottom in
+ (* First step: copy the bits we are sure to copy, i.e. for the minimum size
+ [size_min] if it is not zero. *)
+ let state, (deps_table, written_zone) =
+ if Int.gt size_min Int.zero
+ then
+ let state =
+ copy_offsetmap ~name ~exact:true ~size:size_min ~src ~dst ~dst_lval state
+ in
+ (* If the copy succeeded, update \from dependencies and sure output. *)
+ if Cvalue.Model.is_reachable state
+ then state, add_sure_deps ~size:size_min ~src ~dst empty_deps
+ else state, empty_deps
+ else state, empty_deps
+ in
+ (* Stop here if the first copy failed or if there is nothing more to copy. *)
+ if not (Cvalue.Model.is_reachable state) || Int.equal size_min size_max
+ then state, deps_table, written_zone
+ else
+ (* Second step: size is imprecise, we will now copy some bits that we are
+ not sure to copy, for all possible sizes greater than [size_min]. *)
+ (* [size_min] bits have already been copied. *)
+ let src_shift, dst_shift, size_diff = shift ~factor:size_min src dst size_max in
+ (* Remaining locations to be read/written, as locations of char size. *)
+ let src_loc = char_location src_shift size_diff
+ and dst_loc = char_location dst_shift size_diff in
+ let deps_table = add_deps_loc ~exact:false ~src_loc ~dst_loc deps_table in
+ (* If there is sufficiently few possible sizes, iter on each possible size
+ via [copy_remaining_size_by_size]. Otherwise, use [imprecise_copy] in one
+ step to read the entire range src+(size_min..size_max-1) as one byte, and
+ write the result as one byte in dst+(size_min..size_max-1). *)
+ let state =
+ if Ival.cardinal_is_less_than size (plevel () / 10)
+ then copy_remaining_size_by_size ~name ~src ~dst ~dst_lval ~size state
+ else imprecise_copy ~name ~src_loc ~dst_loc ~dst_lval state
+ in
+ state, deps_table, written_zone
let frama_c_memcpy name state actuals =
- let prefix = "Builtin " ^ name in
- let compute (exp_dst,dst_bytes) (_exp_src,src_bytes) (_exp_size,size) =
- let dst_lval = lval_of_address exp_dst in
- let plevel = Parameters.ArrayPrecisionLevel.get() in
+ match actuals with
+ | [(dst_exp, dst_cvalue); (_src_exp, src_cvalue); (_size_exp, size_cvalue)] ->
+ let dst_lval = lval_of_address dst_exp in
let size =
- try Cvalue.V.project_ival size
+ try Cvalue.V.project_ival size_cvalue
with Cvalue.V.Not_based_on_null -> Ival.top (* TODO: use size_t *)
in
- let min,max = Ival.min_and_max size in
- let min = match min with None -> Int.zero | Some m -> Int.max m Int.zero in
- let char_bits = Bit_utils.sizeofchar() in
- let size_min = Int.mul char_bits min in
- let src = loc_bytes_to_loc_bits src_bytes in
- let dst = loc_bytes_to_loc_bits dst_bytes in
- (* Remove read-only destinations *)
- let dst_bits =
- Location_Bits.filter_base (fun b -> not (Base.is_read_only b)) dst
- in
- let deps_return = deps_nth_arg 0 in
- let empty_cfrom =
- Assigns.{ memory = Memory.empty; return = deps_return }
- in
- let precise_copy state =
- (* First step: copy the bytes we are sure to copy *)
- if Int.gt size_min Int.zero then begin
- match Cvalue.Model.copy_offsetmap src size_min state with
- | `Bottom -> (* Read failed. Source was invalid, but must be read, we
- stop the analysis *)
- raise (Memcpy_result (Cvalue.Model.bottom,empty_cfrom,Zone.bottom))
- | `Value offsetmap ->
- let loc_dst = make_loc dst_bits (Int_Base.inject size_min) in
- memcpy_check_indeterminate_offsetmap offsetmap;
- (* Read succeeded. We write the result *)
- let loc_src = make_loc src (Int_Base.inject size_min) in
- Cvalue_transfer.warn_imprecise_offsm_write ~prefix dst_lval offsetmap;
- let new_state =
- Cvalue.Model.paste_offsetmap
- ~from:offsetmap ~dst_loc:dst_bits ~size:size_min ~exact:true state
- in
- let (deps_table, sure_zone) =
- let zone_dst = enumerate_valid_bits Locations.Write loc_dst in
- let zone_src = enumerate_valid_bits Locations.Read loc_src in
- let deps = Deps.data zone_src in
- (* Note: actually a part may be written for sure (if the
- difference between the offsets in loc_dst is smaller
- than size), but keeping it imprecise reflects more the
- imprecision of the value analysis here. *)
- let exact = Location_Bits.cardinal_zero_or_one dst_bits in
- let deps_table =
- Assigns.Memory.add_binding ~exact
- Assigns.Memory.empty zone_dst deps
- in
- let sure_zone = if exact then zone_dst else Zone.bottom in
- (deps_table, sure_zone)
- in
- new_state, deps_table, sure_zone
- end
- else (* Nothing certain can be copied *)
- (state, Assigns.Memory.empty, Zone.bottom)
+ (* Convert locations and size into bits. *)
+ let size = Ival.scale (Bit_utils.sizeofchar ()) size in
+ let src = loc_bytes_to_loc_bits src_cvalue in
+ let dst = loc_bytes_to_loc_bits dst_cvalue in
+ (* Remove invalid locations. *)
+ let src = reduce_to_valid_loc src size Locations.Read in
+ let dst = reduce_to_valid_loc dst size Locations.Write in
+ (* Do the copy. *)
+ let state, memory, sure_output =
+ compute_memcpy ~name ~dst_lval ~dst ~src ~size state
in
- let imprecise_copy new_state precise_assigns sure_zone =
- (* Second step. Size is imprecise, we will now copy some bits
- that we are not sure to copy *)
- let size_min_ival = Ival.inject_singleton size_min in
- let dst = Location_Bits.shift size_min_ival dst_bits in
- let src = Location_Bits.shift size_min_ival src in
- (* Size remaining to copy imprecisely *)
- let diff = match max with
- | Some max -> Some (Int.mul char_bits (Int.pred (Int.sub max min)))
- | None -> None
- in
- (* Imprecise locations remaining to be read/written. By using ranges
- modulo char_bits, we read and write byte-by-byte, which can preserve
- some precision in the fallback. If sufficiently few sizes need
- to be copied, we use a more precise method (see do_size below).
- However, in all cases, those locations are used to compute the
- read and written bits. *)
- let range =
- Ival.inject_interval ~min:(Some Int.zero) ~max:diff
- ~rem:Int.zero ~modu:char_bits
- in
- let size_char = Int_Base.inject char_bits in
- let loc_src = make_loc (Location_Bits.shift range src) size_char in
- let loc_dst = make_loc (Location_Bits.shift range dst) size_char in
- let c_from =
- let zone_src = enumerate_valid_bits Locations.Read loc_src in
- let zone_dst = enumerate_valid_bits Locations.Write loc_dst in
- let deps = Deps.data zone_src in
- let memory =
- Assigns.Memory.add_binding ~exact:false precise_assigns zone_dst deps
- in
- Assigns.{ memory; return = deps_return }
- in
- try
- (* We try to iter on all the slices inside the value of slice.
- If there are more too many of them, we use a backup solution *)
- ignore (Ival.cardinal_less_than size (plevel / 10));
- let do_size s (dst, src, prev_size, state) =
- let s = Int.mul char_bits s in
- let diff = Int.sub s prev_size in
- if Int.equal s size_min then
- (* occurs the very first time. This copy has already been
- performed at the beginning, skip *)
- (dst, src, s, state)
- else begin
- (* Copy data between prev_size and s *)
- match Cvalue.Model.copy_offsetmap src diff state with
- | `Bottom ->
- (* This size is completely invalid. The following ones
- will also be invalid, stop now with current result *)
- raise (Memcpy_result (state,c_from,sure_zone))
- | `Value offsetmap ->
- memcpy_check_indeterminate_offsetmap offsetmap;
- Cvalue_transfer.warn_imprecise_offsm_write ~prefix dst_lval offsetmap;
- let new_state =
- Cvalue.Model.paste_offsetmap
- ~from:offsetmap ~dst_loc:dst ~size:diff ~exact:false state
- in
- if Cvalue.Model.is_reachable new_state then
- let diffi = Ival.inject_singleton diff in
- let dst = Location_Bits.shift diffi dst in
- let src = Location_Bits.shift diffi src in
- (dst, src, s, new_state)
- else (* As above, invalid size, this time for the destination.
- We stop there *)
- raise (Memcpy_result (state,c_from,sure_zone))
- end
- in
- let _, _, _, state =
- Ival.fold_int do_size size (dst, src, Int.zero, new_state)
- in
- raise (Memcpy_result (state,c_from,sure_zone))
- with
- | Abstract_interp.Not_less_than ->
- Self.debug ~dkey ~once:true
- ~current:true "In memcpy builtin: too many sizes to enumerate, \
- possible loss of precision";
- (* Too many slices in the size. We read the entire range
- src+(size_min..size_max-1) in one step, as one byte, and write the
- result as one byte in dst+(size_min..size_max-1) *)
- let v = (* conflate_bottom=false: we want to copy padding bits *)
- Model.find_indeterminate ~conflate_bottom:false state loc_src
- in
- begin match v with
- | V_Or_Uninitialized.C_init_noesc _ -> ()
- | _ -> Self.result ~dkey ~current:true ~once:true
- "@[In memcpy@ builtin:@ imprecise@ copy of@ indeterminate@ values@]%t"
- Eva_utils.pp_callstack
- end;
- let value = Cvalue.V_Or_Uninitialized.get_v v in
- Cvalue_transfer.warn_imprecise_write ~prefix dst_lval loc_dst value;
- let updated_state =
- Cvalue.Model.add_indeterminate_binding
- ~exact:false new_state loc_dst v
- in
- (* Beware that all the imprecise sizes may be invalid, in which case
- [add_binding] will return [Bottom]. In this case, return the
- previously computed state *)
- if Model.is_reachable updated_state then
- raise (Memcpy_result (updated_state,c_from,sure_zone))
- else
- raise (Memcpy_result (new_state,c_from,sure_zone))
- in
- try
- if Ival.is_zero size then
- raise (Memcpy_result (state, empty_cfrom, Zone.bottom));
- let (precise_state,precise_assigns,sure_zone) = precise_copy state in
- if Option.fold ~none:false ~some:(Int.equal min) max then
- begin
- let c_assigns =
- Assigns.{ memory = precise_assigns; return = deps_return }
- in
- raise (Memcpy_result (precise_state, c_assigns, sure_zone))
- end;
- imprecise_copy precise_state precise_assigns sure_zone
- with
- | Memcpy_result (new_state,c_assigns,sure_zone) ->
- if Model.is_reachable new_state then
- (* Copy at least partially succeeded (with perhaps an
- alarm for some of the sizes *)
- Builtins.Full
- { Builtins.c_values = [Some dst_bytes, new_state];
- c_clobbered = Builtins.clobbered_set_from_ret new_state dst_bytes;
- c_assigns = Some (c_assigns, sure_zone); }
+ (* Build the builtin results. *)
+ let return = deps_nth_arg 0 in
+ let froms = Assigns.{ memory; return } in
+ let c_assigns = Some (froms, sure_output) in
+ let return, c_clobbered =
+ if Model.is_reachable state then
+ (* Copy at least partially succeeded *)
+ Some dst_cvalue, Builtins.clobbered_set_from_ret state dst_cvalue
else
- Builtins.Full
- { Builtins.c_values = [ None, Cvalue.Model.bottom];
- c_clobbered = Base.SetLattice.bottom;
- c_assigns = Some (c_assigns, sure_zone); }
- in
- match actuals with
- | [dst; src; size] -> compute dst src size
+ None, Base.SetLattice.bottom
+ in
+ Builtins.Full { c_values = [ return, state ]; c_clobbered; c_assigns }
| _ -> raise (Builtins.Invalid_nb_of_args 3)
let () =
register_builtin ~replace:"memcpy" "Frama_C_memcpy" (frama_c_memcpy "memcpy");
register_builtin ~replace:"memmove" "Frama_C_memmove" (frama_c_memcpy "memmove")
+(* -------------------------------------------------------------------------- *)
+(* Memset *)
+(* -------------------------------------------------------------------------- *)
+
(* Implementation of [memset] that accepts imprecise arguments. *)
let frama_c_memset_imprecise state dst_lval dst v size =
let prefix = "Builtin memset" in
- let size_char = Bit_utils.sizeofchar () in
- let size_min, size_max_bytes =
- try
- let size = Cvalue.V.project_ival size in
- let min,max = Ival.min_and_max size in
- let min = match min with
- | None -> Int.zero
- | Some m -> Int.mul size_char (Int.max m Int.zero)
- and max = match max with
- | None -> Bit_utils.max_bit_address ()
- | Some m -> m
- in min, max
- with V.Not_based_on_null -> Int.zero, Bit_utils.max_bit_address ()
- in
- let left = loc_bytes_to_loc_bits dst in
+ let size_min, size_max = min_max_size size in
(* Write [v] everywhere that might be written, ie between
[dst] and [dst+size-1]. *)
- let (new_state,over_zone) =
- if Int.gt size_max_bytes Int.zero then
- let shift =
- Ival.inject_range (Some Int.zero) (Some (Int.pred size_max_bytes))
- in
- let loc = Location_Bytes.shift shift dst in
- let loc = loc_bytes_to_loc_bits loc in
- let loc = make_loc loc (Int_Base.inject size_char) in
+ let state, over_zone =
+ if Int.gt size_max Int.zero then
+ let loc = char_location dst size_max in
Cvalue_transfer.warn_imprecise_write ~prefix dst_lval loc v;
let state = Cvalue.Model.add_binding ~exact:false state loc v in
- (state,enumerate_valid_bits Locations.Write loc)
- else (state,Zone.bottom)
+ let written_zone = enumerate_valid_bits Locations.Write loc in
+ state, written_zone
+ else state, Zone.bottom
in
(* Write "sure" bytes in an exact way: they exist only if there is only
one base, and within it, size_min+leftmost_loc > rightmost_loc *)
- let (new_state',sure_zone) =
+ let state, sure_zone =
try
- let base, offset = Location_Bits.find_lonely_key left in
+ let base, offset = Location_Bits.find_lonely_key dst in
let minb, maxb = match Ival.min_and_max offset with
| Some minb, Some maxb -> minb, maxb
| _ -> raise Not_found
in
let sure = Int.sub (Int.add minb size_min) maxb in
if Int.gt sure Int.zero then
- let left' = Location_Bits.inject base (Ival.inject_singleton maxb) in
+ let dst_loc = Location_Bits.inject base (Ival.inject_singleton maxb) in
let vuninit = V_Or_Uninitialized.initialized v in
- let from = V_Offsetmap.create ~size:sure vuninit ~size_v:size_char in
+ let size_v = Bit_utils.sizeofchar () in
+ let from = V_Offsetmap.create ~size:sure vuninit ~size_v in
Cvalue_transfer.warn_imprecise_offsm_write ~prefix dst_lval from;
let state =
Cvalue.Model.paste_offsetmap
- ~from ~dst_loc:left' ~size:sure ~exact:true new_state
+ ~from ~dst_loc ~size:sure ~exact:true state
in
- let sure_loc = make_loc left' (Int_Base.inject sure) in
+ let sure_loc = make_loc dst_loc (Int_Base.inject sure) in
let sure_zone = enumerate_valid_bits Locations.Write sure_loc in
- (state,sure_zone)
+ state, sure_zone
else
- (new_state,Zone.bottom)
- with Not_found -> (new_state,Zone.bottom) (* from find_lonely_key + explicit raise *)
- in
- let c_assigns =
- let value_dep = deps_nth_arg 1 in
- let memory = Assigns.Memory.empty in
- let memory =
- Assigns.Memory.add_binding ~exact:false memory over_zone value_dep
- in
- let memory =
- Assigns.Memory.add_binding ~exact:true memory sure_zone value_dep
- in
- let deps_return = deps_nth_arg 0 in
- Assigns.{ memory; return = deps_return }
+ state, Zone.bottom
+ with Not_found -> state, Zone.bottom (* from find_lonely_key + explicit raise *)
in
- Builtins.Full
- { Builtins.c_values = [Some dst, new_state'];
- c_clobbered = Base.SetLattice.bottom;
- c_assigns = Some (c_assigns,sure_zone); }
-(* let () = register_builtin "Frama_C_memset" frama_c_memset_imprecise *)
+ state, sure_zone, over_zone
(* Type that describes why the 'precise memset' builtin may fail. *)
type imprecise_memset_reason =
@@ -394,23 +316,15 @@ type imprecise_memset_reason =
exception ImpreciseMemset of imprecise_memset_reason
-let pretty_imprecise_memset_reason fmt = function
- | UnsupportedType ->
- Format.pp_print_string fmt "destination has an unknown type"
- | ImpreciseTypeSize ->
- Format.pp_print_string fmt "destination has a type with unknown size"
- | NoTypeForDest ->
- Format.pp_print_string fmt "destination has an unknown form"
- | NotSingletonLoc ->
- Format.pp_print_string fmt "destination is not exact"
- | SizeMismatch ->
- Format.pp_print_string fmt "destination type and size differ"
- | ImpreciseValue ->
- Format.pp_print_string fmt "value to write is imprecise"
- | ImpreciseSize ->
- Format.pp_print_string fmt "size is imprecise"
- | NegativeOrNullSize ->
- Format.pp_print_string fmt "size is negative or null"
+let imprecision_descr = function
+ | UnsupportedType -> "destination has an unknown type"
+ | ImpreciseTypeSize -> "destination has a type with unknown size"
+ | NoTypeForDest -> "destination has an unknown form"
+ | NotSingletonLoc -> "destination is not exact"
+ | SizeMismatch -> "destination type and size differ"
+ | ImpreciseValue -> "value to write is imprecise"
+ | ImpreciseSize -> "size is imprecise"
+ | NegativeOrNullSize -> "size is negative or null"
(* [memset_typ_offsm typ i] returns an offsetmap of size [sizeof(typ)]
@@ -539,14 +453,11 @@ let memset_typ_offsm typ v =
precise abstract values. *)
let frama_c_memset_precise state dst_lval dst v (exp_size, size) =
try
- let size_char = Bit_utils.sizeofchar () in
(* We want an exact size, Otherwise, we can use the imprecise memset as a
fallback *)
- let isize = V.project_ival size in
- let size = Ival.project_int isize in
- let size_bits = Integer.mul size_char size in
+ let size = Ival.project_int size in
(* Extract the location, check that it is precise. *)
- if Location_Bytes.(is_bottom dst || not (cardinal_zero_or_one dst)) then
+ if Location_Bits.(is_bottom dst || not (cardinal_zero_or_one dst)) then
raise (ImpreciseMemset NotSingletonLoc);
if not (Int.gt size Int.zero) then
raise (ImpreciseMemset NegativeOrNullSize);
@@ -564,39 +475,22 @@ let frama_c_memset_precise state dst_lval dst v (exp_size, size) =
| None ->
(* No such luck. Use the base and the offset of [dst] to resynthesize
a type *)
- let base_dst, offset_dst = Location_Bytes.find_lonely_binding dst in
- let offset_dst = Ival.project_int offset_dst in
- let offset_dst_bits = Int.mul offset_dst size_char in
+ let base_dst, offset_dst = Location_Bits.find_lonely_binding dst in
+ let offset = Ival.project_int offset_dst in
let vi_dst = Base.to_varinfo base_dst in
- let mo = Bit_utils.MatchSize size_bits in
- snd (Bit_utils.(find_offset vi_dst.vtype ~offset:offset_dst_bits mo))
+ let mo = Bit_utils.MatchSize size in
+ snd (Bit_utils.(find_offset vi_dst.vtype ~offset mo))
in
let offsm = memset_typ_offsm typ v in
- let dst_loc = Locations.loc_bytes_to_loc_bits dst in
- let (c_from,dst_zone) =
- let input = deps_nth_arg 1 in
- let size_bits = Integer.mul size (Bit_utils.sizeofchar ())in
- let dst_location = Locations.make_loc dst_loc (Int_Base.Value size_bits) in
- let dst_zone = Locations.(enumerate_valid_bits Write dst_location) in
- let memory =
- Assigns.Memory.add_binding ~exact:true
- Assigns.Memory.empty dst_zone input
- in
- let return = deps_nth_arg 0 in
- let c_from = Assigns.{ memory; return } in
- c_from,dst_zone
- in
- let _ = c_from in
let prefix = "Builtin memset" in
Cvalue_transfer.warn_imprecise_offsm_write ~prefix dst_lval offsm;
- let state' =
+ let state =
Cvalue.Model.paste_offsetmap
- ~from:offsm ~dst_loc ~size:size_bits ~exact:true state
+ ~from:offsm ~dst_loc:dst ~size ~exact:true state
in
- Builtins.Full
- { Builtins.c_values = [Some dst, state'];
- c_clobbered = Base.SetLattice.bottom;
- c_assigns = Some (c_from,dst_zone); }
+ let dst_location = Locations.make_loc dst (Int_Base.Value size) in
+ let dst_zone = Locations.(enumerate_valid_bits Write dst_location) in
+ state, dst_zone, dst_zone
with
| Bit_utils.NoMatchingOffset -> raise (ImpreciseMemset SizeMismatch)
| Base.Not_a_C_variable -> raise (ImpreciseMemset NoTypeForDest)
@@ -608,11 +502,18 @@ let frama_c_memset_precise state dst_lval dst v (exp_size, size) =
let frama_c_memset state actuals =
match actuals with
- | [(exp_dst, dst); (_, v); (exp_size, size)] ->
+ | [(dst_exp, dst_cvalue); (_, v); (exp_size, size_cvalue)] ->
begin
- let dst_lval = lval_of_address exp_dst in
+ let dst_lval = lval_of_address dst_exp in
+ let size =
+ try Cvalue.V.project_ival size_cvalue
+ with Cvalue.V.Not_based_on_null -> Ival.top (* TODO: use size_t *)
+ in
+ (* Convert locations and size into bits. *)
+ let size = Ival.scale (Bit_utils.sizeofchar ()) size in
+ let dst = Locations.loc_bytes_to_loc_bits dst_cvalue in
(* Remove read-only destinations *)
- let dst = V.filter_base (fun b -> not (Base.is_read_only b)) dst in
+ let dst = reduce_to_valid_loc dst size Locations.Write in
(* Keep only the first byte of the value argument *)
let _, v = Cvalue.V.extract_bits
~topify:Origin.Misalign_read
@@ -620,18 +521,78 @@ let frama_c_memset state actuals =
~size:(Int.of_int (Cil.bitsSizeOfInt IInt))
v
in
- try frama_c_memset_precise state dst_lval dst v (exp_size, size)
- with ImpreciseMemset reason ->
- Self.debug ~dkey ~current:true
- "Call to builtin precise_memset(%a) failed; %a%t"
- Eva_utils.pretty_actuals actuals pretty_imprecise_memset_reason reason
- Eva_utils.pp_callstack;
- frama_c_memset_imprecise state dst_lval dst v size
+ let state, sure_output, over_output =
+ try frama_c_memset_precise state dst_lval dst v (exp_size, size)
+ with ImpreciseMemset reason ->
+ Self.debug ~dkey ~current:true
+ "Call to builtin precise_memset(%a) failed; %s%t"
+ Eva_utils.pretty_actuals actuals (imprecision_descr reason)
+ Eva_utils.pp_callstack;
+ frama_c_memset_imprecise state dst_lval dst v size
+ in
+ let assigns =
+ let value_dep = deps_nth_arg 1 in
+ let memory = Assigns.Memory.empty in
+ let memory =
+ Assigns.Memory.add_binding ~exact:false memory over_output value_dep
+ in
+ let memory =
+ Assigns.Memory.add_binding ~exact:true memory sure_output value_dep
+ in
+ let return = deps_nth_arg 0 in
+ Assigns.{ memory; return }
+ in
+ Builtins.Full
+ { Builtins.c_values = [ Some dst_cvalue, state ];
+ c_clobbered = Base.SetLattice.bottom;
+ c_assigns = Some (assigns, sure_output); }
end
| _ -> raise (Builtins.Invalid_nb_of_args 3)
let () = register_builtin ~replace:"memset" "Frama_C_memset" frama_c_memset
+(* -------------------------------------------------------------------------- *)
+(* is_base_aligned, offset, split, ungarbled *)
+(* -------------------------------------------------------------------------- *)
+
+let frama_C_is_base_aligned _state = function
+ | [_, x; _, y] ->
+ let result =
+ match Ival.project_small_set (Cvalue.V.project_ival y) with
+ | Some si ->
+ let aligned =
+ Location_Bytes.for_all
+ (fun b _o -> List.for_all (Base.is_aligned_by b) si)
+ x
+ in
+ if aligned then Cvalue.V.singleton_one else Cvalue.V.zero_or_one
+ | None
+ | exception Cvalue.V.Not_based_on_null -> Cvalue.V.zero_or_one
+ in
+ Builtins.Result [result]
+ | _ -> raise (Builtins.Invalid_nb_of_args 2)
+
+let () = register_builtin "Frama_C_is_base_aligned" frama_C_is_base_aligned
+
+
+let frama_c_offset _state = function
+ | [_, x] ->
+ let result =
+ try
+ let acc = Ival.bottom in
+ let offsets = Location_Bytes.fold_i (fun _b -> Ival.join) x acc in
+ Cvalue.V.inject_ival offsets
+ with Abstract_interp.Error_Top ->
+ Self.error ~current:true
+ "Builtin Frama_C_offset is applied to a value not \
+ guaranteed to be an address";
+ Cvalue.V.top_int
+ in
+ Builtins.Result [result]
+ | _ -> raise (Builtins.Invalid_nb_of_args 1)
+
+let () = register_builtin "Frama_C_offset" frama_c_offset
+
let frama_c_interval_split _state actuals =
match actuals with
| [_,lower; _,upper] ->
diff --git a/tests/builtins/memset.c b/tests/builtins/memset.c
index f239d66f3e21ae580447d945b094c751ce191ac2..9c537d24550636043bb34e9e7001e9820bcf01ea 100644
--- a/tests/builtins/memset.c
+++ b/tests/builtins/memset.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: #"-calldeps -eva-msg-key imprecision -eva-plevel 500" +"-inout -no-deps"
+ STDOPT: #"-calldeps -eva-msg-key imprecision -eva-plevel 500 -absolute-valid-range 0x10-0xf0" +"-inout -no-deps"
*/
#include "string.h"
@@ -26,7 +26,7 @@ struct s {
};
struct s ts[5];
-
+extern struct incomplete *incomplete_type;
volatile int vol;
void test() {
@@ -44,7 +44,7 @@ void test() {
memset(p, 0x22, 16); // multiple dest
p = vol ? (char*) 0 : t8;
- memset(p, 0x22, 16); // one valid dest; TODO
+ memset(p, 0x22, 16); // one valid dest;
p = t9+20;
while (1) {
@@ -70,6 +70,11 @@ void test() {
unsigned k = vol;
//@ assert Assume: k <= 12;
memset(t12+k*8, 1, 4); // Imprecise, because of double congruences
+
+ memset(t1, 1, 0); // size is negative or null
+ memset(incomplete_type, 'A', 1); // destination type and size differ
+ char *absolute_valid_range = (char*)0x10;
+ memset(absolute_valid_range, 'B', 2); // destination has an unknown form
}
/* Should not crash and emit uninitialization alarms.
diff --git a/tests/builtins/oracle/memcpy.res.oracle b/tests/builtins/oracle/memcpy.res.oracle
index 1559794a477915a5ad20d5b9232252094712ec3f..2d5891583c8722e65411a6358aaac05cd5295ef9 100644
--- a/tests/builtins/oracle/memcpy.res.oracle
+++ b/tests/builtins/oracle/memcpy.res.oracle
@@ -121,8 +121,6 @@
function memcpy: precondition 'valid_dest' got status unknown.
[eva] memcpy.c:89: function memcpy: precondition 'valid_src' got status valid.
[eva] memcpy.c:89: function memcpy: precondition 'separation' got status valid.
-[kernel] memcpy.c:89:
- writing somewhere in {NULL; v4} because of Arithmetic {memcpy.c:89}.
[eva:alarm] memcpy.c:90: Warning:
pointer downcast. assert (unsigned int)((struct t1 *)t) ≤ 2147483647;
[eva:alarm] memcpy.c:91: Warning:
@@ -135,8 +133,6 @@
function memcpy: precondition 'valid_dest' got status unknown.
[eva] memcpy.c:91: function memcpy: precondition 'valid_src' got status valid.
[eva] memcpy.c:91: function memcpy: precondition 'separation' got status valid.
-[kernel] memcpy.c:91:
- writing somewhere in {NULL; v5} because of Arithmetic {memcpy.c:91}.
[eva] memcpy.c:96: Call to builtin memcpy
[eva:alarm] memcpy.c:96: Warning:
function memcpy: precondition 'valid_dest' got status unknown.
@@ -220,7 +216,7 @@
[eva] memcpy.c:172: function memcpy: precondition 'valid_src' got status valid.
[eva] memcpy.c:172: function memcpy: precondition 'separation' got status valid.
[eva:imprecision] memcpy.c:172:
- In memcpy builtin: precise copy of indeterminate values UNINITIALIZED
+ In memcpy builtin: precise copy of indeterminate values.
[eva] memcpy.c:173: assertion got status valid.
[eva] computing for function itv <- main_uninit <- main_all.
Called from memcpy.c:174.
@@ -233,7 +229,7 @@
[eva:imprecision] memcpy.c:174:
In memcpy builtin: too many sizes to enumerate, possible loss of precision
[eva:imprecision] memcpy.c:174:
- In memcpy builtin: imprecise copy of indeterminate values
+ In memcpy builtin: imprecise copy of indeterminate values.
[eva] memcpy.c:175: assertion got status valid.
[eva] computing for function make_unknown <- main_uninit <- main_all.
Called from memcpy.c:178.
@@ -255,7 +251,7 @@
[eva:imprecision] memcpy.c:181:
In memcpy builtin: too many sizes to enumerate, possible loss of precision
[eva:imprecision] memcpy.c:181:
- In memcpy builtin: imprecise copy of indeterminate values
+ In memcpy builtin: imprecise copy of indeterminate values.
[eva:alarm] memcpy.c:182: Warning:
accessing uninitialized left-value. assert \initialized(&b[11]);
[eva] computing for function make_unknown <- main_uninit <- main_all.
@@ -267,7 +263,7 @@
[eva] memcpy.c:187: function memcpy: precondition 'valid_src' got status valid.
[eva] memcpy.c:187: function memcpy: precondition 'separation' got status valid.
[eva:imprecision] memcpy.c:187:
- In memcpy builtin: precise copy of indeterminate values UNINITIALIZED
+ In memcpy builtin: precise copy of indeterminate values.
[eva] memcpy.c:188: assertion got status valid.
[eva] computing for function itv <- main_uninit <- main_all.
Called from memcpy.c:190.
@@ -279,7 +275,7 @@
[eva:imprecision] memcpy.c:190:
In memcpy builtin: too many sizes to enumerate, possible loss of precision
[eva:imprecision] memcpy.c:190:
- In memcpy builtin: imprecise copy of indeterminate values
+ In memcpy builtin: imprecise copy of indeterminate values.
[eva] memcpy.c:191: assertion got status valid.
[eva:alarm] memcpy.c:192: Warning:
accessing uninitialized left-value. assert \initialized(&b[8]);
@@ -306,7 +302,7 @@
[eva:imprecision] memcpy.c:200:
In memcpy builtin: too many sizes to enumerate, possible loss of precision
[eva:imprecision] memcpy.c:200:
- In memcpy builtin: imprecise copy of indeterminate values
+ In memcpy builtin: imprecise copy of indeterminate values.
[eva:alarm] memcpy.c:201: Warning:
accessing uninitialized left-value. assert \initialized(&b[11]);
[eva] Recording results for main_uninit
@@ -577,10 +573,19 @@
.y ∈ {7}
{.p; .padding[0..23]} ∈ {0}
v3 ∈ {{ garbled mix of &{v1} (origin: Misaligned read {memcpy.c:87}) }}
- v4.x ∈ [--..--]
+ v4.x[bits 0 to 7]# ∈ {0; 5}%32, bits 0 to 7
+ .x[bits 8 to 31] ∈ [--..--]
.y ∈ {{ (int)&t }}
- {.p; .padding[0..23]} ∈ [--..--]
- v5 ∈ {{ garbled mix of &{t} (origin: Misaligned read {memcpy.c:91}) }}
+ {.p; .padding[0..14]} ∈ [--..--]
+ .padding[15]# ∈ {0; 7}%32, bits 24 to 31
+ .padding[16..23] ∈ {0}
+ v5.x[bits 0 to 7]# ∈ {0; 5}%32, bits 0 to 7
+ .x[bits 8 to 31] ∈ [--..--]
+ .y[bits 0 to 7]# ∈ {{ NULL + [--..--] ; (? *)&t }}%32, bits 0 to 7
+ {.y[bits 8 to 31]; .p; .padding[0..14]} ∈
+ {{ garbled mix of &{t} (origin: Merge {memcpy.c:91}) }}
+ .padding[15]# ∈ {{ NULL + [--..--] ; (? *)&t }}%32, bits 24 to 31
+ .padding[16..23] ∈ [--..--]
t{[0]; [1]{.x; .y}} ∈ {0}
[1].p ∈ {{ &v1.y }}
{[1].padding[0..23]; [2]; [3]{.x; .y}} ∈ {0}
diff --git a/tests/builtins/oracle/memset.res.oracle b/tests/builtins/oracle/memset.res.oracle
index a6115d361b6b54206f7f038fd794ce01df915472..f8bbb7519d819bd62c5c137bd158eadb4393d62a 100644
--- a/tests/builtins/oracle/memset.res.oracle
+++ b/tests/builtins/oracle/memset.res.oracle
@@ -4,8 +4,15 @@
'char' and 'int')
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
+[eva:initial-state]
+ creating variable S_incomplete_type with imprecise size (type struct incomplete [2])
+[eva:unknown-size] memset.c:29: Warning:
+ during initialization of variable 'incomplete_type', size of
+ type 'struct incomplete' cannot be computed
+ (abstract type 'struct incomplete')
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
+ NULL[rbits 128 to 1927] ∈ [--..--]
t1[0..99] ∈ {0}
t2[0..99] ∈ {0}
t3[0..99] ∈ {0}
@@ -19,9 +26,11 @@
t11[0..99] ∈ {0}
t12[0..99] ∈ {0}
ts[0..4] ∈ {0}
+ incomplete_type ∈ {{ NULL ; (struct incomplete *)&S_incomplete_type }}
vol ∈ [--..--]
+ S_incomplete_type[bits 0 to ..] ∈ [--..--] or UNINITIALIZED
[eva] computing for function test <- main.
- Called from memset.c:88.
+ Called from memset.c:93.
[eva] memset.c:33: Call to builtin memset
[eva] memset.c:33: function memset: precondition 'valid_s' got status valid.
[eva] FRAMAC_SHARE/libc/string.h:134:
@@ -33,10 +42,6 @@
[eva] memset.c:34: Call to builtin memset
[eva:alarm] memset.c:34: Warning:
function memset: precondition 'valid_s' got status unknown.
-[eva:imprecision] memset.c:34:
- Call to builtin precise_memset(({{ garbled mix of &{t2}
- (origin: Arithmetic {memset.c:34}) }},
- {18},{400})) failed; destination is not exact
[eva] memset.c:35: Call to builtin memset
[eva:alarm] memset.c:35: Warning:
function memset: precondition 'valid_s' got status unknown.
@@ -62,8 +67,6 @@
[eva] memset.c:47: Call to builtin memset
[eva:alarm] memset.c:47: Warning:
function memset: precondition 'valid_s' got status unknown.
-[eva:imprecision] memset.c:47:
- Call to builtin precise_memset(({{ NULL ; (void *)&t8 }},{34},{16})) failed; destination is not exact
[eva] memset.c:50: starting to merge loop iterations
[eva] memset.c:54: Call to builtin memset
[eva:alarm] memset.c:54: Warning:
@@ -85,18 +88,32 @@
[eva] memset.c:72: function memset: precondition 'valid_s' got status valid.
[eva:imprecision] memset.c:72:
Call to builtin precise_memset(({{ &t12 + [0..384],0%32 }},{1},{4})) failed; destination is not exact
+[eva] memset.c:74: Call to builtin memset
+[eva] memset.c:74: function memset: precondition 'valid_s' got status valid.
+[eva:imprecision] memset.c:74:
+ Call to builtin precise_memset(({{ (void *)&t1 }},{1},{0})) failed; size is negative or null
+[eva] memset.c:75: Call to builtin memset
+[eva:alarm] memset.c:75: Warning:
+ function memset: precondition 'valid_s' got status unknown.
+[eva:imprecision] memset.c:75:
+ Call to builtin precise_memset(({{ NULL ; (void *)&S_incomplete_type }},
+ {65},{1})) failed; destination type and size differ
+[eva] memset.c:77: Call to builtin memset
+[eva] memset.c:77: function memset: precondition 'valid_s' got status valid.
+[eva:imprecision] memset.c:77:
+ Call to builtin precise_memset(({16},{66},{2})) failed; destination has an unknown form
[eva] Recording results for test
[from] Computing for function test
[from] Done for function test
[eva] Done for function test
[eva] computing for function uninit <- main.
- Called from memset.c:89.
-[eva:alarm] memset.c:80: Warning:
+ Called from memset.c:94.
+[eva:alarm] memset.c:85: Warning:
accessing uninitialized left-value. assert \initialized(&x);
-[eva:alarm] memset.c:84: Warning:
+[eva:alarm] memset.c:89: Warning:
accessing uninitialized left-value. assert \initialized(&x);
-[eva] memset.c:84: Call to builtin memset
-[eva] memset.c:84: function memset: precondition 'valid_s' got status valid.
+[eva] memset.c:89: Call to builtin memset
+[eva] memset.c:89: function memset: precondition 'valid_s' got status valid.
[eva] Recording results for uninit
[from] Computing for function uninit
[from] Done for function uninit
@@ -105,11 +122,13 @@
[from] Computing for function main
[from] Done for function main
[eva] Done for function main
-[eva] memset.c:80: assertion 'Eva,initialization' got final status invalid.
+[eva] memset.c:85: assertion 'Eva,initialization' got final status invalid.
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function test:
+ NULL[rbits 128 to 143] ∈ {66} repeated %8
+ [rbits 144 to 1927] ∈ [--..--]
t1[0..99] ∈ {286331153}
- t2[0..99] ∈ [--..--]
+ t2[0..99] ∈ {303174162}
t3[0..9] ∈ {0}
[10..99]# ∈ {0; 17} repeated %8
t4[0..99] ∈ {0}
@@ -120,7 +139,7 @@
[14..99] ∈ {0}
t7[0..3]# ∈ {0; 34} repeated %8
[4..99] ∈ {0}
- t8[0..3]# ∈ {0; 34} repeated %8
+ t8[0..3] ∈ {572662306}
[4..99] ∈ {0}
t9[0..19] ∈ {0}
[20..99]# ∈ {0; 254} repeated %8
@@ -160,12 +179,17 @@
s ∈ {12; 36}
s1 ∈ {8; 16}
k ∈ [0..12]
+ absolute_valid_range ∈ {16}
+ S_incomplete_type[bits 0 to 7] ∈ {65}
+ [bits 8 to ..] ∈ [--..--] or UNINITIALIZED
[eva:final-states] Values at end of function uninit:
x ∈ {{ (void *)&a }}
a ∈ {0}
[eva:final-states] Values at end of function main:
+ NULL[rbits 128 to 143] ∈ {66} repeated %8
+ [rbits 144 to 1927] ∈ [--..--]
t1[0..99] ∈ {286331153}
- t2[0..99] ∈ [--..--]
+ t2[0..99] ∈ {303174162}
t3[0..9] ∈ {0}
[10..99]# ∈ {0; 17} repeated %8
t4[0..99] ∈ {0}
@@ -176,7 +200,7 @@
[14..99] ∈ {0}
t7[0..3]# ∈ {0; 34} repeated %8
[4..99] ∈ {0}
- t8[0..3]# ∈ {0; 34} repeated %8
+ t8[0..3] ∈ {572662306}
[4..99] ∈ {0}
t9[0..19] ∈ {0}
[20..99]# ∈ {0; 254} repeated %8
@@ -211,12 +235,14 @@
[4].[bits 8 to 15] ∈ {0; 254}
[4].f2 ∈ {-258; 0}
[4]{.f3; .f4[0..2]} ∈ {-16843010; 0}
+ S_incomplete_type[bits 0 to 7] ∈ {65}
+ [bits 8 to ..] ∈ [--..--] or UNINITIALIZED
[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
[from] call to memset at memset.c:33 (by test):
t1[0..99] FROM c
\result FROM s
[from] call to memset at memset.c:34 (by test):
- t2[0..99] FROM c (and SELF)
+ t2[0..99] FROM c
\result FROM s
[from] call to memset at memset.c:35 (by test):
t3[10..99] FROM c (and SELF)
@@ -232,7 +258,7 @@
t7[0..3] FROM c (and SELF)
\result FROM s
[from] call to memset at memset.c:47 (by test):
- t8[0..3] FROM c (and SELF)
+ t8[0..3] FROM c
\result FROM s
[from] call to memset at memset.c:54 (by test):
t9[20..99] FROM c (and SELF)
@@ -251,18 +277,27 @@
[from] call to memset at memset.c:72 (by test):
t12[0..96] FROM c (and SELF)
\result FROM s
-[from] call to memset at memset.c:84 (by uninit):
+[from] call to memset at memset.c:74 (by test):
+ \result FROM s
+[from] call to memset at memset.c:75 (by test):
+ S_incomplete_type[bits 0 to 7] FROM c
+ \result FROM s
+[from] call to memset at memset.c:77 (by test):
+ NULL[16..17] FROM c
+ \result FROM s
+[from] call to memset at memset.c:89 (by uninit):
a FROM c
\result FROM s
-[from] call to test at memset.c:88 (by main):
+[from] call to test at memset.c:93 (by main):
+ NULL[16..17] FROM \nothing
t1[0..99] FROM \nothing
- t2[0..99] FROM \nothing (and SELF)
+ t2[0..99] FROM \nothing
t3[10..99] FROM \nothing (and SELF)
t4[1..99] FROM vol (and SELF)
t5[0..99] FROM \nothing
t6[10..13] FROM \nothing (and SELF)
t7[0..3] FROM \nothing (and SELF)
- t8[0..3] FROM \nothing (and SELF)
+ t8[0..3] FROM \nothing
t9[20..99] FROM \nothing (and SELF)
t10[4..6] FROM \nothing
[7..12] FROM \nothing (and SELF)
@@ -270,17 +305,19 @@
[3] FROM \nothing
t12[0..96] FROM \nothing (and SELF)
ts[0..4] FROM vol (and SELF)
-[from] call to uninit at memset.c:89 (by main):
+ S_incomplete_type[bits 0 to 7] FROM \nothing
+[from] call to uninit at memset.c:94 (by main):
NO EFFECTS
[from] entry point:
+ NULL[16..17] FROM \nothing
t1[0..99] FROM \nothing
- t2[0..99] FROM \nothing (and SELF)
+ t2[0..99] FROM \nothing
t3[10..99] FROM \nothing (and SELF)
t4[1..99] FROM vol (and SELF)
t5[0..99] FROM \nothing
t6[10..13] FROM \nothing (and SELF)
t7[0..3] FROM \nothing (and SELF)
- t8[0..3] FROM \nothing (and SELF)
+ t8[0..3] FROM \nothing
t9[20..99] FROM \nothing (and SELF)
t10[4..6] FROM \nothing
[7..12] FROM \nothing (and SELF)
@@ -288,20 +325,24 @@
[3] FROM \nothing
t12[0..96] FROM \nothing (and SELF)
ts[0..4] FROM vol (and SELF)
+ S_incomplete_type[bits 0 to 7] FROM \nothing
[from] ====== END OF CALLWISE DEPENDENCIES ======
[inout] Out (internal) for function test:
- t1[0..99]; t2[0..99]; t3[10..99]; t4[1..99]; t5[0..99]; t6[10..13];
- t7[0..3]; t8[0..3]; t9[20..99]; t10[4..12]; t11[2..6]; t12[0..96];
- ts[0..4]; dst; p; tmp_0; s; s1; k
+ NULL[16..17]; t1[0..99]; t2[0..99]; t3[10..99]; t4[1..99]; t5[0..99];
+ t6[10..13]; t7[0..3]; t8[0..3]; t9[20..99]; t10[4..12]; t11[2..6];
+ t12[0..96]; ts[0..4]; dst; p; tmp_0; s; s1; k; absolute_valid_range;
+ S_incomplete_type[bits 0 to 7]
[inout] Inputs for function test:
- vol
+ incomplete_type; vol
[inout] InOut (internal) for function test:
Operational inputs:
- vol
+ incomplete_type; vol
Operational inputs on termination:
- vol
+ incomplete_type; vol
Sure outputs:
- t1[0..99]; t5[0..99]; t10[4..6]; t11[3]; dst; p; tmp_0; s; s1; k
+ NULL[16..17]; t1[0..99]; t2[0..99]; t5[0..99]; t8[0..3]; t10[4..6];
+ t11[3]; dst; p; tmp_0; s; s1; k; absolute_valid_range;
+ S_incomplete_type[bits 0 to 7]
[inout] Out (internal) for function uninit:
x; a
[inout] Inputs for function uninit:
@@ -314,15 +355,16 @@
Sure outputs:
a
[inout] Out (internal) for function main:
- t1[0..99]; t2[0..99]; t3[10..99]; t4[1..99]; t5[0..99]; t6[10..13];
- t7[0..3]; t8[0..3]; t9[20..99]; t10[4..12]; t11[2..6]; t12[0..96];
- ts[0..4]
+ NULL[16..17]; t1[0..99]; t2[0..99]; t3[10..99]; t4[1..99]; t5[0..99];
+ t6[10..13]; t7[0..3]; t8[0..3]; t9[20..99]; t10[4..12]; t11[2..6];
+ t12[0..96]; ts[0..4]; S_incomplete_type[bits 0 to 7]
[inout] Inputs for function main:
- vol
+ incomplete_type; vol
[inout] InOut (internal) for function main:
Operational inputs:
- vol
+ incomplete_type; vol
Operational inputs on termination:
- vol
+ incomplete_type; vol
Sure outputs:
- t1[0..99]; t5[0..99]; t10[4..6]; t11[3]
+ NULL[16..17]; t1[0..99]; t2[0..99]; t5[0..99]; t8[0..3]; t10[4..6];
+ t11[3]; S_incomplete_type[bits 0 to 7]
diff --git a/tests/builtins/oracle_gauges/memcpy.res.oracle b/tests/builtins/oracle_gauges/memcpy.res.oracle
index 78ce5790f07d21391745733139582ff60737e029..a770a6bfa690f6889cc7840880cba52333ba7fbe 100644
--- a/tests/builtins/oracle_gauges/memcpy.res.oracle
+++ b/tests/builtins/oracle_gauges/memcpy.res.oracle
@@ -1,5 +1,5 @@
-150a151,152
+146a147,148
> [eva] memcpy.c:96: Call to builtin memcpy
> [eva] memcpy.c:96: Call to builtin memcpy
-376a379
+372a375
> [eva] memcpy.c:230: starting to merge loop iterations