Linux Driver Verification

This bug causes problems with rather new kernels. Such problems must be eliminated.

Before the rather old linux kernel of 2.6.33.1 version spin lock/unlock functionality was a macros to extern functions and all works good:

include/linux/spinlock.h
  ...
  #define spin_lock(lock) _spin_lock(lock)
  ...
kernel/spinlock.c
  ...  
  void __lockfunc _spin_lock(spinlock_t *lock)
  {
    __spin_lock(lock);
  }
  ...

Then almost all lock/unlock API became unconditional static inline functions like this:

include/linux/spinlock.h
  ...
  static inline void spin_lock(spinlock_t *lock)
  {
    raw_spin_lock(&lock->rlock);
  }
  ...

As we know without aspectator we can't add model functions directly for spin_lock and other static inline functions. The raw_spin_lock is just a macro:

include/linux/spinlock.h
  ...
  #define raw_spin_lock(lock) _raw_spin_lock(lock)
  ...

include/linux/spinlock_api_smp.h
  ...
  void __lockfunc _raw_spin_lock(raw_spinlock_t *lock) __acquires(lock);
  ...

model0039.c
  ... 
  void _spin_lock(spinlock_t *lock) {
    ldv_spin_lock(lock);
  }
  ...
  void _raw_spin_lock(raw_spinlock_t *lock) 
  {
    ldv_raw_spin_lock(lock);
  }
  ...

include/linux/spinlock.h
  ...
  extern void _raw_spin_lock(spinlock_t *lock);

Note that these internal prototypes and types depend on configuration in the tricky way and somebody of course may try to define such configuration that allows to use model both with "old" and "new" kernels. But this is a very complex task and it doesn't give the solution in general because we still won't be able to use model in case when there is no appropriate configuration.

So we assume another obvious solution. We have to make kernel depended models! If the problem just in dependence on the kernel version ("old" kernels have some API while "new" kernels have another API that may be not backward compatible) then we must to define our kernel "API" in depend on the processed kernel version.

The problem was fixed by means of adding '#ifdef' of spin_lock.
After fix three 'Parsing errors' from small regression test set (related with this problem in 39_1 model) becomes two unsafes and one safe.
So after all there is no more problems in small regression test set! Middle test may contain changes now, we'll them tomorrow.

Verified, so close it.