diff --git a/src/plugins/eva/engine/transfer_specification.ml b/src/plugins/eva/engine/transfer_specification.ml index eda7c02d067e4e93673eeda97269043ee84ae50f..c0520b22fcdeefcc45e9882f89f38bb43780267b 100644 --- a/src/plugins/eva/engine/transfer_specification.ml +++ b/src/plugins/eva/engine/transfer_specification.ml @@ -306,13 +306,15 @@ module Make let env = make_env pre in let assigns = get_assigns_for_behavior spec behavior in let check_one_assign cvalue_state (assign, _) = - match evaluate_location env retres_loc Assign assign with - | None -> () - | Some location -> - let loc = Precise_locs.imprecise_location (get_ploc location) in - let cvalue = Cvalue.Model.find cvalue_state loc in - begin - match cvalue with + let location = evaluate_location env retres_loc Assign assign in + let precise_loc = Option.map get_ploc location in + let loc = Option.map Precise_locs.imprecise_location precise_loc in + match loc with + | None | Some Locations.{ size = Top } -> () + | Some Locations.{ loc; size = Value size } -> + let offsm = Cvalue.Model.copy_offsetmap loc size cvalue_state in + let warn v = + match Cvalue.V_Or_Uninitialized.get_v v with | Top (bases, origin) -> if Origin.register_write bases origin then Self.warning ~current:true ~once:true @@ -321,7 +323,8 @@ module Make a garbled mix of addresses@ for %a.@]" Kernel_function.pretty kf pp_assign_clause (Assign, assign) | _ -> () - end + in + Bottom.iter (Cvalue.V_Offsetmap.iter_on_values warn) offsm in let check_one_state state = let cvalue_state = get_cvalue_or_top state in diff --git a/tests/libc/oracle/pwd_h.res.oracle b/tests/libc/oracle/pwd_h.res.oracle index 5dedb215f1a912fec633ab2a5558fcae72075554..6cdda1a2be90568192afabc4b31d25b32fbdfb21 100644 --- a/tests/libc/oracle/pwd_h.res.oracle +++ b/tests/libc/oracle/pwd_h.res.oracle @@ -7,9 +7,6 @@ [eva] computing for function getpwuid <- main. Called from pwd_h.c:10. [eva] using specification for function getpwuid -[eva:garbled-mix:assigns] pwd_h.c:10: - The specification of function getpwuid - has generated a garbled mix of addresses for assigns clause __fc_pwd. [eva] Done for function getpwuid [eva:alarm] pwd_h.c:13: Warning: assertion got status unknown. [eva:alarm] pwd_h.c:14: Warning: assertion got status unknown. @@ -19,9 +16,6 @@ Called from pwd_h.c:18. [eva] using specification for function getpwnam [eva] pwd_h.c:18: function getpwnam: precondition 'valid_name' got status valid. -[eva:garbled-mix:assigns] pwd_h.c:18: - The specification of function getpwnam - has generated a garbled mix of addresses for assigns clause __fc_pwd. [eva] Done for function getpwnam [eva:alarm] pwd_h.c:21: Warning: assertion got status unknown. [eva:alarm] pwd_h.c:22: Warning: assertion got status unknown.