10 December 2001
David Larochelle
11
Overview of checking
•Intraprocedural
–But use annotations on called
procedures and global variables to check calls, entry, exit
points
•Expressions generate constraints
–C
semantics, annotations
•Axiomatic
semantics propagates constraints
•Simplifying
rules (e.g.
maxRead(str+i) ==> maxRead(str) - i)
•Produce
warnings for unresolved constraints