[Tinyos-devel] Will safe protect this kind of code?

[John Regehr]

> How does deputy handle the possibility of a NULL being erroneously enqueued
> whichthen causes the variable current_thread to go null on the dqueue?

Probably it is possible to annotate the queue as containing non-null 
pointers.

> Is there something that give this kind of information about deputy and safe?
> Where should I
> start?

Please see the documentation here:

   http://www.cs.utah.edu/~coop/safetinyos/

In particular, follow the pointers to the Deputy docs (but note that we 
use slightly different annotations than the standard ones).

This documentation is a work in progress, feedback appreciated.

John Regehr