// Skip function: __VERIFIER_error // Skip function: __VERIFIER_nondet_int // Skip function: __VERIFIER_nondet_ulong // Skip function: __VERIFIER_nondet_ushort // Function: __dev_kfree_skb_irq // with type: void __dev_kfree_skb_irq(struct sk_buff *, enum skb_free_reason ) // with return type: void void __dev_kfree_skb_irq(struct sk_buff *arg0, enum skb_free_reason arg1) { // Void type return; } // Function: arcnet_unregister_proto // with type: void arcnet_unregister_proto(struct ArcProto *) // with return type: void void arcnet_unregister_proto(struct ArcProto *arg0) { // Void type return; } // Skip function: calloc // 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: 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; }