From 7c63bef44e7fc6129ae7d9b112864da47f8cb3d9 Mon Sep 17 00:00:00 2001 From: Loc Le Date: Tue, 6 Apr 2021 06:23:49 -0700 Subject: [PATCH] [pulse][isl] enable to check invalid for er specs in interprocedural analysis Reviewed By: skcho Differential Revision: D27587955 fbshipit-source-id: 652f66435 --- infer/src/pulse/PulseInterproc.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml index bc04d7bba..a23e089a1 100644 --- a/infer/src/pulse/PulseInterproc.ml +++ b/infer/src/pulse/PulseInterproc.ml @@ -730,8 +730,7 @@ let apply_prepost ~is_isl_error_prepost callee_proc_name call_location ~callee_p [check_all_valid], whereas the "normal" mode encodes some error specs implicitly in the ContinueProgram ok specs *) let* astate = - if Config.pulse_isl then - if is_isl_error_prepost then Error (AccessResult.ISLError astate) else Ok astate + if Config.pulse_isl then Ok astate else check_all_valid callee_proc_name call_location pre_post call_state in (* reset [visited] *)