Linux Driver Verification » Linux Kernel Safety RuleDB

Bug #4448

Updated by Ilya Shchepetkov about 11 years ago

111_1a model contains a large number of __always_inline functions: 
 <pre> 
 before call(static __always_inline unsigned long __copy_to_user_inatomic(..)) 
 before call(static __always_inline int copy_to_user(..)) 
 before call(static inline int __copy_from_user_nocache(..)) 
 before call(static __always_inline unsigned long __copy_from_user_nocache(..)) 
 before call(static __always_inline unsigned long __copy_from_user_inatomic_nocache(..)) 
 ... 
 </pre> 
 Currently aspeсtator does not support __always_inline macro, and so these functions can't be instrumented. We should fix this.

Back