From 2d41b9d58a7b58389ad5d9befbe92d59d575f05c Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 26 Jun 2019 10:27:34 -0700 Subject: [PATCH] [pulse] skip `folly::SocketAddress::~SocketAddress` Summary: The constructor of `folly::SocketAddress` conditionally deletes some object and then makes that condition false. The destructor then does the same. Pulse ignores conditionals so will see a double delete. Just skip that function for now, but it should be easy for pulse to be more correct here if it knew how to compare constant values. Reviewed By: mbouaziz Differential Revision: D16005395 fbshipit-source-id: 036f5091b --- infer/src/pulse/PulseModels.ml | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 2fd930cd2..8c46f779f 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -18,6 +18,8 @@ type model = exec_fun module Misc = struct let early_exit : model = fun _ ~ret:_ ~actuals:_ _ -> Ok [] + + let skip : model = fun _ ~ret:_ ~actuals:_ astate -> Ok [astate] end module C = struct @@ -156,15 +158,12 @@ module StdVector = struct Ok [astate] end -module DelayedDestruction = struct - let destroy : model = fun _ ~ret:_ ~actuals:_ astate -> Ok [astate] -end - module ProcNameDispatcher = struct let dispatch : (unit, model) ProcnameDispatcher.ProcName.dispatcher = let open ProcnameDispatcher.ProcName in make_dispatcher - [ -"folly" &:: "DelayedDestruction" &:: "destroy" &--> DelayedDestruction.destroy + [ -"folly" &:: "DelayedDestruction" &:: "destroy" &--> Misc.skip + ; -"folly" &:: "SocketAddress" &:: "~SocketAddress" &--> Misc.skip ; -"std" &:: "function" &:: "operator()" &--> Cplusplus.operator_call ; -"std" &:: "vector" &:: "assign" &--> StdVector.invalidate_references Assign ; -"std" &:: "vector" &:: "clear" &--> StdVector.invalidate_references Clear