int * f1 () { return 0; } /*@null@*/ int * f2 () { return 0; } /*@notnull@*/ int * f3 () { return 0; }