From 5cf86cc0c0b3aecc4813f640219b9288df5ee682 Mon Sep 17 00:00:00 2001
From: Loc Le <quangll@fb.com>
Date: Thu, 11 Feb 2021 09:49:49 -0800
Subject: [PATCH] [pulse.isl] init for local variables

Summary: added MustBeValid as init for local variables

Reviewed By: jvillard

Differential Revision: D26127799

fbshipit-source-id: 62eca94fa
---
 infer/src/pulse/PulseAbductiveDomain.ml | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml
index d454ba1c3..9659b863a 100644
--- a/infer/src/pulse/PulseAbductiveDomain.ml
+++ b/infer/src/pulse/PulseAbductiveDomain.ml
@@ -466,6 +466,11 @@ let rec set_uninitialized_post tenv src typ location (post : PostDomain.t) =
   | Tint _ | Tfloat _ | Tptr _ ->
       let {stack; attrs} = (post :> base_domain) in
       let stack, addr = add_edge_on_src src location stack in
+      let attrs =
+        if Config.pulse_isl then
+          BaseAddressAttributes.add_one addr (MustBeValid (Immediate {location; history= []})) attrs
+        else attrs
+      in
       let attrs = BaseAddressAttributes.add_one addr Uninitialized attrs in
       PostDomain.update ~stack ~attrs post
   | Tstruct typ_name when UninitBlocklist.is_blocklisted_struct typ_name ->