null derefs (2)

assert no null derefs

pre ? S ? proc ? -> ! Null in derefs’

interpreting results

find first state s such that s :: derefs contains Null

means null deref in that statement

Previous slide

Next slide

Back to first slide

View graphic version