// Skip function: __VERIFIER_error // Skip function: __VERIFIER_nondet_int // Skip function: __VERIFIER_nondet_u16 // Skip function: __VERIFIER_nondet_u32 // Skip function: __VERIFIER_nondet_u8 // Skip function: __VERIFIER_nondet_uint // Skip function: __VERIFIER_nondet_ulong // 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; } // Skip function: calloc // Function: complete_and_exit // with type: void complete_and_exit(struct completion *, long) // with return type: void void complete_and_exit(struct completion *arg0, long arg1) { // Void type return; } // 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_recursive // with type: void debugfs_remove_recursive(struct dentry *) // with return type: void void debugfs_remove_recursive(struct dentry *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: ieee80211_alloc_hw // with type: struct ieee80211_hw *ieee80211_alloc_hw(size_t , const struct ieee80211_ops *) // with return type: (struct ieee80211_hw)* struct ieee80211_hw *ieee80211_alloc_hw(size_t arg0, const struct ieee80211_ops *arg1) { // Pointer type return ldv_malloc(sizeof(struct ieee80211_hw)); } // Function: ieee80211_channel_to_frequency // with type: int ieee80211_channel_to_frequency(int, enum ieee80211_band ) // with return type: int int __VERIFIER_nondet_int(void); int ieee80211_channel_to_frequency(int arg0, enum ieee80211_band arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: ieee80211_free_hw // with type: void ieee80211_free_hw(struct ieee80211_hw *) // with return type: void void ieee80211_free_hw(struct ieee80211_hw *arg0) { // Void type return; } // Function: ieee80211_free_txskb // with type: void ieee80211_free_txskb(struct ieee80211_hw *, struct sk_buff *) // with return type: void void ieee80211_free_txskb(struct ieee80211_hw *arg0, struct sk_buff *arg1) { // Void type return; } // Function: ieee80211_hdrlen // with type: unsigned int ieee80211_hdrlen(__le16 ) // with return type: unsigned int unsigned int __VERIFIER_nondet_uint(void); unsigned int ieee80211_hdrlen(__le16 arg0) { // Simple type return __VERIFIER_nondet_uint(); } // Function: ieee80211_queue_stopped // with type: int ieee80211_queue_stopped(struct ieee80211_hw *, int) // with return type: int int __VERIFIER_nondet_int(void); int ieee80211_queue_stopped(struct ieee80211_hw *arg0, int arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: ieee80211_register_hw // with type: int ieee80211_register_hw(struct ieee80211_hw *) // with return type: int int __VERIFIER_nondet_int(void); int ieee80211_register_hw(struct ieee80211_hw *arg0) { // Simple type return __VERIFIER_nondet_int(); } // Function: ieee80211_rx_irqsafe // with type: void ieee80211_rx_irqsafe(struct ieee80211_hw *, struct sk_buff *) // with return type: void void ieee80211_rx_irqsafe(struct ieee80211_hw *arg0, struct sk_buff *arg1) { // Void type return; } // Function: ieee80211_start_tx_ba_cb_irqsafe // with type: void ieee80211_start_tx_ba_cb_irqsafe(struct ieee80211_vif *, const u8 *, u16 ) // with return type: void void ieee80211_start_tx_ba_cb_irqsafe(struct ieee80211_vif *arg0, const u8 *arg1, u16 arg2) { // Void type return; } // Function: ieee80211_start_tx_ba_session // with type: int ieee80211_start_tx_ba_session(struct ieee80211_sta *, u16 , u16 ) // with return type: int int __VERIFIER_nondet_int(void); int ieee80211_start_tx_ba_session(struct ieee80211_sta *arg0, u16 arg1, u16 arg2) { // Simple type return __VERIFIER_nondet_int(); } // Function: ieee80211_stop_queue // with type: void ieee80211_stop_queue(struct ieee80211_hw *, int) // with return type: void void ieee80211_stop_queue(struct ieee80211_hw *arg0, int arg1) { // Void type return; } // Function: ieee80211_stop_queues // with type: void ieee80211_stop_queues(struct ieee80211_hw *) // with return type: void void ieee80211_stop_queues(struct ieee80211_hw *arg0) { // Void type return; } // Function: ieee80211_stop_tx_ba_cb_irqsafe // with type: void ieee80211_stop_tx_ba_cb_irqsafe(struct ieee80211_vif *, const u8 *, u16 ) // with return type: void void ieee80211_stop_tx_ba_cb_irqsafe(struct ieee80211_vif *arg0, const u8 *arg1, u16 arg2) { // Void type return; } // Function: ieee80211_tx_status_irqsafe // with type: void ieee80211_tx_status_irqsafe(struct ieee80211_hw *, struct sk_buff *) // with return type: void void ieee80211_tx_status_irqsafe(struct ieee80211_hw *arg0, struct sk_buff *arg1) { // Void type return; } // Function: ieee80211_unregister_hw // with type: void ieee80211_unregister_hw(struct ieee80211_hw *) // with return type: void void ieee80211_unregister_hw(struct ieee80211_hw *arg0) { // Void type return; } // Function: ieee80211_wake_queue // with type: void ieee80211_wake_queue(struct ieee80211_hw *, int) // with return type: void void ieee80211_wake_queue(struct ieee80211_hw *arg0, int arg1) { // Void type return; } // Skip function: kfree // Function: kstrtoul_from_user // with type: int kstrtoul_from_user(const char *, size_t , unsigned int, unsigned long *) // with return type: int int __VERIFIER_nondet_int(void); int kstrtoul_from_user(const char *arg0, size_t arg1, unsigned int arg2, unsigned long *arg3) { // Simple type return __VERIFIER_nondet_int(); } // 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_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__builtin_va_end // with type: void ldv__builtin_va_end(__builtin_va_list ) // with return type: void void ldv__builtin_va_end(__builtin_va_list arg0) { // Void type return; } // Function: ldv__builtin_va_start // with type: void ldv__builtin_va_start(__builtin_va_list ) // with return type: void void ldv__builtin_va_start(__builtin_va_list arg0) { // Void type return; } // Skip function: malloc // Skip function: memcmp // Skip function: memcpy // Skip function: memmove // Skip function: memset // 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_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: seq_printf // with type: int seq_printf(struct seq_file *, const char *, ...) // with return type: int int __VERIFIER_nondet_int(void); int seq_printf(struct seq_file *arg0, const char *arg1, ...) { // Simple type return __VERIFIER_nondet_int(); } // Function: seq_puts // with type: int seq_puts(struct seq_file *, const char *) // with return type: int int __VERIFIER_nondet_int(void); int seq_puts(struct seq_file *arg0, const char *arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: single_open // with type: int single_open(struct file *, int (*)(struct seq_file *, void *), void *) // with return type: int int __VERIFIER_nondet_int(void); int single_open(struct file *arg0, int (*arg1)(struct seq_file *, void *), void *arg2) { // Simple type return __VERIFIER_nondet_int(); } // Function: skb_pull // with type: unsigned char *skb_pull(struct sk_buff *, unsigned int) // with return type: (unsigned char)* unsigned char *skb_pull(struct sk_buff *arg0, unsigned int arg1) { // Pointer type return ldv_malloc(sizeof(unsigned char)); } // Function: skb_push // with type: unsigned char *skb_push(struct sk_buff *, unsigned int) // with return type: (unsigned char)* unsigned char *skb_push(struct sk_buff *arg0, unsigned int arg1) { // Pointer type return ldv_malloc(sizeof(unsigned char)); } // Function: skb_put // with type: unsigned char *skb_put(struct sk_buff *, unsigned int) // with return type: (unsigned char)* unsigned char *skb_put(struct sk_buff *arg0, unsigned int arg1) { unsigned char *ret_val = arg0->data + arg0->tail; // a more precise implementation of skb_put would actually re-allocate memory // here arg0->tail += arg1; // Pointer type return ret_val; } // Function: skb_queue_purge // with type: void skb_queue_purge(struct sk_buff_head *) // with return type: void void skb_queue_purge(struct sk_buff_head *arg0) { // Void type return; } // Function: skb_queue_tail // with type: void skb_queue_tail(struct sk_buff_head *, struct sk_buff *) // with return type: void void skb_queue_tail(struct sk_buff_head *arg0, struct sk_buff *arg1) { // Void type return; } // Skip function: snprintf // Function: sort // with type: void sort(void *, size_t , size_t , int (*)(const void *, const void *), void (*)(void *, void *, int)) // with return type: void void sort(void *arg0, size_t arg1, size_t arg2, int (*arg3)(const void *, const void *), void (*arg4)(void *, void *, int)) { // Void type return; } // 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: 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_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; }