Statically Detecting Likely Buffer Overflow Vulnerablitites

10 December 2001

David Larochelle

8

Annotations

•requires, ensures

•maxSet

–highest index that can be safely written to

•maxRead

–highest index that can be safely read

•char buffer[100];

–ensures maxSet(buffer) == 99