// Skip function: __VERIFIER_error // Skip function: __VERIFIER_nondet_int // Skip function: __VERIFIER_nondet_ulong // 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: _dev_info // with type: void _dev_info(const struct device *, const char *, ...) // with return type: void void _dev_info(const struct device *arg0, const char *arg1, ...) { // Void type return; } // Skip function: calloc // Function: complete // with type: void complete(struct completion *) // with return type: void void complete(struct completion *arg0) { // Void type return; } // Function: consume_skb // with type: void consume_skb(struct sk_buff *) // with return type: void void consume_skb(struct sk_buff *arg0) { // Void type return; } // 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: devm_kmalloc // with type: void *devm_kmalloc(struct device *, size_t , gfp_t ) // with return type: (void)* void *devm_kmalloc(struct device *arg0, size_t arg1, gfp_t arg2) { // Pointer type return ldv_malloc(0UL); } // Skip function: free // Skip function: kfree // Function: kfree_skb // with type: void kfree_skb(struct sk_buff *) // with return type: void void kfree_skb(struct sk_buff *arg0) { // Void type return; } // Function: ldv_after_alloc // with type: void ldv_after_alloc(void *) // with return type: void void ldv_after_alloc(void *arg0) { // Void type return; } // Function: ldv_assert // with type: void ldv_assert(const char *, int) // with return type: void void ldv_assert(const char *arg0, int arg1) { // Void type return; } // Function: ldv_pre_probe // with type: void ldv_pre_probe() // with return type: void void ldv_pre_probe() { // 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: nfc_digital_allocate_device // with type: struct nfc_digital_dev *nfc_digital_allocate_device(struct nfc_digital_ops *, __u32 , __u32 , int, int) // with return type: (struct nfc_digital_dev)* struct nfc_digital_dev *nfc_digital_allocate_device(struct nfc_digital_ops *arg0, __u32 arg1, __u32 arg2, int arg3, int arg4) { // Pointer type return ldv_malloc(sizeof(struct nfc_digital_dev)); } // Function: nfc_digital_free_device // with type: void nfc_digital_free_device(struct nfc_digital_dev *) // with return type: void void nfc_digital_free_device(struct nfc_digital_dev *arg0) { // Void type return; } // Function: nfc_digital_register_device // with type: int nfc_digital_register_device(struct nfc_digital_dev *) // with return type: int int __VERIFIER_nondet_int(void); int nfc_digital_register_device(struct nfc_digital_dev *arg0) { // Simple type return __VERIFIER_nondet_int(); } // Function: nfc_digital_unregister_device // with type: void nfc_digital_unregister_device(struct nfc_digital_dev *) // with return type: void void nfc_digital_unregister_device(struct nfc_digital_dev *arg0) { // Void type return; } // Function: print_hex_dump // with type: void print_hex_dump(const char *, const char *, int, int, int, const void *, size_t , bool ) // with return type: void void print_hex_dump(const char *arg0, const char *arg1, int arg2, int arg3, int arg4, const void *arg5, size_t arg6, bool arg7) { // Void type return; } // 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: 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_trim // with type: void skb_trim(struct sk_buff *, unsigned int) // with return type: void void skb_trim(struct sk_buff *arg0, unsigned int arg1) { // Void type return; } // 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_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_unlink_urb // with type: int usb_unlink_urb(struct urb *) // with return type: int int __VERIFIER_nondet_int(void); int usb_unlink_urb(struct urb *arg0) { // Simple type return __VERIFIER_nondet_int(); } // 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; }