Detection of locking one lock twice

[Petr Muller <afri@afri.cz>]

Hi,

I'm playing with sparse a bit, especially the context/locking problem
detecting stuff. I'm trying to create simple context updating
lock/unlock, everything works as I would expect except for this case
(I've reduced it as much as possible) :

#ifdef __CHECKER__
  #define __acquires(x) __attribute__((context (x, 0, 1)))
  #define __releases(x) __attribute__((context (x, 1, 0)))
  #define __acquire(x) __context__(x,1)
  #define __release(x) __context__(x,-1)
#else
(...)
#endif

(...)

void lock(void)
  __acquires(i)
{
  __acquire(i);
}

void unlock(void)
  __releases(i)
{
  __release(i);
}

void fction(int a)
{
  lock();
  lock();
  unlock();
  unlock();
}

int main(void){
  fction(1);
  return 0;
}

Sparse gives no warning in this code - I would expect that second call
to lock() would violate the 'in' limit of __acquires attribute, but it
does not. I'm wondering if this is actually a problem in sparse, or am I
doing something wrong? 

Thanks,

Petr