From 572080a8e92022759f43cdf5fe359d2d6470986b Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Fri, 19 Mar 2021 02:22:38 -0700 Subject: [PATCH] [pulse] Havoc actuals when lengths of actuals and formals mismatch Summary: In Pulse, it usually havoc the actual parameters to unknown functions. However, it did not do that when the lengths of actuals and formals mismatch, which may happen when the frontend doesn't have enough information about procedures. This diff havoc the actual parameters, also when there is mismatch between lengths of actuals and formals. Reviewed By: ezgicicek Differential Revision: D27163143 fbshipit-source-id: 1c5e0853a --- infer/src/pulse/PulseCallOperations.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/infer/src/pulse/PulseCallOperations.ml b/infer/src/pulse/PulseCallOperations.ml index 0eb6c8ffb..8c3b56151 100644 --- a/infer/src/pulse/PulseCallOperations.ml +++ b/infer/src/pulse/PulseCallOperations.ml @@ -58,12 +58,15 @@ let unknown_call tenv call_loc reason ~ret ~actuals ~formals_opt astate = | _ -> astate in + let havoc_actuals_without_typ_info astate = + List.fold actuals + ~f:(fun astate actual_typ -> havoc_actual_if_ptr actual_typ None astate) + ~init:astate + in L.d_printfln "skipping unknown procedure@." ; ( match formals_opt with | None -> - List.fold actuals - ~f:(fun astate actual_typ -> havoc_actual_if_ptr actual_typ None astate) - ~init:astate + havoc_actuals_without_typ_info astate | Some formals -> ( match List.fold2 actuals formals @@ -74,7 +77,7 @@ let unknown_call tenv call_loc reason ~ret ~actuals ~formals_opt astate = | Unequal_lengths -> L.d_printfln "ERROR: formals have length %d but actuals have length %d" (List.length formals) (List.length actuals) ; - astate + havoc_actuals_without_typ_info astate | Ok result -> result ) ) |> havoc_ret ret |> add_skipped_proc