Feature #11836
closed
Model failures for calloc() and zalloc()
Added by Evgeny Novikov over 1 year ago.
Updated over 1 year ago.
Category:
Environment models
Description
Anton revealed that at the moment models enable failures only for malloc() while there is a huge amount of users of calloc() and zalloc() (through appropriate models). It does have sense to enable failures for the latter and carefully examine obtained verification results.
- Status changed from New to Resolved
I extended models of memory allocation functions to enable nondeterministic failures and added appropriate test cases that check for this behavior in branch enable-extra-alloc-failures. It should be very accurately tested since the change is crucial.
- Status changed from Resolved to Closed
Testing did demonstrate considerable changes.
690ba24 describes the ones for CI tests, namely for validation jobs. The most important changes are finding 2 target bugs that were found by Klever one day and that were fixed in the Linux kernel, but then Klever lost the capability to reveal them. This likely highlights that something happened (I suppose that CPAchecker SMG stopped to assume that memory allocation function can fail).
Verification of a subset of Linux kernel drivers showed that verification tasks became more hard due to they consider more possible execution paths. Hopefully, almost all good verification results remain the same. Only a few safes and false alarms became timeouts. Moreover, one exception has gone.
After all I merged the branch to master in d6a7b4ce1.
Also available in: Atom
PDF