Actions
Feature #2707
closedIS_ERR kernel core function should be modeled because of it is too complex for our verifiers
Start date:
04/04/2012
Due date:
% Done:
0%
Estimated time:
Published in build:
935d93f
Description
This function as well as some other error processing stuff is defined in linux/err.h header file. A typical way of such functions usage is so:
struct request *blk_make_request(struct request_queue *q, struct bio *bio, gfp_t gfp_mask) { struct request *rq = blk_get_request(q, bio_data_dir(bio), gfp_mask); if (unlikely(!rq)) return ERR_PTR(-ENOMEM); ... static int virtblk_get_id(struct gendisk *disk, char *id_str) { ... req = blk_make_request(vblk->disk->queue, bio, GFP_KERNEL); if (IS_ERR(req)) { bio_put(bio); return PTR_ERR(req); } ...
That is when some function, that returns a pointer, needs to report some error, it returns ERR_PTR(-ERRNO), which converts a small negative long integer number to void * pointer, which is represented as a huge unsigned long integer number (something between (UNSIGNED_LONG_MAX - MAX_ERRNO) and UNSIGNED_LONG_MAX). Then IS_ERR function checks whether this return value is in these limits or not, If not, then all is okay. Otherwise a function can return PTR_ERR of this value (that converts it back to small negative long integer number).
I guess that we should model ldv_undef_ptr, PTR_ERR and IS_ERR in the same manner. If ldv_undef_ptr "returns" a big value, say, greater then LDV_PTR_MAX, a called function is failed, IS_ERR model function should return true and PTR_ERR should return some negative nondetermined value.
Updated by Evgeny Novikov over 12 years ago
- Status changed from New to Resolved
- Published in build set to 935d93f
Commit 935d93f of the master branch contains suggested implementation. Partially it's placed to the new interface header ldv.h, partially - to aspect of 101_1a model (because of aspect features are required, but we still don't have aspect includes).
Updated by Evgeny Novikov over 12 years ago
- Status changed from Resolved to Closed
IS_ERR model was merged to master as part of 101_1a rule model. #865 will allow to make this model independent on any particular rule model.
Actions