// Skip function: __VERIFIER_error // Skip function: __VERIFIER_nondet_int // Skip function: __VERIFIER_nondet_uint // Skip function: __VERIFIER_nondet_ulong // Function: __class_create // with type: struct class *__class_create(struct module *, const char *, struct lock_class_key *) // with return type: (struct class)* struct class *__class_create(struct module *arg0, const char *arg1, struct lock_class_key *arg2) { // Pointer type return ldv_malloc(sizeof(struct class)); } // Function: __copy_from_user_overflow // with type: void __copy_from_user_overflow() // with return type: void void __copy_from_user_overflow() { // Void type return; } // Function: __copy_to_user_overflow // with type: void __copy_to_user_overflow() // with return type: void void __copy_to_user_overflow() { // Void type return; } // Function: __might_fault // with type: void __might_fault(const char *, int) // with return type: void void __might_fault(const char *arg0, int arg1) { // Void type return; } // Function: _copy_from_user // with type: unsigned long int _copy_from_user(void *, const void *, unsigned int) // with return type: unsigned long int unsigned long __VERIFIER_nondet_ulong(void); unsigned long int _copy_from_user(void *arg0, const void *arg1, unsigned int arg2) { // Simple type return __VERIFIER_nondet_ulong(); } // Function: _copy_to_user // with type: unsigned long int _copy_to_user(void *, const void *, unsigned int) // with return type: unsigned long int unsigned long __VERIFIER_nondet_ulong(void); unsigned long int _copy_to_user(void *arg0, const void *arg1, unsigned int arg2) { // Simple type return __VERIFIER_nondet_ulong(); } // Function: bdget // with type: struct block_device *bdget(dev_t ) // with return type: (struct block_device)* struct block_device *bdget(dev_t arg0) { // Pointer type return ldv_malloc(sizeof(struct block_device)); } // Function: bdput // with type: void bdput(struct block_device *) // with return type: void void bdput(struct block_device *arg0) { // Void type return; } // Function: blkdev_fsync // with type: int blkdev_fsync(struct file *, loff_t , loff_t , int) // with return type: int int __VERIFIER_nondet_int(void); int blkdev_fsync(struct file *arg0, loff_t arg1, loff_t arg2, int arg3) { // Simple type return __VERIFIER_nondet_int(); } // Function: blkdev_get // with type: int blkdev_get(struct block_device *, fmode_t , void *) // with return type: int int __VERIFIER_nondet_int(void); int blkdev_get(struct block_device *arg0, fmode_t arg1, void *arg2) { // Simple type return __VERIFIER_nondet_int(); } // Function: blkdev_ioctl // with type: int blkdev_ioctl(struct block_device *, fmode_t , unsigned int, unsigned long) // with return type: int int __VERIFIER_nondet_int(void); int blkdev_ioctl(struct block_device *arg0, fmode_t arg1, unsigned int arg2, unsigned long arg3) { // Simple type return __VERIFIER_nondet_int(); } // Function: blkdev_put // with type: void blkdev_put(struct block_device *, fmode_t ) // with return type: void void blkdev_put(struct block_device *arg0, fmode_t arg1) { // Void type return; } // Function: blkdev_read_iter // with type: ssize_t blkdev_read_iter(struct kiocb *, struct iov_iter *) // with return type: ssize_t long __VERIFIER_nondet_long(void); ssize_t blkdev_read_iter(struct kiocb *arg0, struct iov_iter *arg1) { // Typedef type // Real type: __kernel_ssize_t // Typedef type // Real type: __kernel_long_t // Typedef type // Real type: long // Simple type return __VERIFIER_nondet_long(); } // Function: blkdev_write_iter // with type: ssize_t blkdev_write_iter(struct kiocb *, struct iov_iter *) // with return type: ssize_t long __VERIFIER_nondet_long(void); ssize_t blkdev_write_iter(struct kiocb *arg0, struct iov_iter *arg1) { // Typedef type // Real type: __kernel_ssize_t // Typedef type // Real type: __kernel_long_t // Typedef type // Real type: long // Simple type return __VERIFIER_nondet_long(); } // Skip function: calloc // Function: capable // with type: bool capable(int) // with return type: bool bool __VERIFIER_nondet_bool(void); bool capable(int arg0) { // Typedef type // Real type: _Bool // Simple type return __VERIFIER_nondet_bool(); } // Function: cdev_add // with type: int cdev_add(struct cdev *, dev_t , unsigned int) // with return type: int int __VERIFIER_nondet_int(void); int cdev_add(struct cdev *arg0, dev_t arg1, unsigned int arg2) { // Simple type return __VERIFIER_nondet_int(); } // Function: cdev_del // with type: void cdev_del(struct cdev *) // with return type: void void cdev_del(struct cdev *arg0) { // Void type return; } // Function: cdev_init // with type: void cdev_init(struct cdev *, const struct file_operations *) // with return type: void void cdev_init(struct cdev *arg0, const struct file_operations *arg1) { // Void type return; } // Function: class_destroy // with type: void class_destroy(struct class *) // with return type: void void class_destroy(struct class *arg0) { // Void type return; } // Function: default_llseek // with type: loff_t default_llseek(struct file *, loff_t , int) // with return type: loff_t long __VERIFIER_nondet_long(void); loff_t default_llseek(struct file *arg0, loff_t arg1, int arg2) { // Typedef type // Real type: __kernel_loff_t // Typedef type // Real type: long long // Simple type return __VERIFIER_nondet_long(); } // Function: device_create // with type: struct device *device_create(struct class *, struct device *, dev_t , void *, const char *, ...) // with return type: (struct device)* struct device *device_create(struct class *arg0, struct device *arg1, dev_t arg2, void *arg3, const char *arg4, ...) { // Pointer type return ldv_malloc(sizeof(struct device)); } // Function: device_destroy // with type: void device_destroy(struct class *, dev_t ) // with return type: void void device_destroy(struct class *arg0, dev_t arg1) { // Void type return; } // Function: igrab // with type: struct inode *igrab(struct inode *) // with return type: (struct inode)* struct inode *igrab(struct inode *arg0) { // Pointer type return ldv_malloc(sizeof(struct inode)); } // Function: kasprintf // with type: char *kasprintf(gfp_t , const char *, ...) // with return type: (char)* char *kasprintf(gfp_t arg0, const char *arg1, ...) { // Pointer type return ldv_malloc(sizeof(char)); } // Function: ldv_initialize // with type: void ldv_initialize() // with return type: void void ldv_initialize() { // Void type return; } // Function: ldv_release_1 // with type: int ldv_release_1() // with return type: int int __VERIFIER_nondet_int(void); int ldv_release_1() { // Simple type return __VERIFIER_nondet_int(); } // Skip function: malloc // Skip function: memset // Function: mutex_lock_nested // with type: void mutex_lock_nested(struct mutex *, unsigned int) // with return type: void void mutex_lock_nested(struct mutex *arg0, unsigned int arg1) { // Void type return; } // Function: mutex_unlock // with type: void mutex_unlock(struct mutex *) // with return type: void void mutex_unlock(struct mutex *arg0) { // Void type return; } // Function: noop_llseek // with type: loff_t noop_llseek(struct file *, loff_t , int) // with return type: loff_t long __VERIFIER_nondet_long(void); loff_t noop_llseek(struct file *arg0, loff_t arg1, int arg2) { // Typedef type // Real type: __kernel_loff_t // Typedef type // Real type: long long // Simple type return __VERIFIER_nondet_long(); } // Function: printk // with type: int printk(const char *, ...) // with return type: int int __VERIFIER_nondet_int(void); int printk(const char *arg0, ...) { // Simple type return __VERIFIER_nondet_int(); } // Function: register_chrdev_region // with type: int register_chrdev_region(dev_t , unsigned int, const char *) // with return type: int int __VERIFIER_nondet_int(void); int register_chrdev_region(dev_t arg0, unsigned int arg1, const char *arg2) { // Simple type return __VERIFIER_nondet_int(); } // Function: set_blocksize // with type: int set_blocksize(struct block_device *, int) // with return type: int int __VERIFIER_nondet_int(void); int set_blocksize(struct block_device *arg0, int arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: unregister_chrdev_region // with type: void unregister_chrdev_region(dev_t , unsigned int) // with return type: void void unregister_chrdev_region(dev_t arg0, unsigned int arg1) { // Void type return; } // Function: vfree // with type: void vfree(const void *) // with return type: void void vfree(const void *arg0) { // Void type return; } // Function: vzalloc // with type: void *vzalloc(unsigned long) // with return type: (void)* void *vzalloc(unsigned long arg0) { // Pointer type return ldv_malloc(0UL); }