From 301ebd4cd51ffba4c52f928bfd1bf0b09900c570 Mon Sep 17 00:00:00 2001 From: Jia Chen Date: Tue, 27 Jun 2017 18:39:50 -0700 Subject: [PATCH] Teach do_imply additional aliasing rules Reviewed By: jeremydubreil Differential Revision: D5331685 fbshipit-source-id: 413d308 --- infer/src/backend/prover.ml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index 7c01c5b89..067271cd8 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -1202,6 +1202,9 @@ let exp_imply tenv calc_missing subs e1_in e2_in : subst2 = (* symmetric of above case *) let e' = Exp.BinOp (Binop.MinusA, e1, e2') in do_imply subs (Prop.exp_normalize_noabs tenv Sil.sub_empty e') e2 + | Exp.Var id, Exp.Lvar pv when Ident.is_footprint id && Pvar.is_local pv -> + (* Footprint var could never be the same as local address *) + raise (IMPL_EXC ("expression not equal", subs, (EXC_FALSE_EXPS (e1, e2)))) | Exp.Var _, e2 -> if calc_missing then let () = ProverState.add_missing_pi (Sil.Aeq (e1_in, e2_in)) in