Linux Driver Verification » Linux Kernel Safety RuleDB

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.