[infer][biabduction] Minor simplification of the load symbolic execution code

Summary: Cleanup

Reviewed By: mbouaziz

Differential Revision: D5873159

fbshipit-source-id: 30ee521
master
Jeremy Dubreil 7 years ago committed by Facebook Github Bot
parent 5b55179cbf
commit 41451743f7

@ -968,7 +968,7 @@ let add_constraints_on_retval tenv pdesc prop ret_exp ~has_nullable_annot typ ca
else add_ret_non_null ret_exp typ prop else add_ret_non_null ret_exp typ prop
let execute_load ?(report_deref_errors= true) pname pdesc tenv id rhs_exp typ loc prop_ = let execute_load ?(report_deref_errors= true) pname pdesc tenv id rhs_exp typ loc prop_ =
let execute_load_ pdesc tenv id loc acc_in iter = let execute_load_ acc_in iter =
let iter_ren = Prop.prop_iter_make_id_primed tenv id iter in let iter_ren = Prop.prop_iter_make_id_primed tenv id iter in
let prop_ren = Prop.prop_iter_to_prop tenv iter_ren in let prop_ren = Prop.prop_iter_to_prop tenv iter_ren in
match Prop.prop_iter_current tenv iter_ren with match Prop.prop_iter_current tenv iter_ren with
@ -1015,7 +1015,7 @@ let execute_load ?(report_deref_errors= true) pname pdesc tenv id rhs_exp typ lo
let iter_list = let iter_list =
Rearrange.rearrange ~report_deref_errors pdesc tenv n_rhs_exp' typ prop loc Rearrange.rearrange ~report_deref_errors pdesc tenv n_rhs_exp' typ prop loc
in in
List.rev (List.fold ~f:(execute_load_ pdesc tenv id loc) ~init:[] iter_list) List.rev (List.fold ~f:execute_load_ ~init:[] iter_list)
with Exceptions.Symexec_memory_error _ -> with Exceptions.Symexec_memory_error _ ->
(* This should normally be a real alarm and should not be caught but currently happens (* This should normally be a real alarm and should not be caught but currently happens
when the normalization drops hpreds of the form ident |-> footprint var. *) when the normalization drops hpreds of the form ident |-> footprint var. *)

@ -317,7 +317,7 @@ let check_dereferences tenv callee_pname actual_pre sub spec_pre formal_params =
| None | None
-> assert false -> assert false
else if (* Check if the dereferenced expr has the dangling uninitialized attribute. *) else if (* Check if the dereferenced expr has the dangling uninitialized attribute. *)
(* In that case it raise a dangling pointer dereferece *) (* In that case it raise a dangling pointer dereference *)
Attribute.has_dangling_uninit tenv spec_pre e Attribute.has_dangling_uninit tenv spec_pre e
then Some (Deref_undef_exp, desc false (Localise.deref_str_dangling (Some PredSymb.DAuninit))) then Some (Deref_undef_exp, desc false (Localise.deref_str_dangling (Some PredSymb.DAuninit)))
else if Exp.equal e_sub Exp.minus_one then else if Exp.equal e_sub Exp.minus_one then

Loading…
Cancel
Save