// Skip function: __VERIFIER_error // Skip function: __VERIFIER_nondet_int // 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: __ldv_spin_lock // with type: void __ldv_spin_lock(spinlock_t *) // with return type: void void __ldv_spin_lock(spinlock_t *arg0) { // 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: __release_region // with type: void __release_region(struct resource *, resource_size_t , resource_size_t ) // with return type: void void __release_region(struct resource *arg0, resource_size_t arg1, resource_size_t arg2) { // Void type return; } // Function: __request_region // with type: struct resource *__request_region(struct resource *, resource_size_t , resource_size_t , const char *, int) // with return type: (struct resource)* struct resource *__request_region(struct resource *arg0, resource_size_t arg1, resource_size_t arg2, const char *arg3, int arg4) { // Pointer type return ldv_malloc(sizeof(struct resource)); } // 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_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; } // Skip function: calloc // Function: dev_err // with type: int dev_err(const struct device *, const char *, ...) // with return type: int int __VERIFIER_nondet_int(void); int dev_err(const struct device *arg0, const char *arg1, ...) { // Simple type return __VERIFIER_nondet_int(); } // Function: device_init_wakeup // with type: int device_init_wakeup(struct device *, bool ) // with return type: int int __VERIFIER_nondet_int(void); int device_init_wakeup(struct device *arg0, bool arg1) { // Simple type return __VERIFIER_nondet_int(); } // 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; } // Skip function: free // Function: free_irq // with type: void free_irq(unsigned int, void *) // with return type: void void free_irq(unsigned int arg0, void *arg1) { // Void type return; } // Function: ir_raw_event_handle // with type: void ir_raw_event_handle(struct rc_dev *) // with return type: void void ir_raw_event_handle(struct rc_dev *arg0) { // Void type return; } // Function: ir_raw_event_store // with type: int ir_raw_event_store(struct rc_dev *, struct ir_raw_event *) // with return type: int int __VERIFIER_nondet_int(void); int ir_raw_event_store(struct rc_dev *arg0, struct ir_raw_event *arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: ir_raw_event_store_with_filter // with type: int ir_raw_event_store_with_filter(struct rc_dev *, struct ir_raw_event *) // with return type: int int __VERIFIER_nondet_int(void); int ir_raw_event_store_with_filter(struct rc_dev *arg0, struct ir_raw_event *arg1) { // Simple type return __VERIFIER_nondet_int(); } // Skip function: kfree // 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_check_alloc_flags // with type: void ldv_check_alloc_flags(gfp_t ) // with return type: void void ldv_check_alloc_flags(gfp_t arg0) { // Void type return; } // Function: ldv_initialize // with type: void ldv_initialize() // with return type: void void ldv_initialize() { // Void type return; } // Function: ldv_switch_to_interrupt_context // with type: void ldv_switch_to_interrupt_context() // with return type: void void ldv_switch_to_interrupt_context() { // Void type return; } // Function: ldv_switch_to_process_context // with type: void ldv_switch_to_process_context() // with return type: void void ldv_switch_to_process_context() { // Void type return; } // Skip function: malloc // Skip function: memcpy // Skip function: memset // Function: pnp_get_resource // with type: struct resource *pnp_get_resource(struct pnp_dev *, unsigned long, unsigned int) // with return type: (struct resource)* struct resource *pnp_get_resource(struct pnp_dev *arg0, unsigned long arg1, unsigned int arg2) { // Pointer type return ldv_malloc(sizeof(struct resource)); } // Function: pnp_register_driver // with type: int pnp_register_driver(struct pnp_driver *) // with return type: int int __VERIFIER_nondet_int(void); int pnp_register_driver(struct pnp_driver *arg0) { // Simple type return __VERIFIER_nondet_int(); } // Function: pnp_unregister_driver // with type: void pnp_unregister_driver(struct pnp_driver *) // with return type: void void pnp_unregister_driver(struct pnp_driver *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: rc_allocate_device // with type: struct rc_dev *rc_allocate_device() // with return type: (struct rc_dev)* struct rc_dev *rc_allocate_device() { // Pointer type return ldv_malloc(sizeof(struct rc_dev)); } // Function: rc_free_device // with type: void rc_free_device(struct rc_dev *) // with return type: void void rc_free_device(struct rc_dev *arg0) { // Void type return; } // Function: rc_register_device // with type: int rc_register_device(struct rc_dev *) // with return type: int int __VERIFIER_nondet_int(void); int rc_register_device(struct rc_dev *arg0) { // Simple type return __VERIFIER_nondet_int(); } // Function: rc_unregister_device // with type: void rc_unregister_device(struct rc_dev *) // with return type: void void rc_unregister_device(struct rc_dev *arg0) { // Void type return; } // Function: request_threaded_irq // with type: int request_threaded_irq(unsigned int, irqreturn_t (*)(int, void *), irqreturn_t (*)(int, void *), unsigned long, const char *, void *) // with return type: int int __VERIFIER_nondet_int(void); int request_threaded_irq(unsigned int arg0, irqreturn_t (*arg1)(int, void *), irqreturn_t (*arg2)(int, void *), unsigned long arg3, const char *arg4, void *arg5) { // Simple type return __VERIFIER_nondet_int(); } // Function: schedule // with type: void schedule() // with return type: void void schedule() { // Void type return; } // Skip function: strcpy