Q:

keep track of legal values

Assume two external functions init() and revoke(). Init() returns "valid" values, revoke() makes them invalid. I like to verify that use() only uses values which are initialized but not revoked. I don't know how to describe this property as predicate (think random session IDs) or otherwise.
#include <lib.h>

// "ensures valid_val(\result)"
extern int init();
extern revoke(int);

/*
 @ assigns \nothing;
 @ require valid_val(val);
 */
void use(int val) {
    ...
}

int main() {
    int v = init();
    use(v);
    revoke(v);
}

A:

It is indeed not possible to express this property as a single ACSL predicate. In fact, it depends on the whole execution of the program. The Aorai plug-in allows to express allowed sequences of function calls in the form of automata, but I'm afraid it cannot completely capture what you want. More precisely, it would not be able to express scenarios where the lifetime of the tokens overlap (but it would be completely sufficient for proving that the main function of your example is correct).
That said, with a little bit of instrumentation, it should be possible to come up with a general specification. A first trick would be to declare a (ghost) array whose cells are non zero iff the corresponding index is a valid token.
typedef int token;

/*@ ghost extern int valid_token[]; */

/*@ predicate is_valid(token t) = valid_token[t] != 0; */

/*@ 
  assigns valid_token[\at(\result,Post)];
  ensures is_valid(\result);
*/
extern token init();

/*@
  requires is_valid(t);
  assigns valid_token[t];
  ensures !is_valid(t);
*/
extern revoke(token t);

/*@
 @ requires is_valid(val);
 @ assigns \nothing;
 */
void use(token val) {

}

/*@ requires \forall token t; !is_valid(t); */
int main() {
    token v = init();
    use(v);
    revoke(v);
}

If the fact that we use an array with no defined size seems a bit fishy, an almost purely ACSL solution would be to use an undefined predicate whose truth value depends on a state that is modified by init and revoke, as in:
 typedef int token;

/*@ ghost int glob_state; */

/*@ axiomatic validity {
  predicate valid_token{L}(token t) reads glob_state;
}
*/

/*@ predicate unchanged_token{L1,L2}(token t) =
  \forall token t1; t!=t1 ==> 
  valid_token{L1}(t1) <==> valid_token{L2}(t1);
*/

/*@ 
  assigns glob_state;
  ensures valid_token(\result);
  ensures unchanged_token{Pre,Here}(\result);
*/
extern token init();

/*@
  requires valid_token(t);
  assigns glob_state;
  ensures !valid_token(t);
  ensures unchanged_token{Pre,Here}(t);
*/
extern revoke(token t);

/*@
 @ requires valid_token(val);
 @ assigns \nothing;
 */
void use(token val) {

}

/*@ requires \forall token t; !valid_token(t); */
int main() {
    token v = init();
    use(v);
    revoke(v);
}

functions that assign glob_state may modify the predicate. In fact, it changes only for one value of the argument, hence the auxiliary predicate that says that the validity of all tokens but one stays the same between L1 and L2.

