From be754c1558354272a53e190b9e3a3d9b7ef16814 Mon Sep 17 00:00:00 2001
From: Daiva Naudziuniene <daivan@fb.com>
Date: Wed, 6 Jun 2018 03:42:35 -0700
Subject: [PATCH] [bi-abduction] Do not treat for union fields as uninitialized

Summary: There is a number of dangling pointer dereference false positives coming from our treatment of union in c/cpp. For now, do not treat union fields as uninitialised.

Reviewed By: mbouaziz

Differential Revision: D8279802

fbshipit-source-id: a339b0e
---
 infer/src/biabduction/SymExec.ml                       | 10 +++++++++-
 .../tests/codetoanalyze/c/errors/dangling_deref/dpd.c  | 10 ++++++++++
 .../codetoanalyze/cpp/errors/pointers/unintialized.cpp | 10 ++++++++++
 3 files changed, 29 insertions(+), 1 deletion(-)

diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml
index 8445e3516..8e71ca476 100644
--- a/infer/src/biabduction/SymExec.ml
+++ b/infer/src/biabduction/SymExec.ml
@@ -954,13 +954,21 @@ let execute_load ?(report_deref_errors= true) pname pdesc tenv id rhs_exp typ lo
         let contents, new_ptsto, pred_insts_op, lookup_uninitialized =
           ptsto_lookup pdesc tenv prop_ren (lexp, strexp, sizeof_data) offlist id
         in
+        let is_union_field =
+          match rhs_exp with
+          | Exp.Lfield (_, _, {Typ.desc= Tstruct name}) when Typ.Name.is_union name ->
+              true
+          | _ ->
+              false
+        in
         let update acc (pi, sigma) =
           let pi' = Sil.Aeq (Exp.Var id, contents) :: pi in
           let sigma' = new_ptsto :: sigma in
           let iter' = update_iter iter_ren pi' sigma' in
           let prop' = Prop.prop_iter_to_prop tenv iter' in
           let prop'' =
-            if lookup_uninitialized then
+            (* T30105165 remove `is_union_field` check after we improve union translation *)
+            if lookup_uninitialized && not is_union_field then
               Attribute.add_or_replace tenv prop' (Apred (Adangling DAuninit, [Exp.Var id]))
             else prop'
           in
diff --git a/infer/tests/codetoanalyze/c/errors/dangling_deref/dpd.c b/infer/tests/codetoanalyze/c/errors/dangling_deref/dpd.c
index ef52b8bed..13651fbb7 100644
--- a/infer/tests/codetoanalyze/c/errors/dangling_deref/dpd.c
+++ b/infer/tests/codetoanalyze/c/errors/dangling_deref/dpd.c
@@ -37,3 +37,13 @@ void intraprocdpd() {
   *y = 42;
   z = y;
 }
+
+short union_ok(int* param) {
+  union {
+    int* a;
+    short* b;
+  } u;
+  u.a = param;
+  short* p = u.b;
+  return *p;
+}
diff --git a/infer/tests/codetoanalyze/cpp/errors/pointers/unintialized.cpp b/infer/tests/codetoanalyze/cpp/errors/pointers/unintialized.cpp
index 01b87a585..e99ae8cb3 100644
--- a/infer/tests/codetoanalyze/cpp/errors/pointers/unintialized.cpp
+++ b/infer/tests/codetoanalyze/cpp/errors/pointers/unintialized.cpp
@@ -38,3 +38,13 @@ int unknown_ctor_assume_no_dangling_ok() {
   delete t1;
   return ret;
 }
+
+short union_ok(int* param) {
+  union {
+    int* a;
+    short* b;
+  } u;
+  u.a = param;
+  short* p = u.b;
+  return *p;
+}