Lackwit’s type system
•Lackwit ignores the C type declarations
•Computes new types in a richer type system
char*
strcpy(char* dest,char* source)
(numa refb, num a refg) ®f num a refb
Implies
–Result may be
aliased with dest (flow between pointers)
–Values may
flow between the characters of the parameters
–No flow
between source and dest arguments (no
aliasing)