[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

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

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 () =

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