// Skip function: __VERIFIER_error // Skip function: __VERIFIER_nondet_int // Skip function: __VERIFIER_nondet_ulong // Function: __cpu_to_node // with type: int __cpu_to_node(int) // with return type: int int __VERIFIER_nondet_int(void); int __cpu_to_node(int arg0) { // Simple type return __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: __iscsi_complete_pdu // with type: int __iscsi_complete_pdu(struct iscsi_conn *, struct iscsi_hdr *, char *, int) // with return type: int int __VERIFIER_nondet_int(void); int __iscsi_complete_pdu(struct iscsi_conn *arg0, struct iscsi_hdr *arg1, char *arg2, int arg3) { // Simple type return __VERIFIER_nondet_int(); } // Function: __iscsi_put_task // with type: void __iscsi_put_task(struct iscsi_task *) // with return type: void void __iscsi_put_task(struct iscsi_task *arg0) { // 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: __might_sleep // with type: void __might_sleep(const char *, int, int) // with return type: void void __might_sleep(const char *arg0, int arg1, int 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: __register_cpu_notifier // with type: int __register_cpu_notifier(struct notifier_block *) // with return type: int int __VERIFIER_nondet_int(void); int __register_cpu_notifier(struct notifier_block *arg0) { // Simple type return __VERIFIER_nondet_int(); } // Function: __rwlock_init // with type: void __rwlock_init(rwlock_t *, const char *, struct lock_class_key *) // with return type: void void __rwlock_init(rwlock_t *arg0, const char *arg1, struct lock_class_key *arg2) { // Void type return; } // Function: __unregister_cpu_notifier // with type: void __unregister_cpu_notifier(struct notifier_block *) // with return type: void void __unregister_cpu_notifier(struct notifier_block *arg0) { // 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: _raw_read_lock_bh // with type: void _raw_read_lock_bh(rwlock_t *) // with return type: void void _raw_read_lock_bh(rwlock_t *arg0) { // Void type return; } // Function: _raw_read_unlock_bh // with type: void _raw_read_unlock_bh(rwlock_t *) // with return type: void void _raw_read_unlock_bh(rwlock_t *arg0) { // 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_bh // with type: void _raw_spin_lock_bh(raw_spinlock_t *) // with return type: void void _raw_spin_lock_bh(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_bh // with type: void _raw_spin_unlock_bh(raw_spinlock_t *) // with return type: void void _raw_spin_unlock_bh(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: _raw_write_lock_bh // with type: void _raw_write_lock_bh(rwlock_t *) // with return type: void void _raw_write_lock_bh(rwlock_t *arg0) { // Void type return; } // Function: _raw_write_unlock_bh // with type: void _raw_write_unlock_bh(rwlock_t *) // with return type: void void _raw_write_unlock_bh(rwlock_t *arg0) { // Void type return; } // Function: add_timer // with type: void add_timer(struct timer_list *) // with return type: void void add_timer(struct timer_list *arg0) { // Void type return; } // Skip function: calloc // Function: cnic_register_driver // with type: int cnic_register_driver(int, struct cnic_ulp_ops *) // with return type: int int __VERIFIER_nondet_int(void); int cnic_register_driver(int arg0, struct cnic_ulp_ops *arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: cnic_unregister_driver // with type: int cnic_unregister_driver(int) // with return type: int int __VERIFIER_nondet_int(void); int cnic_unregister_driver(int arg0) { // Simple type return __VERIFIER_nondet_int(); } // Function: complete // with type: void complete(struct completion *) // with return type: void void complete(struct completion *arg0) { // Void type return; } // Function: cpu_maps_update_begin // with type: void cpu_maps_update_begin() // with return type: void void cpu_maps_update_begin() { // Void type return; } // Function: cpu_maps_update_done // with type: void cpu_maps_update_done() // with return type: void void cpu_maps_update_done() { // 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_printk // with type: void dev_printk(const char *, const struct device *, const char *, ...) // with return type: void void dev_printk(const char *arg0, const struct device *arg1, const char *arg2, ...) { // 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: find_next_bit // with type: unsigned long int find_next_bit(const unsigned long *, unsigned long, unsigned long) // with return type: unsigned long int unsigned long __VERIFIER_nondet_ulong(void); unsigned long int find_next_bit(const unsigned long *arg0, unsigned long arg1, unsigned long arg2) { // Simple type return __VERIFIER_nondet_ulong(); } // 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: flush_signals // with type: void flush_signals(struct task_struct *) // with return type: void void flush_signals(struct task_struct *arg0) { // Void type return; } // Function: int_to_scsilun // with type: void int_to_scsilun(u64 , struct scsi_lun *) // with return type: void void int_to_scsilun(u64 arg0, struct scsi_lun *arg1) { // Void type return; } // Function: ioremap_nocache // with type: void *ioremap_nocache(resource_size_t , unsigned long) // with return type: (void)* void *ioremap_nocache(resource_size_t arg0, unsigned long arg1) { // Pointer type return ldv_malloc(0UL); } // Function: iounmap // with type: void iounmap(volatile void *) // with return type: void void iounmap(volatile void *arg0) { // Void type return; } // Function: iscsi_conn_bind // with type: int iscsi_conn_bind(struct iscsi_cls_session *, struct iscsi_cls_conn *, int) // with return type: int int __VERIFIER_nondet_int(void); int iscsi_conn_bind(struct iscsi_cls_session *arg0, struct iscsi_cls_conn *arg1, int arg2) { // Simple type return __VERIFIER_nondet_int(); } // Function: iscsi_conn_failure // with type: void iscsi_conn_failure(struct iscsi_conn *, enum iscsi_err ) // with return type: void void iscsi_conn_failure(struct iscsi_conn *arg0, enum iscsi_err arg1) { // Void type return; } // Function: iscsi_conn_get_param // with type: int iscsi_conn_get_param(struct iscsi_cls_conn *, enum iscsi_param , char *) // with return type: int int __VERIFIER_nondet_int(void); int iscsi_conn_get_param(struct iscsi_cls_conn *arg0, enum iscsi_param arg1, char *arg2) { // Simple type return __VERIFIER_nondet_int(); } // Function: iscsi_conn_send_pdu // with type: int iscsi_conn_send_pdu(struct iscsi_cls_conn *, struct iscsi_hdr *, char *, uint32_t ) // with return type: int int __VERIFIER_nondet_int(void); int iscsi_conn_send_pdu(struct iscsi_cls_conn *arg0, struct iscsi_hdr *arg1, char *arg2, uint32_t arg3) { // Simple type return __VERIFIER_nondet_int(); } // Function: iscsi_conn_setup // with type: struct iscsi_cls_conn *iscsi_conn_setup(struct iscsi_cls_session *, int, uint32_t ) // with return type: (struct iscsi_cls_conn)* struct iscsi_cls_conn *iscsi_conn_setup(struct iscsi_cls_session *arg0, int arg1, uint32_t arg2) { // Pointer type return ldv_malloc(sizeof(struct iscsi_cls_conn)); } // Function: iscsi_conn_start // with type: int iscsi_conn_start(struct iscsi_cls_conn *) // with return type: int int __VERIFIER_nondet_int(void); int iscsi_conn_start(struct iscsi_cls_conn *arg0) { // Simple type return __VERIFIER_nondet_int(); } // Function: iscsi_conn_stop // with type: void iscsi_conn_stop(struct iscsi_cls_conn *, int) // with return type: void void iscsi_conn_stop(struct iscsi_cls_conn *arg0, int arg1) { // Void type return; } // Function: iscsi_conn_teardown // with type: void iscsi_conn_teardown(struct iscsi_cls_conn *) // with return type: void void iscsi_conn_teardown(struct iscsi_cls_conn *arg0) { // Void type return; } // Function: iscsi_create_endpoint // with type: struct iscsi_endpoint *iscsi_create_endpoint(int) // with return type: (struct iscsi_endpoint)* struct iscsi_endpoint *iscsi_create_endpoint(int arg0) { // Pointer type return ldv_malloc(sizeof(struct iscsi_endpoint)); } // Function: iscsi_destroy_endpoint // with type: void iscsi_destroy_endpoint(struct iscsi_endpoint *) // with return type: void void iscsi_destroy_endpoint(struct iscsi_endpoint *arg0) { // Void type return; } // Function: iscsi_eh_abort // with type: int iscsi_eh_abort(struct scsi_cmnd *) // with return type: int int __VERIFIER_nondet_int(void); int iscsi_eh_abort(struct scsi_cmnd *arg0) { // Simple type return __VERIFIER_nondet_int(); } // Function: iscsi_eh_device_reset // with type: int iscsi_eh_device_reset(struct scsi_cmnd *) // with return type: int int __VERIFIER_nondet_int(void); int iscsi_eh_device_reset(struct scsi_cmnd *arg0) { // Simple type return __VERIFIER_nondet_int(); } // Function: iscsi_eh_recover_target // with type: int iscsi_eh_recover_target(struct scsi_cmnd *) // with return type: int int __VERIFIER_nondet_int(void); int iscsi_eh_recover_target(struct scsi_cmnd *arg0) { // Simple type return __VERIFIER_nondet_int(); } // Function: iscsi_host_add // with type: int iscsi_host_add(struct Scsi_Host *, struct device *) // with return type: int int __VERIFIER_nondet_int(void); int iscsi_host_add(struct Scsi_Host *arg0, struct device *arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: iscsi_host_alloc // with type: struct Scsi_Host *iscsi_host_alloc(struct scsi_host_template *, int, bool ) // with return type: (struct Scsi_Host)* struct Scsi_Host *iscsi_host_alloc(struct scsi_host_template *arg0, int arg1, bool arg2) { // Pointer type return ldv_malloc(sizeof(struct Scsi_Host)); } // Function: iscsi_host_for_each_session // with type: void iscsi_host_for_each_session(struct Scsi_Host *, void (*)(struct iscsi_cls_session *)) // with return type: void void iscsi_host_for_each_session(struct Scsi_Host *arg0, void (*arg1)(struct iscsi_cls_session *)) { // Void type return; } // Function: iscsi_host_free // with type: void iscsi_host_free(struct Scsi_Host *) // with return type: void void iscsi_host_free(struct Scsi_Host *arg0) { // Void type return; } // Function: iscsi_host_get_param // with type: int iscsi_host_get_param(struct Scsi_Host *, enum iscsi_host_param , char *) // with return type: int int __VERIFIER_nondet_int(void); int iscsi_host_get_param(struct Scsi_Host *arg0, enum iscsi_host_param arg1, char *arg2) { // Simple type return __VERIFIER_nondet_int(); } // Function: iscsi_host_remove // with type: void iscsi_host_remove(struct Scsi_Host *) // with return type: void void iscsi_host_remove(struct Scsi_Host *arg0) { // Void type return; } // Function: iscsi_itt_to_task // with type: struct iscsi_task *iscsi_itt_to_task(struct iscsi_conn *, itt_t ) // with return type: (struct iscsi_task)* struct iscsi_task *iscsi_itt_to_task(struct iscsi_conn *arg0, itt_t arg1) { // Pointer type return ldv_malloc(sizeof(struct iscsi_task)); } // Function: iscsi_lookup_endpoint // with type: struct iscsi_endpoint *iscsi_lookup_endpoint(u64 ) // with return type: (struct iscsi_endpoint)* struct iscsi_endpoint *iscsi_lookup_endpoint(u64 arg0) { // Pointer type return ldv_malloc(sizeof(struct iscsi_endpoint)); } // Function: iscsi_offload_mesg // with type: int iscsi_offload_mesg(struct Scsi_Host *, struct iscsi_transport *, uint32_t , char *, uint16_t ) // with return type: int int __VERIFIER_nondet_int(void); int iscsi_offload_mesg(struct Scsi_Host *arg0, struct iscsi_transport *arg1, uint32_t arg2, char *arg3, uint16_t arg4) { // Simple type return __VERIFIER_nondet_int(); } // Function: iscsi_queuecommand // with type: int iscsi_queuecommand(struct Scsi_Host *, struct scsi_cmnd *) // with return type: int int __VERIFIER_nondet_int(void); int iscsi_queuecommand(struct Scsi_Host *arg0, struct scsi_cmnd *arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: iscsi_register_transport // with type: struct scsi_transport_template *iscsi_register_transport(struct iscsi_transport *) // with return type: (struct scsi_transport_template)* struct scsi_transport_template *iscsi_register_transport(struct iscsi_transport *arg0) { // Pointer type return ldv_malloc(0UL); } // Function: iscsi_session_failure // with type: void iscsi_session_failure(struct iscsi_session *, enum iscsi_err ) // with return type: void void iscsi_session_failure(struct iscsi_session *arg0, enum iscsi_err arg1) { // Void type return; } // Function: iscsi_session_get_param // with type: int iscsi_session_get_param(struct iscsi_cls_session *, enum iscsi_param , char *) // with return type: int int __VERIFIER_nondet_int(void); int iscsi_session_get_param(struct iscsi_cls_session *arg0, enum iscsi_param arg1, char *arg2) { // Simple type return __VERIFIER_nondet_int(); } // Function: iscsi_session_recovery_timedout // with type: void iscsi_session_recovery_timedout(struct iscsi_cls_session *) // with return type: void void iscsi_session_recovery_timedout(struct iscsi_cls_session *arg0) { // Void type return; } // Function: iscsi_session_setup // with type: struct iscsi_cls_session *iscsi_session_setup(struct iscsi_transport *, struct Scsi_Host *, uint16_t , int, int, uint32_t , unsigned int) // with return type: (struct iscsi_cls_session)* struct iscsi_cls_session *iscsi_session_setup(struct iscsi_transport *arg0, struct Scsi_Host *arg1, uint16_t arg2, int arg3, int arg4, uint32_t arg5, unsigned int arg6) { // Pointer type return ldv_malloc(sizeof(struct iscsi_cls_session)); } // Function: iscsi_session_teardown // with type: void iscsi_session_teardown(struct iscsi_cls_session *) // with return type: void void iscsi_session_teardown(struct iscsi_cls_session *arg0) { // Void type return; } // Function: iscsi_set_param // with type: int iscsi_set_param(struct iscsi_cls_conn *, enum iscsi_param , char *, int) // with return type: int int __VERIFIER_nondet_int(void); int iscsi_set_param(struct iscsi_cls_conn *arg0, enum iscsi_param arg1, char *arg2, int arg3) { // Simple type return __VERIFIER_nondet_int(); } // Function: iscsi_suspend_queue // with type: void iscsi_suspend_queue(struct iscsi_conn *) // with return type: void void iscsi_suspend_queue(struct iscsi_conn *arg0) { // Void type return; } // Function: iscsi_target_alloc // with type: int iscsi_target_alloc(struct scsi_target *) // with return type: int int __VERIFIER_nondet_int(void); int iscsi_target_alloc(struct scsi_target *arg0) { // Simple type return __VERIFIER_nondet_int(); } // Function: iscsi_unregister_transport // with type: int iscsi_unregister_transport(struct iscsi_transport *) // with return type: int int __VERIFIER_nondet_int(void); int iscsi_unregister_transport(struct iscsi_transport *arg0) { // Simple type return __VERIFIER_nondet_int(); } // Skip function: kfree // Function: kthread_bind // with type: void kthread_bind(struct task_struct *, unsigned int) // with return type: void void kthread_bind(struct task_struct *arg0, unsigned int arg1) { // Void type return; } // 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: 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_probe_6 // with type: int ldv_probe_6() // with return type: int int __VERIFIER_nondet_int(void); int ldv_probe_6() { // Simple type return __VERIFIER_nondet_int(); } // 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: memcpy // Skip function: memmove // Skip function: memset // 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: pci_dev_get // with type: struct pci_dev *pci_dev_get(struct pci_dev *) // with return type: (struct pci_dev)* struct pci_dev *pci_dev_get(struct pci_dev *arg0) { // Pointer type return ldv_malloc(sizeof(struct pci_dev)); } // Function: pci_dev_put // with type: void pci_dev_put(struct pci_dev *) // with return type: void void pci_dev_put(struct pci_dev *arg0) { // Void type return; } // Function: pci_iomap // with type: void *pci_iomap(struct pci_dev *, int, unsigned long) // with return type: (void)* void *pci_iomap(struct pci_dev *arg0, int arg1, unsigned long arg2) { // Pointer type return ldv_malloc(arg2); } // Function: pci_iounmap // with type: void pci_iounmap(struct pci_dev *, void *) // with return type: void void pci_iounmap(struct pci_dev *arg0, void *arg1) { // Void type return; } // Function: prepare_to_wait_event // with type: long int prepare_to_wait_event(wait_queue_head_t *, wait_queue_t *, int) // with return type: long int long __VERIFIER_nondet_long(void); long int prepare_to_wait_event(wait_queue_head_t *arg0, wait_queue_t *arg1, int arg2) { // 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: 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(); } // Function: scsi_change_queue_depth // with type: int scsi_change_queue_depth(struct scsi_device *, int) // with return type: int int __VERIFIER_nondet_int(void); int scsi_change_queue_depth(struct scsi_device *arg0, int arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: scsi_dma_map // with type: int scsi_dma_map(struct scsi_cmnd *) // with return type: int int __VERIFIER_nondet_int(void); int scsi_dma_map(struct scsi_cmnd *arg0) { // Simple type return __VERIFIER_nondet_int(); } // Function: scsi_dma_unmap // with type: void scsi_dma_unmap(struct scsi_cmnd *) // with return type: void void scsi_dma_unmap(struct scsi_cmnd *arg0) { // Void type return; } // Function: scsi_host_put // with type: void scsi_host_put(struct Scsi_Host *) // with return type: void void scsi_host_put(struct Scsi_Host *arg0) { // Void type return; } // Function: scsi_is_host_device // with type: int scsi_is_host_device(const struct device *) // with return type: int int __VERIFIER_nondet_int(void); int scsi_is_host_device(const struct device *arg0) { // Simple type return __VERIFIER_nondet_int(); } // Function: set_user_nice // with type: void set_user_nice(struct task_struct *, long) // with return type: void void set_user_nice(struct task_struct *arg0, long 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)); } // Skip function: sprintf // Skip function: sscanf // 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: sysfs_format_mac // with type: ssize_t sysfs_format_mac(char *, const unsigned char *, int) // with return type: ssize_t long __VERIFIER_nondet_long(void); ssize_t sysfs_format_mac(char *arg0, const unsigned char *arg1, int arg2) { // 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: wait_for_completion_timeout // with type: unsigned long int wait_for_completion_timeout(struct completion *, unsigned long) // with return type: unsigned long int unsigned long __VERIFIER_nondet_ulong(void); unsigned long int wait_for_completion_timeout(struct completion *arg0, unsigned long arg1) { // Simple type return __VERIFIER_nondet_ulong(); } // 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(); } // 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; }