Re: [PATCH] tools/memory-model: Document herd7 (internal) representation

[Andrea Parri]

> > $ cat T.litmus 
> > C T
> > 
> > {}
> > 
> > P0(spinlock_t *x)
> > {
> > 	int r0;
> > 
> > 	spin_lock(x);
> > 	spin_unlock(x);
> > 	r0 = spin_is_locked(x);
> > }
> 
> No "exists" clause?  Maybe that's your problem.

Nope, that doesn't seem to be it.  (Same result after adding one.)

  Andrea