int create_window_handle(int x);
void WIN_ReleasePtr(int x);
void EnterCriticalSection(int x);
void LeaveCriticalSection(int x);
void USER_Lock(void);
void USER_Unlock(void);
int GDI_GetObjPtr(int x);
void GDI_ReleaseObj(int x);

int a, b, c, d, e, z;

void test1(void)
{
	b = create_window_handle(a);
	z = frob();

	if (d = GDI_GetObjPtr(e))
		GDI_ReleaseObj(e);
	if (GDI_GetObjPtr(e))
		GDI_ReleaseObj(e);
	EnterCriticalSection(c);
	USER_Lock();
	if (b) {
		LeaveCriticalSection(c);
		WIN_ReleasePtr(b);
	}
	WIN_ReleasePtr(b);
	if (z)
		return;
	USER_Unlock();
	if (!b)
		LeaveCriticalSection(c);
}
/*
 * check-name: WINE locking
 * check-command: smatch -p=wine --spammy sm_wine_locking.c
 *
 * check-output-start
sm_wine_locking.c:27 test1() error: double unlock 'create_window_handle:b'
sm_wine_locking.c:29 test1() warn: 'CriticalSection:c' is sometimes locked here and sometimes unlocked.
sm_wine_locking.c:32 test1() warn: inconsistent returns 'USER_Lock:'.
  Locked on:   line 29
  Unlocked on: line 32
 * check-output-end
 */