689 return __VERIFIER_nondet_int();
690}
691inline int scull_read(int tid, int filp, int buf, int count,
692 int f_pos)
693{
694 int dev = filp;
695 int dptr;
696 int quantum = dev_quantum, qset = dev_qset;
697 int itemsize = quantum * qset;
698 int item, s_pos, q_pos, rest;
699 int retval = 0;
700 if (down_interruptible())
701 return -512;
702 __X__ = 0;
703 if (f_pos >= dev_size)
704 goto out;
705 if (f_pos+count >= dev_size)
706 count = dev_size - f_pos;
707 item = f_pos / itemsize;
708 rest = f_pos;
709 s_pos = rest / quantum; q_pos = rest;
710 dptr = scull_follow(dev, item);
711 if (count > quantum - q_pos)
712 count = quantum - q_pos;
713 if (copy_to_user(buf, dev_data + s_pos + q_pos, count)) {
714 retval = -2;
715 goto out;
716 }
717 f_pos += count;
718 retval = count;
719 if (!(__X__ <= 0)) ERROR: goto ERROR;;
720 out:
721 up();
722 return retval;
723}
724inline int scull_write(int tid, int filp, int buf, int count,
725 int f_pos)
726{
727 int dev = filp;
728 int dptr;
729 int quantum = dev_quantum, qset = dev_qset;