Feature #3986
openCommon kernel core model for current and atomic_*
0%
Description
UNSAFE detected by CPAchecker SeqComb in fs/btrfs/btrfs.ko (linux-3.8-rc1) on rule '32_7a' is a false positive because lack of common kernel core model for current and atomic_* inline functions that are implemented in assembler.
I believe a model for these functions will be useful for all rules.
current can be modeled as a pointer to a global variable that is initialized by some proper values.
More correct design is to have two global variables and nondeterministically switch between them in main function between call of different handlers.
atomic_functions modes obviously are just nonatomic counterparts in C.
Updated by Evgeny Novikov over 11 years ago
- Project changed from Linux Driver Verification to Linux Kernel Safety RuleDB
- Assignee set to Ilya Shchepetkov
Models should be added and tested as well as for pointer error processing functions. But this feature request isn't critical, I guess.
Updated by Evgeny Novikov about 10 years ago
- Assignee changed from Ilya Shchepetkov to Vadim Mutilin
New students can try to implement and to experiment with this.