[pulse] array indices need not be valid addresses

Summary:
This was bogus: when evaluating `e[e']` we were checking that `e'` is a
valid pointer.

Reviewed By: ezgicicek

Differential Revision: D17627727

fbshipit-source-id: 536384e95
master
Jules Villard 5 years ago committed by Facebook Github Bot
parent b6557ba2b4
commit c455ac02f4

@ -127,8 +127,6 @@ let eval location exp0 astate =
| Lindex (exp', exp_index) ->
eval exp_index astate
>>= fun (astate, addr_trace_index) ->
check_addr_access action addr_trace_index astate
>>= fun astate ->
eval exp' astate
>>= fun (astate, addr_trace) ->
check_addr_access action addr_trace astate

Loading…
Cancel
Save