// Skip function: __VERIFIER_error // Skip function: __VERIFIER_nondet_int // Function: __init_waitqueue_head // with type: void __init_waitqueue_head(wait_queue_head_t *, const char *, struct lock_class_key *) // with return type: void void __init_waitqueue_head(wait_queue_head_t *arg0, const char *arg1, struct lock_class_key *arg2) { // Void type return; } // Function: __mutex_init // with type: void __mutex_init(struct mutex *, const char *, struct lock_class_key *) // with return type: void void __mutex_init(struct mutex *arg0, const char *arg1, struct lock_class_key *arg2) { // Void type return; } // Function: __raw_spin_lock_init // with type: void __raw_spin_lock_init(raw_spinlock_t *, const char *, struct lock_class_key *) // with return type: void void __raw_spin_lock_init(raw_spinlock_t *arg0, const char *arg1, struct lock_class_key *arg2) { // Void type return; } // Function: __wake_up // with type: void __wake_up(wait_queue_head_t *, unsigned int, int, void *) // with return type: void void __wake_up(wait_queue_head_t *arg0, unsigned int arg1, int arg2, void *arg3) { // 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: _raw_spin_lock // with type: void _raw_spin_lock(raw_spinlock_t *) // with return type: void void _raw_spin_lock(raw_spinlock_t *arg0) { // Void type return; } // Function: _raw_spin_lock_irq // with type: void _raw_spin_lock_irq(raw_spinlock_t *) // with return type: void void _raw_spin_lock_irq(raw_spinlock_t *arg0) { // Void type return; } // Function: _raw_spin_unlock // with type: void _raw_spin_unlock(raw_spinlock_t *) // with return type: void void _raw_spin_unlock(raw_spinlock_t *arg0) { // Void type return; } // Function: _raw_spin_unlock_irq // with type: void _raw_spin_unlock_irq(raw_spinlock_t *) // with return type: void void _raw_spin_unlock_irq(raw_spinlock_t *arg0) { // Void type return; } // Function: complete // with type: void complete(struct completion *) // with return type: void void complete(struct completion *arg0) { // Void type return; } // Function: dev_get_drvdata // with type: void *dev_get_drvdata(const struct device *) // with return type: (void)* void *dev_get_drvdata(const struct device *arg0) { // Pointer type return ldv_malloc(0UL); } // Function: dev_set_drvdata // with type: int dev_set_drvdata(struct device *, void *) // with return type: int int __VERIFIER_nondet_int(void); int dev_set_drvdata(struct device *arg0, void *arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: do_gettimeofday // with type: void do_gettimeofday(struct timeval *) // with return type: void void do_gettimeofday(struct timeval *arg0) { // Void type return; } // Function: finish_wait // with type: void finish_wait(wait_queue_head_t *, wait_queue_t *) // with return type: void void finish_wait(wait_queue_head_t *arg0, wait_queue_t *arg1) { // Void type return; } // Function: input_alloc_absinfo // with type: void input_alloc_absinfo(struct input_dev *) // with return type: void void input_alloc_absinfo(struct input_dev *arg0) { // Void type return; } // Function: input_event // with type: void input_event(struct input_dev *, unsigned int, unsigned int, int) // with return type: void void input_event(struct input_dev *arg0, unsigned int arg1, unsigned int arg2, int arg3) { // Void type return; } // Function: input_event_from_user // with type: int input_event_from_user(const char *, struct input_event *) // with return type: int int __VERIFIER_nondet_int(void); int input_event_from_user(const char *arg0, struct input_event *arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: input_event_to_user // with type: int input_event_to_user(char *, const struct input_event *) // with return type: int int __VERIFIER_nondet_int(void); int input_event_to_user(char *arg0, const struct input_event *arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: input_ff_create // with type: int input_ff_create(struct input_dev *, unsigned int) // with return type: int int __VERIFIER_nondet_int(void); int input_ff_create(struct input_dev *arg0, unsigned int arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: input_ff_destroy // with type: void input_ff_destroy(struct input_dev *) // with return type: void void input_ff_destroy(struct input_dev *arg0) { // Void type return; } // Function: input_free_device // with type: void input_free_device(struct input_dev *) // with return type: void void input_free_device(struct input_dev *arg0) { // Void type return; } // Function: input_mt_init_slots // with type: int input_mt_init_slots(struct input_dev *, unsigned int, unsigned int) // with return type: int int __VERIFIER_nondet_int(void); int input_mt_init_slots(struct input_dev *arg0, unsigned int arg1, unsigned int arg2) { // Simple type return __VERIFIER_nondet_int(); } // Function: input_register_device // with type: int input_register_device(struct input_dev *) // with return type: int int __VERIFIER_nondet_int(void); int input_register_device(struct input_dev *arg0) { // Simple type return __VERIFIER_nondet_int(); } // Function: input_unregister_device // with type: void input_unregister_device(struct input_dev *) // with return type: void void input_unregister_device(struct input_dev *arg0) { // Void type return; } // Skip function: kfree // Function: kstrndup // with type: char *kstrndup(const char *, size_t , gfp_t ) // with return type: (char)* char *kstrndup(const char *arg0, size_t arg1, gfp_t arg2) { // Pointer type return ldv_malloc(sizeof(char)); } // Function: ldv_check_return_value // with type: void ldv_check_return_value(int) // with return type: void void ldv_check_return_value(int arg0) { // Void type return; } // Function: ldv_handler_precall // with type: void ldv_handler_precall() // with return type: void void ldv_handler_precall() { // Void type return; } // Skip function: malloc // Skip function: memcpy // Function: memdup_user // with type: void *memdup_user(const void *, size_t ) // with return type: (void)* void *memdup_user(const void *arg0, size_t arg1) { // Pointer type return ldv_malloc(0UL); } // Skip function: memset // Function: might_fault // with type: void might_fault() // with return type: void void might_fault() { // Void type return; } // Function: misc_deregister // with type: int misc_deregister(struct miscdevice *) // with return type: int int __VERIFIER_nondet_int(void); int misc_deregister(struct miscdevice *arg0) { // Simple type return __VERIFIER_nondet_int(); } // Function: misc_register // with type: int misc_register(struct miscdevice *) // with return type: int int __VERIFIER_nondet_int(void); int misc_register(struct miscdevice *arg0) { // Simple type return __VERIFIER_nondet_int(); } // Function: mutex_lock // with type: void mutex_lock(struct mutex *) // with return type: void void mutex_lock(struct mutex *arg0) { // Void type return; } // Function: mutex_lock_interruptible // with type: int mutex_lock_interruptible(struct mutex *) // with return type: int int __VERIFIER_nondet_int(void); int mutex_lock_interruptible(struct mutex *arg0) { // Simple type return __VERIFIER_nondet_int(); } // Function: mutex_trylock // with type: int mutex_trylock(struct mutex *) // with return type: int int __VERIFIER_nondet_int(void); int mutex_trylock(struct mutex *arg0) { // Simple type return __VERIFIER_nondet_int(); } // Function: mutex_unlock // with type: void mutex_unlock(struct mutex *) // with return type: void void mutex_unlock(struct mutex *arg0) { // Void type return; } // Function: nonseekable_open // with type: int nonseekable_open(struct inode *, struct file *) // with return type: int int __VERIFIER_nondet_int(void); int nonseekable_open(struct inode *arg0, struct file *arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: prepare_to_wait // with type: void prepare_to_wait(wait_queue_head_t *, wait_queue_t *, int) // with return type: void void prepare_to_wait(wait_queue_head_t *arg0, wait_queue_t *arg1, int arg2) { // Void type return; } // 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: schedule // with type: void schedule() // with return type: void void schedule() { // Void type return; } // Function: strndup_user // with type: char *strndup_user(const char *, long) // with return type: (char)* char *strndup_user(const char *arg0, long arg1) { // Pointer type return ldv_malloc(sizeof(char)); } // Function: wait_for_completion // with type: void wait_for_completion(struct completion *) // with return type: void void wait_for_completion(struct completion *arg0) { // Void type return; } // Function: warn_slowpath_fmt // with type: void warn_slowpath_fmt(const char *, const int, const char *, ...) // with return type: void void warn_slowpath_fmt(const char *arg0, const int arg1, const char *arg2, ...) { // Void type return; }