From ecbe8eca76611601cb05f9c759a263c1b77f02f4 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 27 Nov 2018 07:30:16 -0800 Subject: [PATCH] [pulse] remove nullptr model Summary: It is not used yet and still manages to cause false positives. Reviewed By: mbouaziz Differential Revision: D13102948 fbshipit-source-id: 2122666c2 --- infer/src/checkers/Pulse.ml | 2 -- infer/src/checkers/PulseDomain.ml | 5 ----- infer/src/checkers/PulseDomain.mli | 2 -- 3 files changed, 9 deletions(-) diff --git a/infer/src/checkers/Pulse.ml b/infer/src/checkers/Pulse.ml index dda249144..5f4219181 100644 --- a/infer/src/checkers/Pulse.ml +++ b/infer/src/checkers/Pulse.ml @@ -47,8 +47,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | AccessExpression rhs_access -> PulseDomain.read loc rhs_access astate >>= fun (astate, rhs_value) -> PulseDomain.write loc lhs_access rhs_value astate - | Constant (Cint address) when IntLit.iszero address -> - PulseDomain.write loc lhs_access PulseDomain.AbstractAddress.nullptr astate | Cast (_, e) -> exec_assign lhs_access e loc astate | _ -> diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml index 5626fecc3..c2fa49a16 100644 --- a/infer/src/checkers/PulseDomain.ml +++ b/infer/src/checkers/PulseDomain.ml @@ -15,8 +15,6 @@ module Invalidation = PulseInvalidation module AbstractAddress : sig type t = private int [@@deriving compare] - val nullptr : t - val equal : t -> t -> bool val mk_fresh : unit -> t @@ -29,9 +27,6 @@ end = struct let equal = [%compare.equal: t] - (** distinguish 0 since it's always an invalid address *) - let nullptr = 0 - let next_fresh = ref 1 let mk_fresh () = diff --git a/infer/src/checkers/PulseDomain.mli b/infer/src/checkers/PulseDomain.mli index 72a54a7cc..707302962 100644 --- a/infer/src/checkers/PulseDomain.mli +++ b/infer/src/checkers/PulseDomain.mli @@ -10,8 +10,6 @@ open! IStd module AbstractAddress : sig type t = private int [@@deriving compare] - val nullptr : t - val init : unit -> unit end