// Skip function: __VERIFIER_error // Skip function: __VERIFIER_nondet_int // Function: __get_free_pages // with type: unsigned long int __get_free_pages(gfp_t , unsigned int) // with return type: unsigned long int unsigned long __VERIFIER_nondet_ulong(void); unsigned long int __get_free_pages(gfp_t arg0, unsigned int arg1) { // Simple type return __VERIFIER_nondet_ulong(); } // Function: __init_waitqueue_head // with type: void __init_waitqueue_head(wait_queue_head_t *, struct lock_class_key *) // with return type: void void __init_waitqueue_head(wait_queue_head_t *arg0, struct lock_class_key *arg1) { // Void type return; } // Function: __phys_addr // with type: unsigned long int __phys_addr(unsigned long) // with return type: unsigned long int unsigned long __VERIFIER_nondet_ulong(void); unsigned long int __phys_addr(unsigned long arg0) { // Simple type return __VERIFIER_nondet_ulong(); } // 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: __request_module // with type: int __request_module(bool , const char *, ...) // with return type: int int __VERIFIER_nondet_int(void); int __request_module(bool arg0, const char *arg1, ...) { // Simple type return __VERIFIER_nondet_int(); } // 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: _copy_from_user // with type: unsigned long int _copy_from_user(void *, const void *, unsigned int) // with return type: unsigned long int unsigned long __VERIFIER_nondet_ulong(void); unsigned long int _copy_from_user(void *arg0, const void *arg1, unsigned int arg2) { // Simple type return __VERIFIER_nondet_ulong(); } // Function: _copy_to_user // with type: unsigned long int _copy_to_user(void *, const void *, unsigned int) // with return type: unsigned long int unsigned long __VERIFIER_nondet_ulong(void); unsigned long int _copy_to_user(void *arg0, const void *arg1, unsigned int arg2) { // Simple type return __VERIFIER_nondet_ulong(); } // Function: _lock_kernel // with type: void _lock_kernel(const char *, const char *, int) // with return type: void void _lock_kernel(const char *arg0, const char *arg1, int arg2) { // Void type return; } // Function: _raw_spin_lock // with type: void _raw_spin_lock(raw_spinlock_t *) // with return type: void void _raw_spin_lock(raw_spinlock_t *arg0) { // Void type return; } // Function: _raw_spin_lock_irq // with type: void _raw_spin_lock_irq(raw_spinlock_t *) // with return type: void void _raw_spin_lock_irq(raw_spinlock_t *arg0) { // Void type return; } // Function: _raw_spin_lock_irqsave // with type: unsigned long int _raw_spin_lock_irqsave(raw_spinlock_t *) // with return type: unsigned long int unsigned long __VERIFIER_nondet_ulong(void); unsigned long int _raw_spin_lock_irqsave(raw_spinlock_t *arg0) { // Simple type return __VERIFIER_nondet_ulong(); } // Function: _raw_spin_unlock // with type: void _raw_spin_unlock(raw_spinlock_t *) // with return type: void void _raw_spin_unlock(raw_spinlock_t *arg0) { // Void type return; } // Function: _raw_spin_unlock_irq // with type: void _raw_spin_unlock_irq(raw_spinlock_t *) // with return type: void void _raw_spin_unlock_irq(raw_spinlock_t *arg0) { // 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; } // Function: _unlock_kernel // with type: void _unlock_kernel(const char *, const char *, int) // with return type: void void _unlock_kernel(const char *arg0, const char *arg1, int arg2) { // Void type return; } // 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; } // Function: debug_lockdep_rcu_enabled // with type: int debug_lockdep_rcu_enabled() // with return type: int int __VERIFIER_nondet_int(void); int debug_lockdep_rcu_enabled() { // Simple type return __VERIFIER_nondet_int(); } // 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: del_timer_sync // with type: int del_timer_sync(struct timer_list *) // with return type: int int __VERIFIER_nondet_int(void); int del_timer_sync(struct timer_list *arg0) { // Simple type return __VERIFIER_nondet_int(); } extern _Bool __VERIFIER_nondet_bool(void) ; extern void *malloc(size_t) ; void *ldv_malloc(size_t size ) { if(__VERIFIER_nondet_bool()) return 0; return malloc(size); } // Function: device_create // with type: struct device *device_create(struct class *, struct device *, dev_t , void *, const char *, ...) // with return type: (struct device)* struct device *device_create(struct class *arg0, struct device *arg1, dev_t arg2, void *arg3, const char *arg4, ...) { // Pointer type return ldv_malloc(sizeof(struct device)); } // Function: device_destroy // with type: void device_destroy(struct class *, dev_t ) // with return type: void void device_destroy(struct class *arg0, dev_t arg1) { // Void type return; } // Function: free_dma // with type: void free_dma(unsigned int) // with return type: void void free_dma(unsigned int arg0) { // Void type return; } // Function: free_pages // with type: void free_pages(unsigned long, unsigned int) // with return type: void void free_pages(unsigned long arg0, unsigned int arg1) { // Void type return; } // Function: interruptible_sleep_on // with type: void interruptible_sleep_on(wait_queue_head_t *) // with return type: void void interruptible_sleep_on(wait_queue_head_t *arg0) { // Void type return; } // Function: interruptible_sleep_on_timeout // with type: long int interruptible_sleep_on_timeout(wait_queue_head_t *, long) // with return type: long int long __VERIFIER_nondet_long(void); long int interruptible_sleep_on_timeout(wait_queue_head_t *arg0, long arg1) { // Simple type return __VERIFIER_nondet_long(); } // Function: ldv_check_return_value // with type: void ldv_check_return_value(int) // with return type: void void ldv_check_return_value(int arg0) { // Void type return; } // Function: ldv_handler_precall // with type: void ldv_handler_precall() // with return type: void void ldv_handler_precall() { // Void type return; } // Function: lockdep_rcu_dereference // with type: void lockdep_rcu_dereference(const char *, const int) // with return type: void void lockdep_rcu_dereference(const char *arg0, const int arg1) { // Void type return; } // Skip function: memcpy // Skip function: memset // Function: might_fault // with type: void might_fault() // with return type: void void might_fault() { // Void type return; } // Function: module_put // with type: void module_put(struct module *) // with return type: void void module_put(struct module *arg0) { // Void type return; } // Function: mutex_lock // with type: void mutex_lock(struct mutex *) // with return type: void void mutex_lock(struct mutex *arg0) { // Void type return; } // Function: mutex_trylock // with type: int mutex_trylock(struct mutex *) // with return type: int int __VERIFIER_nondet_int(void); int mutex_trylock(struct mutex *arg0) { // Simple type return __VERIFIER_nondet_int(); } // Function: mutex_unlock // with type: void mutex_unlock(struct mutex *) // with return type: void void mutex_unlock(struct mutex *arg0) { // Void type return; } // Function: panic // with type: void panic(const char *, ...) // with return type: void void panic(const char *arg0, ...) { // Void type return; } // 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: register_sound_dsp // with type: int register_sound_dsp(const struct file_operations *, int) // with return type: int int __VERIFIER_nondet_int(void); int register_sound_dsp(const struct file_operations *arg0, int arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: register_sound_midi // with type: int register_sound_midi(const struct file_operations *, int) // with return type: int int __VERIFIER_nondet_int(void); int register_sound_midi(const struct file_operations *arg0, int arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: register_sound_mixer // with type: int register_sound_mixer(const struct file_operations *, int) // with return type: int int __VERIFIER_nondet_int(void); int register_sound_mixer(const struct file_operations *arg0, int arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: register_sound_special // with type: int register_sound_special(const struct file_operations *, int) // with return type: int int __VERIFIER_nondet_int(void); int register_sound_special(const struct file_operations *arg0, int arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: remap_pfn_range // with type: int remap_pfn_range(struct vm_area_struct *, unsigned long, unsigned long, unsigned long, pgprot_t ) // with return type: int int __VERIFIER_nondet_int(void); int remap_pfn_range(struct vm_area_struct *arg0, unsigned long arg1, unsigned long arg2, unsigned long arg3, pgprot_t arg4) { // Simple type return __VERIFIER_nondet_int(); } // Function: request_dma // with type: int request_dma(unsigned int, const char *) // with return type: int int __VERIFIER_nondet_int(void); int request_dma(unsigned int arg0, const char *arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: schedule // with type: void schedule() // with return type: void void schedule() { // Void type return; } // Skip function: strcmp // Skip function: strcpy // Function: strlcpy // with type: size_t strlcpy(char *, const char *, size_t ) // with return type: size_t unsigned long __VERIFIER_nondet_ulong(void); size_t strlcpy(char *arg0, const char *arg1, size_t arg2) { // Typedef type // Real type: __kernel_size_t // Typedef type // Real type: unsigned long // Simple type return __VERIFIER_nondet_ulong(); } // Function: unregister_sound_dsp // with type: void unregister_sound_dsp(int) // with return type: void void unregister_sound_dsp(int arg0) { // Void type return; } // Function: unregister_sound_midi // with type: void unregister_sound_midi(int) // with return type: void void unregister_sound_midi(int arg0) { // Void type return; } // Function: unregister_sound_mixer // with type: void unregister_sound_mixer(int) // with return type: void void unregister_sound_mixer(int arg0) { // Void type return; } // Function: unregister_sound_special // with type: void unregister_sound_special(int) // with return type: void void unregister_sound_special(int arg0) { // Void type return; } // Function: vfree // with type: void vfree(const void *) // with return type: void void vfree(const void *arg0) { // Void type return; } // Function: vmalloc // with type: void *vmalloc(unsigned long) // with return type: (void)* void *vmalloc(unsigned long arg0) { // Pointer type return ldv_malloc(arg0); } // 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; }