From c02edf85a9554b24190eeb5b93db057131b6a268 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 5 Mar 2019 09:34:11 -0800 Subject: [PATCH] [ai] remove option to join sometimes in disjunctive domain Summary: It was unused and not obviously useful. Reviewed By: mbouaziz, skcho Differential Revision: D14258485 fbshipit-source-id: c028e12c1 --- infer/src/absint/TransferFunctions.ml | 16 +--------------- infer/src/absint/TransferFunctions.mli | 5 +---- 2 files changed, 2 insertions(+), 19 deletions(-) diff --git a/infer/src/absint/TransferFunctions.ml b/infer/src/absint/TransferFunctions.ml index 7ebff2594..a39e33074 100644 --- a/infer/src/absint/TransferFunctions.ml +++ b/infer/src/absint/TransferFunctions.ml @@ -34,7 +34,7 @@ module type MakeHIL = functor (C : ProcCfg.S) -> sig end module type DisjunctiveConfig = sig - val join_policy : [`JoinAfter of int | `UnderApproximateAfter of int | `NeverJoin] + val join_policy : [`UnderApproximateAfter of int | `NeverJoin] val widen_policy : [`UnderApproximateAfterNumIterations of int] end @@ -76,20 +76,6 @@ module MakeHILDisjunctive (TransferFunctions : HILDisjReady) (DConfig : Disjunct union | `UnderApproximateAfter n -> if Set.cardinal union <= n then union else lhs - | `JoinAfter n -> - if Set.cardinal union <= n then union - else - let joined = - Set.fold - (fun dom joined -> - match joined with - | None -> - Some dom - | Some joined -> - Some (TransferFunctions.Domain.join dom joined) ) - union None - in - Set.singleton (Option.value_exn joined) let widen ~prev ~next ~num_iters = diff --git a/infer/src/absint/TransferFunctions.mli b/infer/src/absint/TransferFunctions.mli index 41c3cbdc3..d058b3320 100644 --- a/infer/src/absint/TransferFunctions.mli +++ b/infer/src/absint/TransferFunctions.mli @@ -39,10 +39,7 @@ end module type DisjunctiveConfig = sig val join_policy : - [ `JoinAfter of int - (** when the set of disjuncts gets bigger than [n] the underlying domain's join is called to - collapse them into one state *) - | `UnderApproximateAfter of int + [ `UnderApproximateAfter of int (** When the set of disjuncts gets bigger than [n] then just stop adding new states to it, drop any further states on the floor. This corresponds to an under-approximation/bounded approach. *)