[pulse][isl] abduction for null case

Reviewed By: skcho

Differential Revision: D27595100

fbshipit-source-id: 1e75c9d30
master
Loc Le 4 years ago committed by Facebook GitHub Bot
parent 3d4b3ab4be
commit a89d88063d

@ -362,9 +362,7 @@ module AddressAttributes = struct
Attribute.Invalid (Invalidation.ConstantDereference IntLit.zero, access_trace) Attribute.Invalid (Invalidation.ConstantDereference IntLit.zero, access_trace)
in in
let null_astate = add_one addr null_attr astate in let null_astate = add_one addr null_attr astate in
let null_astate = let null_astate = abduce_attribute addr null_attr null_astate in
if is_eq_null then null_astate else abduce_attribute addr null_attr null_astate
in
if null_noop then [Ok null_astate] else [Error (`ISLError null_astate)] if null_noop then [Ok null_astate] else [Error (`ISLError null_astate)]
in in
if is_eq_null then null_astates if is_eq_null then null_astates

Loading…
Cancel
Save