ClabureDB

1/* Generated by CIL v. 1.3.7 */ 2/* print_CIL_Input is true */ 3 4#line 23 "include/asm-generic/int-ll64.h" 5typedef unsigned short __u16; 6#line 26 "include/asm-generic/int-ll64.h" 7typedef unsigned int __u32; 8#line 30 "include/asm-generic/int-ll64.h" 9typedef unsigned long long __u64; 10#line 45 "include/asm-generic/int-ll64.h" 11typedef short s16; 12#line 46 "include/asm-generic/int-ll64.h" 13typedef unsigned short u16; 14#line 48 "include/asm-generic/int-ll64.h" 15typedef int s32; 16#line 49 "include/asm-generic/int-ll64.h" 17typedef unsigned int u32; 18#line 51 "include/asm-generic/int-ll64.h" 19typedef long long s64; 20#line 52 "include/asm-generic/int-ll64.h" 21typedef unsigned long long u64; 22#line 14 "include/asm-generic/posix_types.h" 23typedef long __kernel_long_t; 24#line 15 "include/asm-generic/posix_types.h" 25typedef unsigned long __kernel_ulong_t; 26#line 75 "include/asm-generic/posix_types.h" 27typedef __kernel_ulong_t __kernel_size_t; 28#line 76 "include/asm-generic/posix_types.h" 29typedef __kernel_long_t __kernel_ssize_t; 30#line 91 "include/asm-generic/posix_types.h" 31typedef long long __kernel_loff_t; 32#line 21 "include/linux/types.h" 33typedef __u32 __kernel_dev_t; 34#line 24 "include/linux/types.h" 35typedef __kernel_dev_t dev_t; 36#line 27 "include/linux/types.h" 37typedef unsigned short umode_t; 38#line 38 "include/linux/types.h" 39typedef _Bool bool; 40#line 54 "include/linux/types.h" 41typedef __kernel_loff_t loff_t; 42#line 63 "include/linux/types.h" 43typedef __kernel_size_t size_t; 44#line 68 "include/linux/types.h" 45typedef __kernel_ssize_t ssize_t; 46#line 202 "include/linux/types.h" 47typedef unsigned int gfp_t; 48#line 206 "include/linux/types.h" 49typedef u64 phys_addr_t; 50#line 211 "include/linux/types.h" 51typedef phys_addr_t resource_size_t; 52#line 219 "include/linux/types.h" 53struct __anonstruct_atomic_t_7 { 54 int counter ; 55}; 56#line 219 "include/linux/types.h" 57typedef struct __anonstruct_atomic_t_7 atomic_t; 58#line 224 "include/linux/types.h" 59struct __anonstruct_atomic64_t_8 { 60 long counter ; 61}; 62#line 224 "include/linux/types.h" 63typedef struct __anonstruct_atomic64_t_8 atomic64_t; 64#line 229 "include/linux/types.h" 65struct list_head { 66 struct list_head *next ; 67 struct list_head *prev ; 68}; 69#line 56 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h" 70struct module; 71#line 56 72struct module; 73#line 146 "include/linux/init.h" 74typedef void (*ctor_fn_t)(void); 75#line 9 "include/linux/dynamic_debug.h" 76struct _ddebug { 77 char const *modname ; 78 char const *function ; 79 char const *filename ; 80 char const *format ; 81 unsigned int lineno : 18 ; 82 unsigned int flags : 8 ; 83} __attribute__((__aligned__(8))) ; 84#line 47 85struct device; 86#line 47 87struct device; 88#line 135 "include/linux/kernel.h" 89struct completion; 90#line 135 91struct completion; 92#line 10 "include/asm-generic/bug.h" 93struct bug_entry { 94 int bug_addr_disp ; 95 int file_disp ; 96 unsigned short line ; 97 unsigned short flags ; 98}; 99#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h" 100struct task_struct; 101#line 7 102struct task_struct; 103#line 282 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h" 104struct page; 105#line 295 106struct file; 107#line 295 108struct file; 109#line 46 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h" 110struct page; 111#line 52 112struct task_struct; 113#line 329 114struct arch_spinlock; 115#line 329 116struct arch_spinlock; 117#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h" 118struct task_struct; 119#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h" 120struct task_struct; 121#line 18 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page.h" 122struct page; 123#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h" 124struct static_key; 125#line 234 126struct static_key; 127#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h" 128struct kmem_cache; 129#line 23 "include/asm-generic/atomic-long.h" 130typedef atomic64_t atomic_long_t; 131#line 22 "include/linux/kref.h" 132struct kref { 133 atomic_t refcount ; 134}; 135#line 12 "include/linux/mod_devicetable.h" 136typedef unsigned long kernel_ulong_t; 137#line 219 "include/linux/mod_devicetable.h" 138struct of_device_id { 139 char name[32] ; 140 char type[32] ; 141 char compatible[128] ; 142 void *data ; 143}; 144#line 506 "include/linux/mod_devicetable.h" 145struct platform_device_id { 146 char name[20] ; 147 kernel_ulong_t driver_data __attribute__((__aligned__(sizeof(kernel_ulong_t )))) ; 148}; 149#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h" 150struct task_struct; 151#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h" 152typedef u16 __ticket_t; 153#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h" 154typedef u32 __ticketpair_t; 155#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h" 156struct __raw_tickets { 157 __ticket_t head ; 158 __ticket_t tail ; 159}; 160#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h" 161union __anonunion____missing_field_name_37 { 162 __ticketpair_t head_tail ; 163 struct __raw_tickets tickets ; 164}; 165#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h" 166struct arch_spinlock { 167 union __anonunion____missing_field_name_37 __annonCompField17 ; 168}; 169#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h" 170typedef struct arch_spinlock arch_spinlock_t; 171#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h" 172struct __anonstruct____missing_field_name_39 { 173 u32 read ; 174 s32 write ; 175}; 176#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h" 177union __anonunion_arch_rwlock_t_38 { 178 s64 lock ; 179 struct __anonstruct____missing_field_name_39 __annonCompField18 ; 180}; 181#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h" 182typedef union __anonunion_arch_rwlock_t_38 arch_rwlock_t; 183#line 12 "include/linux/lockdep.h" 184struct task_struct; 185#line 20 "include/linux/spinlock_types.h" 186struct raw_spinlock { 187 arch_spinlock_t raw_lock ; 188 unsigned int magic ; 189 unsigned int owner_cpu ; 190 void *owner ; 191}; 192#line 20 "include/linux/spinlock_types.h" 193typedef struct raw_spinlock raw_spinlock_t; 194#line 64 "include/linux/spinlock_types.h" 195union __anonunion____missing_field_name_40 { 196 struct raw_spinlock rlock ; 197}; 198#line 64 "include/linux/spinlock_types.h" 199struct spinlock { 200 union __anonunion____missing_field_name_40 __annonCompField19 ; 201}; 202#line 64 "include/linux/spinlock_types.h" 203typedef struct spinlock spinlock_t; 204#line 11 "include/linux/rwlock_types.h" 205struct __anonstruct_rwlock_t_41 { 206 arch_rwlock_t raw_lock ; 207 unsigned int magic ; 208 unsigned int owner_cpu ; 209 void *owner ; 210}; 211#line 11 "include/linux/rwlock_types.h" 212typedef struct __anonstruct_rwlock_t_41 rwlock_t; 213#line 28 "include/linux/of.h" 214typedef u32 phandle; 215#line 31 "include/linux/of.h" 216struct property { 217 char *name ; 218 int length ; 219 void *value ; 220 struct property *next ; 221 unsigned long _flags ; 222 unsigned int unique_id ; 223}; 224#line 44 225struct proc_dir_entry; 226#line 44 "include/linux/of.h" 227struct device_node { 228 char const *name ; 229 char const *type ; 230 phandle phandle ; 231 char *full_name ; 232 struct property *properties ; 233 struct property *deadprops ; 234 struct device_node *parent ; 235 struct device_node *child ; 236 struct device_node *sibling ; 237 struct device_node *next ; 238 struct device_node *allnext ; 239 struct proc_dir_entry *pde ; 240 struct kref kref ; 241 unsigned long _flags ; 242 void *data ; 243}; 244#line 44 "include/asm-generic/gpio.h" 245struct device; 246#line 47 247struct module; 248#line 48 249struct device_node; 250#line 10 "include/linux/irqreturn.h" 251enum irqreturn { 252 IRQ_NONE = 0, 253 IRQ_HANDLED = 1, 254 IRQ_WAKE_THREAD = 2 255} ; 256#line 16 "include/linux/irqreturn.h" 257typedef enum irqreturn irqreturn_t; 258#line 18 "include/linux/ioport.h" 259struct resource { 260 resource_size_t start ; 261 resource_size_t end ; 262 char const *name ; 263 unsigned long flags ; 264 struct resource *parent ; 265 struct resource *sibling ; 266 struct resource *child ; 267}; 268#line 202 269struct device; 270#line 103 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mpspec.h" 271struct device; 272#line 46 "include/linux/ktime.h" 273union ktime { 274 s64 tv64 ; 275}; 276#line 59 "include/linux/ktime.h" 277typedef union ktime ktime_t; 278#line 10 "include/linux/timer.h" 279struct tvec_base; 280#line 10 281struct tvec_base; 282#line 12 "include/linux/timer.h" 283struct timer_list { 284 struct list_head entry ; 285 unsigned long expires ; 286 struct tvec_base *base ; 287 void (*function)(unsigned long ) ; 288 unsigned long data ; 289 int slack ; 290 int start_pid ; 291 void *start_site ; 292 char start_comm[16] ; 293}; 294#line 17 "include/linux/workqueue.h" 295struct work_struct; 296#line 17 297struct work_struct; 298#line 79 "include/linux/workqueue.h" 299struct work_struct { 300 atomic_long_t data ; 301 struct list_head entry ; 302 void (*func)(struct work_struct *work ) ; 303}; 304#line 49 "include/linux/wait.h" 305struct __wait_queue_head { 306 spinlock_t lock ; 307 struct list_head task_list ; 308}; 309#line 53 "include/linux/wait.h" 310typedef struct __wait_queue_head wait_queue_head_t; 311#line 55 312struct task_struct; 313#line 25 "include/linux/completion.h" 314struct completion { 315 unsigned int done ; 316 wait_queue_head_t wait ; 317}; 318#line 42 "include/linux/pm.h" 319struct device; 320#line 50 "include/linux/pm.h" 321struct pm_message { 322 int event ; 323}; 324#line 50 "include/linux/pm.h" 325typedef struct pm_message pm_message_t; 326#line 264 "include/linux/pm.h" 327struct dev_pm_ops { 328 int (*prepare)(struct device *dev ) ; 329 void (*complete)(struct device *dev ) ; 330 int (*suspend)(struct device *dev ) ; 331 int (*resume)(struct device *dev ) ; 332 int (*freeze)(struct device *dev ) ; 333 int (*thaw)(struct device *dev ) ; 334 int (*poweroff)(struct device *dev ) ; 335 int (*restore)(struct device *dev ) ; 336 int (*suspend_late)(struct device *dev ) ; 337 int (*resume_early)(struct device *dev ) ; 338 int (*freeze_late)(struct device *dev ) ; 339 int (*thaw_early)(struct device *dev ) ; 340 int (*poweroff_late)(struct device *dev ) ; 341 int (*restore_early)(struct device *dev ) ; 342 int (*suspend_noirq)(struct device *dev ) ; 343 int (*resume_noirq)(struct device *dev ) ; 344 int (*freeze_noirq)(struct device *dev ) ; 345 int (*thaw_noirq)(struct device *dev ) ; 346 int (*poweroff_noirq)(struct device *dev ) ; 347 int (*restore_noirq)(struct device *dev ) ; 348 int (*runtime_suspend)(struct device *dev ) ; 349 int (*runtime_resume)(struct device *dev ) ; 350 int (*runtime_idle)(struct device *dev ) ; 351}; 352#line 458 353enum rpm_status { 354 RPM_ACTIVE = 0, 355 RPM_RESUMING = 1, 356 RPM_SUSPENDED = 2, 357 RPM_SUSPENDING = 3 358} ; 359#line 480 360enum rpm_request { 361 RPM_REQ_NONE = 0, 362 RPM_REQ_IDLE = 1, 363 RPM_REQ_SUSPEND = 2, 364 RPM_REQ_AUTOSUSPEND = 3, 365 RPM_REQ_RESUME = 4 366} ; 367#line 488 368struct wakeup_source; 369#line 488 370struct wakeup_source; 371#line 495 "include/linux/pm.h" 372struct pm_subsys_data { 373 spinlock_t lock ; 374 unsigned int refcount ; 375}; 376#line 506 377struct dev_pm_qos_request; 378#line 506 379struct pm_qos_constraints; 380#line 506 "include/linux/pm.h" 381struct dev_pm_info { 382 pm_message_t power_state ; 383 unsigned int can_wakeup : 1 ; 384 unsigned int async_suspend : 1 ; 385 bool is_prepared : 1 ; 386 bool is_suspended : 1 ; 387 bool ignore_children : 1 ; 388 spinlock_t lock ; 389 struct list_head entry ; 390 struct completion completion ; 391 struct wakeup_source *wakeup ; 392 bool wakeup_path : 1 ; 393 struct timer_list suspend_timer ; 394 unsigned long timer_expires ; 395 struct work_struct work ; 396 wait_queue_head_t wait_queue ; 397 atomic_t usage_count ; 398 atomic_t child_count ; 399 unsigned int disable_depth : 3 ; 400 unsigned int idle_notification : 1 ; 401 unsigned int request_pending : 1 ; 402 unsigned int deferred_resume : 1 ; 403 unsigned int run_wake : 1 ; 404 unsigned int runtime_auto : 1 ; 405 unsigned int no_callbacks : 1 ; 406 unsigned int irq_safe : 1 ; 407 unsigned int use_autosuspend : 1 ; 408 unsigned int timer_autosuspends : 1 ; 409 enum rpm_request request ; 410 enum rpm_status runtime_status ; 411 int runtime_error ; 412 int autosuspend_delay ; 413 unsigned long last_busy ; 414 unsigned long active_jiffies ; 415 unsigned long suspended_jiffies ; 416 unsigned long accounting_timestamp ; 417 ktime_t suspend_time ; 418 s64 max_time_suspended_ns ; 419 struct dev_pm_qos_request *pq_req ; 420 struct pm_subsys_data *subsys_data ; 421 struct pm_qos_constraints *constraints ; 422}; 423#line 564 "include/linux/pm.h" 424struct dev_pm_domain { 425 struct dev_pm_ops ops ; 426}; 427#line 48 "include/linux/mutex.h" 428struct mutex { 429 atomic_t count ; 430 spinlock_t wait_lock ; 431 struct list_head wait_list ; 432 struct task_struct *owner ; 433 char const *name ; 434 void *magic ; 435}; 436#line 8 "include/linux/vmalloc.h" 437struct vm_area_struct; 438#line 8 439struct vm_area_struct; 440#line 60 "include/linux/pageblock-flags.h" 441struct page; 442#line 19 "include/linux/rwsem.h" 443struct rw_semaphore; 444#line 19 445struct rw_semaphore; 446#line 25 "include/linux/rwsem.h" 447struct rw_semaphore { 448 long count ; 449 raw_spinlock_t wait_lock ; 450 struct list_head wait_list ; 451}; 452#line 9 "include/linux/memory_hotplug.h" 453struct page; 454#line 994 "include/linux/mmzone.h" 455struct page; 456#line 10 "include/linux/gfp.h" 457struct vm_area_struct; 458#line 32 "include/linux/irq.h" 459struct module; 460#line 12 "include/linux/irqdesc.h" 461struct proc_dir_entry; 462#line 14 463struct module; 464#line 16 "include/linux/profile.h" 465struct proc_dir_entry; 466#line 65 467struct task_struct; 468#line 94 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/uaccess.h" 469struct exception_table_entry { 470 unsigned long insn ; 471 unsigned long fixup ; 472}; 473#line 132 "include/linux/hardirq.h" 474struct task_struct; 475#line 187 "include/linux/interrupt.h" 476struct device; 477#line 29 "include/linux/sysctl.h" 478struct completion; 479#line 49 "include/linux/kmod.h" 480struct file; 481#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h" 482struct task_struct; 483#line 18 "include/linux/elf.h" 484typedef __u64 Elf64_Addr; 485#line 19 "include/linux/elf.h" 486typedef __u16 Elf64_Half; 487#line 23 "include/linux/elf.h" 488typedef __u32 Elf64_Word; 489#line 24 "include/linux/elf.h" 490typedef __u64 Elf64_Xword; 491#line 194 "include/linux/elf.h" 492struct elf64_sym { 493 Elf64_Word st_name ; 494 unsigned char st_info ; 495 unsigned char st_other ; 496 Elf64_Half st_shndx ; 497 Elf64_Addr st_value ; 498 Elf64_Xword st_size ; 499}; 500#line 194 "include/linux/elf.h" 501typedef struct elf64_sym Elf64_Sym; 502#line 438 503struct file; 504#line 20 "include/linux/kobject_ns.h" 505struct sock; 506#line 20 507struct sock; 508#line 21 509struct kobject; 510#line 21 511struct kobject; 512#line 27 513enum kobj_ns_type { 514 KOBJ_NS_TYPE_NONE = 0, 515 KOBJ_NS_TYPE_NET = 1, 516 KOBJ_NS_TYPES = 2 517} ; 518#line 40 "include/linux/kobject_ns.h" 519struct kobj_ns_type_operations { 520 enum kobj_ns_type type ; 521 void *(*grab_current_ns)(void) ; 522 void const *(*netlink_ns)(struct sock *sk ) ; 523 void const *(*initial_ns)(void) ; 524 void (*drop_ns)(void * ) ; 525}; 526#line 22 "include/linux/sysfs.h" 527struct kobject; 528#line 23 529struct module; 530#line 24 531enum kobj_ns_type; 532#line 26 "include/linux/sysfs.h" 533struct attribute { 534 char const *name ; 535 umode_t mode ; 536}; 537#line 56 "include/linux/sysfs.h" 538struct attribute_group { 539 char const *name ; 540 umode_t (*is_visible)(struct kobject * , struct attribute * , int ) ; 541 struct attribute **attrs ; 542}; 543#line 85 544struct file; 545#line 86 546struct vm_area_struct; 547#line 88 "include/linux/sysfs.h" 548struct bin_attribute { 549 struct attribute attr ; 550 size_t size ; 551 void *private ; 552 ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * , 553 loff_t , size_t ) ; 554 ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * , 555 loff_t , size_t ) ; 556 int (*mmap)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ) ; 557}; 558#line 112 "include/linux/sysfs.h" 559struct sysfs_ops { 560 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ; 561 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ; 562 void const *(*namespace)(struct kobject * , struct attribute const * ) ; 563}; 564#line 118 565struct sysfs_dirent; 566#line 118 567struct sysfs_dirent; 568#line 60 "include/linux/kobject.h" 569struct kset; 570#line 60 571struct kobj_type; 572#line 60 "include/linux/kobject.h" 573struct kobject { 574 char const *name ; 575 struct list_head entry ; 576 struct kobject *parent ; 577 struct kset *kset ; 578 struct kobj_type *ktype ; 579 struct sysfs_dirent *sd ; 580 struct kref kref ; 581 unsigned int state_initialized : 1 ; 582 unsigned int state_in_sysfs : 1 ; 583 unsigned int state_add_uevent_sent : 1 ; 584 unsigned int state_remove_uevent_sent : 1 ; 585 unsigned int uevent_suppress : 1 ; 586}; 587#line 108 "include/linux/kobject.h" 588struct kobj_type { 589 void (*release)(struct kobject *kobj ) ; 590 struct sysfs_ops const *sysfs_ops ; 591 struct attribute **default_attrs ; 592 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject *kobj ) ; 593 void const *(*namespace)(struct kobject *kobj ) ; 594}; 595#line 116 "include/linux/kobject.h" 596struct kobj_uevent_env { 597 char *envp[32] ; 598 int envp_idx ; 599 char buf[2048] ; 600 int buflen ; 601}; 602#line 123 "include/linux/kobject.h" 603struct kset_uevent_ops { 604 int (* const filter)(struct kset *kset , struct kobject *kobj ) ; 605 char const *(* const name)(struct kset *kset , struct kobject *kobj ) ; 606 int (* const uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ; 607}; 608#line 140 609struct sock; 610#line 159 "include/linux/kobject.h" 611struct kset { 612 struct list_head list ; 613 spinlock_t list_lock ; 614 struct kobject kobj ; 615 struct kset_uevent_ops const *uevent_ops ; 616}; 617#line 39 "include/linux/moduleparam.h" 618struct kernel_param; 619#line 39 620struct kernel_param; 621#line 41 "include/linux/moduleparam.h" 622struct kernel_param_ops { 623 int (*set)(char const *val , struct kernel_param const *kp ) ; 624 int (*get)(char *buffer , struct kernel_param const *kp ) ; 625 void (*free)(void *arg ) ; 626}; 627#line 50 628struct kparam_string; 629#line 50 630struct kparam_array; 631#line 50 "include/linux/moduleparam.h" 632union __anonunion____missing_field_name_208 { 633 void *arg ; 634 struct kparam_string const *str ; 635 struct kparam_array const *arr ; 636}; 637#line 50 "include/linux/moduleparam.h" 638struct kernel_param { 639 char const *name ; 640 struct kernel_param_ops const *ops ; 641 u16 perm ; 642 s16 level ; 643 union __anonunion____missing_field_name_208 __annonCompField32 ; 644}; 645#line 63 "include/linux/moduleparam.h" 646struct kparam_string { 647 unsigned int maxlen ; 648 char *string ; 649}; 650#line 69 "include/linux/moduleparam.h" 651struct kparam_array { 652 unsigned int max ; 653 unsigned int elemsize ; 654 unsigned int *num ; 655 struct kernel_param_ops const *ops ; 656 void *elem ; 657}; 658#line 445 659struct module; 660#line 80 "include/linux/jump_label.h" 661struct module; 662#line 143 "include/linux/jump_label.h" 663struct static_key { 664 atomic_t enabled ; 665}; 666#line 22 "include/linux/tracepoint.h" 667struct module; 668#line 23 669struct tracepoint; 670#line 23 671struct tracepoint; 672#line 25 "include/linux/tracepoint.h" 673struct tracepoint_func { 674 void *func ; 675 void *data ; 676}; 677#line 30 "include/linux/tracepoint.h" 678struct tracepoint { 679 char const *name ; 680 struct static_key key ; 681 void (*regfunc)(void) ; 682 void (*unregfunc)(void) ; 683 struct tracepoint_func *funcs ; 684}; 685#line 19 "include/linux/export.h" 686struct kernel_symbol { 687 unsigned long value ; 688 char const *name ; 689}; 690#line 8 "include/asm-generic/module.h" 691struct mod_arch_specific { 692 693}; 694#line 35 "include/linux/module.h" 695struct module; 696#line 37 697struct module_param_attrs; 698#line 37 "include/linux/module.h" 699struct module_kobject { 700 struct kobject kobj ; 701 struct module *mod ; 702 struct kobject *drivers_dir ; 703 struct module_param_attrs *mp ; 704}; 705#line 44 "include/linux/module.h" 706struct module_attribute { 707 struct attribute attr ; 708 ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ; 709 ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const * , 710 size_t count ) ; 711 void (*setup)(struct module * , char const * ) ; 712 int (*test)(struct module * ) ; 713 void (*free)(struct module * ) ; 714}; 715#line 71 716struct exception_table_entry; 717#line 199 718enum module_state { 719 MODULE_STATE_LIVE = 0, 720 MODULE_STATE_COMING = 1, 721 MODULE_STATE_GOING = 2 722} ; 723#line 215 "include/linux/module.h" 724struct module_ref { 725 unsigned long incs ; 726 unsigned long decs ; 727} __attribute__((__aligned__((2) * (sizeof(unsigned long )) ))) ; 728#line 220 729struct module_sect_attrs; 730#line 220 731struct module_notes_attrs; 732#line 220 733struct ftrace_event_call; 734#line 220 "include/linux/module.h" 735struct module { 736 enum module_state state ; 737 struct list_head list ; 738 char name[64UL - sizeof(unsigned long )] ; 739 struct module_kobject mkobj ; 740 struct module_attribute *modinfo_attrs ; 741 char const *version ; 742 char const *srcversion ; 743 struct kobject *holders_dir ; 744 struct kernel_symbol const *syms ; 745 unsigned long const *crcs ; 746 unsigned int num_syms ; 747 struct kernel_param *kp ; 748 unsigned int num_kp ; 749 unsigned int num_gpl_syms ; 750 struct kernel_symbol const *gpl_syms ; 751 unsigned long const *gpl_crcs ; 752 struct kernel_symbol const *unused_syms ; 753 unsigned long const *unused_crcs ; 754 unsigned int num_unused_syms ; 755 unsigned int num_unused_gpl_syms ; 756 struct kernel_symbol const *unused_gpl_syms ; 757 unsigned long const *unused_gpl_crcs ; 758 struct kernel_symbol const *gpl_future_syms ; 759 unsigned long const *gpl_future_crcs ; 760 unsigned int num_gpl_future_syms ; 761 unsigned int num_exentries ; 762 struct exception_table_entry *extable ; 763 int (*init)(void) ; 764 void *module_init ; 765 void *module_core ; 766 unsigned int init_size ; 767 unsigned int core_size ; 768 unsigned int init_text_size ; 769 unsigned int core_text_size ; 770 unsigned int init_ro_size ; 771 unsigned int core_ro_size ; 772 struct mod_arch_specific arch ; 773 unsigned int taints ; 774 unsigned int num_bugs ; 775 struct list_head bug_list ; 776 struct bug_entry *bug_table ; 777 Elf64_Sym *symtab ; 778 Elf64_Sym *core_symtab ; 779 unsigned int num_symtab ; 780 unsigned int core_num_syms ; 781 char *strtab ; 782 char *core_strtab ; 783 struct module_sect_attrs *sect_attrs ; 784 struct module_notes_attrs *notes_attrs ; 785 char *args ; 786 void *percpu ; 787 unsigned int percpu_size ; 788 unsigned int num_tracepoints ; 789 struct tracepoint * const *tracepoints_ptrs ; 790 unsigned int num_trace_bprintk_fmt ; 791 char const **trace_bprintk_fmt_start ; 792 struct ftrace_event_call **trace_events ; 793 unsigned int num_trace_events ; 794 struct list_head source_list ; 795 struct list_head target_list ; 796 struct task_struct *waiter ; 797 void (*exit)(void) ; 798 struct module_ref *refptr ; 799 ctor_fn_t *ctors ; 800 unsigned int num_ctors ; 801}; 802#line 46 "include/linux/slub_def.h" 803struct kmem_cache_cpu { 804 void **freelist ; 805 unsigned long tid ; 806 struct page *page ; 807 struct page *partial ; 808 int node ; 809 unsigned int stat[26] ; 810}; 811#line 57 "include/linux/slub_def.h" 812struct kmem_cache_node { 813 spinlock_t list_lock ; 814 unsigned long nr_partial ; 815 struct list_head partial ; 816 atomic_long_t nr_slabs ; 817 atomic_long_t total_objects ; 818 struct list_head full ; 819}; 820#line 73 "include/linux/slub_def.h" 821struct kmem_cache_order_objects { 822 unsigned long x ; 823}; 824#line 80 "include/linux/slub_def.h" 825struct kmem_cache { 826 struct kmem_cache_cpu *cpu_slab ; 827 unsigned long flags ; 828 unsigned long min_partial ; 829 int size ; 830 int objsize ; 831 int offset ; 832 int cpu_partial ; 833 struct kmem_cache_order_objects oo ; 834 struct kmem_cache_order_objects max ; 835 struct kmem_cache_order_objects min ; 836 gfp_t allocflags ; 837 int refcount ; 838 void (*ctor)(void * ) ; 839 int inuse ; 840 int align ; 841 int reserved ; 842 char const *name ; 843 struct list_head list ; 844 struct kobject kobj ; 845 int remote_node_defrag_ratio ; 846 struct kmem_cache_node *node[1 << 10] ; 847}; 848#line 20 "include/linux/leds.h" 849struct device; 850#line 25 851enum led_brightness { 852 LED_OFF = 0, 853 LED_HALF = 127, 854 LED_FULL = 255 855} ; 856#line 31 857struct led_trigger; 858#line 31 "include/linux/leds.h" 859struct led_classdev { 860 char const *name ; 861 int brightness ; 862 int max_brightness ; 863 int flags ; 864 void (*brightness_set)(struct led_classdev *led_cdev , enum led_brightness brightness ) ; 865 enum led_brightness (*brightness_get)(struct led_classdev *led_cdev ) ; 866 int (*blink_set)(struct led_classdev *led_cdev , unsigned long *delay_on , unsigned long *delay_off ) ; 867 struct device *dev ; 868 struct list_head node ; 869 char const *default_trigger ; 870 unsigned long blink_delay_on ; 871 unsigned long blink_delay_off ; 872 struct timer_list blink_timer ; 873 int blink_brightness ; 874 struct rw_semaphore trigger_lock ; 875 struct led_trigger *trigger ; 876 struct list_head trig_list ; 877 void *trigger_data ; 878}; 879#line 122 "include/linux/leds.h" 880struct led_trigger { 881 char const *name ; 882 void (*activate)(struct led_classdev *led_cdev ) ; 883 void (*deactivate)(struct led_classdev *led_cdev ) ; 884 rwlock_t leddev_list_lock ; 885 struct list_head led_cdevs ; 886 struct list_head next_trig ; 887}; 888#line 210 889struct platform_device; 890#line 19 "include/linux/power_supply.h" 891struct device; 892#line 84 893enum power_supply_property { 894 POWER_SUPPLY_PROP_STATUS = 0, 895 POWER_SUPPLY_PROP_CHARGE_TYPE = 1, 896 POWER_SUPPLY_PROP_HEALTH = 2, 897 POWER_SUPPLY_PROP_PRESENT = 3, 898 POWER_SUPPLY_PROP_ONLINE = 4, 899 POWER_SUPPLY_PROP_TECHNOLOGY = 5, 900 POWER_SUPPLY_PROP_CYCLE_COUNT = 6, 901 POWER_SUPPLY_PROP_VOLTAGE_MAX = 7, 902 POWER_SUPPLY_PROP_VOLTAGE_MIN = 8, 903 POWER_SUPPLY_PROP_VOLTAGE_MAX_DESIGN = 9, 904 POWER_SUPPLY_PROP_VOLTAGE_MIN_DESIGN = 10, 905 POWER_SUPPLY_PROP_VOLTAGE_NOW = 11, 906 POWER_SUPPLY_PROP_VOLTAGE_AVG = 12, 907 POWER_SUPPLY_PROP_CURRENT_MAX = 13, 908 POWER_SUPPLY_PROP_CURRENT_NOW = 14, 909 POWER_SUPPLY_PROP_CURRENT_AVG = 15, 910 POWER_SUPPLY_PROP_POWER_NOW = 16, 911 POWER_SUPPLY_PROP_POWER_AVG = 17, 912 POWER_SUPPLY_PROP_CHARGE_FULL_DESIGN = 18, 913 POWER_SUPPLY_PROP_CHARGE_EMPTY_DESIGN = 19, 914 POWER_SUPPLY_PROP_CHARGE_FULL = 20, 915 POWER_SUPPLY_PROP_CHARGE_EMPTY = 21, 916 POWER_SUPPLY_PROP_CHARGE_NOW = 22, 917 POWER_SUPPLY_PROP_CHARGE_AVG = 23, 918 POWER_SUPPLY_PROP_CHARGE_COUNTER = 24, 919 POWER_SUPPLY_PROP_ENERGY_FULL_DESIGN = 25, 920 POWER_SUPPLY_PROP_ENERGY_EMPTY_DESIGN = 26, 921 POWER_SUPPLY_PROP_ENERGY_FULL = 27, 922 POWER_SUPPLY_PROP_ENERGY_EMPTY = 28, 923 POWER_SUPPLY_PROP_ENERGY_NOW = 29, 924 POWER_SUPPLY_PROP_ENERGY_AVG = 30, 925 POWER_SUPPLY_PROP_CAPACITY = 31, 926 POWER_SUPPLY_PROP_CAPACITY_LEVEL = 32, 927 POWER_SUPPLY_PROP_TEMP = 33, 928 POWER_SUPPLY_PROP_TEMP_AMBIENT = 34, 929 POWER_SUPPLY_PROP_TIME_TO_EMPTY_NOW = 35, 930 POWER_SUPPLY_PROP_TIME_TO_EMPTY_AVG = 36, 931 POWER_SUPPLY_PROP_TIME_TO_FULL_NOW = 37, 932 POWER_SUPPLY_PROP_TIME_TO_FULL_AVG = 38, 933 POWER_SUPPLY_PROP_TYPE = 39, 934 POWER_SUPPLY_PROP_SCOPE = 40, 935 POWER_SUPPLY_PROP_MODEL_NAME = 41, 936 POWER_SUPPLY_PROP_MANUFACTURER = 42, 937 POWER_SUPPLY_PROP_SERIAL_NUMBER = 43 938} ; 939#line 133 940enum power_supply_type { 941 POWER_SUPPLY_TYPE_UNKNOWN = 0, 942 POWER_SUPPLY_TYPE_BATTERY = 1, 943 POWER_SUPPLY_TYPE_UPS = 2, 944 POWER_SUPPLY_TYPE_MAINS = 3, 945 POWER_SUPPLY_TYPE_USB = 4, 946 POWER_SUPPLY_TYPE_USB_DCP = 5, 947 POWER_SUPPLY_TYPE_USB_CDP = 6, 948 POWER_SUPPLY_TYPE_USB_ACA = 7 949} ; 950#line 144 "include/linux/power_supply.h" 951union power_supply_propval { 952 int intval ; 953 char const *strval ; 954}; 955#line 149 "include/linux/power_supply.h" 956struct power_supply { 957 char const *name ; 958 enum power_supply_type type ; 959 enum power_supply_property *properties ; 960 size_t num_properties ; 961 char **supplied_to ; 962 size_t num_supplicants ; 963 int (*get_property)(struct power_supply *psy , enum power_supply_property psp , 964 union power_supply_propval *val ) ; 965 int (*set_property)(struct power_supply *psy , enum power_supply_property psp , 966 union power_supply_propval const *val ) ; 967 int (*property_is_writeable)(struct power_supply *psy , enum power_supply_property psp ) ; 968 void (*external_power_changed)(struct power_supply *psy ) ; 969 void (*set_charged)(struct power_supply *psy ) ; 970 int use_for_apm ; 971 struct device *dev ; 972 struct work_struct changed_work ; 973 struct led_trigger *charging_full_trig ; 974 char *charging_full_trig_name ; 975 struct led_trigger *charging_trig ; 976 char *charging_trig_name ; 977 struct led_trigger *full_trig ; 978 char *full_trig_name ; 979 struct led_trigger *online_trig ; 980 char *online_trig_name ; 981 struct led_trigger *charging_blink_full_solid_trig ; 982 char *charging_blink_full_solid_trig_name ; 983}; 984#line 226 985struct class; 986#line 19 "include/linux/klist.h" 987struct klist_node; 988#line 19 989struct klist_node; 990#line 39 "include/linux/klist.h" 991struct klist_node { 992 void *n_klist ; 993 struct list_head n_node ; 994 struct kref n_ref ; 995}; 996#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h" 997struct dma_map_ops; 998#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h" 999struct dev_archdata { 1000 void *acpi_handle ; 1001 struct dma_map_ops *dma_ops ; 1002 void *iommu ; 1003}; 1004#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h" 1005struct pdev_archdata { 1006 1007}; 1008#line 28 "include/linux/device.h" 1009struct device; 1010#line 29 1011struct device_private; 1012#line 29 1013struct device_private; 1014#line 30 1015struct device_driver; 1016#line 30 1017struct device_driver; 1018#line 31 1019struct driver_private; 1020#line 31 1021struct driver_private; 1022#line 32 1023struct module; 1024#line 33 1025struct class; 1026#line 34 1027struct subsys_private; 1028#line 34 1029struct subsys_private; 1030#line 35 1031struct bus_type; 1032#line 35 1033struct bus_type; 1034#line 36 1035struct device_node; 1036#line 37 1037struct iommu_ops; 1038#line 37 1039struct iommu_ops; 1040#line 39 "include/linux/device.h" 1041struct bus_attribute { 1042 struct attribute attr ; 1043 ssize_t (*show)(struct bus_type *bus , char *buf ) ; 1044 ssize_t (*store)(struct bus_type *bus , char const *buf , size_t count ) ; 1045}; 1046#line 89 1047struct device_attribute; 1048#line 89 1049struct driver_attribute; 1050#line 89 "include/linux/device.h" 1051struct bus_type { 1052 char const *name ; 1053 char const *dev_name ; 1054 struct device *dev_root ; 1055 struct bus_attribute *bus_attrs ; 1056 struct device_attribute *dev_attrs ; 1057 struct driver_attribute *drv_attrs ; 1058 int (*match)(struct device *dev , struct device_driver *drv ) ; 1059 int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ; 1060 int (*probe)(struct device *dev ) ; 1061 int (*remove)(struct device *dev ) ; 1062 void (*shutdown)(struct device *dev ) ; 1063 int (*suspend)(struct device *dev , pm_message_t state ) ; 1064 int (*resume)(struct device *dev ) ; 1065 struct dev_pm_ops const *pm ; 1066 struct iommu_ops *iommu_ops ; 1067 struct subsys_private *p ; 1068}; 1069#line 127 1070struct device_type; 1071#line 214 "include/linux/device.h" 1072struct device_driver { 1073 char const *name ; 1074 struct bus_type *bus ; 1075 struct module *owner ; 1076 char const *mod_name ; 1077 bool suppress_bind_attrs ; 1078 struct of_device_id const *of_match_table ; 1079 int (*probe)(struct device *dev ) ; 1080 int (*remove)(struct device *dev ) ; 1081 void (*shutdown)(struct device *dev ) ; 1082 int (*suspend)(struct device *dev , pm_message_t state ) ; 1083 int (*resume)(struct device *dev ) ; 1084 struct attribute_group const **groups ; 1085 struct dev_pm_ops const *pm ; 1086 struct driver_private *p ; 1087}; 1088#line 249 "include/linux/device.h" 1089struct driver_attribute { 1090 struct attribute attr ; 1091 ssize_t (*show)(struct device_driver *driver , char *buf ) ; 1092 ssize_t (*store)(struct device_driver *driver , char const *buf , size_t count ) ; 1093}; 1094#line 330 1095struct class_attribute; 1096#line 330 "include/linux/device.h" 1097struct class { 1098 char const *name ; 1099 struct module *owner ; 1100 struct class_attribute *class_attrs ; 1101 struct device_attribute *dev_attrs ; 1102 struct bin_attribute *dev_bin_attrs ; 1103 struct kobject *dev_kobj ; 1104 int (*dev_uevent)(struct device *dev , struct kobj_uevent_env *env ) ; 1105 char *(*devnode)(struct device *dev , umode_t *mode ) ; 1106 void (*class_release)(struct class *class ) ; 1107 void (*dev_release)(struct device *dev ) ; 1108 int (*suspend)(struct device *dev , pm_message_t state ) ; 1109 int (*resume)(struct device *dev ) ; 1110 struct kobj_ns_type_operations const *ns_type ; 1111 void const *(*namespace)(struct device *dev ) ; 1112 struct dev_pm_ops const *pm ; 1113 struct subsys_private *p ; 1114}; 1115#line 397 "include/linux/device.h" 1116struct class_attribute { 1117 struct attribute attr ; 1118 ssize_t (*show)(struct class *class , struct class_attribute *attr , char *buf ) ; 1119 ssize_t (*store)(struct class *class , struct class_attribute *attr , char const *buf , 1120 size_t count ) ; 1121 void const *(*namespace)(struct class *class , struct class_attribute const *attr ) ; 1122}; 1123#line 465 "include/linux/device.h" 1124struct device_type { 1125 char const *name ; 1126 struct attribute_group const **groups ; 1127 int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ; 1128 char *(*devnode)(struct device *dev , umode_t *mode ) ; 1129 void (*release)(struct device *dev ) ; 1130 struct dev_pm_ops const *pm ; 1131}; 1132#line 476 "include/linux/device.h" 1133struct device_attribute { 1134 struct attribute attr ; 1135 ssize_t (*show)(struct device *dev , struct device_attribute *attr , char *buf ) ; 1136 ssize_t (*store)(struct device *dev , struct device_attribute *attr , char const *buf , 1137 size_t count ) ; 1138}; 1139#line 559 "include/linux/device.h" 1140struct device_dma_parameters { 1141 unsigned int max_segment_size ; 1142 unsigned long segment_boundary_mask ; 1143}; 1144#line 627 1145struct dma_coherent_mem; 1146#line 627 "include/linux/device.h" 1147struct device { 1148 struct device *parent ; 1149 struct device_private *p ; 1150 struct kobject kobj ; 1151 char const *init_name ; 1152 struct device_type const *type ; 1153 struct mutex mutex ; 1154 struct bus_type *bus ; 1155 struct device_driver *driver ; 1156 void *platform_data ; 1157 struct dev_pm_info power ; 1158 struct dev_pm_domain *pm_domain ; 1159 int numa_node ; 1160 u64 *dma_mask ; 1161 u64 coherent_dma_mask ; 1162 struct device_dma_parameters *dma_parms ; 1163 struct list_head dma_pools ; 1164 struct dma_coherent_mem *dma_mem ; 1165 struct dev_archdata archdata ; 1166 struct device_node *of_node ; 1167 dev_t devt ; 1168 u32 id ; 1169 spinlock_t devres_lock ; 1170 struct list_head devres_head ; 1171 struct klist_node knode_class ; 1172 struct class *class ; 1173 struct attribute_group const **groups ; 1174 void (*release)(struct device *dev ) ; 1175}; 1176#line 43 "include/linux/pm_wakeup.h" 1177struct wakeup_source { 1178 char const *name ; 1179 struct list_head entry ; 1180 spinlock_t lock ; 1181 struct timer_list timer ; 1182 unsigned long timer_expires ; 1183 ktime_t total_time ; 1184 ktime_t max_time ; 1185 ktime_t last_time ; 1186 unsigned long event_count ; 1187 unsigned long active_count ; 1188 unsigned long relax_count ; 1189 unsigned long hit_count ; 1190 unsigned int active : 1 ; 1191}; 1192#line 17 "include/linux/platform_device.h" 1193struct mfd_cell; 1194#line 17 1195struct mfd_cell; 1196#line 19 "include/linux/platform_device.h" 1197struct platform_device { 1198 char const *name ; 1199 int id ; 1200 struct device dev ; 1201 u32 num_resources ; 1202 struct resource *resource ; 1203 struct platform_device_id const *id_entry ; 1204 struct mfd_cell *mfd_cell ; 1205 struct pdev_archdata archdata ; 1206}; 1207#line 164 "include/linux/platform_device.h" 1208struct platform_driver { 1209 int (*probe)(struct platform_device * ) ; 1210 int (*remove)(struct platform_device * ) ; 1211 void (*shutdown)(struct platform_device * ) ; 1212 int (*suspend)(struct platform_device * , pm_message_t state ) ; 1213 int (*resume)(struct platform_device * ) ; 1214 struct device_driver driver ; 1215 struct platform_device_id const *id_table ; 1216}; 1217#line 26 "include/linux/power/max8903_charger.h" 1218struct max8903_pdata { 1219 int cen ; 1220 int dok ; 1221 int uok ; 1222 int chg ; 1223 int flt ; 1224 int dcm ; 1225 int usus ; 1226 bool dc_valid ; 1227 bool usb_valid ; 1228}; 1229#line 32 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/drivers/power/max8903_charger.c.common.c" 1230struct max8903_data { 1231 struct max8903_pdata pdata ; 1232 struct device *dev ; 1233 struct power_supply psy ; 1234 bool fault ; 1235 bool usb_in ; 1236 bool ta_in ; 1237}; 1238#line 290 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/drivers/power/max8903_charger.c.common.c" 1239struct __anonstruct_216 { 1240 int : 0 ; 1241}; 1242#line 1 "<compiler builtins>" 1243 1244#line 1 1245long __builtin_expect(long val , long res ) ; 1246#line 49 "include/linux/dynamic_debug.h" 1247extern int ( /* format attribute */ __dynamic_dev_dbg)(struct _ddebug *descriptor , 1248 struct device const *dev , 1249 char const *fmt , ...) ; 1250#line 34 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/string_64.h" 1251extern void *__memcpy(void *to , void const *from , size_t len ) ; 1252#line 39 "include/asm-generic/gpio.h" 1253__inline static bool gpio_is_valid(int number ) __attribute__((__no_instrument_function__)) ; 1254#line 39 "include/asm-generic/gpio.h" 1255__inline static bool gpio_is_valid(int number ) 1256{ int tmp ; 1257 1258 { 1259#line 41 1260 if (number >= 0) { 1261#line 41 1262 if (number < 256) { 1263#line 41 1264 tmp = 1; 1265 } else { 1266#line 41 1267 tmp = 0; 1268 } 1269 } else { 1270#line 41 1271 tmp = 0; 1272 } 1273#line 41 1274 return ((bool )tmp); 1275} 1276} 1277#line 169 1278extern int __gpio_get_value(unsigned int gpio ) ; 1279#line 170 1280extern void __gpio_set_value(unsigned int gpio , int value ) ; 1281#line 174 1282extern int __gpio_to_irq(unsigned int gpio ) ; 1283#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/gpio.h" 1284__inline static int gpio_get_value(unsigned int gpio ) __attribute__((__no_instrument_function__)) ; 1285#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/gpio.h" 1286__inline static int gpio_get_value(unsigned int gpio ) 1287{ int tmp ; 1288 1289 { 1290 { 1291#line 28 1292 tmp = __gpio_get_value(gpio); 1293 } 1294#line 28 1295 return (tmp); 1296} 1297} 1298#line 31 1299__inline static void gpio_set_value(unsigned int gpio , int value ) __attribute__((__no_instrument_function__)) ; 1300#line 31 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/gpio.h" 1301__inline static void gpio_set_value(unsigned int gpio , int value ) 1302{ 1303 1304 { 1305 { 1306#line 33 1307 __gpio_set_value(gpio, value); 1308 } 1309#line 34 1310 return; 1311} 1312} 1313#line 41 1314__inline static int gpio_to_irq(unsigned int gpio ) __attribute__((__no_instrument_function__)) ; 1315#line 41 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/gpio.h" 1316__inline static int gpio_to_irq(unsigned int gpio ) 1317{ int tmp ; 1318 1319 { 1320 { 1321#line 43 1322 tmp = __gpio_to_irq(gpio); 1323 } 1324#line 43 1325 return (tmp); 1326} 1327} 1328#line 152 "include/linux/mutex.h" 1329void mutex_lock(struct mutex *lock ) ; 1330#line 153 1331int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock ) ; 1332#line 154 1333int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock ) ; 1334#line 168 1335int mutex_trylock(struct mutex *lock ) ; 1336#line 169 1337void mutex_unlock(struct mutex *lock ) ; 1338#line 170 1339int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ; 1340#line 126 "include/linux/interrupt.h" 1341extern int __attribute__((__warn_unused_result__)) request_threaded_irq(unsigned int irq , 1342 irqreturn_t (*handler)(int , 1343 void * ) , 1344 irqreturn_t (*thread_fn)(int , 1345 void * ) , 1346 unsigned long flags , 1347 char const *name , 1348 void *dev ) ; 1349#line 184 1350extern void free_irq(unsigned int , void * ) ; 1351#line 26 "include/linux/export.h" 1352extern struct module __this_module ; 1353#line 67 "include/linux/module.h" 1354int init_module(void) ; 1355#line 68 1356void cleanup_module(void) ; 1357#line 161 "include/linux/slab.h" 1358extern void kfree(void const * ) ; 1359#line 221 "include/linux/slub_def.h" 1360extern void *__kmalloc(size_t size , gfp_t flags ) ; 1361#line 268 1362__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size , 1363 gfp_t flags ) __attribute__((__no_instrument_function__)) ; 1364#line 268 "include/linux/slub_def.h" 1365__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size , 1366 gfp_t flags ) 1367{ void *tmp___2 ; 1368 1369 { 1370 { 1371#line 283 1372 tmp___2 = __kmalloc(size, flags); 1373 } 1374#line 283 1375 return (tmp___2); 1376} 1377} 1378#line 349 "include/linux/slab.h" 1379__inline static void *kzalloc(size_t size , gfp_t flags ) __attribute__((__no_instrument_function__)) ; 1380#line 349 "include/linux/slab.h" 1381__inline static void *kzalloc(size_t size , gfp_t flags ) 1382{ void *tmp ; 1383 unsigned int __cil_tmp4 ; 1384 1385 { 1386 { 1387#line 351 1388 __cil_tmp4 = flags | 32768U; 1389#line 351 1390 tmp = kmalloc(size, __cil_tmp4); 1391 } 1392#line 351 1393 return (tmp); 1394} 1395} 1396#line 210 "include/linux/power_supply.h" 1397extern void power_supply_changed(struct power_supply *psy ) ; 1398#line 220 1399extern int power_supply_register(struct device *parent , struct power_supply *psy ) ; 1400#line 222 1401extern void power_supply_unregister(struct power_supply *psy ) ; 1402#line 792 "include/linux/device.h" 1403extern void *dev_get_drvdata(struct device const *dev ) ; 1404#line 793 1405extern int dev_set_drvdata(struct device *dev , void *data ) ; 1406#line 891 1407extern int ( /* format attribute */ dev_err)(struct device const *dev , char const *fmt 1408 , ...) ; 1409#line 174 "include/linux/platform_device.h" 1410extern int platform_driver_register(struct platform_driver * ) ; 1411#line 175 1412extern void platform_driver_unregister(struct platform_driver * ) ; 1413#line 183 1414__inline static void *platform_get_drvdata(struct platform_device const *pdev ) __attribute__((__no_instrument_function__)) ; 1415#line 183 "include/linux/platform_device.h" 1416__inline static void *platform_get_drvdata(struct platform_device const *pdev ) 1417{ void *tmp ; 1418 unsigned long __cil_tmp3 ; 1419 unsigned long __cil_tmp4 ; 1420 struct device const *__cil_tmp5 ; 1421 1422 { 1423 { 1424#line 185 1425 __cil_tmp3 = (unsigned long )pdev; 1426#line 185 1427 __cil_tmp4 = __cil_tmp3 + 16; 1428#line 185 1429 __cil_tmp5 = (struct device const *)__cil_tmp4; 1430#line 185 1431 tmp = dev_get_drvdata(__cil_tmp5); 1432 } 1433#line 185 1434 return (tmp); 1435} 1436} 1437#line 188 1438__inline static void platform_set_drvdata(struct platform_device *pdev , void *data ) __attribute__((__no_instrument_function__)) ; 1439#line 188 "include/linux/platform_device.h" 1440__inline static void platform_set_drvdata(struct platform_device *pdev , void *data ) 1441{ unsigned long __cil_tmp3 ; 1442 unsigned long __cil_tmp4 ; 1443 struct device *__cil_tmp5 ; 1444 1445 { 1446 { 1447#line 190 1448 __cil_tmp3 = (unsigned long )pdev; 1449#line 190 1450 __cil_tmp4 = __cil_tmp3 + 16; 1451#line 190 1452 __cil_tmp5 = (struct device *)__cil_tmp4; 1453#line 190 1454 dev_set_drvdata(__cil_tmp5, data); 1455 } 1456#line 191 1457 return; 1458} 1459} 1460#line 41 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/drivers/power/max8903_charger.c.common.c" 1461static enum power_supply_property max8903_charger_props[3] = { (enum power_supply_property )0, (enum power_supply_property )4, (enum power_supply_property )2}; 1462#line 47 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/drivers/power/max8903_charger.c.common.c" 1463static int max8903_get_property(struct power_supply *psy , enum power_supply_property psp , 1464 union power_supply_propval *val ) 1465{ struct max8903_data *data ; 1466 struct power_supply const *__mptr ; 1467 int tmp ; 1468 struct max8903_data *__cil_tmp7 ; 1469 unsigned long __cil_tmp8 ; 1470 unsigned long __cil_tmp9 ; 1471 struct power_supply *__cil_tmp10 ; 1472 unsigned int __cil_tmp11 ; 1473 char *__cil_tmp12 ; 1474 char *__cil_tmp13 ; 1475 unsigned long __cil_tmp14 ; 1476 unsigned long __cil_tmp15 ; 1477 unsigned long __cil_tmp16 ; 1478 unsigned long __cil_tmp17 ; 1479 unsigned long __cil_tmp18 ; 1480 unsigned long __cil_tmp19 ; 1481 int __cil_tmp20 ; 1482 unsigned int __cil_tmp21 ; 1483 unsigned long __cil_tmp22 ; 1484 unsigned long __cil_tmp23 ; 1485 unsigned long __cil_tmp24 ; 1486 unsigned long __cil_tmp25 ; 1487 unsigned long __cil_tmp26 ; 1488 unsigned long __cil_tmp27 ; 1489 unsigned long __cil_tmp28 ; 1490 unsigned long __cil_tmp29 ; 1491 unsigned long __cil_tmp30 ; 1492 unsigned long __cil_tmp31 ; 1493 1494 { 1495#line 51 1496 __mptr = (struct power_supply const *)psy; 1497#line 51 1498 __cil_tmp7 = (struct max8903_data *)0; 1499#line 51 1500 __cil_tmp8 = (unsigned long )__cil_tmp7; 1501#line 51 1502 __cil_tmp9 = __cil_tmp8 + 40; 1503#line 51 1504 __cil_tmp10 = (struct power_supply *)__cil_tmp9; 1505#line 51 1506 __cil_tmp11 = (unsigned int )__cil_tmp10; 1507#line 51 1508 __cil_tmp12 = (char *)__mptr; 1509#line 51 1510 __cil_tmp13 = __cil_tmp12 - __cil_tmp11; 1511#line 51 1512 data = (struct max8903_data *)__cil_tmp13; 1513#line 55 1514 if ((int )psp == 0) { 1515#line 55 1516 goto case_0; 1517 } else 1518#line 66 1519 if ((int )psp == 4) { 1520#line 66 1521 goto case_4; 1522 } else 1523#line 71 1524 if ((int )psp == 2) { 1525#line 71 1526 goto case_2; 1527 } else { 1528 { 1529#line 76 1530 goto switch_default; 1531#line 54 1532 if (0) { 1533 case_0: /* CIL Label */ 1534#line 56 1535 *((int *)val) = 0; 1536 { 1537#line 57 1538 __cil_tmp14 = 0 + 12; 1539#line 57 1540 __cil_tmp15 = (unsigned long )data; 1541#line 57 1542 __cil_tmp16 = __cil_tmp15 + __cil_tmp14; 1543#line 57 1544 if (*((int *)__cil_tmp16)) { 1545 { 1546#line 58 1547 __cil_tmp17 = 0 + 12; 1548#line 58 1549 __cil_tmp18 = (unsigned long )data; 1550#line 58 1551 __cil_tmp19 = __cil_tmp18 + __cil_tmp17; 1552#line 58 1553 __cil_tmp20 = *((int *)__cil_tmp19); 1554#line 58 1555 __cil_tmp21 = (unsigned int )__cil_tmp20; 1556#line 58 1557 tmp = gpio_get_value(__cil_tmp21); 1558 } 1559#line 58 1560 if (tmp == 0) { 1561#line 59 1562 *((int *)val) = 1; 1563 } else { 1564 { 1565#line 60 1566 __cil_tmp22 = (unsigned long )data; 1567#line 60 1568 __cil_tmp23 = __cil_tmp22 + 257; 1569#line 60 1570 if (*((bool *)__cil_tmp23)) { 1571#line 61 1572 *((int *)val) = 3; 1573 } else { 1574 { 1575#line 60 1576 __cil_tmp24 = (unsigned long )data; 1577#line 60 1578 __cil_tmp25 = __cil_tmp24 + 258; 1579#line 60 1580 if (*((bool *)__cil_tmp25)) { 1581#line 61 1582 *((int *)val) = 3; 1583 } else { 1584#line 63 1585 *((int *)val) = 2; 1586 } 1587 } 1588 } 1589 } 1590 } 1591 } else { 1592 1593 } 1594 } 1595#line 65 1596 goto switch_break; 1597 case_4: /* CIL Label */ 1598#line 67 1599 *((int *)val) = 0; 1600 { 1601#line 68 1602 __cil_tmp26 = (unsigned long )data; 1603#line 68 1604 __cil_tmp27 = __cil_tmp26 + 257; 1605#line 68 1606 if (*((bool *)__cil_tmp27)) { 1607#line 69 1608 *((int *)val) = 1; 1609 } else { 1610 { 1611#line 68 1612 __cil_tmp28 = (unsigned long )data; 1613#line 68 1614 __cil_tmp29 = __cil_tmp28 + 258; 1615#line 68 1616 if (*((bool *)__cil_tmp29)) { 1617#line 69 1618 *((int *)val) = 1; 1619 } else { 1620 1621 } 1622 } 1623 } 1624 } 1625#line 70 1626 goto switch_break; 1627 case_2: /* CIL Label */ 1628#line 72 1629 *((int *)val) = 1; 1630 { 1631#line 73 1632 __cil_tmp30 = (unsigned long )data; 1633#line 73 1634 __cil_tmp31 = __cil_tmp30 + 256; 1635#line 73 1636 if (*((bool *)__cil_tmp31)) { 1637#line 74 1638 *((int *)val) = 5; 1639 } else { 1640 1641 } 1642 } 1643#line 75 1644 goto switch_break; 1645 switch_default: /* CIL Label */ 1646#line 77 1647 return (-22); 1648 } else { 1649 switch_break: /* CIL Label */ ; 1650 } 1651 } 1652 } 1653#line 79 1654 return (0); 1655} 1656} 1657#line 105 1658static irqreturn_t max8903_dcin(int irq , void *_data___0 ) ; 1659#line 105 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/drivers/power/max8903_charger.c.common.c" 1660static struct _ddebug __attribute__((__aligned__(8))) descriptor __attribute__((__used__, 1661__section__("__verbose"))) = {"max8903_charger", "max8903_dcin", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/drivers/power/max8903_charger.c.common.c", 1662 "TA(DC-IN) Charger %s.\n", 106U, 1U}; 1663#line 82 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/drivers/power/max8903_charger.c.common.c" 1664static irqreturn_t max8903_dcin(int irq , void *_data___0 ) 1665{ struct max8903_data *data ; 1666 struct max8903_pdata *pdata ; 1667 bool ta_in ; 1668 enum power_supply_type old_type ; 1669 int tmp___0 ; 1670 int tmp___1 ; 1671 int tmp___2 ; 1672 int tmp___3 ; 1673 char const *tmp___4 ; 1674 long tmp___5 ; 1675 unsigned long __cil_tmp14 ; 1676 unsigned long __cil_tmp15 ; 1677 int __cil_tmp16 ; 1678 unsigned int __cil_tmp17 ; 1679 unsigned long __cil_tmp18 ; 1680 unsigned long __cil_tmp19 ; 1681 bool __cil_tmp20 ; 1682 int __cil_tmp21 ; 1683 int __cil_tmp22 ; 1684 unsigned long __cil_tmp23 ; 1685 unsigned long __cil_tmp24 ; 1686 unsigned long __cil_tmp25 ; 1687 unsigned long __cil_tmp26 ; 1688 unsigned long __cil_tmp27 ; 1689 unsigned long __cil_tmp28 ; 1690 int __cil_tmp29 ; 1691 unsigned int __cil_tmp30 ; 1692 unsigned long __cil_tmp31 ; 1693 unsigned long __cil_tmp32 ; 1694 int __cil_tmp33 ; 1695 unsigned int __cil_tmp34 ; 1696 struct _ddebug __attribute__((__aligned__(8))) *__cil_tmp35 ; 1697 unsigned int __cil_tmp36 ; 1698 unsigned int __cil_tmp37 ; 1699 int __cil_tmp38 ; 1700 int __cil_tmp39 ; 1701 long __cil_tmp40 ; 1702 unsigned long __cil_tmp41 ; 1703 unsigned long __cil_tmp42 ; 1704 struct device *__cil_tmp43 ; 1705 struct device const *__cil_tmp44 ; 1706 unsigned long __cil_tmp45 ; 1707 unsigned long __cil_tmp46 ; 1708 unsigned long __cil_tmp47 ; 1709 unsigned long __cil_tmp48 ; 1710 unsigned long __cil_tmp49 ; 1711 unsigned long __cil_tmp50 ; 1712 unsigned long __cil_tmp51 ; 1713 unsigned long __cil_tmp52 ; 1714 unsigned long __cil_tmp53 ; 1715 unsigned long __cil_tmp54 ; 1716 unsigned long __cil_tmp55 ; 1717 unsigned long __cil_tmp56 ; 1718 unsigned long __cil_tmp57 ; 1719 unsigned long __cil_tmp58 ; 1720 unsigned long __cil_tmp59 ; 1721 unsigned long __cil_tmp60 ; 1722 unsigned long __cil_tmp61 ; 1723 unsigned long __cil_tmp62 ; 1724 unsigned long __cil_tmp63 ; 1725 enum power_supply_type __cil_tmp64 ; 1726 unsigned int __cil_tmp65 ; 1727 unsigned int __cil_tmp66 ; 1728 unsigned long __cil_tmp67 ; 1729 unsigned long __cil_tmp68 ; 1730 struct power_supply *__cil_tmp69 ; 1731 1732 { 1733 { 1734#line 84 1735 data = (struct max8903_data *)_data___0; 1736#line 85 1737 pdata = (struct max8903_pdata *)data; 1738#line 89 1739 __cil_tmp14 = (unsigned long )pdata; 1740#line 89 1741 __cil_tmp15 = __cil_tmp14 + 4; 1742#line 89 1743 __cil_tmp16 = *((int *)__cil_tmp15); 1744#line 89 1745 __cil_tmp17 = (unsigned int )__cil_tmp16; 1746#line 89 1747 tmp___0 = gpio_get_value(__cil_tmp17); 1748 } 1749#line 89 1750 if (tmp___0) { 1751#line 89 1752 ta_in = (bool )0; 1753 } else { 1754#line 89 1755 ta_in = (bool )1; 1756 } 1757 { 1758#line 91 1759 __cil_tmp18 = (unsigned long )data; 1760#line 91 1761 __cil_tmp19 = __cil_tmp18 + 258; 1762#line 91 1763 __cil_tmp20 = *((bool *)__cil_tmp19); 1764#line 91 1765 __cil_tmp21 = (int )__cil_tmp20; 1766#line 91 1767 __cil_tmp22 = (int )ta_in; 1768#line 91 1769 if (__cil_tmp22 == __cil_tmp21) { 1770#line 92 1771 return ((irqreturn_t )1); 1772 } else { 1773 1774 } 1775 } 1776#line 94 1777 __cil_tmp23 = (unsigned long )data; 1778#line 94 1779 __cil_tmp24 = __cil_tmp23 + 258; 1780#line 94 1781 *((bool *)__cil_tmp24) = ta_in; 1782 { 1783#line 97 1784 __cil_tmp25 = (unsigned long )pdata; 1785#line 97 1786 __cil_tmp26 = __cil_tmp25 + 20; 1787#line 97 1788 if (*((int *)__cil_tmp26)) { 1789#line 98 1790 if (ta_in) { 1791#line 98 1792 tmp___1 = 1; 1793 } else { 1794#line 98 1795 tmp___1 = 0; 1796 } 1797 { 1798#line 98 1799 __cil_tmp27 = (unsigned long )pdata; 1800#line 98 1801 __cil_tmp28 = __cil_tmp27 + 20; 1802#line 98 1803 __cil_tmp29 = *((int *)__cil_tmp28); 1804#line 98 1805 __cil_tmp30 = (unsigned int )__cil_tmp29; 1806#line 98 1807 gpio_set_value(__cil_tmp30, tmp___1); 1808 } 1809 } else { 1810 1811 } 1812 } 1813#line 101 1814 if (*((int *)pdata)) { 1815#line 102 1816 if (ta_in) { 1817#line 102 1818 tmp___3 = 0; 1819 } else { 1820 { 1821#line 102 1822 __cil_tmp31 = (unsigned long )data; 1823#line 102 1824 __cil_tmp32 = __cil_tmp31 + 257; 1825#line 102 1826 if (*((bool *)__cil_tmp32)) { 1827#line 102 1828 tmp___2 = 0; 1829 } else { 1830#line 102 1831 tmp___2 = 1; 1832 } 1833 } 1834#line 102 1835 tmp___3 = tmp___2; 1836 } 1837 { 1838#line 102 1839 __cil_tmp33 = *((int *)pdata); 1840#line 102 1841 __cil_tmp34 = (unsigned int )__cil_tmp33; 1842#line 102 1843 gpio_set_value(__cil_tmp34, tmp___3); 1844 } 1845 } else { 1846 1847 } 1848 { 1849#line 105 1850 while (1) { 1851 while_continue: /* CIL Label */ ; 1852 { 1853#line 105 1854 while (1) { 1855 while_continue___0: /* CIL Label */ ; 1856 { 1857#line 105 1858 __cil_tmp35 = & descriptor; 1859#line 105 1860 __cil_tmp36 = __cil_tmp35->flags; 1861#line 105 1862 __cil_tmp37 = __cil_tmp36 & 1U; 1863#line 105 1864 __cil_tmp38 = ! __cil_tmp37; 1865#line 105 1866 __cil_tmp39 = ! __cil_tmp38; 1867#line 105 1868 __cil_tmp40 = (long )__cil_tmp39; 1869#line 105 1870 tmp___5 = __builtin_expect(__cil_tmp40, 0L); 1871 } 1872#line 105 1873 if (tmp___5) { 1874#line 105 1875 if (ta_in) { 1876#line 105 1877 tmp___4 = "Connected"; 1878 } else { 1879#line 105 1880 tmp___4 = "Disconnected"; 1881 } 1882 { 1883#line 105 1884 __cil_tmp41 = (unsigned long )data; 1885#line 105 1886 __cil_tmp42 = __cil_tmp41 + 32; 1887#line 105 1888 __cil_tmp43 = *((struct device **)__cil_tmp42); 1889#line 105 1890 __cil_tmp44 = (struct device const *)__cil_tmp43; 1891#line 105 1892 __dynamic_dev_dbg(& descriptor, __cil_tmp44, "TA(DC-IN) Charger %s.\n", tmp___4); 1893 } 1894 } else { 1895 1896 } 1897#line 105 1898 goto while_break___0; 1899 } 1900 while_break___0: /* CIL Label */ ; 1901 } 1902#line 105 1903 goto while_break; 1904 } 1905 while_break: /* CIL Label */ ; 1906 } 1907#line 108 1908 __cil_tmp45 = 40 + 8; 1909#line 108 1910 __cil_tmp46 = (unsigned long )data; 1911#line 108 1912 __cil_tmp47 = __cil_tmp46 + __cil_tmp45; 1913#line 108 1914 old_type = *((enum power_supply_type *)__cil_tmp47); 1915 { 1916#line 110 1917 __cil_tmp48 = (unsigned long )data; 1918#line 110 1919 __cil_tmp49 = __cil_tmp48 + 258; 1920#line 110 1921 if (*((bool *)__cil_tmp49)) { 1922#line 111 1923 __cil_tmp50 = 40 + 8; 1924#line 111 1925 __cil_tmp51 = (unsigned long )data; 1926#line 111 1927 __cil_tmp52 = __cil_tmp51 + __cil_tmp50; 1928#line 111 1929 *((enum power_supply_type *)__cil_tmp52) = (enum power_supply_type )3; 1930 } else { 1931 { 1932#line 112 1933 __cil_tmp53 = (unsigned long )data; 1934#line 112 1935 __cil_tmp54 = __cil_tmp53 + 257; 1936#line 112 1937 if (*((bool *)__cil_tmp54)) { 1938#line 113 1939 __cil_tmp55 = 40 + 8; 1940#line 113 1941 __cil_tmp56 = (unsigned long )data; 1942#line 113 1943 __cil_tmp57 = __cil_tmp56 + __cil_tmp55; 1944#line 113 1945 *((enum power_supply_type *)__cil_tmp57) = (enum power_supply_type )4; 1946 } else { 1947#line 115 1948 __cil_tmp58 = 40 + 8; 1949#line 115 1950 __cil_tmp59 = (unsigned long )data; 1951#line 115 1952 __cil_tmp60 = __cil_tmp59 + __cil_tmp58; 1953#line 115 1954 *((enum power_supply_type *)__cil_tmp60) = (enum power_supply_type )1; 1955 } 1956 } 1957 } 1958 } 1959 { 1960#line 117 1961 __cil_tmp61 = 40 + 8; 1962#line 117 1963 __cil_tmp62 = (unsigned long )data; 1964#line 117 1965 __cil_tmp63 = __cil_tmp62 + __cil_tmp61; 1966#line 117 1967 __cil_tmp64 = *((enum power_supply_type *)__cil_tmp63); 1968#line 117 1969 __cil_tmp65 = (unsigned int )__cil_tmp64; 1970#line 117 1971 __cil_tmp66 = (unsigned int )old_type; 1972#line 117 1973 if (__cil_tmp66 != __cil_tmp65) { 1974 { 1975#line 118 1976 __cil_tmp67 = (unsigned long )data; 1977#line 118 1978 __cil_tmp68 = __cil_tmp67 + 40; 1979#line 118 1980 __cil_tmp69 = (struct power_supply *)__cil_tmp68; 1981#line 118 1982 power_supply_changed(__cil_tmp69); 1983 } 1984 } else { 1985 1986 } 1987 } 1988#line 120 1989 return ((irqreturn_t )1); 1990} 1991} 1992#line 144 1993static irqreturn_t max8903_usbin(int irq , void *_data___0 ) ; 1994#line 144 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/drivers/power/max8903_charger.c.common.c" 1995static struct _ddebug __attribute__((__aligned__(8))) descriptor___0 __attribute__((__used__, 1996__section__("__verbose"))) = {"max8903_charger", "max8903_usbin", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/drivers/power/max8903_charger.c.common.c", 1997 "USB Charger %s.\n", 145U, 1U}; 1998#line 123 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/drivers/power/max8903_charger.c.common.c" 1999static irqreturn_t max8903_usbin(int irq , void *_data___0 ) 2000{ struct max8903_data *data ; 2001 struct max8903_pdata *pdata ; 2002 bool usb_in ; 2003 enum power_supply_type old_type ; 2004 int tmp___0 ; 2005 int tmp___1 ; 2006 int tmp___2 ; 2007 char const *tmp___3 ; 2008 long tmp___4 ; 2009 unsigned long __cil_tmp13 ; 2010 unsigned long __cil_tmp14 ; 2011 int __cil_tmp15 ; 2012 unsigned int __cil_tmp16 ; 2013 unsigned long __cil_tmp17 ; 2014 unsigned long __cil_tmp18 ; 2015 bool __cil_tmp19 ; 2016 int __cil_tmp20 ; 2017 int __cil_tmp21 ; 2018 unsigned long __cil_tmp22 ; 2019 unsigned long __cil_tmp23 ; 2020 unsigned long __cil_tmp24 ; 2021 unsigned long __cil_tmp25 ; 2022 int __cil_tmp26 ; 2023 unsigned int __cil_tmp27 ; 2024 struct _ddebug __attribute__((__aligned__(8))) *__cil_tmp28 ; 2025 unsigned int __cil_tmp29 ; 2026 unsigned int __cil_tmp30 ; 2027 int __cil_tmp31 ; 2028 int __cil_tmp32 ; 2029 long __cil_tmp33 ; 2030 unsigned long __cil_tmp34 ; 2031 unsigned long __cil_tmp35 ; 2032 struct device *__cil_tmp36 ; 2033 struct device const *__cil_tmp37 ; 2034 unsigned long __cil_tmp38 ; 2035 unsigned long __cil_tmp39 ; 2036 unsigned long __cil_tmp40 ; 2037 unsigned long __cil_tmp41 ; 2038 unsigned long __cil_tmp42 ; 2039 unsigned long __cil_tmp43 ; 2040 unsigned long __cil_tmp44 ; 2041 unsigned long __cil_tmp45 ; 2042 unsigned long __cil_tmp46 ; 2043 unsigned long __cil_tmp47 ; 2044 unsigned long __cil_tmp48 ; 2045 unsigned long __cil_tmp49 ; 2046 unsigned long __cil_tmp50 ; 2047 unsigned long __cil_tmp51 ; 2048 unsigned long __cil_tmp52 ; 2049 unsigned long __cil_tmp53 ; 2050 unsigned long __cil_tmp54 ; 2051 unsigned long __cil_tmp55 ; 2052 unsigned long __cil_tmp56 ; 2053 enum power_supply_type __cil_tmp57 ; 2054 unsigned int __cil_tmp58 ; 2055 unsigned int __cil_tmp59 ; 2056 unsigned long __cil_tmp60 ; 2057 unsigned long __cil_tmp61 ; 2058 struct power_supply *__cil_tmp62 ; 2059 2060 { 2061 { 2062#line 125 2063 data = (struct max8903_data *)_data___0; 2064#line 126 2065 pdata = (struct max8903_pdata *)data; 2066#line 130 2067 __cil_tmp13 = (unsigned long )pdata; 2068#line 130 2069 __cil_tmp14 = __cil_tmp13 + 8; 2070#line 130 2071 __cil_tmp15 = *((int *)__cil_tmp14); 2072#line 130 2073 __cil_tmp16 = (unsigned int )__cil_tmp15; 2074#line 130 2075 tmp___0 = gpio_get_value(__cil_tmp16); 2076 } 2077#line 130 2078 if (tmp___0) { 2079#line 130 2080 usb_in = (bool )0; 2081 } else { 2082#line 130 2083 usb_in = (bool )1; 2084 } 2085 { 2086#line 132 2087 __cil_tmp17 = (unsigned long )data; 2088#line 132 2089 __cil_tmp18 = __cil_tmp17 + 257; 2090#line 132 2091 __cil_tmp19 = *((bool *)__cil_tmp18); 2092#line 132 2093 __cil_tmp20 = (int )__cil_tmp19; 2094#line 132 2095 __cil_tmp21 = (int )usb_in; 2096#line 132 2097 if (__cil_tmp21 == __cil_tmp20) { 2098#line 133 2099 return ((irqreturn_t )1); 2100 } else { 2101 2102 } 2103 } 2104#line 135 2105 __cil_tmp22 = (unsigned long )data; 2106#line 135 2107 __cil_tmp23 = __cil_tmp22 + 257; 2108#line 135 2109 *((bool *)__cil_tmp23) = usb_in; 2110#line 140 2111 if (*((int *)pdata)) { 2112#line 141 2113 if (usb_in) { 2114#line 141 2115 tmp___2 = 0; 2116 } else { 2117 { 2118#line 141 2119 __cil_tmp24 = (unsigned long )data; 2120#line 141 2121 __cil_tmp25 = __cil_tmp24 + 258; 2122#line 141 2123 if (*((bool *)__cil_tmp25)) { 2124#line 141 2125 tmp___1 = 0; 2126 } else { 2127#line 141 2128 tmp___1 = 1; 2129 } 2130 } 2131#line 141 2132 tmp___2 = tmp___1; 2133 } 2134 { 2135#line 141 2136 __cil_tmp26 = *((int *)pdata); 2137#line 141 2138 __cil_tmp27 = (unsigned int )__cil_tmp26; 2139#line 141 2140 gpio_set_value(__cil_tmp27, tmp___2); 2141 } 2142 } else { 2143 2144 } 2145 { 2146#line 144 2147 while (1) { 2148 while_continue: /* CIL Label */ ; 2149 { 2150#line 144 2151 while (1) { 2152 while_continue___0: /* CIL Label */ ; 2153 { 2154#line 144 2155 __cil_tmp28 = & descriptor___0; 2156#line 144 2157 __cil_tmp29 = __cil_tmp28->flags; 2158#line 144 2159 __cil_tmp30 = __cil_tmp29 & 1U; 2160#line 144 2161 __cil_tmp31 = ! __cil_tmp30; 2162#line 144 2163 __cil_tmp32 = ! __cil_tmp31; 2164#line 144 2165 __cil_tmp33 = (long )__cil_tmp32; 2166#line 144 2167 tmp___4 = __builtin_expect(__cil_tmp33, 0L); 2168 } 2169#line 144 2170 if (tmp___4) { 2171#line 144 2172 if (usb_in) { 2173#line 144 2174 tmp___3 = "Connected"; 2175 } else { 2176#line 144 2177 tmp___3 = "Disconnected"; 2178 } 2179 { 2180#line 144 2181 __cil_tmp34 = (unsigned long )data; 2182#line 144 2183 __cil_tmp35 = __cil_tmp34 + 32; 2184#line 144 2185 __cil_tmp36 = *((struct device **)__cil_tmp35); 2186#line 144 2187 __cil_tmp37 = (struct device const *)__cil_tmp36; 2188#line 144 2189 __dynamic_dev_dbg(& descriptor___0, __cil_tmp37, "USB Charger %s.\n", tmp___3); 2190 } 2191 } else { 2192 2193 } 2194#line 144 2195 goto while_break___0; 2196 } 2197 while_break___0: /* CIL Label */ ; 2198 } 2199#line 144 2200 goto while_break; 2201 } 2202 while_break: /* CIL Label */ ; 2203 } 2204#line 147 2205 __cil_tmp38 = 40 + 8; 2206#line 147 2207 __cil_tmp39 = (unsigned long )data; 2208#line 147 2209 __cil_tmp40 = __cil_tmp39 + __cil_tmp38; 2210#line 147 2211 old_type = *((enum power_supply_type *)__cil_tmp40); 2212 { 2213#line 149 2214 __cil_tmp41 = (unsigned long )data; 2215#line 149 2216 __cil_tmp42 = __cil_tmp41 + 258; 2217#line 149 2218 if (*((bool *)__cil_tmp42)) { 2219#line 150 2220 __cil_tmp43 = 40 + 8; 2221#line 150 2222 __cil_tmp44 = (unsigned long )data; 2223#line 150 2224 __cil_tmp45 = __cil_tmp44 + __cil_tmp43; 2225#line 150 2226 *((enum power_supply_type *)__cil_tmp45) = (enum power_supply_type )3; 2227 } else { 2228 { 2229#line 151 2230 __cil_tmp46 = (unsigned long )data; 2231#line 151 2232 __cil_tmp47 = __cil_tmp46 + 257; 2233#line 151 2234 if (*((bool *)__cil_tmp47)) { 2235#line 152 2236 __cil_tmp48 = 40 + 8; 2237#line 152 2238 __cil_tmp49 = (unsigned long )data; 2239#line 152 2240 __cil_tmp50 = __cil_tmp49 + __cil_tmp48; 2241#line 152 2242 *((enum power_supply_type *)__cil_tmp50) = (enum power_supply_type )4; 2243 } else { 2244#line 154 2245 __cil_tmp51 = 40 + 8; 2246#line 154 2247 __cil_tmp52 = (unsigned long )data; 2248#line 154 2249 __cil_tmp53 = __cil_tmp52 + __cil_tmp51; 2250#line 154 2251 *((enum power_supply_type *)__cil_tmp53) = (enum power_supply_type )1; 2252 } 2253 } 2254 } 2255 } 2256 { 2257#line 156 2258 __cil_tmp54 = 40 + 8; 2259#line 156 2260 __cil_tmp55 = (unsigned long )data; 2261#line 156 2262 __cil_tmp56 = __cil_tmp55 + __cil_tmp54; 2263#line 156 2264 __cil_tmp57 = *((enum power_supply_type *)__cil_tmp56); 2265#line 156 2266 __cil_tmp58 = (unsigned int )__cil_tmp57; 2267#line 156 2268 __cil_tmp59 = (unsigned int )old_type; 2269#line 156 2270 if (__cil_tmp59 != __cil_tmp58) { 2271 { 2272#line 157 2273 __cil_tmp60 = (unsigned long )data; 2274#line 157 2275 __cil_tmp61 = __cil_tmp60 + 40; 2276#line 157 2277 __cil_tmp62 = (struct power_supply *)__cil_tmp61; 2278#line 157 2279 power_supply_changed(__cil_tmp62); 2280 } 2281 } else { 2282 2283 } 2284 } 2285#line 159 2286 return ((irqreturn_t )1); 2287} 2288} 2289#line 162 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/drivers/power/max8903_charger.c.common.c" 2290static irqreturn_t max8903_fault(int irq , void *_data___0 ) 2291{ struct max8903_data *data ; 2292 struct max8903_pdata *pdata ; 2293 bool fault ; 2294 int tmp___0 ; 2295 unsigned long __cil_tmp8 ; 2296 unsigned long __cil_tmp9 ; 2297 int __cil_tmp10 ; 2298 unsigned int __cil_tmp11 ; 2299 unsigned long __cil_tmp12 ; 2300 unsigned long __cil_tmp13 ; 2301 bool __cil_tmp14 ; 2302 int __cil_tmp15 ; 2303 int __cil_tmp16 ; 2304 unsigned long __cil_tmp17 ; 2305 unsigned long __cil_tmp18 ; 2306 unsigned long __cil_tmp19 ; 2307 unsigned long __cil_tmp20 ; 2308 struct device *__cil_tmp21 ; 2309 struct device const *__cil_tmp22 ; 2310 unsigned long __cil_tmp23 ; 2311 unsigned long __cil_tmp24 ; 2312 struct device *__cil_tmp25 ; 2313 struct device const *__cil_tmp26 ; 2314 2315 { 2316 { 2317#line 164 2318 data = (struct max8903_data *)_data___0; 2319#line 165 2320 pdata = (struct max8903_pdata *)data; 2321#line 168 2322 __cil_tmp8 = (unsigned long )pdata; 2323#line 168 2324 __cil_tmp9 = __cil_tmp8 + 16; 2325#line 168 2326 __cil_tmp10 = *((int *)__cil_tmp9); 2327#line 168 2328 __cil_tmp11 = (unsigned int )__cil_tmp10; 2329#line 168 2330 tmp___0 = gpio_get_value(__cil_tmp11); 2331 } 2332#line 168 2333 if (tmp___0) { 2334#line 168 2335 fault = (bool )0; 2336 } else { 2337#line 168 2338 fault = (bool )1; 2339 } 2340 { 2341#line 170 2342 __cil_tmp12 = (unsigned long )data; 2343#line 170 2344 __cil_tmp13 = __cil_tmp12 + 256; 2345#line 170 2346 __cil_tmp14 = *((bool *)__cil_tmp13); 2347#line 170 2348 __cil_tmp15 = (int )__cil_tmp14; 2349#line 170 2350 __cil_tmp16 = (int )fault; 2351#line 170 2352 if (__cil_tmp16 == __cil_tmp15) { 2353#line 171 2354 return ((irqreturn_t )1); 2355 } else { 2356 2357 } 2358 } 2359#line 173 2360 __cil_tmp17 = (unsigned long )data; 2361#line 173 2362 __cil_tmp18 = __cil_tmp17 + 256; 2363#line 173 2364 *((bool *)__cil_tmp18) = fault; 2365#line 175 2366 if (fault) { 2367 { 2368#line 176 2369 __cil_tmp19 = (unsigned long )data; 2370#line 176 2371 __cil_tmp20 = __cil_tmp19 + 32; 2372#line 176 2373 __cil_tmp21 = *((struct device **)__cil_tmp20); 2374#line 176 2375 __cil_tmp22 = (struct device const *)__cil_tmp21; 2376#line 176 2377 dev_err(__cil_tmp22, "Charger suffers a fault and stops.\n"); 2378 } 2379 } else { 2380 { 2381#line 178 2382 __cil_tmp23 = (unsigned long )data; 2383#line 178 2384 __cil_tmp24 = __cil_tmp23 + 32; 2385#line 178 2386 __cil_tmp25 = *((struct device **)__cil_tmp24); 2387#line 178 2388 __cil_tmp26 = (struct device const *)__cil_tmp25; 2389#line 178 2390 dev_err(__cil_tmp26, "Charger recovered from a fault.\n"); 2391 } 2392 } 2393#line 180 2394 return ((irqreturn_t )1); 2395} 2396} 2397#line 183 2398static int max8903_probe(struct platform_device *pdev ) __attribute__((__section__(".devinit.text"), 2399__no_instrument_function__)) ; 2400#line 183 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/drivers/power/max8903_charger.c.common.c" 2401static int max8903_probe(struct platform_device *pdev ) 2402{ struct max8903_data *data ; 2403 struct device *dev ; 2404 struct max8903_pdata *pdata ; 2405 int ret ; 2406 int gpio ; 2407 int ta_in ; 2408 int usb_in ; 2409 void *tmp ; 2410 size_t __len ; 2411 void *__ret ; 2412 int tmp___1 ; 2413 bool tmp___2 ; 2414 bool tmp___3 ; 2415 bool tmp___4 ; 2416 int tmp___6 ; 2417 bool tmp___7 ; 2418 int tmp___8 ; 2419 bool tmp___9 ; 2420 bool tmp___10 ; 2421 bool tmp___11 ; 2422 bool tmp___12 ; 2423 int tmp___13 ; 2424 int tmp___14 ; 2425 int tmp___15 ; 2426 int tmp___16 ; 2427 int tmp___17 ; 2428 int tmp___18 ; 2429 int tmp___19 ; 2430 int tmp___20 ; 2431 int tmp___21 ; 2432 unsigned long __cil_tmp34 ; 2433 unsigned long __cil_tmp35 ; 2434 unsigned long __cil_tmp36 ; 2435 unsigned long __cil_tmp37 ; 2436 unsigned long __cil_tmp38 ; 2437 void *__cil_tmp39 ; 2438 void *__cil_tmp40 ; 2439 unsigned long __cil_tmp41 ; 2440 unsigned long __cil_tmp42 ; 2441 struct device const *__cil_tmp43 ; 2442 struct max8903_pdata *__cil_tmp44 ; 2443 void *__cil_tmp45 ; 2444 void const *__cil_tmp46 ; 2445 struct max8903_pdata *__cil_tmp47 ; 2446 void *__cil_tmp48 ; 2447 void const *__cil_tmp49 ; 2448 unsigned long __cil_tmp50 ; 2449 unsigned long __cil_tmp51 ; 2450 void *__cil_tmp52 ; 2451 unsigned long __cil_tmp53 ; 2452 unsigned long __cil_tmp54 ; 2453 bool __cil_tmp55 ; 2454 int __cil_tmp56 ; 2455 unsigned long __cil_tmp57 ; 2456 unsigned long __cil_tmp58 ; 2457 bool __cil_tmp59 ; 2458 int __cil_tmp60 ; 2459 struct device const *__cil_tmp61 ; 2460 unsigned long __cil_tmp62 ; 2461 unsigned long __cil_tmp63 ; 2462 unsigned long __cil_tmp64 ; 2463 unsigned long __cil_tmp65 ; 2464 unsigned long __cil_tmp66 ; 2465 unsigned long __cil_tmp67 ; 2466 int __cil_tmp68 ; 2467 unsigned long __cil_tmp69 ; 2468 unsigned long __cil_tmp70 ; 2469 unsigned long __cil_tmp71 ; 2470 unsigned long __cil_tmp72 ; 2471 int __cil_tmp73 ; 2472 unsigned long __cil_tmp74 ; 2473 unsigned long __cil_tmp75 ; 2474 unsigned int __cil_tmp76 ; 2475 unsigned long __cil_tmp77 ; 2476 unsigned long __cil_tmp78 ; 2477 unsigned int __cil_tmp79 ; 2478 struct device const *__cil_tmp80 ; 2479 struct device const *__cil_tmp81 ; 2480 struct device const *__cil_tmp82 ; 2481 struct device const *__cil_tmp83 ; 2482 unsigned long __cil_tmp84 ; 2483 unsigned long __cil_tmp85 ; 2484 unsigned long __cil_tmp86 ; 2485 unsigned long __cil_tmp87 ; 2486 int __cil_tmp88 ; 2487 unsigned long __cil_tmp89 ; 2488 unsigned long __cil_tmp90 ; 2489 int __cil_tmp91 ; 2490 unsigned int __cil_tmp92 ; 2491 struct device const *__cil_tmp93 ; 2492 unsigned long __cil_tmp94 ; 2493 unsigned long __cil_tmp95 ; 2494 unsigned long __cil_tmp96 ; 2495 unsigned long __cil_tmp97 ; 2496 unsigned long __cil_tmp98 ; 2497 unsigned long __cil_tmp99 ; 2498 int __cil_tmp100 ; 2499 unsigned long __cil_tmp101 ; 2500 unsigned long __cil_tmp102 ; 2501 unsigned int __cil_tmp103 ; 2502 struct device const *__cil_tmp104 ; 2503 struct device const *__cil_tmp105 ; 2504 int __cil_tmp106 ; 2505 int __cil_tmp107 ; 2506 unsigned int __cil_tmp108 ; 2507 struct device const *__cil_tmp109 ; 2508 unsigned long __cil_tmp110 ; 2509 unsigned long __cil_tmp111 ; 2510 unsigned long __cil_tmp112 ; 2511 unsigned long __cil_tmp113 ; 2512 int __cil_tmp114 ; 2513 struct device const *__cil_tmp115 ; 2514 unsigned long __cil_tmp116 ; 2515 unsigned long __cil_tmp117 ; 2516 unsigned long __cil_tmp118 ; 2517 unsigned long __cil_tmp119 ; 2518 int __cil_tmp120 ; 2519 struct device const *__cil_tmp121 ; 2520 unsigned long __cil_tmp122 ; 2521 unsigned long __cil_tmp123 ; 2522 unsigned long __cil_tmp124 ; 2523 unsigned long __cil_tmp125 ; 2524 int __cil_tmp126 ; 2525 struct device const *__cil_tmp127 ; 2526 unsigned long __cil_tmp128 ; 2527 unsigned long __cil_tmp129 ; 2528 unsigned long __cil_tmp130 ; 2529 unsigned long __cil_tmp131 ; 2530 unsigned long __cil_tmp132 ; 2531 unsigned long __cil_tmp133 ; 2532 unsigned long __cil_tmp134 ; 2533 unsigned long __cil_tmp135 ; 2534 unsigned long __cil_tmp136 ; 2535 unsigned long __cil_tmp137 ; 2536 unsigned long __cil_tmp138 ; 2537 unsigned long __cil_tmp139 ; 2538 unsigned long __cil_tmp140 ; 2539 unsigned long __cil_tmp141 ; 2540 unsigned long __cil_tmp142 ; 2541 unsigned long __cil_tmp143 ; 2542 unsigned long __cil_tmp144 ; 2543 unsigned long __cil_tmp145 ; 2544 unsigned long __cil_tmp146 ; 2545 unsigned long __cil_tmp147 ; 2546 unsigned long __cil_tmp148 ; 2547 unsigned long __cil_tmp149 ; 2548 unsigned long __cil_tmp150 ; 2549 unsigned long __cil_tmp151 ; 2550 unsigned long __cil_tmp152 ; 2551 unsigned long __cil_tmp153 ; 2552 unsigned long __cil_tmp154 ; 2553 unsigned long __cil_tmp155 ; 2554 struct power_supply *__cil_tmp156 ; 2555 struct device const *__cil_tmp157 ; 2556 unsigned long __cil_tmp158 ; 2557 unsigned long __cil_tmp159 ; 2558 unsigned long __cil_tmp160 ; 2559 unsigned long __cil_tmp161 ; 2560 int __cil_tmp162 ; 2561 unsigned int __cil_tmp163 ; 2562 unsigned int __cil_tmp164 ; 2563 void *__cil_tmp165 ; 2564 irqreturn_t (*__cil_tmp166)(int , void * ) ; 2565 void *__cil_tmp167 ; 2566 unsigned long __cil_tmp168 ; 2567 unsigned long __cil_tmp169 ; 2568 int __cil_tmp170 ; 2569 unsigned int __cil_tmp171 ; 2570 struct device const *__cil_tmp172 ; 2571 unsigned long __cil_tmp173 ; 2572 unsigned long __cil_tmp174 ; 2573 unsigned long __cil_tmp175 ; 2574 unsigned long __cil_tmp176 ; 2575 int __cil_tmp177 ; 2576 unsigned int __cil_tmp178 ; 2577 unsigned int __cil_tmp179 ; 2578 void *__cil_tmp180 ; 2579 irqreturn_t (*__cil_tmp181)(int , void * ) ; 2580 void *__cil_tmp182 ; 2581 unsigned long __cil_tmp183 ; 2582 unsigned long __cil_tmp184 ; 2583 int __cil_tmp185 ; 2584 unsigned int __cil_tmp186 ; 2585 struct device const *__cil_tmp187 ; 2586 unsigned long __cil_tmp188 ; 2587 unsigned long __cil_tmp189 ; 2588 unsigned long __cil_tmp190 ; 2589 unsigned long __cil_tmp191 ; 2590 int __cil_tmp192 ; 2591 unsigned int __cil_tmp193 ; 2592 unsigned int __cil_tmp194 ; 2593 void *__cil_tmp195 ; 2594 irqreturn_t (*__cil_tmp196)(int , void * ) ; 2595 void *__cil_tmp197 ; 2596 unsigned long __cil_tmp198 ; 2597 unsigned long __cil_tmp199 ; 2598 int __cil_tmp200 ; 2599 unsigned int __cil_tmp201 ; 2600 struct device const *__cil_tmp202 ; 2601 unsigned long __cil_tmp203 ; 2602 unsigned long __cil_tmp204 ; 2603 unsigned long __cil_tmp205 ; 2604 unsigned long __cil_tmp206 ; 2605 int __cil_tmp207 ; 2606 unsigned int __cil_tmp208 ; 2607 unsigned int __cil_tmp209 ; 2608 void *__cil_tmp210 ; 2609 unsigned long __cil_tmp211 ; 2610 unsigned long __cil_tmp212 ; 2611 unsigned long __cil_tmp213 ; 2612 unsigned long __cil_tmp214 ; 2613 int __cil_tmp215 ; 2614 unsigned int __cil_tmp216 ; 2615 unsigned int __cil_tmp217 ; 2616 void *__cil_tmp218 ; 2617 unsigned long __cil_tmp219 ; 2618 unsigned long __cil_tmp220 ; 2619 struct power_supply *__cil_tmp221 ; 2620 void const *__cil_tmp222 ; 2621 2622 { 2623 { 2624#line 186 2625 __cil_tmp34 = (unsigned long )pdev; 2626#line 186 2627 __cil_tmp35 = __cil_tmp34 + 16; 2628#line 186 2629 dev = (struct device *)__cil_tmp35; 2630#line 187 2631 __cil_tmp36 = 16 + 184; 2632#line 187 2633 __cil_tmp37 = (unsigned long )pdev; 2634#line 187 2635 __cil_tmp38 = __cil_tmp37 + __cil_tmp36; 2636#line 187 2637 __cil_tmp39 = *((void **)__cil_tmp38); 2638#line 187 2639 pdata = (struct max8903_pdata *)__cil_tmp39; 2640#line 188 2641 ret = 0; 2642#line 190 2643 ta_in = 0; 2644#line 191 2645 usb_in = 0; 2646#line 193 2647 tmp = kzalloc(264UL, 208U); 2648#line 193 2649 data = (struct max8903_data *)tmp; 2650 } 2651 { 2652#line 194 2653 __cil_tmp40 = (void *)0; 2654#line 194 2655 __cil_tmp41 = (unsigned long )__cil_tmp40; 2656#line 194 2657 __cil_tmp42 = (unsigned long )data; 2658#line 194 2659 if (__cil_tmp42 == __cil_tmp41) { 2660 { 2661#line 195 2662 __cil_tmp43 = (struct device const *)dev; 2663#line 195 2664 dev_err(__cil_tmp43, "Cannot allocate memory.\n"); 2665 } 2666#line 196 2667 return (-12); 2668 } else { 2669 2670 } 2671 } 2672#line 198 2673 __len = 32UL; 2674#line 198 2675 if (__len >= 64UL) { 2676 { 2677#line 198 2678 __cil_tmp44 = (struct max8903_pdata *)data; 2679#line 198 2680 __cil_tmp45 = (void *)__cil_tmp44; 2681#line 198 2682 __cil_tmp46 = (void const *)pdata; 2683#line 198 2684 __ret = __memcpy(__cil_tmp45, __cil_tmp46, __len); 2685 } 2686 } else { 2687 { 2688#line 198 2689 __cil_tmp47 = (struct max8903_pdata *)data; 2690#line 198 2691 __cil_tmp48 = (void *)__cil_tmp47; 2692#line 198 2693 __cil_tmp49 = (void const *)pdata; 2694#line 198 2695 __ret = __builtin_memcpy(__cil_tmp48, __cil_tmp49, __len); 2696 } 2697 } 2698 { 2699#line 199 2700 __cil_tmp50 = (unsigned long )data; 2701#line 199 2702 __cil_tmp51 = __cil_tmp50 + 32; 2703#line 199 2704 *((struct device **)__cil_tmp51) = dev; 2705#line 200 2706 __cil_tmp52 = (void *)data; 2707#line 200 2708 platform_set_drvdata(pdev, __cil_tmp52); 2709 } 2710 { 2711#line 202 2712 __cil_tmp53 = (unsigned long )pdata; 2713#line 202 2714 __cil_tmp54 = __cil_tmp53 + 28; 2715#line 202 2716 __cil_tmp55 = *((bool *)__cil_tmp54); 2717#line 202 2718 __cil_tmp56 = (int )__cil_tmp55; 2719#line 202 2720 if (__cil_tmp56 == 0) { 2721 { 2722#line 202 2723 __cil_tmp57 = (unsigned long )pdata; 2724#line 202 2725 __cil_tmp58 = __cil_tmp57 + 29; 2726#line 202 2727 __cil_tmp59 = *((bool *)__cil_tmp58); 2728#line 202 2729 __cil_tmp60 = (int )__cil_tmp59; 2730#line 202 2731 if (__cil_tmp60 == 0) { 2732 { 2733#line 203 2734 __cil_tmp61 = (struct device const *)dev; 2735#line 203 2736 dev_err(__cil_tmp61, "No valid power sources.\n"); 2737#line 204 2738 ret = -22; 2739 } 2740#line 205 2741 goto err; 2742 } else { 2743 2744 } 2745 } 2746 } else { 2747 2748 } 2749 } 2750 { 2751#line 208 2752 __cil_tmp62 = (unsigned long )pdata; 2753#line 208 2754 __cil_tmp63 = __cil_tmp62 + 28; 2755#line 208 2756 if (*((bool *)__cil_tmp63)) { 2757 { 2758#line 209 2759 __cil_tmp64 = (unsigned long )pdata; 2760#line 209 2761 __cil_tmp65 = __cil_tmp64 + 4; 2762#line 209 2763 if (*((int *)__cil_tmp65)) { 2764 { 2765#line 209 2766 __cil_tmp66 = (unsigned long )pdata; 2767#line 209 2768 __cil_tmp67 = __cil_tmp66 + 4; 2769#line 209 2770 __cil_tmp68 = *((int *)__cil_tmp67); 2771#line 209 2772 tmp___2 = gpio_is_valid(__cil_tmp68); 2773 } 2774#line 209 2775 if (tmp___2) { 2776 { 2777#line 209 2778 __cil_tmp69 = (unsigned long )pdata; 2779#line 209 2780 __cil_tmp70 = __cil_tmp69 + 20; 2781#line 209 2782 if (*((int *)__cil_tmp70)) { 2783 { 2784#line 209 2785 __cil_tmp71 = (unsigned long )pdata; 2786#line 209 2787 __cil_tmp72 = __cil_tmp71 + 20; 2788#line 209 2789 __cil_tmp73 = *((int *)__cil_tmp72); 2790#line 209 2791 tmp___3 = gpio_is_valid(__cil_tmp73); 2792 } 2793#line 209 2794 if (tmp___3) { 2795 { 2796#line 211 2797 __cil_tmp74 = (unsigned long )pdata; 2798#line 211 2799 __cil_tmp75 = __cil_tmp74 + 4; 2800#line 211 2801 gpio = *((int *)__cil_tmp75); 2802#line 212 2803 __cil_tmp76 = (unsigned int )gpio; 2804#line 212 2805 tmp___1 = gpio_get_value(__cil_tmp76); 2806 } 2807#line 212 2808 if (tmp___1) { 2809#line 212 2810 ta_in = 0; 2811 } else { 2812#line 212 2813 ta_in = 1; 2814 } 2815 { 2816#line 214 2817 __cil_tmp77 = (unsigned long )pdata; 2818#line 214 2819 __cil_tmp78 = __cil_tmp77 + 20; 2820#line 214 2821 gpio = *((int *)__cil_tmp78); 2822#line 215 2823 __cil_tmp79 = (unsigned int )gpio; 2824#line 215 2825 gpio_set_value(__cil_tmp79, ta_in); 2826 } 2827 } else { 2828 { 2829#line 217 2830 __cil_tmp80 = (struct device const *)dev; 2831#line 217 2832 dev_err(__cil_tmp80, "When DC is wired, DOK and DCM should be wired as well.\n"); 2833#line 219 2834 ret = -22; 2835 } 2836#line 220 2837 goto err; 2838 } 2839 } else { 2840 { 2841#line 217 2842 __cil_tmp81 = (struct device const *)dev; 2843#line 217 2844 dev_err(__cil_tmp81, "When DC is wired, DOK and DCM should be wired as well.\n"); 2845#line 219 2846 ret = -22; 2847 } 2848#line 220 2849 goto err; 2850 } 2851 } 2852 } else { 2853 { 2854#line 217 2855 __cil_tmp82 = (struct device const *)dev; 2856#line 217 2857 dev_err(__cil_tmp82, "When DC is wired, DOK and DCM should be wired as well.\n"); 2858#line 219 2859 ret = -22; 2860 } 2861#line 220 2862 goto err; 2863 } 2864 } else { 2865 { 2866#line 217 2867 __cil_tmp83 = (struct device const *)dev; 2868#line 217 2869 dev_err(__cil_tmp83, "When DC is wired, DOK and DCM should be wired as well.\n"); 2870#line 219 2871 ret = -22; 2872 } 2873#line 220 2874 goto err; 2875 } 2876 } 2877 } else { 2878 { 2879#line 223 2880 __cil_tmp84 = (unsigned long )pdata; 2881#line 223 2882 __cil_tmp85 = __cil_tmp84 + 20; 2883#line 223 2884 if (*((int *)__cil_tmp85)) { 2885 { 2886#line 224 2887 __cil_tmp86 = (unsigned long )pdata; 2888#line 224 2889 __cil_tmp87 = __cil_tmp86 + 20; 2890#line 224 2891 __cil_tmp88 = *((int *)__cil_tmp87); 2892#line 224 2893 tmp___4 = gpio_is_valid(__cil_tmp88); 2894 } 2895#line 224 2896 if (tmp___4) { 2897 { 2898#line 225 2899 __cil_tmp89 = (unsigned long )pdata; 2900#line 225 2901 __cil_tmp90 = __cil_tmp89 + 20; 2902#line 225 2903 __cil_tmp91 = *((int *)__cil_tmp90); 2904#line 225 2905 __cil_tmp92 = (unsigned int )__cil_tmp91; 2906#line 225 2907 gpio_set_value(__cil_tmp92, 0); 2908 } 2909 } else { 2910 { 2911#line 227 2912 __cil_tmp93 = (struct device const *)dev; 2913#line 227 2914 dev_err(__cil_tmp93, "Invalid pin: dcm.\n"); 2915#line 228 2916 ret = -22; 2917 } 2918#line 229 2919 goto err; 2920 } 2921 } else { 2922 2923 } 2924 } 2925 } 2926 } 2927 { 2928#line 234 2929 __cil_tmp94 = (unsigned long )pdata; 2930#line 234 2931 __cil_tmp95 = __cil_tmp94 + 29; 2932#line 234 2933 if (*((bool *)__cil_tmp95)) { 2934 { 2935#line 235 2936 __cil_tmp96 = (unsigned long )pdata; 2937#line 235 2938 __cil_tmp97 = __cil_tmp96 + 8; 2939#line 235 2940 if (*((int *)__cil_tmp97)) { 2941 { 2942#line 235 2943 __cil_tmp98 = (unsigned long )pdata; 2944#line 235 2945 __cil_tmp99 = __cil_tmp98 + 8; 2946#line 235 2947 __cil_tmp100 = *((int *)__cil_tmp99); 2948#line 235 2949 tmp___7 = gpio_is_valid(__cil_tmp100); 2950 } 2951#line 235 2952 if (tmp___7) { 2953 { 2954#line 236 2955 __cil_tmp101 = (unsigned long )pdata; 2956#line 236 2957 __cil_tmp102 = __cil_tmp101 + 8; 2958#line 236 2959 gpio = *((int *)__cil_tmp102); 2960#line 237 2961 __cil_tmp103 = (unsigned int )gpio; 2962#line 237 2963 tmp___6 = gpio_get_value(__cil_tmp103); 2964 } 2965#line 237 2966 if (tmp___6) { 2967#line 237 2968 usb_in = 0; 2969 } else { 2970#line 237 2971 usb_in = 1; 2972 } 2973 } else { 2974 { 2975#line 239 2976 __cil_tmp104 = (struct device const *)dev; 2977#line 239 2978 dev_err(__cil_tmp104, "When USB is wired, UOK should be wired.as well.\n"); 2979#line 241 2980 ret = -22; 2981 } 2982#line 242 2983 goto err; 2984 } 2985 } else { 2986 { 2987#line 239 2988 __cil_tmp105 = (struct device const *)dev; 2989#line 239 2990 dev_err(__cil_tmp105, "When USB is wired, UOK should be wired.as well.\n"); 2991#line 241 2992 ret = -22; 2993 } 2994#line 242 2995 goto err; 2996 } 2997 } 2998 } else { 2999 3000 } 3001 } 3002#line 246 3003 if (*((int *)pdata)) { 3004 { 3005#line 247 3006 __cil_tmp106 = *((int *)pdata); 3007#line 247 3008 tmp___9 = gpio_is_valid(__cil_tmp106); 3009 } 3010#line 247 3011 if (tmp___9) { 3012#line 248 3013 if (ta_in) { 3014#line 248 3015 tmp___8 = 0; 3016 } else 3017#line 248 3018 if (usb_in) { 3019#line 248 3020 tmp___8 = 0; 3021 } else { 3022#line 248 3023 tmp___8 = 1; 3024 } 3025 { 3026#line 248 3027 __cil_tmp107 = *((int *)pdata); 3028#line 248 3029 __cil_tmp108 = (unsigned int )__cil_tmp107; 3030#line 248 3031 gpio_set_value(__cil_tmp108, tmp___8); 3032 } 3033 } else { 3034 { 3035#line 250 3036 __cil_tmp109 = (struct device const *)dev; 3037#line 250 3038 dev_err(__cil_tmp109, "Invalid pin: cen.\n"); 3039#line 251 3040 ret = -22; 3041 } 3042#line 252 3043 goto err; 3044 } 3045 } else { 3046 3047 } 3048 { 3049#line 256 3050 __cil_tmp110 = (unsigned long )pdata; 3051#line 256 3052 __cil_tmp111 = __cil_tmp110 + 12; 3053#line 256 3054 if (*((int *)__cil_tmp111)) { 3055 { 3056#line 257 3057 __cil_tmp112 = (unsigned long )pdata; 3058#line 257 3059 __cil_tmp113 = __cil_tmp112 + 12; 3060#line 257 3061 __cil_tmp114 = *((int *)__cil_tmp113); 3062#line 257 3063 tmp___10 = gpio_is_valid(__cil_tmp114); 3064 } 3065#line 257 3066 if (tmp___10) { 3067 3068 } else { 3069 { 3070#line 258 3071 __cil_tmp115 = (struct device const *)dev; 3072#line 258 3073 dev_err(__cil_tmp115, "Invalid pin: chg.\n"); 3074#line 259 3075 ret = -22; 3076 } 3077#line 260 3078 goto err; 3079 } 3080 } else { 3081 3082 } 3083 } 3084 { 3085#line 264 3086 __cil_tmp116 = (unsigned long )pdata; 3087#line 264 3088 __cil_tmp117 = __cil_tmp116 + 16; 3089#line 264 3090 if (*((int *)__cil_tmp117)) { 3091 { 3092#line 265 3093 __cil_tmp118 = (unsigned long )pdata; 3094#line 265 3095 __cil_tmp119 = __cil_tmp118 + 16; 3096#line 265 3097 __cil_tmp120 = *((int *)__cil_tmp119); 3098#line 265 3099 tmp___11 = gpio_is_valid(__cil_tmp120); 3100 } 3101#line 265 3102 if (tmp___11) { 3103 3104 } else { 3105 { 3106#line 266 3107 __cil_tmp121 = (struct device const *)dev; 3108#line 266 3109 dev_err(__cil_tmp121, "Invalid pin: flt.\n"); 3110#line 267 3111 ret = -22; 3112 } 3113#line 268 3114 goto err; 3115 } 3116 } else { 3117 3118 } 3119 } 3120 { 3121#line 272 3122 __cil_tmp122 = (unsigned long )pdata; 3123#line 272 3124 __cil_tmp123 = __cil_tmp122 + 24; 3125#line 272 3126 if (*((int *)__cil_tmp123)) { 3127 { 3128#line 273 3129 __cil_tmp124 = (unsigned long )pdata; 3130#line 273 3131 __cil_tmp125 = __cil_tmp124 + 24; 3132#line 273 3133 __cil_tmp126 = *((int *)__cil_tmp125); 3134#line 273 3135 tmp___12 = gpio_is_valid(__cil_tmp126); 3136 } 3137#line 273 3138 if (tmp___12) { 3139 3140 } else { 3141 { 3142#line 274 3143 __cil_tmp127 = (struct device const *)dev; 3144#line 274 3145 dev_err(__cil_tmp127, "Invalid pin: usus.\n"); 3146#line 275 3147 ret = -22; 3148 } 3149#line 276 3150 goto err; 3151 } 3152 } else { 3153 3154 } 3155 } 3156#line 280 3157 __cil_tmp128 = (unsigned long )data; 3158#line 280 3159 __cil_tmp129 = __cil_tmp128 + 256; 3160#line 280 3161 *((bool *)__cil_tmp129) = (bool )0; 3162#line 281 3163 __cil_tmp130 = (unsigned long )data; 3164#line 281 3165 __cil_tmp131 = __cil_tmp130 + 258; 3166#line 281 3167 *((bool *)__cil_tmp131) = (bool )ta_in; 3168#line 282 3169 __cil_tmp132 = (unsigned long )data; 3170#line 282 3171 __cil_tmp133 = __cil_tmp132 + 257; 3172#line 282 3173 *((bool *)__cil_tmp133) = (bool )usb_in; 3174#line 284 3175 __cil_tmp134 = (unsigned long )data; 3176#line 284 3177 __cil_tmp135 = __cil_tmp134 + 40; 3178#line 284 3179 *((char const **)__cil_tmp135) = "max8903_charger"; 3180#line 285 3181 if (ta_in) { 3182#line 285 3183 __cil_tmp136 = 40 + 8; 3184#line 285 3185 __cil_tmp137 = (unsigned long )data; 3186#line 285 3187 __cil_tmp138 = __cil_tmp137 + __cil_tmp136; 3188#line 285 3189 *((enum power_supply_type *)__cil_tmp138) = (enum power_supply_type )3; 3190 } else { 3191#line 285 3192 if (usb_in) { 3193#line 285 3194 tmp___13 = 4; 3195 } else { 3196#line 285 3197 tmp___13 = 1; 3198 } 3199#line 285 3200 __cil_tmp139 = 40 + 8; 3201#line 285 3202 __cil_tmp140 = (unsigned long )data; 3203#line 285 3204 __cil_tmp141 = __cil_tmp140 + __cil_tmp139; 3205#line 285 3206 *((enum power_supply_type *)__cil_tmp141) = (enum power_supply_type )tmp___13; 3207 } 3208 { 3209#line 288 3210 __cil_tmp142 = 40 + 48; 3211#line 288 3212 __cil_tmp143 = (unsigned long )data; 3213#line 288 3214 __cil_tmp144 = __cil_tmp143 + __cil_tmp142; 3215#line 288 3216 *((int (**)(struct power_supply *psy , enum power_supply_property psp , union power_supply_propval *val ))__cil_tmp144) = & max8903_get_property; 3217#line 289 3218 __cil_tmp145 = 40 + 16; 3219#line 289 3220 __cil_tmp146 = (unsigned long )data; 3221#line 289 3222 __cil_tmp147 = __cil_tmp146 + __cil_tmp145; 3223#line 289 3224 __cil_tmp148 = 0 * 4UL; 3225#line 289 3226 __cil_tmp149 = (unsigned long )(max8903_charger_props) + __cil_tmp148; 3227#line 289 3228 *((enum power_supply_property **)__cil_tmp147) = (enum power_supply_property *)__cil_tmp149; 3229#line 290 3230 __cil_tmp150 = 40 + 24; 3231#line 290 3232 __cil_tmp151 = (unsigned long )data; 3233#line 290 3234 __cil_tmp152 = __cil_tmp151 + __cil_tmp150; 3235#line 290 3236 __cil_tmp153 = 12UL / 4UL; 3237#line 290 3238 *((size_t *)__cil_tmp152) = __cil_tmp153 + 0UL; 3239#line 292 3240 __cil_tmp154 = (unsigned long )data; 3241#line 292 3242 __cil_tmp155 = __cil_tmp154 + 40; 3243#line 292 3244 __cil_tmp156 = (struct power_supply *)__cil_tmp155; 3245#line 292 3246 ret = power_supply_register(dev, __cil_tmp156); 3247 } 3248#line 293 3249 if (ret) { 3250 { 3251#line 294 3252 __cil_tmp157 = (struct device const *)dev; 3253#line 294 3254 dev_err(__cil_tmp157, "failed: power supply register.\n"); 3255 } 3256#line 295 3257 goto err; 3258 } else { 3259 3260 } 3261 { 3262#line 298 3263 __cil_tmp158 = (unsigned long )pdata; 3264#line 298 3265 __cil_tmp159 = __cil_tmp158 + 28; 3266#line 298 3267 if (*((bool *)__cil_tmp159)) { 3268 { 3269#line 299 3270 __cil_tmp160 = (unsigned long )pdata; 3271#line 299 3272 __cil_tmp161 = __cil_tmp160 + 4; 3273#line 299 3274 __cil_tmp162 = *((int *)__cil_tmp161); 3275#line 299 3276 __cil_tmp163 = (unsigned int )__cil_tmp162; 3277#line 299 3278 tmp___14 = gpio_to_irq(__cil_tmp163); 3279#line 299 3280 __cil_tmp164 = (unsigned int )tmp___14; 3281#line 299 3282 __cil_tmp165 = (void *)0; 3283#line 299 3284 __cil_tmp166 = (irqreturn_t (*)(int , void * ))__cil_tmp165; 3285#line 299 3286 __cil_tmp167 = (void *)data; 3287#line 299 3288 ret = (int )request_threaded_irq(__cil_tmp164, __cil_tmp166, & max8903_dcin, 3UL, 3289 "MAX8903 DC IN", __cil_tmp167); 3290 } 3291#line 303 3292 if (ret) { 3293 { 3294#line 304 3295 __cil_tmp168 = (unsigned long )pdata; 3296#line 304 3297 __cil_tmp169 = __cil_tmp168 + 4; 3298#line 304 3299 __cil_tmp170 = *((int *)__cil_tmp169); 3300#line 304 3301 __cil_tmp171 = (unsigned int )__cil_tmp170; 3302#line 304 3303 tmp___15 = gpio_to_irq(__cil_tmp171); 3304#line 304 3305 __cil_tmp172 = (struct device const *)dev; 3306#line 304 3307 dev_err(__cil_tmp172, "Cannot request irq %d for DC (%d)\n", tmp___15, ret); 3308 } 3309#line 306 3310 goto err_psy; 3311 } else { 3312 3313 } 3314 } else { 3315 3316 } 3317 } 3318 { 3319#line 310 3320 __cil_tmp173 = (unsigned long )pdata; 3321#line 310 3322 __cil_tmp174 = __cil_tmp173 + 29; 3323#line 310 3324 if (*((bool *)__cil_tmp174)) { 3325 { 3326#line 311 3327 __cil_tmp175 = (unsigned long )pdata; 3328#line 311 3329 __cil_tmp176 = __cil_tmp175 + 8; 3330#line 311 3331 __cil_tmp177 = *((int *)__cil_tmp176); 3332#line 311 3333 __cil_tmp178 = (unsigned int )__cil_tmp177; 3334#line 311 3335 tmp___16 = gpio_to_irq(__cil_tmp178); 3336#line 311 3337 __cil_tmp179 = (unsigned int )tmp___16; 3338#line 311 3339 __cil_tmp180 = (void *)0; 3340#line 311 3341 __cil_tmp181 = (irqreturn_t (*)(int , void * ))__cil_tmp180; 3342#line 311 3343 __cil_tmp182 = (void *)data; 3344#line 311 3345 ret = (int )request_threaded_irq(__cil_tmp179, __cil_tmp181, & max8903_usbin, 3346 3UL, "MAX8903 USB IN", __cil_tmp182); 3347 } 3348#line 315 3349 if (ret) { 3350 { 3351#line 316 3352 __cil_tmp183 = (unsigned long )pdata; 3353#line 316 3354 __cil_tmp184 = __cil_tmp183 + 8; 3355#line 316 3356 __cil_tmp185 = *((int *)__cil_tmp184); 3357#line 316 3358 __cil_tmp186 = (unsigned int )__cil_tmp185; 3359#line 316 3360 tmp___17 = gpio_to_irq(__cil_tmp186); 3361#line 316 3362 __cil_tmp187 = (struct device const *)dev; 3363#line 316 3364 dev_err(__cil_tmp187, "Cannot request irq %d for USB (%d)\n", tmp___17, ret); 3365 } 3366#line 318 3367 goto err_dc_irq; 3368 } else { 3369 3370 } 3371 } else { 3372 3373 } 3374 } 3375 { 3376#line 322 3377 __cil_tmp188 = (unsigned long )pdata; 3378#line 322 3379 __cil_tmp189 = __cil_tmp188 + 16; 3380#line 322 3381 if (*((int *)__cil_tmp189)) { 3382 { 3383#line 323 3384 __cil_tmp190 = (unsigned long )pdata; 3385#line 323 3386 __cil_tmp191 = __cil_tmp190 + 16; 3387#line 323 3388 __cil_tmp192 = *((int *)__cil_tmp191); 3389#line 323 3390 __cil_tmp193 = (unsigned int )__cil_tmp192; 3391#line 323 3392 tmp___18 = gpio_to_irq(__cil_tmp193); 3393#line 323 3394 __cil_tmp194 = (unsigned int )tmp___18; 3395#line 323 3396 __cil_tmp195 = (void *)0; 3397#line 323 3398 __cil_tmp196 = (irqreturn_t (*)(int , void * ))__cil_tmp195; 3399#line 323 3400 __cil_tmp197 = (void *)data; 3401#line 323 3402 ret = (int )request_threaded_irq(__cil_tmp194, __cil_tmp196, & max8903_fault, 3403 3UL, "MAX8903 Fault", __cil_tmp197); 3404 } 3405#line 327 3406 if (ret) { 3407 { 3408#line 328 3409 __cil_tmp198 = (unsigned long )pdata; 3410#line 328 3411 __cil_tmp199 = __cil_tmp198 + 16; 3412#line 328 3413 __cil_tmp200 = *((int *)__cil_tmp199); 3414#line 328 3415 __cil_tmp201 = (unsigned int )__cil_tmp200; 3416#line 328 3417 tmp___19 = gpio_to_irq(__cil_tmp201); 3418#line 328 3419 __cil_tmp202 = (struct device const *)dev; 3420#line 328 3421 dev_err(__cil_tmp202, "Cannot request irq %d for Fault (%d)\n", tmp___19, ret); 3422 } 3423#line 330 3424 goto err_usb_irq; 3425 } else { 3426 3427 } 3428 } else { 3429 3430 } 3431 } 3432#line 334 3433 return (0); 3434 err_usb_irq: 3435 { 3436#line 337 3437 __cil_tmp203 = (unsigned long )pdata; 3438#line 337 3439 __cil_tmp204 = __cil_tmp203 + 29; 3440#line 337 3441 if (*((bool *)__cil_tmp204)) { 3442 { 3443#line 338 3444 __cil_tmp205 = (unsigned long )pdata; 3445#line 338 3446 __cil_tmp206 = __cil_tmp205 + 8; 3447#line 338 3448 __cil_tmp207 = *((int *)__cil_tmp206); 3449#line 338 3450 __cil_tmp208 = (unsigned int )__cil_tmp207; 3451#line 338 3452 tmp___20 = gpio_to_irq(__cil_tmp208); 3453#line 338 3454 __cil_tmp209 = (unsigned int )tmp___20; 3455#line 338 3456 __cil_tmp210 = (void *)data; 3457#line 338 3458 free_irq(__cil_tmp209, __cil_tmp210); 3459 } 3460 } else { 3461 3462 } 3463 } 3464 err_dc_irq: 3465 { 3466#line 340 3467 __cil_tmp211 = (unsigned long )pdata; 3468#line 340 3469 __cil_tmp212 = __cil_tmp211 + 28; 3470#line 340 3471 if (*((bool *)__cil_tmp212)) { 3472 { 3473#line 341 3474 __cil_tmp213 = (unsigned long )pdata; 3475#line 341 3476 __cil_tmp214 = __cil_tmp213 + 4; 3477#line 341 3478 __cil_tmp215 = *((int *)__cil_tmp214); 3479#line 341 3480 __cil_tmp216 = (unsigned int )__cil_tmp215; 3481#line 341 3482 tmp___21 = gpio_to_irq(__cil_tmp216); 3483#line 341 3484 __cil_tmp217 = (unsigned int )tmp___21; 3485#line 341 3486 __cil_tmp218 = (void *)data; 3487#line 341 3488 free_irq(__cil_tmp217, __cil_tmp218); 3489 } 3490 } else { 3491 3492 } 3493 } 3494 err_psy: 3495 { 3496#line 343 3497 __cil_tmp219 = (unsigned long )data; 3498#line 343 3499 __cil_tmp220 = __cil_tmp219 + 40; 3500#line 343 3501 __cil_tmp221 = (struct power_supply *)__cil_tmp220; 3502#line 343 3503 power_supply_unregister(__cil_tmp221); 3504 } 3505 err: 3506 { 3507#line 345 3508 __cil_tmp222 = (void const *)data; 3509#line 345 3510 kfree(__cil_tmp222); 3511 } 3512#line 346 3513 return (ret); 3514} 3515} 3516#line 349 3517static int max8903_remove(struct platform_device *pdev ) __attribute__((__section__(".devexit.text"), 3518__no_instrument_function__)) ; 3519#line 349 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/drivers/power/max8903_charger.c.common.c" 3520static int max8903_remove(struct platform_device *pdev ) 3521{ struct max8903_data *data ; 3522 void *tmp ; 3523 struct max8903_pdata *pdata ; 3524 int tmp___0 ; 3525 int tmp___1 ; 3526 int tmp___2 ; 3527 struct platform_device const *__cil_tmp8 ; 3528 unsigned long __cil_tmp9 ; 3529 unsigned long __cil_tmp10 ; 3530 unsigned long __cil_tmp11 ; 3531 unsigned long __cil_tmp12 ; 3532 int __cil_tmp13 ; 3533 unsigned int __cil_tmp14 ; 3534 unsigned int __cil_tmp15 ; 3535 void *__cil_tmp16 ; 3536 unsigned long __cil_tmp17 ; 3537 unsigned long __cil_tmp18 ; 3538 unsigned long __cil_tmp19 ; 3539 unsigned long __cil_tmp20 ; 3540 int __cil_tmp21 ; 3541 unsigned int __cil_tmp22 ; 3542 unsigned int __cil_tmp23 ; 3543 void *__cil_tmp24 ; 3544 unsigned long __cil_tmp25 ; 3545 unsigned long __cil_tmp26 ; 3546 unsigned long __cil_tmp27 ; 3547 unsigned long __cil_tmp28 ; 3548 int __cil_tmp29 ; 3549 unsigned int __cil_tmp30 ; 3550 unsigned int __cil_tmp31 ; 3551 void *__cil_tmp32 ; 3552 unsigned long __cil_tmp33 ; 3553 unsigned long __cil_tmp34 ; 3554 struct power_supply *__cil_tmp35 ; 3555 void const *__cil_tmp36 ; 3556 3557 { 3558 { 3559#line 351 3560 __cil_tmp8 = (struct platform_device const *)pdev; 3561#line 351 3562 tmp = platform_get_drvdata(__cil_tmp8); 3563#line 351 3564 data = (struct max8903_data *)tmp; 3565 } 3566#line 353 3567 if (data) { 3568#line 354 3569 pdata = (struct max8903_pdata *)data; 3570 { 3571#line 356 3572 __cil_tmp9 = (unsigned long )pdata; 3573#line 356 3574 __cil_tmp10 = __cil_tmp9 + 16; 3575#line 356 3576 if (*((int *)__cil_tmp10)) { 3577 { 3578#line 357 3579 __cil_tmp11 = (unsigned long )pdata; 3580#line 357 3581 __cil_tmp12 = __cil_tmp11 + 16; 3582#line 357 3583 __cil_tmp13 = *((int *)__cil_tmp12); 3584#line 357 3585 __cil_tmp14 = (unsigned int )__cil_tmp13; 3586#line 357 3587 tmp___0 = gpio_to_irq(__cil_tmp14); 3588#line 357 3589 __cil_tmp15 = (unsigned int )tmp___0; 3590#line 357 3591 __cil_tmp16 = (void *)data; 3592#line 357 3593 free_irq(__cil_tmp15, __cil_tmp16); 3594 } 3595 } else { 3596 3597 } 3598 } 3599 { 3600#line 358 3601 __cil_tmp17 = (unsigned long )pdata; 3602#line 358 3603 __cil_tmp18 = __cil_tmp17 + 29; 3604#line 358 3605 if (*((bool *)__cil_tmp18)) { 3606 { 3607#line 359 3608 __cil_tmp19 = (unsigned long )pdata; 3609#line 359 3610 __cil_tmp20 = __cil_tmp19 + 8; 3611#line 359 3612 __cil_tmp21 = *((int *)__cil_tmp20); 3613#line 359 3614 __cil_tmp22 = (unsigned int )__cil_tmp21; 3615#line 359 3616 tmp___1 = gpio_to_irq(__cil_tmp22); 3617#line 359 3618 __cil_tmp23 = (unsigned int )tmp___1; 3619#line 359 3620 __cil_tmp24 = (void *)data; 3621#line 359 3622 free_irq(__cil_tmp23, __cil_tmp24); 3623 } 3624 } else { 3625 3626 } 3627 } 3628 { 3629#line 360 3630 __cil_tmp25 = (unsigned long )pdata; 3631#line 360 3632 __cil_tmp26 = __cil_tmp25 + 28; 3633#line 360 3634 if (*((bool *)__cil_tmp26)) { 3635 { 3636#line 361 3637 __cil_tmp27 = (unsigned long )pdata; 3638#line 361 3639 __cil_tmp28 = __cil_tmp27 + 4; 3640#line 361 3641 __cil_tmp29 = *((int *)__cil_tmp28); 3642#line 361 3643 __cil_tmp30 = (unsigned int )__cil_tmp29; 3644#line 361 3645 tmp___2 = gpio_to_irq(__cil_tmp30); 3646#line 361 3647 __cil_tmp31 = (unsigned int )tmp___2; 3648#line 361 3649 __cil_tmp32 = (void *)data; 3650#line 361 3651 free_irq(__cil_tmp31, __cil_tmp32); 3652 } 3653 } else { 3654 3655 } 3656 } 3657 { 3658#line 362 3659 __cil_tmp33 = (unsigned long )data; 3660#line 362 3661 __cil_tmp34 = __cil_tmp33 + 40; 3662#line 362 3663 __cil_tmp35 = (struct power_supply *)__cil_tmp34; 3664#line 362 3665 power_supply_unregister(__cil_tmp35); 3666#line 363 3667 __cil_tmp36 = (void const *)data; 3668#line 363 3669 kfree(__cil_tmp36); 3670 } 3671 } else { 3672 3673 } 3674#line 366 3675 return (0); 3676} 3677} 3678#line 369 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/drivers/power/max8903_charger.c.common.c" 3679static struct platform_driver max8903_driver = {& max8903_probe, & max8903_remove, (void (*)(struct platform_device * ))0, (int (*)(struct platform_device * , 3680 pm_message_t state ))0, 3681 (int (*)(struct platform_device * ))0, {"max8903-charger", (struct bus_type *)0, 3682 & __this_module, (char const *)0, (_Bool)0, 3683 (struct of_device_id const *)0, (int (*)(struct device *dev ))0, 3684 (int (*)(struct device *dev ))0, (void (*)(struct device *dev ))0, 3685 (int (*)(struct device *dev , pm_message_t state ))0, 3686 (int (*)(struct device *dev ))0, (struct attribute_group const **)0, 3687 (struct dev_pm_ops const *)0, (struct driver_private *)0}, 3688 (struct platform_device_id const *)0}; 3689#line 378 3690static int max8903_driver_init(void) __attribute__((__section__(".init.text"), __no_instrument_function__)) ; 3691#line 378 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/drivers/power/max8903_charger.c.common.c" 3692static int max8903_driver_init(void) 3693{ int tmp ; 3694 3695 { 3696 { 3697#line 378 3698 tmp = platform_driver_register(& max8903_driver); 3699 } 3700#line 378 3701 return (tmp); 3702} 3703} 3704#line 378 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/drivers/power/max8903_charger.c.common.c" 3705int init_module(void) 3706{ int tmp ; 3707 3708 { 3709 { 3710#line 378 3711 tmp = max8903_driver_init(); 3712 } 3713#line 378 3714 return (tmp); 3715} 3716} 3717#line 378 3718static void max8903_driver_exit(void) __attribute__((__section__(".exit.text"), __no_instrument_function__)) ; 3719#line 378 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/drivers/power/max8903_charger.c.common.c" 3720static void max8903_driver_exit(void) 3721{ 3722 3723 { 3724 { 3725#line 378 3726 platform_driver_unregister(& max8903_driver); 3727 } 3728#line 378 3729 return; 3730} 3731} 3732#line 378 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/drivers/power/max8903_charger.c.common.c" 3733void cleanup_module(void) 3734{ 3735 3736 { 3737 { 3738#line 378 3739 max8903_driver_exit(); 3740 } 3741#line 378 3742 return; 3743} 3744} 3745#line 380 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/drivers/power/max8903_charger.c.common.c" 3746static char const __mod_license380[12] __attribute__((__used__, __unused__, __section__(".modinfo"), 3747__aligned__(1))) = 3748#line 380 3749 { (char const )'l', (char const )'i', (char const )'c', (char const )'e', 3750 (char const )'n', (char const )'s', (char const )'e', (char const )'=', 3751 (char const )'G', (char const )'P', (char const )'L', (char const )'\000'}; 3752#line 381 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/drivers/power/max8903_charger.c.common.c" 3753static char const __mod_description381[35] __attribute__((__used__, __unused__, 3754__section__(".modinfo"), __aligned__(1))) = 3755#line 381 3756 { (char const )'d', (char const )'e', (char const )'s', (char const )'c', 3757 (char const )'r', (char const )'i', (char const )'p', (char const )'t', 3758 (char const )'i', (char const )'o', (char const )'n', (char const )'=', 3759 (char const )'M', (char const )'A', (char const )'X', (char const )'8', 3760 (char const )'9', (char const )'0', (char const )'3', (char const )' ', 3761 (char const )'C', (char const )'h', (char const )'a', (char const )'r', 3762 (char const )'g', (char const )'e', (char const )'r', (char const )' ', 3763 (char const )'D', (char const )'r', (char const )'i', (char const )'v', 3764 (char const )'e', (char const )'r', (char const )'\000'}; 3765#line 382 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/drivers/power/max8903_charger.c.common.c" 3766static char const __mod_author382[47] __attribute__((__used__, __unused__, __section__(".modinfo"), 3767__aligned__(1))) = 3768#line 382 3769 { (char const )'a', (char const )'u', (char const )'t', (char const )'h', 3770 (char const )'o', (char const )'r', (char const )'=', (char const )'M', 3771 (char const )'y', (char const )'u', (char const )'n', (char const )'g', 3772 (char const )'J', (char const )'o', (char const )'o', (char const )' ', 3773 (char const )'H', (char const )'a', (char const )'m', (char const )' ', 3774 (char const )'<', (char const )'m', (char const )'y', (char const )'u', 3775 (char const )'n', (char const )'g', (char const )'j', (char const )'o', 3776 (char const )'o', (char const )'.', (char const )'h', (char const )'a', 3777 (char const )'m', (char const )'@', (char const )'s', (char const )'a', 3778 (char const )'m', (char const )'s', (char const )'u', (char const )'n', 3779 (char const )'g', (char const )'.', (char const )'c', (char const )'o', 3780 (char const )'m', (char const )'>', (char const )'\000'}; 3781#line 383 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/drivers/power/max8903_charger.c.common.c" 3782static char const __mod_alias383[31] __attribute__((__used__, __unused__, __section__(".modinfo"), 3783__aligned__(1))) = 3784#line 383 3785 { (char const )'a', (char const )'l', (char const )'i', (char const )'a', 3786 (char const )'s', (char const )'=', (char const )'p', (char const )'l', 3787 (char const )'a', (char const )'t', (char const )'f', (char const )'o', 3788 (char const )'r', (char const )'m', (char const )':', (char const )'m', 3789 (char const )'a', (char const )'x', (char const )'8', (char const )'9', 3790 (char const )'0', (char const )'3', (char const )'-', (char const )'c', 3791 (char const )'h', (char const )'a', (char const )'r', (char const )'g', 3792 (char const )'e', (char const )'r', (char const )'\000'}; 3793#line 401 3794void ldv_check_final_state(void) ; 3795#line 404 3796extern void ldv_check_return_value(int res ) ; 3797#line 407 3798extern void ldv_initialize(void) ; 3799#line 410 3800extern int __VERIFIER_nondet_int(void) ; 3801#line 413 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/drivers/power/max8903_charger.c.common.c" 3802int LDV_IN_INTERRUPT ; 3803#line 428 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/drivers/power/max8903_charger.c.common.c" 3804static int res_max8903_probe_4 ; 3805#line 416 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/drivers/power/max8903_charger.c.common.c" 3806void main(void) 3807{ struct platform_device *var_group1 ; 3808 int var_max8903_dcin_1_p0 ; 3809 void *var_max8903_dcin_1_p1 ; 3810 int var_max8903_fault_3_p0 ; 3811 void *var_max8903_fault_3_p1 ; 3812 int var_max8903_usbin_2_p0 ; 3813 void *var_max8903_usbin_2_p1 ; 3814 int ldv_s_max8903_driver_platform_driver ; 3815 int tmp ; 3816 int tmp___0 ; 3817 int __cil_tmp11 ; 3818 3819 { 3820 { 3821#line 456 3822 LDV_IN_INTERRUPT = 1; 3823#line 465 3824 ldv_initialize(); 3825#line 466 3826 ldv_s_max8903_driver_platform_driver = 0; 3827 } 3828 { 3829#line 471 3830 while (1) { 3831 while_continue: /* CIL Label */ ; 3832 { 3833#line 471 3834 tmp___0 = __VERIFIER_nondet_int(); 3835 } 3836#line 471 3837 if (tmp___0) { 3838 3839 } else { 3840 { 3841#line 471 3842 __cil_tmp11 = ldv_s_max8903_driver_platform_driver == 0; 3843#line 471 3844 if (! __cil_tmp11) { 3845 3846 } else { 3847#line 471 3848 goto while_break; 3849 } 3850 } 3851 } 3852 { 3853#line 475 3854 tmp = __VERIFIER_nondet_int(); 3855 } 3856#line 477 3857 if (tmp == 0) { 3858#line 477 3859 goto case_0; 3860 } else 3861#line 496 3862 if (tmp == 1) { 3863#line 496 3864 goto case_1; 3865 } else 3866#line 512 3867 if (tmp == 2) { 3868#line 512 3869 goto case_2; 3870 } else 3871#line 528 3872 if (tmp == 3) { 3873#line 528 3874 goto case_3; 3875 } else { 3876 { 3877#line 544 3878 goto switch_default; 3879#line 475 3880 if (0) { 3881 case_0: /* CIL Label */ 3882#line 480 3883 if (ldv_s_max8903_driver_platform_driver == 0) { 3884 { 3885#line 485 3886 res_max8903_probe_4 = max8903_probe(var_group1); 3887#line 486 3888 ldv_check_return_value(res_max8903_probe_4); 3889 } 3890#line 487 3891 if (res_max8903_probe_4) { 3892#line 488 3893 goto ldv_module_exit; 3894 } else { 3895 3896 } 3897#line 489 3898 ldv_s_max8903_driver_platform_driver = 0; 3899 } else { 3900 3901 } 3902#line 495 3903 goto switch_break; 3904 case_1: /* CIL Label */ 3905 { 3906#line 499 3907 LDV_IN_INTERRUPT = 2; 3908#line 504 3909 max8903_dcin(var_max8903_dcin_1_p0, var_max8903_dcin_1_p1); 3910#line 505 3911 LDV_IN_INTERRUPT = 1; 3912 } 3913#line 511 3914 goto switch_break; 3915 case_2: /* CIL Label */ 3916 { 3917#line 515 3918 LDV_IN_INTERRUPT = 2; 3919#line 520 3920 max8903_fault(var_max8903_fault_3_p0, var_max8903_fault_3_p1); 3921#line 521 3922 LDV_IN_INTERRUPT = 1; 3923 } 3924#line 527 3925 goto switch_break; 3926 case_3: /* CIL Label */ 3927 { 3928#line 531 3929 LDV_IN_INTERRUPT = 2; 3930#line 536 3931 max8903_usbin(var_max8903_usbin_2_p0, var_max8903_usbin_2_p1); 3932#line 537 3933 LDV_IN_INTERRUPT = 1; 3934 } 3935#line 543 3936 goto switch_break; 3937 switch_default: /* CIL Label */ 3938#line 544 3939 goto switch_break; 3940 } else { 3941 switch_break: /* CIL Label */ ; 3942 } 3943 } 3944 } 3945 } 3946 while_break: /* CIL Label */ ; 3947 } 3948 ldv_module_exit: 3949 { 3950#line 553 3951 ldv_check_final_state(); 3952 } 3953#line 556 3954 return; 3955} 3956} 3957#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h" 3958void ldv_blast_assert(void) 3959{ 3960 3961 { 3962 ERROR: 3963#line 6 3964 goto ERROR; 3965} 3966} 3967#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h" 3968extern int __VERIFIER_nondet_int(void) ; 3969#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c" 3970int ldv_mutex = 1; 3971#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c" 3972int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock ) 3973{ int nondetermined ; 3974 3975 { 3976#line 29 3977 if (ldv_mutex == 1) { 3978 3979 } else { 3980 { 3981#line 29 3982 ldv_blast_assert(); 3983 } 3984 } 3985 { 3986#line 32 3987 nondetermined = __VERIFIER_nondet_int(); 3988 } 3989#line 35 3990 if (nondetermined) { 3991#line 38 3992 ldv_mutex = 2; 3993#line 40 3994 return (0); 3995 } else { 3996#line 45 3997 return (-4); 3998 } 3999} 4000} 4001#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c" 4002int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock ) 4003{ int nondetermined ; 4004 4005 { 4006#line 57 4007 if (ldv_mutex == 1) { 4008 4009 } else { 4010 { 4011#line 57 4012 ldv_blast_assert(); 4013 } 4014 } 4015 { 4016#line 60 4017 nondetermined = __VERIFIER_nondet_int(); 4018 } 4019#line 63 4020 if (nondetermined) { 4021#line 66 4022 ldv_mutex = 2; 4023#line 68 4024 return (0); 4025 } else { 4026#line 73 4027 return (-4); 4028 } 4029} 4030} 4031#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c" 4032int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) 4033{ int atomic_value_after_dec ; 4034 4035 { 4036#line 83 4037 if (ldv_mutex == 1) { 4038 4039 } else { 4040 { 4041#line 83 4042 ldv_blast_assert(); 4043 } 4044 } 4045 { 4046#line 86 4047 atomic_value_after_dec = __VERIFIER_nondet_int(); 4048 } 4049#line 89 4050 if (atomic_value_after_dec == 0) { 4051#line 92 4052 ldv_mutex = 2; 4053#line 94 4054 return (1); 4055 } else { 4056 4057 } 4058#line 98 4059 return (0); 4060} 4061} 4062#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c" 4063void mutex_lock(struct mutex *lock ) 4064{ 4065 4066 { 4067#line 108 4068 if (ldv_mutex == 1) { 4069 4070 } else { 4071 { 4072#line 108 4073 ldv_blast_assert(); 4074 } 4075 } 4076#line 110 4077 ldv_mutex = 2; 4078#line 111 4079 return; 4080} 4081} 4082#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c" 4083int mutex_trylock(struct mutex *lock ) 4084{ int nondetermined ; 4085 4086 { 4087#line 121 4088 if (ldv_mutex == 1) { 4089 4090 } else { 4091 { 4092#line 121 4093 ldv_blast_assert(); 4094 } 4095 } 4096 { 4097#line 124 4098 nondetermined = __VERIFIER_nondet_int(); 4099 } 4100#line 127 4101 if (nondetermined) { 4102#line 130 4103 ldv_mutex = 2; 4104#line 132 4105 return (1); 4106 } else { 4107#line 137 4108 return (0); 4109 } 4110} 4111} 4112#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c" 4113void mutex_unlock(struct mutex *lock ) 4114{ 4115 4116 { 4117#line 147 4118 if (ldv_mutex == 2) { 4119 4120 } else { 4121 { 4122#line 147 4123 ldv_blast_assert(); 4124 } 4125 } 4126#line 149 4127 ldv_mutex = 1; 4128#line 150 4129 return; 4130} 4131} 4132#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c" 4133void ldv_check_final_state(void) 4134{ 4135 4136 { 4137#line 156 4138 if (ldv_mutex == 1) { 4139 4140 } else { 4141 { 4142#line 156 4143 ldv_blast_assert(); 4144 } 4145 } 4146#line 157 4147 return; 4148} 4149} 4150#line 565 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/drivers/power/max8903_charger.c.common.c" 4151long s__builtin_expect(long val , long res ) 4152{ 4153 4154 { 4155#line 566 4156 return (val); 4157} 4158}

User:	Jiri Slaby
Error type:	Reachable Error Location
Error type description:	A specified error location is reachable in some program path
File location:	ldv-linux-3.4/32_1_cilled_safe_ok_nondet_linux-3.4-32_1-drivers--power--max8903_charger.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file:	3962
Project:	SV-COMP 2013
Project version:	2.6.28
Tools:	Manual Work
Entered:	2013-01-17 16:57:54 UTC

ClabureDB: Classified Bug-Reports Database

Project: SV-COMP 2013

Showing error 580

Source: