Feature #7540 ยป 0001-rule-spec-block-request-fix-error-__GFP_WAIT-undecla.patch
| bridge/jobs/presets/linux-3.14/linux/block/request.c | ||
|---|---|---|
|
#include <verifier/common.h>
|
||
|
#include <verifier/nondet.h>
|
||
|
/*
|
||
|
* If gfp_mask argument of blk_get_request() has __GFP_WAIT(linux 4.4 or below)
|
||
|
* or __GFP_DIRECT_RECLAIM(linux 4.4+) set, blk_get_request() cannot fail.
|
||
|
* Potentially it can fail if queue is dying, but we ingnore that for now.
|
||
|
*/
|
||
|
#if defined(__GFP_WAIT)
|
||
|
#ifdef LDV_BITWISE
|
||
|
#define ldv_blk_get_request_cannot_fail(gfp_mask) (gfp_mask | __GFP_WAIT)
|
||
|
#else
|
||
|
/* Let's use approximation if verifier does not support bitwise operations */
|
||
|
#define ldv_blk_get_request_cannot_fail(gfp_mask) \
|
||
|
(gfp_mask == __GFP_WAIT || gfp_mask == GFP_KERNEL || gfp_mask == GFP_NOIO)
|
||
|
#endif
|
||
|
#else
|
||
|
#ifdef LDV_BITWISE
|
||
|
#define ldv_blk_get_request_cannot_fail(gfp_mask) (gfp_mask | __GFP_DIRECT_RECLAIM)
|
||
|
#else
|
||
|
/* Let's use approximation if verifier does not support bitwise operations */
|
||
|
/* __GFP_RECLAIM is used where __GFP_WAIT was used before at call side */
|
||
|
#define ldv_blk_get_request_cannot_fail(gfp_mask) \
|
||
|
(gfp_mask == __GFP_RECLAIM || gfp_mask == GFP_KERNEL || gfp_mask == GFP_NOIO)
|
||
|
#endif
|
||
|
#endif
|
||
|
/* There are 2 possible states of blk request. */
|
||
|
enum
|
||
|
{
|
||
| ... | ... | |
|
/* NOTE Generate valid pointer or NULL. */
|
||
|
res = (struct request *)ldv_undef_ptr();
|
||
|
/* NOTE If gfp_mask argument has __GFP_WAIT set, blk_get_request() cannot fail. */
|
||
|
if (mask == __GFP_WAIT || mask == GFP_KERNEL || mask == GFP_NOIO)
|
||
|
/* NOTE If gfp_mask argument has __GFP_WAIT(before 4.4) or __GFP_DIRECT_RECLAIM(4.4+) set, blk_get_request() cannot fail. */
|
||
|
if (ldv_blk_get_request_cannot_fail(mask))
|
||
|
ldv_assume(res != NULL);
|
||
|
if (res != NULL) {
|
||