// RUN: %sea --mem=-1 -m64 pf --step=large -g --horn-global-constraints=true --track=mem --horn-stats --enable-nondet-init --strip-extern --externalize-addr-taken-functions --horn-singleton-aliases=true --devirt-functions --horn-ignore-calloc=false --enable-indvar --enable-loop-idiom --horn-make-undef-warning-error=false --inline "%s"
// CHECK: ^unsat$

extern void __VERIFIER_error() __attribute__ ((__noreturn__));

/* Generated by CIL v. 1.5.1 */
/* print_CIL_Input is false */

#line 20 "include/asm-generic/int-ll64.h"
typedef unsigned char __u8;
#line 23 "include/asm-generic/int-ll64.h"
typedef unsigned short __u16;
#line 26 "include/asm-generic/int-ll64.h"
typedef unsigned int __u32;
#line 30 "include/asm-generic/int-ll64.h"
typedef unsigned long long __u64;
#line 43 "include/asm-generic/int-ll64.h"
typedef unsigned char u8;
#line 46 "include/asm-generic/int-ll64.h"
typedef unsigned short u16;
#line 49 "include/asm-generic/int-ll64.h"
typedef unsigned int u32;
#line 51 "include/asm-generic/int-ll64.h"
typedef long long s64;
#line 52 "include/asm-generic/int-ll64.h"
typedef unsigned long long u64;
#line 23 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/inst/current/envs/linux-stable-af3071a/linux-stable-af3071a/arch/arm/include/asm/posix_types.h"
typedef unsigned short __kernel_mode_t;
#line 30 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/inst/current/envs/linux-stable-af3071a/linux-stable-af3071a/arch/arm/include/asm/posix_types.h"
typedef unsigned int __kernel_size_t;
#line 31 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/inst/current/envs/linux-stable-af3071a/linux-stable-af3071a/arch/arm/include/asm/posix_types.h"
typedef int __kernel_ssize_t;
#line 33 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/inst/current/envs/linux-stable-af3071a/linux-stable-af3071a/arch/arm/include/asm/posix_types.h"
typedef long __kernel_time_t;
#line 37 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/inst/current/envs/linux-stable-af3071a/linux-stable-af3071a/arch/arm/include/asm/posix_types.h"
typedef int __kernel_clockid_t;
#line 50 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/inst/current/envs/linux-stable-af3071a/linux-stable-af3071a/arch/arm/include/asm/posix_types.h"
typedef long long __kernel_loff_t;
#line 21 "include/linux/types.h"
typedef __u32 __kernel_dev_t;
#line 24 "include/linux/types.h"
typedef __kernel_dev_t dev_t;
#line 26 "include/linux/types.h"
typedef __kernel_mode_t mode_t;
#line 34 "include/linux/types.h"
typedef __kernel_clockid_t clockid_t;
#line 37 "include/linux/types.h"
typedef _Bool bool;
#line 53 "include/linux/types.h"
typedef __kernel_loff_t loff_t;
#line 62 "include/linux/types.h"
typedef __kernel_size_t size_t;
#line 67 "include/linux/types.h"
typedef __kernel_ssize_t ssize_t;
#line 201 "include/linux/types.h"
typedef unsigned int gfp_t;
#line 207 "include/linux/types.h"
typedef u32 phys_addr_t;
#line 210 "include/linux/types.h"
typedef phys_addr_t resource_size_t;
#line 214 "include/linux/types.h"
struct __anonstruct_atomic_t_6 {
   int counter ;
};
#line 214 "include/linux/types.h"
typedef struct __anonstruct_atomic_t_6 atomic_t;
#line 215 "include/linux/types.h"
struct list_head {
   struct list_head *next ;
   struct list_head *prev ;
};
#line 240 "include/linux/types.h"
struct resource {
   resource_size_t start ;
   resource_size_t end ;
   char const   *name ;
   unsigned long flags ;
   struct resource *parent ;
   struct resource *sibling ;
   struct resource *child ;
};
#line 175 "include/linux/ioport.h"
struct device;
#line 199
struct task_struct;
#line 663 "include/linux/list.h"
struct lockdep_map;
#line 101 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/inst/current/envs/linux-stable-af3071a/linux-stable-af3071a/arch/arm/include/asm/outercache.h"
struct thread_info;
#line 293 "include/linux/printk.h"
struct module;
#line 70 "include/asm-generic/bug.h"
struct completion;
#line 141 "include/asm-generic/atomic-long.h"
typedef atomic_t atomic_long_t;
#line 55 "include/linux/debug_locks.h"
struct stack_trace {
   unsigned int nr_entries ;
   unsigned int max_entries ;
   unsigned long *entries ;
   int skip ;
};
#line 23 "include/linux/stacktrace.h"
struct lockdep_subclass_key {
   char __one_byte ;
};
#line 53 "include/linux/lockdep.h"
struct lock_class_key {
   struct lockdep_subclass_key subkeys[8U] ;
};
#line 59 "include/linux/lockdep.h"
struct lock_class {
   struct list_head hash_entry ;
   struct list_head lock_entry ;
   struct lockdep_subclass_key *key ;
   unsigned int subclass ;
   unsigned int dep_gen_id ;
   unsigned long usage_mask ;
   struct stack_trace usage_traces[13U] ;
   struct list_head locks_after ;
   struct list_head locks_before ;
   unsigned int version ;
   unsigned long ops ;
   char const   *name ;
   int name_version ;
   unsigned long contention_point[4U] ;
   unsigned long contending_point[4U] ;
};
#line 144 "include/linux/lockdep.h"
struct lockdep_map {
   struct lock_class_key *key ;
   struct lock_class *class_cache[2U] ;
   char const   *name ;
   int cpu ;
   unsigned long ip ;
};
#line 549
struct sock;
#line 550
struct kobject;
#line 551
enum kobj_ns_type {
    KOBJ_NS_TYPE_NONE = 0,
    KOBJ_NS_TYPE_NET = 1,
    KOBJ_NS_TYPES = 2
} ;
#line 557 "include/linux/lockdep.h"
struct kobj_ns_type_operations {
   enum kobj_ns_type type ;
   void const   *(*current_ns)(void) ;
   void const   *(*netlink_ns)(struct sock * ) ;
   void const   *(*initial_ns)(void) ;
};
#line 55 "include/linux/kobject_ns.h"
struct attribute {
   char const   *name ;
   mode_t mode ;
   struct lock_class_key *key ;
   struct lock_class_key skey ;
};
#line 33 "include/linux/sysfs.h"
struct attribute_group {
   char const   *name ;
   mode_t (*is_visible)(struct kobject * , struct attribute * , int  ) ;
   struct attribute **attrs ;
};
#line 62
struct file;
#line 63
struct vm_area_struct;
#line 64 "include/linux/sysfs.h"
struct bin_attribute {
   struct attribute attr ;
   size_t size ;
   void *private ;
   ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
                   loff_t  , size_t  ) ;
   ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
                    loff_t  , size_t  ) ;
   int (*mmap)(struct file * , struct kobject * , struct bin_attribute * , struct vm_area_struct * ) ;
};
#line 98 "include/linux/sysfs.h"
struct sysfs_ops {
   ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
   ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
};
#line 116
struct sysfs_dirent;
#line 185
struct timespec;
#line 187 "include/linux/sysfs.h"
struct __anonstruct_futex_9 {
   u32 *uaddr ;
   u32 val ;
   u32 flags ;
   u32 bitset ;
   u64 time ;
   u32 *uaddr2 ;
};
#line 187 "include/linux/sysfs.h"
struct __anonstruct_nanosleep_10 {
   clockid_t index ;
   struct timespec *rmtp ;
   u64 expires ;
};
#line 187
struct pollfd;
#line 187 "include/linux/sysfs.h"
struct __anonstruct_poll_11 {
   struct pollfd *ufds ;
   int nfds ;
   int has_timeout ;
   unsigned long tv_sec ;
   unsigned long tv_nsec ;
};
#line 187 "include/linux/sysfs.h"
union __anonunion_ldv_2937_8 {
   struct __anonstruct_futex_9 futex ;
   struct __anonstruct_nanosleep_10 nanosleep ;
   struct __anonstruct_poll_11 poll ;
};
#line 187 "include/linux/sysfs.h"
struct restart_block {
   long (*fn)(struct restart_block * ) ;
   union __anonunion_ldv_2937_8 ldv_2937 ;
};
#line 51 "include/linux/thread_info.h"
struct vfp_hard_struct {
   __u64 fpregs[16U] ;
   __u32 fpexc ;
   __u32 fpscr ;
   __u32 fpinst ;
   __u32 fpinst2 ;
};
#line 43 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/inst/current/envs/linux-stable-af3071a/linux-stable-af3071a/arch/arm/include/asm/fpstate.h"
union vfp_state {
   struct vfp_hard_struct hard ;
};
#line 54 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/inst/current/envs/linux-stable-af3071a/linux-stable-af3071a/arch/arm/include/asm/fpstate.h"
struct fp_hard_struct {
   unsigned int save[35U] ;
};
#line 60 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/inst/current/envs/linux-stable-af3071a/linux-stable-af3071a/arch/arm/include/asm/fpstate.h"
struct fp_soft_struct {
   unsigned int save[35U] ;
};
#line 72 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/inst/current/envs/linux-stable-af3071a/linux-stable-af3071a/arch/arm/include/asm/fpstate.h"
union fp_state {
   struct fp_hard_struct hard ;
   struct fp_soft_struct soft ;
};
#line 77 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/inst/current/envs/linux-stable-af3071a/linux-stable-af3071a/arch/arm/include/asm/fpstate.h"
struct crunch_state {
   unsigned int mvdx[16U][2U] ;
   unsigned int mvax[4U][3U] ;
   unsigned int dspsc[2U] ;
};
#line 88
struct exec_domain;
#line 30 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/inst/current/envs/linux-stable-af3071a/linux-stable-af3071a/arch/arm/include/asm/thread_info.h"
typedef unsigned long mm_segment_t;
#line 31 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/inst/current/envs/linux-stable-af3071a/linux-stable-af3071a/arch/arm/include/asm/thread_info.h"
struct cpu_context_save {
   __u32 r4 ;
   __u32 r5 ;
   __u32 r6 ;
   __u32 r7 ;
   __u32 r8 ;
   __u32 r9 ;
   __u32 sl ;
   __u32 fp ;
   __u32 sp ;
   __u32 pc ;
   __u32 extra[2U] ;
};
#line 45 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/inst/current/envs/linux-stable-af3071a/linux-stable-af3071a/arch/arm/include/asm/thread_info.h"
struct thread_info {
   unsigned long flags ;
   int preempt_count ;
   mm_segment_t addr_limit ;
   struct task_struct *task ;
   struct exec_domain *exec_domain ;
   __u32 cpu ;
   __u32 cpu_domain ;
   struct cpu_context_save cpu_context ;
   __u32 syscall ;
   __u8 used_cp[16U] ;
   unsigned long tp_value ;
   struct crunch_state crunchstate ;
   union fp_state fpstate ;
   union vfp_state vfpstate ;
   struct restart_block restart_block ;
};
#line 19 "include/linux/spinlock_types_up.h"
struct __anonstruct_arch_spinlock_t_12 {
   unsigned int volatile   slock ;
};
#line 19 "include/linux/spinlock_types_up.h"
typedef struct __anonstruct_arch_spinlock_t_12 arch_spinlock_t;
#line 36 "include/linux/spinlock_types_up.h"
struct raw_spinlock {
   arch_spinlock_t raw_lock ;
   unsigned int magic ;
   unsigned int owner_cpu ;
   void *owner ;
   struct lockdep_map dep_map ;
};
#line 33 "include/linux/spinlock_types.h"
struct __anonstruct_ldv_3075_15 {
   u8 __padding[1U] ;
   struct lockdep_map dep_map ;
};
#line 33 "include/linux/spinlock_types.h"
union __anonunion_ldv_3076_14 {
   struct raw_spinlock rlock ;
   struct __anonstruct_ldv_3075_15 ldv_3075 ;
};
#line 33 "include/linux/spinlock_types.h"
struct spinlock {
   union __anonunion_ldv_3076_14 ldv_3076 ;
};
#line 77 "include/linux/spinlock_types.h"
typedef struct spinlock spinlock_t;
#line 397 "include/linux/spinlock.h"
struct kref {
   atomic_t refcount ;
};
#line 49 "include/linux/wait.h"
struct __wait_queue_head {
   spinlock_t lock ;
   struct list_head task_list ;
};
#line 54 "include/linux/wait.h"
typedef struct __wait_queue_head wait_queue_head_t;
#line 49 "include/linux/kobject.h"
struct kset;
#line 49
struct kobj_type;
#line 49 "include/linux/kobject.h"
struct kobject {
   char const   *name ;
   struct list_head entry ;
   struct kobject *parent ;
   struct kset *kset ;
   struct kobj_type *ktype ;
   struct sysfs_dirent *sd ;
   struct kref kref ;
   unsigned char state_initialized : 1 ;
   unsigned char state_in_sysfs : 1 ;
   unsigned char state_add_uevent_sent : 1 ;
   unsigned char state_remove_uevent_sent : 1 ;
   unsigned char uevent_suppress : 1 ;
};
#line 109 "include/linux/kobject.h"
struct kobj_type {
   void (*release)(struct kobject * ) ;
   struct sysfs_ops  const  *sysfs_ops ;
   struct attribute **default_attrs ;
   struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject * ) ;
   void const   *(*namespace)(struct kobject * ) ;
};
#line 117 "include/linux/kobject.h"
struct kobj_uevent_env {
   char *envp[32U] ;
   int envp_idx ;
   char buf[2048U] ;
   int buflen ;
};
#line 124 "include/linux/kobject.h"
struct kset_uevent_ops {
   int (* const  filter)(struct kset * , struct kobject * ) ;
   char const   *(* const  name)(struct kset * , struct kobject * ) ;
   int (* const  uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
};
#line 141 "include/linux/kobject.h"
struct kset {
   struct list_head list ;
   spinlock_t list_lock ;
   struct kobject kobj ;
   struct kset_uevent_ops  const  *uevent_ops ;
};
#line 219
struct klist_node;
#line 37 "include/linux/klist.h"
struct klist_node {
   void *n_klist ;
   struct list_head n_node ;
   struct kref n_ref ;
};
#line 116 "include/linux/math64.h"
struct timespec {
   __kernel_time_t tv_sec ;
   long tv_nsec ;
};
#line 145 "include/linux/init.h"
typedef void (*ctor_fn_t)(void);
#line 501 "include/linux/nodemask.h"
struct page;
#line 645 "include/linux/mmzone.h"
struct mutex {
   atomic_t count ;
   spinlock_t wait_lock ;
   struct list_head wait_list ;
   struct thread_info *owner ;
   char const   *name ;
   void *magic ;
   struct lockdep_map dep_map ;
};
#line 312 "include/linux/jiffies.h"
union ktime {
   s64 tv64 ;
};
#line 59 "include/linux/ktime.h"
typedef union ktime ktime_t;
#line 99 "include/linux/debugobjects.h"
struct tvec_base;
#line 100 "include/linux/debugobjects.h"
struct timer_list {
   struct list_head entry ;
   unsigned long expires ;
   struct tvec_base *base ;
   void (*function)(unsigned long  ) ;
   unsigned long data ;
   int slack ;
   int start_pid ;
   void *start_site ;
   char start_comm[16U] ;
   struct lockdep_map lockdep_map ;
};
#line 302 "include/linux/timer.h"
struct work_struct;
#line 45 "include/linux/workqueue.h"
struct work_struct {
   atomic_long_t data ;
   struct list_head entry ;
   void (*func)(struct work_struct * ) ;
   struct lockdep_map lockdep_map ;
};
#line 20 "include/linux/elf.h"
typedef __u32 Elf32_Addr;
#line 21 "include/linux/elf.h"
typedef __u16 Elf32_Half;
#line 24 "include/linux/elf.h"
typedef __u32 Elf32_Word;
#line 193 "include/linux/elf.h"
struct elf32_sym {
   Elf32_Word st_name ;
   Elf32_Addr st_value ;
   Elf32_Word st_size ;
   unsigned char st_info ;
   unsigned char st_other ;
   Elf32_Half st_shndx ;
};
#line 201 "include/linux/elf.h"
typedef struct elf32_sym Elf32_Sym;
#line 443
struct kernel_param;
#line 444 "include/linux/elf.h"
struct kernel_param_ops {
   int (*set)(char const   * , struct kernel_param  const  * ) ;
   int (*get)(char * , struct kernel_param  const  * ) ;
   void (*free)(void * ) ;
};
#line 44 "include/linux/moduleparam.h"
struct kparam_string;
#line 44
struct kparam_array;
#line 44 "include/linux/moduleparam.h"
union __anonunion_ldv_6603_22 {
   void *arg ;
   struct kparam_string  const  *str ;
   struct kparam_array  const  *arr ;
};
#line 44 "include/linux/moduleparam.h"
struct kernel_param {
   char const   *name ;
   struct kernel_param_ops  const  *ops ;
   u16 perm ;
   u16 flags ;
   union __anonunion_ldv_6603_22 ldv_6603 ;
};
#line 59 "include/linux/moduleparam.h"
struct kparam_string {
   unsigned int maxlen ;
   char *string ;
};
#line 65 "include/linux/moduleparam.h"
struct kparam_array {
   unsigned int max ;
   unsigned int *num ;
   struct kernel_param_ops  const  *ops ;
   unsigned int elemsize ;
   void *elem ;
};
#line 398 "include/linux/moduleparam.h"
struct completion {
   unsigned int done ;
   wait_queue_head_t wait ;
};
#line 798 "include/linux/rcupdate.h"
struct tracepoint;
#line 799 "include/linux/rcupdate.h"
struct tracepoint_func {
   void *func ;
   void *data ;
};
#line 29 "include/linux/tracepoint.h"
struct tracepoint {
   char const   *name ;
   int state ;
   void (*regfunc)(void) ;
   void (*unregfunc)(void) ;
   struct tracepoint_func *funcs ;
};
#line 84
struct unwind_table;
#line 94 "include/linux/tracepoint.h"
struct mod_arch_specific {
   struct unwind_table *unwind[5U] ;
};
#line 127 "include/trace/events/module.h"
struct kernel_symbol {
   unsigned long value ;
   char const   *name ;
};
#line 48 "include/linux/module.h"
struct module_attribute {
   struct attribute attr ;
   ssize_t (*show)(struct module_attribute * , struct module * , char * ) ;
   ssize_t (*store)(struct module_attribute * , struct module * , char const   * ,
                    size_t  ) ;
   void (*setup)(struct module * , char const   * ) ;
   int (*test)(struct module * ) ;
   void (*free)(struct module * ) ;
};
#line 66
struct module_param_attrs;
#line 66 "include/linux/module.h"
struct module_kobject {
   struct kobject kobj ;
   struct module *mod ;
   struct kobject *drivers_dir ;
   struct module_param_attrs *mp ;
};
#line 78
struct exception_table_entry;
#line 217
enum module_state {
    MODULE_STATE_LIVE = 0,
    MODULE_STATE_COMING = 1,
    MODULE_STATE_GOING = 2
} ;
#line 223 "include/linux/module.h"
struct module_ref {
   unsigned int incs ;
   unsigned int decs ;
};
#line 416
struct module_sect_attrs;
#line 416
struct module_notes_attrs;
#line 416
struct ftrace_event_call;
#line 416 "include/linux/module.h"
struct module {
   enum module_state state ;
   struct list_head list ;
   char name[60U] ;
   struct module_kobject mkobj ;
   struct module_attribute *modinfo_attrs ;
   char const   *version ;
   char const   *srcversion ;
   struct kobject *holders_dir ;
   struct kernel_symbol  const  *syms ;
   unsigned long const   *crcs ;
   unsigned int num_syms ;
   struct kernel_param *kp ;
   unsigned int num_kp ;
   unsigned int num_gpl_syms ;
   struct kernel_symbol  const  *gpl_syms ;
   unsigned long const   *gpl_crcs ;
   struct kernel_symbol  const  *unused_syms ;
   unsigned long const   *unused_crcs ;
   unsigned int num_unused_syms ;
   unsigned int num_unused_gpl_syms ;
   struct kernel_symbol  const  *unused_gpl_syms ;
   unsigned long const   *unused_gpl_crcs ;
   struct kernel_symbol  const  *gpl_future_syms ;
   unsigned long const   *gpl_future_crcs ;
   unsigned int num_gpl_future_syms ;
   unsigned int num_exentries ;
   struct exception_table_entry *extable ;
   int (*init)(void) ;
   void *module_init ;
   void *module_core ;
   unsigned int init_size ;
   unsigned int core_size ;
   unsigned int init_text_size ;
   unsigned int core_text_size ;
   unsigned int init_ro_size ;
   unsigned int core_ro_size ;
   struct mod_arch_specific arch ;
   unsigned int taints ;
   Elf32_Sym *symtab ;
   Elf32_Sym *core_symtab ;
   unsigned int num_symtab ;
   unsigned int core_num_syms ;
   char *strtab ;
   char *core_strtab ;
   struct module_sect_attrs *sect_attrs ;
   struct module_notes_attrs *notes_attrs ;
   char *args ;
   struct tracepoint * const  *tracepoints_ptrs ;
   unsigned int num_tracepoints ;
   char const   **trace_bprintk_fmt_start ;
   unsigned int num_trace_bprintk_fmt ;
   struct ftrace_event_call **trace_events ;
   unsigned int num_trace_events ;
   struct list_head source_list ;
   struct list_head target_list ;
   struct task_struct *waiter ;
   void (*exit)(void) ;
   struct module_ref *refptr ;
   ctor_fn_t (**ctors)(void) ;
   unsigned int num_ctors ;
};
#line 46 "include/linux/pm.h"
struct pm_message {
   int event ;
};
#line 52 "include/linux/pm.h"
typedef struct pm_message pm_message_t;
#line 53 "include/linux/pm.h"
struct dev_pm_ops {
   int (*prepare)(struct device * ) ;
   void (*complete)(struct device * ) ;
   int (*suspend)(struct device * ) ;
   int (*resume)(struct device * ) ;
   int (*freeze)(struct device * ) ;
   int (*thaw)(struct device * ) ;
   int (*poweroff)(struct device * ) ;
   int (*restore)(struct device * ) ;
   int (*suspend_noirq)(struct device * ) ;
   int (*resume_noirq)(struct device * ) ;
   int (*freeze_noirq)(struct device * ) ;
   int (*thaw_noirq)(struct device * ) ;
   int (*poweroff_noirq)(struct device * ) ;
   int (*restore_noirq)(struct device * ) ;
   int (*runtime_suspend)(struct device * ) ;
   int (*runtime_resume)(struct device * ) ;
   int (*runtime_idle)(struct device * ) ;
};
#line 272
enum rpm_status {
    RPM_ACTIVE = 0,
    RPM_RESUMING = 1,
    RPM_SUSPENDED = 2,
    RPM_SUSPENDING = 3
} ;
#line 279
enum rpm_request {
    RPM_REQ_NONE = 0,
    RPM_REQ_IDLE = 1,
    RPM_REQ_SUSPEND = 2,
    RPM_REQ_AUTOSUSPEND = 3,
    RPM_REQ_RESUME = 4
} ;
#line 287
struct wakeup_source;
#line 288 "include/linux/pm.h"
struct dev_pm_info {
   pm_message_t power_state ;
   unsigned char can_wakeup : 1 ;
   unsigned char async_suspend : 1 ;
   unsigned char in_suspend : 1 ;
   spinlock_t lock ;
   struct list_head entry ;
   struct completion completion ;
   struct wakeup_source *wakeup ;
   struct timer_list suspend_timer ;
   unsigned long timer_expires ;
   struct work_struct work ;
   wait_queue_head_t wait_queue ;
   atomic_t usage_count ;
   atomic_t child_count ;
   unsigned char disable_depth : 3 ;
   unsigned char ignore_children : 1 ;
   unsigned char idle_notification : 1 ;
   unsigned char request_pending : 1 ;
   unsigned char deferred_resume : 1 ;
   unsigned char run_wake : 1 ;
   unsigned char runtime_auto : 1 ;
   unsigned char no_callbacks : 1 ;
   unsigned char irq_safe : 1 ;
   unsigned char use_autosuspend : 1 ;
   unsigned char timer_autosuspends : 1 ;
   enum rpm_request request ;
   enum rpm_status runtime_status ;
   int runtime_error ;
   int autosuspend_delay ;
   unsigned long last_busy ;
   unsigned long active_jiffies ;
   unsigned long suspended_jiffies ;
   unsigned long accounting_timestamp ;
};
#line 467 "include/linux/pm.h"
struct dev_power_domain {
   struct dev_pm_ops ops ;
};
#line 588 "include/linux/pm.h"
struct dev_archdata {

};
#line 591 "include/linux/pm.h"
struct pdev_archdata {

};
#line 594
struct device_private;
#line 595
struct device_driver;
#line 596
struct driver_private;
#line 597
struct class;
#line 598
struct subsys_private;
#line 599
struct bus_type;
#line 600
struct device_node;
#line 601 "include/linux/pm.h"
struct bus_attribute {
   struct attribute attr ;
   ssize_t (*show)(struct bus_type * , char * ) ;
   ssize_t (*store)(struct bus_type * , char const   * , size_t  ) ;
};
#line 49 "include/linux/device.h"
struct device_attribute;
#line 49
struct driver_attribute;
#line 49 "include/linux/device.h"
struct bus_type {
   char const   *name ;
   struct bus_attribute *bus_attrs ;
   struct device_attribute *dev_attrs ;
   struct driver_attribute *drv_attrs ;
   int (*match)(struct device * , struct device_driver * ) ;
   int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
   int (*probe)(struct device * ) ;
   int (*remove)(struct device * ) ;
   void (*shutdown)(struct device * ) ;
   int (*suspend)(struct device * , pm_message_t  ) ;
   int (*resume)(struct device * ) ;
   struct dev_pm_ops  const  *pm ;
   struct subsys_private *p ;
};
#line 121
struct of_device_id;
#line 121 "include/linux/device.h"
struct device_driver {
   char const   *name ;
   struct bus_type *bus ;
   struct module *owner ;
   char const   *mod_name ;
   bool suppress_bind_attrs ;
   struct of_device_id  const  *of_match_table ;
   int (*probe)(struct device * ) ;
   int (*remove)(struct device * ) ;
   void (*shutdown)(struct device * ) ;
   int (*suspend)(struct device * , pm_message_t  ) ;
   int (*resume)(struct device * ) ;
   struct attribute_group  const  **groups ;
   struct dev_pm_ops  const  *pm ;
   struct driver_private *p ;
};
#line 155 "include/linux/device.h"
struct driver_attribute {
   struct attribute attr ;
   ssize_t (*show)(struct device_driver * , char * ) ;
   ssize_t (*store)(struct device_driver * , char const   * , size_t  ) ;
};
#line 185
struct class_attribute;
#line 185 "include/linux/device.h"
struct class {
   char const   *name ;
   struct module *owner ;
   struct class_attribute *class_attrs ;
   struct device_attribute *dev_attrs ;
   struct bin_attribute *dev_bin_attrs ;
   struct kobject *dev_kobj ;
   int (*dev_uevent)(struct device * , struct kobj_uevent_env * ) ;
   char *(*devnode)(struct device * , mode_t * ) ;
   void (*class_release)(struct class * ) ;
   void (*dev_release)(struct device * ) ;
   int (*suspend)(struct device * , pm_message_t  ) ;
   int (*resume)(struct device * ) ;
   struct kobj_ns_type_operations  const  *ns_type ;
   void const   *(*namespace)(struct device * ) ;
   struct dev_pm_ops  const  *pm ;
   struct subsys_private *p ;
};
#line 216
struct device_type;
#line 255 "include/linux/device.h"
struct class_attribute {
   struct attribute attr ;
   ssize_t (*show)(struct class * , struct class_attribute * , char * ) ;
   ssize_t (*store)(struct class * , struct class_attribute * , char const   * , size_t  ) ;
};
#line 306 "include/linux/device.h"
struct device_type {
   char const   *name ;
   struct attribute_group  const  **groups ;
   int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
   char *(*devnode)(struct device * , mode_t * ) ;
   void (*release)(struct device * ) ;
   struct dev_pm_ops  const  *pm ;
};
#line 333 "include/linux/device.h"
struct device_attribute {
   struct attribute attr ;
   ssize_t (*show)(struct device * , struct device_attribute * , char * ) ;
   ssize_t (*store)(struct device * , struct device_attribute * , char const   * ,
                    size_t  ) ;
};
#line 402 "include/linux/device.h"
struct device_dma_parameters {
   unsigned int max_segment_size ;
   unsigned long segment_boundary_mask ;
};
#line 411
struct dma_coherent_mem;
#line 411 "include/linux/device.h"
struct device {
   struct device *parent ;
   struct device_private *p ;
   struct kobject kobj ;
   char const   *init_name ;
   struct device_type *type ;
   struct mutex mutex ;
   struct bus_type *bus ;
   struct device_driver *driver ;
   void *platform_data ;
   struct dev_pm_info power ;
   struct dev_power_domain *pwr_domain ;
   u64 *dma_mask ;
   u64 coherent_dma_mask ;
   struct device_dma_parameters *dma_parms ;
   struct list_head dma_pools ;
   struct dma_coherent_mem *dma_mem ;
   struct dev_archdata archdata ;
   struct device_node *of_node ;
   dev_t devt ;
   spinlock_t devres_lock ;
   struct list_head devres_head ;
   struct klist_node knode_class ;
   struct class *class ;
   struct attribute_group  const  **groups ;
   void (*release)(struct device * ) ;
};
#line 465 "include/linux/device.h"
struct wakeup_source {
   char *name ;
   struct list_head entry ;
   spinlock_t lock ;
   struct timer_list timer ;
   unsigned long timer_expires ;
   ktime_t total_time ;
   ktime_t max_time ;
   ktime_t last_time ;
   unsigned long event_count ;
   unsigned long active_count ;
   unsigned long relax_count ;
   unsigned long hit_count ;
   unsigned char active : 1 ;
};
#line 101 "include/linux/slab.h"
struct kmem_cache;
#line 79 "include/linux/kmemleak.h"
struct kmem_cache_cpu {
   void **freelist ;
   struct page *page ;
   int node ;
   unsigned int stat[19U] ;
};
#line 48 "include/linux/slub_def.h"
struct kmem_cache_node {
   spinlock_t list_lock ;
   unsigned long nr_partial ;
   struct list_head partial ;
   atomic_long_t nr_slabs ;
   atomic_long_t total_objects ;
   struct list_head full ;
};
#line 59 "include/linux/slub_def.h"
struct kmem_cache_order_objects {
   unsigned long x ;
};
#line 69 "include/linux/slub_def.h"
struct kmem_cache {
   struct kmem_cache_cpu *cpu_slab ;
   unsigned long flags ;
   unsigned long min_partial ;
   int size ;
   int objsize ;
   int offset ;
   struct kmem_cache_order_objects oo ;
   struct kmem_cache_order_objects max ;
   struct kmem_cache_order_objects min ;
   gfp_t allocflags ;
   int refcount ;
   void (*ctor)(void * ) ;
   int inuse ;
   int align ;
   int reserved ;
   char const   *name ;
   struct list_head list ;
   struct kobject kobj ;
   struct kmem_cache_node *node[1U] ;
};
#line 12 "include/linux/mod_devicetable.h"
typedef unsigned long kernel_ulong_t;
#line 215 "include/linux/mod_devicetable.h"
struct of_device_id {
   char name[32U] ;
   char type[32U] ;
   char compatible[128U] ;
   void *data ;
};
#line 457 "include/linux/mod_devicetable.h"
struct platform_device_id {
   char name[20U] ;
   kernel_ulong_t driver_data ;
};
#line 518
struct mfd_cell;
#line 519 "include/linux/mod_devicetable.h"
struct platform_device {
   char const   *name ;
   int id ;
   struct device dev ;
   u32 num_resources ;
   struct resource *resource ;
   struct platform_device_id  const  *id_entry ;
   struct mfd_cell *mfd_cell ;
   struct pdev_archdata archdata ;
};
#line 118 "include/linux/platform_device.h"
struct platform_driver {
   int (*probe)(struct platform_device * ) ;
   int (*remove)(struct platform_device * ) ;
   void (*shutdown)(struct platform_device * ) ;
   int (*suspend)(struct platform_device * , pm_message_t  ) ;
   int (*resume)(struct platform_device * ) ;
   struct device_driver driver ;
   struct platform_device_id  const  *id_table ;
};
#line 33 "include/linux/hwmon.h"
struct sensor_device_attribute {
   struct device_attribute dev_attr ;
   int index ;
};
#line 43 "include/linux/hwmon-sysfs.h"
struct s3c_adc_client;
#line 34 "arch/arm/plat-samsung/include/plat/adc.h"
struct s3c_hwmon_chcfg {
   char const   *name ;
   unsigned int mult ;
   unsigned int div ;
};
#line 31 "arch/arm/plat-samsung/include/plat/hwmon.h"
struct s3c_hwmon_pdata {
   struct s3c_hwmon_chcfg *in[8U] ;
};
#line 49 "arch/arm/plat-samsung/include/plat/hwmon.h"
struct s3c_hwmon_attr {
   struct sensor_device_attribute in ;
   struct sensor_device_attribute label ;
   char in_name[12U] ;
   char label_name[12U] ;
};
#line 56 "arch/arm/plat-samsung/include/plat/hwmon.h"
struct s3c_hwmon {
   struct mutex lock ;
   struct s3c_adc_client *client ;
   struct device *hwmon_dev ;
   struct s3c_hwmon_attr attrs[8U] ;
};
#line 2 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/work/current--X--drivers/hwmon/s3c-hwmon.ko--X--defaultlinux-stable-af3071a--X--130_7a--X--cpachecker/linux-stable-af3071a/csd_deg_dscv/11/dscv_tempdir/dscv/ri/130_7a/drivers/hwmon/s3c-hwmon.c.prepared"
long ldv_is_err(void const   *ptr ) ;
#line 5
long ldv_ptr_err(void const   *ptr ) ;
#line 264 "include/linux/kernel.h"
extern int snprintf(char * , size_t  , char const   *  , ...) ;
#line 115 "include/linux/mutex.h"
extern void __mutex_init(struct mutex * , char const   * , struct lock_class_key * ) ;
#line 135
extern int mutex_lock_interruptible_nested(struct mutex * , unsigned int  ) ;
#line 160
extern void mutex_unlock(struct mutex * ) ;
#line 96 "include/linux/module.h"
extern struct module __this_module ;
#line 350 "include/linux/device.h"
int ldv_device_create_file_5(struct device *ldv_func_arg1 , struct device_attribute  const  *ldv_func_arg2 ) ;
#line 354
int ldv_device_create_file_6(struct device *ldv_func_arg1 , struct device_attribute  const  *ldv_func_arg2 ) ;
#line 356
extern void device_remove_file(struct device * , struct device_attribute  const  * ) ;
#line 558
extern void *dev_get_drvdata(struct device  const  * ) ;
#line 559
extern void dev_set_drvdata(struct device * , void * ) ;
#line 648
extern int dev_printk(char const   * , struct device  const  * , char const   *  , ...) ;
#line 657
extern int dev_err(struct device  const  * , char const   *  , ...) ;
#line 659
extern int dev_warn(struct device  const  * , char const   *  , ...) ;
#line 9 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/work/current--X--drivers/hwmon/s3c-hwmon.ko--X--defaultlinux-stable-af3071a--X--130_7a--X--cpachecker/linux-stable-af3071a/csd_deg_dscv/11/dscv_tempdir/dscv/ri/130_7a/drivers/hwmon/s3c-hwmon.c.prepared"
void ldv_sysfs(void) ;
#line 10
int ldv_device_create_file_dev_attr_of_sensor_device_attribute(struct device_attribute  const  *attr ) ;
#line 141 "include/linux/slab.h"
extern void kfree(void const   * ) ;
#line 221 "include/linux/slub_def.h"
extern void *__kmalloc(size_t  , gfp_t  ) ;
#line 255 "include/linux/slub_def.h"
__inline static void *kmalloc(size_t size , gfp_t flags ) 
{ 
  void *tmp___2 ;

  {
#line 270
  tmp___2 = __kmalloc(size, flags);
#line 270
  return (tmp___2);
}
}
#line 318 "include/linux/slab.h"
__inline static void *kzalloc(size_t size , gfp_t flags ) 
{ 
  void *tmp ;

  {
#line 320
  tmp = kmalloc(size, flags | 32768U);
#line 320
  return (tmp);
}
}
#line 31 "include/linux/err.h"
__inline static long PTR_ERR(void const   *ptr ) ;
#line 40
__inline static long IS_ERR(void const   *ptr ) ;
#line 129 "include/linux/platform_device.h"
extern int platform_driver_register(struct platform_driver * ) ;
#line 130
extern void platform_driver_unregister(struct platform_driver * ) ;
#line 138 "include/linux/platform_device.h"
__inline static void *platform_get_drvdata(struct platform_device  const  *pdev ) 
{ 
  void *tmp ;

  {
#line 140
  tmp = dev_get_drvdata(& pdev->dev);
#line 140
  return (tmp);
}
}
#line 143 "include/linux/platform_device.h"
__inline static void platform_set_drvdata(struct platform_device *pdev , void *data ) 
{ 


  {
#line 145
  dev_set_drvdata(& pdev->dev, data);
#line 146
  return;
}
}
#line 19 "include/linux/hwmon.h"
extern struct device *hwmon_device_register(struct device * ) ;
#line 21
extern void hwmon_device_unregister(struct device * ) ;
#line 22 "arch/arm/plat-samsung/include/plat/adc.h"
extern int s3c_adc_read(struct s3c_adc_client * , unsigned int  ) ;
#line 25
extern struct s3c_adc_client *s3c_adc_register(struct platform_device * , void (*)(struct s3c_adc_client * ,
                                                                                   unsigned int  ) ,
                                               void (*)(struct s3c_adc_client * ,
                                                        unsigned int  , unsigned int  ,
                                                        unsigned int * ) , unsigned int  ) ;
#line 33
extern void s3c_adc_release(struct s3c_adc_client * ) ;
#line 82 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/work/current--X--drivers/hwmon/s3c-hwmon.ko--X--defaultlinux-stable-af3071a--X--130_7a--X--cpachecker/linux-stable-af3071a/csd_deg_dscv/11/dscv_tempdir/dscv/ri/130_7a/drivers/hwmon/s3c-hwmon.c.prepared"
static int s3c_hwmon_read_ch(struct device *dev , struct s3c_hwmon *hwmon , int channel ) 
{ 
  int ret ;

  {
#line 87
  ret = mutex_lock_interruptible_nested(& hwmon->lock, 0U);
#line 88
  if (ret < 0) {
#line 89
    return (ret);
  } else {

  }
#line 91
  dev_printk("<7>", (struct device  const  *)dev, "reading channel %d\n", channel);
#line 93
  ret = s3c_adc_read(hwmon->client, (unsigned int )channel);
#line 94
  mutex_unlock(& hwmon->lock);
#line 96
  return (ret);
}
}
#line 162 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/work/current--X--drivers/hwmon/s3c-hwmon.ko--X--defaultlinux-stable-af3071a--X--130_7a--X--cpachecker/linux-stable-af3071a/csd_deg_dscv/11/dscv_tempdir/dscv/ri/130_7a/drivers/hwmon/s3c-hwmon.c.prepared"
__inline static int s3c_hwmon_add_raw(struct device *dev ) 
{ 


  {
#line 162
  return (0);
}
}
#line 163 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/work/current--X--drivers/hwmon/s3c-hwmon.ko--X--defaultlinux-stable-af3071a--X--130_7a--X--cpachecker/linux-stable-af3071a/csd_deg_dscv/11/dscv_tempdir/dscv/ri/130_7a/drivers/hwmon/s3c-hwmon.c.prepared"
__inline static void s3c_hwmon_remove_raw(struct device *dev ) 
{ 


  {
#line 165
  return;
}
}
#line 177 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/work/current--X--drivers/hwmon/s3c-hwmon.ko--X--defaultlinux-stable-af3071a--X--130_7a--X--cpachecker/linux-stable-af3071a/csd_deg_dscv/11/dscv_tempdir/dscv/ri/130_7a/drivers/hwmon/s3c-hwmon.c.prepared"
static ssize_t s3c_hwmon_ch_show(struct device *dev , struct device_attribute *attr ,
                                 char *buf ) 
{ 
  struct sensor_device_attribute *sen_attr ;
  struct device_attribute  const  *__mptr ;
  struct s3c_hwmon *hwmon ;
  struct device  const  *__mptr___0 ;
  void *tmp ;
  struct s3c_hwmon_pdata *pdata ;
  struct s3c_hwmon_chcfg *cfg ;
  int ret ;
  unsigned int __divisor ;
  int tmp___0 ;

  {
#line 181
  __mptr = (struct device_attribute  const  *)attr;
#line 181
  sen_attr = (struct sensor_device_attribute *)__mptr;
#line 182
  __mptr___0 = (struct device  const  *)dev;
#line 182
  tmp = platform_get_drvdata((struct platform_device  const  *)((struct platform_device *)__mptr___0 + 0xfffffffffffffff8UL));
#line 182
  hwmon = (struct s3c_hwmon *)tmp;
#line 183
  pdata = (struct s3c_hwmon_pdata *)dev->platform_data;
#line 187
  cfg = pdata->in[sen_attr->index];
#line 189
  ret = s3c_hwmon_read_ch(dev, hwmon, sen_attr->index);
#line 190
  if (ret < 0) {
#line 191
    return (ret);
  } else {

  }
#line 193
  ret = (int )(cfg->mult * (unsigned int )ret);
#line 194
  __divisor = cfg->div;
#line 194
  ret = (int )((__divisor / 2U + (unsigned int )ret) / __divisor);
#line 196
  tmp___0 = snprintf(buf, 4096U, "%d\n", ret);
#line 196
  return (tmp___0);
}
}
#line 207 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/work/current--X--drivers/hwmon/s3c-hwmon.ko--X--defaultlinux-stable-af3071a--X--130_7a--X--cpachecker/linux-stable-af3071a/csd_deg_dscv/11/dscv_tempdir/dscv/ri/130_7a/drivers/hwmon/s3c-hwmon.c.prepared"
static ssize_t s3c_hwmon_label_show(struct device *dev , struct device_attribute *attr ,
                                    char *buf ) 
{ 
  struct sensor_device_attribute *sen_attr ;
  struct device_attribute  const  *__mptr ;
  struct s3c_hwmon_pdata *pdata ;
  struct s3c_hwmon_chcfg *cfg ;
  int tmp ;

  {
#line 211
  __mptr = (struct device_attribute  const  *)attr;
#line 211
  sen_attr = (struct sensor_device_attribute *)__mptr;
#line 212
  pdata = (struct s3c_hwmon_pdata *)dev->platform_data;
#line 215
  cfg = pdata->in[sen_attr->index];
#line 217
  tmp = snprintf(buf, 4096U, "%s\n", cfg->name);
#line 217
  return (tmp);
}
}
#line 234 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/work/current--X--drivers/hwmon/s3c-hwmon.ko--X--defaultlinux-stable-af3071a--X--130_7a--X--cpachecker/linux-stable-af3071a/csd_deg_dscv/11/dscv_tempdir/dscv/ri/130_7a/drivers/hwmon/s3c-hwmon.c.prepared"
static int s3c_hwmon_create_attr(struct device *dev , struct s3c_hwmon_chcfg *cfg ,
                                 struct s3c_hwmon_attr *attrs , int channel ) 
{ 
  struct sensor_device_attribute *attr ;
  int ret ;

  {
#line 242
  snprintf((char *)(& attrs->in_name), 12U, "in%d_input", channel);
#line 244
  attr = & attrs->in;
#line 245
  attr->index = channel;
#line 246
  ldv_sysfs();
#line 247
  attr->dev_attr.attr.name = (char const   *)(& attrs->in_name);
#line 248
  attr->dev_attr.attr.mode = 292U;
#line 249
  attr->dev_attr.show = & s3c_hwmon_ch_show;
#line 251
  ret = ldv_device_create_file_5(dev, (struct device_attribute  const  *)(& attr->dev_attr));
#line 252
  if (ret < 0) {
#line 253
    dev_err((struct device  const  *)dev, "failed to create input attribute\n");
#line 254
    return (ret);
  } else {

  }
#line 258
  if ((unsigned long )cfg->name != (unsigned long )((char const   *)0)) {
#line 259
    snprintf((char *)(& attrs->label_name), 12U, "in%d_label", channel);
#line 262
    attr = & attrs->label;
#line 263
    attr->index = channel;
#line 264
    ldv_sysfs();
#line 265
    attr->dev_attr.attr.name = (char const   *)(& attrs->label_name);
#line 266
    attr->dev_attr.attr.mode = 292U;
#line 267
    attr->dev_attr.show = & s3c_hwmon_label_show;
#line 269
    ret = ldv_device_create_file_6(dev, (struct device_attribute  const  *)(& attr->dev_attr));
#line 270
    if (ret < 0) {
#line 271
      device_remove_file(dev, (struct device_attribute  const  *)(& attrs->in.dev_attr));
#line 272
      dev_err((struct device  const  *)dev, "failed to create label attribute\n");
    } else {

    }
  } else {

  }
#line 276
  return (ret);
}
}
#line 279 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/work/current--X--drivers/hwmon/s3c-hwmon.ko--X--defaultlinux-stable-af3071a--X--130_7a--X--cpachecker/linux-stable-af3071a/csd_deg_dscv/11/dscv_tempdir/dscv/ri/130_7a/drivers/hwmon/s3c-hwmon.c.prepared"
static void s3c_hwmon_remove_attr(struct device *dev , struct s3c_hwmon_attr *attrs ) 
{ 


  {
#line 282
  device_remove_file(dev, (struct device_attribute  const  *)(& attrs->in.dev_attr));
#line 283
  device_remove_file(dev, (struct device_attribute  const  *)(& attrs->label.dev_attr));
#line 284
  return;
}
}
#line 290 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/work/current--X--drivers/hwmon/s3c-hwmon.ko--X--defaultlinux-stable-af3071a--X--130_7a--X--cpachecker/linux-stable-af3071a/csd_deg_dscv/11/dscv_tempdir/dscv/ri/130_7a/drivers/hwmon/s3c-hwmon.c.prepared"
static int s3c_hwmon_probe(struct platform_device *dev ) 
{ 
  struct s3c_hwmon_pdata *pdata ;
  struct s3c_hwmon *hwmon ;
  int ret ;
  int i ;
  void *tmp ;
  struct lock_class_key __key ;
  long tmp___0 ;
  long tmp___1 ;
  long tmp___2 ;
  long tmp___3 ;
  struct s3c_hwmon_chcfg *cfg ;

  {
#line 292
  pdata = (struct s3c_hwmon_pdata *)dev->dev.platform_data;
#line 294
  ret = 0;
#line 297
  if ((unsigned long )pdata == (unsigned long )((struct s3c_hwmon_pdata *)0)) {
#line 298
    dev_err((struct device  const  *)(& dev->dev), "no platform data supplied\n");
#line 299
    return (-22);
  } else {

  }
#line 302
  tmp = kzalloc(800U, 208U);
#line 302
  hwmon = (struct s3c_hwmon *)tmp;
#line 303
  if ((unsigned long )hwmon == (unsigned long )((struct s3c_hwmon *)0)) {
#line 304
    dev_err((struct device  const  *)(& dev->dev), "no memory\n");
#line 305
    return (-12);
  } else {

  }
#line 308
  platform_set_drvdata(dev, (void *)hwmon);
#line 310
  __mutex_init(& hwmon->lock, "&hwmon->lock", & __key);
#line 314
  hwmon->client = s3c_adc_register(dev, 0, 0, 0U);
#line 315
  tmp___1 = IS_ERR((void const   *)hwmon->client);
#line 315
  if (tmp___1 != 0L) {
#line 316
    dev_err((struct device  const  *)(& dev->dev), "cannot register adc\n");
#line 317
    tmp___0 = PTR_ERR((void const   *)hwmon->client);
#line 317
    ret = (int )tmp___0;
#line 318
    goto err_mem;
  } else {

  }
#line 323
  ret = s3c_hwmon_add_raw(& dev->dev);
#line 324
  if (ret != 0) {
#line 325
    goto err_registered;
  } else {

  }
#line 329
  hwmon->hwmon_dev = hwmon_device_register(& dev->dev);
#line 330
  tmp___3 = IS_ERR((void const   *)hwmon->hwmon_dev);
#line 330
  if (tmp___3 != 0L) {
#line 331
    dev_err((struct device  const  *)(& dev->dev), "error registering with hwmon\n");
#line 332
    tmp___2 = PTR_ERR((void const   *)hwmon->hwmon_dev);
#line 332
    ret = (int )tmp___2;
#line 333
    goto err_raw_attribute;
  } else {

  }
#line 336
  i = 0;
#line 336
  goto ldv_9894;
  ldv_9893: 
#line 337
  cfg = pdata->in[i];
#line 339
  if ((unsigned long )cfg == (unsigned long )((struct s3c_hwmon_chcfg *)0)) {
#line 340
    goto ldv_9888;
  } else {

  }
#line 342
  if (cfg->mult > 65535U) {
#line 343
    dev_warn((struct device  const  *)(& dev->dev), "channel %d multiplier too large\n",
             i);
  } else {

  }
#line 347
  if (cfg->div == 0U) {
#line 348
    dev_err((struct device  const  *)(& dev->dev), "channel %d divider zero\n", i);
#line 349
    goto ldv_9888;
  } else {

  }
#line 352
  ret = s3c_hwmon_create_attr(& dev->dev, pdata->in[i], (struct s3c_hwmon_attr *)(& hwmon->attrs) + (unsigned int )i,
                              i);
#line 354
  if (ret != 0) {
#line 355
    dev_err((struct device  const  *)(& dev->dev), "error creating channel %d\n",
            i);
#line 358
    i = i - 1;
#line 358
    goto ldv_9890;
    ldv_9889: 
#line 359
    s3c_hwmon_remove_attr(& dev->dev, (struct s3c_hwmon_attr *)(& hwmon->attrs) + (unsigned int )i);
#line 358
    i = i - 1;
    ldv_9890: ;
#line 358
    if (i >= 0) {
#line 360
      goto ldv_9889;
    } else {

    }

#line 362
    goto err_hwmon_register;
  } else {

  }
  ldv_9888: 
#line 336
  i = i + 1;
  ldv_9894: ;
#line 336
  if ((unsigned int )i <= 7U) {
#line 338
    goto ldv_9893;
  } else {

  }

#line 366
  return (0);
  err_hwmon_register: 
#line 369
  hwmon_device_unregister(hwmon->hwmon_dev);
  err_raw_attribute: 
#line 372
  s3c_hwmon_remove_raw(& dev->dev);
  err_registered: 
#line 375
  s3c_adc_release(hwmon->client);
  err_mem: 
#line 378
  kfree((void const   *)hwmon);
#line 379
  return (ret);
}
}
#line 382 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/work/current--X--drivers/hwmon/s3c-hwmon.ko--X--defaultlinux-stable-af3071a--X--130_7a--X--cpachecker/linux-stable-af3071a/csd_deg_dscv/11/dscv_tempdir/dscv/ri/130_7a/drivers/hwmon/s3c-hwmon.c.prepared"
static int s3c_hwmon_remove(struct platform_device *dev ) 
{ 
  struct s3c_hwmon *hwmon ;
  void *tmp ;
  int i ;

  {
#line 384
  tmp = platform_get_drvdata((struct platform_device  const  *)dev);
#line 384
  hwmon = (struct s3c_hwmon *)tmp;
#line 387
  s3c_hwmon_remove_raw(& dev->dev);
#line 389
  i = 0;
#line 389
  goto ldv_9904;
  ldv_9903: 
#line 390
  s3c_hwmon_remove_attr(& dev->dev, (struct s3c_hwmon_attr *)(& hwmon->attrs) + (unsigned int )i);
#line 389
  i = i + 1;
  ldv_9904: ;
#line 389
  if ((unsigned int )i <= 7U) {
#line 391
    goto ldv_9903;
  } else {

  }
#line 392
  hwmon_device_unregister(hwmon->hwmon_dev);
#line 393
  s3c_adc_release(hwmon->client);
#line 395
  return (0);
}
}
#line 398 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/work/current--X--drivers/hwmon/s3c-hwmon.ko--X--defaultlinux-stable-af3071a--X--130_7a--X--cpachecker/linux-stable-af3071a/csd_deg_dscv/11/dscv_tempdir/dscv/ri/130_7a/drivers/hwmon/s3c-hwmon.c.prepared"
static struct platform_driver s3c_hwmon_driver  =    {& s3c_hwmon_probe, & s3c_hwmon_remove, 0, 0, 0, {"s3c-hwmon", 0, & __this_module,
                                                     0, (_Bool)0, 0, 0, 0, 0, 0, 0,
                                                     0, 0, 0}, 0};
#line 407 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/work/current--X--drivers/hwmon/s3c-hwmon.ko--X--defaultlinux-stable-af3071a--X--130_7a--X--cpachecker/linux-stable-af3071a/csd_deg_dscv/11/dscv_tempdir/dscv/ri/130_7a/drivers/hwmon/s3c-hwmon.c.prepared"
static int s3c_hwmon_init(void) 
{ 
  int tmp ;

  {
#line 409
  tmp = platform_driver_register(& s3c_hwmon_driver);
#line 409
  return (tmp);
}
}
#line 412 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/work/current--X--drivers/hwmon/s3c-hwmon.ko--X--defaultlinux-stable-af3071a--X--130_7a--X--cpachecker/linux-stable-af3071a/csd_deg_dscv/11/dscv_tempdir/dscv/ri/130_7a/drivers/hwmon/s3c-hwmon.c.prepared"
static void s3c_hwmon_exit(void) 
{ 


  {
#line 414
  platform_driver_unregister(& s3c_hwmon_driver);
#line 415
  return;
}
}
#line 441
extern void ldv_check_final_state(void) ;
#line 444
extern void ldv_check_return_value(int  ) ;
#line 447
extern void ldv_check_return_value_probe(int  ) ;
#line 450
void ldv_initialize(void) ;
#line 453
extern void ldv_handler_precall(void) ;
#line 456
extern int __VERIFIER_nondet_int(void) ;
#line 459 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/work/current--X--drivers/hwmon/s3c-hwmon.ko--X--defaultlinux-stable-af3071a--X--130_7a--X--cpachecker/linux-stable-af3071a/csd_deg_dscv/11/dscv_tempdir/dscv/ri/130_7a/drivers/hwmon/s3c-hwmon.c.prepared"
int LDV_IN_INTERRUPT  ;
#line 462 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/work/current--X--drivers/hwmon/s3c-hwmon.ko--X--defaultlinux-stable-af3071a--X--130_7a--X--cpachecker/linux-stable-af3071a/csd_deg_dscv/11/dscv_tempdir/dscv/ri/130_7a/drivers/hwmon/s3c-hwmon.c.prepared"
int main(void) 
{ 
  struct platform_device *var_group1 ;
  int res_s3c_hwmon_probe_10 ;
  int ldv_s_s3c_hwmon_driver_platform_driver ;
  int tmp ;
  int tmp___0 ;
  int tmp___1 ;

  {
#line 520
  ldv_s_s3c_hwmon_driver_platform_driver = 0;
#line 496
  LDV_IN_INTERRUPT = 1;
#line 505
  ldv_initialize();
#line 517
  ldv_handler_precall();
#line 518
  tmp = s3c_hwmon_init();
#line 518
  if (tmp != 0) {
#line 519
    goto ldv_final;
  } else {

  }
#line 523
  goto ldv_9953;
  ldv_9952: 
#line 527
  tmp___0 = __VERIFIER_nondet_int();
#line 527
  switch (tmp___0) {
  case 0: ;
#line 532
  if (ldv_s_s3c_hwmon_driver_platform_driver == 0) {
#line 543
    res_s3c_hwmon_probe_10 = s3c_hwmon_probe(var_group1);
#line 544
    ldv_check_return_value(res_s3c_hwmon_probe_10);
#line 545
    ldv_check_return_value_probe(res_s3c_hwmon_probe_10);
#line 546
    if (res_s3c_hwmon_probe_10 != 0) {
#line 547
      goto ldv_module_exit;
    } else {

    }
#line 548
    ldv_s_s3c_hwmon_driver_platform_driver = ldv_s_s3c_hwmon_driver_platform_driver + 1;
  } else {

  }
#line 554
  goto ldv_9949;
  case 1: ;
#line 558
  if (ldv_s_s3c_hwmon_driver_platform_driver == 1) {
#line 569
    ldv_handler_precall();
#line 570
    s3c_hwmon_remove(var_group1);
#line 571
    ldv_s_s3c_hwmon_driver_platform_driver = 0;
  } else {

  }
#line 577
  goto ldv_9949;
  default: ;
#line 578
  goto ldv_9949;
  }
  ldv_9949: ;
  ldv_9953: 
#line 523
  tmp___1 = __VERIFIER_nondet_int();
#line 523
  if (tmp___1 != 0 || ldv_s_s3c_hwmon_driver_platform_driver != 0) {
#line 526
    goto ldv_9952;
  } else {

  }

  ldv_module_exit: 
#line 596
  ldv_handler_precall();
#line 597
  s3c_hwmon_exit();
  ldv_final: 
#line 600
  ldv_check_final_state();
#line 603
  return 0;
}
}
#line 615 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/work/current--X--drivers/hwmon/s3c-hwmon.ko--X--defaultlinux-stable-af3071a--X--130_7a--X--cpachecker/linux-stable-af3071a/csd_deg_dscv/11/dscv_tempdir/dscv/ri/130_7a/drivers/hwmon/s3c-hwmon.c.prepared"
__inline static long PTR_ERR(void const   *ptr ) 
{ 
  long tmp ;

  {
#line 620
  tmp = ldv_ptr_err(ptr);
#line 620
  return (tmp);
}
}
#line 623 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/work/current--X--drivers/hwmon/s3c-hwmon.ko--X--defaultlinux-stable-af3071a--X--130_7a--X--cpachecker/linux-stable-af3071a/csd_deg_dscv/11/dscv_tempdir/dscv/ri/130_7a/drivers/hwmon/s3c-hwmon.c.prepared"
__inline static long IS_ERR(void const   *ptr ) 
{ 
  long tmp ;

  {
#line 628
  tmp = ldv_is_err(ptr);
#line 628
  return (tmp);
}
}
#line 639 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/work/current--X--drivers/hwmon/s3c-hwmon.ko--X--defaultlinux-stable-af3071a--X--130_7a--X--cpachecker/linux-stable-af3071a/csd_deg_dscv/11/dscv_tempdir/dscv/ri/130_7a/drivers/hwmon/s3c-hwmon.c.prepared"
int ldv_device_create_file_5(struct device *ldv_func_arg1 , struct device_attribute  const  *ldv_func_arg2 ) 
{ 
  int tmp ;

  {
#line 645
  tmp = ldv_device_create_file_dev_attr_of_sensor_device_attribute(ldv_func_arg2);
#line 645
  return (tmp);
}
}
#line 648 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/work/current--X--drivers/hwmon/s3c-hwmon.ko--X--defaultlinux-stable-af3071a--X--130_7a--X--cpachecker/linux-stable-af3071a/csd_deg_dscv/11/dscv_tempdir/dscv/ri/130_7a/drivers/hwmon/s3c-hwmon.c.prepared"
int ldv_device_create_file_6(struct device *ldv_func_arg1 , struct device_attribute  const  *ldv_func_arg2 ) 
{ 
  int tmp ;

  {
#line 654
  tmp = ldv_device_create_file_dev_attr_of_sensor_device_attribute(ldv_func_arg2);
#line 654
  return (tmp);
}
}
#line 1 "<compiler builtins>"
long ldv__builtin_expect(long exp , long c ) ;
#line 10 "/work/vladimir/kernel-rules/verifier/rcv.h"
__inline static void ldv_error(void) 
{ 


  {
  ERROR: __VERIFIER_error();
}
}
#line 49 "/work/vladimir/kernel-rules/verifier/rcv.h"
long ldv__builtin_expect(long exp , long c ) 
{ 


  {
#line 51
  return (exp);
}
}
#line 5 "/work/vladimir/kernel-rules/kernel-model/ERR.inc"
long ldv_is_err(void const   *ptr ) 
{ 


  {
#line 8
  return ((unsigned long )ptr > 2012UL);
}
}
#line 12 "/work/vladimir/kernel-rules/kernel-model/ERR.inc"
void *ldv_err_ptr(long error ) 
{ 


  {
#line 15
  return ((void *)(2012L - error));
}
}
#line 19 "/work/vladimir/kernel-rules/kernel-model/ERR.inc"
long ldv_ptr_err(void const   *ptr ) 
{ 


  {
#line 22
  return ((long )(2012UL - (unsigned long )ptr));
}
}
#line 26 "/work/vladimir/kernel-rules/kernel-model/ERR.inc"
long ldv_is_err_or_null(void const   *ptr ) 
{ 
  long tmp ;
  int tmp___0 ;

  {
#line 29
  if (! ptr) {
#line 29
    tmp___0 = 1;
  } else {
#line 29
    tmp = ldv_is_err((unsigned long )ptr);
#line 29
    if (tmp) {
#line 29
      tmp___0 = 1;
    } else {
#line 29
      tmp___0 = 0;
    }
  }
#line 29
  return (tmp___0);
}
}
#line 6 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/work/current--X--drivers/hwmon/s3c-hwmon.ko--X--defaultlinux-stable-af3071a--X--130_7a--X--cpachecker/linux-stable-af3071a/csd_deg_dscv/11/dscv_tempdir/rule-instrumentor/130_7a/common-model/ldv_common_model.c"
int ldv_count_1  =    0;
#line 8 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/work/current--X--drivers/hwmon/s3c-hwmon.ko--X--defaultlinux-stable-af3071a--X--130_7a--X--cpachecker/linux-stable-af3071a/csd_deg_dscv/11/dscv_tempdir/rule-instrumentor/130_7a/common-model/ldv_common_model.c"
int ldv_count_2  =    0;
#line 11 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/work/current--X--drivers/hwmon/s3c-hwmon.ko--X--defaultlinux-stable-af3071a--X--130_7a--X--cpachecker/linux-stable-af3071a/csd_deg_dscv/11/dscv_tempdir/rule-instrumentor/130_7a/common-model/ldv_common_model.c"
void ldv_sysfs(void) 
{ 


  {
#line 13
  ldv_count_1 = ldv_count_1 + 1;
#line 14
  return;
}
}
#line 18 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/work/current--X--drivers/hwmon/s3c-hwmon.ko--X--defaultlinux-stable-af3071a--X--130_7a--X--cpachecker/linux-stable-af3071a/csd_deg_dscv/11/dscv_tempdir/rule-instrumentor/130_7a/common-model/ldv_common_model.c"
int ldv_call_dev_attr_of_sensor_device_attribute  =    0;
#line 21 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/work/current--X--drivers/hwmon/s3c-hwmon.ko--X--defaultlinux-stable-af3071a--X--130_7a--X--cpachecker/linux-stable-af3071a/csd_deg_dscv/11/dscv_tempdir/rule-instrumentor/130_7a/common-model/ldv_common_model.c"
int ldv_device_create_file_dev_attr_of_sensor_device_attribute(struct device_attribute  const  *attr ) 
{ 


  {
#line 23
  if (ldv_call_dev_attr_of_sensor_device_attribute == 0) {
#line 25
    ldv_count_2 = ldv_count_2 + 1;
#line 27
    ldv_call_dev_attr_of_sensor_device_attribute = 1;
#line 29
    if (ldv_count_1 >= ldv_count_2) {

    } else {
#line 29
      ldv_error();
    }
  } else {

  }
#line 32
  return (0);
}
}
#line 37 "/work/vladimir/commit-test/commit-test-work/task-083--linux-stable--dir/work/current--X--drivers/hwmon/s3c-hwmon.ko--X--defaultlinux-stable-af3071a--X--130_7a--X--cpachecker/linux-stable-af3071a/csd_deg_dscv/11/dscv_tempdir/rule-instrumentor/130_7a/common-model/ldv_common_model.c"
void ldv_initialize(void) 
{ 


  {
#line 39
  return;
}
}
