Project

General

Profile

Download (26.7 KB)

Bug #4396 » 0032.tmpl.aspect.i

Evgeny Novikov, 07/27/2013 07:56 PM

 
# 1 "/work/novikov/test/work/current--X--drivers--X--defaultlinux-3.10-rc1.tar--X--32_7a/linux-3.10-rc1.tar/csd_deg_dscv/5460/dscv_tempdir/rule-instrumentor/32_7a/0032.tmpl.aspect"
# 1 "<built-in>"
# 1 "<command-line>"
# 1 "/home/novikov/work/ldv-tools-inst/ri/ri.aspect" 1
# 1 "<command-line>" 2
# 1 "/work/novikov/test/work/current--X--drivers--X--defaultlinux-3.10-rc1.tar--X--32_7a/linux-3.10-rc1.tar/csd_deg_dscv/5460/dscv_tempdir/rule-instrumentor/32_7a/0032.tmpl.aspect"
before: file ("$this")
{
#include <linux/kernel.h>
#include <linux/mutex.h>

extern int mutex_lock_interruptible(struct mutex *lock);
extern int mutex_lock_killable(struct mutex *lock);
extern void mutex_lock(struct mutex *lock);
extern int ldv_mutex_lock_interruptible_lock(struct mutex *lock);
extern int ldv_mutex_lock_killable_lock(struct mutex *lock);
extern void ldv_mutex_lock_nested_lock(struct mutex *lock, unsigned int subclass);
extern void ldv_mutex_lock_lock(struct mutex *lock);
extern int ldv_mutex_trylock_lock(struct mutex *lock);
extern int ldv_atomic_dec_and_mutex_lock_lock(atomic_t *cnt, struct mutex *lock);
extern int ldv_mutex_is_locked_lock(struct mutex *lock);
extern void ldv_mutex_unlock_lock(struct mutex *lock);
extern int ldv_mutex_lock_interruptible_mutex_of_device(struct mutex *lock);
extern int ldv_mutex_lock_killable_mutex_of_device(struct mutex *lock);
extern void ldv_mutex_lock_nested_mutex_of_device(struct mutex *lock, unsigned int subclass);
extern void ldv_mutex_lock_mutex_of_device(struct mutex *lock);
extern int ldv_mutex_trylock_mutex_of_device(struct mutex *lock);
extern int ldv_atomic_dec_and_mutex_lock_mutex_of_device(atomic_t *cnt, struct mutex *lock);
extern int ldv_mutex_is_locked_mutex_of_device(struct mutex *lock);
extern void ldv_mutex_unlock_mutex_of_device(struct mutex *lock);
extern int ldv_mutex_lock_interruptible_mutex_of_ffs_data(struct mutex *lock);
extern int ldv_mutex_lock_killable_mutex_of_ffs_data(struct mutex *lock);
extern void ldv_mutex_lock_nested_mutex_of_ffs_data(struct mutex *lock, unsigned int subclass);
extern void ldv_mutex_lock_mutex_of_ffs_data(struct mutex *lock);
extern int ldv_mutex_trylock_mutex_of_ffs_data(struct mutex *lock);
extern int ldv_atomic_dec_and_mutex_lock_mutex_of_ffs_data(atomic_t *cnt, struct mutex *lock);
extern int ldv_mutex_is_locked_mutex_of_ffs_data(struct mutex *lock);
extern void ldv_mutex_unlock_mutex_of_ffs_data(struct mutex *lock);
extern int ldv_mutex_lock_interruptible_mutex_of_ffs_epfile(struct mutex *lock);
extern int ldv_mutex_lock_killable_mutex_of_ffs_epfile(struct mutex *lock);
extern void ldv_mutex_lock_nested_mutex_of_ffs_epfile(struct mutex *lock, unsigned int subclass);
extern void ldv_mutex_lock_mutex_of_ffs_epfile(struct mutex *lock);
extern int ldv_mutex_trylock_mutex_of_ffs_epfile(struct mutex *lock);
extern int ldv_atomic_dec_and_mutex_lock_mutex_of_ffs_epfile(atomic_t *cnt, struct mutex *lock);
extern int ldv_mutex_is_locked_mutex_of_ffs_epfile(struct mutex *lock);
extern void ldv_mutex_unlock_mutex_of_ffs_epfile(struct mutex *lock);
}


around: define(mutex_lock_interruptible(lock))
{
mutex_lock_interruptible(lock)
}

around: define(mutex_lock_killable(lock))
{
mutex_lock_killable(lock)
}

around: define(mutex_lock(lock))
{
mutex_lock(lock)
}

after: call(int mutex_lock_interruptible(struct mutex *))
{
return ldv_mutex_lock_interruptible_$arg_sign1($arg1);
}

after: call(int mutex_lock_killable(struct mutex *))
{
return ldv_mutex_lock_killable_$arg_sign1($arg1);
}

/* mutex_lock_nested is treated like mutex_lock. This model is required because
of mutex_lock_nested is a function if CONFIG_DEBUG_LOCK_ALLOC is true (see
#3324 and #785 for details). */
before: call(void mutex_lock_nested(struct mutex *, unsigned int))
{
ldv_mutex_lock_$arg_sign1($arg1);
}

before: call(void mutex_lock(struct mutex *))
{
ldv_mutex_lock_$arg_sign1($arg1);
}

after: call(int mutex_trylock(struct mutex *))
{
return ldv_mutex_trylock_$arg_sign1($arg1);
}

after: call(int atomic_dec_and_mutex_lock(..))
{
return ldv_atomic_dec_and_mutex_lock_$arg_sign1($arg1, $arg2);
}

after: call(static inline int mutex_is_locked(struct mutex *))
{
return ldv_mutex_is_locked_$arg_sign1($arg1);
}

before: call(void mutex_unlock(struct mutex *))
{
ldv_mutex_unlock_$arg_sign1($arg1);
}

around: call(static inline int kref_put_mutex(..))
{
if ($arg_value2) {
ldv_mutex_lock_$arg_sign3($arg3);
$arg_value2($arg1);
return 1;
} else return 0;
}


new: file("$env<LDV_COMMON_MODEL>")
{

#include <linux/kernel.h>
#include <linux/mutex.h>

#include <verifier/rcv.h>

static int ldv_mutex_lock;

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_mutex_lock_interruptible_lock') Check that mutex 'lock' was unlocked and nondeterministically lock it. Return the corresponding error code on fails */
int ldv_mutex_lock_interruptible_lock(struct mutex *lock)
{
int nondetermined;

/* LDV_COMMENT_ASSERT Mutex 'lock' must be unlocked */
ldv_assert(ldv_mutex_lock == 1);

/* LDV_COMMENT_OTHER Construct nondetermined result*/
nondetermined = ldv_undef_int();

/* LDV_COMMENT_ASSERT Nondeterministically lock mutex 'lock' */
if (nondetermined)
{
/* LDV_COMMENT_CHANGE_STATE Lock mutex 'lock' */
ldv_mutex_lock = 2;
/* LDV_COMMENT_RETURN Finish with success */
return 0;
}
else
{
/* LDV_COMMENT_RETURN Finish with fail. Mutex 'lock' is keeped unlocked */
return -EINTR;
}
}

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_mutex_lock_killable_lock') Check that mutex 'lock' wasn unlocked and nondeterministically lock it. Return the corresponding error code on fails*/
int ldv_mutex_lock_killable_lock(struct mutex *lock)
{
int nondetermined;

/* LDV_COMMENT_ASSERT Mutex 'lock' must be unlocked */
ldv_assert(ldv_mutex_lock == 1);

/* LDV_COMMENT_OTHER Construct nondetermined result */
nondetermined = ldv_undef_int();

/* LDV_COMMENT_ASSERT Nondeterministically lock mutex 'lock' */
if (nondetermined)
{
/* LDV_COMMENT_CHANGE_STATE Lock mutex 'lock' */
ldv_mutex_lock = 2;
/* LDV_COMMENT_RETURN Finish with success*/
return 0;
}
else
{
/* LDV_COMMENT_RETURN Finish with the fail. Mutex 'lock' is keeped unlocked */
return -EINTR;
}
}

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_mutex_lock_lock') Check that mutex 'lock' was not locked and lock it */
void ldv_mutex_lock_lock(struct mutex *lock)
{
/* LDV_COMMENT_ASSERT Mutex 'lock' must be unlocked */
ldv_assert(ldv_mutex_lock == 1);
/* LDV_COMMENT_CHANGE_STATE Lock mutex 'lock' */
ldv_mutex_lock = 2;
}

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_mutex_trylock_lock') Check that mutex 'lock' was not locked and nondeterministically lock it. Return 0 on fails */
int ldv_mutex_trylock_lock(struct mutex *lock)
{
int is_mutex_held_by_another_thread;

/* LDV_COMMENT_ASSERT It may be an error if mutex 'lock' is locked at this point */
ldv_assert(ldv_mutex_lock == 1);

/* LDV_COMMENT_OTHER Construct nondetermined result */
is_mutex_held_by_another_thread = ldv_undef_int();

/* LDV_COMMENT_ASSERT Nondeterministically lock mutex 'lock' */
if (is_mutex_held_by_another_thread)
{
/* LDV_COMMENT_RETURN Finish with fail */
return 0;
}
else
{
/* LDV_COMMENT_CHANGE_STATE Lock mutex 'lock' */
ldv_mutex_lock = 2;
/* LDV_COMMENT_RETURN Finish with success */
return 1;
}
}

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_atomic_dec_and_mutex_lock_lock') Lock mutex 'lock' if atomic decrement result is zero */
int ldv_atomic_dec_and_mutex_lock_lock(atomic_t *cnt, struct mutex *lock)
{
int atomic_value_after_dec;

/* LDV_COMMENT_ASSERT Mutex 'lock' must be unlocked (since we may lock it in this function) */
ldv_assert(ldv_mutex_lock == 1);

/* LDV_COMMENT_OTHER Assign the result of atomic decrement */
atomic_value_after_dec = ldv_undef_int();

/* LDV_COMMENT_ASSERT Check if atomic decrement returns zero */
if (atomic_value_after_dec == 0)
{
/* LDV_COMMENT_CHANGE_STATE Lock mutex 'lock', as atomic has decremented to zero */
ldv_mutex_lock = 2;
/* LDV_COMMENT_RETURN Return 1 with locked mutex 'lock' */
return 1;
}

/* LDV_COMMENT_RETURN Atomic decrement is still not zero, return 0 without locking mutex 'lock' */
return 0;
}

/* TODO Syncronize with 39_7a ldv_spin_is_locked! */
/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_mutex_is_locked_lock') Check whether mutex 'lock' was locked */
int ldv_mutex_is_locked_lock(struct mutex *lock)
{
int nondetermined;

if(ldv_mutex_lock == 1)
{
/* LDV_COMMENT_OTHER Construct nondetermined result */
nondetermined = ldv_undef_int();

/* LDV_COMMENT_ASSERT Nondeterministically understand whether mutex 'lock' was locked */
if(nondetermined)
{
/* LDV_COMMENT_RETURN Mutex 'lock' was unlocked */
return 0;
}
else
{
/* LDV_COMMENT_RETURN Mutex 'lock' was locked */
return 1;
}
}
else
{
/* LDV_COMMENT_RETURN Mutex 'lock' was locked */
return 1;
}
}

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_mutex_unlock_lock') Check that mutex 'lock' was locked and unlock it */
void ldv_mutex_unlock_lock(struct mutex *lock)
{
/* LDV_COMMENT_ASSERT Mutex 'lock' must be locked */
ldv_assert(ldv_mutex_lock == 2);
/* LDV_COMMENT_CHANGE_STATE Unlock mutex 'lock' */
ldv_mutex_lock = 1;
}

static int ldv_mutex_mutex_of_device;

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_mutex_lock_interruptible_mutex_of_device') Check that mutex 'mutex_of_device' was unlocked and nondeterministically lock it. Return the corresponding error code on fails */
int ldv_mutex_lock_interruptible_mutex_of_device(struct mutex *lock)
{
int nondetermined;

/* LDV_COMMENT_ASSERT Mutex 'mutex_of_device' must be unlocked */
ldv_assert(ldv_mutex_mutex_of_device == 1);

/* LDV_COMMENT_OTHER Construct nondetermined result*/
nondetermined = ldv_undef_int();

/* LDV_COMMENT_ASSERT Nondeterministically lock mutex 'mutex_of_device' */
if (nondetermined)
{
/* LDV_COMMENT_CHANGE_STATE Lock mutex 'mutex_of_device' */
ldv_mutex_mutex_of_device = 2;
/* LDV_COMMENT_RETURN Finish with success */
return 0;
}
else
{
/* LDV_COMMENT_RETURN Finish with fail. Mutex 'mutex_of_device' is keeped unlocked */
return -EINTR;
}
}

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_mutex_lock_killable_mutex_of_device') Check that mutex 'mutex_of_device' wasn unlocked and nondeterministically lock it. Return the corresponding error code on fails*/
int ldv_mutex_lock_killable_mutex_of_device(struct mutex *lock)
{
int nondetermined;

/* LDV_COMMENT_ASSERT Mutex 'mutex_of_device' must be unlocked */
ldv_assert(ldv_mutex_mutex_of_device == 1);

/* LDV_COMMENT_OTHER Construct nondetermined result */
nondetermined = ldv_undef_int();

/* LDV_COMMENT_ASSERT Nondeterministically lock mutex 'mutex_of_device' */
if (nondetermined)
{
/* LDV_COMMENT_CHANGE_STATE Lock mutex 'mutex_of_device' */
ldv_mutex_mutex_of_device = 2;
/* LDV_COMMENT_RETURN Finish with success*/
return 0;
}
else
{
/* LDV_COMMENT_RETURN Finish with the fail. Mutex 'mutex_of_device' is keeped unlocked */
return -EINTR;
}
}

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_mutex_lock_mutex_of_device') Check that mutex 'mutex_of_device' was not locked and lock it */
void ldv_mutex_lock_mutex_of_device(struct mutex *lock)
{
/* LDV_COMMENT_ASSERT Mutex 'mutex_of_device' must be unlocked */
ldv_assert(ldv_mutex_mutex_of_device == 1);
/* LDV_COMMENT_CHANGE_STATE Lock mutex 'mutex_of_device' */
ldv_mutex_mutex_of_device = 2;
}

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_mutex_trylock_mutex_of_device') Check that mutex 'mutex_of_device' was not locked and nondeterministically lock it. Return 0 on fails */
int ldv_mutex_trylock_mutex_of_device(struct mutex *lock)
{
int is_mutex_held_by_another_thread;

/* LDV_COMMENT_ASSERT It may be an error if mutex 'mutex_of_device' is locked at this point */
ldv_assert(ldv_mutex_mutex_of_device == 1);

/* LDV_COMMENT_OTHER Construct nondetermined result */
is_mutex_held_by_another_thread = ldv_undef_int();

/* LDV_COMMENT_ASSERT Nondeterministically lock mutex 'mutex_of_device' */
if (is_mutex_held_by_another_thread)
{
/* LDV_COMMENT_RETURN Finish with fail */
return 0;
}
else
{
/* LDV_COMMENT_CHANGE_STATE Lock mutex 'mutex_of_device' */
ldv_mutex_mutex_of_device = 2;
/* LDV_COMMENT_RETURN Finish with success */
return 1;
}
}

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_atomic_dec_and_mutex_lock_mutex_of_device') Lock mutex 'mutex_of_device' if atomic decrement result is zero */
int ldv_atomic_dec_and_mutex_lock_mutex_of_device(atomic_t *cnt, struct mutex *lock)
{
int atomic_value_after_dec;

/* LDV_COMMENT_ASSERT Mutex 'mutex_of_device' must be unlocked (since we may lock it in this function) */
ldv_assert(ldv_mutex_mutex_of_device == 1);

/* LDV_COMMENT_OTHER Assign the result of atomic decrement */
atomic_value_after_dec = ldv_undef_int();

/* LDV_COMMENT_ASSERT Check if atomic decrement returns zero */
if (atomic_value_after_dec == 0)
{
/* LDV_COMMENT_CHANGE_STATE Lock mutex 'mutex_of_device', as atomic has decremented to zero */
ldv_mutex_mutex_of_device = 2;
/* LDV_COMMENT_RETURN Return 1 with locked mutex 'mutex_of_device' */
return 1;
}

/* LDV_COMMENT_RETURN Atomic decrement is still not zero, return 0 without locking mutex 'mutex_of_device' */
return 0;
}

/* TODO Syncronize with 39_7a ldv_spin_is_locked! */
/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_mutex_is_locked_mutex_of_device') Check whether mutex 'mutex_of_device' was locked */
int ldv_mutex_is_locked_mutex_of_device(struct mutex *lock)
{
int nondetermined;

if(ldv_mutex_mutex_of_device == 1)
{
/* LDV_COMMENT_OTHER Construct nondetermined result */
nondetermined = ldv_undef_int();

/* LDV_COMMENT_ASSERT Nondeterministically understand whether mutex 'mutex_of_device' was locked */
if(nondetermined)
{
/* LDV_COMMENT_RETURN Mutex 'mutex_of_device' was unlocked */
return 0;
}
else
{
/* LDV_COMMENT_RETURN Mutex 'mutex_of_device' was locked */
return 1;
}
}
else
{
/* LDV_COMMENT_RETURN Mutex 'mutex_of_device' was locked */
return 1;
}
}

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_mutex_unlock_mutex_of_device') Check that mutex 'mutex_of_device' was locked and unlock it */
void ldv_mutex_unlock_mutex_of_device(struct mutex *lock)
{
/* LDV_COMMENT_ASSERT Mutex 'mutex_of_device' must be locked */
ldv_assert(ldv_mutex_mutex_of_device == 2);
/* LDV_COMMENT_CHANGE_STATE Unlock mutex 'mutex_of_device' */
ldv_mutex_mutex_of_device = 1;
}

static int ldv_mutex_mutex_of_ffs_data;

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_mutex_lock_interruptible_mutex_of_ffs_data') Check that mutex 'mutex_of_ffs_data' was unlocked and nondeterministically lock it. Return the corresponding error code on fails */
int ldv_mutex_lock_interruptible_mutex_of_ffs_data(struct mutex *lock)
{
int nondetermined;

/* LDV_COMMENT_ASSERT Mutex 'mutex_of_ffs_data' must be unlocked */
ldv_assert(ldv_mutex_mutex_of_ffs_data == 1);

/* LDV_COMMENT_OTHER Construct nondetermined result*/
nondetermined = ldv_undef_int();

/* LDV_COMMENT_ASSERT Nondeterministically lock mutex 'mutex_of_ffs_data' */
if (nondetermined)
{
/* LDV_COMMENT_CHANGE_STATE Lock mutex 'mutex_of_ffs_data' */
ldv_mutex_mutex_of_ffs_data = 2;
/* LDV_COMMENT_RETURN Finish with success */
return 0;
}
else
{
/* LDV_COMMENT_RETURN Finish with fail. Mutex 'mutex_of_ffs_data' is keeped unlocked */
return -EINTR;
}
}

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_mutex_lock_killable_mutex_of_ffs_data') Check that mutex 'mutex_of_ffs_data' wasn unlocked and nondeterministically lock it. Return the corresponding error code on fails*/
int ldv_mutex_lock_killable_mutex_of_ffs_data(struct mutex *lock)
{
int nondetermined;

/* LDV_COMMENT_ASSERT Mutex 'mutex_of_ffs_data' must be unlocked */
ldv_assert(ldv_mutex_mutex_of_ffs_data == 1);

/* LDV_COMMENT_OTHER Construct nondetermined result */
nondetermined = ldv_undef_int();

/* LDV_COMMENT_ASSERT Nondeterministically lock mutex 'mutex_of_ffs_data' */
if (nondetermined)
{
/* LDV_COMMENT_CHANGE_STATE Lock mutex 'mutex_of_ffs_data' */
ldv_mutex_mutex_of_ffs_data = 2;
/* LDV_COMMENT_RETURN Finish with success*/
return 0;
}
else
{
/* LDV_COMMENT_RETURN Finish with the fail. Mutex 'mutex_of_ffs_data' is keeped unlocked */
return -EINTR;
}
}

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_mutex_lock_mutex_of_ffs_data') Check that mutex 'mutex_of_ffs_data' was not locked and lock it */
void ldv_mutex_lock_mutex_of_ffs_data(struct mutex *lock)
{
/* LDV_COMMENT_ASSERT Mutex 'mutex_of_ffs_data' must be unlocked */
ldv_assert(ldv_mutex_mutex_of_ffs_data == 1);
/* LDV_COMMENT_CHANGE_STATE Lock mutex 'mutex_of_ffs_data' */
ldv_mutex_mutex_of_ffs_data = 2;
}

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_mutex_trylock_mutex_of_ffs_data') Check that mutex 'mutex_of_ffs_data' was not locked and nondeterministically lock it. Return 0 on fails */
int ldv_mutex_trylock_mutex_of_ffs_data(struct mutex *lock)
{
int is_mutex_held_by_another_thread;

/* LDV_COMMENT_ASSERT It may be an error if mutex 'mutex_of_ffs_data' is locked at this point */
ldv_assert(ldv_mutex_mutex_of_ffs_data == 1);

/* LDV_COMMENT_OTHER Construct nondetermined result */
is_mutex_held_by_another_thread = ldv_undef_int();

/* LDV_COMMENT_ASSERT Nondeterministically lock mutex 'mutex_of_ffs_data' */
if (is_mutex_held_by_another_thread)
{
/* LDV_COMMENT_RETURN Finish with fail */
return 0;
}
else
{
/* LDV_COMMENT_CHANGE_STATE Lock mutex 'mutex_of_ffs_data' */
ldv_mutex_mutex_of_ffs_data = 2;
/* LDV_COMMENT_RETURN Finish with success */
return 1;
}
}

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_atomic_dec_and_mutex_lock_mutex_of_ffs_data') Lock mutex 'mutex_of_ffs_data' if atomic decrement result is zero */
int ldv_atomic_dec_and_mutex_lock_mutex_of_ffs_data(atomic_t *cnt, struct mutex *lock)
{
int atomic_value_after_dec;

/* LDV_COMMENT_ASSERT Mutex 'mutex_of_ffs_data' must be unlocked (since we may lock it in this function) */
ldv_assert(ldv_mutex_mutex_of_ffs_data == 1);

/* LDV_COMMENT_OTHER Assign the result of atomic decrement */
atomic_value_after_dec = ldv_undef_int();

/* LDV_COMMENT_ASSERT Check if atomic decrement returns zero */
if (atomic_value_after_dec == 0)
{
/* LDV_COMMENT_CHANGE_STATE Lock mutex 'mutex_of_ffs_data', as atomic has decremented to zero */
ldv_mutex_mutex_of_ffs_data = 2;
/* LDV_COMMENT_RETURN Return 1 with locked mutex 'mutex_of_ffs_data' */
return 1;
}

/* LDV_COMMENT_RETURN Atomic decrement is still not zero, return 0 without locking mutex 'mutex_of_ffs_data' */
return 0;
}

/* TODO Syncronize with 39_7a ldv_spin_is_locked! */
/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_mutex_is_locked_mutex_of_ffs_data') Check whether mutex 'mutex_of_ffs_data' was locked */
int ldv_mutex_is_locked_mutex_of_ffs_data(struct mutex *lock)
{
int nondetermined;

if(ldv_mutex_mutex_of_ffs_data == 1)
{
/* LDV_COMMENT_OTHER Construct nondetermined result */
nondetermined = ldv_undef_int();

/* LDV_COMMENT_ASSERT Nondeterministically understand whether mutex 'mutex_of_ffs_data' was locked */
if(nondetermined)
{
/* LDV_COMMENT_RETURN Mutex 'mutex_of_ffs_data' was unlocked */
return 0;
}
else
{
/* LDV_COMMENT_RETURN Mutex 'mutex_of_ffs_data' was locked */
return 1;
}
}
else
{
/* LDV_COMMENT_RETURN Mutex 'mutex_of_ffs_data' was locked */
return 1;
}
}

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_mutex_unlock_mutex_of_ffs_data') Check that mutex 'mutex_of_ffs_data' was locked and unlock it */
void ldv_mutex_unlock_mutex_of_ffs_data(struct mutex *lock)
{
/* LDV_COMMENT_ASSERT Mutex 'mutex_of_ffs_data' must be locked */
ldv_assert(ldv_mutex_mutex_of_ffs_data == 2);
/* LDV_COMMENT_CHANGE_STATE Unlock mutex 'mutex_of_ffs_data' */
ldv_mutex_mutex_of_ffs_data = 1;
}

static int ldv_mutex_mutex_of_ffs_epfile;

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_mutex_lock_interruptible_mutex_of_ffs_epfile') Check that mutex 'mutex_of_ffs_epfile' was unlocked and nondeterministically lock it. Return the corresponding error code on fails */
int ldv_mutex_lock_interruptible_mutex_of_ffs_epfile(struct mutex *lock)
{
int nondetermined;

/* LDV_COMMENT_ASSERT Mutex 'mutex_of_ffs_epfile' must be unlocked */
ldv_assert(ldv_mutex_mutex_of_ffs_epfile == 1);

/* LDV_COMMENT_OTHER Construct nondetermined result*/
nondetermined = ldv_undef_int();

/* LDV_COMMENT_ASSERT Nondeterministically lock mutex 'mutex_of_ffs_epfile' */
if (nondetermined)
{
/* LDV_COMMENT_CHANGE_STATE Lock mutex 'mutex_of_ffs_epfile' */
ldv_mutex_mutex_of_ffs_epfile = 2;
/* LDV_COMMENT_RETURN Finish with success */
return 0;
}
else
{
/* LDV_COMMENT_RETURN Finish with fail. Mutex 'mutex_of_ffs_epfile' is keeped unlocked */
return -EINTR;
}
}

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_mutex_lock_killable_mutex_of_ffs_epfile') Check that mutex 'mutex_of_ffs_epfile' wasn unlocked and nondeterministically lock it. Return the corresponding error code on fails*/
int ldv_mutex_lock_killable_mutex_of_ffs_epfile(struct mutex *lock)
{
int nondetermined;

/* LDV_COMMENT_ASSERT Mutex 'mutex_of_ffs_epfile' must be unlocked */
ldv_assert(ldv_mutex_mutex_of_ffs_epfile == 1);

/* LDV_COMMENT_OTHER Construct nondetermined result */
nondetermined = ldv_undef_int();

/* LDV_COMMENT_ASSERT Nondeterministically lock mutex 'mutex_of_ffs_epfile' */
if (nondetermined)
{
/* LDV_COMMENT_CHANGE_STATE Lock mutex 'mutex_of_ffs_epfile' */
ldv_mutex_mutex_of_ffs_epfile = 2;
/* LDV_COMMENT_RETURN Finish with success*/
return 0;
}
else
{
/* LDV_COMMENT_RETURN Finish with the fail. Mutex 'mutex_of_ffs_epfile' is keeped unlocked */
return -EINTR;
}
}

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_mutex_lock_mutex_of_ffs_epfile') Check that mutex 'mutex_of_ffs_epfile' was not locked and lock it */
void ldv_mutex_lock_mutex_of_ffs_epfile(struct mutex *lock)
{
/* LDV_COMMENT_ASSERT Mutex 'mutex_of_ffs_epfile' must be unlocked */
ldv_assert(ldv_mutex_mutex_of_ffs_epfile == 1);
/* LDV_COMMENT_CHANGE_STATE Lock mutex 'mutex_of_ffs_epfile' */
ldv_mutex_mutex_of_ffs_epfile = 2;
}

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_mutex_trylock_mutex_of_ffs_epfile') Check that mutex 'mutex_of_ffs_epfile' was not locked and nondeterministically lock it. Return 0 on fails */
int ldv_mutex_trylock_mutex_of_ffs_epfile(struct mutex *lock)
{
int is_mutex_held_by_another_thread;

/* LDV_COMMENT_ASSERT It may be an error if mutex 'mutex_of_ffs_epfile' is locked at this point */
ldv_assert(ldv_mutex_mutex_of_ffs_epfile == 1);

/* LDV_COMMENT_OTHER Construct nondetermined result */
is_mutex_held_by_another_thread = ldv_undef_int();

/* LDV_COMMENT_ASSERT Nondeterministically lock mutex 'mutex_of_ffs_epfile' */
if (is_mutex_held_by_another_thread)
{
/* LDV_COMMENT_RETURN Finish with fail */
return 0;
}
else
{
/* LDV_COMMENT_CHANGE_STATE Lock mutex 'mutex_of_ffs_epfile' */
ldv_mutex_mutex_of_ffs_epfile = 2;
/* LDV_COMMENT_RETURN Finish with success */
return 1;
}
}

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_atomic_dec_and_mutex_lock_mutex_of_ffs_epfile') Lock mutex 'mutex_of_ffs_epfile' if atomic decrement result is zero */
int ldv_atomic_dec_and_mutex_lock_mutex_of_ffs_epfile(atomic_t *cnt, struct mutex *lock)
{
int atomic_value_after_dec;

/* LDV_COMMENT_ASSERT Mutex 'mutex_of_ffs_epfile' must be unlocked (since we may lock it in this function) */
ldv_assert(ldv_mutex_mutex_of_ffs_epfile == 1);

/* LDV_COMMENT_OTHER Assign the result of atomic decrement */
atomic_value_after_dec = ldv_undef_int();

/* LDV_COMMENT_ASSERT Check if atomic decrement returns zero */
if (atomic_value_after_dec == 0)
{
/* LDV_COMMENT_CHANGE_STATE Lock mutex 'mutex_of_ffs_epfile', as atomic has decremented to zero */
ldv_mutex_mutex_of_ffs_epfile = 2;
/* LDV_COMMENT_RETURN Return 1 with locked mutex 'mutex_of_ffs_epfile' */
return 1;
}

/* LDV_COMMENT_RETURN Atomic decrement is still not zero, return 0 without locking mutex 'mutex_of_ffs_epfile' */
return 0;
}

/* TODO Syncronize with 39_7a ldv_spin_is_locked! */
/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_mutex_is_locked_mutex_of_ffs_epfile') Check whether mutex 'mutex_of_ffs_epfile' was locked */
int ldv_mutex_is_locked_mutex_of_ffs_epfile(struct mutex *lock)
{
int nondetermined;

if(ldv_mutex_mutex_of_ffs_epfile == 1)
{
/* LDV_COMMENT_OTHER Construct nondetermined result */
nondetermined = ldv_undef_int();

/* LDV_COMMENT_ASSERT Nondeterministically understand whether mutex 'mutex_of_ffs_epfile' was locked */
if(nondetermined)
{
/* LDV_COMMENT_RETURN Mutex 'mutex_of_ffs_epfile' was unlocked */
return 0;
}
else
{
/* LDV_COMMENT_RETURN Mutex 'mutex_of_ffs_epfile' was locked */
return 1;
}
}
else
{
/* LDV_COMMENT_RETURN Mutex 'mutex_of_ffs_epfile' was locked */
return 1;
}
}

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_mutex_unlock_mutex_of_ffs_epfile') Check that mutex 'mutex_of_ffs_epfile' was locked and unlock it */
void ldv_mutex_unlock_mutex_of_ffs_epfile(struct mutex *lock)
{
/* LDV_COMMENT_ASSERT Mutex 'mutex_of_ffs_epfile' must be locked */
ldv_assert(ldv_mutex_mutex_of_ffs_epfile == 2);
/* LDV_COMMENT_CHANGE_STATE Unlock mutex 'mutex_of_ffs_epfile' */
ldv_mutex_mutex_of_ffs_epfile = 1;
}


/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_initialize') Make all mutexes unlocked at the beginning */
void ldv_initialize(void)
{
/* LDV_COMMENT_CHANGE_STATE Make mutex 'lock' unlocked at the beginning */
ldv_mutex_lock = 1;
/* LDV_COMMENT_CHANGE_STATE Make mutex 'mutex_of_device' unlocked at the beginning */
ldv_mutex_mutex_of_device = 1;
/* LDV_COMMENT_CHANGE_STATE Make mutex 'mutex_of_ffs_data' unlocked at the beginning */
ldv_mutex_mutex_of_ffs_data = 1;
/* LDV_COMMENT_CHANGE_STATE Make mutex 'mutex_of_ffs_epfile' unlocked at the beginning */
ldv_mutex_mutex_of_ffs_epfile = 1;
}

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_check_final_state') Check that all mutexes are unlocked at the end */
void ldv_check_final_state(void)
{
/* LDV_COMMENT_ASSERT Mutex 'lock' must be unlocked at the end */
ldv_assert(ldv_mutex_lock == 1);
/* LDV_COMMENT_ASSERT Mutex 'mutex_of_device' must be unlocked at the end */
ldv_assert(ldv_mutex_mutex_of_device == 1);
/* LDV_COMMENT_ASSERT Mutex 'mutex_of_ffs_data' must be unlocked at the end */
ldv_assert(ldv_mutex_mutex_of_ffs_data == 1);
/* LDV_COMMENT_ASSERT Mutex 'mutex_of_ffs_epfile' must be unlocked at the end */
ldv_assert(ldv_mutex_mutex_of_ffs_epfile == 1);
}

}
(2-2/2)