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 49 "include/asm-generic/int-ll64.h" 15typedef unsigned int u32; 16#line 51 "include/asm-generic/int-ll64.h" 17typedef long long s64; 18#line 52 "include/asm-generic/int-ll64.h" 19typedef unsigned long long u64; 20#line 14 "include/asm-generic/posix_types.h" 21typedef long __kernel_long_t; 22#line 15 "include/asm-generic/posix_types.h" 23typedef unsigned long __kernel_ulong_t; 24#line 75 "include/asm-generic/posix_types.h" 25typedef __kernel_ulong_t __kernel_size_t; 26#line 76 "include/asm-generic/posix_types.h" 27typedef __kernel_long_t __kernel_ssize_t; 28#line 91 "include/asm-generic/posix_types.h" 29typedef long long __kernel_loff_t; 30#line 21 "include/linux/types.h" 31typedef __u32 __kernel_dev_t; 32#line 24 "include/linux/types.h" 33typedef __kernel_dev_t dev_t; 34#line 27 "include/linux/types.h" 35typedef unsigned short umode_t; 36#line 38 "include/linux/types.h" 37typedef _Bool bool; 38#line 54 "include/linux/types.h" 39typedef __kernel_loff_t loff_t; 40#line 63 "include/linux/types.h" 41typedef __kernel_size_t size_t; 42#line 68 "include/linux/types.h" 43typedef __kernel_ssize_t ssize_t; 44#line 202 "include/linux/types.h" 45typedef unsigned int gfp_t; 46#line 206 "include/linux/types.h" 47typedef u64 phys_addr_t; 48#line 211 "include/linux/types.h" 49typedef phys_addr_t resource_size_t; 50#line 219 "include/linux/types.h" 51struct __anonstruct_atomic_t_7 { 52 int counter ; 53}; 54#line 219 "include/linux/types.h" 55typedef struct __anonstruct_atomic_t_7 atomic_t; 56#line 224 "include/linux/types.h" 57struct __anonstruct_atomic64_t_8 { 58 long counter ; 59}; 60#line 224 "include/linux/types.h" 61typedef struct __anonstruct_atomic64_t_8 atomic64_t; 62#line 229 "include/linux/types.h" 63struct list_head { 64 struct list_head *next ; 65 struct list_head *prev ; 66}; 67#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h" 68typedef u16 __ticket_t; 69#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h" 70typedef u32 __ticketpair_t; 71#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h" 72struct __raw_tickets { 73 __ticket_t head ; 74 __ticket_t tail ; 75}; 76#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h" 77union __anonunion____missing_field_name_9 { 78 __ticketpair_t head_tail ; 79 struct __raw_tickets tickets ; 80}; 81#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h" 82struct arch_spinlock { 83 union __anonunion____missing_field_name_9 __annonCompField4 ; 84}; 85#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h" 86typedef struct arch_spinlock arch_spinlock_t; 87#line 12 "include/linux/lockdep.h" 88struct task_struct; 89#line 12 90struct task_struct; 91#line 391 "include/linux/lockdep.h" 92struct lock_class_key { 93 94}; 95#line 20 "include/linux/spinlock_types.h" 96struct raw_spinlock { 97 arch_spinlock_t raw_lock ; 98 unsigned int magic ; 99 unsigned int owner_cpu ; 100 void *owner ; 101}; 102#line 64 "include/linux/spinlock_types.h" 103union __anonunion____missing_field_name_12 { 104 struct raw_spinlock rlock ; 105}; 106#line 64 "include/linux/spinlock_types.h" 107struct spinlock { 108 union __anonunion____missing_field_name_12 __annonCompField6 ; 109}; 110#line 64 "include/linux/spinlock_types.h" 111typedef struct spinlock spinlock_t; 112#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h" 113struct task_struct; 114#line 146 "include/linux/init.h" 115typedef void (*ctor_fn_t)(void); 116#line 282 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h" 117struct page; 118#line 295 119struct file; 120#line 295 121struct file; 122#line 46 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h" 123struct page; 124#line 52 125struct task_struct; 126#line 329 127struct arch_spinlock; 128#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h" 129struct task_struct; 130#line 56 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h" 131struct module; 132#line 56 133struct module; 134#line 9 "include/linux/dynamic_debug.h" 135struct _ddebug { 136 char const *modname ; 137 char const *function ; 138 char const *filename ; 139 char const *format ; 140 unsigned int lineno : 18 ; 141 unsigned int flags : 8 ; 142} __attribute__((__aligned__(8))) ; 143#line 47 144struct device; 145#line 47 146struct device; 147#line 135 "include/linux/kernel.h" 148struct completion; 149#line 135 150struct completion; 151#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h" 152struct task_struct; 153#line 18 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page.h" 154struct page; 155#line 10 "include/asm-generic/bug.h" 156struct bug_entry { 157 int bug_addr_disp ; 158 int file_disp ; 159 unsigned short line ; 160 unsigned short flags ; 161}; 162#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h" 163struct static_key; 164#line 234 165struct static_key; 166#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h" 167struct kmem_cache; 168#line 23 "include/asm-generic/atomic-long.h" 169typedef atomic64_t atomic_long_t; 170#line 48 "include/linux/mutex.h" 171struct mutex { 172 atomic_t count ; 173 spinlock_t wait_lock ; 174 struct list_head wait_list ; 175 struct task_struct *owner ; 176 char const *name ; 177 void *magic ; 178}; 179#line 18 "include/linux/ioport.h" 180struct resource { 181 resource_size_t start ; 182 resource_size_t end ; 183 char const *name ; 184 unsigned long flags ; 185 struct resource *parent ; 186 struct resource *sibling ; 187 struct resource *child ; 188}; 189#line 202 190struct device; 191#line 20 "include/linux/kobject_ns.h" 192struct sock; 193#line 20 194struct sock; 195#line 21 196struct kobject; 197#line 21 198struct kobject; 199#line 27 200enum kobj_ns_type { 201 KOBJ_NS_TYPE_NONE = 0, 202 KOBJ_NS_TYPE_NET = 1, 203 KOBJ_NS_TYPES = 2 204} ; 205#line 40 "include/linux/kobject_ns.h" 206struct kobj_ns_type_operations { 207 enum kobj_ns_type type ; 208 void *(*grab_current_ns)(void) ; 209 void const *(*netlink_ns)(struct sock *sk ) ; 210 void const *(*initial_ns)(void) ; 211 void (*drop_ns)(void * ) ; 212}; 213#line 22 "include/linux/sysfs.h" 214struct kobject; 215#line 23 216struct module; 217#line 24 218enum kobj_ns_type; 219#line 26 "include/linux/sysfs.h" 220struct attribute { 221 char const *name ; 222 umode_t mode ; 223}; 224#line 56 "include/linux/sysfs.h" 225struct attribute_group { 226 char const *name ; 227 umode_t (*is_visible)(struct kobject * , struct attribute * , int ) ; 228 struct attribute **attrs ; 229}; 230#line 85 231struct file; 232#line 86 233struct vm_area_struct; 234#line 86 235struct vm_area_struct; 236#line 88 "include/linux/sysfs.h" 237struct bin_attribute { 238 struct attribute attr ; 239 size_t size ; 240 void *private ; 241 ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * , 242 loff_t , size_t ) ; 243 ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * , 244 loff_t , size_t ) ; 245 int (*mmap)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ) ; 246}; 247#line 112 "include/linux/sysfs.h" 248struct sysfs_ops { 249 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ; 250 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ; 251 void const *(*namespace)(struct kobject * , struct attribute const * ) ; 252}; 253#line 118 254struct sysfs_dirent; 255#line 118 256struct sysfs_dirent; 257#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h" 258struct task_struct; 259#line 22 "include/linux/kref.h" 260struct kref { 261 atomic_t refcount ; 262}; 263#line 49 "include/linux/wait.h" 264struct __wait_queue_head { 265 spinlock_t lock ; 266 struct list_head task_list ; 267}; 268#line 53 "include/linux/wait.h" 269typedef struct __wait_queue_head wait_queue_head_t; 270#line 55 271struct task_struct; 272#line 60 "include/linux/kobject.h" 273struct kset; 274#line 60 275struct kobj_type; 276#line 60 "include/linux/kobject.h" 277struct kobject { 278 char const *name ; 279 struct list_head entry ; 280 struct kobject *parent ; 281 struct kset *kset ; 282 struct kobj_type *ktype ; 283 struct sysfs_dirent *sd ; 284 struct kref kref ; 285 unsigned int state_initialized : 1 ; 286 unsigned int state_in_sysfs : 1 ; 287 unsigned int state_add_uevent_sent : 1 ; 288 unsigned int state_remove_uevent_sent : 1 ; 289 unsigned int uevent_suppress : 1 ; 290}; 291#line 108 "include/linux/kobject.h" 292struct kobj_type { 293 void (*release)(struct kobject *kobj ) ; 294 struct sysfs_ops const *sysfs_ops ; 295 struct attribute **default_attrs ; 296 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject *kobj ) ; 297 void const *(*namespace)(struct kobject *kobj ) ; 298}; 299#line 116 "include/linux/kobject.h" 300struct kobj_uevent_env { 301 char *envp[32] ; 302 int envp_idx ; 303 char buf[2048] ; 304 int buflen ; 305}; 306#line 123 "include/linux/kobject.h" 307struct kset_uevent_ops { 308 int (* const filter)(struct kset *kset , struct kobject *kobj ) ; 309 char const *(* const name)(struct kset *kset , struct kobject *kobj ) ; 310 int (* const uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ; 311}; 312#line 140 313struct sock; 314#line 159 "include/linux/kobject.h" 315struct kset { 316 struct list_head list ; 317 spinlock_t list_lock ; 318 struct kobject kobj ; 319 struct kset_uevent_ops const *uevent_ops ; 320}; 321#line 19 "include/linux/klist.h" 322struct klist_node; 323#line 19 324struct klist_node; 325#line 39 "include/linux/klist.h" 326struct klist_node { 327 void *n_klist ; 328 struct list_head n_node ; 329 struct kref n_ref ; 330}; 331#line 46 "include/linux/ktime.h" 332union ktime { 333 s64 tv64 ; 334}; 335#line 59 "include/linux/ktime.h" 336typedef union ktime ktime_t; 337#line 10 "include/linux/timer.h" 338struct tvec_base; 339#line 10 340struct tvec_base; 341#line 12 "include/linux/timer.h" 342struct timer_list { 343 struct list_head entry ; 344 unsigned long expires ; 345 struct tvec_base *base ; 346 void (*function)(unsigned long ) ; 347 unsigned long data ; 348 int slack ; 349 int start_pid ; 350 void *start_site ; 351 char start_comm[16] ; 352}; 353#line 17 "include/linux/workqueue.h" 354struct work_struct; 355#line 17 356struct work_struct; 357#line 79 "include/linux/workqueue.h" 358struct work_struct { 359 atomic_long_t data ; 360 struct list_head entry ; 361 void (*func)(struct work_struct *work ) ; 362}; 363#line 25 "include/linux/completion.h" 364struct completion { 365 unsigned int done ; 366 wait_queue_head_t wait ; 367}; 368#line 42 "include/linux/pm.h" 369struct device; 370#line 50 "include/linux/pm.h" 371struct pm_message { 372 int event ; 373}; 374#line 50 "include/linux/pm.h" 375typedef struct pm_message pm_message_t; 376#line 264 "include/linux/pm.h" 377struct dev_pm_ops { 378 int (*prepare)(struct device *dev ) ; 379 void (*complete)(struct device *dev ) ; 380 int (*suspend)(struct device *dev ) ; 381 int (*resume)(struct device *dev ) ; 382 int (*freeze)(struct device *dev ) ; 383 int (*thaw)(struct device *dev ) ; 384 int (*poweroff)(struct device *dev ) ; 385 int (*restore)(struct device *dev ) ; 386 int (*suspend_late)(struct device *dev ) ; 387 int (*resume_early)(struct device *dev ) ; 388 int (*freeze_late)(struct device *dev ) ; 389 int (*thaw_early)(struct device *dev ) ; 390 int (*poweroff_late)(struct device *dev ) ; 391 int (*restore_early)(struct device *dev ) ; 392 int (*suspend_noirq)(struct device *dev ) ; 393 int (*resume_noirq)(struct device *dev ) ; 394 int (*freeze_noirq)(struct device *dev ) ; 395 int (*thaw_noirq)(struct device *dev ) ; 396 int (*poweroff_noirq)(struct device *dev ) ; 397 int (*restore_noirq)(struct device *dev ) ; 398 int (*runtime_suspend)(struct device *dev ) ; 399 int (*runtime_resume)(struct device *dev ) ; 400 int (*runtime_idle)(struct device *dev ) ; 401}; 402#line 458 403enum rpm_status { 404 RPM_ACTIVE = 0, 405 RPM_RESUMING = 1, 406 RPM_SUSPENDED = 2, 407 RPM_SUSPENDING = 3 408} ; 409#line 480 410enum rpm_request { 411 RPM_REQ_NONE = 0, 412 RPM_REQ_IDLE = 1, 413 RPM_REQ_SUSPEND = 2, 414 RPM_REQ_AUTOSUSPEND = 3, 415 RPM_REQ_RESUME = 4 416} ; 417#line 488 418struct wakeup_source; 419#line 488 420struct wakeup_source; 421#line 495 "include/linux/pm.h" 422struct pm_subsys_data { 423 spinlock_t lock ; 424 unsigned int refcount ; 425}; 426#line 506 427struct dev_pm_qos_request; 428#line 506 429struct pm_qos_constraints; 430#line 506 "include/linux/pm.h" 431struct dev_pm_info { 432 pm_message_t power_state ; 433 unsigned int can_wakeup : 1 ; 434 unsigned int async_suspend : 1 ; 435 bool is_prepared : 1 ; 436 bool is_suspended : 1 ; 437 bool ignore_children : 1 ; 438 spinlock_t lock ; 439 struct list_head entry ; 440 struct completion completion ; 441 struct wakeup_source *wakeup ; 442 bool wakeup_path : 1 ; 443 struct timer_list suspend_timer ; 444 unsigned long timer_expires ; 445 struct work_struct work ; 446 wait_queue_head_t wait_queue ; 447 atomic_t usage_count ; 448 atomic_t child_count ; 449 unsigned int disable_depth : 3 ; 450 unsigned int idle_notification : 1 ; 451 unsigned int request_pending : 1 ; 452 unsigned int deferred_resume : 1 ; 453 unsigned int run_wake : 1 ; 454 unsigned int runtime_auto : 1 ; 455 unsigned int no_callbacks : 1 ; 456 unsigned int irq_safe : 1 ; 457 unsigned int use_autosuspend : 1 ; 458 unsigned int timer_autosuspends : 1 ; 459 enum rpm_request request ; 460 enum rpm_status runtime_status ; 461 int runtime_error ; 462 int autosuspend_delay ; 463 unsigned long last_busy ; 464 unsigned long active_jiffies ; 465 unsigned long suspended_jiffies ; 466 unsigned long accounting_timestamp ; 467 ktime_t suspend_time ; 468 s64 max_time_suspended_ns ; 469 struct dev_pm_qos_request *pq_req ; 470 struct pm_subsys_data *subsys_data ; 471 struct pm_qos_constraints *constraints ; 472}; 473#line 564 "include/linux/pm.h" 474struct dev_pm_domain { 475 struct dev_pm_ops ops ; 476}; 477#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h" 478struct dma_map_ops; 479#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h" 480struct dev_archdata { 481 void *acpi_handle ; 482 struct dma_map_ops *dma_ops ; 483 void *iommu ; 484}; 485#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h" 486struct pdev_archdata { 487 488}; 489#line 28 "include/linux/device.h" 490struct device; 491#line 29 492struct device_private; 493#line 29 494struct device_private; 495#line 30 496struct device_driver; 497#line 30 498struct device_driver; 499#line 31 500struct driver_private; 501#line 31 502struct driver_private; 503#line 32 504struct module; 505#line 33 506struct class; 507#line 33 508struct class; 509#line 34 510struct subsys_private; 511#line 34 512struct subsys_private; 513#line 35 514struct bus_type; 515#line 35 516struct bus_type; 517#line 36 518struct device_node; 519#line 36 520struct device_node; 521#line 37 522struct iommu_ops; 523#line 37 524struct iommu_ops; 525#line 39 "include/linux/device.h" 526struct bus_attribute { 527 struct attribute attr ; 528 ssize_t (*show)(struct bus_type *bus , char *buf ) ; 529 ssize_t (*store)(struct bus_type *bus , char const *buf , size_t count ) ; 530}; 531#line 89 532struct device_attribute; 533#line 89 534struct driver_attribute; 535#line 89 "include/linux/device.h" 536struct bus_type { 537 char const *name ; 538 char const *dev_name ; 539 struct device *dev_root ; 540 struct bus_attribute *bus_attrs ; 541 struct device_attribute *dev_attrs ; 542 struct driver_attribute *drv_attrs ; 543 int (*match)(struct device *dev , struct device_driver *drv ) ; 544 int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ; 545 int (*probe)(struct device *dev ) ; 546 int (*remove)(struct device *dev ) ; 547 void (*shutdown)(struct device *dev ) ; 548 int (*suspend)(struct device *dev , pm_message_t state ) ; 549 int (*resume)(struct device *dev ) ; 550 struct dev_pm_ops const *pm ; 551 struct iommu_ops *iommu_ops ; 552 struct subsys_private *p ; 553}; 554#line 127 555struct device_type; 556#line 214 557struct of_device_id; 558#line 214 "include/linux/device.h" 559struct device_driver { 560 char const *name ; 561 struct bus_type *bus ; 562 struct module *owner ; 563 char const *mod_name ; 564 bool suppress_bind_attrs ; 565 struct of_device_id const *of_match_table ; 566 int (*probe)(struct device *dev ) ; 567 int (*remove)(struct device *dev ) ; 568 void (*shutdown)(struct device *dev ) ; 569 int (*suspend)(struct device *dev , pm_message_t state ) ; 570 int (*resume)(struct device *dev ) ; 571 struct attribute_group const **groups ; 572 struct dev_pm_ops const *pm ; 573 struct driver_private *p ; 574}; 575#line 249 "include/linux/device.h" 576struct driver_attribute { 577 struct attribute attr ; 578 ssize_t (*show)(struct device_driver *driver , char *buf ) ; 579 ssize_t (*store)(struct device_driver *driver , char const *buf , size_t count ) ; 580}; 581#line 330 582struct class_attribute; 583#line 330 "include/linux/device.h" 584struct class { 585 char const *name ; 586 struct module *owner ; 587 struct class_attribute *class_attrs ; 588 struct device_attribute *dev_attrs ; 589 struct bin_attribute *dev_bin_attrs ; 590 struct kobject *dev_kobj ; 591 int (*dev_uevent)(struct device *dev , struct kobj_uevent_env *env ) ; 592 char *(*devnode)(struct device *dev , umode_t *mode ) ; 593 void (*class_release)(struct class *class ) ; 594 void (*dev_release)(struct device *dev ) ; 595 int (*suspend)(struct device *dev , pm_message_t state ) ; 596 int (*resume)(struct device *dev ) ; 597 struct kobj_ns_type_operations const *ns_type ; 598 void const *(*namespace)(struct device *dev ) ; 599 struct dev_pm_ops const *pm ; 600 struct subsys_private *p ; 601}; 602#line 397 "include/linux/device.h" 603struct class_attribute { 604 struct attribute attr ; 605 ssize_t (*show)(struct class *class , struct class_attribute *attr , char *buf ) ; 606 ssize_t (*store)(struct class *class , struct class_attribute *attr , char const *buf , 607 size_t count ) ; 608 void const *(*namespace)(struct class *class , struct class_attribute const *attr ) ; 609}; 610#line 465 "include/linux/device.h" 611struct device_type { 612 char const *name ; 613 struct attribute_group const **groups ; 614 int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ; 615 char *(*devnode)(struct device *dev , umode_t *mode ) ; 616 void (*release)(struct device *dev ) ; 617 struct dev_pm_ops const *pm ; 618}; 619#line 476 "include/linux/device.h" 620struct device_attribute { 621 struct attribute attr ; 622 ssize_t (*show)(struct device *dev , struct device_attribute *attr , char *buf ) ; 623 ssize_t (*store)(struct device *dev , struct device_attribute *attr , char const *buf , 624 size_t count ) ; 625}; 626#line 559 "include/linux/device.h" 627struct device_dma_parameters { 628 unsigned int max_segment_size ; 629 unsigned long segment_boundary_mask ; 630}; 631#line 627 632struct dma_coherent_mem; 633#line 627 "include/linux/device.h" 634struct device { 635 struct device *parent ; 636 struct device_private *p ; 637 struct kobject kobj ; 638 char const *init_name ; 639 struct device_type const *type ; 640 struct mutex mutex ; 641 struct bus_type *bus ; 642 struct device_driver *driver ; 643 void *platform_data ; 644 struct dev_pm_info power ; 645 struct dev_pm_domain *pm_domain ; 646 int numa_node ; 647 u64 *dma_mask ; 648 u64 coherent_dma_mask ; 649 struct device_dma_parameters *dma_parms ; 650 struct list_head dma_pools ; 651 struct dma_coherent_mem *dma_mem ; 652 struct dev_archdata archdata ; 653 struct device_node *of_node ; 654 dev_t devt ; 655 u32 id ; 656 spinlock_t devres_lock ; 657 struct list_head devres_head ; 658 struct klist_node knode_class ; 659 struct class *class ; 660 struct attribute_group const **groups ; 661 void (*release)(struct device *dev ) ; 662}; 663#line 43 "include/linux/pm_wakeup.h" 664struct wakeup_source { 665 char const *name ; 666 struct list_head entry ; 667 spinlock_t lock ; 668 struct timer_list timer ; 669 unsigned long timer_expires ; 670 ktime_t total_time ; 671 ktime_t max_time ; 672 ktime_t last_time ; 673 unsigned long event_count ; 674 unsigned long active_count ; 675 unsigned long relax_count ; 676 unsigned long hit_count ; 677 unsigned int active : 1 ; 678}; 679#line 12 "include/linux/mod_devicetable.h" 680typedef unsigned long kernel_ulong_t; 681#line 219 "include/linux/mod_devicetable.h" 682struct of_device_id { 683 char name[32] ; 684 char type[32] ; 685 char compatible[128] ; 686 void *data ; 687}; 688#line 506 "include/linux/mod_devicetable.h" 689struct platform_device_id { 690 char name[20] ; 691 kernel_ulong_t driver_data __attribute__((__aligned__(sizeof(kernel_ulong_t )))) ; 692}; 693#line 17 "include/linux/platform_device.h" 694struct mfd_cell; 695#line 17 696struct mfd_cell; 697#line 19 "include/linux/platform_device.h" 698struct platform_device { 699 char const *name ; 700 int id ; 701 struct device dev ; 702 u32 num_resources ; 703 struct resource *resource ; 704 struct platform_device_id const *id_entry ; 705 struct mfd_cell *mfd_cell ; 706 struct pdev_archdata archdata ; 707}; 708#line 164 "include/linux/platform_device.h" 709struct platform_driver { 710 int (*probe)(struct platform_device * ) ; 711 int (*remove)(struct platform_device * ) ; 712 void (*shutdown)(struct platform_device * ) ; 713 int (*suspend)(struct platform_device * , pm_message_t state ) ; 714 int (*resume)(struct platform_device * ) ; 715 struct device_driver driver ; 716 struct platform_device_id const *id_table ; 717}; 718#line 38 "include/linux/regulator/consumer.h" 719struct device; 720#line 109 721struct regulator; 722#line 109 723struct regulator; 724#line 60 "include/linux/pageblock-flags.h" 725struct page; 726#line 9 "include/linux/memory_hotplug.h" 727struct page; 728#line 103 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mpspec.h" 729struct device; 730#line 8 "include/linux/vmalloc.h" 731struct vm_area_struct; 732#line 994 "include/linux/mmzone.h" 733struct page; 734#line 10 "include/linux/gfp.h" 735struct vm_area_struct; 736#line 46 "include/linux/slub_def.h" 737struct kmem_cache_cpu { 738 void **freelist ; 739 unsigned long tid ; 740 struct page *page ; 741 struct page *partial ; 742 int node ; 743 unsigned int stat[26] ; 744}; 745#line 57 "include/linux/slub_def.h" 746struct kmem_cache_node { 747 spinlock_t list_lock ; 748 unsigned long nr_partial ; 749 struct list_head partial ; 750 atomic_long_t nr_slabs ; 751 atomic_long_t total_objects ; 752 struct list_head full ; 753}; 754#line 73 "include/linux/slub_def.h" 755struct kmem_cache_order_objects { 756 unsigned long x ; 757}; 758#line 80 "include/linux/slub_def.h" 759struct kmem_cache { 760 struct kmem_cache_cpu *cpu_slab ; 761 unsigned long flags ; 762 unsigned long min_partial ; 763 int size ; 764 int objsize ; 765 int offset ; 766 int cpu_partial ; 767 struct kmem_cache_order_objects oo ; 768 struct kmem_cache_order_objects max ; 769 struct kmem_cache_order_objects min ; 770 gfp_t allocflags ; 771 int refcount ; 772 void (*ctor)(void * ) ; 773 int inuse ; 774 int align ; 775 int reserved ; 776 char const *name ; 777 struct list_head list ; 778 struct kobject kobj ; 779 int remote_node_defrag_ratio ; 780 struct kmem_cache_node *node[1 << 10] ; 781}; 782#line 29 "include/linux/sysctl.h" 783struct completion; 784#line 49 "include/linux/kmod.h" 785struct file; 786#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h" 787struct task_struct; 788#line 18 "include/linux/elf.h" 789typedef __u64 Elf64_Addr; 790#line 19 "include/linux/elf.h" 791typedef __u16 Elf64_Half; 792#line 23 "include/linux/elf.h" 793typedef __u32 Elf64_Word; 794#line 24 "include/linux/elf.h" 795typedef __u64 Elf64_Xword; 796#line 194 "include/linux/elf.h" 797struct elf64_sym { 798 Elf64_Word st_name ; 799 unsigned char st_info ; 800 unsigned char st_other ; 801 Elf64_Half st_shndx ; 802 Elf64_Addr st_value ; 803 Elf64_Xword st_size ; 804}; 805#line 194 "include/linux/elf.h" 806typedef struct elf64_sym Elf64_Sym; 807#line 438 808struct file; 809#line 39 "include/linux/moduleparam.h" 810struct kernel_param; 811#line 39 812struct kernel_param; 813#line 41 "include/linux/moduleparam.h" 814struct kernel_param_ops { 815 int (*set)(char const *val , struct kernel_param const *kp ) ; 816 int (*get)(char *buffer , struct kernel_param const *kp ) ; 817 void (*free)(void *arg ) ; 818}; 819#line 50 820struct kparam_string; 821#line 50 822struct kparam_array; 823#line 50 "include/linux/moduleparam.h" 824union __anonunion____missing_field_name_200 { 825 void *arg ; 826 struct kparam_string const *str ; 827 struct kparam_array const *arr ; 828}; 829#line 50 "include/linux/moduleparam.h" 830struct kernel_param { 831 char const *name ; 832 struct kernel_param_ops const *ops ; 833 u16 perm ; 834 s16 level ; 835 union __anonunion____missing_field_name_200 __annonCompField32 ; 836}; 837#line 63 "include/linux/moduleparam.h" 838struct kparam_string { 839 unsigned int maxlen ; 840 char *string ; 841}; 842#line 69 "include/linux/moduleparam.h" 843struct kparam_array { 844 unsigned int max ; 845 unsigned int elemsize ; 846 unsigned int *num ; 847 struct kernel_param_ops const *ops ; 848 void *elem ; 849}; 850#line 445 851struct module; 852#line 80 "include/linux/jump_label.h" 853struct module; 854#line 143 "include/linux/jump_label.h" 855struct static_key { 856 atomic_t enabled ; 857}; 858#line 22 "include/linux/tracepoint.h" 859struct module; 860#line 23 861struct tracepoint; 862#line 23 863struct tracepoint; 864#line 25 "include/linux/tracepoint.h" 865struct tracepoint_func { 866 void *func ; 867 void *data ; 868}; 869#line 30 "include/linux/tracepoint.h" 870struct tracepoint { 871 char const *name ; 872 struct static_key key ; 873 void (*regfunc)(void) ; 874 void (*unregfunc)(void) ; 875 struct tracepoint_func *funcs ; 876}; 877#line 19 "include/linux/export.h" 878struct kernel_symbol { 879 unsigned long value ; 880 char const *name ; 881}; 882#line 8 "include/asm-generic/module.h" 883struct mod_arch_specific { 884 885}; 886#line 35 "include/linux/module.h" 887struct module; 888#line 37 889struct module_param_attrs; 890#line 37 "include/linux/module.h" 891struct module_kobject { 892 struct kobject kobj ; 893 struct module *mod ; 894 struct kobject *drivers_dir ; 895 struct module_param_attrs *mp ; 896}; 897#line 44 "include/linux/module.h" 898struct module_attribute { 899 struct attribute attr ; 900 ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ; 901 ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const * , 902 size_t count ) ; 903 void (*setup)(struct module * , char const * ) ; 904 int (*test)(struct module * ) ; 905 void (*free)(struct module * ) ; 906}; 907#line 71 908struct exception_table_entry; 909#line 71 910struct exception_table_entry; 911#line 199 912enum module_state { 913 MODULE_STATE_LIVE = 0, 914 MODULE_STATE_COMING = 1, 915 MODULE_STATE_GOING = 2 916} ; 917#line 215 "include/linux/module.h" 918struct module_ref { 919 unsigned long incs ; 920 unsigned long decs ; 921} __attribute__((__aligned__((2) * (sizeof(unsigned long )) ))) ; 922#line 220 923struct module_sect_attrs; 924#line 220 925struct module_notes_attrs; 926#line 220 927struct ftrace_event_call; 928#line 220 "include/linux/module.h" 929struct module { 930 enum module_state state ; 931 struct list_head list ; 932 char name[64UL - sizeof(unsigned long )] ; 933 struct module_kobject mkobj ; 934 struct module_attribute *modinfo_attrs ; 935 char const *version ; 936 char const *srcversion ; 937 struct kobject *holders_dir ; 938 struct kernel_symbol const *syms ; 939 unsigned long const *crcs ; 940 unsigned int num_syms ; 941 struct kernel_param *kp ; 942 unsigned int num_kp ; 943 unsigned int num_gpl_syms ; 944 struct kernel_symbol const *gpl_syms ; 945 unsigned long const *gpl_crcs ; 946 struct kernel_symbol const *unused_syms ; 947 unsigned long const *unused_crcs ; 948 unsigned int num_unused_syms ; 949 unsigned int num_unused_gpl_syms ; 950 struct kernel_symbol const *unused_gpl_syms ; 951 unsigned long const *unused_gpl_crcs ; 952 struct kernel_symbol const *gpl_future_syms ; 953 unsigned long const *gpl_future_crcs ; 954 unsigned int num_gpl_future_syms ; 955 unsigned int num_exentries ; 956 struct exception_table_entry *extable ; 957 int (*init)(void) ; 958 void *module_init ; 959 void *module_core ; 960 unsigned int init_size ; 961 unsigned int core_size ; 962 unsigned int init_text_size ; 963 unsigned int core_text_size ; 964 unsigned int init_ro_size ; 965 unsigned int core_ro_size ; 966 struct mod_arch_specific arch ; 967 unsigned int taints ; 968 unsigned int num_bugs ; 969 struct list_head bug_list ; 970 struct bug_entry *bug_table ; 971 Elf64_Sym *symtab ; 972 Elf64_Sym *core_symtab ; 973 unsigned int num_symtab ; 974 unsigned int core_num_syms ; 975 char *strtab ; 976 char *core_strtab ; 977 struct module_sect_attrs *sect_attrs ; 978 struct module_notes_attrs *notes_attrs ; 979 char *args ; 980 void *percpu ; 981 unsigned int percpu_size ; 982 unsigned int num_tracepoints ; 983 struct tracepoint * const *tracepoints_ptrs ; 984 unsigned int num_trace_bprintk_fmt ; 985 char const **trace_bprintk_fmt_start ; 986 struct ftrace_event_call **trace_events ; 987 unsigned int num_trace_events ; 988 struct list_head source_list ; 989 struct list_head target_list ; 990 struct task_struct *waiter ; 991 void (*exit)(void) ; 992 struct module_ref *refptr ; 993 ctor_fn_t *ctors ; 994 unsigned int num_ctors ; 995}; 996#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 997struct virtual_consumer_data { 998 struct mutex lock ; 999 struct regulator *regulator ; 1000 bool enabled ; 1001 int min_uV ; 1002 int max_uV ; 1003 int min_uA ; 1004 int max_uA ; 1005 unsigned int mode ; 1006}; 1007#line 1 "<compiler builtins>" 1008long __builtin_expect(long val , long res ) ; 1009#line 27 "include/linux/err.h" 1010__inline static long __attribute__((__warn_unused_result__)) PTR_ERR(void const *ptr ) __attribute__((__no_instrument_function__)) ; 1011#line 27 "include/linux/err.h" 1012__inline static long __attribute__((__warn_unused_result__)) PTR_ERR(void const *ptr ) 1013{ 1014 1015 { 1016#line 29 1017 return ((long )ptr); 1018} 1019} 1020#line 32 1021__inline static long __attribute__((__warn_unused_result__)) IS_ERR(void const *ptr ) __attribute__((__no_instrument_function__)) ; 1022#line 32 "include/linux/err.h" 1023__inline static long __attribute__((__warn_unused_result__)) IS_ERR(void const *ptr ) 1024{ long tmp ; 1025 unsigned long __cil_tmp3 ; 1026 int __cil_tmp4 ; 1027 int __cil_tmp5 ; 1028 int __cil_tmp6 ; 1029 long __cil_tmp7 ; 1030 1031 { 1032 { 1033#line 34 1034 __cil_tmp3 = (unsigned long )ptr; 1035#line 34 1036 __cil_tmp4 = __cil_tmp3 >= 0xfffffffffffff001UL; 1037#line 34 1038 __cil_tmp5 = ! __cil_tmp4; 1039#line 34 1040 __cil_tmp6 = ! __cil_tmp5; 1041#line 34 1042 __cil_tmp7 = (long )__cil_tmp6; 1043#line 34 1044 tmp = __builtin_expect(__cil_tmp7, 0L); 1045 } 1046#line 34 1047 return (tmp); 1048} 1049} 1050#line 49 "include/linux/dynamic_debug.h" 1051extern int ( /* format attribute */ __dynamic_dev_dbg)(struct _ddebug *descriptor , 1052 struct device const *dev , 1053 char const *fmt , ...) ; 1054#line 216 "include/linux/kernel.h" 1055extern int __attribute__((__warn_unused_result__)) _kstrtol(char const *s , unsigned int base , 1056 long *res ) ; 1057#line 219 1058extern int __attribute__((__warn_unused_result__)) kstrtoll(char const *s , unsigned int base , 1059 long long *res ) ; 1060#line 233 1061__inline static int __attribute__((__warn_unused_result__)) kstrtol(char const *s , 1062 unsigned int base , 1063 long *res ) __attribute__((__no_instrument_function__)) ; 1064#line 233 "include/linux/kernel.h" 1065__inline static int __attribute__((__warn_unused_result__)) kstrtol(char const *s , 1066 unsigned int base , 1067 long *res ) 1068{ int tmp ; 1069 int tmp___0 ; 1070 long long *__cil_tmp6 ; 1071 1072 { 1073#line 239 1074 if (8UL == 8UL) { 1075#line 239 1076 if (8UL == 8UL) { 1077 { 1078#line 241 1079 __cil_tmp6 = (long long *)res; 1080#line 241 1081 tmp = (int )kstrtoll(s, base, __cil_tmp6); 1082 } 1083#line 241 1084 return (tmp); 1085 } else { 1086 { 1087#line 243 1088 tmp___0 = (int )_kstrtol(s, base, res); 1089 } 1090#line 243 1091 return (tmp___0); 1092 } 1093 } else { 1094 { 1095#line 243 1096 tmp___0 = (int )_kstrtol(s, base, res); 1097 } 1098#line 243 1099 return (tmp___0); 1100 } 1101} 1102} 1103#line 320 1104extern int ( /* format attribute */ sprintf)(char *buf , char const *fmt , ...) ; 1105#line 126 "include/linux/string.h" 1106extern bool sysfs_streq(char const *s1 , char const *s2 ) ; 1107#line 115 "include/linux/mutex.h" 1108extern void __mutex_init(struct mutex *lock , char const *name , struct lock_class_key *key ) ; 1109#line 152 1110void mutex_lock(struct mutex *lock ) ; 1111#line 153 1112int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock ) ; 1113#line 154 1114int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock ) ; 1115#line 168 1116int mutex_trylock(struct mutex *lock ) ; 1117#line 169 1118void mutex_unlock(struct mutex *lock ) ; 1119#line 170 1120int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ; 1121#line 158 "include/linux/sysfs.h" 1122extern int __attribute__((__warn_unused_result__)) sysfs_create_group(struct kobject *kobj , 1123 struct attribute_group const *grp ) ; 1124#line 162 1125extern void sysfs_remove_group(struct kobject *kobj , struct attribute_group const *grp ) ; 1126#line 792 "include/linux/device.h" 1127extern void *dev_get_drvdata(struct device const *dev ) ; 1128#line 793 1129extern int dev_set_drvdata(struct device *dev , void *data ) ; 1130#line 891 1131extern int ( /* format attribute */ dev_err)(struct device const *dev , char const *fmt 1132 , ...) ; 1133#line 174 "include/linux/platform_device.h" 1134extern int platform_driver_register(struct platform_driver * ) ; 1135#line 175 1136extern void platform_driver_unregister(struct platform_driver * ) ; 1137#line 183 1138__inline static void *platform_get_drvdata(struct platform_device const *pdev ) __attribute__((__no_instrument_function__)) ; 1139#line 183 "include/linux/platform_device.h" 1140__inline static void *platform_get_drvdata(struct platform_device const *pdev ) 1141{ void *tmp ; 1142 unsigned long __cil_tmp3 ; 1143 unsigned long __cil_tmp4 ; 1144 struct device const *__cil_tmp5 ; 1145 1146 { 1147 { 1148#line 185 1149 __cil_tmp3 = (unsigned long )pdev; 1150#line 185 1151 __cil_tmp4 = __cil_tmp3 + 16; 1152#line 185 1153 __cil_tmp5 = (struct device const *)__cil_tmp4; 1154#line 185 1155 tmp = dev_get_drvdata(__cil_tmp5); 1156 } 1157#line 185 1158 return (tmp); 1159} 1160} 1161#line 188 1162__inline static void platform_set_drvdata(struct platform_device *pdev , void *data ) __attribute__((__no_instrument_function__)) ; 1163#line 188 "include/linux/platform_device.h" 1164__inline static void platform_set_drvdata(struct platform_device *pdev , void *data ) 1165{ unsigned long __cil_tmp3 ; 1166 unsigned long __cil_tmp4 ; 1167 struct device *__cil_tmp5 ; 1168 1169 { 1170 { 1171#line 190 1172 __cil_tmp3 = (unsigned long )pdev; 1173#line 190 1174 __cil_tmp4 = __cil_tmp3 + 16; 1175#line 190 1176 __cil_tmp5 = (struct device *)__cil_tmp4; 1177#line 190 1178 dev_set_drvdata(__cil_tmp5, data); 1179 } 1180#line 191 1181 return; 1182} 1183} 1184#line 134 "include/linux/regulator/consumer.h" 1185extern struct regulator * __attribute__((__warn_unused_result__)) regulator_get(struct device *dev , 1186 char const *id ) ; 1187#line 140 1188extern void regulator_put(struct regulator *regulator ) ; 1189#line 144 1190extern int regulator_enable(struct regulator *regulator ) ; 1191#line 145 1192extern int regulator_disable(struct regulator *regulator ) ; 1193#line 167 1194extern int regulator_set_voltage(struct regulator *regulator , int min_uV , int max_uV ) ; 1195#line 172 1196extern int regulator_set_current_limit(struct regulator *regulator , int min_uA , 1197 int max_uA ) ; 1198#line 176 1199extern int regulator_set_mode(struct regulator *regulator , unsigned int mode ) ; 1200#line 177 1201extern unsigned int regulator_get_mode(struct regulator *regulator ) ; 1202#line 161 "include/linux/slab.h" 1203extern void kfree(void const * ) ; 1204#line 221 "include/linux/slub_def.h" 1205extern void *__kmalloc(size_t size , gfp_t flags ) ; 1206#line 268 1207__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size , 1208 gfp_t flags ) __attribute__((__no_instrument_function__)) ; 1209#line 268 "include/linux/slub_def.h" 1210__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size , 1211 gfp_t flags ) 1212{ void *tmp___2 ; 1213 1214 { 1215 { 1216#line 283 1217 tmp___2 = __kmalloc(size, flags); 1218 } 1219#line 283 1220 return (tmp___2); 1221} 1222} 1223#line 349 "include/linux/slab.h" 1224__inline static void *kzalloc(size_t size , gfp_t flags ) __attribute__((__no_instrument_function__)) ; 1225#line 349 "include/linux/slab.h" 1226__inline static void *kzalloc(size_t size , gfp_t flags ) 1227{ void *tmp ; 1228 unsigned int __cil_tmp4 ; 1229 1230 { 1231 { 1232#line 351 1233 __cil_tmp4 = flags | 32768U; 1234#line 351 1235 tmp = kmalloc(size, __cil_tmp4); 1236 } 1237#line 351 1238 return (tmp); 1239} 1240} 1241#line 26 "include/linux/export.h" 1242extern struct module __this_module ; 1243#line 67 "include/linux/module.h" 1244int init_module(void) ; 1245#line 68 1246void cleanup_module(void) ; 1247#line 40 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 1248static void update_voltage_constraints(struct device *dev , struct virtual_consumer_data *data ) ; 1249#line 40 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 1250static struct _ddebug __attribute__((__aligned__(8))) descriptor __attribute__((__used__, 1251__section__("__verbose"))) = {"virtual", "update_voltage_constraints", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c", 1252 "Requesting %d-%duV\n", 41U, 1U}; 1253#line 52 1254static void update_voltage_constraints(struct device *dev , struct virtual_consumer_data *data ) ; 1255#line 52 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 1256static struct _ddebug __attribute__((__aligned__(8))) descriptor___0 __attribute__((__used__, 1257__section__("__verbose"))) = {"virtual", "update_voltage_constraints", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c", 1258 "Enabling regulator\n", 52U, 1U}; 1259#line 62 1260static void update_voltage_constraints(struct device *dev , struct virtual_consumer_data *data ) ; 1261#line 62 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 1262static struct _ddebug __attribute__((__aligned__(8))) descriptor___1 __attribute__((__used__, 1263__section__("__verbose"))) = {"virtual", "update_voltage_constraints", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c", 1264 "Disabling regulator\n", 62U, 1U}; 1265#line 33 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 1266static void update_voltage_constraints(struct device *dev , struct virtual_consumer_data *data ) 1267{ int ret ; 1268 long tmp ; 1269 long tmp___0 ; 1270 long tmp___1 ; 1271 unsigned long __cil_tmp7 ; 1272 unsigned long __cil_tmp8 ; 1273 unsigned long __cil_tmp9 ; 1274 unsigned long __cil_tmp10 ; 1275 unsigned long __cil_tmp11 ; 1276 unsigned long __cil_tmp12 ; 1277 int __cil_tmp13 ; 1278 unsigned long __cil_tmp14 ; 1279 unsigned long __cil_tmp15 ; 1280 int __cil_tmp16 ; 1281 struct _ddebug __attribute__((__aligned__(8))) *__cil_tmp17 ; 1282 unsigned int __cil_tmp18 ; 1283 unsigned int __cil_tmp19 ; 1284 int __cil_tmp20 ; 1285 int __cil_tmp21 ; 1286 long __cil_tmp22 ; 1287 struct device const *__cil_tmp23 ; 1288 unsigned long __cil_tmp24 ; 1289 unsigned long __cil_tmp25 ; 1290 int __cil_tmp26 ; 1291 unsigned long __cil_tmp27 ; 1292 unsigned long __cil_tmp28 ; 1293 int __cil_tmp29 ; 1294 unsigned long __cil_tmp30 ; 1295 unsigned long __cil_tmp31 ; 1296 struct regulator *__cil_tmp32 ; 1297 unsigned long __cil_tmp33 ; 1298 unsigned long __cil_tmp34 ; 1299 int __cil_tmp35 ; 1300 unsigned long __cil_tmp36 ; 1301 unsigned long __cil_tmp37 ; 1302 int __cil_tmp38 ; 1303 struct device const *__cil_tmp39 ; 1304 unsigned long __cil_tmp40 ; 1305 unsigned long __cil_tmp41 ; 1306 unsigned long __cil_tmp42 ; 1307 unsigned long __cil_tmp43 ; 1308 unsigned long __cil_tmp44 ; 1309 unsigned long __cil_tmp45 ; 1310 bool __cil_tmp46 ; 1311 struct _ddebug __attribute__((__aligned__(8))) *__cil_tmp47 ; 1312 unsigned int __cil_tmp48 ; 1313 unsigned int __cil_tmp49 ; 1314 int __cil_tmp50 ; 1315 int __cil_tmp51 ; 1316 long __cil_tmp52 ; 1317 struct device const *__cil_tmp53 ; 1318 unsigned long __cil_tmp54 ; 1319 unsigned long __cil_tmp55 ; 1320 struct regulator *__cil_tmp56 ; 1321 unsigned long __cil_tmp57 ; 1322 unsigned long __cil_tmp58 ; 1323 struct device const *__cil_tmp59 ; 1324 unsigned long __cil_tmp60 ; 1325 unsigned long __cil_tmp61 ; 1326 unsigned long __cil_tmp62 ; 1327 unsigned long __cil_tmp63 ; 1328 unsigned long __cil_tmp64 ; 1329 unsigned long __cil_tmp65 ; 1330 struct _ddebug __attribute__((__aligned__(8))) *__cil_tmp66 ; 1331 unsigned int __cil_tmp67 ; 1332 unsigned int __cil_tmp68 ; 1333 int __cil_tmp69 ; 1334 int __cil_tmp70 ; 1335 long __cil_tmp71 ; 1336 struct device const *__cil_tmp72 ; 1337 unsigned long __cil_tmp73 ; 1338 unsigned long __cil_tmp74 ; 1339 struct regulator *__cil_tmp75 ; 1340 unsigned long __cil_tmp76 ; 1341 unsigned long __cil_tmp77 ; 1342 struct device const *__cil_tmp78 ; 1343 1344 { 1345 { 1346#line 38 1347 __cil_tmp7 = (unsigned long )data; 1348#line 38 1349 __cil_tmp8 = __cil_tmp7 + 84; 1350#line 38 1351 if (*((int *)__cil_tmp8)) { 1352 { 1353#line 38 1354 __cil_tmp9 = (unsigned long )data; 1355#line 38 1356 __cil_tmp10 = __cil_tmp9 + 88; 1357#line 38 1358 if (*((int *)__cil_tmp10)) { 1359 { 1360#line 38 1361 __cil_tmp11 = (unsigned long )data; 1362#line 38 1363 __cil_tmp12 = __cil_tmp11 + 88; 1364#line 38 1365 __cil_tmp13 = *((int *)__cil_tmp12); 1366#line 38 1367 __cil_tmp14 = (unsigned long )data; 1368#line 38 1369 __cil_tmp15 = __cil_tmp14 + 84; 1370#line 38 1371 __cil_tmp16 = *((int *)__cil_tmp15); 1372#line 38 1373 if (__cil_tmp16 <= __cil_tmp13) { 1374 { 1375#line 40 1376 while (1) { 1377 while_continue: /* CIL Label */ ; 1378 { 1379#line 40 1380 while (1) { 1381 while_continue___0: /* CIL Label */ ; 1382 { 1383#line 40 1384 __cil_tmp17 = & descriptor; 1385#line 40 1386 __cil_tmp18 = __cil_tmp17->flags; 1387#line 40 1388 __cil_tmp19 = __cil_tmp18 & 1U; 1389#line 40 1390 __cil_tmp20 = ! __cil_tmp19; 1391#line 40 1392 __cil_tmp21 = ! __cil_tmp20; 1393#line 40 1394 __cil_tmp22 = (long )__cil_tmp21; 1395#line 40 1396 tmp = __builtin_expect(__cil_tmp22, 0L); 1397 } 1398#line 40 1399 if (tmp) { 1400 { 1401#line 40 1402 __cil_tmp23 = (struct device const *)dev; 1403#line 40 1404 __cil_tmp24 = (unsigned long )data; 1405#line 40 1406 __cil_tmp25 = __cil_tmp24 + 84; 1407#line 40 1408 __cil_tmp26 = *((int *)__cil_tmp25); 1409#line 40 1410 __cil_tmp27 = (unsigned long )data; 1411#line 40 1412 __cil_tmp28 = __cil_tmp27 + 88; 1413#line 40 1414 __cil_tmp29 = *((int *)__cil_tmp28); 1415#line 40 1416 __dynamic_dev_dbg(& descriptor, __cil_tmp23, "Requesting %d-%duV\n", 1417 __cil_tmp26, __cil_tmp29); 1418 } 1419 } else { 1420 1421 } 1422#line 40 1423 goto while_break___0; 1424 } 1425 while_break___0: /* CIL Label */ ; 1426 } 1427#line 40 1428 goto while_break; 1429 } 1430 while_break: /* CIL Label */ ; 1431 } 1432 { 1433#line 42 1434 __cil_tmp30 = (unsigned long )data; 1435#line 42 1436 __cil_tmp31 = __cil_tmp30 + 72; 1437#line 42 1438 __cil_tmp32 = *((struct regulator **)__cil_tmp31); 1439#line 42 1440 __cil_tmp33 = (unsigned long )data; 1441#line 42 1442 __cil_tmp34 = __cil_tmp33 + 84; 1443#line 42 1444 __cil_tmp35 = *((int *)__cil_tmp34); 1445#line 42 1446 __cil_tmp36 = (unsigned long )data; 1447#line 42 1448 __cil_tmp37 = __cil_tmp36 + 88; 1449#line 42 1450 __cil_tmp38 = *((int *)__cil_tmp37); 1451#line 42 1452 ret = regulator_set_voltage(__cil_tmp32, __cil_tmp35, __cil_tmp38); 1453 } 1454#line 44 1455 if (ret != 0) { 1456 { 1457#line 45 1458 __cil_tmp39 = (struct device const *)dev; 1459#line 45 1460 dev_err(__cil_tmp39, "regulator_set_voltage() failed: %d\n", ret); 1461 } 1462#line 47 1463 return; 1464 } else { 1465 1466 } 1467 } else { 1468 1469 } 1470 } 1471 } else { 1472 1473 } 1474 } 1475 } else { 1476 1477 } 1478 } 1479 { 1480#line 51 1481 __cil_tmp40 = (unsigned long )data; 1482#line 51 1483 __cil_tmp41 = __cil_tmp40 + 84; 1484#line 51 1485 if (*((int *)__cil_tmp41)) { 1486 { 1487#line 51 1488 __cil_tmp42 = (unsigned long )data; 1489#line 51 1490 __cil_tmp43 = __cil_tmp42 + 88; 1491#line 51 1492 if (*((int *)__cil_tmp43)) { 1493 { 1494#line 51 1495 __cil_tmp44 = (unsigned long )data; 1496#line 51 1497 __cil_tmp45 = __cil_tmp44 + 80; 1498#line 51 1499 __cil_tmp46 = *((bool *)__cil_tmp45); 1500#line 51 1501 if (! __cil_tmp46) { 1502 { 1503#line 52 1504 while (1) { 1505 while_continue___1: /* CIL Label */ ; 1506 { 1507#line 52 1508 while (1) { 1509 while_continue___2: /* CIL Label */ ; 1510 { 1511#line 52 1512 __cil_tmp47 = & descriptor___0; 1513#line 52 1514 __cil_tmp48 = __cil_tmp47->flags; 1515#line 52 1516 __cil_tmp49 = __cil_tmp48 & 1U; 1517#line 52 1518 __cil_tmp50 = ! __cil_tmp49; 1519#line 52 1520 __cil_tmp51 = ! __cil_tmp50; 1521#line 52 1522 __cil_tmp52 = (long )__cil_tmp51; 1523#line 52 1524 tmp___0 = __builtin_expect(__cil_tmp52, 0L); 1525 } 1526#line 52 1527 if (tmp___0) { 1528 { 1529#line 52 1530 __cil_tmp53 = (struct device const *)dev; 1531#line 52 1532 __dynamic_dev_dbg(& descriptor___0, __cil_tmp53, "Enabling regulator\n"); 1533 } 1534 } else { 1535 1536 } 1537#line 52 1538 goto while_break___2; 1539 } 1540 while_break___2: /* CIL Label */ ; 1541 } 1542#line 52 1543 goto while_break___1; 1544 } 1545 while_break___1: /* CIL Label */ ; 1546 } 1547 { 1548#line 53 1549 __cil_tmp54 = (unsigned long )data; 1550#line 53 1551 __cil_tmp55 = __cil_tmp54 + 72; 1552#line 53 1553 __cil_tmp56 = *((struct regulator **)__cil_tmp55); 1554#line 53 1555 ret = regulator_enable(__cil_tmp56); 1556 } 1557#line 54 1558 if (ret == 0) { 1559#line 55 1560 __cil_tmp57 = (unsigned long )data; 1561#line 55 1562 __cil_tmp58 = __cil_tmp57 + 80; 1563#line 55 1564 *((bool *)__cil_tmp58) = (bool )1; 1565 } else { 1566 { 1567#line 57 1568 __cil_tmp59 = (struct device const *)dev; 1569#line 57 1570 dev_err(__cil_tmp59, "regulator_enable() failed: %d\n", ret); 1571 } 1572 } 1573 } else { 1574 1575 } 1576 } 1577 } else { 1578 1579 } 1580 } 1581 } else { 1582 1583 } 1584 } 1585 { 1586#line 61 1587 __cil_tmp60 = (unsigned long )data; 1588#line 61 1589 __cil_tmp61 = __cil_tmp60 + 84; 1590#line 61 1591 if (*((int *)__cil_tmp61)) { 1592 { 1593#line 61 1594 __cil_tmp62 = (unsigned long )data; 1595#line 61 1596 __cil_tmp63 = __cil_tmp62 + 88; 1597#line 61 1598 if (*((int *)__cil_tmp63)) { 1599 1600 } else { 1601#line 61 1602 goto _L; 1603 } 1604 } 1605 } else { 1606 _L: /* CIL Label */ 1607 { 1608#line 61 1609 __cil_tmp64 = (unsigned long )data; 1610#line 61 1611 __cil_tmp65 = __cil_tmp64 + 80; 1612#line 61 1613 if (*((bool *)__cil_tmp65)) { 1614 { 1615#line 62 1616 while (1) { 1617 while_continue___3: /* CIL Label */ ; 1618 { 1619#line 62 1620 while (1) { 1621 while_continue___4: /* CIL Label */ ; 1622 { 1623#line 62 1624 __cil_tmp66 = & descriptor___1; 1625#line 62 1626 __cil_tmp67 = __cil_tmp66->flags; 1627#line 62 1628 __cil_tmp68 = __cil_tmp67 & 1U; 1629#line 62 1630 __cil_tmp69 = ! __cil_tmp68; 1631#line 62 1632 __cil_tmp70 = ! __cil_tmp69; 1633#line 62 1634 __cil_tmp71 = (long )__cil_tmp70; 1635#line 62 1636 tmp___1 = __builtin_expect(__cil_tmp71, 0L); 1637 } 1638#line 62 1639 if (tmp___1) { 1640 { 1641#line 62 1642 __cil_tmp72 = (struct device const *)dev; 1643#line 62 1644 __dynamic_dev_dbg(& descriptor___1, __cil_tmp72, "Disabling regulator\n"); 1645 } 1646 } else { 1647 1648 } 1649#line 62 1650 goto while_break___4; 1651 } 1652 while_break___4: /* CIL Label */ ; 1653 } 1654#line 62 1655 goto while_break___3; 1656 } 1657 while_break___3: /* CIL Label */ ; 1658 } 1659 { 1660#line 63 1661 __cil_tmp73 = (unsigned long )data; 1662#line 63 1663 __cil_tmp74 = __cil_tmp73 + 72; 1664#line 63 1665 __cil_tmp75 = *((struct regulator **)__cil_tmp74); 1666#line 63 1667 ret = regulator_disable(__cil_tmp75); 1668 } 1669#line 64 1670 if (ret == 0) { 1671#line 65 1672 __cil_tmp76 = (unsigned long )data; 1673#line 65 1674 __cil_tmp77 = __cil_tmp76 + 80; 1675#line 65 1676 *((bool *)__cil_tmp77) = (bool )0; 1677 } else { 1678 { 1679#line 67 1680 __cil_tmp78 = (struct device const *)dev; 1681#line 67 1682 dev_err(__cil_tmp78, "regulator_disable() failed: %d\n", ret); 1683 } 1684 } 1685 } else { 1686 1687 } 1688 } 1689 } 1690 } 1691#line 70 1692 return; 1693} 1694} 1695#line 79 1696static void update_current_limit_constraints(struct device *dev , struct virtual_consumer_data *data ) ; 1697#line 79 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 1698static struct _ddebug __attribute__((__aligned__(8))) descriptor___2 __attribute__((__used__, 1699__section__("__verbose"))) = {"virtual", "update_current_limit_constraints", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c", 1700 "Requesting %d-%duA\n", 80U, 1U}; 1701#line 92 1702static void update_current_limit_constraints(struct device *dev , struct virtual_consumer_data *data ) ; 1703#line 92 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 1704static struct _ddebug __attribute__((__aligned__(8))) descriptor___3 __attribute__((__used__, 1705__section__("__verbose"))) = {"virtual", "update_current_limit_constraints", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c", 1706 "Enabling regulator\n", 92U, 1U}; 1707#line 102 1708static void update_current_limit_constraints(struct device *dev , struct virtual_consumer_data *data ) ; 1709#line 102 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 1710static struct _ddebug __attribute__((__aligned__(8))) descriptor___4 __attribute__((__used__, 1711__section__("__verbose"))) = {"virtual", "update_current_limit_constraints", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c", 1712 "Disabling regulator\n", 102U, 1U}; 1713#line 72 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 1714static void update_current_limit_constraints(struct device *dev , struct virtual_consumer_data *data ) 1715{ int ret ; 1716 long tmp ; 1717 long tmp___0 ; 1718 long tmp___1 ; 1719 unsigned long __cil_tmp7 ; 1720 unsigned long __cil_tmp8 ; 1721 unsigned long __cil_tmp9 ; 1722 unsigned long __cil_tmp10 ; 1723 int __cil_tmp11 ; 1724 unsigned long __cil_tmp12 ; 1725 unsigned long __cil_tmp13 ; 1726 int __cil_tmp14 ; 1727 struct _ddebug __attribute__((__aligned__(8))) *__cil_tmp15 ; 1728 unsigned int __cil_tmp16 ; 1729 unsigned int __cil_tmp17 ; 1730 int __cil_tmp18 ; 1731 int __cil_tmp19 ; 1732 long __cil_tmp20 ; 1733 struct device const *__cil_tmp21 ; 1734 unsigned long __cil_tmp22 ; 1735 unsigned long __cil_tmp23 ; 1736 int __cil_tmp24 ; 1737 unsigned long __cil_tmp25 ; 1738 unsigned long __cil_tmp26 ; 1739 int __cil_tmp27 ; 1740 unsigned long __cil_tmp28 ; 1741 unsigned long __cil_tmp29 ; 1742 struct regulator *__cil_tmp30 ; 1743 unsigned long __cil_tmp31 ; 1744 unsigned long __cil_tmp32 ; 1745 int __cil_tmp33 ; 1746 unsigned long __cil_tmp34 ; 1747 unsigned long __cil_tmp35 ; 1748 int __cil_tmp36 ; 1749 struct device const *__cil_tmp37 ; 1750 unsigned long __cil_tmp38 ; 1751 unsigned long __cil_tmp39 ; 1752 unsigned long __cil_tmp40 ; 1753 unsigned long __cil_tmp41 ; 1754 bool __cil_tmp42 ; 1755 struct _ddebug __attribute__((__aligned__(8))) *__cil_tmp43 ; 1756 unsigned int __cil_tmp44 ; 1757 unsigned int __cil_tmp45 ; 1758 int __cil_tmp46 ; 1759 int __cil_tmp47 ; 1760 long __cil_tmp48 ; 1761 struct device const *__cil_tmp49 ; 1762 unsigned long __cil_tmp50 ; 1763 unsigned long __cil_tmp51 ; 1764 struct regulator *__cil_tmp52 ; 1765 unsigned long __cil_tmp53 ; 1766 unsigned long __cil_tmp54 ; 1767 struct device const *__cil_tmp55 ; 1768 unsigned long __cil_tmp56 ; 1769 unsigned long __cil_tmp57 ; 1770 unsigned long __cil_tmp58 ; 1771 unsigned long __cil_tmp59 ; 1772 unsigned long __cil_tmp60 ; 1773 unsigned long __cil_tmp61 ; 1774 struct _ddebug __attribute__((__aligned__(8))) *__cil_tmp62 ; 1775 unsigned int __cil_tmp63 ; 1776 unsigned int __cil_tmp64 ; 1777 int __cil_tmp65 ; 1778 int __cil_tmp66 ; 1779 long __cil_tmp67 ; 1780 struct device const *__cil_tmp68 ; 1781 unsigned long __cil_tmp69 ; 1782 unsigned long __cil_tmp70 ; 1783 struct regulator *__cil_tmp71 ; 1784 unsigned long __cil_tmp72 ; 1785 unsigned long __cil_tmp73 ; 1786 struct device const *__cil_tmp74 ; 1787 1788 { 1789 { 1790#line 77 1791 __cil_tmp7 = (unsigned long )data; 1792#line 77 1793 __cil_tmp8 = __cil_tmp7 + 96; 1794#line 77 1795 if (*((int *)__cil_tmp8)) { 1796 { 1797#line 77 1798 __cil_tmp9 = (unsigned long )data; 1799#line 77 1800 __cil_tmp10 = __cil_tmp9 + 96; 1801#line 77 1802 __cil_tmp11 = *((int *)__cil_tmp10); 1803#line 77 1804 __cil_tmp12 = (unsigned long )data; 1805#line 77 1806 __cil_tmp13 = __cil_tmp12 + 92; 1807#line 77 1808 __cil_tmp14 = *((int *)__cil_tmp13); 1809#line 77 1810 if (__cil_tmp14 <= __cil_tmp11) { 1811 { 1812#line 79 1813 while (1) { 1814 while_continue: /* CIL Label */ ; 1815 { 1816#line 79 1817 while (1) { 1818 while_continue___0: /* CIL Label */ ; 1819 { 1820#line 79 1821 __cil_tmp15 = & descriptor___2; 1822#line 79 1823 __cil_tmp16 = __cil_tmp15->flags; 1824#line 79 1825 __cil_tmp17 = __cil_tmp16 & 1U; 1826#line 79 1827 __cil_tmp18 = ! __cil_tmp17; 1828#line 79 1829 __cil_tmp19 = ! __cil_tmp18; 1830#line 79 1831 __cil_tmp20 = (long )__cil_tmp19; 1832#line 79 1833 tmp = __builtin_expect(__cil_tmp20, 0L); 1834 } 1835#line 79 1836 if (tmp) { 1837 { 1838#line 79 1839 __cil_tmp21 = (struct device const *)dev; 1840#line 79 1841 __cil_tmp22 = (unsigned long )data; 1842#line 79 1843 __cil_tmp23 = __cil_tmp22 + 92; 1844#line 79 1845 __cil_tmp24 = *((int *)__cil_tmp23); 1846#line 79 1847 __cil_tmp25 = (unsigned long )data; 1848#line 79 1849 __cil_tmp26 = __cil_tmp25 + 96; 1850#line 79 1851 __cil_tmp27 = *((int *)__cil_tmp26); 1852#line 79 1853 __dynamic_dev_dbg(& descriptor___2, __cil_tmp21, "Requesting %d-%duA\n", 1854 __cil_tmp24, __cil_tmp27); 1855 } 1856 } else { 1857 1858 } 1859#line 79 1860 goto while_break___0; 1861 } 1862 while_break___0: /* CIL Label */ ; 1863 } 1864#line 79 1865 goto while_break; 1866 } 1867 while_break: /* CIL Label */ ; 1868 } 1869 { 1870#line 81 1871 __cil_tmp28 = (unsigned long )data; 1872#line 81 1873 __cil_tmp29 = __cil_tmp28 + 72; 1874#line 81 1875 __cil_tmp30 = *((struct regulator **)__cil_tmp29); 1876#line 81 1877 __cil_tmp31 = (unsigned long )data; 1878#line 81 1879 __cil_tmp32 = __cil_tmp31 + 92; 1880#line 81 1881 __cil_tmp33 = *((int *)__cil_tmp32); 1882#line 81 1883 __cil_tmp34 = (unsigned long )data; 1884#line 81 1885 __cil_tmp35 = __cil_tmp34 + 96; 1886#line 81 1887 __cil_tmp36 = *((int *)__cil_tmp35); 1888#line 81 1889 ret = regulator_set_current_limit(__cil_tmp30, __cil_tmp33, __cil_tmp36); 1890 } 1891#line 83 1892 if (ret != 0) { 1893 { 1894#line 84 1895 __cil_tmp37 = (struct device const *)dev; 1896#line 84 1897 dev_err(__cil_tmp37, "regulator_set_current_limit() failed: %d\n", ret); 1898 } 1899#line 87 1900 return; 1901 } else { 1902 1903 } 1904 } else { 1905 1906 } 1907 } 1908 } else { 1909 1910 } 1911 } 1912 { 1913#line 91 1914 __cil_tmp38 = (unsigned long )data; 1915#line 91 1916 __cil_tmp39 = __cil_tmp38 + 96; 1917#line 91 1918 if (*((int *)__cil_tmp39)) { 1919 { 1920#line 91 1921 __cil_tmp40 = (unsigned long )data; 1922#line 91 1923 __cil_tmp41 = __cil_tmp40 + 80; 1924#line 91 1925 __cil_tmp42 = *((bool *)__cil_tmp41); 1926#line 91 1927 if (! __cil_tmp42) { 1928 { 1929#line 92 1930 while (1) { 1931 while_continue___1: /* CIL Label */ ; 1932 { 1933#line 92 1934 while (1) { 1935 while_continue___2: /* CIL Label */ ; 1936 { 1937#line 92 1938 __cil_tmp43 = & descriptor___3; 1939#line 92 1940 __cil_tmp44 = __cil_tmp43->flags; 1941#line 92 1942 __cil_tmp45 = __cil_tmp44 & 1U; 1943#line 92 1944 __cil_tmp46 = ! __cil_tmp45; 1945#line 92 1946 __cil_tmp47 = ! __cil_tmp46; 1947#line 92 1948 __cil_tmp48 = (long )__cil_tmp47; 1949#line 92 1950 tmp___0 = __builtin_expect(__cil_tmp48, 0L); 1951 } 1952#line 92 1953 if (tmp___0) { 1954 { 1955#line 92 1956 __cil_tmp49 = (struct device const *)dev; 1957#line 92 1958 __dynamic_dev_dbg(& descriptor___3, __cil_tmp49, "Enabling regulator\n"); 1959 } 1960 } else { 1961 1962 } 1963#line 92 1964 goto while_break___2; 1965 } 1966 while_break___2: /* CIL Label */ ; 1967 } 1968#line 92 1969 goto while_break___1; 1970 } 1971 while_break___1: /* CIL Label */ ; 1972 } 1973 { 1974#line 93 1975 __cil_tmp50 = (unsigned long )data; 1976#line 93 1977 __cil_tmp51 = __cil_tmp50 + 72; 1978#line 93 1979 __cil_tmp52 = *((struct regulator **)__cil_tmp51); 1980#line 93 1981 ret = regulator_enable(__cil_tmp52); 1982 } 1983#line 94 1984 if (ret == 0) { 1985#line 95 1986 __cil_tmp53 = (unsigned long )data; 1987#line 95 1988 __cil_tmp54 = __cil_tmp53 + 80; 1989#line 95 1990 *((bool *)__cil_tmp54) = (bool )1; 1991 } else { 1992 { 1993#line 97 1994 __cil_tmp55 = (struct device const *)dev; 1995#line 97 1996 dev_err(__cil_tmp55, "regulator_enable() failed: %d\n", ret); 1997 } 1998 } 1999 } else { 2000 2001 } 2002 } 2003 } else { 2004 2005 } 2006 } 2007 { 2008#line 101 2009 __cil_tmp56 = (unsigned long )data; 2010#line 101 2011 __cil_tmp57 = __cil_tmp56 + 92; 2012#line 101 2013 if (*((int *)__cil_tmp57)) { 2014 { 2015#line 101 2016 __cil_tmp58 = (unsigned long )data; 2017#line 101 2018 __cil_tmp59 = __cil_tmp58 + 96; 2019#line 101 2020 if (*((int *)__cil_tmp59)) { 2021 2022 } else { 2023#line 101 2024 goto _L; 2025 } 2026 } 2027 } else { 2028 _L: /* CIL Label */ 2029 { 2030#line 101 2031 __cil_tmp60 = (unsigned long )data; 2032#line 101 2033 __cil_tmp61 = __cil_tmp60 + 80; 2034#line 101 2035 if (*((bool *)__cil_tmp61)) { 2036 { 2037#line 102 2038 while (1) { 2039 while_continue___3: /* CIL Label */ ; 2040 { 2041#line 102 2042 while (1) { 2043 while_continue___4: /* CIL Label */ ; 2044 { 2045#line 102 2046 __cil_tmp62 = & descriptor___4; 2047#line 102 2048 __cil_tmp63 = __cil_tmp62->flags; 2049#line 102 2050 __cil_tmp64 = __cil_tmp63 & 1U; 2051#line 102 2052 __cil_tmp65 = ! __cil_tmp64; 2053#line 102 2054 __cil_tmp66 = ! __cil_tmp65; 2055#line 102 2056 __cil_tmp67 = (long )__cil_tmp66; 2057#line 102 2058 tmp___1 = __builtin_expect(__cil_tmp67, 0L); 2059 } 2060#line 102 2061 if (tmp___1) { 2062 { 2063#line 102 2064 __cil_tmp68 = (struct device const *)dev; 2065#line 102 2066 __dynamic_dev_dbg(& descriptor___4, __cil_tmp68, "Disabling regulator\n"); 2067 } 2068 } else { 2069 2070 } 2071#line 102 2072 goto while_break___4; 2073 } 2074 while_break___4: /* CIL Label */ ; 2075 } 2076#line 102 2077 goto while_break___3; 2078 } 2079 while_break___3: /* CIL Label */ ; 2080 } 2081 { 2082#line 103 2083 __cil_tmp69 = (unsigned long )data; 2084#line 103 2085 __cil_tmp70 = __cil_tmp69 + 72; 2086#line 103 2087 __cil_tmp71 = *((struct regulator **)__cil_tmp70); 2088#line 103 2089 ret = regulator_disable(__cil_tmp71); 2090 } 2091#line 104 2092 if (ret == 0) { 2093#line 105 2094 __cil_tmp72 = (unsigned long )data; 2095#line 105 2096 __cil_tmp73 = __cil_tmp72 + 80; 2097#line 105 2098 *((bool *)__cil_tmp73) = (bool )0; 2099 } else { 2100 { 2101#line 107 2102 __cil_tmp74 = (struct device const *)dev; 2103#line 107 2104 dev_err(__cil_tmp74, "regulator_disable() failed: %d\n", ret); 2105 } 2106 } 2107 } else { 2108 2109 } 2110 } 2111 } 2112 } 2113#line 110 2114 return; 2115} 2116} 2117#line 112 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 2118static ssize_t show_min_uV(struct device *dev , struct device_attribute *attr , char *buf ) 2119{ struct virtual_consumer_data *data ; 2120 void *tmp ; 2121 int tmp___0 ; 2122 struct device const *__cil_tmp7 ; 2123 unsigned long __cil_tmp8 ; 2124 unsigned long __cil_tmp9 ; 2125 int __cil_tmp10 ; 2126 2127 { 2128 { 2129#line 115 2130 __cil_tmp7 = (struct device const *)dev; 2131#line 115 2132 tmp = dev_get_drvdata(__cil_tmp7); 2133#line 115 2134 data = (struct virtual_consumer_data *)tmp; 2135#line 116 2136 __cil_tmp8 = (unsigned long )data; 2137#line 116 2138 __cil_tmp9 = __cil_tmp8 + 84; 2139#line 116 2140 __cil_tmp10 = *((int *)__cil_tmp9); 2141#line 116 2142 tmp___0 = sprintf(buf, "%d\n", __cil_tmp10); 2143 } 2144#line 116 2145 return ((ssize_t )tmp___0); 2146} 2147} 2148#line 119 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 2149static ssize_t set_min_uV(struct device *dev , struct device_attribute *attr , char const *buf , 2150 size_t count ) 2151{ struct virtual_consumer_data *data ; 2152 void *tmp ; 2153 long val ; 2154 int tmp___0 ; 2155 struct device const *__cil_tmp9 ; 2156 struct mutex *__cil_tmp10 ; 2157 unsigned long __cil_tmp11 ; 2158 unsigned long __cil_tmp12 ; 2159 long *__cil_tmp13 ; 2160 long __cil_tmp14 ; 2161 struct mutex *__cil_tmp15 ; 2162 2163 { 2164 { 2165#line 122 2166 __cil_tmp9 = (struct device const *)dev; 2167#line 122 2168 tmp = dev_get_drvdata(__cil_tmp9); 2169#line 122 2170 data = (struct virtual_consumer_data *)tmp; 2171#line 125 2172 tmp___0 = (int )kstrtol(buf, 10U, & val); 2173 } 2174#line 125 2175 if (tmp___0 != 0) { 2176#line 126 2177 return ((ssize_t )count); 2178 } else { 2179 2180 } 2181 { 2182#line 128 2183 __cil_tmp10 = (struct mutex *)data; 2184#line 128 2185 mutex_lock(__cil_tmp10); 2186#line 130 2187 __cil_tmp11 = (unsigned long )data; 2188#line 130 2189 __cil_tmp12 = __cil_tmp11 + 84; 2190#line 130 2191 __cil_tmp13 = & val; 2192#line 130 2193 __cil_tmp14 = *__cil_tmp13; 2194#line 130 2195 *((int *)__cil_tmp12) = (int )__cil_tmp14; 2196#line 131 2197 update_voltage_constraints(dev, data); 2198#line 133 2199 __cil_tmp15 = (struct mutex *)data; 2200#line 133 2201 mutex_unlock(__cil_tmp15); 2202 } 2203#line 135 2204 return ((ssize_t )count); 2205} 2206} 2207#line 138 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 2208static ssize_t show_max_uV(struct device *dev , struct device_attribute *attr , char *buf ) 2209{ struct virtual_consumer_data *data ; 2210 void *tmp ; 2211 int tmp___0 ; 2212 struct device const *__cil_tmp7 ; 2213 unsigned long __cil_tmp8 ; 2214 unsigned long __cil_tmp9 ; 2215 int __cil_tmp10 ; 2216 2217 { 2218 { 2219#line 141 2220 __cil_tmp7 = (struct device const *)dev; 2221#line 141 2222 tmp = dev_get_drvdata(__cil_tmp7); 2223#line 141 2224 data = (struct virtual_consumer_data *)tmp; 2225#line 142 2226 __cil_tmp8 = (unsigned long )data; 2227#line 142 2228 __cil_tmp9 = __cil_tmp8 + 88; 2229#line 142 2230 __cil_tmp10 = *((int *)__cil_tmp9); 2231#line 142 2232 tmp___0 = sprintf(buf, "%d\n", __cil_tmp10); 2233 } 2234#line 142 2235 return ((ssize_t )tmp___0); 2236} 2237} 2238#line 145 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 2239static ssize_t set_max_uV(struct device *dev , struct device_attribute *attr , char const *buf , 2240 size_t count ) 2241{ struct virtual_consumer_data *data ; 2242 void *tmp ; 2243 long val ; 2244 int tmp___0 ; 2245 struct device const *__cil_tmp9 ; 2246 struct mutex *__cil_tmp10 ; 2247 unsigned long __cil_tmp11 ; 2248 unsigned long __cil_tmp12 ; 2249 long *__cil_tmp13 ; 2250 long __cil_tmp14 ; 2251 struct mutex *__cil_tmp15 ; 2252 2253 { 2254 { 2255#line 148 2256 __cil_tmp9 = (struct device const *)dev; 2257#line 148 2258 tmp = dev_get_drvdata(__cil_tmp9); 2259#line 148 2260 data = (struct virtual_consumer_data *)tmp; 2261#line 151 2262 tmp___0 = (int )kstrtol(buf, 10U, & val); 2263 } 2264#line 151 2265 if (tmp___0 != 0) { 2266#line 152 2267 return ((ssize_t )count); 2268 } else { 2269 2270 } 2271 { 2272#line 154 2273 __cil_tmp10 = (struct mutex *)data; 2274#line 154 2275 mutex_lock(__cil_tmp10); 2276#line 156 2277 __cil_tmp11 = (unsigned long )data; 2278#line 156 2279 __cil_tmp12 = __cil_tmp11 + 88; 2280#line 156 2281 __cil_tmp13 = & val; 2282#line 156 2283 __cil_tmp14 = *__cil_tmp13; 2284#line 156 2285 *((int *)__cil_tmp12) = (int )__cil_tmp14; 2286#line 157 2287 update_voltage_constraints(dev, data); 2288#line 159 2289 __cil_tmp15 = (struct mutex *)data; 2290#line 159 2291 mutex_unlock(__cil_tmp15); 2292 } 2293#line 161 2294 return ((ssize_t )count); 2295} 2296} 2297#line 164 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 2298static ssize_t show_min_uA(struct device *dev , struct device_attribute *attr , char *buf ) 2299{ struct virtual_consumer_data *data ; 2300 void *tmp ; 2301 int tmp___0 ; 2302 struct device const *__cil_tmp7 ; 2303 unsigned long __cil_tmp8 ; 2304 unsigned long __cil_tmp9 ; 2305 int __cil_tmp10 ; 2306 2307 { 2308 { 2309#line 167 2310 __cil_tmp7 = (struct device const *)dev; 2311#line 167 2312 tmp = dev_get_drvdata(__cil_tmp7); 2313#line 167 2314 data = (struct virtual_consumer_data *)tmp; 2315#line 168 2316 __cil_tmp8 = (unsigned long )data; 2317#line 168 2318 __cil_tmp9 = __cil_tmp8 + 92; 2319#line 168 2320 __cil_tmp10 = *((int *)__cil_tmp9); 2321#line 168 2322 tmp___0 = sprintf(buf, "%d\n", __cil_tmp10); 2323 } 2324#line 168 2325 return ((ssize_t )tmp___0); 2326} 2327} 2328#line 171 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 2329static ssize_t set_min_uA(struct device *dev , struct device_attribute *attr , char const *buf , 2330 size_t count ) 2331{ struct virtual_consumer_data *data ; 2332 void *tmp ; 2333 long val ; 2334 int tmp___0 ; 2335 struct device const *__cil_tmp9 ; 2336 struct mutex *__cil_tmp10 ; 2337 unsigned long __cil_tmp11 ; 2338 unsigned long __cil_tmp12 ; 2339 long *__cil_tmp13 ; 2340 long __cil_tmp14 ; 2341 struct mutex *__cil_tmp15 ; 2342 2343 { 2344 { 2345#line 174 2346 __cil_tmp9 = (struct device const *)dev; 2347#line 174 2348 tmp = dev_get_drvdata(__cil_tmp9); 2349#line 174 2350 data = (struct virtual_consumer_data *)tmp; 2351#line 177 2352 tmp___0 = (int )kstrtol(buf, 10U, & val); 2353 } 2354#line 177 2355 if (tmp___0 != 0) { 2356#line 178 2357 return ((ssize_t )count); 2358 } else { 2359 2360 } 2361 { 2362#line 180 2363 __cil_tmp10 = (struct mutex *)data; 2364#line 180 2365 mutex_lock(__cil_tmp10); 2366#line 182 2367 __cil_tmp11 = (unsigned long )data; 2368#line 182 2369 __cil_tmp12 = __cil_tmp11 + 92; 2370#line 182 2371 __cil_tmp13 = & val; 2372#line 182 2373 __cil_tmp14 = *__cil_tmp13; 2374#line 182 2375 *((int *)__cil_tmp12) = (int )__cil_tmp14; 2376#line 183 2377 update_current_limit_constraints(dev, data); 2378#line 185 2379 __cil_tmp15 = (struct mutex *)data; 2380#line 185 2381 mutex_unlock(__cil_tmp15); 2382 } 2383#line 187 2384 return ((ssize_t )count); 2385} 2386} 2387#line 190 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 2388static ssize_t show_max_uA(struct device *dev , struct device_attribute *attr , char *buf ) 2389{ struct virtual_consumer_data *data ; 2390 void *tmp ; 2391 int tmp___0 ; 2392 struct device const *__cil_tmp7 ; 2393 unsigned long __cil_tmp8 ; 2394 unsigned long __cil_tmp9 ; 2395 int __cil_tmp10 ; 2396 2397 { 2398 { 2399#line 193 2400 __cil_tmp7 = (struct device const *)dev; 2401#line 193 2402 tmp = dev_get_drvdata(__cil_tmp7); 2403#line 193 2404 data = (struct virtual_consumer_data *)tmp; 2405#line 194 2406 __cil_tmp8 = (unsigned long )data; 2407#line 194 2408 __cil_tmp9 = __cil_tmp8 + 96; 2409#line 194 2410 __cil_tmp10 = *((int *)__cil_tmp9); 2411#line 194 2412 tmp___0 = sprintf(buf, "%d\n", __cil_tmp10); 2413 } 2414#line 194 2415 return ((ssize_t )tmp___0); 2416} 2417} 2418#line 197 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 2419static ssize_t set_max_uA(struct device *dev , struct device_attribute *attr , char const *buf , 2420 size_t count ) 2421{ struct virtual_consumer_data *data ; 2422 void *tmp ; 2423 long val ; 2424 int tmp___0 ; 2425 struct device const *__cil_tmp9 ; 2426 struct mutex *__cil_tmp10 ; 2427 unsigned long __cil_tmp11 ; 2428 unsigned long __cil_tmp12 ; 2429 long *__cil_tmp13 ; 2430 long __cil_tmp14 ; 2431 struct mutex *__cil_tmp15 ; 2432 2433 { 2434 { 2435#line 200 2436 __cil_tmp9 = (struct device const *)dev; 2437#line 200 2438 tmp = dev_get_drvdata(__cil_tmp9); 2439#line 200 2440 data = (struct virtual_consumer_data *)tmp; 2441#line 203 2442 tmp___0 = (int )kstrtol(buf, 10U, & val); 2443 } 2444#line 203 2445 if (tmp___0 != 0) { 2446#line 204 2447 return ((ssize_t )count); 2448 } else { 2449 2450 } 2451 { 2452#line 206 2453 __cil_tmp10 = (struct mutex *)data; 2454#line 206 2455 mutex_lock(__cil_tmp10); 2456#line 208 2457 __cil_tmp11 = (unsigned long )data; 2458#line 208 2459 __cil_tmp12 = __cil_tmp11 + 96; 2460#line 208 2461 __cil_tmp13 = & val; 2462#line 208 2463 __cil_tmp14 = *__cil_tmp13; 2464#line 208 2465 *((int *)__cil_tmp12) = (int )__cil_tmp14; 2466#line 209 2467 update_current_limit_constraints(dev, data); 2468#line 211 2469 __cil_tmp15 = (struct mutex *)data; 2470#line 211 2471 mutex_unlock(__cil_tmp15); 2472 } 2473#line 213 2474 return ((ssize_t )count); 2475} 2476} 2477#line 216 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 2478static ssize_t show_mode(struct device *dev , struct device_attribute *attr , char *buf ) 2479{ struct virtual_consumer_data *data ; 2480 void *tmp ; 2481 int tmp___0 ; 2482 int tmp___1 ; 2483 int tmp___2 ; 2484 int tmp___3 ; 2485 int tmp___4 ; 2486 struct device const *__cil_tmp11 ; 2487 unsigned long __cil_tmp12 ; 2488 unsigned long __cil_tmp13 ; 2489 unsigned int __cil_tmp14 ; 2490 2491 { 2492 { 2493#line 219 2494 __cil_tmp11 = (struct device const *)dev; 2495#line 219 2496 tmp = dev_get_drvdata(__cil_tmp11); 2497#line 219 2498 data = (struct virtual_consumer_data *)tmp; 2499 } 2500 { 2501#line 221 2502 __cil_tmp12 = (unsigned long )data; 2503#line 221 2504 __cil_tmp13 = __cil_tmp12 + 100; 2505#line 221 2506 __cil_tmp14 = *((unsigned int *)__cil_tmp13); 2507#line 222 2508 if ((int )__cil_tmp14 == 1) { 2509#line 222 2510 goto case_1; 2511 } else 2512#line 224 2513 if ((int )__cil_tmp14 == 2) { 2514#line 224 2515 goto case_2; 2516 } else 2517#line 226 2518 if ((int )__cil_tmp14 == 4) { 2519#line 226 2520 goto case_4; 2521 } else 2522#line 228 2523 if ((int )__cil_tmp14 == 8) { 2524#line 228 2525 goto case_8; 2526 } else { 2527 { 2528#line 230 2529 goto switch_default; 2530#line 221 2531 if (0) { 2532 case_1: /* CIL Label */ 2533 { 2534#line 223 2535 tmp___0 = sprintf(buf, "fast\n"); 2536 } 2537#line 223 2538 return ((ssize_t )tmp___0); 2539 case_2: /* CIL Label */ 2540 { 2541#line 225 2542 tmp___1 = sprintf(buf, "normal\n"); 2543 } 2544#line 225 2545 return ((ssize_t )tmp___1); 2546 case_4: /* CIL Label */ 2547 { 2548#line 227 2549 tmp___2 = sprintf(buf, "idle\n"); 2550 } 2551#line 227 2552 return ((ssize_t )tmp___2); 2553 case_8: /* CIL Label */ 2554 { 2555#line 229 2556 tmp___3 = sprintf(buf, "standby\n"); 2557 } 2558#line 229 2559 return ((ssize_t )tmp___3); 2560 switch_default: /* CIL Label */ 2561 { 2562#line 231 2563 tmp___4 = sprintf(buf, "unknown\n"); 2564 } 2565#line 231 2566 return ((ssize_t )tmp___4); 2567 } else { 2568 switch_break: /* CIL Label */ ; 2569 } 2570 } 2571 } 2572 } 2573} 2574} 2575#line 235 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 2576static ssize_t set_mode(struct device *dev , struct device_attribute *attr , char const *buf , 2577 size_t count ) 2578{ struct virtual_consumer_data *data ; 2579 void *tmp ; 2580 unsigned int mode ; 2581 int ret ; 2582 bool tmp___0 ; 2583 bool tmp___1 ; 2584 bool tmp___2 ; 2585 bool tmp___3 ; 2586 struct device const *__cil_tmp13 ; 2587 struct device const *__cil_tmp14 ; 2588 struct mutex *__cil_tmp15 ; 2589 unsigned long __cil_tmp16 ; 2590 unsigned long __cil_tmp17 ; 2591 struct regulator *__cil_tmp18 ; 2592 unsigned long __cil_tmp19 ; 2593 unsigned long __cil_tmp20 ; 2594 struct device const *__cil_tmp21 ; 2595 struct mutex *__cil_tmp22 ; 2596 2597 { 2598 { 2599#line 238 2600 __cil_tmp13 = (struct device const *)dev; 2601#line 238 2602 tmp = dev_get_drvdata(__cil_tmp13); 2603#line 238 2604 data = (struct virtual_consumer_data *)tmp; 2605#line 246 2606 tmp___3 = sysfs_streq(buf, "fast\n"); 2607 } 2608#line 246 2609 if (tmp___3) { 2610#line 247 2611 mode = 1U; 2612 } else { 2613 { 2614#line 248 2615 tmp___2 = sysfs_streq(buf, "normal\n"); 2616 } 2617#line 248 2618 if (tmp___2) { 2619#line 249 2620 mode = 2U; 2621 } else { 2622 { 2623#line 250 2624 tmp___1 = sysfs_streq(buf, "idle\n"); 2625 } 2626#line 250 2627 if (tmp___1) { 2628#line 251 2629 mode = 4U; 2630 } else { 2631 { 2632#line 252 2633 tmp___0 = sysfs_streq(buf, "standby\n"); 2634 } 2635#line 252 2636 if (tmp___0) { 2637#line 253 2638 mode = 8U; 2639 } else { 2640 { 2641#line 255 2642 __cil_tmp14 = (struct device const *)dev; 2643#line 255 2644 dev_err(__cil_tmp14, "Configuring invalid mode\n"); 2645 } 2646#line 256 2647 return ((ssize_t )count); 2648 } 2649 } 2650 } 2651 } 2652 { 2653#line 259 2654 __cil_tmp15 = (struct mutex *)data; 2655#line 259 2656 mutex_lock(__cil_tmp15); 2657#line 260 2658 __cil_tmp16 = (unsigned long )data; 2659#line 260 2660 __cil_tmp17 = __cil_tmp16 + 72; 2661#line 260 2662 __cil_tmp18 = *((struct regulator **)__cil_tmp17); 2663#line 260 2664 ret = regulator_set_mode(__cil_tmp18, mode); 2665 } 2666#line 261 2667 if (ret == 0) { 2668#line 262 2669 __cil_tmp19 = (unsigned long )data; 2670#line 262 2671 __cil_tmp20 = __cil_tmp19 + 100; 2672#line 262 2673 *((unsigned int *)__cil_tmp20) = mode; 2674 } else { 2675 { 2676#line 264 2677 __cil_tmp21 = (struct device const *)dev; 2678#line 264 2679 dev_err(__cil_tmp21, "Failed to configure mode: %d\n", ret); 2680 } 2681 } 2682 { 2683#line 265 2684 __cil_tmp22 = (struct mutex *)data; 2685#line 265 2686 mutex_unlock(__cil_tmp22); 2687 } 2688#line 267 2689 return ((ssize_t )count); 2690} 2691} 2692#line 270 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 2693static struct device_attribute dev_attr_min_microvolts = {{"min_microvolts", (umode_t )438}, & show_min_uV, & set_min_uV}; 2694#line 271 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 2695static struct device_attribute dev_attr_max_microvolts = {{"max_microvolts", (umode_t )438}, & show_max_uV, & set_max_uV}; 2696#line 272 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 2697static struct device_attribute dev_attr_min_microamps = {{"min_microamps", (umode_t )438}, & show_min_uA, & set_min_uA}; 2698#line 273 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 2699static struct device_attribute dev_attr_max_microamps = {{"max_microamps", (umode_t )438}, & show_max_uA, & set_max_uA}; 2700#line 274 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 2701static struct device_attribute dev_attr_mode = {{"mode", (umode_t )438}, & show_mode, & set_mode}; 2702#line 276 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 2703static struct attribute *regulator_virtual_attributes[6] = { & dev_attr_min_microvolts.attr, & dev_attr_max_microvolts.attr, & dev_attr_min_microamps.attr, & dev_attr_max_microamps.attr, 2704 & dev_attr_mode.attr, (struct attribute *)((void *)0)}; 2705#line 285 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 2706static struct attribute_group const regulator_virtual_attr_group = {(char const *)0, (umode_t (*)(struct kobject * , struct attribute * , int ))0, 2707 regulator_virtual_attributes}; 2708#line 299 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 2709static struct lock_class_key __key___2 ; 2710#line 289 2711static int regulator_virtual_probe(struct platform_device *pdev ) __attribute__((__section__(".devinit.text"), 2712__no_instrument_function__)) ; 2713#line 289 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 2714static int regulator_virtual_probe(struct platform_device *pdev ) 2715{ char *reg_id ; 2716 struct virtual_consumer_data *drvdata ; 2717 int ret ; 2718 void *tmp ; 2719 long tmp___0 ; 2720 long tmp___1 ; 2721 unsigned long __cil_tmp8 ; 2722 unsigned long __cil_tmp9 ; 2723 unsigned long __cil_tmp10 ; 2724 void *__cil_tmp11 ; 2725 void *__cil_tmp12 ; 2726 unsigned long __cil_tmp13 ; 2727 unsigned long __cil_tmp14 ; 2728 struct mutex *__cil_tmp15 ; 2729 unsigned long __cil_tmp16 ; 2730 unsigned long __cil_tmp17 ; 2731 unsigned long __cil_tmp18 ; 2732 unsigned long __cil_tmp19 ; 2733 struct device *__cil_tmp20 ; 2734 char const *__cil_tmp21 ; 2735 unsigned long __cil_tmp22 ; 2736 unsigned long __cil_tmp23 ; 2737 struct regulator *__cil_tmp24 ; 2738 void const *__cil_tmp25 ; 2739 unsigned long __cil_tmp26 ; 2740 unsigned long __cil_tmp27 ; 2741 struct regulator *__cil_tmp28 ; 2742 void const *__cil_tmp29 ; 2743 unsigned long __cil_tmp30 ; 2744 unsigned long __cil_tmp31 ; 2745 struct device *__cil_tmp32 ; 2746 struct device const *__cil_tmp33 ; 2747 unsigned long __cil_tmp34 ; 2748 unsigned long __cil_tmp35 ; 2749 unsigned long __cil_tmp36 ; 2750 struct kobject *__cil_tmp37 ; 2751 unsigned long __cil_tmp38 ; 2752 unsigned long __cil_tmp39 ; 2753 struct device *__cil_tmp40 ; 2754 struct device const *__cil_tmp41 ; 2755 unsigned long __cil_tmp42 ; 2756 unsigned long __cil_tmp43 ; 2757 unsigned long __cil_tmp44 ; 2758 unsigned long __cil_tmp45 ; 2759 struct regulator *__cil_tmp46 ; 2760 void *__cil_tmp47 ; 2761 unsigned long __cil_tmp48 ; 2762 unsigned long __cil_tmp49 ; 2763 struct regulator *__cil_tmp50 ; 2764 void const *__cil_tmp51 ; 2765 2766 { 2767 { 2768#line 291 2769 __cil_tmp8 = 16 + 184; 2770#line 291 2771 __cil_tmp9 = (unsigned long )pdev; 2772#line 291 2773 __cil_tmp10 = __cil_tmp9 + __cil_tmp8; 2774#line 291 2775 __cil_tmp11 = *((void **)__cil_tmp10); 2776#line 291 2777 reg_id = (char *)__cil_tmp11; 2778#line 295 2779 tmp = kzalloc(104UL, 208U); 2780#line 295 2781 drvdata = (struct virtual_consumer_data *)tmp; 2782 } 2783 { 2784#line 296 2785 __cil_tmp12 = (void *)0; 2786#line 296 2787 __cil_tmp13 = (unsigned long )__cil_tmp12; 2788#line 296 2789 __cil_tmp14 = (unsigned long )drvdata; 2790#line 296 2791 if (__cil_tmp14 == __cil_tmp13) { 2792#line 297 2793 return (-12); 2794 } else { 2795 2796 } 2797 } 2798 { 2799#line 299 2800 while (1) { 2801 while_continue: /* CIL Label */ ; 2802 { 2803#line 299 2804 __cil_tmp15 = (struct mutex *)drvdata; 2805#line 299 2806 __mutex_init(__cil_tmp15, "&drvdata->lock", & __key___2); 2807 } 2808#line 299 2809 goto while_break; 2810 } 2811 while_break: /* CIL Label */ ; 2812 } 2813 { 2814#line 301 2815 __cil_tmp16 = (unsigned long )drvdata; 2816#line 301 2817 __cil_tmp17 = __cil_tmp16 + 72; 2818#line 301 2819 __cil_tmp18 = (unsigned long )pdev; 2820#line 301 2821 __cil_tmp19 = __cil_tmp18 + 16; 2822#line 301 2823 __cil_tmp20 = (struct device *)__cil_tmp19; 2824#line 301 2825 __cil_tmp21 = (char const *)reg_id; 2826#line 301 2827 *((struct regulator **)__cil_tmp17) = (struct regulator *)regulator_get(__cil_tmp20, 2828 __cil_tmp21); 2829#line 302 2830 __cil_tmp22 = (unsigned long )drvdata; 2831#line 302 2832 __cil_tmp23 = __cil_tmp22 + 72; 2833#line 302 2834 __cil_tmp24 = *((struct regulator **)__cil_tmp23); 2835#line 302 2836 __cil_tmp25 = (void const *)__cil_tmp24; 2837#line 302 2838 tmp___1 = (long )IS_ERR(__cil_tmp25); 2839 } 2840#line 302 2841 if (tmp___1) { 2842 { 2843#line 303 2844 __cil_tmp26 = (unsigned long )drvdata; 2845#line 303 2846 __cil_tmp27 = __cil_tmp26 + 72; 2847#line 303 2848 __cil_tmp28 = *((struct regulator **)__cil_tmp27); 2849#line 303 2850 __cil_tmp29 = (void const *)__cil_tmp28; 2851#line 303 2852 tmp___0 = (long )PTR_ERR(__cil_tmp29); 2853#line 303 2854 ret = (int )tmp___0; 2855#line 304 2856 __cil_tmp30 = (unsigned long )pdev; 2857#line 304 2858 __cil_tmp31 = __cil_tmp30 + 16; 2859#line 304 2860 __cil_tmp32 = (struct device *)__cil_tmp31; 2861#line 304 2862 __cil_tmp33 = (struct device const *)__cil_tmp32; 2863#line 304 2864 dev_err(__cil_tmp33, "Failed to obtain supply \'%s\': %d\n", reg_id, ret); 2865 } 2866#line 306 2867 goto err; 2868 } else { 2869 2870 } 2871 { 2872#line 309 2873 __cil_tmp34 = 16 + 16; 2874#line 309 2875 __cil_tmp35 = (unsigned long )pdev; 2876#line 309 2877 __cil_tmp36 = __cil_tmp35 + __cil_tmp34; 2878#line 309 2879 __cil_tmp37 = (struct kobject *)__cil_tmp36; 2880#line 309 2881 ret = (int )sysfs_create_group(__cil_tmp37, & regulator_virtual_attr_group); 2882 } 2883#line 311 2884 if (ret != 0) { 2885 { 2886#line 312 2887 __cil_tmp38 = (unsigned long )pdev; 2888#line 312 2889 __cil_tmp39 = __cil_tmp38 + 16; 2890#line 312 2891 __cil_tmp40 = (struct device *)__cil_tmp39; 2892#line 312 2893 __cil_tmp41 = (struct device const *)__cil_tmp40; 2894#line 312 2895 dev_err(__cil_tmp41, "Failed to create attribute group: %d\n", ret); 2896 } 2897#line 314 2898 goto err_regulator; 2899 } else { 2900 2901 } 2902 { 2903#line 317 2904 __cil_tmp42 = (unsigned long )drvdata; 2905#line 317 2906 __cil_tmp43 = __cil_tmp42 + 100; 2907#line 317 2908 __cil_tmp44 = (unsigned long )drvdata; 2909#line 317 2910 __cil_tmp45 = __cil_tmp44 + 72; 2911#line 317 2912 __cil_tmp46 = *((struct regulator **)__cil_tmp45); 2913#line 317 2914 *((unsigned int *)__cil_tmp43) = regulator_get_mode(__cil_tmp46); 2915#line 319 2916 __cil_tmp47 = (void *)drvdata; 2917#line 319 2918 platform_set_drvdata(pdev, __cil_tmp47); 2919 } 2920#line 321 2921 return (0); 2922 err_regulator: 2923 { 2924#line 324 2925 __cil_tmp48 = (unsigned long )drvdata; 2926#line 324 2927 __cil_tmp49 = __cil_tmp48 + 72; 2928#line 324 2929 __cil_tmp50 = *((struct regulator **)__cil_tmp49); 2930#line 324 2931 regulator_put(__cil_tmp50); 2932 } 2933 err: 2934 { 2935#line 326 2936 __cil_tmp51 = (void const *)drvdata; 2937#line 326 2938 kfree(__cil_tmp51); 2939 } 2940#line 327 2941 return (ret); 2942} 2943} 2944#line 330 2945static int regulator_virtual_remove(struct platform_device *pdev ) __attribute__((__section__(".devexit.text"), 2946__no_instrument_function__)) ; 2947#line 330 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 2948static int regulator_virtual_remove(struct platform_device *pdev ) 2949{ struct virtual_consumer_data *drvdata ; 2950 void *tmp ; 2951 struct platform_device const *__cil_tmp4 ; 2952 unsigned long __cil_tmp5 ; 2953 unsigned long __cil_tmp6 ; 2954 unsigned long __cil_tmp7 ; 2955 struct kobject *__cil_tmp8 ; 2956 unsigned long __cil_tmp9 ; 2957 unsigned long __cil_tmp10 ; 2958 unsigned long __cil_tmp11 ; 2959 unsigned long __cil_tmp12 ; 2960 struct regulator *__cil_tmp13 ; 2961 unsigned long __cil_tmp14 ; 2962 unsigned long __cil_tmp15 ; 2963 struct regulator *__cil_tmp16 ; 2964 void const *__cil_tmp17 ; 2965 void *__cil_tmp18 ; 2966 2967 { 2968 { 2969#line 332 2970 __cil_tmp4 = (struct platform_device const *)pdev; 2971#line 332 2972 tmp = platform_get_drvdata(__cil_tmp4); 2973#line 332 2974 drvdata = (struct virtual_consumer_data *)tmp; 2975#line 334 2976 __cil_tmp5 = 16 + 16; 2977#line 334 2978 __cil_tmp6 = (unsigned long )pdev; 2979#line 334 2980 __cil_tmp7 = __cil_tmp6 + __cil_tmp5; 2981#line 334 2982 __cil_tmp8 = (struct kobject *)__cil_tmp7; 2983#line 334 2984 sysfs_remove_group(__cil_tmp8, & regulator_virtual_attr_group); 2985 } 2986 { 2987#line 336 2988 __cil_tmp9 = (unsigned long )drvdata; 2989#line 336 2990 __cil_tmp10 = __cil_tmp9 + 80; 2991#line 336 2992 if (*((bool *)__cil_tmp10)) { 2993 { 2994#line 337 2995 __cil_tmp11 = (unsigned long )drvdata; 2996#line 337 2997 __cil_tmp12 = __cil_tmp11 + 72; 2998#line 337 2999 __cil_tmp13 = *((struct regulator **)__cil_tmp12); 3000#line 337 3001 regulator_disable(__cil_tmp13); 3002 } 3003 } else { 3004 3005 } 3006 } 3007 { 3008#line 338 3009 __cil_tmp14 = (unsigned long )drvdata; 3010#line 338 3011 __cil_tmp15 = __cil_tmp14 + 72; 3012#line 338 3013 __cil_tmp16 = *((struct regulator **)__cil_tmp15); 3014#line 338 3015 regulator_put(__cil_tmp16); 3016#line 340 3017 __cil_tmp17 = (void const *)drvdata; 3018#line 340 3019 kfree(__cil_tmp17); 3020#line 342 3021 __cil_tmp18 = (void *)0; 3022#line 342 3023 platform_set_drvdata(pdev, __cil_tmp18); 3024 } 3025#line 344 3026 return (0); 3027} 3028} 3029#line 347 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 3030static struct platform_driver regulator_virtual_consumer_driver = {& regulator_virtual_probe, & regulator_virtual_remove, (void (*)(struct platform_device * ))0, 3031 (int (*)(struct platform_device * , pm_message_t state ))0, (int (*)(struct platform_device * ))0, 3032 {"reg-virt-consumer", (struct bus_type *)0, & __this_module, (char const *)0, 3033 (_Bool)0, (struct of_device_id const *)0, (int (*)(struct device *dev ))0, 3034 (int (*)(struct device *dev ))0, (void (*)(struct device *dev ))0, (int (*)(struct device *dev , 3035 pm_message_t state ))0, 3036 (int (*)(struct device *dev ))0, (struct attribute_group const **)0, (struct dev_pm_ops const *)0, 3037 (struct driver_private *)0}, (struct platform_device_id const *)0}; 3038#line 356 3039static int regulator_virtual_consumer_driver_init(void) __attribute__((__section__(".init.text"), 3040__no_instrument_function__)) ; 3041#line 356 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 3042static int regulator_virtual_consumer_driver_init(void) 3043{ int tmp ; 3044 3045 { 3046 { 3047#line 356 3048 tmp = platform_driver_register(& regulator_virtual_consumer_driver); 3049 } 3050#line 356 3051 return (tmp); 3052} 3053} 3054#line 356 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 3055int init_module(void) 3056{ int tmp ; 3057 3058 { 3059 { 3060#line 356 3061 tmp = regulator_virtual_consumer_driver_init(); 3062 } 3063#line 356 3064 return (tmp); 3065} 3066} 3067#line 356 3068static void regulator_virtual_consumer_driver_exit(void) __attribute__((__section__(".exit.text"), 3069__no_instrument_function__)) ; 3070#line 356 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 3071static void regulator_virtual_consumer_driver_exit(void) 3072{ 3073 3074 { 3075 { 3076#line 356 3077 platform_driver_unregister(& regulator_virtual_consumer_driver); 3078 } 3079#line 356 3080 return; 3081} 3082} 3083#line 356 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 3084void cleanup_module(void) 3085{ 3086 3087 { 3088 { 3089#line 356 3090 regulator_virtual_consumer_driver_exit(); 3091 } 3092#line 356 3093 return; 3094} 3095} 3096#line 358 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 3097static char const __mod_author358[56] __attribute__((__used__, __unused__, __section__(".modinfo"), 3098__aligned__(1))) = 3099#line 358 3100 { (char const )'a', (char const )'u', (char const )'t', (char const )'h', 3101 (char const )'o', (char const )'r', (char const )'=', (char const )'M', 3102 (char const )'a', (char const )'r', (char const )'k', (char const )' ', 3103 (char const )'B', (char const )'r', (char const )'o', (char const )'w', 3104 (char const )'n', (char const )' ', (char const )'<', (char const )'b', 3105 (char const )'r', (char const )'o', (char const )'o', (char const )'n', 3106 (char const )'i', (char const )'e', (char const )'@', (char const )'o', 3107 (char const )'p', (char const )'e', (char const )'n', (char const )'s', 3108 (char const )'o', (char const )'u', (char const )'r', (char const )'c', 3109 (char const )'e', (char const )'.', (char const )'w', (char const )'o', 3110 (char const )'l', (char const )'f', (char const )'s', (char const )'o', 3111 (char const )'n', (char const )'m', (char const )'i', (char const )'c', 3112 (char const )'r', (char const )'o', (char const )'.', (char const )'c', 3113 (char const )'o', (char const )'m', (char const )'>', (char const )'\000'}; 3114#line 359 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 3115static char const __mod_description359[39] __attribute__((__used__, __unused__, 3116__section__(".modinfo"), __aligned__(1))) = 3117#line 359 3118 { (char const )'d', (char const )'e', (char const )'s', (char const )'c', 3119 (char const )'r', (char const )'i', (char const )'p', (char const )'t', 3120 (char const )'i', (char const )'o', (char const )'n', (char const )'=', 3121 (char const )'V', (char const )'i', (char const )'r', (char const )'t', 3122 (char const )'u', (char const )'a', (char const )'l', (char const )' ', 3123 (char const )'r', (char const )'e', (char const )'g', (char const )'u', 3124 (char const )'l', (char const )'a', (char const )'t', (char const )'o', 3125 (char const )'r', (char const )' ', (char const )'c', (char const )'o', 3126 (char const )'n', (char const )'s', (char const )'u', (char const )'m', 3127 (char const )'e', (char const )'r', (char const )'\000'}; 3128#line 360 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 3129static char const __mod_license360[12] __attribute__((__used__, __unused__, __section__(".modinfo"), 3130__aligned__(1))) = 3131#line 360 3132 { (char const )'l', (char const )'i', (char const )'c', (char const )'e', 3133 (char const )'n', (char const )'s', (char const )'e', (char const )'=', 3134 (char const )'G', (char const )'P', (char const )'L', (char const )'\000'}; 3135#line 361 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 3136static char const __mod_alias361[33] __attribute__((__used__, __unused__, __section__(".modinfo"), 3137__aligned__(1))) = 3138#line 361 3139 { (char const )'a', (char const )'l', (char const )'i', (char const )'a', 3140 (char const )'s', (char const )'=', (char const )'p', (char const )'l', 3141 (char const )'a', (char const )'t', (char const )'f', (char const )'o', 3142 (char const )'r', (char const )'m', (char const )':', (char const )'r', 3143 (char const )'e', (char const )'g', (char const )'-', (char const )'v', 3144 (char const )'i', (char const )'r', (char const )'t', (char const )'-', 3145 (char const )'c', (char const )'o', (char const )'n', (char const )'s', 3146 (char const )'u', (char const )'m', (char const )'e', (char const )'r', 3147 (char const )'\000'}; 3148#line 379 3149void ldv_check_final_state(void) ; 3150#line 382 3151extern void ldv_check_return_value(int res ) ; 3152#line 385 3153extern void ldv_initialize(void) ; 3154#line 388 3155extern int __VERIFIER_nondet_int(void) ; 3156#line 391 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 3157int LDV_IN_INTERRUPT ; 3158#line 406 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 3159static int res_regulator_virtual_probe_12 ; 3160#line 394 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 3161void main(void) 3162{ struct platform_device *var_group1 ; 3163 int ldv_s_regulator_virtual_consumer_driver_platform_driver ; 3164 int tmp ; 3165 int tmp___0 ; 3166 int __cil_tmp5 ; 3167 3168 { 3169 { 3170#line 414 3171 LDV_IN_INTERRUPT = 1; 3172#line 423 3173 ldv_initialize(); 3174#line 424 3175 ldv_s_regulator_virtual_consumer_driver_platform_driver = 0; 3176 } 3177 { 3178#line 427 3179 while (1) { 3180 while_continue: /* CIL Label */ ; 3181 { 3182#line 427 3183 tmp___0 = __VERIFIER_nondet_int(); 3184 } 3185#line 427 3186 if (tmp___0) { 3187 3188 } else { 3189 { 3190#line 427 3191 __cil_tmp5 = ldv_s_regulator_virtual_consumer_driver_platform_driver == 0; 3192#line 427 3193 if (! __cil_tmp5) { 3194 3195 } else { 3196#line 427 3197 goto while_break; 3198 } 3199 } 3200 } 3201 { 3202#line 431 3203 tmp = __VERIFIER_nondet_int(); 3204 } 3205#line 433 3206 if (tmp == 0) { 3207#line 433 3208 goto case_0; 3209 } else { 3210 { 3211#line 452 3212 goto switch_default; 3213#line 431 3214 if (0) { 3215 case_0: /* CIL Label */ 3216#line 436 3217 if (ldv_s_regulator_virtual_consumer_driver_platform_driver == 0) { 3218 { 3219#line 441 3220 res_regulator_virtual_probe_12 = regulator_virtual_probe(var_group1); 3221#line 442 3222 ldv_check_return_value(res_regulator_virtual_probe_12); 3223 } 3224#line 443 3225 if (res_regulator_virtual_probe_12) { 3226#line 444 3227 goto ldv_module_exit; 3228 } else { 3229 3230 } 3231#line 445 3232 ldv_s_regulator_virtual_consumer_driver_platform_driver = 0; 3233 } else { 3234 3235 } 3236#line 451 3237 goto switch_break; 3238 switch_default: /* CIL Label */ 3239#line 452 3240 goto switch_break; 3241 } else { 3242 switch_break: /* CIL Label */ ; 3243 } 3244 } 3245 } 3246 } 3247 while_break: /* CIL Label */ ; 3248 } 3249 ldv_module_exit: 3250 { 3251#line 461 3252 ldv_check_final_state(); 3253 } 3254#line 464 3255 return; 3256} 3257} 3258#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h" 3259void ldv_blast_assert(void) 3260{ 3261 3262 { 3263 ERROR: 3264#line 6 3265 goto ERROR; 3266} 3267} 3268#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h" 3269extern int __VERIFIER_nondet_int(void) ; 3270#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c" 3271int ldv_mutex = 1; 3272#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c" 3273int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock ) 3274{ int nondetermined ; 3275 3276 { 3277#line 29 3278 if (ldv_mutex == 1) { 3279 3280 } else { 3281 { 3282#line 29 3283 ldv_blast_assert(); 3284 } 3285 } 3286 { 3287#line 32 3288 nondetermined = __VERIFIER_nondet_int(); 3289 } 3290#line 35 3291 if (nondetermined) { 3292#line 38 3293 ldv_mutex = 2; 3294#line 40 3295 return (0); 3296 } else { 3297#line 45 3298 return (-4); 3299 } 3300} 3301} 3302#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c" 3303int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock ) 3304{ int nondetermined ; 3305 3306 { 3307#line 57 3308 if (ldv_mutex == 1) { 3309 3310 } else { 3311 { 3312#line 57 3313 ldv_blast_assert(); 3314 } 3315 } 3316 { 3317#line 60 3318 nondetermined = __VERIFIER_nondet_int(); 3319 } 3320#line 63 3321 if (nondetermined) { 3322#line 66 3323 ldv_mutex = 2; 3324#line 68 3325 return (0); 3326 } else { 3327#line 73 3328 return (-4); 3329 } 3330} 3331} 3332#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c" 3333int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) 3334{ int atomic_value_after_dec ; 3335 3336 { 3337#line 83 3338 if (ldv_mutex == 1) { 3339 3340 } else { 3341 { 3342#line 83 3343 ldv_blast_assert(); 3344 } 3345 } 3346 { 3347#line 86 3348 atomic_value_after_dec = __VERIFIER_nondet_int(); 3349 } 3350#line 89 3351 if (atomic_value_after_dec == 0) { 3352#line 92 3353 ldv_mutex = 2; 3354#line 94 3355 return (1); 3356 } else { 3357 3358 } 3359#line 98 3360 return (0); 3361} 3362} 3363#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c" 3364void mutex_lock(struct mutex *lock ) 3365{ 3366 3367 { 3368#line 108 3369 if (ldv_mutex == 1) { 3370 3371 } else { 3372 { 3373#line 108 3374 ldv_blast_assert(); 3375 } 3376 } 3377#line 110 3378 ldv_mutex = 2; 3379#line 111 3380 return; 3381} 3382} 3383#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c" 3384int mutex_trylock(struct mutex *lock ) 3385{ int nondetermined ; 3386 3387 { 3388#line 121 3389 if (ldv_mutex == 1) { 3390 3391 } else { 3392 { 3393#line 121 3394 ldv_blast_assert(); 3395 } 3396 } 3397 { 3398#line 124 3399 nondetermined = __VERIFIER_nondet_int(); 3400 } 3401#line 127 3402 if (nondetermined) { 3403#line 130 3404 ldv_mutex = 2; 3405#line 132 3406 return (1); 3407 } else { 3408#line 137 3409 return (0); 3410 } 3411} 3412} 3413#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c" 3414void mutex_unlock(struct mutex *lock ) 3415{ 3416 3417 { 3418#line 147 3419 if (ldv_mutex == 2) { 3420 3421 } else { 3422 { 3423#line 147 3424 ldv_blast_assert(); 3425 } 3426 } 3427#line 149 3428 ldv_mutex = 1; 3429#line 150 3430 return; 3431} 3432} 3433#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c" 3434void ldv_check_final_state(void) 3435{ 3436 3437 { 3438#line 156 3439 if (ldv_mutex == 1) { 3440 3441 } else { 3442 { 3443#line 156 3444 ldv_blast_assert(); 3445 } 3446 } 3447#line 157 3448 return; 3449} 3450} 3451#line 473 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4591/dscv_tempdir/dscv/ri/32_1/drivers/regulator/virtual.c.common.c" 3452long s__builtin_expect(long val , long res ) 3453{ 3454 3455 { 3456#line 474 3457 return (val); 3458} 3459}

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--regulator--virtual.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file:	3263
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 590

Source: