// 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: __dev_kfree_skb_any // with type: void __dev_kfree_skb_any(struct sk_buff *, enum skb_free_reason ) // with return type: void void __dev_kfree_skb_any(struct sk_buff *arg0, enum skb_free_reason arg1) { // Void type return; } // Function: __netdev_alloc_skb // with type: struct sk_buff *__netdev_alloc_skb(struct net_device *, unsigned int, gfp_t ) // with return type: (struct sk_buff)* struct sk_buff *__netdev_alloc_skb(struct net_device *arg0, unsigned int arg1, gfp_t arg2) { // Pointer type struct sk_buff *skb = ldv_malloc(sizeof(struct sk_buff)); if(skb) { skb->dev = arg0; skb->head = ldv_malloc(arg1); skb->data = skb->head; skb->tail = 0; } return skb; } // 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: 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: hisax_register // with type: int hisax_register(struct hisax_d_if *, struct hisax_b_if **, char *, int) // with return type: int int __VERIFIER_nondet_int(void); int hisax_register(struct hisax_d_if *arg0, struct hisax_b_if **arg1, char *arg2, int arg3) { // Simple type return __VERIFIER_nondet_int(); } // Function: hisax_unregister // with type: void hisax_unregister(struct hisax_d_if *) // with return type: void void hisax_unregister(struct hisax_d_if *arg0) { // Void type return; } // Skip function: kfree // Function: kmem_cache_alloc // with type: void *kmem_cache_alloc(struct kmem_cache *, gfp_t ) // with return type: (void)* void *kmem_cache_alloc(struct kmem_cache *arg0, gfp_t arg1) { // Pointer type return ldv_malloc(0UL); } // 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___0 *ldv_some_page() // with return type: (struct page___0)* struct page___0 *ldv_some_page() { // Pointer type return ldv_malloc(sizeof(struct page___0)); } // Skip function: malloc // Skip function: memcpy // Skip function: memset // 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: pskb_expand_head // with type: int pskb_expand_head(struct sk_buff *, int, int, gfp_t ) // with return type: int int __VERIFIER_nondet_int(void); int pskb_expand_head(struct sk_buff *arg0, int arg1, int arg2, gfp_t arg3) { // Simple type return __VERIFIER_nondet_int(); } // 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: skb_clone // with type: struct sk_buff *skb_clone(struct sk_buff *, gfp_t ) // with return type: (struct sk_buff)* struct sk_buff *skb_clone(struct sk_buff *arg0, gfp_t arg1) { // Pointer type return ldv_malloc(sizeof(struct sk_buff)); } // Function: skb_copy // with type: struct sk_buff *skb_copy(const struct sk_buff *, gfp_t ) // with return type: (struct sk_buff)* struct sk_buff *skb_copy(const struct sk_buff *arg0, gfp_t arg1) { // Pointer type return ldv_malloc(sizeof(struct sk_buff)); } // 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_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; } // Skip function: sscanf // Function: usb_alloc_urb // with type: struct urb *usb_alloc_urb(int, gfp_t ) // with return type: (struct urb)* struct urb *usb_alloc_urb(int arg0, gfp_t arg1) { // Pointer type return ldv_malloc(sizeof(struct urb)); } // 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_urb // with type: void usb_free_urb(struct urb *) // with return type: void void usb_free_urb(struct urb *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_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: usb_submit_urb // with type: int usb_submit_urb(struct urb *, gfp_t ) // with return type: int int __VERIFIER_nondet_int(void); int usb_submit_urb(struct urb *arg0, gfp_t arg1) { // Simple type return __VERIFIER_nondet_int(); }