pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[biabd] various very minor changes

Browse Source 
Summary: I think these improve readability.

Reviewed By: jeremydubreil

Differential Revision: D15294782

fbshipit-source-id: b2eccba75
master
Jules Villard 6 years ago committed by Facebook Github Bot
parent 3b3139a29e
commit 9717be7e2f
2 changed files with 17 additions and 24 deletions
Show Stats Download Patch File Download Diff File

10
infer/src/biabduction/Dom.ml
Unescape View File

@ -2109,12 +2109,6 @@ let pathset_collapse tenv pset =
let pathset_join pname tenv (pset1 : Paths.PathSet.t) (pset2 : Paths.PathSet.t) : let pathset_join pname tenv (pset1 : Paths.PathSet.t) (pset2 : Paths.PathSet.t) :
Paths.PathSet.t * Paths.PathSet.t = Paths.PathSet.t * Paths.PathSet.t =
let mode = JoinState.Post in let mode = JoinState.Post in
let pset_to_plist pset =
let f_list p pa acc = (p, pa) :: acc in
Paths.PathSet.fold f_list pset []
in
let ppalist1 = pset_to_plist pset1 in
let ppalist2 = pset_to_plist pset2 in
let rec join_proppath_plist ppalist2_acc ((p2, pa2) as ppa2) = function let rec join_proppath_plist ppalist2_acc ((p2, pa2) as ppa2) = function
| [] -> | [] ->
(ppa2, List.rev ppalist2_acc) (ppa2, List.rev ppalist2_acc)
@ -2149,7 +2143,9 @@ let pathset_join pname tenv (pset1 : Paths.PathSet.t) (pset2 : Paths.PathSet.t)
let ppa2_new, ppalist1_cur' = join_proppath_plist [] ppa2'' ppalist1_cur in let ppa2_new, ppalist1_cur' = join_proppath_plist [] ppa2'' ppalist1_cur in
join ppalist1_cur' (ppa2_new :: ppalist2_acc') ppalist2_rest' join ppalist1_cur' (ppa2_new :: ppalist2_acc') ppalist2_rest'
in in
let ppalist1_res_, ppalist2_res_ = join ppalist1 [] ppalist2 in let ppalist1_res_, ppalist2_res_ =
join (Paths.PathSet.elements pset1) [] (Paths.PathSet.elements pset2)
in
let ren l = List.map ~f:(fun (p, x) -> (Prop.prop_rename_primed_footprint_vars tenv p, x)) l in let ren l = List.map ~f:(fun (p, x) -> (Prop.prop_rename_primed_footprint_vars tenv p, x)) l in
let ppalist1_res, ppalist2_res = (ren ppalist1_res_, ren ppalist2_res_) in let ppalist1_res, ppalist2_res = (ren ppalist1_res_, ren ppalist2_res_) in
let res = let res =

31
infer/src/biabduction/interproc.ml
Unescape View File

@ -139,19 +139,16 @@ let htable_retrieve (htable : (Procdesc.Node.id, Paths.PathSet.t) Hashtbl.t)
(** Add [d] to the pathset todo at [node] returning true if changed *) (** Add [d] to the pathset todo at [node] returning true if changed *)
let path_set_put_todo (wl : Worklist.t) (node : Procdesc.Node.t) (d : Paths.PathSet.t) : bool = let path_set_put_todo (wl : Worklist.t) (node : Procdesc.Node.t) (d : Paths.PathSet.t) : bool =
let changed = if Paths.PathSet.is_empty d then false
if Paths.PathSet.is_empty d then false else
else let node_id = Procdesc.Node.get_id node in
let node_id = Procdesc.Node.get_id node in let old_todo = htable_retrieve wl.Worklist.path_set_todo node_id in
let old_todo = htable_retrieve wl.Worklist.path_set_todo node_id in let old_visited = htable_retrieve wl.Worklist.path_set_visited node_id in
let old_visited = htable_retrieve wl.Worklist.path_set_visited node_id in let d' = Paths.PathSet.diff d old_visited in
let d' = Paths.PathSet.diff d old_visited in (* differential fixpoint *)
(* differential fixpoint *) let todo_new = Paths.PathSet.union old_todo d' in
let todo_new = Paths.PathSet.union old_todo d' in Hashtbl.replace wl.Worklist.path_set_todo node_id todo_new ;
Hashtbl.replace wl.Worklist.path_set_todo node_id todo_new ; not (Paths.PathSet.equal old_todo todo_new)
not (Paths.PathSet.equal old_todo todo_new)
in
changed
let path_set_checkout_todo (wl : Worklist.t) (node : Procdesc.Node.t) : Paths.PathSet.t = let path_set_checkout_todo (wl : Worklist.t) (node : Procdesc.Node.t) : Paths.PathSet.t =
@ -718,7 +715,7 @@ let prop_init_formals_seed tenv new_formals (prop : 'a Prop.t) : Prop.exposed Pr
(** Construct an initial prop by extending [prop] with locals, and formals if [add_formals] is true (** Construct an initial prop by extending [prop] with locals, and formals if [add_formals] is true
as well as seed variables *) as well as seed variables *)
let initial_prop tenv (curr_f : Procdesc.t) (prop : 'a Prop.t) add_formals : Prop.normal Prop.t = let initial_prop tenv (curr_f : Procdesc.t) (prop : 'a Prop.t) ~add_formals : Prop.normal Prop.t =
let construct_decl (x, typ) = (Pvar.mk x (Procdesc.get_proc_name curr_f), typ) in let construct_decl (x, typ) = (Pvar.mk x (Procdesc.get_proc_name curr_f), typ) in
let new_formals = let new_formals =
if add_formals then List.map ~f:construct_decl (Procdesc.get_formals curr_f) else [] if add_formals then List.map ~f:construct_decl (Procdesc.get_formals curr_f) else []
@ -733,7 +730,7 @@ let initial_prop tenv (curr_f : Procdesc.t) (prop : 'a Prop.t) add_formals : Pro
(** Construct an initial prop from the empty prop *) (** Construct an initial prop from the empty prop *)
let initial_prop_from_emp tenv curr_f = initial_prop tenv curr_f Prop.prop_emp true let initial_prop_from_emp tenv curr_f = initial_prop tenv curr_f Prop.prop_emp ~add_formals:true
(** Construct an initial prop from an existing pre with formals *) (** Construct an initial prop from an existing pre with formals *)
let initial_prop_from_pre tenv curr_f pre = let initial_prop_from_pre tenv curr_f pre =
@ -745,8 +742,8 @@ let initial_prop_from_pre tenv curr_f pre =
let sub = Sil.subst_of_list sub_list in let sub = Sil.subst_of_list sub_list in
let pre2 = Prop.prop_sub sub pre in let pre2 = Prop.prop_sub sub pre in
let pre3 = Prop.set pre2 ~pi_fp:(Prop.get_pure pre2) ~sigma_fp:pre2.Prop.sigma in let pre3 = Prop.set pre2 ~pi_fp:(Prop.get_pure pre2) ~sigma_fp:pre2.Prop.sigma in
initial_prop tenv curr_f pre3 false initial_prop tenv curr_f pre3 ~add_formals:false
else initial_prop tenv curr_f pre false else initial_prop tenv curr_f pre ~add_formals:false
(** Re-execute one precondition and return some spec if there was no re-execution error. *) (** Re-execute one precondition and return some spec if there was no re-execution error. *)

Write Preview
Loading…
Cancel
Save