From f0a31f460b88915628e8d0bd64d9807f59b7520f Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Thu, 22 Sep 2016 19:13:31 -0700 Subject: [PATCH] [checkers] don't crash when a frontend temp is reassigned Reviewed By: jeremydubreil Differential Revision: D3867083 fbshipit-source-id: 8cd5cfe --- infer/src/checkers/IdAccessPathMapDomain.ml | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/infer/src/checkers/IdAccessPathMapDomain.ml b/infer/src/checkers/IdAccessPathMapDomain.ml index 34b4289f7..dd5fed01a 100644 --- a/infer/src/checkers/IdAccessPathMapDomain.ml +++ b/infer/src/checkers/IdAccessPathMapDomain.ml @@ -41,11 +41,18 @@ let join astate1 astate2 = then astate1 else IdMap.merge - (fun _ ap1_opt ap2_opt -> match ap1_opt, ap2_opt with + (fun var ap1_opt ap2_opt -> match ap1_opt, ap2_opt with | Some ap1, Some ap2 -> (* in principle, could do a join here if the access paths have the same root. but they should always be equal if we are using the map correctly *) - assert (AccessPath.raw_equal ap1 ap2); + let check_invariant () = match var with + | Var.ProgramVar pvar when Pvar.is_frontend_tmp pvar -> + (* Sawja reuses temporary variables which sometimes breaks this invariant *) + (* TODO: fix (13370224) *) + () + | _ -> + assert (AccessPath.raw_equal ap1 ap2) in + check_invariant (); ap1_opt | Some _, None -> ap1_opt | None, Some _ -> ap2_opt