// Skip function: __VERIFIER_error // Skip function: __VERIFIER_nondet_int // Skip function: __VERIFIER_nondet_ulong // Function: __alloc_workqueue_key // with type: struct workqueue_struct *__alloc_workqueue_key(const char *, unsigned int, int, struct lock_class_key *, const char *, ...) // with return type: (struct workqueue_struct)* struct workqueue_struct *__alloc_workqueue_key(const char *arg0, unsigned int arg1, int arg2, struct lock_class_key *arg3, const char *arg4, ...) { // Pointer type return ldv_malloc(0UL); } // Function: __const_udelay // with type: void __const_udelay(unsigned long) // with return type: void void __const_udelay(unsigned long arg0) { // Void type return; } // 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: __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: __kfifo_alloc // with type: int __kfifo_alloc(struct __kfifo *, unsigned int, size_t , gfp_t ) // with return type: int int __VERIFIER_nondet_int(void); int __kfifo_alloc(struct __kfifo *arg0, unsigned int arg1, size_t arg2, gfp_t arg3) { // Simple type return __VERIFIER_nondet_int(); } // Function: __kfifo_free // with type: void __kfifo_free(struct __kfifo *) // with return type: void void __kfifo_free(struct __kfifo *arg0) { // Void type return; } // Function: __kfifo_in // with type: unsigned int __kfifo_in(struct __kfifo *, const void *, unsigned int) // with return type: unsigned int unsigned int __VERIFIER_nondet_uint(void); unsigned int __kfifo_in(struct __kfifo *arg0, const void *arg1, unsigned int arg2) { // Simple type return __VERIFIER_nondet_uint(); } // Function: __kfifo_in_r // with type: unsigned int __kfifo_in_r(struct __kfifo *, const void *, unsigned int, size_t ) // with return type: unsigned int unsigned int __VERIFIER_nondet_uint(void); unsigned int __kfifo_in_r(struct __kfifo *arg0, const void *arg1, unsigned int arg2, size_t arg3) { // Simple type return __VERIFIER_nondet_uint(); } // Function: __kfifo_out // with type: unsigned int __kfifo_out(struct __kfifo *, void *, unsigned int) // with return type: unsigned int unsigned int __VERIFIER_nondet_uint(void); unsigned int __kfifo_out(struct __kfifo *arg0, void *arg1, unsigned int arg2) { // Simple type return __VERIFIER_nondet_uint(); } // Function: __kfifo_out_r // with type: unsigned int __kfifo_out_r(struct __kfifo *, void *, unsigned int, size_t ) // with return type: unsigned int unsigned int __VERIFIER_nondet_uint(void); unsigned int __kfifo_out_r(struct __kfifo *arg0, void *arg1, unsigned int arg2, size_t arg3) { // Simple type return __VERIFIER_nondet_uint(); } // Function: __mutex_init // with type: void __mutex_init(struct mutex *, const char *, struct lock_class_key *) // with return type: void void __mutex_init(struct mutex *arg0, const char *arg1, struct lock_class_key *arg2) { // 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: __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: destroy_workqueue // with type: void destroy_workqueue(struct workqueue_struct *) // with return type: void void destroy_workqueue(struct workqueue_struct *arg0) { // 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); } // 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; } // Function: flush_workqueue // with type: void flush_workqueue(struct workqueue_struct *) // with return type: void void flush_workqueue(struct workqueue_struct *arg0) { // Void type return; } // Function: i2c_del_driver // with type: void i2c_del_driver(struct i2c_driver *) // with return type: void void i2c_del_driver(struct i2c_driver *arg0) { // Void type return; } // Function: i2c_master_send // with type: int i2c_master_send(const struct i2c_client *, const char *, int) // with return type: int int __VERIFIER_nondet_int(void); int i2c_master_send(const struct i2c_client *arg0, const char *arg1, int arg2) { // Simple type return __VERIFIER_nondet_int(); } // Function: i2c_register_driver // with type: int i2c_register_driver(struct module *, struct i2c_driver *) // with return type: int int __VERIFIER_nondet_int(void); int i2c_register_driver(struct module *arg0, struct i2c_driver *arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: i2c_transfer // with type: int i2c_transfer(struct i2c_adapter *, struct i2c_msg *, int) // with return type: int int __VERIFIER_nondet_int(void); int i2c_transfer(struct i2c_adapter *arg0, struct i2c_msg *arg1, int arg2) { // Simple type return __VERIFIER_nondet_int(); } // 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_probe_4 // with type: int ldv_probe_4() // with return type: int int __VERIFIER_nondet_int(void); int ldv_probe_4() { // Simple type return __VERIFIER_nondet_int(); } // Function: ldv_release_4 // with type: int ldv_release_4() // with return type: int int __VERIFIER_nondet_int(void); int ldv_release_4() { // Simple type return __VERIFIER_nondet_int(); } // Function: ldv_some_page // with type: struct page *ldv_some_page() // with return type: (struct page)* struct page *ldv_some_page() { // Pointer type return ldv_malloc(sizeof(struct page)); } // 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 // Function: media_entity_init // with type: int media_entity_init(struct media_entity *, u16 , struct media_pad *, u16 ) // with return type: int int __VERIFIER_nondet_int(void); int media_entity_init(struct media_entity *arg0, u16 arg1, struct media_pad *arg2, u16 arg3) { // Simple type return __VERIFIER_nondet_int(); } // Skip function: memcpy // Skip function: memmove // Skip function: memset // Function: mutex_lock_nested // with type: void mutex_lock_nested(struct mutex *, unsigned int) // with return type: void void mutex_lock_nested(struct mutex *arg0, unsigned int arg1) { // Void type return; } // Function: mutex_unlock // with type: void mutex_unlock(struct mutex *) // with return type: void void mutex_unlock(struct mutex *arg0) { // Void type return; } // Function: prepare_to_wait // with type: void prepare_to_wait(wait_queue_head_t *, wait_queue_t *, int) // with return type: void void prepare_to_wait(wait_queue_head_t *arg0, wait_queue_t *arg1, int arg2) { // 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: queue_delayed_work_on // with type: bool queue_delayed_work_on(int, struct workqueue_struct *, struct delayed_work *, unsigned long) // with return type: bool bool __VERIFIER_nondet_bool(void); bool queue_delayed_work_on(int arg0, struct workqueue_struct *arg1, struct delayed_work *arg2, unsigned long arg3) { // Typedef type // Real type: _Bool // Simple type return __VERIFIER_nondet_bool(); } // 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: release_firmware // with type: void release_firmware(const struct firmware *) // with return type: void void release_firmware(const struct firmware *arg0) { // Void type return; } // Function: request_firmware // with type: int request_firmware(const struct firmware **, const char *, struct device *) // with return type: int int __VERIFIER_nondet_int(void); int request_firmware(const struct firmware **arg0, const char *arg1, struct device *arg2) { // Simple type return __VERIFIER_nondet_int(); } // Function: schedule // with type: void schedule() // with return type: void void schedule() { // Void type return; } // Function: v4l2_ctrl_cluster // with type: void v4l2_ctrl_cluster(unsigned int, struct v4l2_ctrl **) // with return type: void void v4l2_ctrl_cluster(unsigned int arg0, struct v4l2_ctrl **arg1) { // Void type return; } // Function: v4l2_ctrl_handler_free // with type: void v4l2_ctrl_handler_free(struct v4l2_ctrl_handler *) // with return type: void void v4l2_ctrl_handler_free(struct v4l2_ctrl_handler *arg0) { // Void type return; } // Function: v4l2_ctrl_handler_init_class // with type: int v4l2_ctrl_handler_init_class(struct v4l2_ctrl_handler *, unsigned int, struct lock_class_key *, const char *) // with return type: int int __VERIFIER_nondet_int(void); int v4l2_ctrl_handler_init_class(struct v4l2_ctrl_handler *arg0, unsigned int arg1, struct lock_class_key *arg2, const char *arg3) { // Simple type return __VERIFIER_nondet_int(); } // Function: v4l2_ctrl_handler_log_status // with type: void v4l2_ctrl_handler_log_status(struct v4l2_ctrl_handler *, const char *) // with return type: void void v4l2_ctrl_handler_log_status(struct v4l2_ctrl_handler *arg0, const char *arg1) { // Void type return; } // Function: v4l2_ctrl_handler_setup // with type: int v4l2_ctrl_handler_setup(struct v4l2_ctrl_handler *) // with return type: int int __VERIFIER_nondet_int(void); int v4l2_ctrl_handler_setup(struct v4l2_ctrl_handler *arg0) { // Simple type return __VERIFIER_nondet_int(); } // Function: v4l2_ctrl_new_std // with type: struct v4l2_ctrl *v4l2_ctrl_new_std(struct v4l2_ctrl_handler *, const struct v4l2_ctrl_ops *, u32 , s64 , s64 , u64 , s64 ) // with return type: (struct v4l2_ctrl)* struct v4l2_ctrl *v4l2_ctrl_new_std(struct v4l2_ctrl_handler *arg0, const struct v4l2_ctrl_ops *arg1, u32 arg2, s64 arg3, s64 arg4, u64 arg5, s64 arg6) { // Pointer type return ldv_malloc(sizeof(struct v4l2_ctrl)); } // Function: v4l2_device_unregister_subdev // with type: void v4l2_device_unregister_subdev(struct v4l2_subdev *) // with return type: void void v4l2_device_unregister_subdev(struct v4l2_subdev *arg0) { // Void type return; } // Function: v4l2_i2c_subdev_init // with type: void v4l2_i2c_subdev_init(struct v4l2_subdev *, struct i2c_client *, const struct v4l2_subdev_ops *) // with return type: void void v4l2_i2c_subdev_init(struct v4l2_subdev *arg0, struct i2c_client *arg1, const struct v4l2_subdev_ops *arg2) { // Void type return; } // Function: v4l2_subdev_g_ctrl // with type: int v4l2_subdev_g_ctrl(struct v4l2_subdev *, struct v4l2_control *) // with return type: int int __VERIFIER_nondet_int(void); int v4l2_subdev_g_ctrl(struct v4l2_subdev *arg0, struct v4l2_control *arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: v4l2_subdev_g_ext_ctrls // with type: int v4l2_subdev_g_ext_ctrls(struct v4l2_subdev *, struct v4l2_ext_controls *) // with return type: int int __VERIFIER_nondet_int(void); int v4l2_subdev_g_ext_ctrls(struct v4l2_subdev *arg0, struct v4l2_ext_controls *arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: v4l2_subdev_queryctrl // with type: int v4l2_subdev_queryctrl(struct v4l2_subdev *, struct v4l2_queryctrl *) // with return type: int int __VERIFIER_nondet_int(void); int v4l2_subdev_queryctrl(struct v4l2_subdev *arg0, struct v4l2_queryctrl *arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: v4l2_subdev_querymenu // with type: int v4l2_subdev_querymenu(struct v4l2_subdev *, struct v4l2_querymenu *) // with return type: int int __VERIFIER_nondet_int(void); int v4l2_subdev_querymenu(struct v4l2_subdev *arg0, struct v4l2_querymenu *arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: v4l2_subdev_s_ctrl // with type: int v4l2_subdev_s_ctrl(struct v4l2_subdev *, struct v4l2_control *) // with return type: int int __VERIFIER_nondet_int(void); int v4l2_subdev_s_ctrl(struct v4l2_subdev *arg0, struct v4l2_control *arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: v4l2_subdev_s_ext_ctrls // with type: int v4l2_subdev_s_ext_ctrls(struct v4l2_subdev *, struct v4l2_ext_controls *) // with return type: int int __VERIFIER_nondet_int(void); int v4l2_subdev_s_ext_ctrls(struct v4l2_subdev *arg0, struct v4l2_ext_controls *arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: v4l2_subdev_try_ext_ctrls // with type: int v4l2_subdev_try_ext_ctrls(struct v4l2_subdev *, struct v4l2_ext_controls *) // with return type: int int __VERIFIER_nondet_int(void); int v4l2_subdev_try_ext_ctrls(struct v4l2_subdev *arg0, struct v4l2_ext_controls *arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: autoremove_wake_function // with type: int autoremove_wake_function(wait_queue_t *, unsigned int, int, void *) // with return type: int int __VERIFIER_nondet_int(void); int autoremove_wake_function(wait_queue_t *arg0, unsigned int arg1, int arg2, void * arg3) { // Simple type return __VERIFIER_nondet_int(); }