diff --git a/infer/src/pulse/PulseArithmetic.ml b/infer/src/pulse/PulseArithmetic.ml index 50f25aae7..b01f8f1fb 100644 --- a/infer/src/pulse/PulseArithmetic.ml +++ b/infer/src/pulse/PulseArithmetic.ml @@ -161,6 +161,13 @@ let pp fmt = function F.fprintf fmt "∉[%a,%a]" IntLit.pp l IntLit.pp u +let is_equal_to_zero = function + | Between (Int l, Int u) when IntLit.iszero l && IntLit.iszero u -> + true + | _ -> + false + + let has_empty_intersection a1 a2 = match (a1, a2) with | Outside _, Outside _ -> diff --git a/infer/src/pulse/PulseArithmetic.mli b/infer/src/pulse/PulseArithmetic.mli index 4bd448044..25adbe31d 100644 --- a/infer/src/pulse/PulseArithmetic.mli +++ b/infer/src/pulse/PulseArithmetic.mli @@ -7,15 +7,12 @@ open! IStd module F = Format -module Bound : sig - type t = Int of IntLit.t | MinusInfinity | PlusInfinity -end - -type t = private Between of Bound.t * Bound.t | Outside of IntLit.t * IntLit.t -[@@deriving compare] +type t [@@deriving compare] val equal_to : IntLit.t -> t +val is_equal_to_zero : t -> bool + val pp : F.formatter -> t -> unit type abduction_result = diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index a166b86c5..d239a8bf5 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -57,7 +57,13 @@ end module C = struct let free deleted_access : model = fun ~caller_summary:_ location ~ret:_ astate -> - PulseOperations.invalidate location Invalidation.CFree deleted_access astate >>| List.return + match Memory.get_arithmetic (fst deleted_access) astate with + | Some (arith, _) when Arithmetic.is_equal_to_zero arith -> + (* freeing 0 is a no-op *) + Ok [astate] + | _ -> + PulseOperations.invalidate location Invalidation.CFree deleted_access astate + >>| fun astate -> [astate] end module Cplusplus = struct diff --git a/infer/tests/codetoanalyze/cpp/pulse/use_after_free.cpp b/infer/tests/codetoanalyze/cpp/pulse/use_after_free.cpp index 7ff1679d3..9e5cf5b5d 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/use_after_free.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/use_after_free.cpp @@ -24,3 +24,8 @@ void double_free_global_bad() { free_global_pointer_ok(); free_global_pointer_ok(); } + +void free_nullptr_ok() { + int* p = nullptr; + free(p); +}