Idea: range

[Finny Merrill]

I was thinking of having a /*@range ...@*/ clause for function parameters 
and return values, like:


void handle_ferror(int input /*@range 0-UCHAR_MAX, EOF@*/) { }