654}
655inline int __put_user(int size, int ptr)
656{
657 return __VERIFIER_nondet_int();
658}
659int scull_quantum = 4000;
660int scull_qset = 1000;
661int dev_data;
662int dev_quantum;
663int dev_qset;
664int dev_size;
665int __X__;
666int scull_trim(int dev)
667{
668 int qset = dev_qset;
669 dev_size = 0;
670 dev_quantum = scull_quantum;
671 dev_qset = scull_qset;
672 dev_data = 0;
673 return 0;
674}
675inline int scull_open(int tid, int i, int filp)
676{
677 int dev;
678 dev = i;
679 filp = dev;
680 if (down_interruptible())
681 return -512;
682 __X__ = 2;
683 scull_trim(dev);
684 if (!(__X__ >= 2)) ERROR: goto ERROR;;
685 up();
686 return 0;
687}
688inline int scull_follow(int dev, int n) {
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;