Fix aliasing rules about local variables introduced before

Reviewed By: jeremydubreil

Differential Revision: D5316284

fbshipit-source-id: 1a70188

infer/src/backend/prover.ml

@@ -635,9 +635,9 @@ let check_disequal tenv prop e1 e2 =
     | Exp.Lvar pv0, Exp.Lvar pv1 ->
         (* Addresses of any two local vars must be different *)
         not (Pvar.equal pv0 pv1)
-    | Exp.Lvar _, Exp.Var id | Exp.Var id, Exp.Lvar _ ->
-        (* Address of any local var must be different from the value of any footprint var *)
-        Ident.is_footprint id
+    | Exp.Lvar pv, Exp.Var id | Exp.Var id, Exp.Lvar pv ->
+        (* Address of any non-global var must be different from the value of any footprint var *)
+        (not (Pvar.is_global pv)) && Ident.is_footprint id
     | _, _ -> false in
   let ineq = lazy (Inequalities.from_prop tenv prop) in
   let check_pi_implies_disequal e1 e2 =

infer/tests/codetoanalyze/c/biabduction/example.c

@@ -12,18 +12,28 @@ void foo() {
   *p = 42;
 }
 
-void local_addr_noalis_ok(int* p) {
+void local_addr_noalias_ok(int* p) {
   int* q = 0;
   int x = 1;
-  if (&x == p)
+  if (&x == p) {
     *q = 42;
+  }
 }
 
 void local_addr_noalias_bad(int* p) {
   int* q = 0;
   int x = 1;
-  if (&x != p)
+  if (&x != p) {
     *q = 42;
+  }
+}
+
+static int g = 0;
+void global_addr_alias_bad(int* p) {
+  int* q = 0;
+  if (&g == p) {
+    *q = 42;
+  }
 }
 
 int bar() {