// Skip function: __VERIFIER_error

// Skip function: __VERIFIER_nondet_int

// Skip function: __VERIFIER_nondet_ulong

// Function: ___might_sleep
// with type: void ___might_sleep(const char *, int, int)
// with return type: void
void ___might_sleep(const char *arg0, int arg1, int arg2) {
  // Void type
  return;
}

// 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: __bitmap_or
// with type: void __bitmap_or(unsigned long *, const unsigned long *, const unsigned long *, unsigned int)
// with return type: void
void __bitmap_or(unsigned long *arg0, const unsigned long *arg1, const unsigned long *arg2, unsigned int arg3) {
  // Void type
  return;
}

// Skip function: __builtin_alloca

// Skip function: __builtin_va_copy

// Function: __compiletime_assert_1008
// with type: void __compiletime_assert_1008()
// with return type: void
void __compiletime_assert_1008() {
  // Void type
  return;
}

// Function: __compiletime_assert_1077
// with type: void __compiletime_assert_1077()
// with return type: void
void __compiletime_assert_1077() {
  // Void type
  return;
}

// Function: __compiletime_assert_1079
// with type: void __compiletime_assert_1079()
// with return type: void
void __compiletime_assert_1079() {
  // Void type
  return;
}

// Function: __compiletime_assert_1096
// with type: void __compiletime_assert_1096()
// with return type: void
void __compiletime_assert_1096() {
  // Void type
  return;
}

// Function: __compiletime_assert_1132
// with type: void __compiletime_assert_1132()
// with return type: void
void __compiletime_assert_1132() {
  // Void type
  return;
}

// Function: __compiletime_assert_2298
// with type: void __compiletime_assert_2298()
// with return type: void
void __compiletime_assert_2298() {
  // Void type
  return;
}

// Function: __compiletime_assert_347
// with type: void __compiletime_assert_347()
// with return type: void
void __compiletime_assert_347() {
  // Void type
  return;
}

// Function: __compiletime_assert_351
// with type: void __compiletime_assert_351()
// with return type: void
void __compiletime_assert_351() {
  // Void type
  return;
}

// Function: __compiletime_assert_557
// with type: void __compiletime_assert_557()
// with return type: void
void __compiletime_assert_557() {
  // Void type
  return;
}

// Function: __compiletime_assert_563
// with type: void __compiletime_assert_563()
// with return type: void
void __compiletime_assert_563() {
  // Void type
  return;
}

// Function: __compiletime_assert_5980
// with type: void __compiletime_assert_5980()
// with return type: void
void __compiletime_assert_5980() {
  // Void type
  return;
}

// Function: __compiletime_assert_6051
// with type: void __compiletime_assert_6051()
// with return type: void
void __compiletime_assert_6051() {
  // Void type
  return;
}

// Function: __compiletime_assert_6062
// with type: void __compiletime_assert_6062()
// with return type: void
void __compiletime_assert_6062() {
  // Void type
  return;
}

// Function: __compiletime_assert_6067
// with type: void __compiletime_assert_6067()
// with return type: void
void __compiletime_assert_6067() {
  // Void type
  return;
}

// Function: __compiletime_assert_6256
// with type: void __compiletime_assert_6256()
// with return type: void
void __compiletime_assert_6256() {
  // Void type
  return;
}

// Function: __compiletime_assert_6260
// with type: void __compiletime_assert_6260()
// with return type: void
void __compiletime_assert_6260() {
  // Void type
  return;
}

// Function: __compiletime_assert_6275
// with type: void __compiletime_assert_6275()
// with return type: void
void __compiletime_assert_6275() {
  // Void type
  return;
}

// Function: __compiletime_assert_6315
// with type: void __compiletime_assert_6315()
// with return type: void
void __compiletime_assert_6315() {
  // Void type
  return;
}

// Function: __compiletime_assert_6376
// with type: void __compiletime_assert_6376()
// with return type: void
void __compiletime_assert_6376() {
  // Void type
  return;
}

// Function: __compiletime_assert_6422
// with type: void __compiletime_assert_6422()
// with return type: void
void __compiletime_assert_6422() {
  // Void type
  return;
}

// Function: __compiletime_assert_6468
// with type: void __compiletime_assert_6468()
// with return type: void
void __compiletime_assert_6468() {
  // Void type
  return;
}

// Function: __compiletime_assert_6537
// with type: void __compiletime_assert_6537()
// with return type: void
void __compiletime_assert_6537() {
  // Void type
  return;
}

// Function: __compiletime_assert_6555
// with type: void __compiletime_assert_6555()
// with return type: void
void __compiletime_assert_6555() {
  // Void type
  return;
}

// Function: __compiletime_assert_6572
// with type: void __compiletime_assert_6572()
// with return type: void
void __compiletime_assert_6572() {
  // Void type
  return;
}

// Function: __compiletime_assert_6588
// with type: void __compiletime_assert_6588()
// with return type: void
void __compiletime_assert_6588() {
  // Void type
  return;
}

// Function: __compiletime_assert_6608
// with type: void __compiletime_assert_6608()
// with return type: void
void __compiletime_assert_6608() {
  // Void type
  return;
}

// Function: __compiletime_assert_838
// with type: void __compiletime_assert_838()
// with return type: void
void __compiletime_assert_838() {
  // Void type
  return;
}

// Function: __compiletime_assert_854
// with type: void __compiletime_assert_854()
// with return type: void
void __compiletime_assert_854() {
  // Void type
  return;
}

// Function: __compiletime_assert_883
// with type: void __compiletime_assert_883()
// with return type: void
void __compiletime_assert_883() {
  // Void type
  return;
}

// Function: __compiletime_assert_902
// with type: void __compiletime_assert_902()
// with return type: void
void __compiletime_assert_902() {
  // Void type
  return;
}

// Function: __compiletime_assert_926
// with type: void __compiletime_assert_926()
// with return type: void
void __compiletime_assert_926() {
  // Void type
  return;
}

// Function: __compiletime_assert_953
// with type: void __compiletime_assert_953()
// with return type: void
void __compiletime_assert_953() {
  // Void type
  return;
}

// Function: __compiletime_assert_978
// with type: void __compiletime_assert_978()
// with return type: void
void __compiletime_assert_978() {
  // Void type
  return;
}

// Function: __const_udelay
// with type: void __const_udelay(unsigned long)
// with return type: void
void __const_udelay(unsigned long arg0) {
  // Void type
  return;
}

// Function: __copy_from_user_overflow
// with type: void __copy_from_user_overflow()
// with return type: void
void __copy_from_user_overflow() {
  // Void type
  return;
}

// Function: __copy_to_user_overflow
// with type: void __copy_to_user_overflow()
// with return type: void
void __copy_to_user_overflow() {
  // Void type
  return;
}

// Function: __copy_user_nocache
// with type: long int __copy_user_nocache(void *, const void *, unsigned int, int)
// with return type: long int
long __VERIFIER_nondet_long(void);
long int __copy_user_nocache(void *arg0, const void *arg1, unsigned int arg2, int arg3) {
  // Simple type
  return __VERIFIER_nondet_long();
}

// Function: __devm_request_region
// with type: struct resource *__devm_request_region(struct device *, struct resource *, resource_size_t , resource_size_t , const char *)
// with return type: (struct resource)*
struct resource *__devm_request_region(struct device *arg0, struct resource *arg1, resource_size_t arg2, resource_size_t arg3, const char *arg4) {
  // Pointer type
  return ldv_malloc(sizeof(struct resource));
}

// Function: __drm_atomic_helper_crtc_duplicate_state
// with type: void __drm_atomic_helper_crtc_duplicate_state(struct drm_crtc *, struct drm_crtc_state *)
// with return type: void
void __drm_atomic_helper_crtc_duplicate_state(struct drm_crtc *arg0, struct drm_crtc_state *arg1) {
  // Void type
  return;
}

// Function: __drm_atomic_helper_plane_duplicate_state
// with type: void __drm_atomic_helper_plane_duplicate_state(struct drm_plane *, struct drm_plane_state *)
// with return type: void
void __drm_atomic_helper_plane_duplicate_state(struct drm_plane *arg0, struct drm_plane_state *arg1) {
  // Void type
  return;
}

// Function: __dynamic_dev_dbg
// with type: void __dynamic_dev_dbg(struct _ddebug *, const struct device *, const char *, ...)
// with return type: void
void __dynamic_dev_dbg(struct _ddebug *arg0, const struct device *arg1, const char *arg2, ...) {
  // Void type
  return;
}

// Function: __free_pages
// with type: void __free_pages(struct page *, unsigned int)
// with return type: void
void __free_pages(struct page *arg0, unsigned int arg1) {
  // Void type
  return;
}

// Function: __get_user_pages_fast
// with type: int __get_user_pages_fast(unsigned long, int, int, struct page **)
// with return type: int
int __VERIFIER_nondet_int(void);
int __get_user_pages_fast(unsigned long arg0, int arg1, int arg2, struct page **arg3) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// 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: __kmalloc
// with type: void *__kmalloc(size_t , gfp_t )
// with return type: (void)*
void *__kmalloc(size_t arg0, gfp_t arg1) {
  // Pointer type
  return ldv_malloc(arg0);
}

// Function: __list_add
// with type: void __list_add(struct list_head *, struct list_head *, struct list_head *)
// with return type: void
void __list_add(struct list_head *arg0, struct list_head *arg1, struct list_head *arg2) {
  // Void type
  return;
}

// Function: __list_del_entry
// with type: void __list_del_entry(struct list_head *)
// with return type: void
void __list_del_entry(struct list_head *arg0) {
  // Void type
  return;
}

// Function: __might_fault
// with type: void __might_fault(const char *, int)
// with return type: void
void __might_fault(const char *arg0, int arg1) {
  // Void type
  return;
}

// Function: __might_sleep
// with type: void __might_sleep(const char *, int, int)
// with return type: void
void __might_sleep(const char *arg0, int arg1, int arg2) {
  // Void type
  return;
}

// Function: __mmdrop
// with type: void __mmdrop(struct mm_struct *)
// with return type: void
void __mmdrop(struct mm_struct *arg0) {
  // Void type
  return;
}

// Function: __mmu_notifier_register
// with type: int __mmu_notifier_register(struct mmu_notifier *, struct mm_struct *)
// with return type: int
int __VERIFIER_nondet_int(void);
int __mmu_notifier_register(struct mmu_notifier *arg0, struct mm_struct *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: __msecs_to_jiffies
// with type: unsigned long int __msecs_to_jiffies(const unsigned int)
// with return type: unsigned long int
unsigned long __VERIFIER_nondet_ulong(void);
unsigned long int __msecs_to_jiffies(const unsigned int arg0) {
  // Simple type
  return __VERIFIER_nondet_ulong();
}

// 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: __pm_runtime_disable
// with type: void __pm_runtime_disable(struct device *, bool )
// with return type: void
void __pm_runtime_disable(struct device *arg0, bool arg1) {
  // Void type
  return;
}

// Function: __pm_runtime_resume
// with type: int __pm_runtime_resume(struct device *, int)
// with return type: int
int __VERIFIER_nondet_int(void);
int __pm_runtime_resume(struct device *arg0, int arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: __pm_runtime_set_status
// with type: int __pm_runtime_set_status(struct device *, unsigned int)
// with return type: int
int __VERIFIER_nondet_int(void);
int __pm_runtime_set_status(struct device *arg0, unsigned int arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: __pm_runtime_suspend
// with type: int __pm_runtime_suspend(struct device *, int)
// with return type: int
int __VERIFIER_nondet_int(void);
int __pm_runtime_suspend(struct device *arg0, int arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: __pm_runtime_use_autosuspend
// with type: void __pm_runtime_use_autosuspend(struct device *, bool )
// with return type: void
void __pm_runtime_use_autosuspend(struct device *arg0, bool arg1) {
  // Void type
  return;
}

// Function: __put_task_struct
// with type: void __put_task_struct(struct task_struct *)
// with return type: void
void __put_task_struct(struct task_struct *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: __sg_page_iter_next
// with type: bool __sg_page_iter_next(struct sg_page_iter *)
// with return type: bool 
bool __VERIFIER_nondet_bool(void);
bool __sg_page_iter_next(struct sg_page_iter *arg0) {
  // Typedef type
  // Real type: _Bool
  // Simple type
  return __VERIFIER_nondet_bool();
}

// Function: __sg_page_iter_start
// with type: void __sg_page_iter_start(struct sg_page_iter *, struct scatterlist *, unsigned int, unsigned long)
// with return type: void
void __sg_page_iter_start(struct sg_page_iter *arg0, struct scatterlist *arg1, unsigned int arg2, unsigned long arg3) {
  // Void type
  return;
}

// Function: __symbol_get
// with type: void *__symbol_get(const char *)
// with return type: (void)*
void *__symbol_get(const char *arg0) {
  // Pointer type
  return ldv_malloc(0UL);
}

// Function: __symbol_put
// with type: void __symbol_put(const char *)
// with return type: void
void __symbol_put(const char *arg0) {
  // Void type
  return;
}

// Function: __usecs_to_jiffies
// with type: unsigned long int __usecs_to_jiffies(const unsigned int)
// with return type: unsigned long int
unsigned long __VERIFIER_nondet_ulong(void);
unsigned long int __usecs_to_jiffies(const unsigned int arg0) {
  // Simple type
  return __VERIFIER_nondet_ulong();
}

// Function: __vmalloc
// with type: void *__vmalloc(unsigned long, gfp_t , pgprot_t )
// with return type: (void)*
void *__vmalloc(unsigned long arg0, gfp_t arg1, pgprot_t arg2) {
  // Pointer type
  return ldv_malloc(0UL);
}

// 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: _cond_resched
// with type: int _cond_resched()
// with return type: int
int __VERIFIER_nondet_int(void);
int _cond_resched() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// 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: _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: acpi_bus_get_device
// with type: int acpi_bus_get_device(acpi_handle , struct acpi_device **)
// with return type: int
int __VERIFIER_nondet_int(void);
int acpi_bus_get_device(acpi_handle arg0, struct acpi_device **arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: acpi_check_dsm
// with type: bool acpi_check_dsm(acpi_handle , const u8 *, int, u64 )
// with return type: bool 
bool __VERIFIER_nondet_bool(void);
bool acpi_check_dsm(acpi_handle arg0, const u8 *arg1, int arg2, u64 arg3) {
  // Typedef type
  // Real type: _Bool
  // Simple type
  return __VERIFIER_nondet_bool();
}

// Function: acpi_evaluate_dsm
// with type: union acpi_object *acpi_evaluate_dsm(acpi_handle , const u8 *, int, int, union acpi_object *)
// with return type: (union acpi_object)*
union acpi_object *acpi_evaluate_dsm(acpi_handle arg0, const u8 *arg1, int arg2, int arg3, union acpi_object *arg4) {
  // Pointer type
  return ldv_malloc(sizeof(union acpi_object));
}

// Function: acpi_evaluate_integer
// with type: acpi_status acpi_evaluate_integer(acpi_handle , acpi_string , struct acpi_object_list *, unsigned long long *)
// with return type: acpi_status 
unsigned int __VERIFIER_nondet_uint(void);
acpi_status acpi_evaluate_integer(acpi_handle arg0, acpi_string arg1, struct acpi_object_list *arg2, unsigned long long *arg3) {
  // Typedef type
  // Real type: u32 
  // Typedef type
  // Real type: unsigned int
  // Simple type
  return __VERIFIER_nondet_uint();
}

// Function: acpi_get_name
// with type: acpi_status acpi_get_name(acpi_handle , u32 , struct acpi_buffer *)
// with return type: acpi_status 
unsigned int __VERIFIER_nondet_uint(void);
acpi_status acpi_get_name(acpi_handle arg0, u32 arg1, struct acpi_buffer *arg2) {
  // Typedef type
  // Real type: u32 
  // Typedef type
  // Real type: unsigned int
  // Simple type
  return __VERIFIER_nondet_uint();
}

// Function: acpi_is_video_device
// with type: long int acpi_is_video_device(acpi_handle )
// with return type: long int
long __VERIFIER_nondet_long(void);
long int acpi_is_video_device(acpi_handle arg0) {
  // Simple type
  return __VERIFIER_nondet_long();
}

// Function: acpi_lid_notifier_register
// with type: int acpi_lid_notifier_register(struct notifier_block *)
// with return type: int
int __VERIFIER_nondet_int(void);
int acpi_lid_notifier_register(struct notifier_block *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: acpi_lid_notifier_unregister
// with type: int acpi_lid_notifier_unregister(struct notifier_block *)
// with return type: int
int __VERIFIER_nondet_int(void);
int acpi_lid_notifier_unregister(struct notifier_block *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: acpi_lid_open
// with type: int acpi_lid_open()
// with return type: int
int __VERIFIER_nondet_int(void);
int acpi_lid_open() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: acpi_target_system_state
// with type: u32 acpi_target_system_state()
// with return type: u32 
unsigned int __VERIFIER_nondet_uint(void);
u32 acpi_target_system_state() {
  // Typedef type
  // Real type: unsigned int
  // Simple type
  return __VERIFIER_nondet_uint();
}

// Function: acpi_video_get_backlight_type
// with type: enum acpi_backlight_type acpi_video_get_backlight_type()
// with return type: enum acpi_backlight_type
int __VERIFIER_nondet_int(void);
enum acpi_backlight_type acpi_video_get_backlight_type() {
  // Enum type
  return __VERIFIER_nondet_int();
}

// Function: acpi_video_register
// with type: int acpi_video_register()
// with return type: int
int __VERIFIER_nondet_int(void);
int acpi_video_register() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: acpi_video_unregister
// with type: void acpi_video_unregister()
// with return type: void
void acpi_video_unregister() {
  // Void type
  return;
}

// Function: alloc_pages_current
// with type: struct page *alloc_pages_current(gfp_t , unsigned int)
// with return type: (struct page)*
struct page *alloc_pages_current(gfp_t arg0, unsigned int arg1) {
  // Pointer type
  return ldv_malloc(sizeof(struct page));
}

// Function: arch_phys_wc_add
// with type: int arch_phys_wc_add(unsigned long, unsigned long)
// with return type: int
int __VERIFIER_nondet_int(void);
int arch_phys_wc_add(unsigned long arg0, unsigned long arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: arch_phys_wc_del
// with type: void arch_phys_wc_del(int)
// with return type: void
void arch_phys_wc_del(int arg0) {
  // Void type
  return;
}

// Function: async_schedule
// with type: async_cookie_t async_schedule(void (*)(void *, async_cookie_t ), void *)
// with return type: async_cookie_t 
unsigned long __VERIFIER_nondet_ulong(void);
async_cookie_t async_schedule(void (*arg0)(void *, async_cookie_t ), void *arg1) {
  // Typedef type
  // Real type: u64 
  // Typedef type
  // Real type: unsigned long long
  // Simple type
  return __VERIFIER_nondet_ulong();
}

// Function: async_synchronize_full
// with type: void async_synchronize_full()
// with return type: void
void async_synchronize_full() {
  // Void type
  return;
}

// Function: backlight_device_register
// with type: struct backlight_device *backlight_device_register(const char *, struct device *, void *, const struct backlight_ops *, const struct backlight_properties *)
// with return type: (struct backlight_device)*
struct backlight_device *backlight_device_register(const char *arg0, struct device *arg1, void *arg2, const struct backlight_ops *arg3, const struct backlight_properties *arg4) {
  // Pointer type
  return ldv_malloc(sizeof(struct backlight_device));
}

// Function: backlight_device_unregister
// with type: void backlight_device_unregister(struct backlight_device *)
// with return type: void
void backlight_device_unregister(struct backlight_device *arg0) {
  // Void type
  return;
}

// Function: bitmap_set
// with type: void bitmap_set(unsigned long *, unsigned int, int)
// with return type: void
void bitmap_set(unsigned long *arg0, unsigned int arg1, int arg2) {
  // Void type
  return;
}

// Skip function: calloc

// Function: cancel_delayed_work
// with type: bool cancel_delayed_work(struct delayed_work *)
// with return type: bool 
bool __VERIFIER_nondet_bool(void);
bool cancel_delayed_work(struct delayed_work *arg0) {
  // Typedef type
  // Real type: _Bool
  // Simple type
  return __VERIFIER_nondet_bool();
}

// Function: cancel_delayed_work_sync
// with type: bool cancel_delayed_work_sync(struct delayed_work *)
// with return type: bool 
bool __VERIFIER_nondet_bool(void);
bool cancel_delayed_work_sync(struct delayed_work *arg0) {
  // Typedef type
  // Real type: _Bool
  // Simple type
  return __VERIFIER_nondet_bool();
}

// Function: cancel_work_sync
// with type: bool cancel_work_sync(struct work_struct *)
// with return type: bool 
bool __VERIFIER_nondet_bool(void);
bool cancel_work_sync(struct work_struct *arg0) {
  // Typedef type
  // Real type: _Bool
  // Simple type
  return __VERIFIER_nondet_bool();
}

// Function: capable
// with type: bool capable(int)
// with return type: bool 
bool __VERIFIER_nondet_bool(void);
bool capable(int arg0) {
  // Typedef type
  // Real type: _Bool
  // Simple type
  return __VERIFIER_nondet_bool();
}

// Function: cfb_copyarea
// with type: void cfb_copyarea(struct fb_info *, const struct fb_copyarea *)
// with return type: void
void cfb_copyarea(struct fb_info *arg0, const struct fb_copyarea *arg1) {
  // Void type
  return;
}

// Function: cfb_fillrect
// with type: void cfb_fillrect(struct fb_info *, const struct fb_fillrect *)
// with return type: void
void cfb_fillrect(struct fb_info *arg0, const struct fb_fillrect *arg1) {
  // Void type
  return;
}

// Function: cfb_imageblit
// with type: void cfb_imageblit(struct fb_info *, const struct fb_image *)
// with return type: void
void cfb_imageblit(struct fb_info *arg0, const struct fb_image *arg1) {
  // Void type
  return;
}

// Function: compat_alloc_user_space
// with type: void *compat_alloc_user_space(unsigned long)
// with return type: (void)*
void *compat_alloc_user_space(unsigned long arg0) {
  // Pointer type
  return ldv_malloc(0UL);
}

// Function: component_add
// with type: int component_add(struct device *, const struct component_ops *)
// with return type: int
int __VERIFIER_nondet_int(void);
int component_add(struct device *arg0, const struct component_ops *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: component_del
// with type: void component_del(struct device *, const struct component_ops *)
// with return type: void
void component_del(struct device *arg0, const struct component_ops *arg1) {
  // Void type
  return;
}

// Function: con_is_bound
// with type: int con_is_bound(const struct consw *)
// with return type: int
int __VERIFIER_nondet_int(void);
int con_is_bound(const struct consw *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: console_lock
// with type: void console_lock()
// with return type: void
void console_lock() {
  // Void type
  return;
}

// Function: console_trylock
// with type: int console_trylock()
// with return type: int
int __VERIFIER_nondet_int(void);
int console_trylock() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: console_unlock
// with type: void console_unlock()
// with return type: void
void console_unlock() {
  // Void type
  return;
}

// Function: cpufreq_cpu_get
// with type: struct cpufreq_policy *cpufreq_cpu_get(unsigned int)
// with return type: (struct cpufreq_policy)*
struct cpufreq_policy *cpufreq_cpu_get(unsigned int arg0) {
  // Pointer type
  return ldv_malloc(sizeof(struct cpufreq_policy));
}

// Function: cpufreq_cpu_put
// with type: void cpufreq_cpu_put(struct cpufreq_policy *)
// with return type: void
void cpufreq_cpu_put(struct cpufreq_policy *arg0) {
  // Void type
  return;
}

// Function: debug_dma_map_page
// with type: void debug_dma_map_page(struct device *, struct page *, size_t , size_t , int, dma_addr_t , bool )
// with return type: void
void debug_dma_map_page(struct device *arg0, struct page *arg1, size_t arg2, size_t arg3, int arg4, dma_addr_t arg5, bool arg6) {
  // Void type
  return;
}

// Function: debug_dma_map_sg
// with type: void debug_dma_map_sg(struct device *, struct scatterlist *, int, int, int)
// with return type: void
void debug_dma_map_sg(struct device *arg0, struct scatterlist *arg1, int arg2, int arg3, int arg4) {
  // Void type
  return;
}

// Function: debug_dma_mapping_error
// with type: void debug_dma_mapping_error(struct device *, dma_addr_t )
// with return type: void
void debug_dma_mapping_error(struct device *arg0, dma_addr_t arg1) {
  // Void type
  return;
}

// Function: debug_dma_unmap_page
// with type: void debug_dma_unmap_page(struct device *, dma_addr_t , size_t , int, bool )
// with return type: void
void debug_dma_unmap_page(struct device *arg0, dma_addr_t arg1, size_t arg2, int arg3, bool arg4) {
  // Void type
  return;
}

// Function: debug_dma_unmap_sg
// with type: void debug_dma_unmap_sg(struct device *, struct scatterlist *, int, int)
// with return type: void
void debug_dma_unmap_sg(struct device *arg0, struct scatterlist *arg1, int arg2, int arg3) {
  // 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: debugfs_create_file
// with type: struct dentry *debugfs_create_file(const char *, umode_t , struct dentry *, void *, const struct file_operations *)
// with return type: (struct dentry)*
struct dentry *debugfs_create_file(const char *arg0, umode_t arg1, struct dentry *arg2, void *arg3, const struct file_operations *arg4) {
  // Pointer type
  return ldv_malloc(sizeof(struct dentry));
}

// Function: debugfs_remove
// with type: void debugfs_remove(struct dentry *)
// with return type: void
void debugfs_remove(struct dentry *arg0) {
  // Void type
  return;
}

// Function: default_llseek
// with type: loff_t default_llseek(struct file *, loff_t , int)
// with return type: loff_t 
long __VERIFIER_nondet_long(void);
loff_t default_llseek(struct file *arg0, loff_t arg1, int arg2) {
  // Typedef type
  // Real type: __kernel_loff_t 
  // Typedef type
  // Real type: long long
  // Simple type
  return __VERIFIER_nondet_long();
}

// 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();
}

// Function: destroy_timer_on_stack
// with type: void destroy_timer_on_stack(struct timer_list *)
// with return type: void
void destroy_timer_on_stack(struct timer_list *arg0) {
  // Void type
  return;
}

// 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: dev_err
// with type: void dev_err(const struct device *, const char *, ...)
// with return type: void
void dev_err(const struct device *arg0, const char *arg1, ...) {
  // Void type
  return;
}

// Function: device_create_bin_file
// with type: int device_create_bin_file(struct device *, const struct bin_attribute *)
// with return type: int
int __VERIFIER_nondet_int(void);
int device_create_bin_file(struct device *arg0, const struct bin_attribute *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: device_remove_bin_file
// with type: void device_remove_bin_file(struct device *, const struct bin_attribute *)
// with return type: void
void device_remove_bin_file(struct device *arg0, const struct bin_attribute *arg1) {
  // 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: dma_buf_attach
// with type: struct dma_buf_attachment *dma_buf_attach(struct dma_buf *, struct device *)
// with return type: (struct dma_buf_attachment)*
struct dma_buf_attachment *dma_buf_attach(struct dma_buf *arg0, struct device *arg1) {
  // Pointer type
  return ldv_malloc(sizeof(struct dma_buf_attachment));
}

// Function: dma_buf_detach
// with type: void dma_buf_detach(struct dma_buf *, struct dma_buf_attachment *)
// with return type: void
void dma_buf_detach(struct dma_buf *arg0, struct dma_buf_attachment *arg1) {
  // Void type
  return;
}

// Function: dma_buf_export
// with type: struct dma_buf *dma_buf_export(const struct dma_buf_export_info *)
// with return type: (struct dma_buf)*
struct dma_buf *dma_buf_export(const struct dma_buf_export_info *arg0) {
  // Pointer type
  return ldv_malloc(sizeof(struct dma_buf));
}

// Function: dma_buf_map_attachment
// with type: struct sg_table *dma_buf_map_attachment(struct dma_buf_attachment *, enum dma_data_direction )
// with return type: (struct sg_table)*
struct sg_table *dma_buf_map_attachment(struct dma_buf_attachment *arg0, enum dma_data_direction arg1) {
  // Pointer type
  return ldv_malloc(sizeof(struct sg_table));
}

// Function: dma_buf_put
// with type: void dma_buf_put(struct dma_buf *)
// with return type: void
void dma_buf_put(struct dma_buf *arg0) {
  // Void type
  return;
}

// Function: dma_buf_unmap_attachment
// with type: void dma_buf_unmap_attachment(struct dma_buf_attachment *, struct sg_table *, enum dma_data_direction )
// with return type: void
void dma_buf_unmap_attachment(struct dma_buf_attachment *arg0, struct sg_table *arg1, enum dma_data_direction arg2) {
  // Void type
  return;
}

// Function: dma_set_mask
// with type: int dma_set_mask(struct device *, u64 )
// with return type: int
int __VERIFIER_nondet_int(void);
int dma_set_mask(struct device *arg0, u64 arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: dma_supported
// with type: int dma_supported(struct device *, u64 )
// with return type: int
int __VERIFIER_nondet_int(void);
int dma_supported(struct device *arg0, u64 arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: dmi_check_system
// with type: int dmi_check_system(const struct dmi_system_id *)
// with return type: int
int __VERIFIER_nondet_int(void);
int dmi_check_system(const struct dmi_system_id *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: do_gettimeofday
// with type: void do_gettimeofday(struct timeval *)
// with return type: void
void do_gettimeofday(struct timeval *arg0) {
  // Void type
  return;
}

// Function: do_take_over_console
// with type: int do_take_over_console(const struct consw *, int, int, int)
// with return type: int
int __VERIFIER_nondet_int(void);
int do_take_over_console(const struct consw *arg0, int arg1, int arg2, int arg3) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: do_unregister_con_driver
// with type: int do_unregister_con_driver(const struct consw *)
// with return type: int
int __VERIFIER_nondet_int(void);
int do_unregister_con_driver(const struct consw *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: down_read
// with type: void down_read(struct rw_semaphore *)
// with return type: void
void down_read(struct rw_semaphore *arg0) {
  // Void type
  return;
}

// Function: down_write
// with type: void down_write(struct rw_semaphore *)
// with return type: void
void down_write(struct rw_semaphore *arg0) {
  // Void type
  return;
}

// Function: drm_add_edid_modes
// with type: int drm_add_edid_modes(struct drm_connector *, struct edid *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_add_edid_modes(struct drm_connector *arg0, struct edid *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_atomic_add_affected_connectors
// with type: int drm_atomic_add_affected_connectors(struct drm_atomic_state *, struct drm_crtc *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_atomic_add_affected_connectors(struct drm_atomic_state *arg0, struct drm_crtc *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_atomic_connectors_for_crtc
// with type: int drm_atomic_connectors_for_crtc(struct drm_atomic_state *, struct drm_crtc *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_atomic_connectors_for_crtc(struct drm_atomic_state *arg0, struct drm_crtc *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_atomic_get_connector_state
// with type: struct drm_connector_state *drm_atomic_get_connector_state(struct drm_atomic_state *, struct drm_connector *)
// with return type: (struct drm_connector_state)*
struct drm_connector_state *drm_atomic_get_connector_state(struct drm_atomic_state *arg0, struct drm_connector *arg1) {
  // Pointer type
  return ldv_malloc(sizeof(struct drm_connector_state));
}

// Function: drm_atomic_get_crtc_state
// with type: struct drm_crtc_state *drm_atomic_get_crtc_state(struct drm_atomic_state *, struct drm_crtc *)
// with return type: (struct drm_crtc_state)*
struct drm_crtc_state *drm_atomic_get_crtc_state(struct drm_atomic_state *arg0, struct drm_crtc *arg1) {
  // Pointer type
  return ldv_malloc(sizeof(struct drm_crtc_state));
}

// Function: drm_atomic_get_plane_state
// with type: struct drm_plane_state *drm_atomic_get_plane_state(struct drm_atomic_state *, struct drm_plane *)
// with return type: (struct drm_plane_state)*
struct drm_plane_state *drm_atomic_get_plane_state(struct drm_atomic_state *arg0, struct drm_plane *arg1) {
  // Pointer type
  return ldv_malloc(sizeof(struct drm_plane_state));
}

// Function: drm_atomic_helper_check_modeset
// with type: int drm_atomic_helper_check_modeset(struct drm_device *, struct drm_atomic_state *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_atomic_helper_check_modeset(struct drm_device *arg0, struct drm_atomic_state *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_atomic_helper_check_planes
// with type: int drm_atomic_helper_check_planes(struct drm_device *, struct drm_atomic_state *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_atomic_helper_check_planes(struct drm_device *arg0, struct drm_atomic_state *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_atomic_helper_cleanup_planes
// with type: void drm_atomic_helper_cleanup_planes(struct drm_device *, struct drm_atomic_state *)
// with return type: void
void drm_atomic_helper_cleanup_planes(struct drm_device *arg0, struct drm_atomic_state *arg1) {
  // Void type
  return;
}

// Function: drm_atomic_helper_commit_planes
// with type: void drm_atomic_helper_commit_planes(struct drm_device *, struct drm_atomic_state *)
// with return type: void
void drm_atomic_helper_commit_planes(struct drm_device *arg0, struct drm_atomic_state *arg1) {
  // Void type
  return;
}

// Function: drm_atomic_helper_connector_destroy_state
// with type: void drm_atomic_helper_connector_destroy_state(struct drm_connector *, struct drm_connector_state *)
// with return type: void
void drm_atomic_helper_connector_destroy_state(struct drm_connector *arg0, struct drm_connector_state *arg1) {
  // Void type
  return;
}

// Function: drm_atomic_helper_connector_duplicate_state
// with type: struct drm_connector_state *drm_atomic_helper_connector_duplicate_state(struct drm_connector *)
// with return type: (struct drm_connector_state)*
struct drm_connector_state *drm_atomic_helper_connector_duplicate_state(struct drm_connector *arg0) {
  // Pointer type
  return ldv_malloc(sizeof(struct drm_connector_state));
}

// Function: drm_atomic_helper_crtc_destroy_state
// with type: void drm_atomic_helper_crtc_destroy_state(struct drm_crtc *, struct drm_crtc_state *)
// with return type: void
void drm_atomic_helper_crtc_destroy_state(struct drm_crtc *arg0, struct drm_crtc_state *arg1) {
  // Void type
  return;
}

// Function: drm_atomic_helper_disable_plane
// with type: int drm_atomic_helper_disable_plane(struct drm_plane *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_atomic_helper_disable_plane(struct drm_plane *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_atomic_helper_plane_destroy_state
// with type: void drm_atomic_helper_plane_destroy_state(struct drm_plane *, struct drm_plane_state *)
// with return type: void
void drm_atomic_helper_plane_destroy_state(struct drm_plane *arg0, struct drm_plane_state *arg1) {
  // Void type
  return;
}

// Function: drm_atomic_helper_plane_set_property
// with type: int drm_atomic_helper_plane_set_property(struct drm_plane *, struct drm_property *, uint64_t )
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_atomic_helper_plane_set_property(struct drm_plane *arg0, struct drm_property *arg1, uint64_t arg2) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_atomic_helper_prepare_planes
// with type: int drm_atomic_helper_prepare_planes(struct drm_device *, struct drm_atomic_state *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_atomic_helper_prepare_planes(struct drm_device *arg0, struct drm_atomic_state *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_atomic_helper_swap_state
// with type: void drm_atomic_helper_swap_state(struct drm_device *, struct drm_atomic_state *)
// with return type: void
void drm_atomic_helper_swap_state(struct drm_device *arg0, struct drm_atomic_state *arg1) {
  // Void type
  return;
}

// Function: drm_atomic_helper_update_plane
// with type: int drm_atomic_helper_update_plane(struct drm_plane *, struct drm_crtc *, struct drm_framebuffer *, int, int, unsigned int, unsigned int, uint32_t , uint32_t , uint32_t , uint32_t )
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_atomic_helper_update_plane(struct drm_plane *arg0, struct drm_crtc *arg1, struct drm_framebuffer *arg2, int arg3, int arg4, unsigned int arg5, unsigned int arg6, uint32_t arg7, uint32_t arg8, uint32_t arg9, uint32_t arg10) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_atomic_helper_wait_for_vblanks
// with type: void drm_atomic_helper_wait_for_vblanks(struct drm_device *, struct drm_atomic_state *)
// with return type: void
void drm_atomic_helper_wait_for_vblanks(struct drm_device *arg0, struct drm_atomic_state *arg1) {
  // Void type
  return;
}

// Function: drm_atomic_set_crtc_for_connector
// with type: int drm_atomic_set_crtc_for_connector(struct drm_connector_state *, struct drm_crtc *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_atomic_set_crtc_for_connector(struct drm_connector_state *arg0, struct drm_crtc *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_atomic_set_crtc_for_plane
// with type: int drm_atomic_set_crtc_for_plane(struct drm_plane_state *, struct drm_crtc *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_atomic_set_crtc_for_plane(struct drm_plane_state *arg0, struct drm_crtc *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_atomic_set_fb_for_plane
// with type: void drm_atomic_set_fb_for_plane(struct drm_plane_state *, struct drm_framebuffer *)
// with return type: void
void drm_atomic_set_fb_for_plane(struct drm_plane_state *arg0, struct drm_framebuffer *arg1) {
  // Void type
  return;
}

// Function: drm_atomic_state_alloc
// with type: struct drm_atomic_state *drm_atomic_state_alloc(struct drm_device *)
// with return type: (struct drm_atomic_state)*
struct drm_atomic_state *drm_atomic_state_alloc(struct drm_device *arg0) {
  // Pointer type
  return ldv_malloc(sizeof(struct drm_atomic_state));
}

// Function: drm_atomic_state_free
// with type: void drm_atomic_state_free(struct drm_atomic_state *)
// with return type: void
void drm_atomic_state_free(struct drm_atomic_state *arg0) {
  // Void type
  return;
}

// Function: drm_av_sync_delay
// with type: int drm_av_sync_delay(struct drm_connector *, struct drm_display_mode *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_av_sync_delay(struct drm_connector *arg0, struct drm_display_mode *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_calc_timestamping_constants
// with type: void drm_calc_timestamping_constants(struct drm_crtc *, const struct drm_display_mode *)
// with return type: void
void drm_calc_timestamping_constants(struct drm_crtc *arg0, const struct drm_display_mode *arg1) {
  // Void type
  return;
}

// Function: drm_calc_vbltimestamp_from_scanoutpos
// with type: int drm_calc_vbltimestamp_from_scanoutpos(struct drm_device *, int, int *, struct timeval *, unsigned int, const struct drm_crtc *, const struct drm_display_mode *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_calc_vbltimestamp_from_scanoutpos(struct drm_device *arg0, int arg1, int *arg2, struct timeval *arg3, unsigned int arg4, const struct drm_crtc *arg5, const struct drm_display_mode *arg6) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_clflush_pages
// with type: void drm_clflush_pages(struct page **, unsigned long)
// with return type: void
void drm_clflush_pages(struct page **arg0, unsigned long arg1) {
  // Void type
  return;
}

// Function: drm_clflush_sg
// with type: void drm_clflush_sg(struct sg_table *)
// with return type: void
void drm_clflush_sg(struct sg_table *arg0) {
  // Void type
  return;
}

// Function: drm_clflush_virt_range
// with type: void drm_clflush_virt_range(void *, unsigned long)
// with return type: void
void drm_clflush_virt_range(void *arg0, unsigned long arg1) {
  // Void type
  return;
}

// Function: drm_compat_ioctl
// with type: long int drm_compat_ioctl(struct file *, unsigned int, unsigned long)
// with return type: long int
long __VERIFIER_nondet_long(void);
long int drm_compat_ioctl(struct file *arg0, unsigned int arg1, unsigned long arg2) {
  // Simple type
  return __VERIFIER_nondet_long();
}

// Function: drm_connector_cleanup
// with type: void drm_connector_cleanup(struct drm_connector *)
// with return type: void
void drm_connector_cleanup(struct drm_connector *arg0) {
  // Void type
  return;
}

// Function: drm_connector_init
// with type: int drm_connector_init(struct drm_device *, struct drm_connector *, const struct drm_connector_funcs *, int)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_connector_init(struct drm_device *arg0, struct drm_connector *arg1, const struct drm_connector_funcs *arg2, int arg3) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_connector_register
// with type: int drm_connector_register(struct drm_connector *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_connector_register(struct drm_connector *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_connector_unregister
// with type: void drm_connector_unregister(struct drm_connector *)
// with return type: void
void drm_connector_unregister(struct drm_connector *arg0) {
  // Void type
  return;
}

// Function: drm_crtc_cleanup
// with type: void drm_crtc_cleanup(struct drm_crtc *)
// with return type: void
void drm_crtc_cleanup(struct drm_crtc *arg0) {
  // Void type
  return;
}

// Function: drm_crtc_get_hv_timing
// with type: void drm_crtc_get_hv_timing(const struct drm_display_mode *, int *, int *)
// with return type: void
void drm_crtc_get_hv_timing(const struct drm_display_mode *arg0, int *arg1, int *arg2) {
  // Void type
  return;
}

// Function: drm_crtc_index
// with type: unsigned int drm_crtc_index(struct drm_crtc *)
// with return type: unsigned int
unsigned int __VERIFIER_nondet_uint(void);
unsigned int drm_crtc_index(struct drm_crtc *arg0) {
  // Simple type
  return __VERIFIER_nondet_uint();
}

// Function: drm_crtc_init_with_planes
// with type: int drm_crtc_init_with_planes(struct drm_device *, struct drm_crtc *, struct drm_plane *, struct drm_plane *, const struct drm_crtc_funcs *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_crtc_init_with_planes(struct drm_device *arg0, struct drm_crtc *arg1, struct drm_plane *arg2, struct drm_plane *arg3, const struct drm_crtc_funcs *arg4) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_crtc_vblank_count
// with type: u32 drm_crtc_vblank_count(struct drm_crtc *)
// with return type: u32 
unsigned int __VERIFIER_nondet_uint(void);
u32 drm_crtc_vblank_count(struct drm_crtc *arg0) {
  // Typedef type
  // Real type: unsigned int
  // Simple type
  return __VERIFIER_nondet_uint();
}

// Function: drm_crtc_vblank_get
// with type: int drm_crtc_vblank_get(struct drm_crtc *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_crtc_vblank_get(struct drm_crtc *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_crtc_vblank_off
// with type: void drm_crtc_vblank_off(struct drm_crtc *)
// with return type: void
void drm_crtc_vblank_off(struct drm_crtc *arg0) {
  // Void type
  return;
}

// Function: drm_crtc_vblank_on
// with type: void drm_crtc_vblank_on(struct drm_crtc *)
// with return type: void
void drm_crtc_vblank_on(struct drm_crtc *arg0) {
  // Void type
  return;
}

// Function: drm_crtc_vblank_put
// with type: void drm_crtc_vblank_put(struct drm_crtc *)
// with return type: void
void drm_crtc_vblank_put(struct drm_crtc *arg0) {
  // Void type
  return;
}

// Function: drm_crtc_vblank_reset
// with type: void drm_crtc_vblank_reset(struct drm_crtc *)
// with return type: void
void drm_crtc_vblank_reset(struct drm_crtc *arg0) {
  // Void type
  return;
}

// Function: drm_debugfs_create_files
// with type: int drm_debugfs_create_files(const struct drm_info_list *, int, struct dentry *, struct drm_minor *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_debugfs_create_files(const struct drm_info_list *arg0, int arg1, struct dentry *arg2, struct drm_minor *arg3) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_debugfs_remove_files
// with type: int drm_debugfs_remove_files(const struct drm_info_list *, int, struct drm_minor *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_debugfs_remove_files(const struct drm_info_list *arg0, int arg1, struct drm_minor *arg2) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_detect_hdmi_monitor
// with type: bool drm_detect_hdmi_monitor(struct edid *)
// with return type: bool 
bool __VERIFIER_nondet_bool(void);
bool drm_detect_hdmi_monitor(struct edid *arg0) {
  // Typedef type
  // Real type: _Bool
  // Simple type
  return __VERIFIER_nondet_bool();
}

// Function: drm_detect_monitor_audio
// with type: bool drm_detect_monitor_audio(struct edid *)
// with return type: bool 
bool __VERIFIER_nondet_bool(void);
bool drm_detect_monitor_audio(struct edid *arg0) {
  // Typedef type
  // Real type: _Bool
  // Simple type
  return __VERIFIER_nondet_bool();
}

// Function: drm_dp_aux_register
// with type: int drm_dp_aux_register(struct drm_dp_aux *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_dp_aux_register(struct drm_dp_aux *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_dp_aux_unregister
// with type: void drm_dp_aux_unregister(struct drm_dp_aux *)
// with return type: void
void drm_dp_aux_unregister(struct drm_dp_aux *arg0) {
  // Void type
  return;
}

// Function: drm_dp_calc_pbn_mode
// with type: int drm_dp_calc_pbn_mode(int, int)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_dp_calc_pbn_mode(int arg0, int arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_dp_channel_eq_ok
// with type: bool drm_dp_channel_eq_ok(const u8 *, int)
// with return type: bool 
bool __VERIFIER_nondet_bool(void);
bool drm_dp_channel_eq_ok(const u8 *arg0, int arg1) {
  // Typedef type
  // Real type: _Bool
  // Simple type
  return __VERIFIER_nondet_bool();
}

// Function: drm_dp_check_act_status
// with type: int drm_dp_check_act_status(struct drm_dp_mst_topology_mgr *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_dp_check_act_status(struct drm_dp_mst_topology_mgr *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_dp_clock_recovery_ok
// with type: bool drm_dp_clock_recovery_ok(const u8 *, int)
// with return type: bool 
bool __VERIFIER_nondet_bool(void);
bool drm_dp_clock_recovery_ok(const u8 *arg0, int arg1) {
  // Typedef type
  // Real type: _Bool
  // Simple type
  return __VERIFIER_nondet_bool();
}

// Function: drm_dp_dpcd_read
// with type: ssize_t drm_dp_dpcd_read(struct drm_dp_aux *, unsigned int, void *, size_t )
// with return type: ssize_t 
long __VERIFIER_nondet_long(void);
ssize_t drm_dp_dpcd_read(struct drm_dp_aux *arg0, unsigned int arg1, void *arg2, size_t arg3) {
  // Typedef type
  // Real type: __kernel_ssize_t 
  // Typedef type
  // Real type: __kernel_long_t 
  // Typedef type
  // Real type: long
  // Simple type
  return __VERIFIER_nondet_long();
}

// Function: drm_dp_dpcd_write
// with type: ssize_t drm_dp_dpcd_write(struct drm_dp_aux *, unsigned int, void *, size_t )
// with return type: ssize_t 
long __VERIFIER_nondet_long(void);
ssize_t drm_dp_dpcd_write(struct drm_dp_aux *arg0, unsigned int arg1, void *arg2, size_t arg3) {
  // Typedef type
  // Real type: __kernel_ssize_t 
  // Typedef type
  // Real type: __kernel_long_t 
  // Typedef type
  // Real type: long
  // Simple type
  return __VERIFIER_nondet_long();
}

// Function: drm_dp_find_vcpi_slots
// with type: int drm_dp_find_vcpi_slots(struct drm_dp_mst_topology_mgr *, int)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_dp_find_vcpi_slots(struct drm_dp_mst_topology_mgr *arg0, int arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_dp_get_adjust_request_pre_emphasis
// with type: u8 drm_dp_get_adjust_request_pre_emphasis(const u8 *, int)
// with return type: u8 
unsigned char __VERIFIER_nondet_uchar(void);
u8 drm_dp_get_adjust_request_pre_emphasis(const u8 *arg0, int arg1) {
  // Typedef type
  // Real type: unsigned char
  // Simple type
  return __VERIFIER_nondet_uchar();
}

// Function: drm_dp_get_adjust_request_voltage
// with type: u8 drm_dp_get_adjust_request_voltage(const u8 *, int)
// with return type: u8 
unsigned char __VERIFIER_nondet_uchar(void);
u8 drm_dp_get_adjust_request_voltage(const u8 *arg0, int arg1) {
  // Typedef type
  // Real type: unsigned char
  // Simple type
  return __VERIFIER_nondet_uchar();
}

// Function: drm_dp_link_rate_to_bw_code
// with type: u8 drm_dp_link_rate_to_bw_code(int)
// with return type: u8 
unsigned char __VERIFIER_nondet_uchar(void);
u8 drm_dp_link_rate_to_bw_code(int arg0) {
  // Typedef type
  // Real type: unsigned char
  // Simple type
  return __VERIFIER_nondet_uchar();
}

// Function: drm_dp_link_train_channel_eq_delay
// with type: void drm_dp_link_train_channel_eq_delay(const u8 *)
// with return type: void
void drm_dp_link_train_channel_eq_delay(const u8 *arg0) {
  // Void type
  return;
}

// Function: drm_dp_link_train_clock_recovery_delay
// with type: void drm_dp_link_train_clock_recovery_delay(const u8 *)
// with return type: void
void drm_dp_link_train_clock_recovery_delay(const u8 *arg0) {
  // Void type
  return;
}

// Function: drm_dp_mst_allocate_vcpi
// with type: bool drm_dp_mst_allocate_vcpi(struct drm_dp_mst_topology_mgr *, struct drm_dp_mst_port *, int, int *)
// with return type: bool 
bool __VERIFIER_nondet_bool(void);
bool drm_dp_mst_allocate_vcpi(struct drm_dp_mst_topology_mgr *arg0, struct drm_dp_mst_port *arg1, int arg2, int *arg3) {
  // Typedef type
  // Real type: _Bool
  // Simple type
  return __VERIFIER_nondet_bool();
}

// Function: drm_dp_mst_deallocate_vcpi
// with type: void drm_dp_mst_deallocate_vcpi(struct drm_dp_mst_topology_mgr *, struct drm_dp_mst_port *)
// with return type: void
void drm_dp_mst_deallocate_vcpi(struct drm_dp_mst_topology_mgr *arg0, struct drm_dp_mst_port *arg1) {
  // Void type
  return;
}

// Function: drm_dp_mst_detect_port
// with type: enum drm_connector_status drm_dp_mst_detect_port(struct drm_connector *, struct drm_dp_mst_topology_mgr *, struct drm_dp_mst_port *)
// with return type: enum drm_connector_status
int __VERIFIER_nondet_int(void);
enum drm_connector_status drm_dp_mst_detect_port(struct drm_connector *arg0, struct drm_dp_mst_topology_mgr *arg1, struct drm_dp_mst_port *arg2) {
  // Enum type
  return __VERIFIER_nondet_int();
}

// Function: drm_dp_mst_dump_topology
// with type: void drm_dp_mst_dump_topology(struct seq_file *, struct drm_dp_mst_topology_mgr *)
// with return type: void
void drm_dp_mst_dump_topology(struct seq_file *arg0, struct drm_dp_mst_topology_mgr *arg1) {
  // Void type
  return;
}

// Function: drm_dp_mst_get_edid
// with type: struct edid *drm_dp_mst_get_edid(struct drm_connector *, struct drm_dp_mst_topology_mgr *, struct drm_dp_mst_port *)
// with return type: (struct edid)*
struct edid *drm_dp_mst_get_edid(struct drm_connector *arg0, struct drm_dp_mst_topology_mgr *arg1, struct drm_dp_mst_port *arg2) {
  // Pointer type
  return ldv_malloc(sizeof(struct edid));
}

// Function: drm_dp_mst_hpd_irq
// with type: int drm_dp_mst_hpd_irq(struct drm_dp_mst_topology_mgr *, u8 *, bool *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_dp_mst_hpd_irq(struct drm_dp_mst_topology_mgr *arg0, u8 *arg1, bool *arg2) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_dp_mst_reset_vcpi_slots
// with type: void drm_dp_mst_reset_vcpi_slots(struct drm_dp_mst_topology_mgr *, struct drm_dp_mst_port *)
// with return type: void
void drm_dp_mst_reset_vcpi_slots(struct drm_dp_mst_topology_mgr *arg0, struct drm_dp_mst_port *arg1) {
  // Void type
  return;
}

// Function: drm_dp_mst_topology_mgr_destroy
// with type: void drm_dp_mst_topology_mgr_destroy(struct drm_dp_mst_topology_mgr *)
// with return type: void
void drm_dp_mst_topology_mgr_destroy(struct drm_dp_mst_topology_mgr *arg0) {
  // Void type
  return;
}

// Function: drm_dp_mst_topology_mgr_init
// with type: int drm_dp_mst_topology_mgr_init(struct drm_dp_mst_topology_mgr *, struct device *, struct drm_dp_aux *, int, int, int)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_dp_mst_topology_mgr_init(struct drm_dp_mst_topology_mgr *arg0, struct device *arg1, struct drm_dp_aux *arg2, int arg3, int arg4, int arg5) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_dp_mst_topology_mgr_resume
// with type: int drm_dp_mst_topology_mgr_resume(struct drm_dp_mst_topology_mgr *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_dp_mst_topology_mgr_resume(struct drm_dp_mst_topology_mgr *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_dp_mst_topology_mgr_set_mst
// with type: int drm_dp_mst_topology_mgr_set_mst(struct drm_dp_mst_topology_mgr *, bool )
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_dp_mst_topology_mgr_set_mst(struct drm_dp_mst_topology_mgr *arg0, bool arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_dp_mst_topology_mgr_suspend
// with type: void drm_dp_mst_topology_mgr_suspend(struct drm_dp_mst_topology_mgr *)
// with return type: void
void drm_dp_mst_topology_mgr_suspend(struct drm_dp_mst_topology_mgr *arg0) {
  // Void type
  return;
}

// Function: drm_dp_update_payload_part1
// with type: int drm_dp_update_payload_part1(struct drm_dp_mst_topology_mgr *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_dp_update_payload_part1(struct drm_dp_mst_topology_mgr *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_dp_update_payload_part2
// with type: int drm_dp_update_payload_part2(struct drm_dp_mst_topology_mgr *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_dp_update_payload_part2(struct drm_dp_mst_topology_mgr *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_edid_duplicate
// with type: struct edid *drm_edid_duplicate(const struct edid *)
// with return type: (struct edid)*
struct edid *drm_edid_duplicate(const struct edid *arg0) {
  // Pointer type
  return ldv_malloc(sizeof(struct edid));
}

// Function: drm_edid_to_eld
// with type: void drm_edid_to_eld(struct drm_connector *, struct edid *)
// with return type: void
void drm_edid_to_eld(struct drm_connector *arg0, struct edid *arg1) {
  // Void type
  return;
}

// Function: drm_encoder_cleanup
// with type: void drm_encoder_cleanup(struct drm_encoder *)
// with return type: void
void drm_encoder_cleanup(struct drm_encoder *arg0) {
  // Void type
  return;
}

// Function: drm_encoder_init
// with type: int drm_encoder_init(struct drm_device *, struct drm_encoder *, const struct drm_encoder_funcs *, int)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_encoder_init(struct drm_device *arg0, struct drm_encoder *arg1, const struct drm_encoder_funcs *arg2, int arg3) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_err
// with type: void drm_err(const char *, ...)
// with return type: void
void drm_err(const char *arg0, ...) {
  // Void type
  return;
}

// Function: drm_fb_helper_add_one_connector
// with type: int drm_fb_helper_add_one_connector(struct drm_fb_helper *, struct drm_connector *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_fb_helper_add_one_connector(struct drm_fb_helper *arg0, struct drm_connector *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_fb_helper_blank
// with type: int drm_fb_helper_blank(int, struct fb_info *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_fb_helper_blank(int arg0, struct fb_info *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_fb_helper_check_var
// with type: int drm_fb_helper_check_var(struct fb_var_screeninfo *, struct fb_info *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_fb_helper_check_var(struct fb_var_screeninfo *arg0, struct fb_info *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_fb_helper_debug_enter
// with type: int drm_fb_helper_debug_enter(struct fb_info *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_fb_helper_debug_enter(struct fb_info *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_fb_helper_debug_leave
// with type: int drm_fb_helper_debug_leave(struct fb_info *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_fb_helper_debug_leave(struct fb_info *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_fb_helper_fill_fix
// with type: void drm_fb_helper_fill_fix(struct fb_info *, uint32_t , uint32_t )
// with return type: void
void drm_fb_helper_fill_fix(struct fb_info *arg0, uint32_t arg1, uint32_t arg2) {
  // Void type
  return;
}

// Function: drm_fb_helper_fill_var
// with type: void drm_fb_helper_fill_var(struct fb_info *, struct drm_fb_helper *, uint32_t , uint32_t )
// with return type: void
void drm_fb_helper_fill_var(struct fb_info *arg0, struct drm_fb_helper *arg1, uint32_t arg2, uint32_t arg3) {
  // Void type
  return;
}

// Function: drm_fb_helper_fini
// with type: void drm_fb_helper_fini(struct drm_fb_helper *)
// with return type: void
void drm_fb_helper_fini(struct drm_fb_helper *arg0) {
  // Void type
  return;
}

// Function: drm_fb_helper_hotplug_event
// with type: int drm_fb_helper_hotplug_event(struct drm_fb_helper *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_fb_helper_hotplug_event(struct drm_fb_helper *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_fb_helper_init
// with type: int drm_fb_helper_init(struct drm_device *, struct drm_fb_helper *, int, int)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_fb_helper_init(struct drm_device *arg0, struct drm_fb_helper *arg1, int arg2, int arg3) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_fb_helper_initial_config
// with type: int drm_fb_helper_initial_config(struct drm_fb_helper *, int)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_fb_helper_initial_config(struct drm_fb_helper *arg0, int arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_fb_helper_pan_display
// with type: int drm_fb_helper_pan_display(struct fb_var_screeninfo *, struct fb_info *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_fb_helper_pan_display(struct fb_var_screeninfo *arg0, struct fb_info *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_fb_helper_prepare
// with type: void drm_fb_helper_prepare(struct drm_device *, struct drm_fb_helper *, const struct drm_fb_helper_funcs *)
// with return type: void
void drm_fb_helper_prepare(struct drm_device *arg0, struct drm_fb_helper *arg1, const struct drm_fb_helper_funcs *arg2) {
  // Void type
  return;
}

// Function: drm_fb_helper_remove_one_connector
// with type: int drm_fb_helper_remove_one_connector(struct drm_fb_helper *, struct drm_connector *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_fb_helper_remove_one_connector(struct drm_fb_helper *arg0, struct drm_connector *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_fb_helper_restore_fbdev_mode_unlocked
// with type: bool drm_fb_helper_restore_fbdev_mode_unlocked(struct drm_fb_helper *)
// with return type: bool 
bool __VERIFIER_nondet_bool(void);
bool drm_fb_helper_restore_fbdev_mode_unlocked(struct drm_fb_helper *arg0) {
  // Typedef type
  // Real type: _Bool
  // Simple type
  return __VERIFIER_nondet_bool();
}

// Function: drm_fb_helper_set_par
// with type: int drm_fb_helper_set_par(struct fb_info *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_fb_helper_set_par(struct fb_info *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_fb_helper_setcmap
// with type: int drm_fb_helper_setcmap(struct fb_cmap *, struct fb_info *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_fb_helper_setcmap(struct fb_cmap *arg0, struct fb_info *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_fb_helper_single_add_all_connectors
// with type: int drm_fb_helper_single_add_all_connectors(struct drm_fb_helper *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_fb_helper_single_add_all_connectors(struct drm_fb_helper *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_format_plane_cpp
// with type: int drm_format_plane_cpp(uint32_t , int)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_format_plane_cpp(uint32_t arg0, int arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_framebuffer_cleanup
// with type: void drm_framebuffer_cleanup(struct drm_framebuffer *)
// with return type: void
void drm_framebuffer_cleanup(struct drm_framebuffer *arg0) {
  // Void type
  return;
}

// Function: drm_framebuffer_init
// with type: int drm_framebuffer_init(struct drm_device *, struct drm_framebuffer *, const struct drm_framebuffer_funcs *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_framebuffer_init(struct drm_device *arg0, struct drm_framebuffer *arg1, const struct drm_framebuffer_funcs *arg2) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_framebuffer_reference
// with type: void drm_framebuffer_reference(struct drm_framebuffer *)
// with return type: void
void drm_framebuffer_reference(struct drm_framebuffer *arg0) {
  // Void type
  return;
}

// Function: drm_framebuffer_remove
// with type: void drm_framebuffer_remove(struct drm_framebuffer *)
// with return type: void
void drm_framebuffer_remove(struct drm_framebuffer *arg0) {
  // Void type
  return;
}

// Function: drm_framebuffer_unreference
// with type: void drm_framebuffer_unreference(struct drm_framebuffer *)
// with return type: void
void drm_framebuffer_unreference(struct drm_framebuffer *arg0) {
  // Void type
  return;
}

// Function: drm_framebuffer_unregister_private
// with type: void drm_framebuffer_unregister_private(struct drm_framebuffer *)
// with return type: void
void drm_framebuffer_unregister_private(struct drm_framebuffer *arg0) {
  // Void type
  return;
}

// Function: drm_gem_create_mmap_offset
// with type: int drm_gem_create_mmap_offset(struct drm_gem_object *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_gem_create_mmap_offset(struct drm_gem_object *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_gem_dmabuf_release
// with type: void drm_gem_dmabuf_release(struct dma_buf *)
// with return type: void
void drm_gem_dmabuf_release(struct dma_buf *arg0) {
  // Void type
  return;
}

// Function: drm_gem_dumb_destroy
// with type: int drm_gem_dumb_destroy(struct drm_file *, struct drm_device *, uint32_t )
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_gem_dumb_destroy(struct drm_file *arg0, struct drm_device *arg1, uint32_t arg2) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_gem_free_mmap_offset
// with type: void drm_gem_free_mmap_offset(struct drm_gem_object *)
// with return type: void
void drm_gem_free_mmap_offset(struct drm_gem_object *arg0) {
  // Void type
  return;
}

// Function: drm_gem_handle_create
// with type: int drm_gem_handle_create(struct drm_file *, struct drm_gem_object *, u32 *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_gem_handle_create(struct drm_file *arg0, struct drm_gem_object *arg1, u32 *arg2) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_gem_mmap
// with type: int drm_gem_mmap(struct file *, struct vm_area_struct *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_gem_mmap(struct file *arg0, struct vm_area_struct *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_gem_object_init
// with type: int drm_gem_object_init(struct drm_device *, struct drm_gem_object *, size_t )
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_gem_object_init(struct drm_device *arg0, struct drm_gem_object *arg1, size_t arg2) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_gem_object_lookup
// with type: struct drm_gem_object *drm_gem_object_lookup(struct drm_device *, struct drm_file *, u32 )
// with return type: (struct drm_gem_object)*
struct drm_gem_object *drm_gem_object_lookup(struct drm_device *arg0, struct drm_file *arg1, u32 arg2) {
  // Pointer type
  return ldv_malloc(sizeof(struct drm_gem_object));
}

// Function: drm_gem_object_release
// with type: void drm_gem_object_release(struct drm_gem_object *)
// with return type: void
void drm_gem_object_release(struct drm_gem_object *arg0) {
  // Void type
  return;
}

// Function: drm_gem_prime_fd_to_handle
// with type: int drm_gem_prime_fd_to_handle(struct drm_device *, struct drm_file *, int, uint32_t *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_gem_prime_fd_to_handle(struct drm_device *arg0, struct drm_file *arg1, int arg2, uint32_t *arg3) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_gem_prime_handle_to_fd
// with type: int drm_gem_prime_handle_to_fd(struct drm_device *, struct drm_file *, uint32_t , uint32_t , int *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_gem_prime_handle_to_fd(struct drm_device *arg0, struct drm_file *arg1, uint32_t arg2, uint32_t arg3, int *arg4) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_gem_private_object_init
// with type: void drm_gem_private_object_init(struct drm_device *, struct drm_gem_object *, size_t )
// with return type: void
void drm_gem_private_object_init(struct drm_device *arg0, struct drm_gem_object *arg1, size_t arg2) {
  // Void type
  return;
}

// Function: drm_gem_vm_close
// with type: void drm_gem_vm_close(struct vm_area_struct *)
// with return type: void
void drm_gem_vm_close(struct vm_area_struct *arg0) {
  // Void type
  return;
}

// Function: drm_gem_vm_open
// with type: void drm_gem_vm_open(struct vm_area_struct *)
// with return type: void
void drm_gem_vm_open(struct vm_area_struct *arg0) {
  // Void type
  return;
}

// Function: drm_get_connector_status_name
// with type: const char *drm_get_connector_status_name(enum drm_connector_status )
// with return type: (const char)*
const char *drm_get_connector_status_name(enum drm_connector_status arg0) {
  // Pointer type
  return ldv_malloc(sizeof(char));
}

// Function: drm_get_edid
// with type: struct edid *drm_get_edid(struct drm_connector *, struct i2c_adapter *)
// with return type: (struct edid)*
struct edid *drm_get_edid(struct drm_connector *arg0, struct i2c_adapter *arg1) {
  // Pointer type
  return ldv_malloc(sizeof(struct edid));
}

// Function: drm_get_format_name
// with type: const char *drm_get_format_name(uint32_t )
// with return type: (const char)*
const char *drm_get_format_name(uint32_t arg0) {
  // Pointer type
  return ldv_malloc(sizeof(char));
}

// Function: drm_get_pci_dev
// with type: int drm_get_pci_dev(struct pci_dev *, const struct pci_device_id *, struct drm_driver *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_get_pci_dev(struct pci_dev *arg0, const struct pci_device_id *arg1, struct drm_driver *arg2) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_get_subpixel_order_name
// with type: const char *drm_get_subpixel_order_name(enum subpixel_order )
// with return type: (const char)*
const char *drm_get_subpixel_order_name(enum subpixel_order arg0) {
  // Pointer type
  return ldv_malloc(sizeof(char));
}

// Function: drm_handle_vblank
// with type: bool drm_handle_vblank(struct drm_device *, int)
// with return type: bool 
bool __VERIFIER_nondet_bool(void);
bool drm_handle_vblank(struct drm_device *arg0, int arg1) {
  // Typedef type
  // Real type: _Bool
  // Simple type
  return __VERIFIER_nondet_bool();
}

// Function: drm_has_preferred_mode
// with type: struct drm_display_mode *drm_has_preferred_mode(struct drm_fb_helper_connector *, int, int)
// with return type: (struct drm_display_mode)*
struct drm_display_mode *drm_has_preferred_mode(struct drm_fb_helper_connector *arg0, int arg1, int arg2) {
  // Pointer type
  return ldv_malloc(sizeof(struct drm_display_mode));
}

// Function: drm_hdmi_avi_infoframe_from_display_mode
// with type: int drm_hdmi_avi_infoframe_from_display_mode(struct hdmi_avi_infoframe *, const struct drm_display_mode *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_hdmi_avi_infoframe_from_display_mode(struct hdmi_avi_infoframe *arg0, const struct drm_display_mode *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_hdmi_vendor_infoframe_from_display_mode
// with type: int drm_hdmi_vendor_infoframe_from_display_mode(struct hdmi_vendor_infoframe *, const struct drm_display_mode *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_hdmi_vendor_infoframe_from_display_mode(struct hdmi_vendor_infoframe *arg0, const struct drm_display_mode *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_helper_hpd_irq_event
// with type: bool drm_helper_hpd_irq_event(struct drm_device *)
// with return type: bool 
bool __VERIFIER_nondet_bool(void);
bool drm_helper_hpd_irq_event(struct drm_device *arg0) {
  // Typedef type
  // Real type: _Bool
  // Simple type
  return __VERIFIER_nondet_bool();
}

// Function: drm_helper_mode_fill_fb_struct
// with type: void drm_helper_mode_fill_fb_struct(struct drm_framebuffer *, struct drm_mode_fb_cmd2 *)
// with return type: void
void drm_helper_mode_fill_fb_struct(struct drm_framebuffer *arg0, struct drm_mode_fb_cmd2 *arg1) {
  // Void type
  return;
}

// Function: drm_helper_move_panel_connectors_to_head
// with type: void drm_helper_move_panel_connectors_to_head(struct drm_device *)
// with return type: void
void drm_helper_move_panel_connectors_to_head(struct drm_device *arg0) {
  // Void type
  return;
}

// Function: drm_helper_probe_single_connector_modes
// with type: int drm_helper_probe_single_connector_modes(struct drm_connector *, uint32_t , uint32_t )
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_helper_probe_single_connector_modes(struct drm_connector *arg0, uint32_t arg1, uint32_t arg2) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_ioctl
// with type: long int drm_ioctl(struct file *, unsigned int, unsigned long)
// with return type: long int
long __VERIFIER_nondet_long(void);
long int drm_ioctl(struct file *arg0, unsigned int arg1, unsigned long arg2) {
  // Simple type
  return __VERIFIER_nondet_long();
}

// Function: drm_irq_install
// with type: int drm_irq_install(struct drm_device *, int)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_irq_install(struct drm_device *arg0, int arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_irq_uninstall
// with type: int drm_irq_uninstall(struct drm_device *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_irq_uninstall(struct drm_device *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_kms_helper_hotplug_event
// with type: void drm_kms_helper_hotplug_event(struct drm_device *)
// with return type: void
void drm_kms_helper_hotplug_event(struct drm_device *arg0) {
  // Void type
  return;
}

// Function: drm_kms_helper_poll_disable
// with type: void drm_kms_helper_poll_disable(struct drm_device *)
// with return type: void
void drm_kms_helper_poll_disable(struct drm_device *arg0) {
  // Void type
  return;
}

// Function: drm_kms_helper_poll_enable
// with type: void drm_kms_helper_poll_enable(struct drm_device *)
// with return type: void
void drm_kms_helper_poll_enable(struct drm_device *arg0) {
  // Void type
  return;
}

// Function: drm_kms_helper_poll_fini
// with type: void drm_kms_helper_poll_fini(struct drm_device *)
// with return type: void
void drm_kms_helper_poll_fini(struct drm_device *arg0) {
  // Void type
  return;
}

// Function: drm_kms_helper_poll_init
// with type: void drm_kms_helper_poll_init(struct drm_device *)
// with return type: void
void drm_kms_helper_poll_init(struct drm_device *arg0) {
  // Void type
  return;
}

// Function: drm_match_cea_mode
// with type: u8 drm_match_cea_mode(const struct drm_display_mode *)
// with return type: u8 
unsigned char __VERIFIER_nondet_uchar(void);
u8 drm_match_cea_mode(const struct drm_display_mode *arg0) {
  // Typedef type
  // Real type: unsigned char
  // Simple type
  return __VERIFIER_nondet_uchar();
}

// Function: drm_mm_init
// with type: void drm_mm_init(struct drm_mm *, u64 , u64 )
// with return type: void
void drm_mm_init(struct drm_mm *arg0, u64 arg1, u64 arg2) {
  // Void type
  return;
}

// Function: drm_mm_init_scan
// with type: void drm_mm_init_scan(struct drm_mm *, u64 , unsigned int, unsigned long)
// with return type: void
void drm_mm_init_scan(struct drm_mm *arg0, u64 arg1, unsigned int arg2, unsigned long arg3) {
  // Void type
  return;
}

// Function: drm_mm_init_scan_with_range
// with type: void drm_mm_init_scan_with_range(struct drm_mm *, u64 , unsigned int, unsigned long, u64 , u64 )
// with return type: void
void drm_mm_init_scan_with_range(struct drm_mm *arg0, u64 arg1, unsigned int arg2, unsigned long arg3, u64 arg4, u64 arg5) {
  // Void type
  return;
}

// Function: drm_mm_insert_node_generic
// with type: int drm_mm_insert_node_generic(struct drm_mm *, struct drm_mm_node *, u64 , unsigned int, unsigned long, enum drm_mm_search_flags , enum drm_mm_allocator_flags )
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_mm_insert_node_generic(struct drm_mm *arg0, struct drm_mm_node *arg1, u64 arg2, unsigned int arg3, unsigned long arg4, enum drm_mm_search_flags arg5, enum drm_mm_allocator_flags arg6) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_mm_insert_node_in_range_generic
// with type: int drm_mm_insert_node_in_range_generic(struct drm_mm *, struct drm_mm_node *, u64 , unsigned int, unsigned long, u64 , u64 , enum drm_mm_search_flags , enum drm_mm_allocator_flags )
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_mm_insert_node_in_range_generic(struct drm_mm *arg0, struct drm_mm_node *arg1, u64 arg2, unsigned int arg3, unsigned long arg4, u64 arg5, u64 arg6, enum drm_mm_search_flags arg7, enum drm_mm_allocator_flags arg8) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_mm_remove_node
// with type: void drm_mm_remove_node(struct drm_mm_node *)
// with return type: void
void drm_mm_remove_node(struct drm_mm_node *arg0) {
  // Void type
  return;
}

// Function: drm_mm_reserve_node
// with type: int drm_mm_reserve_node(struct drm_mm *, struct drm_mm_node *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_mm_reserve_node(struct drm_mm *arg0, struct drm_mm_node *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_mm_scan_add_block
// with type: bool drm_mm_scan_add_block(struct drm_mm_node *)
// with return type: bool 
bool __VERIFIER_nondet_bool(void);
bool drm_mm_scan_add_block(struct drm_mm_node *arg0) {
  // Typedef type
  // Real type: _Bool
  // Simple type
  return __VERIFIER_nondet_bool();
}

// Function: drm_mm_scan_remove_block
// with type: bool drm_mm_scan_remove_block(struct drm_mm_node *)
// with return type: bool 
bool __VERIFIER_nondet_bool(void);
bool drm_mm_scan_remove_block(struct drm_mm_node *arg0) {
  // Typedef type
  // Real type: _Bool
  // Simple type
  return __VERIFIER_nondet_bool();
}

// Function: drm_mm_takedown
// with type: void drm_mm_takedown(struct drm_mm *)
// with return type: void
void drm_mm_takedown(struct drm_mm *arg0) {
  // Void type
  return;
}

// Function: drm_mode_config_cleanup
// with type: void drm_mode_config_cleanup(struct drm_device *)
// with return type: void
void drm_mode_config_cleanup(struct drm_device *arg0) {
  // Void type
  return;
}

// Function: drm_mode_config_init
// with type: void drm_mode_config_init(struct drm_device *)
// with return type: void
void drm_mode_config_init(struct drm_device *arg0) {
  // Void type
  return;
}

// Function: drm_mode_config_reset
// with type: void drm_mode_config_reset(struct drm_device *)
// with return type: void
void drm_mode_config_reset(struct drm_device *arg0) {
  // Void type
  return;
}

// Function: drm_mode_connector_attach_encoder
// with type: int drm_mode_connector_attach_encoder(struct drm_connector *, struct drm_encoder *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_mode_connector_attach_encoder(struct drm_connector *arg0, struct drm_encoder *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_mode_connector_set_path_property
// with type: int drm_mode_connector_set_path_property(struct drm_connector *, const char *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_mode_connector_set_path_property(struct drm_connector *arg0, const char *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_mode_connector_update_edid_property
// with type: int drm_mode_connector_update_edid_property(struct drm_connector *, const struct edid *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_mode_connector_update_edid_property(struct drm_connector *arg0, const struct edid *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_mode_copy
// with type: void drm_mode_copy(struct drm_display_mode *, const struct drm_display_mode *)
// with return type: void
void drm_mode_copy(struct drm_display_mode *arg0, const struct drm_display_mode *arg1) {
  // Void type
  return;
}

// Function: drm_mode_create
// with type: struct drm_display_mode *drm_mode_create(struct drm_device *)
// with return type: (struct drm_display_mode)*
struct drm_display_mode *drm_mode_create(struct drm_device *arg0) {
  // Pointer type
  return ldv_malloc(sizeof(struct drm_display_mode));
}

// Function: drm_mode_create_aspect_ratio_property
// with type: int drm_mode_create_aspect_ratio_property(struct drm_device *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_mode_create_aspect_ratio_property(struct drm_device *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_mode_create_rotation_property
// with type: struct drm_property *drm_mode_create_rotation_property(struct drm_device *, unsigned int)
// with return type: (struct drm_property)*
struct drm_property *drm_mode_create_rotation_property(struct drm_device *arg0, unsigned int arg1) {
  // Pointer type
  return ldv_malloc(sizeof(struct drm_property));
}

// Function: drm_mode_create_scaling_mode_property
// with type: int drm_mode_create_scaling_mode_property(struct drm_device *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_mode_create_scaling_mode_property(struct drm_device *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_mode_create_tv_properties
// with type: int drm_mode_create_tv_properties(struct drm_device *, unsigned int, char **)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_mode_create_tv_properties(struct drm_device *arg0, unsigned int arg1, char **arg2) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_mode_crtc_set_gamma_size
// with type: int drm_mode_crtc_set_gamma_size(struct drm_crtc *, int)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_mode_crtc_set_gamma_size(struct drm_crtc *arg0, int arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_mode_debug_printmodeline
// with type: void drm_mode_debug_printmodeline(const struct drm_display_mode *)
// with return type: void
void drm_mode_debug_printmodeline(const struct drm_display_mode *arg0) {
  // Void type
  return;
}

// Function: drm_mode_destroy
// with type: void drm_mode_destroy(struct drm_device *, struct drm_display_mode *)
// with return type: void
void drm_mode_destroy(struct drm_device *arg0, struct drm_display_mode *arg1) {
  // Void type
  return;
}

// Function: drm_mode_duplicate
// with type: struct drm_display_mode *drm_mode_duplicate(struct drm_device *, const struct drm_display_mode *)
// with return type: (struct drm_display_mode)*
struct drm_display_mode *drm_mode_duplicate(struct drm_device *arg0, const struct drm_display_mode *arg1) {
  // Pointer type
  return ldv_malloc(sizeof(struct drm_display_mode));
}

// Function: drm_mode_legacy_fb_format
// with type: uint32_t drm_mode_legacy_fb_format(uint32_t , uint32_t )
// with return type: uint32_t 
unsigned int __VERIFIER_nondet_uint(void);
uint32_t drm_mode_legacy_fb_format(uint32_t arg0, uint32_t arg1) {
  // Typedef type
  // Real type: __u32 
  // Typedef type
  // Real type: unsigned int
  // Simple type
  return __VERIFIER_nondet_uint();
}

// Function: drm_mode_object_find
// with type: struct drm_mode_object *drm_mode_object_find(struct drm_device *, uint32_t , uint32_t )
// with return type: (struct drm_mode_object)*
struct drm_mode_object *drm_mode_object_find(struct drm_device *arg0, uint32_t arg1, uint32_t arg2) {
  // Pointer type
  return ldv_malloc(sizeof(struct drm_mode_object));
}

// Function: drm_mode_probed_add
// with type: void drm_mode_probed_add(struct drm_connector *, struct drm_display_mode *)
// with return type: void
void drm_mode_probed_add(struct drm_connector *arg0, struct drm_display_mode *arg1) {
  // Void type
  return;
}

// Function: drm_mode_set_crtcinfo
// with type: void drm_mode_set_crtcinfo(struct drm_display_mode *, int)
// with return type: void
void drm_mode_set_crtcinfo(struct drm_display_mode *arg0, int arg1) {
  // Void type
  return;
}

// Function: drm_mode_set_name
// with type: void drm_mode_set_name(struct drm_display_mode *)
// with return type: void
void drm_mode_set_name(struct drm_display_mode *arg0) {
  // Void type
  return;
}

// Function: drm_mode_vrefresh
// with type: int drm_mode_vrefresh(const struct drm_display_mode *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_mode_vrefresh(const struct drm_display_mode *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_modeset_acquire_fini
// with type: void drm_modeset_acquire_fini(struct drm_modeset_acquire_ctx *)
// with return type: void
void drm_modeset_acquire_fini(struct drm_modeset_acquire_ctx *arg0) {
  // Void type
  return;
}

// Function: drm_modeset_acquire_init
// with type: void drm_modeset_acquire_init(struct drm_modeset_acquire_ctx *, uint32_t )
// with return type: void
void drm_modeset_acquire_init(struct drm_modeset_acquire_ctx *arg0, uint32_t arg1) {
  // Void type
  return;
}

// Function: drm_modeset_backoff
// with type: void drm_modeset_backoff(struct drm_modeset_acquire_ctx *)
// with return type: void
void drm_modeset_backoff(struct drm_modeset_acquire_ctx *arg0) {
  // Void type
  return;
}

// Function: drm_modeset_drop_locks
// with type: void drm_modeset_drop_locks(struct drm_modeset_acquire_ctx *)
// with return type: void
void drm_modeset_drop_locks(struct drm_modeset_acquire_ctx *arg0) {
  // Void type
  return;
}

// Function: drm_modeset_lock
// with type: int drm_modeset_lock(struct drm_modeset_lock *, struct drm_modeset_acquire_ctx *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_modeset_lock(struct drm_modeset_lock *arg0, struct drm_modeset_acquire_ctx *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_modeset_lock_all
// with type: void drm_modeset_lock_all(struct drm_device *)
// with return type: void
void drm_modeset_lock_all(struct drm_device *arg0) {
  // Void type
  return;
}

// Function: drm_modeset_unlock
// with type: void drm_modeset_unlock(struct drm_modeset_lock *)
// with return type: void
void drm_modeset_unlock(struct drm_modeset_lock *arg0) {
  // Void type
  return;
}

// Function: drm_modeset_unlock_all
// with type: void drm_modeset_unlock_all(struct drm_device *)
// with return type: void
void drm_modeset_unlock_all(struct drm_device *arg0) {
  // Void type
  return;
}

// Function: drm_object_attach_property
// with type: void drm_object_attach_property(struct drm_mode_object *, struct drm_property *, uint64_t )
// with return type: void
void drm_object_attach_property(struct drm_mode_object *arg0, struct drm_property *arg1, uint64_t arg2) {
  // Void type
  return;
}

// Function: drm_object_property_set_value
// with type: int drm_object_property_set_value(struct drm_mode_object *, struct drm_property *, uint64_t )
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_object_property_set_value(struct drm_mode_object *arg0, struct drm_property *arg1, uint64_t arg2) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_open
// with type: int drm_open(struct inode *, struct file *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_open(struct inode *arg0, struct file *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_panel_add
// with type: int drm_panel_add(struct drm_panel *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_panel_add(struct drm_panel *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_panel_attach
// with type: int drm_panel_attach(struct drm_panel *, struct drm_connector *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_panel_attach(struct drm_panel *arg0, struct drm_connector *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_panel_detach
// with type: int drm_panel_detach(struct drm_panel *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_panel_detach(struct drm_panel *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_panel_init
// with type: void drm_panel_init(struct drm_panel *)
// with return type: void
void drm_panel_init(struct drm_panel *arg0) {
  // Void type
  return;
}

// Function: drm_panel_remove
// with type: void drm_panel_remove(struct drm_panel *)
// with return type: void
void drm_panel_remove(struct drm_panel *arg0) {
  // Void type
  return;
}

// Function: drm_pci_alloc
// with type: struct drm_dma_handle *drm_pci_alloc(struct drm_device *, size_t , size_t )
// with return type: (struct drm_dma_handle)*
struct drm_dma_handle *drm_pci_alloc(struct drm_device *arg0, size_t arg1, size_t arg2) {
  // Pointer type
  return ldv_malloc(sizeof(struct drm_dma_handle));
}

// Function: drm_pci_exit
// with type: void drm_pci_exit(struct drm_driver *, struct pci_driver *)
// with return type: void
void drm_pci_exit(struct drm_driver *arg0, struct pci_driver *arg1) {
  // Void type
  return;
}

// Function: drm_pci_free
// with type: void drm_pci_free(struct drm_device *, struct drm_dma_handle *)
// with return type: void
void drm_pci_free(struct drm_device *arg0, struct drm_dma_handle *arg1) {
  // Void type
  return;
}

// Function: drm_pci_init
// with type: int drm_pci_init(struct drm_driver *, struct pci_driver *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_pci_init(struct drm_driver *arg0, struct pci_driver *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_pci_set_busid
// with type: int drm_pci_set_busid(struct drm_device *, struct drm_master *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_pci_set_busid(struct drm_device *arg0, struct drm_master *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_pick_cmdline_mode
// with type: struct drm_display_mode *drm_pick_cmdline_mode(struct drm_fb_helper_connector *, int, int)
// with return type: (struct drm_display_mode)*
struct drm_display_mode *drm_pick_cmdline_mode(struct drm_fb_helper_connector *arg0, int arg1, int arg2) {
  // Pointer type
  return ldv_malloc(sizeof(struct drm_display_mode));
}

// Function: drm_plane_cleanup
// with type: void drm_plane_cleanup(struct drm_plane *)
// with return type: void
void drm_plane_cleanup(struct drm_plane *arg0) {
  // Void type
  return;
}

// Function: drm_plane_from_index
// with type: struct drm_plane *drm_plane_from_index(struct drm_device *, int)
// with return type: (struct drm_plane)*
struct drm_plane *drm_plane_from_index(struct drm_device *arg0, int arg1) {
  // Pointer type
  return ldv_malloc(sizeof(struct drm_plane));
}

// Function: drm_plane_helper_check_update
// with type: int drm_plane_helper_check_update(struct drm_plane *, struct drm_crtc *, struct drm_framebuffer *, struct drm_rect *, struct drm_rect *, const struct drm_rect *, int, int, bool , bool , bool *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_plane_helper_check_update(struct drm_plane *arg0, struct drm_crtc *arg1, struct drm_framebuffer *arg2, struct drm_rect *arg3, struct drm_rect *arg4, const struct drm_rect *arg5, int arg6, int arg7, bool arg8, bool arg9, bool *arg10) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_plane_helper_disable
// with type: int drm_plane_helper_disable(struct drm_plane *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_plane_helper_disable(struct drm_plane *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_plane_helper_update
// with type: int drm_plane_helper_update(struct drm_plane *, struct drm_crtc *, struct drm_framebuffer *, int, int, unsigned int, unsigned int, uint32_t , uint32_t , uint32_t , uint32_t )
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_plane_helper_update(struct drm_plane *arg0, struct drm_crtc *arg1, struct drm_framebuffer *arg2, int arg3, int arg4, unsigned int arg5, unsigned int arg6, uint32_t arg7, uint32_t arg8, uint32_t arg9, uint32_t arg10) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_plane_index
// with type: unsigned int drm_plane_index(struct drm_plane *)
// with return type: unsigned int
unsigned int __VERIFIER_nondet_uint(void);
unsigned int drm_plane_index(struct drm_plane *arg0) {
  // Simple type
  return __VERIFIER_nondet_uint();
}

// Function: drm_poll
// with type: unsigned int drm_poll(struct file *, struct poll_table_struct *)
// with return type: unsigned int
unsigned int __VERIFIER_nondet_uint(void);
unsigned int drm_poll(struct file *arg0, struct poll_table_struct *arg1) {
  // Simple type
  return __VERIFIER_nondet_uint();
}

// Function: drm_prime_gem_destroy
// with type: void drm_prime_gem_destroy(struct drm_gem_object *, struct sg_table *)
// with return type: void
void drm_prime_gem_destroy(struct drm_gem_object *arg0, struct sg_table *arg1) {
  // Void type
  return;
}

// Function: drm_probe_ddc
// with type: bool drm_probe_ddc(struct i2c_adapter *)
// with return type: bool 
bool __VERIFIER_nondet_bool(void);
bool drm_probe_ddc(struct i2c_adapter *arg0) {
  // Typedef type
  // Real type: _Bool
  // Simple type
  return __VERIFIER_nondet_bool();
}

// Function: drm_property_add_enum
// with type: int drm_property_add_enum(struct drm_property *, int, uint64_t , const char *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_property_add_enum(struct drm_property *arg0, int arg1, uint64_t arg2, const char *arg3) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_property_create
// with type: struct drm_property *drm_property_create(struct drm_device *, int, const char *, int)
// with return type: (struct drm_property)*
struct drm_property *drm_property_create(struct drm_device *arg0, int arg1, const char *arg2, int arg3) {
  // Pointer type
  return ldv_malloc(sizeof(struct drm_property));
}

// Function: drm_property_create_enum
// with type: struct drm_property *drm_property_create_enum(struct drm_device *, int, const char *, const struct drm_prop_enum_list *, int)
// with return type: (struct drm_property)*
struct drm_property *drm_property_create_enum(struct drm_device *arg0, int arg1, const char *arg2, const struct drm_prop_enum_list *arg3, int arg4) {
  // Pointer type
  return ldv_malloc(sizeof(struct drm_property));
}

// Function: drm_property_create_range
// with type: struct drm_property *drm_property_create_range(struct drm_device *, int, const char *, uint64_t , uint64_t )
// with return type: (struct drm_property)*
struct drm_property *drm_property_create_range(struct drm_device *arg0, int arg1, const char *arg2, uint64_t arg3, uint64_t arg4) {
  // Pointer type
  return ldv_malloc(sizeof(struct drm_property));
}

// Function: drm_put_dev
// with type: void drm_put_dev(struct drm_device *)
// with return type: void
void drm_put_dev(struct drm_device *arg0) {
  // Void type
  return;
}

// Function: drm_read
// with type: ssize_t drm_read(struct file *, char *, size_t , loff_t *)
// with return type: ssize_t 
long __VERIFIER_nondet_long(void);
ssize_t drm_read(struct file *arg0, char *arg1, size_t arg2, loff_t *arg3) {
  // Typedef type
  // Real type: __kernel_ssize_t 
  // Typedef type
  // Real type: __kernel_long_t 
  // Typedef type
  // Real type: long
  // Simple type
  return __VERIFIER_nondet_long();
}

// Function: drm_rect_calc_hscale
// with type: int drm_rect_calc_hscale(const struct drm_rect *, const struct drm_rect *, int, int)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_rect_calc_hscale(const struct drm_rect *arg0, const struct drm_rect *arg1, int arg2, int arg3) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_rect_calc_hscale_relaxed
// with type: int drm_rect_calc_hscale_relaxed(struct drm_rect *, struct drm_rect *, int, int)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_rect_calc_hscale_relaxed(struct drm_rect *arg0, struct drm_rect *arg1, int arg2, int arg3) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_rect_calc_vscale
// with type: int drm_rect_calc_vscale(const struct drm_rect *, const struct drm_rect *, int, int)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_rect_calc_vscale(const struct drm_rect *arg0, const struct drm_rect *arg1, int arg2, int arg3) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_rect_calc_vscale_relaxed
// with type: int drm_rect_calc_vscale_relaxed(struct drm_rect *, struct drm_rect *, int, int)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_rect_calc_vscale_relaxed(struct drm_rect *arg0, struct drm_rect *arg1, int arg2, int arg3) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_rect_clip_scaled
// with type: bool drm_rect_clip_scaled(struct drm_rect *, struct drm_rect *, const struct drm_rect *, int, int)
// with return type: bool 
bool __VERIFIER_nondet_bool(void);
bool drm_rect_clip_scaled(struct drm_rect *arg0, struct drm_rect *arg1, const struct drm_rect *arg2, int arg3, int arg4) {
  // Typedef type
  // Real type: _Bool
  // Simple type
  return __VERIFIER_nondet_bool();
}

// Function: drm_rect_debug_print
// with type: void drm_rect_debug_print(const struct drm_rect *, bool )
// with return type: void
void drm_rect_debug_print(const struct drm_rect *arg0, bool arg1) {
  // Void type
  return;
}

// Function: drm_rect_rotate
// with type: void drm_rect_rotate(struct drm_rect *, int, int, unsigned int)
// with return type: void
void drm_rect_rotate(struct drm_rect *arg0, int arg1, int arg2, unsigned int arg3) {
  // Void type
  return;
}

// Function: drm_rect_rotate_inv
// with type: void drm_rect_rotate_inv(struct drm_rect *, int, int, unsigned int)
// with return type: void
void drm_rect_rotate_inv(struct drm_rect *arg0, int arg1, int arg2, unsigned int arg3) {
  // Void type
  return;
}

// Function: drm_reinit_primary_mode_group
// with type: void drm_reinit_primary_mode_group(struct drm_device *)
// with return type: void
void drm_reinit_primary_mode_group(struct drm_device *arg0) {
  // Void type
  return;
}

// Function: drm_release
// with type: int drm_release(struct inode *, struct file *)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_release(struct inode *arg0, struct file *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_rgb_quant_range_selectable
// with type: bool drm_rgb_quant_range_selectable(struct edid *)
// with return type: bool 
bool __VERIFIER_nondet_bool(void);
bool drm_rgb_quant_range_selectable(struct edid *arg0) {
  // Typedef type
  // Real type: _Bool
  // Simple type
  return __VERIFIER_nondet_bool();
}

// Function: drm_select_eld
// with type: struct drm_connector *drm_select_eld(struct drm_encoder *, struct drm_display_mode *)
// with return type: (struct drm_connector)*
struct drm_connector *drm_select_eld(struct drm_encoder *arg0, struct drm_display_mode *arg1) {
  // Pointer type
  return ldv_malloc(sizeof(struct drm_connector));
}

// Function: drm_send_vblank_event
// with type: void drm_send_vblank_event(struct drm_device *, int, struct drm_pending_vblank_event *)
// with return type: void
void drm_send_vblank_event(struct drm_device *arg0, int arg1, struct drm_pending_vblank_event *arg2) {
  // Void type
  return;
}

// Function: drm_universal_plane_init
// with type: int drm_universal_plane_init(struct drm_device *, struct drm_plane *, unsigned long, const struct drm_plane_funcs *, const uint32_t *, uint32_t , enum drm_plane_type )
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_universal_plane_init(struct drm_device *arg0, struct drm_plane *arg1, unsigned long arg2, const struct drm_plane_funcs *arg3, const uint32_t *arg4, uint32_t arg5, enum drm_plane_type arg6) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_ut_debug_printk
// with type: void drm_ut_debug_printk(const char *, const char *, ...)
// with return type: void
void drm_ut_debug_printk(const char *arg0, const char *arg1, ...) {
  // Void type
  return;
}

// Function: drm_vblank_cleanup
// with type: void drm_vblank_cleanup(struct drm_device *)
// with return type: void
void drm_vblank_cleanup(struct drm_device *arg0) {
  // Void type
  return;
}

// Function: drm_vblank_count
// with type: u32 drm_vblank_count(struct drm_device *, int)
// with return type: u32 
unsigned int __VERIFIER_nondet_uint(void);
u32 drm_vblank_count(struct drm_device *arg0, int arg1) {
  // Typedef type
  // Real type: unsigned int
  // Simple type
  return __VERIFIER_nondet_uint();
}

// Function: drm_vblank_init
// with type: int drm_vblank_init(struct drm_device *, int)
// with return type: int
int __VERIFIER_nondet_int(void);
int drm_vblank_init(struct drm_device *arg0, int arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: drm_wait_one_vblank
// with type: void drm_wait_one_vblank(struct drm_device *, int)
// with return type: void
void drm_wait_one_vblank(struct drm_device *arg0, int arg1) {
  // Void type
  return;
}

// Function: fb_alloc_cmap
// with type: int fb_alloc_cmap(struct fb_cmap *, int, int)
// with return type: int
int __VERIFIER_nondet_int(void);
int fb_alloc_cmap(struct fb_cmap *arg0, int arg1, int arg2) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: fb_dealloc_cmap
// with type: void fb_dealloc_cmap(struct fb_cmap *)
// with return type: void
void fb_dealloc_cmap(struct fb_cmap *arg0) {
  // Void type
  return;
}

// Function: fb_set_suspend
// with type: void fb_set_suspend(struct fb_info *, int)
// with return type: void
void fb_set_suspend(struct fb_info *arg0, int arg1) {
  // Void type
  return;
}

// Function: find_first_bit
// with type: unsigned long int find_first_bit(const unsigned long *, unsigned long)
// with return type: unsigned long int
unsigned long __VERIFIER_nondet_ulong(void);
unsigned long int find_first_bit(const unsigned long *arg0, unsigned long arg1) {
  // Simple type
  return __VERIFIER_nondet_ulong();
}

// Function: find_next_bit
// with type: unsigned long int find_next_bit(const unsigned long *, unsigned long, unsigned long)
// with return type: unsigned long int
unsigned long __VERIFIER_nondet_ulong(void);
unsigned long int find_next_bit(const unsigned long *arg0, unsigned long arg1, unsigned long arg2) {
  // Simple type
  return __VERIFIER_nondet_ulong();
}

// Function: find_vma
// with type: struct vm_area_struct *find_vma(struct mm_struct *, unsigned long)
// with return type: (struct vm_area_struct)*
struct vm_area_struct *find_vma(struct mm_struct *arg0, unsigned long arg1) {
  // Pointer type
  return ldv_malloc(sizeof(struct vm_area_struct));
}

// 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_delayed_work
// with type: bool flush_delayed_work(struct delayed_work *)
// with return type: bool 
bool __VERIFIER_nondet_bool(void);
bool flush_delayed_work(struct delayed_work *arg0) {
  // Typedef type
  // Real type: _Bool
  // Simple type
  return __VERIFIER_nondet_bool();
}

// Function: flush_work
// with type: bool flush_work(struct work_struct *)
// with return type: bool 
bool __VERIFIER_nondet_bool(void);
bool flush_work(struct work_struct *arg0) {
  // Typedef type
  // Real type: _Bool
  // Simple type
  return __VERIFIER_nondet_bool();
}

// 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: framebuffer_alloc
// with type: struct fb_info *framebuffer_alloc(size_t , struct device *)
// with return type: (struct fb_info)*
struct fb_info *framebuffer_alloc(size_t arg0, struct device *arg1) {
  // Pointer type
  return ldv_malloc(sizeof(struct fb_info));
}

// Function: framebuffer_release
// with type: void framebuffer_release(struct fb_info *)
// with return type: void
void framebuffer_release(struct fb_info *arg0) {
  // Void type
  return;
}

// Function: generic_file_llseek
// with type: loff_t generic_file_llseek(struct file *, loff_t , int)
// with return type: loff_t 
long __VERIFIER_nondet_long(void);
loff_t generic_file_llseek(struct file *arg0, loff_t arg1, int arg2) {
  // Typedef type
  // Real type: __kernel_loff_t 
  // Typedef type
  // Real type: long long
  // Simple type
  return __VERIFIER_nondet_long();
}

// Function: get_pid_task
// with type: struct task_struct *get_pid_task(struct pid *, enum pid_type )
// with return type: (struct task_struct)*
struct task_struct *get_pid_task(struct pid *arg0, enum pid_type arg1) {
  // Pointer type
  return ldv_malloc(sizeof(struct task_struct));
}

// Function: get_seconds
// with type: unsigned long int get_seconds()
// with return type: unsigned long int
unsigned long __VERIFIER_nondet_ulong(void);
unsigned long int get_seconds() {
  // Simple type
  return __VERIFIER_nondet_ulong();
}

// Function: get_user_pages
// with type: long int get_user_pages(struct task_struct *, struct mm_struct *, unsigned long, unsigned long, int, int, struct page **, struct vm_area_struct **)
// with return type: long int
long __VERIFIER_nondet_long(void);
long int get_user_pages(struct task_struct *arg0, struct mm_struct *arg1, unsigned long arg2, unsigned long arg3, int arg4, int arg5, struct page **arg6, struct vm_area_struct **arg7) {
  // Simple type
  return __VERIFIER_nondet_long();
}

// Function: hdmi_infoframe_pack
// with type: ssize_t hdmi_infoframe_pack(union hdmi_infoframe *, void *, size_t )
// with return type: ssize_t 
long __VERIFIER_nondet_long(void);
ssize_t hdmi_infoframe_pack(union hdmi_infoframe *arg0, void *arg1, size_t arg2) {
  // Typedef type
  // Real type: __kernel_ssize_t 
  // Typedef type
  // Real type: __kernel_long_t 
  // Typedef type
  // Real type: long
  // Simple type
  return __VERIFIER_nondet_long();
}

// Function: hdmi_spd_infoframe_init
// with type: int hdmi_spd_infoframe_init(struct hdmi_spd_infoframe *, const char *, const char *)
// with return type: int
int __VERIFIER_nondet_int(void);
int hdmi_spd_infoframe_init(struct hdmi_spd_infoframe *arg0, const char *arg1, const char *arg2) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: i2c_add_adapter
// with type: int i2c_add_adapter(struct i2c_adapter *)
// with return type: int
int __VERIFIER_nondet_int(void);
int i2c_add_adapter(struct i2c_adapter *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: i2c_del_adapter
// with type: void i2c_del_adapter(struct i2c_adapter *)
// with return type: void
void i2c_del_adapter(struct i2c_adapter *arg0) {
  // Void type
  return;
}

// 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: idr_alloc
// with type: int idr_alloc(struct idr *, void *, int, int, gfp_t )
// with return type: int
int __VERIFIER_nondet_int(void);
int idr_alloc(struct idr *arg0, void *arg1, int arg2, int arg3, gfp_t arg4) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: idr_destroy
// with type: void idr_destroy(struct idr *)
// with return type: void
void idr_destroy(struct idr *arg0) {
  // Void type
  return;
}

// Function: idr_find_slowpath
// with type: void *idr_find_slowpath(struct idr *, int)
// with return type: (void)*
void *idr_find_slowpath(struct idr *arg0, int arg1) {
  // Pointer type
  return ldv_malloc(0UL);
}

// Function: idr_for_each
// with type: int idr_for_each(struct idr *, int (*)(int, void *, void *), void *)
// with return type: int
int __VERIFIER_nondet_int(void);
int idr_for_each(struct idr *arg0, int (*arg1)(int, void *, void *), void *arg2) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: idr_init
// with type: void idr_init(struct idr *)
// with return type: void
void idr_init(struct idr *arg0) {
  // Void type
  return;
}

// Function: idr_remove
// with type: void idr_remove(struct idr *, int)
// with return type: void
void idr_remove(struct idr *arg0, int arg1) {
  // Void type
  return;
}

// Function: init_timer_key
// with type: void init_timer_key(struct timer_list *, unsigned int, const char *, struct lock_class_key *)
// with return type: void
void init_timer_key(struct timer_list *arg0, unsigned int arg1, const char *arg2, struct lock_class_key *arg3) {
  // Void type
  return;
}

// Function: intel_enable_gtt
// with type: bool intel_enable_gtt()
// with return type: bool 
bool __VERIFIER_nondet_bool(void);
bool intel_enable_gtt() {
  // Typedef type
  // Real type: _Bool
  // Simple type
  return __VERIFIER_nondet_bool();
}

// Function: intel_gmch_probe
// with type: int intel_gmch_probe(struct pci_dev *, struct pci_dev *, struct agp_bridge_data *)
// with return type: int
int __VERIFIER_nondet_int(void);
int intel_gmch_probe(struct pci_dev *arg0, struct pci_dev *arg1, struct agp_bridge_data *arg2) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: intel_gmch_remove
// with type: void intel_gmch_remove()
// with return type: void
void intel_gmch_remove() {
  // Void type
  return;
}

// Function: intel_gtt_chipset_flush
// with type: void intel_gtt_chipset_flush()
// with return type: void
void intel_gtt_chipset_flush() {
  // Void type
  return;
}

// Function: intel_gtt_clear_range
// with type: void intel_gtt_clear_range(unsigned int, unsigned int)
// with return type: void
void intel_gtt_clear_range(unsigned int arg0, unsigned int arg1) {
  // Void type
  return;
}

// Function: intel_gtt_get
// with type: void intel_gtt_get(size_t *, size_t *, phys_addr_t *, unsigned long *)
// with return type: void
void intel_gtt_get(size_t *arg0, size_t *arg1, phys_addr_t *arg2, unsigned long *arg3) {
  // Void type
  return;
}

// Function: intel_gtt_insert_sg_entries
// with type: void intel_gtt_insert_sg_entries(struct sg_table *, unsigned int, unsigned int)
// with return type: void
void intel_gtt_insert_sg_entries(struct sg_table *arg0, unsigned int arg1, unsigned int arg2) {
  // Void type
  return;
}

// Function: interval_tree_insert
// with type: void interval_tree_insert(struct interval_tree_node *, struct rb_root *)
// with return type: void
void interval_tree_insert(struct interval_tree_node *arg0, struct rb_root *arg1) {
  // Void type
  return;
}

// Function: interval_tree_iter_first
// with type: struct interval_tree_node *interval_tree_iter_first(struct rb_root *, unsigned long, unsigned long)
// with return type: (struct interval_tree_node)*
struct interval_tree_node *interval_tree_iter_first(struct rb_root *arg0, unsigned long arg1, unsigned long arg2) {
  // Pointer type
  return ldv_malloc(sizeof(struct interval_tree_node));
}

// Function: interval_tree_iter_next
// with type: struct interval_tree_node *interval_tree_iter_next(struct interval_tree_node *, unsigned long, unsigned long)
// with return type: (struct interval_tree_node)*
struct interval_tree_node *interval_tree_iter_next(struct interval_tree_node *arg0, unsigned long arg1, unsigned long arg2) {
  // Pointer type
  return ldv_malloc(sizeof(struct interval_tree_node));
}

// Function: interval_tree_remove
// with type: void interval_tree_remove(struct interval_tree_node *, struct rb_root *)
// with return type: void
void interval_tree_remove(struct interval_tree_node *arg0, struct rb_root *arg1) {
  // Void type
  return;
}

// Function: invalidate_mapping_pages
// with type: unsigned long int invalidate_mapping_pages(struct address_space *, unsigned long, unsigned long)
// with return type: unsigned long int
unsigned long __VERIFIER_nondet_ulong(void);
unsigned long int invalidate_mapping_pages(struct address_space *arg0, unsigned long arg1, unsigned long arg2) {
  // Simple type
  return __VERIFIER_nondet_ulong();
}

// Function: io_schedule_timeout
// with type: long int io_schedule_timeout(long)
// with return type: long int
long __VERIFIER_nondet_long(void);
long int io_schedule_timeout(long arg0) {
  // Simple type
  return __VERIFIER_nondet_long();
}

// Function: ioread32
// with type: unsigned int ioread32(void *)
// with return type: unsigned int
unsigned int __VERIFIER_nondet_uint(void);
unsigned int ioread32(void *arg0) {
  // Simple type
  return __VERIFIER_nondet_uint();
}

// Function: ioremap_cache
// with type: void *ioremap_cache(resource_size_t , unsigned long)
// with return type: (void)*
void *ioremap_cache(resource_size_t arg0, unsigned long arg1) {
  // Pointer type
  return ldv_malloc(0UL);
}

// Function: ioremap_nocache
// with type: void *ioremap_nocache(resource_size_t , unsigned long)
// with return type: (void)*
void *ioremap_nocache(resource_size_t arg0, unsigned long arg1) {
  // Pointer type
  return ldv_malloc(0UL);
}

// Function: ioremap_wc
// with type: void *ioremap_wc(resource_size_t , unsigned long)
// with return type: (void)*
void *ioremap_wc(resource_size_t arg0, unsigned long arg1) {
  // Pointer type
  return ldv_malloc(0UL);
}

// Function: iounmap
// with type: void iounmap(volatile void *)
// with return type: void
void iounmap(volatile void *arg0) {
  // Void type
  return;
}

// Function: iowrite32
// with type: void iowrite32(u32 , void *)
// with return type: void
void iowrite32(u32 arg0, void *arg1) {
  // Void type
  return;
}

// Function: jiffies_to_msecs
// with type: unsigned int jiffies_to_msecs(const unsigned long)
// with return type: unsigned int
unsigned int __VERIFIER_nondet_uint(void);
unsigned int jiffies_to_msecs(const unsigned long arg0) {
  // Simple type
  return __VERIFIER_nondet_uint();
}

// Function: jiffies_to_usecs
// with type: unsigned int jiffies_to_usecs(const unsigned long)
// with return type: unsigned int
unsigned int __VERIFIER_nondet_uint(void);
unsigned int jiffies_to_usecs(const unsigned long arg0) {
  // Simple type
  return __VERIFIER_nondet_uint();
}

// Function: kasprintf
// with type: char *kasprintf(gfp_t , const char *, ...)
// with return type: (char)*
char *kasprintf(gfp_t arg0, const char *arg1, ...) {
  // Pointer type
  return ldv_malloc(sizeof(char));
}

// 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: kmem_cache_create
// with type: struct kmem_cache *kmem_cache_create(const char *, size_t , size_t , unsigned long, void (*)(void *))
// with return type: (struct kmem_cache)*
struct kmem_cache *kmem_cache_create(const char *arg0, size_t arg1, size_t arg2, unsigned long arg3, void (*arg4)(void *)) {
  // Pointer type
  return ldv_malloc(0UL);
}

// Function: kmem_cache_destroy
// with type: void kmem_cache_destroy(struct kmem_cache *)
// with return type: void
void kmem_cache_destroy(struct kmem_cache *arg0) {
  // Void type
  return;
}

// Function: kmem_cache_free
// with type: void kmem_cache_free(struct kmem_cache *, void *)
// with return type: void
void kmem_cache_free(struct kmem_cache *arg0, void *arg1) {
  // Void type
  return;
}

// Function: kmemdup
// with type: void *kmemdup(const void *, size_t , gfp_t )
// with return type: (void)*
void *kmemdup(const void *arg0, size_t arg1, gfp_t arg2) {
  // Pointer type
  return ldv_malloc(0UL);
}

// Function: kobject_uevent_env
// with type: int kobject_uevent_env(struct kobject *, enum kobject_action , char **)
// with return type: int
int __VERIFIER_nondet_int(void);
int kobject_uevent_env(struct kobject *arg0, enum kobject_action arg1, char **arg2) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: kstrtoint
// with type: int kstrtoint(const char *, unsigned int, int *)
// with return type: int
int __VERIFIER_nondet_int(void);
int kstrtoint(const char *arg0, unsigned int arg1, int *arg2) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: kstrtouint
// with type: int kstrtouint(const char *, unsigned int, unsigned int *)
// with return type: int
int __VERIFIER_nondet_int(void);
int kstrtouint(const char *arg0, unsigned int arg1, unsigned int *arg2) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ktime_get
// with type: ktime_t ktime_get()
// with return type: ktime_t 
ktime_t ktime_get() {
  // Typedef type
  // Real type: union ktime
  // Composite type
  return *(union ktime *)ldv_xmalloc(sizeof(union ktime));
}

// Function: ktime_get_raw
// with type: ktime_t ktime_get_raw()
// with return type: ktime_t 
ktime_t ktime_get_raw() {
  // Typedef type
  // Real type: union ktime
  // Composite type
  return *(union ktime *)ldv_xmalloc(sizeof(union ktime));
}

// Function: kvfree
// with type: void kvfree(const void *)
// with return type: void
void kvfree(const void *arg0) {
  // Void type
  return;
}

// Function: ldv__builtin_va_end
// with type: void ldv__builtin_va_end(__builtin_va_list *)
// with return type: void
void ldv__builtin_va_end(__builtin_va_list *arg0) {
  // Void type
  return;
}

// Function: ldv__builtin_va_start
// with type: void ldv__builtin_va_start(__builtin_va_list *)
// with return type: void
void ldv__builtin_va_start(__builtin_va_list *arg0) {
  // Void type
  return;
}

// Function: ldv_close_46
// with type: int ldv_close_46()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_close_46() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_complete_191
// with type: int ldv_complete_191()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_complete_191() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_freeze_noirq_191
// with type: int ldv_freeze_noirq_191()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_freeze_noirq_191() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_initialize
// with type: void ldv_initialize()
// with return type: void
void ldv_initialize() {
  // Void type
  return;
}

// Function: ldv_open_46
// with type: int ldv_open_46()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_open_46() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_poweroff_noirq_191
// with type: int ldv_poweroff_noirq_191()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_poweroff_noirq_191() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_prepare_191
// with type: int ldv_prepare_191()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_prepare_191() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_probe_135
// with type: int ldv_probe_135()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_probe_135() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_probe_137
// with type: int ldv_probe_137()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_probe_137() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_probe_139
// with type: int ldv_probe_139()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_probe_139() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_probe_141
// with type: int ldv_probe_141()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_probe_141() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_probe_171
// with type: int ldv_probe_171()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_probe_171() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_probe_180
// with type: int ldv_probe_180()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_probe_180() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_probe_181
// with type: int ldv_probe_181()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_probe_181() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_probe_24
// with type: int ldv_probe_24()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_probe_24() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_probe_26
// with type: int ldv_probe_26()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_probe_26() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_probe_28
// with type: int ldv_probe_28()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_probe_28() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_probe_30
// with type: int ldv_probe_30()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_probe_30() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_probe_32
// with type: int ldv_probe_32()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_probe_32() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_probe_33
// with type: int ldv_probe_33()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_probe_33() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_probe_36
// with type: int ldv_probe_36()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_probe_36() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_probe_38
// with type: int ldv_probe_38()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_probe_38() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_probe_39
// with type: int ldv_probe_39()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_probe_39() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_probe_41
// with type: int ldv_probe_41()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_probe_41() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_probe_43
// with type: int ldv_probe_43()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_probe_43() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_probe_45
// with type: int ldv_probe_45()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_probe_45() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_probe_46
// with type: int ldv_probe_46()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_probe_46() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_probe_48
// with type: int ldv_probe_48()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_probe_48() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_probe_50
// with type: int ldv_probe_50()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_probe_50() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_probe_51
// with type: int ldv_probe_51()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_probe_51() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_probe_53
// with type: int ldv_probe_53()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_probe_53() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_probe_54
// with type: int ldv_probe_54()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_probe_54() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_probe_55
// with type: int ldv_probe_55()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_probe_55() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_probe_57
// with type: int ldv_probe_57()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_probe_57() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_probe_69
// with type: int ldv_probe_69()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_probe_69() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_probe_70
// with type: int ldv_probe_70()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_probe_70() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_probe_71
// with type: int ldv_probe_71()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_probe_71() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_release_171
// with type: int ldv_release_171()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_release_171() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_release_180
// with type: int ldv_release_180()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_release_180() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_release_181
// with type: int ldv_release_181()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_release_181() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_release_188
// with type: int ldv_release_188()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_release_188() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_release_46
// with type: int ldv_release_46()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_release_46() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_restore_noirq_191
// with type: int ldv_restore_noirq_191()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_restore_noirq_191() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_resume_noirq_191
// with type: int ldv_resume_noirq_191()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_resume_noirq_191() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_setup_59
// with type: int ldv_setup_59()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_setup_59() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_setup_60
// with type: int ldv_setup_60()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_setup_60() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_setup_61
// with type: int ldv_setup_61()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_setup_61() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_setup_62
// with type: int ldv_setup_62()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_setup_62() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_setup_63
// with type: int ldv_setup_63()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_setup_63() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_setup_64
// with type: int ldv_setup_64()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_setup_64() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_shutdown_187
// with type: int ldv_shutdown_187()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_shutdown_187() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_suspend_noirq_191
// with type: int ldv_suspend_noirq_191()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_suspend_noirq_191() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: ldv_thaw_noirq_191
// with type: int ldv_thaw_noirq_191()
// with return type: int
int __VERIFIER_nondet_int(void);
int ldv_thaw_noirq_191() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: list_del
// with type: void list_del(struct list_head *)
// with return type: void
void list_del(struct list_head *arg0) {
  // Void type
  return;
}

// Function: list_sort
// with type: void list_sort(void *, struct list_head *, int (*)(void *, struct list_head *, struct list_head *))
// with return type: void
void list_sort(void *arg0, struct list_head *arg1, int (*arg2)(void *, struct list_head *, struct list_head *)) {
  // Void type
  return;
}

// Function: lock_acquire
// with type: void lock_acquire(struct lockdep_map *, unsigned int, int, int, int, struct lockdep_map *, unsigned long)
// with return type: void
void lock_acquire(struct lockdep_map *arg0, unsigned int arg1, int arg2, int arg3, int arg4, struct lockdep_map *arg5, unsigned long arg6) {
  // Void type
  return;
}

// Function: lock_is_held
// with type: int lock_is_held(struct lockdep_map *)
// with return type: int
int __VERIFIER_nondet_int(void);
int lock_is_held(struct lockdep_map *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: lock_release
// with type: void lock_release(struct lockdep_map *, int, unsigned long)
// with return type: void
void lock_release(struct lockdep_map *arg0, int arg1, unsigned long arg2) {
  // Void type
  return;
}

// 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;
}

// Function: lockdep_rcu_suspicious
// with type: void lockdep_rcu_suspicious(const char *, const int, const char *)
// with return type: void
void lockdep_rcu_suspicious(const char *arg0, const int arg1, const char *arg2) {
  // Void type
  return;
}

// Skip function: malloc

// Function: mark_page_accessed
// with type: void mark_page_accessed(struct page *)
// with return type: void
void mark_page_accessed(struct page *arg0) {
  // Void type
  return;
}

// Skip function: memcmp

// Skip function: memcpy

// Skip function: memmove

// Skip function: memset

// Function: mipi_dsi_attach
// with type: int mipi_dsi_attach(struct mipi_dsi_device *)
// with return type: int
int __VERIFIER_nondet_int(void);
int mipi_dsi_attach(struct mipi_dsi_device *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: mipi_dsi_create_packet
// with type: int mipi_dsi_create_packet(struct mipi_dsi_packet *, const struct mipi_dsi_msg *)
// with return type: int
int __VERIFIER_nondet_int(void);
int mipi_dsi_create_packet(struct mipi_dsi_packet *arg0, const struct mipi_dsi_msg *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: mipi_dsi_dcs_write_buffer
// with type: ssize_t mipi_dsi_dcs_write_buffer(struct mipi_dsi_device *, const void *, size_t )
// with return type: ssize_t 
long __VERIFIER_nondet_long(void);
ssize_t mipi_dsi_dcs_write_buffer(struct mipi_dsi_device *arg0, const void *arg1, size_t arg2) {
  // Typedef type
  // Real type: __kernel_ssize_t 
  // Typedef type
  // Real type: __kernel_long_t 
  // Typedef type
  // Real type: long
  // Simple type
  return __VERIFIER_nondet_long();
}

// Function: mipi_dsi_generic_write
// with type: ssize_t mipi_dsi_generic_write(struct mipi_dsi_device *, const void *, size_t )
// with return type: ssize_t 
long __VERIFIER_nondet_long(void);
ssize_t mipi_dsi_generic_write(struct mipi_dsi_device *arg0, const void *arg1, size_t arg2) {
  // Typedef type
  // Real type: __kernel_ssize_t 
  // Typedef type
  // Real type: __kernel_long_t 
  // Typedef type
  // Real type: long
  // Simple type
  return __VERIFIER_nondet_long();
}

// Function: mmu_notifier_unregister
// with type: void mmu_notifier_unregister(struct mmu_notifier *, struct mm_struct *)
// with return type: void
void mmu_notifier_unregister(struct mmu_notifier *arg0, struct mm_struct *arg1) {
  // Void type
  return;
}

// Function: mod_delayed_work_on
// with type: bool mod_delayed_work_on(int, struct workqueue_struct *, struct delayed_work *, unsigned long)
// with return type: bool 
bool __VERIFIER_nondet_bool(void);
bool mod_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: mod_timer
// with type: int mod_timer(struct timer_list *, unsigned long)
// with return type: int
int __VERIFIER_nondet_int(void);
int mod_timer(struct timer_list *arg0, unsigned long arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: mod_timer_pinned
// with type: int mod_timer_pinned(struct timer_list *, unsigned long)
// with return type: int
int __VERIFIER_nondet_int(void);
int mod_timer_pinned(struct timer_list *arg0, unsigned long arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: msleep
// with type: void msleep(unsigned int)
// with return type: void
void msleep(unsigned int arg0) {
  // Void type
  return;
}

// Function: mutex_lock_interruptible_nested
// with type: int mutex_lock_interruptible_nested(struct mutex *, unsigned int)
// with return type: int
int __VERIFIER_nondet_int(void);
int mutex_lock_interruptible_nested(struct mutex *arg0, unsigned int arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// 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_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: noop_llseek
// with type: loff_t noop_llseek(struct file *, loff_t , int)
// with return type: loff_t 
long __VERIFIER_nondet_long(void);
loff_t noop_llseek(struct file *arg0, loff_t arg1, int arg2) {
  // Typedef type
  // Real type: __kernel_loff_t 
  // Typedef type
  // Real type: long long
  // Simple type
  return __VERIFIER_nondet_long();
}

// Function: nsecs_to_jiffies64
// with type: u64 nsecs_to_jiffies64(u64 )
// with return type: u64 
unsigned long __VERIFIER_nondet_ulong(void);
u64 nsecs_to_jiffies64(u64 arg0) {
  // Typedef type
  // Real type: unsigned long long
  // Simple type
  return __VERIFIER_nondet_ulong();
}

// Function: pci_bus_alloc_resource
// with type: int pci_bus_alloc_resource(struct pci_bus *, struct resource *, resource_size_t , resource_size_t , resource_size_t , unsigned long, resource_size_t (*)(void *, const struct resource *, resource_size_t , resource_size_t ), void *)
// with return type: int
int __VERIFIER_nondet_int(void);
int pci_bus_alloc_resource(struct pci_bus *arg0, struct resource *arg1, resource_size_t arg2, resource_size_t arg3, resource_size_t arg4, unsigned long arg5, resource_size_t (*arg6)(void *, const struct resource *, resource_size_t , resource_size_t ), void *arg7) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: pci_bus_read_config_byte
// with type: int pci_bus_read_config_byte(struct pci_bus *, unsigned int, int, u8 *)
// with return type: int
int __VERIFIER_nondet_int(void);
int pci_bus_read_config_byte(struct pci_bus *arg0, unsigned int arg1, int arg2, u8 *arg3) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: pci_bus_read_config_dword
// with type: int pci_bus_read_config_dword(struct pci_bus *, unsigned int, int, u32 *)
// with return type: int
int __VERIFIER_nondet_int(void);
int pci_bus_read_config_dword(struct pci_bus *arg0, unsigned int arg1, int arg2, u32 *arg3) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: pci_bus_read_config_word
// with type: int pci_bus_read_config_word(struct pci_bus *, unsigned int, int, u16 *)
// with return type: int
int __VERIFIER_nondet_int(void);
int pci_bus_read_config_word(struct pci_bus *arg0, unsigned int arg1, int arg2, u16 *arg3) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: pci_bus_write_config_byte
// with type: int pci_bus_write_config_byte(struct pci_bus *, unsigned int, int, u8 )
// with return type: int
int __VERIFIER_nondet_int(void);
int pci_bus_write_config_byte(struct pci_bus *arg0, unsigned int arg1, int arg2, u8 arg3) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: pci_bus_write_config_dword
// with type: int pci_bus_write_config_dword(struct pci_bus *, unsigned int, int, u32 )
// with return type: int
int __VERIFIER_nondet_int(void);
int pci_bus_write_config_dword(struct pci_bus *arg0, unsigned int arg1, int arg2, u32 arg3) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: pci_bus_write_config_word
// with type: int pci_bus_write_config_word(struct pci_bus *, unsigned int, int, u16 )
// with return type: int
int __VERIFIER_nondet_int(void);
int pci_bus_write_config_word(struct pci_bus *arg0, unsigned int arg1, int arg2, u16 arg3) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: pci_dev_put
// with type: void pci_dev_put(struct pci_dev *)
// with return type: void
void pci_dev_put(struct pci_dev *arg0) {
  // Void type
  return;
}

// Function: pci_disable_device
// with type: void pci_disable_device(struct pci_dev *)
// with return type: void
void pci_disable_device(struct pci_dev *arg0) {
  // Void type
  return;
}

// Function: pci_disable_msi
// with type: void pci_disable_msi(struct pci_dev *)
// with return type: void
void pci_disable_msi(struct pci_dev *arg0) {
  // Void type
  return;
}

// Function: pci_enable_device
// with type: int pci_enable_device(struct pci_dev *)
// with return type: int
int __VERIFIER_nondet_int(void);
int pci_enable_device(struct pci_dev *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: pci_enable_msi_range
// with type: int pci_enable_msi_range(struct pci_dev *, int, int)
// with return type: int
int __VERIFIER_nondet_int(void);
int pci_enable_msi_range(struct pci_dev *arg0, int arg1, int arg2) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: pci_get_class
// with type: struct pci_dev *pci_get_class(unsigned int, struct pci_dev *)
// with return type: (struct pci_dev)*
struct pci_dev *pci_get_class(unsigned int arg0, struct pci_dev *arg1) {
  // Pointer type
  return ldv_malloc(sizeof(struct pci_dev));
}

// Function: pci_get_domain_bus_and_slot
// with type: struct pci_dev *pci_get_domain_bus_and_slot(int, unsigned int, unsigned int)
// with return type: (struct pci_dev)*
struct pci_dev *pci_get_domain_bus_and_slot(int arg0, unsigned int arg1, unsigned int arg2) {
  // Pointer type
  return ldv_malloc(sizeof(struct pci_dev));
}

// Function: pci_iomap
// with type: void *pci_iomap(struct pci_dev *, int, unsigned long)
// with return type: (void)*
void *pci_iomap(struct pci_dev *arg0, int arg1, unsigned long arg2) {
  // Pointer type
  return ldv_malloc(arg2);
}

// Function: pci_iounmap
// with type: void pci_iounmap(struct pci_dev *, void *)
// with return type: void
void pci_iounmap(struct pci_dev *arg0, void *arg1) {
  // Void type
  return;
}

// Function: pci_map_rom
// with type: void *pci_map_rom(struct pci_dev *, size_t *)
// with return type: (void)*
void *pci_map_rom(struct pci_dev *arg0, size_t *arg1) {
  // Pointer type
  return ldv_malloc(0UL);
}

// Function: pci_save_state
// with type: int pci_save_state(struct pci_dev *)
// with return type: int
int __VERIFIER_nondet_int(void);
int pci_save_state(struct pci_dev *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: pci_set_master
// with type: void pci_set_master(struct pci_dev *)
// with return type: void
void pci_set_master(struct pci_dev *arg0) {
  // Void type
  return;
}

// Function: pci_set_power_state
// with type: int pci_set_power_state(struct pci_dev *, pci_power_t )
// with return type: int
int __VERIFIER_nondet_int(void);
int pci_set_power_state(struct pci_dev *arg0, pci_power_t arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: pci_unmap_rom
// with type: void pci_unmap_rom(struct pci_dev *, void *)
// with return type: void
void pci_unmap_rom(struct pci_dev *arg0, void *arg1) {
  // Void type
  return;
}

// Function: pgprot_writecombine
// with type: pgprot_t pgprot_writecombine(pgprot_t )
// with return type: pgprot_t 
pgprot_t pgprot_writecombine(pgprot_t arg0) {
  // Typedef type
  // Real type: struct pgprot
  // Composite type
  return *(struct pgprot *)ldv_xmalloc(sizeof(struct pgprot));
}

// Function: pid_task
// with type: struct task_struct *pid_task(struct pid *, enum pid_type )
// with return type: (struct task_struct)*
struct task_struct *pid_task(struct pid *arg0, enum pid_type arg1) {
  // Pointer type
  return ldv_malloc(sizeof(struct task_struct));
}

// Function: pm_qos_add_request
// with type: void pm_qos_add_request(struct pm_qos_request *, int, s32 )
// with return type: void
void pm_qos_add_request(struct pm_qos_request *arg0, int arg1, s32 arg2) {
  // Void type
  return;
}

// Function: pm_qos_remove_request
// with type: void pm_qos_remove_request(struct pm_qos_request *)
// with return type: void
void pm_qos_remove_request(struct pm_qos_request *arg0) {
  // Void type
  return;
}

// Function: pm_qos_update_request
// with type: void pm_qos_update_request(struct pm_qos_request *, s32 )
// with return type: void
void pm_qos_update_request(struct pm_qos_request *arg0, s32 arg1) {
  // Void type
  return;
}

// Function: pm_runtime_set_autosuspend_delay
// with type: void pm_runtime_set_autosuspend_delay(struct device *, int)
// with return type: void
void pm_runtime_set_autosuspend_delay(struct device *arg0, int arg1) {
  // Void type
  return;
}

// Function: pnp_range_reserved
// with type: int pnp_range_reserved(resource_size_t , resource_size_t )
// with return type: int
int __VERIFIER_nondet_int(void);
int pnp_range_reserved(resource_size_t arg0, resource_size_t arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// 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: 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: put_page
// with type: void put_page(struct page *)
// with return type: void
void put_page(struct page *arg0) {
  // Void type
  return;
}

// Function: put_pid
// with type: void put_pid(struct pid *)
// with return type: void
void put_pid(struct pid *arg0) {
  // Void type
  return;
}

// 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: rcu_is_watching
// with type: bool rcu_is_watching()
// with return type: bool 
bool __VERIFIER_nondet_bool(void);
bool rcu_is_watching() {
  // Typedef type
  // Real type: _Bool
  // Simple type
  return __VERIFIER_nondet_bool();
}

// Function: rcu_lockdep_current_cpu_online
// with type: bool rcu_lockdep_current_cpu_online()
// with return type: bool 
bool __VERIFIER_nondet_bool(void);
bool rcu_lockdep_current_cpu_online() {
  // Typedef type
  // Real type: _Bool
  // Simple type
  return __VERIFIER_nondet_bool();
}

// Function: register_acpi_notifier
// with type: int register_acpi_notifier(struct notifier_block *)
// with return type: int
int __VERIFIER_nondet_int(void);
int register_acpi_notifier(struct notifier_block *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: register_oom_notifier
// with type: int register_oom_notifier(struct notifier_block *)
// with return type: int
int __VERIFIER_nondet_int(void);
int register_oom_notifier(struct notifier_block *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: register_reboot_notifier
// with type: int register_reboot_notifier(struct notifier_block *)
// with return type: int
int __VERIFIER_nondet_int(void);
int register_reboot_notifier(struct notifier_block *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: register_shrinker
// with type: int register_shrinker(struct shrinker *)
// with return type: int
int __VERIFIER_nondet_int(void);
int register_shrinker(struct shrinker *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// 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: release_pages
// with type: void release_pages(struct page **, int, bool )
// with return type: void
void release_pages(struct page **arg0, int arg1, bool arg2) {
  // Void type
  return;
}

// Function: release_resource
// with type: int release_resource(struct resource *)
// with return type: int
int __VERIFIER_nondet_int(void);
int release_resource(struct resource *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: remove_conflicting_framebuffers
// with type: int remove_conflicting_framebuffers(struct apertures_struct *, const char *, bool )
// with return type: int
int __VERIFIER_nondet_int(void);
int remove_conflicting_framebuffers(struct apertures_struct *arg0, const char *arg1, bool arg2) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: request_firmware_nowait
// with type: int request_firmware_nowait(struct module *, bool , const char *, struct device *, gfp_t , void *, void (*)(const struct firmware *, void *))
// with return type: int
int __VERIFIER_nondet_int(void);
int request_firmware_nowait(struct module *arg0, bool arg1, const char *arg2, struct device *arg3, gfp_t arg4, void *arg5, void (*arg6)(const struct firmware *, void *)) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: round_jiffies_up_relative
// with type: unsigned long int round_jiffies_up_relative(unsigned long)
// with return type: unsigned long int
unsigned long __VERIFIER_nondet_ulong(void);
unsigned long int round_jiffies_up_relative(unsigned long arg0) {
  // Simple type
  return __VERIFIER_nondet_ulong();
}

// Function: schedule
// with type: void schedule()
// with return type: void
void schedule() {
  // Void type
  return;
}

// 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: schedule_timeout_killable
// with type: long int schedule_timeout_killable(long)
// with return type: long int
long __VERIFIER_nondet_long(void);
long int schedule_timeout_killable(long arg0) {
  // Simple type
  return __VERIFIER_nondet_long();
}

// Function: schedule_timeout_uninterruptible
// with type: long int schedule_timeout_uninterruptible(long)
// with return type: long int
long __VERIFIER_nondet_long(void);
long int schedule_timeout_uninterruptible(long arg0) {
  // Simple type
  return __VERIFIER_nondet_long();
}

// Function: scnprintf
// with type: int scnprintf(char *, size_t , const char *, ...)
// with return type: int
int __VERIFIER_nondet_int(void);
int scnprintf(char *arg0, size_t arg1, const char *arg2, ...) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: seq_lseek
// with type: loff_t seq_lseek(struct file *, loff_t , int)
// with return type: loff_t 
long __VERIFIER_nondet_long(void);
loff_t seq_lseek(struct file *arg0, loff_t arg1, int arg2) {
  // Typedef type
  // Real type: __kernel_loff_t 
  // Typedef type
  // Real type: long long
  // Simple type
  return __VERIFIER_nondet_long();
}

// Function: seq_printf
// with type: int seq_printf(struct seq_file *, const char *, ...)
// with return type: int
int __VERIFIER_nondet_int(void);
int seq_printf(struct seq_file *arg0, const char *arg1, ...) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: seq_putc
// with type: int seq_putc(struct seq_file *, char)
// with return type: int
int __VERIFIER_nondet_int(void);
int seq_putc(struct seq_file *arg0, char arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: seq_puts
// with type: int seq_puts(struct seq_file *, const char *)
// with return type: int
int __VERIFIER_nondet_int(void);
int seq_puts(struct seq_file *arg0, const char *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: seq_read
// with type: ssize_t seq_read(struct file *, char *, size_t , loff_t *)
// with return type: ssize_t 
long __VERIFIER_nondet_long(void);
ssize_t seq_read(struct file *arg0, char *arg1, size_t arg2, loff_t *arg3) {
  // Typedef type
  // Real type: __kernel_ssize_t 
  // Typedef type
  // Real type: __kernel_long_t 
  // Typedef type
  // Real type: long
  // Simple type
  return __VERIFIER_nondet_long();
}

// Function: seq_write
// with type: int seq_write(struct seq_file *, const void *, size_t )
// with return type: int
int __VERIFIER_nondet_int(void);
int seq_write(struct seq_file *arg0, const void *arg1, size_t arg2) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: set_page_dirty
// with type: int set_page_dirty(struct page *)
// with return type: int
int __VERIFIER_nondet_int(void);
int set_page_dirty(struct page *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: set_pages_uc
// with type: int set_pages_uc(struct page *, int)
// with return type: int
int __VERIFIER_nondet_int(void);
int set_pages_uc(struct page *arg0, int arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: set_pages_wb
// with type: int set_pages_wb(struct page *, int)
// with return type: int
int __VERIFIER_nondet_int(void);
int set_pages_wb(struct page *arg0, int arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: sg_alloc_table
// with type: int sg_alloc_table(struct sg_table *, unsigned int, gfp_t )
// with return type: int
int __VERIFIER_nondet_int(void);
int sg_alloc_table(struct sg_table *arg0, unsigned int arg1, gfp_t arg2) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: sg_alloc_table_from_pages
// with type: int sg_alloc_table_from_pages(struct sg_table *, struct page **, unsigned int, unsigned long, unsigned long, gfp_t )
// with return type: int
int __VERIFIER_nondet_int(void);
int sg_alloc_table_from_pages(struct sg_table *arg0, struct page **arg1, unsigned int arg2, unsigned long arg3, unsigned long arg4, gfp_t arg5) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: sg_free_table
// with type: void sg_free_table(struct sg_table *)
// with return type: void
void sg_free_table(struct sg_table *arg0) {
  // Void type
  return;
}

// Function: sg_next
// with type: struct scatterlist *sg_next(struct scatterlist *)
// with return type: (struct scatterlist)*
struct scatterlist *sg_next(struct scatterlist *arg0) {
  // Pointer type
  return ldv_malloc(sizeof(struct scatterlist));
}

// Function: shmem_read_mapping_page_gfp
// with type: struct page *shmem_read_mapping_page_gfp(struct address_space *, unsigned long, gfp_t )
// with return type: (struct page)*
struct page *shmem_read_mapping_page_gfp(struct address_space *arg0, unsigned long arg1, gfp_t arg2) {
  // Pointer type
  return ldv_malloc(sizeof(struct page));
}

// Function: shmem_truncate_range
// with type: void shmem_truncate_range(struct inode *, loff_t , loff_t )
// with return type: void
void shmem_truncate_range(struct inode *arg0, loff_t arg1, loff_t arg2) {
  // Void type
  return;
}

// Function: simple_attr_open
// with type: int simple_attr_open(struct inode *, struct file *, int (*)(void *, u64 *), int (*)(void *, u64 ), const char *)
// with return type: int
int __VERIFIER_nondet_int(void);
int simple_attr_open(struct inode *arg0, struct file *arg1, int (*arg2)(void *, u64 *), int (*arg3)(void *, u64 ), const char *arg4) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: simple_attr_read
// with type: ssize_t simple_attr_read(struct file *, char *, size_t , loff_t *)
// with return type: ssize_t 
long __VERIFIER_nondet_long(void);
ssize_t simple_attr_read(struct file *arg0, char *arg1, size_t arg2, loff_t *arg3) {
  // Typedef type
  // Real type: __kernel_ssize_t 
  // Typedef type
  // Real type: __kernel_long_t 
  // Typedef type
  // Real type: long
  // Simple type
  return __VERIFIER_nondet_long();
}

// Function: simple_attr_release
// with type: int simple_attr_release(struct inode *, struct file *)
// with return type: int
int __VERIFIER_nondet_int(void);
int simple_attr_release(struct inode *arg0, struct file *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: simple_attr_write
// with type: ssize_t simple_attr_write(struct file *, const char *, size_t , loff_t *)
// with return type: ssize_t 
long __VERIFIER_nondet_long(void);
ssize_t simple_attr_write(struct file *arg0, const char *arg1, size_t arg2, loff_t *arg3) {
  // Typedef type
  // Real type: __kernel_ssize_t 
  // Typedef type
  // Real type: __kernel_long_t 
  // Typedef type
  // Real type: long
  // Simple type
  return __VERIFIER_nondet_long();
}

// Function: simple_read_from_buffer
// with type: ssize_t simple_read_from_buffer(void *, size_t , loff_t *, const void *, size_t )
// with return type: ssize_t 
long __VERIFIER_nondet_long(void);
ssize_t simple_read_from_buffer(void *arg0, size_t arg1, loff_t *arg2, const void *arg3, size_t arg4) {
  // Typedef type
  // Real type: __kernel_ssize_t 
  // Typedef type
  // Real type: __kernel_long_t 
  // Typedef type
  // Real type: long
  // Simple type
  return __VERIFIER_nondet_long();
}

// Function: single_open
// with type: int single_open(struct file *, int (*)(struct seq_file *, void *), void *)
// with return type: int
int __VERIFIER_nondet_int(void);
int single_open(struct file *arg0, int (*arg1)(struct seq_file *, void *), void *arg2) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: single_release
// with type: int single_release(struct inode *, struct file *)
// with return type: int
int __VERIFIER_nondet_int(void);
int single_release(struct inode *arg0, struct file *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: skip_spaces
// with type: char *skip_spaces(const char *)
// with return type: (char)*
char *skip_spaces(const char *arg0) {
  // Pointer type
  return ldv_malloc(sizeof(char));
}

// Skip function: snprintf

// Skip function: sscanf

// Skip function: strcmp

// Skip function: strcpy

// Skip function: strlen

// Skip function: strncpy

// Function: swiotlb_nr_tbl
// with type: unsigned long int swiotlb_nr_tbl()
// with return type: unsigned long int
unsigned long __VERIFIER_nondet_ulong(void);
unsigned long int swiotlb_nr_tbl() {
  // Simple type
  return __VERIFIER_nondet_ulong();
}

// Function: synchronize_irq
// with type: void synchronize_irq(unsigned int)
// with return type: void
void synchronize_irq(unsigned int arg0) {
  // Void type
  return;
}

// Function: sysfs_create_bin_file
// with type: int sysfs_create_bin_file(struct kobject *, const struct bin_attribute *)
// with return type: int
int __VERIFIER_nondet_int(void);
int sysfs_create_bin_file(struct kobject *arg0, const struct bin_attribute *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: sysfs_create_files
// with type: int sysfs_create_files(struct kobject *, const struct attribute **)
// with return type: int
int __VERIFIER_nondet_int(void);
int sysfs_create_files(struct kobject *arg0, const struct attribute **arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: sysfs_create_link
// with type: int sysfs_create_link(struct kobject *, struct kobject *, const char *)
// with return type: int
int __VERIFIER_nondet_int(void);
int sysfs_create_link(struct kobject *arg0, struct kobject *arg1, const char *arg2) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: sysfs_merge_group
// with type: int sysfs_merge_group(struct kobject *, const struct attribute_group *)
// with return type: int
int __VERIFIER_nondet_int(void);
int sysfs_merge_group(struct kobject *arg0, const struct attribute_group *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: sysfs_remove_bin_file
// with type: void sysfs_remove_bin_file(struct kobject *, const struct bin_attribute *)
// with return type: void
void sysfs_remove_bin_file(struct kobject *arg0, const struct bin_attribute *arg1) {
  // Void type
  return;
}

// Function: sysfs_remove_files
// with type: void sysfs_remove_files(struct kobject *, const struct attribute **)
// with return type: void
void sysfs_remove_files(struct kobject *arg0, const struct attribute **arg1) {
  // Void type
  return;
}

// Function: sysfs_remove_link
// with type: void sysfs_remove_link(struct kobject *, const char *)
// with return type: void
void sysfs_remove_link(struct kobject *arg0, const char *arg1) {
  // Void type
  return;
}

// Function: sysfs_unmerge_group
// with type: void sysfs_unmerge_group(struct kobject *, const struct attribute_group *)
// with return type: void
void sysfs_unmerge_group(struct kobject *arg0, const struct attribute_group *arg1) {
  // Void type
  return;
}

// Function: trace_define_field
// with type: int trace_define_field(struct trace_event_call *, const char *, const char *, int, int, int, int)
// with return type: int
int __VERIFIER_nondet_int(void);
int trace_define_field(struct trace_event_call *arg0, const char *arg1, const char *arg2, int arg3, int arg4, int arg5, int arg6) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: trace_event_raw_init
// with type: int trace_event_raw_init(struct trace_event_call *)
// with return type: int
int __VERIFIER_nondet_int(void);
int trace_event_raw_init(struct trace_event_call *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: trace_event_reg
// with type: int trace_event_reg(struct trace_event_call *, enum trace_reg , void *)
// with return type: int
int __VERIFIER_nondet_int(void);
int trace_event_reg(struct trace_event_call *arg0, enum trace_reg arg1, void *arg2) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: trace_hardirqs_off
// with type: void trace_hardirqs_off()
// with return type: void
void trace_hardirqs_off() {
  // Void type
  return;
}

// Function: trace_hardirqs_on
// with type: void trace_hardirqs_on()
// with return type: void
void trace_hardirqs_on() {
  // Void type
  return;
}

// Function: trace_raw_output_prep
// with type: int trace_raw_output_prep(struct trace_iterator *, struct trace_event *)
// with return type: int
int __VERIFIER_nondet_int(void);
int trace_raw_output_prep(struct trace_iterator *arg0, struct trace_event *arg1) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: trace_seq_printf
// with type: void trace_seq_printf(struct trace_seq *, const char *, ...)
// with return type: void
void trace_seq_printf(struct trace_seq *arg0, const char *arg1, ...) {
  // Void type
  return;
}

// Function: unmap_mapping_range
// with type: void unmap_mapping_range(struct address_space *, const loff_t , const loff_t , int)
// with return type: void
void unmap_mapping_range(struct address_space *arg0, const loff_t arg1, const loff_t arg2, int arg3) {
  // Void type
  return;
}

// Function: unregister_acpi_notifier
// with type: int unregister_acpi_notifier(struct notifier_block *)
// with return type: int
int __VERIFIER_nondet_int(void);
int unregister_acpi_notifier(struct notifier_block *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: unregister_framebuffer
// with type: int unregister_framebuffer(struct fb_info *)
// with return type: int
int __VERIFIER_nondet_int(void);
int unregister_framebuffer(struct fb_info *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: unregister_oom_notifier
// with type: int unregister_oom_notifier(struct notifier_block *)
// with return type: int
int __VERIFIER_nondet_int(void);
int unregister_oom_notifier(struct notifier_block *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: unregister_reboot_notifier
// with type: int unregister_reboot_notifier(struct notifier_block *)
// with return type: int
int __VERIFIER_nondet_int(void);
int unregister_reboot_notifier(struct notifier_block *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: unregister_shrinker
// with type: void unregister_shrinker(struct shrinker *)
// with return type: void
void unregister_shrinker(struct shrinker *arg0) {
  // Void type
  return;
}

// Function: up_read
// with type: void up_read(struct rw_semaphore *)
// with return type: void
void up_read(struct rw_semaphore *arg0) {
  // Void type
  return;
}

// Function: up_write
// with type: void up_write(struct rw_semaphore *)
// with return type: void
void up_write(struct rw_semaphore *arg0) {
  // Void type
  return;
}

// Function: usleep_range
// with type: void usleep_range(unsigned long, unsigned long)
// with return type: void
void usleep_range(unsigned long arg0, unsigned long arg1) {
  // Void type
  return;
}

// Function: vga_client_register
// with type: int vga_client_register(struct pci_dev *, void *, void (*)(void *, bool ), unsigned int (*)(void *, bool ))
// with return type: int
int __VERIFIER_nondet_int(void);
int vga_client_register(struct pci_dev *arg0, void *arg1, void (*arg2)(void *, bool ), unsigned int (*arg3)(void *, bool )) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: vga_get
// with type: int vga_get(struct pci_dev *, unsigned int, int)
// with return type: int
int __VERIFIER_nondet_int(void);
int vga_get(struct pci_dev *arg0, unsigned int arg1, int arg2) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: vga_put
// with type: void vga_put(struct pci_dev *, unsigned int)
// with return type: void
void vga_put(struct pci_dev *arg0, unsigned int arg1) {
  // Void type
  return;
}

// Function: vga_switcheroo_client_fb_set
// with type: void vga_switcheroo_client_fb_set(struct pci_dev *, struct fb_info *)
// with return type: void
void vga_switcheroo_client_fb_set(struct pci_dev *arg0, struct fb_info *arg1) {
  // Void type
  return;
}

// Function: vga_switcheroo_process_delayed_switch
// with type: int vga_switcheroo_process_delayed_switch()
// with return type: int
int __VERIFIER_nondet_int(void);
int vga_switcheroo_process_delayed_switch() {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: vga_switcheroo_register_client
// with type: int vga_switcheroo_register_client(struct pci_dev *, const struct vga_switcheroo_client_ops *, bool )
// with return type: int
int __VERIFIER_nondet_int(void);
int vga_switcheroo_register_client(struct pci_dev *arg0, const struct vga_switcheroo_client_ops *arg1, bool arg2) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: vga_switcheroo_unregister_client
// with type: void vga_switcheroo_unregister_client(struct pci_dev *)
// with return type: void
void vga_switcheroo_unregister_client(struct pci_dev *arg0) {
  // Void type
  return;
}

// Function: vgacon_text_force
// with type: bool vgacon_text_force()
// with return type: bool 
bool __VERIFIER_nondet_bool(void);
bool vgacon_text_force() {
  // Typedef type
  // Real type: _Bool
  // Simple type
  return __VERIFIER_nondet_bool();
}

// Function: vm_get_page_prot
// with type: pgprot_t vm_get_page_prot(unsigned long)
// with return type: pgprot_t 
pgprot_t vm_get_page_prot(unsigned long arg0) {
  // Typedef type
  // Real type: struct pgprot
  // Composite type
  return *(struct pgprot *)ldv_xmalloc(sizeof(struct pgprot));
}

// Function: vm_insert_pfn
// with type: int vm_insert_pfn(struct vm_area_struct *, unsigned long, unsigned long)
// with return type: int
int __VERIFIER_nondet_int(void);
int vm_insert_pfn(struct vm_area_struct *arg0, unsigned long arg1, unsigned long arg2) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Function: vm_mmap
// with type: unsigned long int vm_mmap(struct file *, unsigned long, unsigned long, unsigned long, unsigned long, unsigned long)
// with return type: unsigned long int
unsigned long __VERIFIER_nondet_ulong(void);
unsigned long int vm_mmap(struct file *arg0, unsigned long arg1, unsigned long arg2, unsigned long arg3, unsigned long arg4, unsigned long arg5) {
  // Simple type
  return __VERIFIER_nondet_ulong();
}

// Function: vmap
// with type: void *vmap(struct page **, unsigned int, unsigned long, pgprot_t )
// with return type: (void)*
void *vmap(struct page **arg0, unsigned int arg1, unsigned long arg2, pgprot_t arg3) {
  // Pointer type
  return ldv_malloc(0UL);
}

// Function: vscnprintf
// with type: int vscnprintf(char *, size_t , const char *, va_list *)
// with return type: int
int __VERIFIER_nondet_int(void);
int vscnprintf(char *arg0, size_t arg1, const char *arg2, va_list *arg3) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// Skip function: vsnprintf

// Function: vunmap
// with type: void vunmap(const void *)
// with return type: void
void vunmap(const void *arg0) {
  // Void type
  return;
}

// Function: wake_up_process
// with type: int wake_up_process(struct task_struct *)
// with return type: int
int __VERIFIER_nondet_int(void);
int wake_up_process(struct task_struct *arg0) {
  // Simple type
  return __VERIFIER_nondet_int();
}

// 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;
}

// Function: warn_slowpath_null
// with type: void warn_slowpath_null(const char *, const int)
// with return type: void
void warn_slowpath_null(const char *arg0, const int arg1) {
  // Void type
  return;
}

// Function: work_busy
// with type: unsigned int work_busy(struct work_struct *)
// with return type: unsigned int
unsigned int __VERIFIER_nondet_uint(void);
unsigned int work_busy(struct work_struct *arg0) {
  // Simple type
  return __VERIFIER_nondet_uint();
}

// 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();
}