From b86b8a67750cb941702571d5aee55f02ffee2a8f Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 27 Feb 2018 09:19:16 -0800 Subject: [PATCH] subtle dead code in prop/fav stuff Summary: A list of free variables was computed and passed around, but never used. The reason OCaml wasn't complaining is that the list is eventually passed to a recursive function, which passes it to its recursive call, so it looks like it's used there. Reviewed By: mbouaziz Differential Revision: D7098556 fbshipit-source-id: b22a591 --- infer/src/backend/prop.ml | 36 ++++++++++-------------------------- 1 file changed, 10 insertions(+), 26 deletions(-) diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 82526a241..371b9696a 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -2480,28 +2480,18 @@ let prop_iter_fav_add fav iter = (** Find fav of the iterator *) let prop_iter_fav iter = Sil.fav_imperative_to_functional prop_iter_fav_add iter -(** Free vars of the iterator except the current hpred (and footprint). *) -let prop_iter_noncurr_fav_add fav iter = - sigma_fav_add fav iter.pit_old ; - sigma_fav_add fav iter.pit_new ; - Sil.sub_fav_add fav iter.pit_sub ; - pi_fav_add fav iter.pit_pi - - (** Extract the sigma part of the footprint *) let prop_iter_get_footprint_sigma iter = iter.pit_sigma_fp (** Replace the sigma part of the footprint *) let prop_iter_replace_footprint_sigma iter sigma = {iter with pit_sigma_fp= sigma} -let prop_iter_noncurr_fav iter = Sil.fav_imperative_to_functional prop_iter_noncurr_fav_add iter - -let rec strexp_gc_fields (fav: Sil.fav) (se: Sil.strexp) = +let rec strexp_gc_fields (se: Sil.strexp) = match se with | Eexp _ -> Some se | Estruct (fsel, inst) -> - let fselo = List.map ~f:(fun (f, se) -> (f, strexp_gc_fields fav se)) fsel in + let fselo = List.map ~f:(fun (f, se) -> (f, strexp_gc_fields se)) fsel in let fsel' = let fselo' = List.filter ~f:(function _, Some _ -> true | _ -> false) fselo in List.map ~f:(function f, seo -> (f, unSome seo)) fselo' @@ -2512,17 +2502,14 @@ let rec strexp_gc_fields (fav: Sil.fav) (se: Sil.strexp) = Some se -let hpred_gc_fields (fav: Sil.fav) (hpred: Sil.hpred) : Sil.hpred = +let hpred_gc_fields (hpred: Sil.hpred) : Sil.hpred = match hpred with - | Hpointsto (e, se, te) - -> ( - Sil.exp_fav_add fav e ; - Sil.exp_fav_add fav te ; - match strexp_gc_fields fav se with - | None -> - hpred - | Some se' -> - if Sil.equal_strexp se se' then hpred else Hpointsto (e, se', te) ) + | Hpointsto (e, se, te) -> ( + match strexp_gc_fields se with + | None -> + hpred + | Some se' -> + if Sil.equal_strexp se se' then hpred else Hpointsto (e, se', te) ) | Hlseg _ | Hdllseg _ -> hpred @@ -2535,10 +2522,7 @@ let rec prop_iter_map f iter = (** Collect garbage fields. *) let prop_iter_gc_fields iter = - let f iter' = - let fav = prop_iter_noncurr_fav iter' in - hpred_gc_fields fav iter'.pit_curr - in + let f iter' = hpred_gc_fields iter'.pit_curr in prop_iter_map f iter