@ -784,6 +784,13 @@ let handle_special_cases_call tenv cfg pname actual_params =
else pname , actual_params
let handle_objc_method_call actual_pars actual_params pre tenv cfg ret_ids pdesc callee_pname loc path =
let receiver_self receiver prop =
list_exists ( fun hpred ->
match hpred with
| Sil . Hpointsto ( Sil . Lvar pv , Sil . Eexp ( e , _ ) , _ ) ->
Sil . exp_equal e receiver && Sil . pvar_is_seed pv &&
Sil . pvar_get_name pv = Mangled . from_string " self "
| _ -> false ) ( Prop . get_sigma prop ) in
let path_description = " Message " ^ ( Procname . to_simplified_string callee_pname ) ^ " with receiver nil returns nil. " in
let receiver = ( match actual_pars with
| ( e , _ ) :: _ -> e
@ -793,6 +800,10 @@ let handle_objc_method_call actual_pars actual_params pre tenv cfg ret_ids pdesc
match actual_pars with
| ( e , _ ) :: _ when Sil . exp_equal e Sil . exp_zero | | Option . is_some ( Prop . get_objc_null_attribute pre e ) -> true
| _ -> false in
let prop_null =
match ret_ids with
| [ ret_id ] -> Prop . conjoin_eq ( Sil . Var ret_id ) Sil . exp_zero pre
| _ -> pre in
let add_objc_null_attribute_or_nullify_result prop =
match ret_ids with
| [ ret_id ] ->
@ -815,16 +826,22 @@ let handle_objc_method_call actual_pars actual_params pre tenv cfg ret_ids pdesc
| _ -> false in
if ! Config . footprint && not is_undef then
let res_null = (* returns: ( objc_null ( res ) /\ receiver=0 ) or an empty list of results *)
let pre_with_attr_or_null = add_objc_null_attribute_or_nullify_result pre in
let is_receiver_self = receiver_self receiver pre in
let pre_with_attr_or_null =
if is_receiver_self then prop_null
else add_objc_null_attribute_or_nullify_result pre in
let propset = prune_ne tenv false receiver Sil . exp_zero pre_with_attr_or_null in
if Propset . is_empty propset then []
else
let prop = list_hd ( Propset . to_proplist propset ) in
let path = Paths . Path . add_description path path_description in
let path =
if is_receiver_self then path
else Paths . Path . add_description path path_description in
[ ( prop , path ) ] in
res_null @ res
else res (* Not known if receiver = 0 and not footprint. Standard tabulation *)
let normalize_params pdesc prop actual_params =
let norm_arg ( p , args ) ( e , t ) =
let e' , p' = exp_norm_check_arith pdesc p e in
@ -832,6 +849,7 @@ let normalize_params pdesc prop actual_params =
let prop , args = list_fold_left norm_arg ( prop , [] ) actual_params in
( prop , list_rev args )
(* * Execute [instr] with a symbolic heap [prop]. *)
let rec sym_exec cfg tenv pdesc _ instr ( _ prop : Prop . normal Prop . t ) path
: ( Prop . normal Prop . t * Paths . Path . t ) list =