// Skip function: __VERIFIER_error // Skip function: __VERIFIER_nondet_int // Skip function: __VERIFIER_nondet_size_t // Skip function: __VERIFIER_nondet_uint // Skip function: __VERIFIER_nondet_ulong // Function: __const_udelay // with type: void __const_udelay(unsigned long) // with return type: void void __const_udelay(unsigned long arg0) { // Void type return; } // 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: __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: __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: __list_del_entry // with type: void __list_del_entry(struct list_head *) // with return type: void void __list_del_entry(struct list_head *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: __video_register_device // with type: int __video_register_device(struct video_device *, int, int, int, struct module *) // with return type: int int __VERIFIER_nondet_int(void); int __video_register_device(struct video_device *arg0, int arg1, int arg2, int arg3, struct module *arg4) { // Simple type return __VERIFIER_nondet_int(); } // 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_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_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_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; } // Skip function: calloc // Function: del_timer // with type: int del_timer(struct timer_list *) // with return type: int int __VERIFIER_nondet_int(void); int del_timer(struct timer_list *arg0) { // Simple type return __VERIFIER_nondet_int(); } // Function: dev_err // with type: int dev_err(const struct device *, const char *, ...) // with return type: int int __VERIFIER_nondet_int(void); int dev_err(const struct device *arg0, const char *arg1, ...) { // 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: device_create_file // with type: int device_create_file(struct device *, const struct device_attribute *) // with return type: int int __VERIFIER_nondet_int(void); int device_create_file(struct device *arg0, const struct device_attribute *arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: device_remove_file // with type: void device_remove_file(struct device *, const struct device_attribute *) // with return type: void void device_remove_file(struct device *arg0, const struct device_attribute *arg1) { // 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: i2c_add_adapter // with type: int i2c_add_adapter(struct i2c_adapter *) // with return type: int int __VERIFIER_nondet_int(void); int i2c_add_adapter(struct i2c_adapter *arg0) { // Simple type return __VERIFIER_nondet_int(); } // Function: i2c_del_adapter // with type: void i2c_del_adapter(struct i2c_adapter *) // with return type: void void i2c_del_adapter(struct i2c_adapter *arg0) { // Void type return; } // Skip function: kfree // Function: ldv_initialize // with type: void ldv_initialize() // with return type: void void ldv_initialize() { // Void type return; } // Function: ldv_probe_4 // with type: int ldv_probe_4() // with return type: int int __VERIFIER_nondet_int(void); int ldv_probe_4() { // Simple type return __VERIFIER_nondet_int(); } // Function: ldv_probe_7 // with type: int ldv_probe_7() // with return type: int int __VERIFIER_nondet_int(void); int ldv_probe_7() { // 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: memset // Function: might_fault // with type: void might_fault() // with return type: void void might_fault() { // Void type return; } // 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: 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: mutex_lock_interruptible_nested // with type: int mutex_lock_interruptible_nested(struct mutex *, unsigned int) // with return type: int int __VERIFIER_nondet_int(void); int mutex_lock_interruptible_nested(struct mutex *arg0, unsigned int arg1) { // Simple type return __VERIFIER_nondet_int(); } // 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: 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: queue_work_on // with type: bool queue_work_on(int, struct workqueue_struct *, struct work_struct *) // with return type: bool bool __VERIFIER_nondet_bool(void); bool queue_work_on(int arg0, struct workqueue_struct *arg1, struct work_struct *arg2) { // Typedef type // Real type: _Bool // Simple type return __VERIFIER_nondet_bool(); } // Function: schedule // with type: void schedule() // with return type: void void schedule() { // Void type return; } // Function: schedule_timeout // with type: long int schedule_timeout(long) // with return type: long int long __VERIFIER_nondet_long(void); long int schedule_timeout(long arg0) { // Simple type return __VERIFIER_nondet_long(); } // Skip function: snprintf // Skip function: sprintf // Skip function: strcpy // Function: strlcpy // with type: size_t strlcpy(char *, const char *, size_t ) // with return type: size_t unsigned long __VERIFIER_nondet_ulong(void); size_t strlcpy(char *arg0, const char *arg1, size_t arg2) { // Typedef type // Real type: __kernel_size_t // Typedef type // Real type: __kernel_ulong_t // Typedef type // Real type: unsigned long // Simple type return __VERIFIER_nondet_ulong(); } // Function: usb_alloc_coherent // with type: void *usb_alloc_coherent(struct usb_device *, size_t , gfp_t , dma_addr_t *) // with return type: (void)* void *usb_alloc_coherent(struct usb_device *arg0, size_t arg1, gfp_t arg2, dma_addr_t *arg3) { // Pointer type return ldv_malloc(0UL); } // Function: usb_control_msg // with type: int usb_control_msg(struct usb_device *, unsigned int, __u8 , __u8 , __u16 , __u16 , void *, __u16 , int) // with return type: int int __VERIFIER_nondet_int(void); int usb_control_msg(struct usb_device *arg0, unsigned int arg1, __u8 arg2, __u8 arg3, __u16 arg4, __u16 arg5, void *arg6, __u16 arg7, int arg8) { // Simple type return __VERIFIER_nondet_int(); } // Function: usb_deregister // with type: void usb_deregister(struct usb_driver *) // with return type: void void usb_deregister(struct usb_driver *arg0) { // Void type return; } // Function: usb_free_coherent // with type: void usb_free_coherent(struct usb_device *, size_t , void *, dma_addr_t ) // with return type: void void usb_free_coherent(struct usb_device *arg0, size_t arg1, void *arg2, dma_addr_t arg3) { // Void type return; } // Function: usb_kill_urb // with type: void usb_kill_urb(struct urb *) // with return type: void void usb_kill_urb(struct urb *arg0) { // Void type return; } // Function: usb_register_driver // with type: int usb_register_driver(struct usb_driver *, struct module *, const char *) // with return type: int int __VERIFIER_nondet_int(void); int usb_register_driver(struct usb_driver *arg0, struct module *arg1, const char *arg2) { // Simple type return __VERIFIER_nondet_int(); } // Function: usb_set_interface // with type: int usb_set_interface(struct usb_device *, int, int) // with return type: int int __VERIFIER_nondet_int(void); int usb_set_interface(struct usb_device *arg0, int arg1, int arg2) { // Simple type return __VERIFIER_nondet_int(); } // Function: v4l2_device_disconnect // with type: void v4l2_device_disconnect(struct v4l2_device *) // with return type: void void v4l2_device_disconnect(struct v4l2_device *arg0) { // Void type return; } // Function: v4l2_device_register // with type: int v4l2_device_register(struct device *, struct v4l2_device *) // with return type: int int __VERIFIER_nondet_int(void); int v4l2_device_register(struct device *arg0, struct v4l2_device *arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: v4l2_device_unregister // with type: void v4l2_device_unregister(struct v4l2_device *) // with return type: void void v4l2_device_unregister(struct v4l2_device *arg0) { // Void type return; } // Function: v4l2_get_timestamp // with type: void v4l2_get_timestamp(struct timeval *) // with return type: void void v4l2_get_timestamp(struct timeval *arg0) { // Void type return; } // Function: v4l2_i2c_new_subdev // with type: struct v4l2_subdev *v4l2_i2c_new_subdev(struct v4l2_device *, struct i2c_adapter *, const char *, u8 , const unsigned short *) // with return type: (struct v4l2_subdev)* struct v4l2_subdev *v4l2_i2c_new_subdev(struct v4l2_device *arg0, struct i2c_adapter *arg1, const char *arg2, u8 arg3, const unsigned short *arg4) { // Pointer type return ldv_malloc(sizeof(struct v4l2_subdev)); } // Function: v4l2_i2c_subdev_addr // with type: unsigned short int v4l2_i2c_subdev_addr(struct v4l2_subdev *) // with return type: unsigned short int unsigned short __VERIFIER_nondet_ushort(void); unsigned short int v4l2_i2c_subdev_addr(struct v4l2_subdev *arg0) { // Simple type return __VERIFIER_nondet_ushort(); } // Function: v4l2_i2c_tuner_addrs // with type: const unsigned short *v4l2_i2c_tuner_addrs(enum v4l2_i2c_tuner_type ) // with return type: (const unsigned short)* const unsigned short *v4l2_i2c_tuner_addrs(enum v4l2_i2c_tuner_type arg0) { // Pointer type return ldv_malloc(sizeof(unsigned short)); } // Function: vfree // with type: void vfree(const void *) // with return type: void void vfree(const void *arg0) { // Void type return; } // Function: video_devdata // with type: struct video_device *video_devdata(struct file *) // with return type: (struct video_device)* struct video_device *video_devdata(struct file *arg0) { // Pointer type return ldv_malloc(sizeof(struct video_device)); } // Function: video_device_alloc // with type: struct video_device *video_device_alloc() // with return type: (struct video_device)* struct video_device *video_device_alloc() { // Pointer type return ldv_malloc(sizeof(struct video_device)); } // Function: video_device_release // with type: void video_device_release(struct video_device *) // with return type: void void video_device_release(struct video_device *arg0) { // Void type return; } // Function: video_ioctl2 // with type: long int video_ioctl2(struct file *, unsigned int, unsigned long) // with return type: long int long __VERIFIER_nondet_long(void); long int video_ioctl2(struct file *arg0, unsigned int arg1, unsigned long arg2) { // Simple type return __VERIFIER_nondet_long(); } // Function: video_unregister_device // with type: void video_unregister_device(struct video_device *) // with return type: void void video_unregister_device(struct video_device *arg0) { // Void type return; } // Function: vm_insert_page // with type: int vm_insert_page(struct vm_area_struct *, unsigned long, struct page *) // with return type: int int __VERIFIER_nondet_int(void); int vm_insert_page(struct vm_area_struct *arg0, unsigned long arg1, struct page *arg2) { // Simple type return __VERIFIER_nondet_int(); } // Function: vmalloc_32 // with type: void *vmalloc_32(unsigned long) // with return type: (void)* void *vmalloc_32(unsigned long arg0) { // Pointer type return ldv_malloc(0UL); } // Function: vmalloc_to_page // with type: struct page *vmalloc_to_page(const void *) // with return type: (struct page)* struct page *vmalloc_to_page(const void *arg0) { // Pointer type return ldv_malloc(sizeof(struct page)); } // Function: autoremove_wake_function // with type: int autoremove_wake_function(wait_queue_t *, unsigned int, int, void *) // with return type: int int __VERIFIER_nondet_int(void); int autoremove_wake_function(wait_queue_t *arg0, unsigned int arg1, int arg2, void * arg3) { // Simple type return __VERIFIER_nondet_int(); }