// Skip function: __VERIFIER_error // Skip function: __VERIFIER_nondet_int // Skip function: __VERIFIER_nondet_long // Function: __class_register // with type: int __class_register(struct class *, struct lock_class_key *) // with return type: int int __VERIFIER_nondet_int(void); int __class_register(struct class *arg0, struct lock_class_key *arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: __dynamic_pr_debug // with type: int __dynamic_pr_debug(struct _ddebug *, const char *, ...) // with return type: int int __VERIFIER_nondet_int(void); int __dynamic_pr_debug(struct _ddebug *arg0, const char *arg1, ...) { // Simple type return __VERIFIER_nondet_int(); } // Function: __init_work // with type: void __init_work(struct work_struct *, int) // with return type: void void __init_work(struct work_struct *arg0, int arg1) { // Void type return; } // Function: __kfifo_alloc // with type: int __kfifo_alloc(struct __kfifo *, unsigned int, size_t , gfp_t ) // with return type: int int __VERIFIER_nondet_int(void); int __kfifo_alloc(struct __kfifo *arg0, unsigned int arg1, size_t arg2, gfp_t arg3) { // Simple type return __VERIFIER_nondet_int(); } // Function: __kfifo_free // with type: void __kfifo_free(struct __kfifo *) // with return type: void void __kfifo_free(struct __kfifo *arg0) { // Void type return; } // Function: __kfifo_in // with type: unsigned int __kfifo_in(struct __kfifo *, const void *, unsigned int) // with return type: unsigned int unsigned int __VERIFIER_nondet_uint(void); unsigned int __kfifo_in(struct __kfifo *arg0, const void *arg1, unsigned int arg2) { // Simple type return __VERIFIER_nondet_uint(); } // Function: __kfifo_in_r // with type: unsigned int __kfifo_in_r(struct __kfifo *, const void *, unsigned int, size_t ) // with return type: unsigned int unsigned int __VERIFIER_nondet_uint(void); unsigned int __kfifo_in_r(struct __kfifo *arg0, const void *arg1, unsigned int arg2, size_t arg3) { // Simple type return __VERIFIER_nondet_uint(); } // Function: __kfifo_out // with type: unsigned int __kfifo_out(struct __kfifo *, void *, unsigned int) // with return type: unsigned int unsigned int __VERIFIER_nondet_uint(void); unsigned int __kfifo_out(struct __kfifo *arg0, void *arg1, unsigned int arg2) { // Simple type return __VERIFIER_nondet_uint(); } // Function: __kfifo_out_r // with type: unsigned int __kfifo_out_r(struct __kfifo *, void *, unsigned int, size_t ) // with return type: unsigned int unsigned int __VERIFIER_nondet_uint(void); unsigned int __kfifo_out_r(struct __kfifo *arg0, void *arg1, unsigned int arg2, size_t arg3) { // Simple type return __VERIFIER_nondet_uint(); } // Function: __list_add // with type: void __list_add(struct list_head *, struct list_head *, struct list_head *) // with return type: void void __list_add(struct list_head *arg0, struct list_head *arg1, struct list_head *arg2) { // Void type return; } // Function: __module_get // with type: void __module_get(struct module *) // with return type: void void __module_get(struct module *arg0) { // 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: __request_module // with type: int __request_module(bool , const char *, ...) // with return type: int int __VERIFIER_nondet_int(void); int __request_module(bool arg0, const char *arg1, ...) { // Simple type return __VERIFIER_nondet_int(); } // 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_lock_irqsave // with type: unsigned long int _raw_spin_lock_irqsave(raw_spinlock_t *) // with return type: unsigned long int unsigned long __VERIFIER_nondet_ulong(void); unsigned long int _raw_spin_lock_irqsave(raw_spinlock_t *arg0) { // Simple type return __VERIFIER_nondet_ulong(); } // 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: _raw_spin_unlock_irqrestore // with type: void _raw_spin_unlock_irqrestore(raw_spinlock_t *, unsigned long) // with return type: void void _raw_spin_unlock_irqrestore(raw_spinlock_t *arg0, unsigned long arg1) { // Void type return; } // Function: add_uevent_var // with type: int add_uevent_var(struct kobj_uevent_env *, const char *, ...) // with return type: int int __VERIFIER_nondet_int(void); int add_uevent_var(struct kobj_uevent_env *arg0, const char *arg1, ...) { // Simple type return __VERIFIER_nondet_int(); } // Function: class_unregister // with type: void class_unregister(struct class *) // with return type: void void class_unregister(struct class *arg0) { // Void type return; } // Function: del_timer_sync // with type: int del_timer_sync(struct timer_list *) // with return type: int int __VERIFIER_nondet_int(void); int del_timer_sync(struct timer_list *arg0) { // Simple type return __VERIFIER_nondet_int(); } // 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: dev_set_name // with type: int dev_set_name(struct device *, const char *, ...) // with return type: int int __VERIFIER_nondet_int(void); int dev_set_name(struct device *arg0, const char *arg1, ...) { // Simple type return __VERIFIER_nondet_int(); } // Function: device_add // with type: int device_add(struct device *) // with return type: int int __VERIFIER_nondet_int(void); int device_add(struct device *arg0) { // Simple type return __VERIFIER_nondet_int(); } // Function: device_del // with type: void device_del(struct device *) // with return type: void void device_del(struct device *arg0) { // Void type return; } // Function: device_initialize // with type: void device_initialize(struct device *) // with return type: void void device_initialize(struct device *arg0) { // Void type return; } // Function: init_timer_key // with type: void init_timer_key(struct timer_list *, unsigned int, const char *, struct lock_class_key *) // with return type: void void init_timer_key(struct timer_list *arg0, unsigned int arg1, const char *arg2, struct lock_class_key *arg3) { // 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_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_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_scancode_to_scalar // with type: int input_scancode_to_scalar(const struct input_keymap_entry *, unsigned int *) // with return type: int int __VERIFIER_nondet_int(void); int input_scancode_to_scalar(const struct input_keymap_entry *arg0, unsigned int *arg1) { // 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; } // 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)); } // Skip function: kfree // Function: kobject_get_path // with type: char *kobject_get_path(struct kobject *, gfp_t ) // with return type: (char)* char *kobject_get_path(struct kobject *arg0, gfp_t arg1) { // Pointer type return ldv_malloc(sizeof(char)); } // Function: kthread_create_on_node // with type: struct task_struct *kthread_create_on_node(int (*)(void *), void *, int, const char *, ...) // with return type: (struct task_struct)* struct task_struct *kthread_create_on_node(int (*arg0)(void *), void *arg1, int arg2, const char *arg3, ...) { // Pointer type return ldv_malloc(sizeof(struct task_struct)); } // Function: kthread_should_stop // with type: bool kthread_should_stop() // with return type: bool bool __VERIFIER_nondet_bool(void); bool kthread_should_stop() { // Typedef type // Real type: _Bool // Simple type return __VERIFIER_nondet_bool(); } // Function: kthread_stop // with type: int kthread_stop(struct task_struct *) // with return type: int int __VERIFIER_nondet_int(void); int kthread_stop(struct task_struct *arg0) { // Simple type return __VERIFIER_nondet_int(); } // Function: ktime_get // with type: ktime_t ktime_get() // with return type: ktime_t ktime_t ktime_get() { // Typedef type // Real type: union ktime // Composite type return *(union ktime *)ldv_xmalloc(sizeof(union ktime)); } // Function: ldv_rc_dev_type_probe_1 // with type: int ldv_rc_dev_type_probe_1() // with return type: int int __VERIFIER_nondet_int(void); int ldv_rc_dev_type_probe_1() { // Simple type return __VERIFIER_nondet_int(); } // Function: list_del // with type: void list_del(struct list_head *) // with return type: void void list_del(struct list_head *arg0) { // Void type return; } // Function: lockdep_init_map // with type: void lockdep_init_map(struct lockdep_map *, const char *, struct lock_class_key *, int) // with return type: void void lockdep_init_map(struct lockdep_map *arg0, const char *arg1, struct lock_class_key *arg2, int arg3) { // Void type return; } // Skip function: malloc // Skip function: memcpy // Skip function: memmove // Skip function: memset // Function: mod_timer // with type: int mod_timer(struct timer_list *, unsigned long) // with return type: int int __VERIFIER_nondet_int(void); int mod_timer(struct timer_list *arg0, unsigned long arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: module_put // with type: void module_put(struct module *) // with return type: void void module_put(struct module *arg0) { // Void type return; } // Function: msecs_to_jiffies // with type: unsigned long int msecs_to_jiffies(const unsigned int) // with return type: unsigned long int unsigned long __VERIFIER_nondet_ulong(void); unsigned long int msecs_to_jiffies(const unsigned int arg0) { // Simple type return __VERIFIER_nondet_ulong(); } // Function: msleep // with type: void msleep(unsigned int) // with return type: void void msleep(unsigned int arg0) { // Void type return; } // 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_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: 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: put_device // with type: void put_device(struct device *) // with return type: void void put_device(struct device *arg0) { // Void type return; } // Function: schedule // with type: void schedule() // with return type: void void schedule() { // Void type return; } // Function: schedule_work // with type: bool schedule_work(struct work_struct *) // with return type: bool bool __VERIFIER_nondet_bool(void); bool schedule_work(struct work_struct *arg0) { // Typedef type // Real type: _Bool // Simple type return __VERIFIER_nondet_bool(); } // Skip function: sprintf // Function: strcasecmp // with type: int strcasecmp(const char *, const char *) // with return type: int int __VERIFIER_nondet_int(void); int strcasecmp(const char *arg0, const char *arg1) { // Simple type return __VERIFIER_nondet_int(); } // Skip function: strcmp // Function: strsep // with type: char *strsep(char **, const char *) // with return type: (char)* char *strsep(char **arg0, const char *arg1) { // Pointer type return ldv_malloc(sizeof(char)); } // Function: wake_up_process // with type: int wake_up_process(struct task_struct *) // with return type: int int __VERIFIER_nondet_int(void); int wake_up_process(struct task_struct *arg0) { // Simple type return __VERIFIER_nondet_int(); }