/* MYBINARYNAME only works because our pathname usually includes 'model' (e.g.,
* /.../model-checker/test/userprog.o) */
/* MYBINARYNAME only works because our pathname usually includes 'model' (e.g.,
* /.../model-checker/test/userprog.o) */
/** This method returns to the last snapshot before the inputted
* sequence number. This function must be called from the model
* checking thread and not from a snapshotted stack.
/** This method returns to the last snapshot before the inputted
* sequence number. This function must be called from the model
* checking thread and not from a snapshotted stack.
/** This method takes a snapshot at the given sequence number. */
void SnapshotStack::snapshotStep(int seqindex)
{
/** This method takes a snapshot at the given sequence number. */
void SnapshotStack::snapshotStep(int seqindex)
{