Feature #7942
Updated by Evgeny Novikov about 7 years ago
See http://ldvstore:8998/reports/unsafe/75886/ Functions atomic_dec_and_test and atomic_set are not modeled while some of atomic* functions use inline assembler unsupported by verifiers, modeled, therefore free is not called in unix_release_addr. Note, that corresponding models already invoked but just by rule specification linux:usb:dev. exist in linux:usb:dev rule.