Feature #11836
closedModel failures for calloc() and zalloc()
0%
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.
Updated by Evgeny Novikov over 1 year ago
- 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.
Updated by Evgeny Novikov over 1 year ago
- 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.