diff --git a/infer/src/checkers/Pulse.ml b/infer/src/checkers/Pulse.ml index a000b1f39..204bb492b 100644 --- a/infer/src/checkers/Pulse.ml +++ b/infer/src/checkers/Pulse.ml @@ -123,6 +123,7 @@ module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Exceptional) (Transf let checker {Callbacks.proc_desc; tenv; summary} = let proc_data = ProcData.make proc_desc tenv summary in + PulseDomain.AbstractAddress.init () ; ( try ignore (Analyzer.compute_post proc_data ~initial:PulseDomain.initial) with AbstractDomain.Stop_analysis -> () ) ; summary diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml index 9c4293b9d..db7146ec1 100644 --- a/infer/src/checkers/PulseDomain.ml +++ b/infer/src/checkers/PulseDomain.ml @@ -22,6 +22,8 @@ module AbstractAddress : sig val mk_fresh : unit -> t val pp : F.formatter -> t -> unit + + val init : unit -> unit end = struct type t = int [@@deriving compare] @@ -38,6 +40,8 @@ end = struct let pp = F.pp_print_int + + let init () = next_fresh := 1 end (* {3 Heap domain } *) diff --git a/infer/src/checkers/PulseDomain.mli b/infer/src/checkers/PulseDomain.mli index 18a6d99a9..25974fd98 100644 --- a/infer/src/checkers/PulseDomain.mli +++ b/infer/src/checkers/PulseDomain.mli @@ -11,6 +11,8 @@ module AbstractAddress : sig type t = private int [@@deriving compare] val nullptr : t + + val init : unit -> unit end type t