int *a = 0; /*@null@*/ int* b = 0; /*@notnull@*/ int *c = 0;