// Skip function: __VERIFIER_error // Skip function: __VERIFIER_nondet_int // 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: __dynamic_dev_dbg // with type: void __dynamic_dev_dbg(struct _ddebug *, const struct device *, const char *, ...) // with return type: void void __dynamic_dev_dbg(struct _ddebug *arg0, const struct device *arg1, const char *arg2, ...) { // Void type return; } // Function: __dynamic_pr_debug // with type: void __dynamic_pr_debug(struct _ddebug *, const char *, ...) // with return type: void void __dynamic_pr_debug(struct _ddebug *arg0, const char *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: __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_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: _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: _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: debugfs_create_dir // with type: struct dentry *debugfs_create_dir(const char *, struct dentry *) // with return type: (struct dentry)* struct dentry *debugfs_create_dir(const char *arg0, struct dentry *arg1) { // Pointer type return ldv_malloc(sizeof(struct dentry)); } // Function: debugfs_create_file // with type: struct dentry *debugfs_create_file(const char *, umode_t , struct dentry *, void *, const struct file_operations *) // with return type: (struct dentry)* struct dentry *debugfs_create_file(const char *arg0, umode_t arg1, struct dentry *arg2, void *arg3, const struct file_operations *arg4) { // Pointer type return ldv_malloc(sizeof(struct dentry)); } // Function: debugfs_remove // with type: void debugfs_remove(struct dentry *) // with return type: void void debugfs_remove(struct dentry *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: 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_err // with type: void dev_err(const struct device *, const char *, ...) // with return type: void void dev_err(const struct device *arg0, const char *arg1, ...) { // Void type return; } // Function: dev_warn // with type: void dev_warn(const struct device *, const char *, ...) // with return type: void void dev_warn(const struct device *arg0, const char *arg1, ...) { // Void type return; } // Function: device_set_wakeup_capable // with type: void device_set_wakeup_capable(struct device *, bool ) // with return type: void void device_set_wakeup_capable(struct device *arg0, bool arg1) { // Void type return; } // Function: dma_alloc_attrs // with type: void *dma_alloc_attrs(struct device *, size_t , dma_addr_t *, gfp_t , struct dma_attrs *) // with return type: (void)* void *dma_alloc_attrs(struct device *arg0, size_t arg1, dma_addr_t *arg2, gfp_t arg3, struct dma_attrs *arg4) { // Pointer type return ldv_malloc(0UL); } // Function: dma_free_attrs // with type: void dma_free_attrs(struct device *, size_t , void *, dma_addr_t , struct dma_attrs *) // with return type: void void dma_free_attrs(struct device *arg0, size_t arg1, void *arg2, dma_addr_t arg3, struct dma_attrs *arg4) { // Void type return; } // Function: dma_pool_create // with type: struct dma_pool *dma_pool_create(const char *, struct device *, size_t , size_t , size_t ) // with return type: (struct dma_pool)* struct dma_pool *dma_pool_create(const char *arg0, struct device *arg1, size_t arg2, size_t arg3, size_t arg4) { // Pointer type return ldv_malloc(0UL); } // Function: dma_pool_destroy // with type: void dma_pool_destroy(struct dma_pool *) // with return type: void void dma_pool_destroy(struct dma_pool *arg0) { // Void type return; } // Function: dma_pool_free // with type: void dma_pool_free(struct dma_pool *, void *, dma_addr_t ) // with return type: void void dma_pool_free(struct dma_pool *arg0, void *arg1, dma_addr_t arg2) { // Void type return; } // Function: flush_work // with type: bool flush_work(struct work_struct *) // with return type: bool bool __VERIFIER_nondet_bool(void); bool flush_work(struct work_struct *arg0) { // Typedef type // Real type: _Bool // Simple type return __VERIFIER_nondet_bool(); } // Function: free_irq // with type: void free_irq(unsigned int, void *) // with return type: void void free_irq(unsigned int arg0, void *arg1) { // Void type return; } // Function: free_pages // with type: void free_pages(unsigned long, unsigned int) // with return type: void void free_pages(unsigned long arg0, unsigned int arg1) { // Void type return; } // Function: get_zeroed_page // with type: unsigned long int get_zeroed_page(gfp_t ) // with return type: unsigned long int unsigned long __VERIFIER_nondet_ulong(void); unsigned long int get_zeroed_page(gfp_t arg0) { // Simple type return __VERIFIER_nondet_ulong(); } // Skip function: kfree // Function: ldv_check_final_state // with type: void ldv_check_final_state() // with return type: void void ldv_check_final_state() { // Void type return; } // Function: ldv_initialize // with type: void ldv_initialize() // with return type: void void ldv_initialize() { // Void type return; } // Function: ldv_some_page // with type: struct page *ldv_some_page() // with return type: (struct page)* struct page *ldv_some_page() { // Pointer type return ldv_malloc(sizeof(struct page)); } // 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; } // Skip function: malloc // 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: msleep // with type: void msleep(unsigned int) // with return type: void void msleep(unsigned int arg0) { // Void type return; } // 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: 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: sb800_prefetch // with type: void sb800_prefetch(struct device *, int) // with return type: void void sb800_prefetch(struct device *arg0, int arg1) { // Void type return; } // Function: schedule_timeout_uninterruptible // with type: long int schedule_timeout_uninterruptible(long) // with return type: long int long __VERIFIER_nondet_long(void); long int schedule_timeout_uninterruptible(long arg0) { // Simple type return __VERIFIER_nondet_long(); } // Function: scnprintf // with type: int scnprintf(char *, size_t , const char *, ...) // with return type: int int __VERIFIER_nondet_int(void); int scnprintf(char *arg0, size_t arg1, const char *arg2, ...) { // Simple type return __VERIFIER_nondet_int(); } // Function: set_timer_slack // with type: void set_timer_slack(struct timer_list *, int) // with return type: void void set_timer_slack(struct timer_list *arg0, int arg1) { // Void type return; } // Function: sg_next // with type: struct scatterlist *sg_next(struct scatterlist *) // with return type: (struct scatterlist)* struct scatterlist *sg_next(struct scatterlist *arg0) { // Pointer type return ldv_malloc(sizeof(struct scatterlist)); } // Function: simple_read_from_buffer // with type: ssize_t simple_read_from_buffer(void *, size_t , loff_t *, const void *, size_t ) // with return type: ssize_t long __VERIFIER_nondet_long(void); ssize_t simple_read_from_buffer(void *arg0, size_t arg1, loff_t *arg2, const void *arg3, size_t arg4) { // 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: synchronize_irq // with type: void synchronize_irq(unsigned int) // with return type: void void synchronize_irq(unsigned int arg0) { // Void type return; } // Function: usb_amd_dev_put // with type: void usb_amd_dev_put() // with return type: void void usb_amd_dev_put() { // Void type return; } // Function: usb_amd_quirk_pll_disable // with type: void usb_amd_quirk_pll_disable() // with return type: void void usb_amd_quirk_pll_disable() { // Void type return; } // Function: usb_amd_quirk_pll_enable // with type: void usb_amd_quirk_pll_enable() // with return type: void void usb_amd_quirk_pll_enable() { // Void type return; } // Function: usb_calc_bus_time // with type: long int usb_calc_bus_time(int, int, int, int) // with return type: long int long __VERIFIER_nondet_long(void); long int usb_calc_bus_time(int arg0, int arg1, int arg2, int arg3) { // Simple type return __VERIFIER_nondet_long(); } // Function: usb_disabled // with type: int usb_disabled() // with return type: int int __VERIFIER_nondet_int(void); int usb_disabled() { // Simple type return __VERIFIER_nondet_int(); } // Function: usb_hc_died // with type: void usb_hc_died(struct usb_hcd *) // with return type: void void usb_hc_died(struct usb_hcd *arg0) { // Void type return; } // Function: usb_hcd_check_unlink_urb // with type: int usb_hcd_check_unlink_urb(struct usb_hcd *, struct urb *, int) // with return type: int int __VERIFIER_nondet_int(void); int usb_hcd_check_unlink_urb(struct usb_hcd *arg0, struct urb *arg1, int arg2) { // Simple type return __VERIFIER_nondet_int(); } // Function: usb_hcd_giveback_urb // with type: void usb_hcd_giveback_urb(struct usb_hcd *, struct urb *, int) // with return type: void void usb_hcd_giveback_urb(struct usb_hcd *arg0, struct urb *arg1, int arg2) { // Void type return; } // Function: usb_hcd_link_urb_to_ep // with type: int usb_hcd_link_urb_to_ep(struct usb_hcd *, struct urb *) // with return type: int int __VERIFIER_nondet_int(void); int usb_hcd_link_urb_to_ep(struct usb_hcd *arg0, struct urb *arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: usb_hcd_poll_rh_status // with type: void usb_hcd_poll_rh_status(struct usb_hcd *) // with return type: void void usb_hcd_poll_rh_status(struct usb_hcd *arg0) { // Void type return; } // Function: usb_hcd_resume_root_hub // with type: void usb_hcd_resume_root_hub(struct usb_hcd *) // with return type: void void usb_hcd_resume_root_hub(struct usb_hcd *arg0) { // Void type return; } // Function: usb_hcd_unlink_urb_from_ep // with type: void usb_hcd_unlink_urb_from_ep(struct usb_hcd *, struct urb *) // with return type: void void usb_hcd_unlink_urb_from_ep(struct usb_hcd *arg0, struct urb *arg1) { // Void type return; } // Function: usb_root_hub_lost_power // with type: void usb_root_hub_lost_power(struct usb_device *) // with return type: void void usb_root_hub_lost_power(struct usb_device *arg0) { // Void type return; } // Function: warn_slowpath_null // with type: void warn_slowpath_null(const char *, const int) // with return type: void void warn_slowpath_null(const char *arg0, const int arg1) { // Void type return; }