From 4bad4bf63c49f721ea5077102ca468835bbe7dc4 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 25 May 2021 09:09:30 -0700 Subject: [PATCH] [pulse][3/5] delete stale comment Summary: We do have a value analysis now :) Reviewed By: skcho Differential Revision: D28674728 fbshipit-source-id: 5caa54b63 --- infer/src/pulse/PulseInterproc.ml | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml index e1551951d..98938f159 100644 --- a/infer/src/pulse/PulseInterproc.ml +++ b/infer/src/pulse/PulseInterproc.ml @@ -703,14 +703,7 @@ let isl_check_all_invalid invalid_addr_callers callee_proc_name call_location - for each actual, write the post for that actual - - if aliasing is introduced at any time then give up - - questions: - - - what if some preconditions raise lifetime issues but others don't? Have to be careful with - the noise that this will introduce since we don't care about values. For instance, if the pre - is for a path where [formal != 0] and we pass [0] then it will be an FP. Maybe the solution is - to bake in some value analysis. *) + - if aliasing is introduced at any time then give up *) let apply_prepost ~is_isl_error_prepost callee_proc_name call_location ~callee_prepost:pre_post ~captured_vars_with_actuals ~formals ~actuals astate = L.d_printfln "Applying pre/post for %a(%a):@\n%a" Procname.pp callee_proc_name