[pulse] reset abstract address fresh counter for each function

Summary:
Smaller numbers are easier to read and abstract addresses should never
be shared across functions anyway.

Reviewed By: da319

Differential Revision: D12881988

fbshipit-source-id: f9bcfa343
master
Jules Villard 6 years ago committed by Facebook Github Bot
parent 54fb38b7e8
commit b8bb1f318f

@ -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

@ -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 } *)

@ -11,6 +11,8 @@ module AbstractAddress : sig
type t = private int [@@deriving compare]
val nullptr : t
val init : unit -> unit
end
type t

Loading…
Cancel
Save