int foo(bar) /*@modifies *bar*/ int *bar; { return 3; }