From 4442c52f7f18223d5c64291b187820bf16fb1195 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Fri, 23 Oct 2020 05:24:28 -0700 Subject: [PATCH] [pulse][minor] inline a module definition Summary: It's only used once. Reviewed By: da319 Differential Revision: D24503170 fbshipit-source-id: fc35239b3 --- infer/src/pulse/PulseAbductiveDomain.ml | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 433cda285..93bba3011 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -41,8 +41,10 @@ end type base_domain = BaseDomain.t = {heap: BaseMemory.t; stack: BaseStack.t; attrs: BaseAddressAttributes.t} -(** operations common to [Domain] and [PreDomain], see also the [BaseDomain] signature *) -module BaseDomainCommon = struct +(** represents the post abstract state at each program point *) +module PostDomain : BaseDomainSig = struct + include BaseDomain + let update ?stack ?heap ?attrs foot = let new_stack, new_heap, new_attrs = ( Option.value ~default:foot.stack stack @@ -70,12 +72,6 @@ module BaseDomainCommon = struct (update ~heap:heap' ~attrs:attrs' foot, discarded_addresses) end -(** represents the post abstract state at each program point *) -module PostDomain : BaseDomainSig = struct - include BaseDomainCommon - include BaseDomain -end - (* NOTE: [PreDomain] and [Domain] theoretically differ in that [PreDomain] should be the inverted lattice of [Domain], but since we never actually join states or check implication the two collapse into one. *) (** represents the inferred pre-condition at each program point, biabduction style *)