diff --git a/infer/src/backend/Payloads.ml b/infer/src/backend/Payloads.ml index 89baac116..8fb1ec3e4 100644 --- a/infer/src/backend/Payloads.ml +++ b/infer/src/backend/Payloads.ml @@ -19,7 +19,7 @@ type t = ; resources: ResourceLeakDomain.summary option ; siof: SiofDomain.Summary.astate option ; typestate: TypeState.t option - ; uninit: UninitDomain.summary option + ; uninit: UninitDomain.Summary.t option ; cost: CostDomain.summary option ; starvation: StarvationDomain.summary option ; purity: PurityDomain.summary option } @@ -59,7 +59,7 @@ let pp pe fmt buffer_overrun (pp_opt "AnnotationReachability" AnnotReachabilityDomain.pp) annot_map - (pp_opt "Uninitialised" UninitDomain.pp_summary) + (pp_opt "Uninitialised" UninitDomain.Summary.pp) uninit (pp_opt "Cost" CostDomain.pp_summary) cost diff --git a/infer/src/backend/Payloads.mli b/infer/src/backend/Payloads.mli index 4ea301e94..27c8adfce 100644 --- a/infer/src/backend/Payloads.mli +++ b/infer/src/backend/Payloads.mli @@ -19,7 +19,7 @@ type t = ; resources: ResourceLeakDomain.summary option ; siof: SiofDomain.Summary.astate option ; typestate: TypeState.t option - ; uninit: UninitDomain.summary option + ; uninit: UninitDomain.Summary.t option ; cost: CostDomain.summary option ; starvation: StarvationDomain.summary option ; purity: PurityDomain.summary option } diff --git a/infer/src/checkers/uninit.ml b/infer/src/checkers/uninit.ml index 37d2a1dcc..b460e4f5f 100644 --- a/infer/src/checkers/uninit.ml +++ b/infer/src/checkers/uninit.ml @@ -17,7 +17,7 @@ module AliasedVars = AbstractDomain.FiniteSet (UninitDomain.VarPair) module RecordDomain = UninitDomain.Record (UninitVars) (AliasedVars) (D) module Payload = SummaryPayload.Make (struct - type t = UninitDomain.summary + type t = UninitDomain.Summary.t let update_payloads sum (payloads : Payloads.t) = {payloads with uninit= Some sum} diff --git a/infer/src/checkers/uninitDomain.ml b/infer/src/checkers/uninitDomain.ml index 46e4957c0..f8ee9b4d6 100644 --- a/infer/src/checkers/uninitDomain.ml +++ b/infer/src/checkers/uninitDomain.ml @@ -13,20 +13,12 @@ module Domain = AbstractDomain.InvertedSet (AccessExpression) type 'a prepost = {pre: 'a; post: 'a} -(* pre = set of parameters initialized inside the procedure; - post = set of uninit local variables of the procedure *) -type summary = Domain.t prepost - module VarPair = struct type t = Var.t * Var.t [@@deriving compare] let pp fmt pair = F.fprintf fmt " (%a, %a)" Var.pp (fst pair) Var.pp (snd pair) end -let pp_summary fmt {pre; post} = - F.fprintf fmt "@\n Pre: %a @\nPost: %a @\n" Domain.pp pre Domain.pp post - - module Record (Domain1 : AbstractDomain.S) (Domain2 : AbstractDomain.S) @@ -82,3 +74,11 @@ struct F.fprintf fmt "@\n uninit_vars: %a @\n aliased_vars: %a @\n prepost: (%a, %a)" Domain1.pp uv Domain2.pp av Domain3.pp pre Domain3.pp post end + +module Summary = struct + (* pre = set of parameters initialized inside the procedure; + post = set of uninit local variables of the procedure *) + type t = Domain.t prepost + + let pp fmt {pre; post} = F.fprintf fmt "@\n Pre: %a @\nPost: %a @\n" Domain.pp pre Domain.pp post +end