@ find_drv_name @
identifier drv;
identifier mutex;
@@

pthread_mutex_protects_3(&drv->mutex, ...);

@ find_hint @
type T;
T *drv;
identifier mutex, item_1, item_2, item_3;
@@

pthread_mutex_protects_3(&drv->mutex, drv->item_1, drv->item_2, drv->item_3);

@ add_instrumentation_vars @
type find_hint.T;
identifier find_hint.mutex, find_hint.item_1, find_hint.item_2, find_hint.item_3;
type T1, T2;
fresh identifier instr_item_1 = "__instr_" ## item_1;
fresh identifier instr_item_2 = "__instr_" ## item_2;
fresh identifier instr_item_3 = "__instr_" ## item_3;
@@

T {
	...
+	int instr_item_1;
	T1 item_1;
	...
+	int instr_item_2;
	T2 item_2;
	...
+	int instr_item_3;
	T2 item_3;
	...
};

@ add_counter depends on add_instrumentation_vars @
type find_hint.T;
identifier find_hint.mutex, find_hint.item_1, find_hint.item_2, find_hint.item_3;
identifier find_drv_name.drv;
fresh identifier fn_instr = "__instr_" ## mutex;
@@

#include <string.h>
+
+T;
+static void fn_instr(T *drv)
+{
+}
+

@ find_pthread_fn depends on find_hint @
identifier fn, ret;
expression thread, attr, val;
@@

ret = pthread_create(thread, attr, fn, val);

@ check_fn_access @
identifier find_pthread_fn.fn;
type find_hint.T;
T *drv;
//identifier find_drv_name.drv;
identifier add_counter.fn_instr;
identifier find_hint.mutex;
identifier find_hint.item_1;
identifier find_hint.item_2;
identifier find_hint.item_3;
@@

fn (...)
{
	<+...
(
	drv->item_1
|
	drv->item_2
|
	drv->item_3
)
        ...+>
+
+	/* top level routine accesses drv */
+	fn_instr(drv);
+
}

@ check_helpers depends on find_pthread_fn @
identifier helper;
identifier find_pthread_fn.fn;
identifier find_hint.mutex;
type find_hint.T;
T *drv;
@@

fn (...)
{
	<+... when != pthread_mutex_lock(&drv->mutex);
+	/* going to check this routine */
	helper(...);
	...+>
}

@ helper_accessing_with_lock exists @
identifier check_helpers.helper;
type find_hint.T;
T *drv;
identifier find_hint.mutex;
identifier find_hint.item_1;
identifier find_hint.item_2;
identifier find_hint.item_3;
position p1, p2;
identifier add_counter.fn_instr;
@@

helper(...)
{
	...
	pthread_mutex_lock@p1(&drv->mutex);
	<+...
(
	drv->item_1
|
	drv->item_2
|
	drv->item_3
)
        ...+>
	pthread_mutex_unlock@p2(&drv->mutex);
+	/* routine had a lock */
+	fn_instr(drv);
}

@ helper_accessing_without_lock exists @
identifier check_helpers.helper;
type find_hint.T;
T *drv;
identifier find_hint.mutex;
identifier find_hint.item_1;
identifier find_hint.item_2;
identifier find_hint.item_3;
identifier add_counter.fn_instr;
@@

helper(...)
{
	<+... when != pthread_mutex_lock(&drv->mutex);
(
	drv->item_1
|
	drv->item_2
|
	drv->item_3
)
        ...+>
+	/* was missing lock */
+	fn_instr(drv);
}