Showing error 1180

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/43_1a_cilled_safe_ok_nondet_linux-43_1a-drivers--regulator--userspace-consumer.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 1909
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

   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 43 "include/asm-generic/int-ll64.h"
  11typedef unsigned char u8;
  12#line 45 "include/asm-generic/int-ll64.h"
  13typedef short s16;
  14#line 46 "include/asm-generic/int-ll64.h"
  15typedef unsigned short u16;
  16#line 49 "include/asm-generic/int-ll64.h"
  17typedef unsigned int u32;
  18#line 51 "include/asm-generic/int-ll64.h"
  19typedef long long s64;
  20#line 52 "include/asm-generic/int-ll64.h"
  21typedef unsigned long long u64;
  22#line 14 "include/asm-generic/posix_types.h"
  23typedef long __kernel_long_t;
  24#line 15 "include/asm-generic/posix_types.h"
  25typedef unsigned long __kernel_ulong_t;
  26#line 75 "include/asm-generic/posix_types.h"
  27typedef __kernel_ulong_t __kernel_size_t;
  28#line 76 "include/asm-generic/posix_types.h"
  29typedef __kernel_long_t __kernel_ssize_t;
  30#line 91 "include/asm-generic/posix_types.h"
  31typedef long long __kernel_loff_t;
  32#line 21 "include/linux/types.h"
  33typedef __u32 __kernel_dev_t;
  34#line 24 "include/linux/types.h"
  35typedef __kernel_dev_t dev_t;
  36#line 27 "include/linux/types.h"
  37typedef unsigned short umode_t;
  38#line 38 "include/linux/types.h"
  39typedef _Bool bool;
  40#line 54 "include/linux/types.h"
  41typedef __kernel_loff_t loff_t;
  42#line 63 "include/linux/types.h"
  43typedef __kernel_size_t size_t;
  44#line 68 "include/linux/types.h"
  45typedef __kernel_ssize_t ssize_t;
  46#line 202 "include/linux/types.h"
  47typedef unsigned int gfp_t;
  48#line 206 "include/linux/types.h"
  49typedef u64 phys_addr_t;
  50#line 211 "include/linux/types.h"
  51typedef phys_addr_t resource_size_t;
  52#line 221 "include/linux/types.h"
  53struct __anonstruct_atomic_t_6 {
  54   int counter ;
  55};
  56#line 221 "include/linux/types.h"
  57typedef struct __anonstruct_atomic_t_6 atomic_t;
  58#line 226 "include/linux/types.h"
  59struct __anonstruct_atomic64_t_7 {
  60   long counter ;
  61};
  62#line 226 "include/linux/types.h"
  63typedef struct __anonstruct_atomic64_t_7 atomic64_t;
  64#line 227 "include/linux/types.h"
  65struct list_head {
  66   struct list_head *next ;
  67   struct list_head *prev ;
  68};
  69#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
  70struct module;
  71#line 55
  72struct module;
  73#line 146 "include/linux/init.h"
  74typedef void (*ctor_fn_t)(void);
  75#line 46 "include/linux/dynamic_debug.h"
  76struct device;
  77#line 46
  78struct device;
  79#line 57
  80struct completion;
  81#line 57
  82struct completion;
  83#line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
  84struct page;
  85#line 58
  86struct page;
  87#line 26 "include/asm-generic/getorder.h"
  88struct task_struct;
  89#line 26
  90struct task_struct;
  91#line 290 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
  92struct file;
  93#line 290
  94struct file;
  95#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
  96struct arch_spinlock;
  97#line 327
  98struct arch_spinlock;
  99#line 306 "include/linux/bitmap.h"
 100struct bug_entry {
 101   int bug_addr_disp ;
 102   int file_disp ;
 103   unsigned short line ;
 104   unsigned short flags ;
 105};
 106#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
 107struct static_key;
 108#line 234
 109struct static_key;
 110#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 111struct kmem_cache;
 112#line 23 "include/asm-generic/atomic-long.h"
 113typedef atomic64_t atomic_long_t;
 114#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 115typedef u16 __ticket_t;
 116#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 117typedef u32 __ticketpair_t;
 118#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 119struct __raw_tickets {
 120   __ticket_t head ;
 121   __ticket_t tail ;
 122};
 123#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 124union __anonunion_ldv_5907_29 {
 125   __ticketpair_t head_tail ;
 126   struct __raw_tickets tickets ;
 127};
 128#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 129struct arch_spinlock {
 130   union __anonunion_ldv_5907_29 ldv_5907 ;
 131};
 132#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 133typedef struct arch_spinlock arch_spinlock_t;
 134#line 34 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 135struct lockdep_map;
 136#line 34
 137struct lockdep_map;
 138#line 55 "include/linux/debug_locks.h"
 139struct stack_trace {
 140   unsigned int nr_entries ;
 141   unsigned int max_entries ;
 142   unsigned long *entries ;
 143   int skip ;
 144};
 145#line 26 "include/linux/stacktrace.h"
 146struct lockdep_subclass_key {
 147   char __one_byte ;
 148};
 149#line 53 "include/linux/lockdep.h"
 150struct lock_class_key {
 151   struct lockdep_subclass_key subkeys[8U] ;
 152};
 153#line 59 "include/linux/lockdep.h"
 154struct lock_class {
 155   struct list_head hash_entry ;
 156   struct list_head lock_entry ;
 157   struct lockdep_subclass_key *key ;
 158   unsigned int subclass ;
 159   unsigned int dep_gen_id ;
 160   unsigned long usage_mask ;
 161   struct stack_trace usage_traces[13U] ;
 162   struct list_head locks_after ;
 163   struct list_head locks_before ;
 164   unsigned int version ;
 165   unsigned long ops ;
 166   char const   *name ;
 167   int name_version ;
 168   unsigned long contention_point[4U] ;
 169   unsigned long contending_point[4U] ;
 170};
 171#line 144 "include/linux/lockdep.h"
 172struct lockdep_map {
 173   struct lock_class_key *key ;
 174   struct lock_class *class_cache[2U] ;
 175   char const   *name ;
 176   int cpu ;
 177   unsigned long ip ;
 178};
 179#line 556 "include/linux/lockdep.h"
 180struct raw_spinlock {
 181   arch_spinlock_t raw_lock ;
 182   unsigned int magic ;
 183   unsigned int owner_cpu ;
 184   void *owner ;
 185   struct lockdep_map dep_map ;
 186};
 187#line 33 "include/linux/spinlock_types.h"
 188struct __anonstruct_ldv_6122_33 {
 189   u8 __padding[24U] ;
 190   struct lockdep_map dep_map ;
 191};
 192#line 33 "include/linux/spinlock_types.h"
 193union __anonunion_ldv_6123_32 {
 194   struct raw_spinlock rlock ;
 195   struct __anonstruct_ldv_6122_33 ldv_6122 ;
 196};
 197#line 33 "include/linux/spinlock_types.h"
 198struct spinlock {
 199   union __anonunion_ldv_6123_32 ldv_6123 ;
 200};
 201#line 76 "include/linux/spinlock_types.h"
 202typedef struct spinlock spinlock_t;
 203#line 48 "include/linux/wait.h"
 204struct __wait_queue_head {
 205   spinlock_t lock ;
 206   struct list_head task_list ;
 207};
 208#line 53 "include/linux/wait.h"
 209typedef struct __wait_queue_head wait_queue_head_t;
 210#line 670 "include/linux/mmzone.h"
 211struct mutex {
 212   atomic_t count ;
 213   spinlock_t wait_lock ;
 214   struct list_head wait_list ;
 215   struct task_struct *owner ;
 216   char const   *name ;
 217   void *magic ;
 218   struct lockdep_map dep_map ;
 219};
 220#line 128 "include/linux/rwsem.h"
 221struct completion {
 222   unsigned int done ;
 223   wait_queue_head_t wait ;
 224};
 225#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/e820.h"
 226struct resource {
 227   resource_size_t start ;
 228   resource_size_t end ;
 229   char const   *name ;
 230   unsigned long flags ;
 231   struct resource *parent ;
 232   struct resource *sibling ;
 233   struct resource *child ;
 234};
 235#line 312 "include/linux/jiffies.h"
 236union ktime {
 237   s64 tv64 ;
 238};
 239#line 59 "include/linux/ktime.h"
 240typedef union ktime ktime_t;
 241#line 341
 242struct tvec_base;
 243#line 341
 244struct tvec_base;
 245#line 342 "include/linux/ktime.h"
 246struct timer_list {
 247   struct list_head entry ;
 248   unsigned long expires ;
 249   struct tvec_base *base ;
 250   void (*function)(unsigned long  ) ;
 251   unsigned long data ;
 252   int slack ;
 253   int start_pid ;
 254   void *start_site ;
 255   char start_comm[16U] ;
 256   struct lockdep_map lockdep_map ;
 257};
 258#line 302 "include/linux/timer.h"
 259struct work_struct;
 260#line 302
 261struct work_struct;
 262#line 45 "include/linux/workqueue.h"
 263struct work_struct {
 264   atomic_long_t data ;
 265   struct list_head entry ;
 266   void (*func)(struct work_struct * ) ;
 267   struct lockdep_map lockdep_map ;
 268};
 269#line 46 "include/linux/pm.h"
 270struct pm_message {
 271   int event ;
 272};
 273#line 52 "include/linux/pm.h"
 274typedef struct pm_message pm_message_t;
 275#line 53 "include/linux/pm.h"
 276struct dev_pm_ops {
 277   int (*prepare)(struct device * ) ;
 278   void (*complete)(struct device * ) ;
 279   int (*suspend)(struct device * ) ;
 280   int (*resume)(struct device * ) ;
 281   int (*freeze)(struct device * ) ;
 282   int (*thaw)(struct device * ) ;
 283   int (*poweroff)(struct device * ) ;
 284   int (*restore)(struct device * ) ;
 285   int (*suspend_late)(struct device * ) ;
 286   int (*resume_early)(struct device * ) ;
 287   int (*freeze_late)(struct device * ) ;
 288   int (*thaw_early)(struct device * ) ;
 289   int (*poweroff_late)(struct device * ) ;
 290   int (*restore_early)(struct device * ) ;
 291   int (*suspend_noirq)(struct device * ) ;
 292   int (*resume_noirq)(struct device * ) ;
 293   int (*freeze_noirq)(struct device * ) ;
 294   int (*thaw_noirq)(struct device * ) ;
 295   int (*poweroff_noirq)(struct device * ) ;
 296   int (*restore_noirq)(struct device * ) ;
 297   int (*runtime_suspend)(struct device * ) ;
 298   int (*runtime_resume)(struct device * ) ;
 299   int (*runtime_idle)(struct device * ) ;
 300};
 301#line 289
 302enum rpm_status {
 303    RPM_ACTIVE = 0,
 304    RPM_RESUMING = 1,
 305    RPM_SUSPENDED = 2,
 306    RPM_SUSPENDING = 3
 307} ;
 308#line 296
 309enum rpm_request {
 310    RPM_REQ_NONE = 0,
 311    RPM_REQ_IDLE = 1,
 312    RPM_REQ_SUSPEND = 2,
 313    RPM_REQ_AUTOSUSPEND = 3,
 314    RPM_REQ_RESUME = 4
 315} ;
 316#line 304
 317struct wakeup_source;
 318#line 304
 319struct wakeup_source;
 320#line 494 "include/linux/pm.h"
 321struct pm_subsys_data {
 322   spinlock_t lock ;
 323   unsigned int refcount ;
 324};
 325#line 499
 326struct dev_pm_qos_request;
 327#line 499
 328struct pm_qos_constraints;
 329#line 499 "include/linux/pm.h"
 330struct dev_pm_info {
 331   pm_message_t power_state ;
 332   unsigned char can_wakeup : 1 ;
 333   unsigned char async_suspend : 1 ;
 334   bool is_prepared ;
 335   bool is_suspended ;
 336   bool ignore_children ;
 337   spinlock_t lock ;
 338   struct list_head entry ;
 339   struct completion completion ;
 340   struct wakeup_source *wakeup ;
 341   bool wakeup_path ;
 342   struct timer_list suspend_timer ;
 343   unsigned long timer_expires ;
 344   struct work_struct work ;
 345   wait_queue_head_t wait_queue ;
 346   atomic_t usage_count ;
 347   atomic_t child_count ;
 348   unsigned char disable_depth : 3 ;
 349   unsigned char idle_notification : 1 ;
 350   unsigned char request_pending : 1 ;
 351   unsigned char deferred_resume : 1 ;
 352   unsigned char run_wake : 1 ;
 353   unsigned char runtime_auto : 1 ;
 354   unsigned char no_callbacks : 1 ;
 355   unsigned char irq_safe : 1 ;
 356   unsigned char use_autosuspend : 1 ;
 357   unsigned char timer_autosuspends : 1 ;
 358   enum rpm_request request ;
 359   enum rpm_status runtime_status ;
 360   int runtime_error ;
 361   int autosuspend_delay ;
 362   unsigned long last_busy ;
 363   unsigned long active_jiffies ;
 364   unsigned long suspended_jiffies ;
 365   unsigned long accounting_timestamp ;
 366   ktime_t suspend_time ;
 367   s64 max_time_suspended_ns ;
 368   struct dev_pm_qos_request *pq_req ;
 369   struct pm_subsys_data *subsys_data ;
 370   struct pm_qos_constraints *constraints ;
 371};
 372#line 558 "include/linux/pm.h"
 373struct dev_pm_domain {
 374   struct dev_pm_ops ops ;
 375};
 376#line 18 "include/asm-generic/pci_iomap.h"
 377struct vm_area_struct;
 378#line 18
 379struct vm_area_struct;
 380#line 18 "include/linux/elf.h"
 381typedef __u64 Elf64_Addr;
 382#line 19 "include/linux/elf.h"
 383typedef __u16 Elf64_Half;
 384#line 23 "include/linux/elf.h"
 385typedef __u32 Elf64_Word;
 386#line 24 "include/linux/elf.h"
 387typedef __u64 Elf64_Xword;
 388#line 193 "include/linux/elf.h"
 389struct elf64_sym {
 390   Elf64_Word st_name ;
 391   unsigned char st_info ;
 392   unsigned char st_other ;
 393   Elf64_Half st_shndx ;
 394   Elf64_Addr st_value ;
 395   Elf64_Xword st_size ;
 396};
 397#line 201 "include/linux/elf.h"
 398typedef struct elf64_sym Elf64_Sym;
 399#line 445
 400struct sock;
 401#line 445
 402struct sock;
 403#line 446
 404struct kobject;
 405#line 446
 406struct kobject;
 407#line 447
 408enum kobj_ns_type {
 409    KOBJ_NS_TYPE_NONE = 0,
 410    KOBJ_NS_TYPE_NET = 1,
 411    KOBJ_NS_TYPES = 2
 412} ;
 413#line 453 "include/linux/elf.h"
 414struct kobj_ns_type_operations {
 415   enum kobj_ns_type type ;
 416   void *(*grab_current_ns)(void) ;
 417   void const   *(*netlink_ns)(struct sock * ) ;
 418   void const   *(*initial_ns)(void) ;
 419   void (*drop_ns)(void * ) ;
 420};
 421#line 57 "include/linux/kobject_ns.h"
 422struct attribute {
 423   char const   *name ;
 424   umode_t mode ;
 425   struct lock_class_key *key ;
 426   struct lock_class_key skey ;
 427};
 428#line 33 "include/linux/sysfs.h"
 429struct attribute_group {
 430   char const   *name ;
 431   umode_t (*is_visible)(struct kobject * , struct attribute * , int  ) ;
 432   struct attribute **attrs ;
 433};
 434#line 62 "include/linux/sysfs.h"
 435struct bin_attribute {
 436   struct attribute attr ;
 437   size_t size ;
 438   void *private ;
 439   ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 440                   loff_t  , size_t  ) ;
 441   ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 442                    loff_t  , size_t  ) ;
 443   int (*mmap)(struct file * , struct kobject * , struct bin_attribute * , struct vm_area_struct * ) ;
 444};
 445#line 98 "include/linux/sysfs.h"
 446struct sysfs_ops {
 447   ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
 448   ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
 449   void const   *(*namespace)(struct kobject * , struct attribute  const  * ) ;
 450};
 451#line 117
 452struct sysfs_dirent;
 453#line 117
 454struct sysfs_dirent;
 455#line 182 "include/linux/sysfs.h"
 456struct kref {
 457   atomic_t refcount ;
 458};
 459#line 49 "include/linux/kobject.h"
 460struct kset;
 461#line 49
 462struct kobj_type;
 463#line 49 "include/linux/kobject.h"
 464struct kobject {
 465   char const   *name ;
 466   struct list_head entry ;
 467   struct kobject *parent ;
 468   struct kset *kset ;
 469   struct kobj_type *ktype ;
 470   struct sysfs_dirent *sd ;
 471   struct kref kref ;
 472   unsigned char state_initialized : 1 ;
 473   unsigned char state_in_sysfs : 1 ;
 474   unsigned char state_add_uevent_sent : 1 ;
 475   unsigned char state_remove_uevent_sent : 1 ;
 476   unsigned char uevent_suppress : 1 ;
 477};
 478#line 107 "include/linux/kobject.h"
 479struct kobj_type {
 480   void (*release)(struct kobject * ) ;
 481   struct sysfs_ops  const  *sysfs_ops ;
 482   struct attribute **default_attrs ;
 483   struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject * ) ;
 484   void const   *(*namespace)(struct kobject * ) ;
 485};
 486#line 115 "include/linux/kobject.h"
 487struct kobj_uevent_env {
 488   char *envp[32U] ;
 489   int envp_idx ;
 490   char buf[2048U] ;
 491   int buflen ;
 492};
 493#line 122 "include/linux/kobject.h"
 494struct kset_uevent_ops {
 495   int (* const  filter)(struct kset * , struct kobject * ) ;
 496   char const   *(* const  name)(struct kset * , struct kobject * ) ;
 497   int (* const  uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
 498};
 499#line 139 "include/linux/kobject.h"
 500struct kset {
 501   struct list_head list ;
 502   spinlock_t list_lock ;
 503   struct kobject kobj ;
 504   struct kset_uevent_ops  const  *uevent_ops ;
 505};
 506#line 215
 507struct kernel_param;
 508#line 215
 509struct kernel_param;
 510#line 216 "include/linux/kobject.h"
 511struct kernel_param_ops {
 512   int (*set)(char const   * , struct kernel_param  const  * ) ;
 513   int (*get)(char * , struct kernel_param  const  * ) ;
 514   void (*free)(void * ) ;
 515};
 516#line 49 "include/linux/moduleparam.h"
 517struct kparam_string;
 518#line 49
 519struct kparam_array;
 520#line 49 "include/linux/moduleparam.h"
 521union __anonunion_ldv_13363_134 {
 522   void *arg ;
 523   struct kparam_string  const  *str ;
 524   struct kparam_array  const  *arr ;
 525};
 526#line 49 "include/linux/moduleparam.h"
 527struct kernel_param {
 528   char const   *name ;
 529   struct kernel_param_ops  const  *ops ;
 530   u16 perm ;
 531   s16 level ;
 532   union __anonunion_ldv_13363_134 ldv_13363 ;
 533};
 534#line 61 "include/linux/moduleparam.h"
 535struct kparam_string {
 536   unsigned int maxlen ;
 537   char *string ;
 538};
 539#line 67 "include/linux/moduleparam.h"
 540struct kparam_array {
 541   unsigned int max ;
 542   unsigned int elemsize ;
 543   unsigned int *num ;
 544   struct kernel_param_ops  const  *ops ;
 545   void *elem ;
 546};
 547#line 458 "include/linux/moduleparam.h"
 548struct static_key {
 549   atomic_t enabled ;
 550};
 551#line 225 "include/linux/jump_label.h"
 552struct tracepoint;
 553#line 225
 554struct tracepoint;
 555#line 226 "include/linux/jump_label.h"
 556struct tracepoint_func {
 557   void *func ;
 558   void *data ;
 559};
 560#line 29 "include/linux/tracepoint.h"
 561struct tracepoint {
 562   char const   *name ;
 563   struct static_key key ;
 564   void (*regfunc)(void) ;
 565   void (*unregfunc)(void) ;
 566   struct tracepoint_func *funcs ;
 567};
 568#line 86 "include/linux/tracepoint.h"
 569struct kernel_symbol {
 570   unsigned long value ;
 571   char const   *name ;
 572};
 573#line 27 "include/linux/export.h"
 574struct mod_arch_specific {
 575
 576};
 577#line 34 "include/linux/module.h"
 578struct module_param_attrs;
 579#line 34 "include/linux/module.h"
 580struct module_kobject {
 581   struct kobject kobj ;
 582   struct module *mod ;
 583   struct kobject *drivers_dir ;
 584   struct module_param_attrs *mp ;
 585};
 586#line 43 "include/linux/module.h"
 587struct module_attribute {
 588   struct attribute attr ;
 589   ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
 590   ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const   * ,
 591                    size_t  ) ;
 592   void (*setup)(struct module * , char const   * ) ;
 593   int (*test)(struct module * ) ;
 594   void (*free)(struct module * ) ;
 595};
 596#line 69
 597struct exception_table_entry;
 598#line 69
 599struct exception_table_entry;
 600#line 198
 601enum module_state {
 602    MODULE_STATE_LIVE = 0,
 603    MODULE_STATE_COMING = 1,
 604    MODULE_STATE_GOING = 2
 605} ;
 606#line 204 "include/linux/module.h"
 607struct module_ref {
 608   unsigned long incs ;
 609   unsigned long decs ;
 610};
 611#line 219
 612struct module_sect_attrs;
 613#line 219
 614struct module_notes_attrs;
 615#line 219
 616struct ftrace_event_call;
 617#line 219 "include/linux/module.h"
 618struct module {
 619   enum module_state state ;
 620   struct list_head list ;
 621   char name[56U] ;
 622   struct module_kobject mkobj ;
 623   struct module_attribute *modinfo_attrs ;
 624   char const   *version ;
 625   char const   *srcversion ;
 626   struct kobject *holders_dir ;
 627   struct kernel_symbol  const  *syms ;
 628   unsigned long const   *crcs ;
 629   unsigned int num_syms ;
 630   struct kernel_param *kp ;
 631   unsigned int num_kp ;
 632   unsigned int num_gpl_syms ;
 633   struct kernel_symbol  const  *gpl_syms ;
 634   unsigned long const   *gpl_crcs ;
 635   struct kernel_symbol  const  *unused_syms ;
 636   unsigned long const   *unused_crcs ;
 637   unsigned int num_unused_syms ;
 638   unsigned int num_unused_gpl_syms ;
 639   struct kernel_symbol  const  *unused_gpl_syms ;
 640   unsigned long const   *unused_gpl_crcs ;
 641   struct kernel_symbol  const  *gpl_future_syms ;
 642   unsigned long const   *gpl_future_crcs ;
 643   unsigned int num_gpl_future_syms ;
 644   unsigned int num_exentries ;
 645   struct exception_table_entry *extable ;
 646   int (*init)(void) ;
 647   void *module_init ;
 648   void *module_core ;
 649   unsigned int init_size ;
 650   unsigned int core_size ;
 651   unsigned int init_text_size ;
 652   unsigned int core_text_size ;
 653   unsigned int init_ro_size ;
 654   unsigned int core_ro_size ;
 655   struct mod_arch_specific arch ;
 656   unsigned int taints ;
 657   unsigned int num_bugs ;
 658   struct list_head bug_list ;
 659   struct bug_entry *bug_table ;
 660   Elf64_Sym *symtab ;
 661   Elf64_Sym *core_symtab ;
 662   unsigned int num_symtab ;
 663   unsigned int core_num_syms ;
 664   char *strtab ;
 665   char *core_strtab ;
 666   struct module_sect_attrs *sect_attrs ;
 667   struct module_notes_attrs *notes_attrs ;
 668   char *args ;
 669   void *percpu ;
 670   unsigned int percpu_size ;
 671   unsigned int num_tracepoints ;
 672   struct tracepoint * const  *tracepoints_ptrs ;
 673   unsigned int num_trace_bprintk_fmt ;
 674   char const   **trace_bprintk_fmt_start ;
 675   struct ftrace_event_call **trace_events ;
 676   unsigned int num_trace_events ;
 677   struct list_head source_list ;
 678   struct list_head target_list ;
 679   struct task_struct *waiter ;
 680   void (*exit)(void) ;
 681   struct module_ref *refptr ;
 682   ctor_fn_t (**ctors)(void) ;
 683   unsigned int num_ctors ;
 684};
 685#line 88 "include/linux/kmemleak.h"
 686struct kmem_cache_cpu {
 687   void **freelist ;
 688   unsigned long tid ;
 689   struct page *page ;
 690   struct page *partial ;
 691   int node ;
 692   unsigned int stat[26U] ;
 693};
 694#line 55 "include/linux/slub_def.h"
 695struct kmem_cache_node {
 696   spinlock_t list_lock ;
 697   unsigned long nr_partial ;
 698   struct list_head partial ;
 699   atomic_long_t nr_slabs ;
 700   atomic_long_t total_objects ;
 701   struct list_head full ;
 702};
 703#line 66 "include/linux/slub_def.h"
 704struct kmem_cache_order_objects {
 705   unsigned long x ;
 706};
 707#line 76 "include/linux/slub_def.h"
 708struct kmem_cache {
 709   struct kmem_cache_cpu *cpu_slab ;
 710   unsigned long flags ;
 711   unsigned long min_partial ;
 712   int size ;
 713   int objsize ;
 714   int offset ;
 715   int cpu_partial ;
 716   struct kmem_cache_order_objects oo ;
 717   struct kmem_cache_order_objects max ;
 718   struct kmem_cache_order_objects min ;
 719   gfp_t allocflags ;
 720   int refcount ;
 721   void (*ctor)(void * ) ;
 722   int inuse ;
 723   int align ;
 724   int reserved ;
 725   char const   *name ;
 726   struct list_head list ;
 727   struct kobject kobj ;
 728   int remote_node_defrag_ratio ;
 729   struct kmem_cache_node *node[1024U] ;
 730};
 731#line 15 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12251/dscv_tempdir/dscv/ri/43_1a/drivers/regulator/userspace-consumer.c.p"
 732struct klist_node;
 733#line 15
 734struct klist_node;
 735#line 37 "include/linux/klist.h"
 736struct klist_node {
 737   void *n_klist ;
 738   struct list_head n_node ;
 739   struct kref n_ref ;
 740};
 741#line 67
 742struct dma_map_ops;
 743#line 67 "include/linux/klist.h"
 744struct dev_archdata {
 745   void *acpi_handle ;
 746   struct dma_map_ops *dma_ops ;
 747   void *iommu ;
 748};
 749#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 750struct pdev_archdata {
 751
 752};
 753#line 17
 754struct device_private;
 755#line 17
 756struct device_private;
 757#line 18
 758struct device_driver;
 759#line 18
 760struct device_driver;
 761#line 19
 762struct driver_private;
 763#line 19
 764struct driver_private;
 765#line 20
 766struct class;
 767#line 20
 768struct class;
 769#line 21
 770struct subsys_private;
 771#line 21
 772struct subsys_private;
 773#line 22
 774struct bus_type;
 775#line 22
 776struct bus_type;
 777#line 23
 778struct device_node;
 779#line 23
 780struct device_node;
 781#line 24
 782struct iommu_ops;
 783#line 24
 784struct iommu_ops;
 785#line 25 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 786struct bus_attribute {
 787   struct attribute attr ;
 788   ssize_t (*show)(struct bus_type * , char * ) ;
 789   ssize_t (*store)(struct bus_type * , char const   * , size_t  ) ;
 790};
 791#line 51 "include/linux/device.h"
 792struct device_attribute;
 793#line 51
 794struct driver_attribute;
 795#line 51 "include/linux/device.h"
 796struct bus_type {
 797   char const   *name ;
 798   char const   *dev_name ;
 799   struct device *dev_root ;
 800   struct bus_attribute *bus_attrs ;
 801   struct device_attribute *dev_attrs ;
 802   struct driver_attribute *drv_attrs ;
 803   int (*match)(struct device * , struct device_driver * ) ;
 804   int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
 805   int (*probe)(struct device * ) ;
 806   int (*remove)(struct device * ) ;
 807   void (*shutdown)(struct device * ) ;
 808   int (*suspend)(struct device * , pm_message_t  ) ;
 809   int (*resume)(struct device * ) ;
 810   struct dev_pm_ops  const  *pm ;
 811   struct iommu_ops *iommu_ops ;
 812   struct subsys_private *p ;
 813};
 814#line 125
 815struct device_type;
 816#line 182
 817struct of_device_id;
 818#line 182 "include/linux/device.h"
 819struct device_driver {
 820   char const   *name ;
 821   struct bus_type *bus ;
 822   struct module *owner ;
 823   char const   *mod_name ;
 824   bool suppress_bind_attrs ;
 825   struct of_device_id  const  *of_match_table ;
 826   int (*probe)(struct device * ) ;
 827   int (*remove)(struct device * ) ;
 828   void (*shutdown)(struct device * ) ;
 829   int (*suspend)(struct device * , pm_message_t  ) ;
 830   int (*resume)(struct device * ) ;
 831   struct attribute_group  const  **groups ;
 832   struct dev_pm_ops  const  *pm ;
 833   struct driver_private *p ;
 834};
 835#line 245 "include/linux/device.h"
 836struct driver_attribute {
 837   struct attribute attr ;
 838   ssize_t (*show)(struct device_driver * , char * ) ;
 839   ssize_t (*store)(struct device_driver * , char const   * , size_t  ) ;
 840};
 841#line 299
 842struct class_attribute;
 843#line 299 "include/linux/device.h"
 844struct class {
 845   char const   *name ;
 846   struct module *owner ;
 847   struct class_attribute *class_attrs ;
 848   struct device_attribute *dev_attrs ;
 849   struct bin_attribute *dev_bin_attrs ;
 850   struct kobject *dev_kobj ;
 851   int (*dev_uevent)(struct device * , struct kobj_uevent_env * ) ;
 852   char *(*devnode)(struct device * , umode_t * ) ;
 853   void (*class_release)(struct class * ) ;
 854   void (*dev_release)(struct device * ) ;
 855   int (*suspend)(struct device * , pm_message_t  ) ;
 856   int (*resume)(struct device * ) ;
 857   struct kobj_ns_type_operations  const  *ns_type ;
 858   void const   *(*namespace)(struct device * ) ;
 859   struct dev_pm_ops  const  *pm ;
 860   struct subsys_private *p ;
 861};
 862#line 394 "include/linux/device.h"
 863struct class_attribute {
 864   struct attribute attr ;
 865   ssize_t (*show)(struct class * , struct class_attribute * , char * ) ;
 866   ssize_t (*store)(struct class * , struct class_attribute * , char const   * , size_t  ) ;
 867   void const   *(*namespace)(struct class * , struct class_attribute  const  * ) ;
 868};
 869#line 447 "include/linux/device.h"
 870struct device_type {
 871   char const   *name ;
 872   struct attribute_group  const  **groups ;
 873   int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
 874   char *(*devnode)(struct device * , umode_t * ) ;
 875   void (*release)(struct device * ) ;
 876   struct dev_pm_ops  const  *pm ;
 877};
 878#line 474 "include/linux/device.h"
 879struct device_attribute {
 880   struct attribute attr ;
 881   ssize_t (*show)(struct device * , struct device_attribute * , char * ) ;
 882   ssize_t (*store)(struct device * , struct device_attribute * , char const   * ,
 883                    size_t  ) ;
 884};
 885#line 557 "include/linux/device.h"
 886struct device_dma_parameters {
 887   unsigned int max_segment_size ;
 888   unsigned long segment_boundary_mask ;
 889};
 890#line 567
 891struct dma_coherent_mem;
 892#line 567 "include/linux/device.h"
 893struct device {
 894   struct device *parent ;
 895   struct device_private *p ;
 896   struct kobject kobj ;
 897   char const   *init_name ;
 898   struct device_type  const  *type ;
 899   struct mutex mutex ;
 900   struct bus_type *bus ;
 901   struct device_driver *driver ;
 902   void *platform_data ;
 903   struct dev_pm_info power ;
 904   struct dev_pm_domain *pm_domain ;
 905   int numa_node ;
 906   u64 *dma_mask ;
 907   u64 coherent_dma_mask ;
 908   struct device_dma_parameters *dma_parms ;
 909   struct list_head dma_pools ;
 910   struct dma_coherent_mem *dma_mem ;
 911   struct dev_archdata archdata ;
 912   struct device_node *of_node ;
 913   dev_t devt ;
 914   u32 id ;
 915   spinlock_t devres_lock ;
 916   struct list_head devres_head ;
 917   struct klist_node knode_class ;
 918   struct class *class ;
 919   struct attribute_group  const  **groups ;
 920   void (*release)(struct device * ) ;
 921};
 922#line 681 "include/linux/device.h"
 923struct wakeup_source {
 924   char const   *name ;
 925   struct list_head entry ;
 926   spinlock_t lock ;
 927   struct timer_list timer ;
 928   unsigned long timer_expires ;
 929   ktime_t total_time ;
 930   ktime_t max_time ;
 931   ktime_t last_time ;
 932   unsigned long event_count ;
 933   unsigned long active_count ;
 934   unsigned long relax_count ;
 935   unsigned long hit_count ;
 936   unsigned char active : 1 ;
 937};
 938#line 12 "include/linux/mod_devicetable.h"
 939typedef unsigned long kernel_ulong_t;
 940#line 215 "include/linux/mod_devicetable.h"
 941struct of_device_id {
 942   char name[32U] ;
 943   char type[32U] ;
 944   char compatible[128U] ;
 945   void *data ;
 946};
 947#line 492 "include/linux/mod_devicetable.h"
 948struct platform_device_id {
 949   char name[20U] ;
 950   kernel_ulong_t driver_data ;
 951};
 952#line 584
 953struct mfd_cell;
 954#line 584
 955struct mfd_cell;
 956#line 585 "include/linux/mod_devicetable.h"
 957struct platform_device {
 958   char const   *name ;
 959   int id ;
 960   struct device dev ;
 961   u32 num_resources ;
 962   struct resource *resource ;
 963   struct platform_device_id  const  *id_entry ;
 964   struct mfd_cell *mfd_cell ;
 965   struct pdev_archdata archdata ;
 966};
 967#line 272 "include/linux/platform_device.h"
 968struct regulator;
 969#line 272
 970struct regulator;
 971#line 273 "include/linux/platform_device.h"
 972struct regulator_bulk_data {
 973   char const   *supply ;
 974   struct regulator *consumer ;
 975   int ret ;
 976};
 977#line 190 "include/linux/regulator/consumer.h"
 978struct regulator_userspace_consumer_data {
 979   char const   *name ;
 980   int num_supplies ;
 981   struct regulator_bulk_data *supplies ;
 982   bool init_on ;
 983};
 984#line 24 "include/linux/regulator/userspace-consumer.h"
 985struct userspace_consumer_data {
 986   char const   *name ;
 987   struct mutex lock ;
 988   bool enabled ;
 989   int num_supplies ;
 990   struct regulator_bulk_data *supplies ;
 991};
 992#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12251/dscv_tempdir/dscv/ri/43_1a/drivers/regulator/userspace-consumer.c.p"
 993void ldv_spin_lock(void) ;
 994#line 3
 995void ldv_spin_unlock(void) ;
 996#line 4
 997int ldv_spin_trylock(void) ;
 998#line 320 "include/linux/kernel.h"
 999extern int sprintf(char * , char const   *  , ...) ;
1000#line 126 "include/linux/string.h"
1001extern bool sysfs_streq(char const   * , char const   * ) ;
1002#line 115 "include/linux/mutex.h"
1003extern void __mutex_init(struct mutex * , char const   * , struct lock_class_key * ) ;
1004#line 134
1005extern void mutex_lock_nested(struct mutex * , unsigned int  ) ;
1006#line 169
1007extern void mutex_unlock(struct mutex * ) ;
1008#line 158 "include/linux/sysfs.h"
1009extern int sysfs_create_group(struct kobject * , struct attribute_group  const  * ) ;
1010#line 162
1011extern void sysfs_remove_group(struct kobject * , struct attribute_group  const  * ) ;
1012#line 161 "include/linux/slab.h"
1013extern void kfree(void const   * ) ;
1014#line 220 "include/linux/slub_def.h"
1015extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t  ) ;
1016#line 223
1017void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
1018#line 353 "include/linux/slab.h"
1019__inline static void *kzalloc(size_t size , gfp_t flags ) ;
1020#line 10 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12251/dscv_tempdir/dscv/ri/43_1a/drivers/regulator/userspace-consumer.c.p"
1021extern void *__VERIFIER_nondet_pointer(void) ;
1022#line 11
1023void ldv_check_alloc_flags(gfp_t flags ) ;
1024#line 12
1025void ldv_check_alloc_nonatomic(void) ;
1026#line 14
1027struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
1028#line 792 "include/linux/device.h"
1029extern void *dev_get_drvdata(struct device  const  * ) ;
1030#line 793
1031extern int dev_set_drvdata(struct device * , void * ) ;
1032#line 892
1033extern int dev_err(struct device  const  * , char const   *  , ...) ;
1034#line 183 "include/linux/platform_device.h"
1035__inline static void *platform_get_drvdata(struct platform_device  const  *pdev ) 
1036{ void *tmp ;
1037  unsigned long __cil_tmp3 ;
1038  unsigned long __cil_tmp4 ;
1039  struct device  const  *__cil_tmp5 ;
1040
1041  {
1042  {
1043#line 185
1044  __cil_tmp3 = (unsigned long )pdev;
1045#line 185
1046  __cil_tmp4 = __cil_tmp3 + 16;
1047#line 185
1048  __cil_tmp5 = (struct device  const  *)__cil_tmp4;
1049#line 185
1050  tmp = dev_get_drvdata(__cil_tmp5);
1051  }
1052#line 185
1053  return (tmp);
1054}
1055}
1056#line 188 "include/linux/platform_device.h"
1057__inline static void platform_set_drvdata(struct platform_device *pdev , void *data ) 
1058{ unsigned long __cil_tmp3 ;
1059  unsigned long __cil_tmp4 ;
1060  struct device *__cil_tmp5 ;
1061
1062  {
1063  {
1064#line 190
1065  __cil_tmp3 = (unsigned long )pdev;
1066#line 190
1067  __cil_tmp4 = __cil_tmp3 + 16;
1068#line 190
1069  __cil_tmp5 = (struct device *)__cil_tmp4;
1070#line 190
1071  dev_set_drvdata(__cil_tmp5, data);
1072  }
1073#line 191
1074  return;
1075}
1076}
1077#line 150 "include/linux/regulator/consumer.h"
1078extern int regulator_bulk_get(struct device * , int  , struct regulator_bulk_data * ) ;
1079#line 154
1080extern int regulator_bulk_enable(int  , struct regulator_bulk_data * ) ;
1081#line 156
1082extern int regulator_bulk_disable(int  , struct regulator_bulk_data * ) ;
1083#line 160
1084extern void regulator_bulk_free(int  , struct regulator_bulk_data * ) ;
1085#line 52 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12251/dscv_tempdir/dscv/ri/43_1a/drivers/regulator/userspace-consumer.c.p"
1086static ssize_t reg_show_name(struct device *dev , struct device_attribute *attr ,
1087                             char *buf ) 
1088{ struct userspace_consumer_data *data ;
1089  void *tmp ;
1090  int tmp___0 ;
1091  struct device  const  *__cil_tmp7 ;
1092  char const   *__cil_tmp8 ;
1093
1094  {
1095  {
1096#line 55
1097  __cil_tmp7 = (struct device  const  *)dev;
1098#line 55
1099  tmp = dev_get_drvdata(__cil_tmp7);
1100#line 55
1101  data = (struct userspace_consumer_data *)tmp;
1102#line 57
1103  __cil_tmp8 = *((char const   **)data);
1104#line 57
1105  tmp___0 = sprintf(buf, "%s\n", __cil_tmp8);
1106  }
1107#line 57
1108  return ((ssize_t )tmp___0);
1109}
1110}
1111#line 60 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12251/dscv_tempdir/dscv/ri/43_1a/drivers/regulator/userspace-consumer.c.p"
1112static ssize_t reg_show_state(struct device *dev , struct device_attribute *attr ,
1113                              char *buf ) 
1114{ struct userspace_consumer_data *data ;
1115  void *tmp ;
1116  int tmp___0 ;
1117  int tmp___1 ;
1118  struct device  const  *__cil_tmp8 ;
1119  unsigned long __cil_tmp9 ;
1120  unsigned long __cil_tmp10 ;
1121  bool __cil_tmp11 ;
1122
1123  {
1124  {
1125#line 63
1126  __cil_tmp8 = (struct device  const  *)dev;
1127#line 63
1128  tmp = dev_get_drvdata(__cil_tmp8);
1129#line 63
1130  data = (struct userspace_consumer_data *)tmp;
1131  }
1132  {
1133#line 65
1134  __cil_tmp9 = (unsigned long )data;
1135#line 65
1136  __cil_tmp10 = __cil_tmp9 + 176;
1137#line 65
1138  __cil_tmp11 = *((bool *)__cil_tmp10);
1139#line 65
1140  if ((int )__cil_tmp11) {
1141    {
1142#line 66
1143    tmp___0 = sprintf(buf, "enabled\n");
1144    }
1145#line 66
1146    return ((ssize_t )tmp___0);
1147  } else {
1148
1149  }
1150  }
1151  {
1152#line 68
1153  tmp___1 = sprintf(buf, "disabled\n");
1154  }
1155#line 68
1156  return ((ssize_t )tmp___1);
1157}
1158}
1159#line 71 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12251/dscv_tempdir/dscv/ri/43_1a/drivers/regulator/userspace-consumer.c.p"
1160static ssize_t reg_set_state(struct device *dev , struct device_attribute *attr ,
1161                             char const   *buf , size_t count ) 
1162{ struct userspace_consumer_data *data ;
1163  void *tmp ;
1164  bool enabled ;
1165  int ret ;
1166  bool tmp___0 ;
1167  bool tmp___1 ;
1168  bool tmp___2 ;
1169  bool tmp___3 ;
1170  struct device  const  *__cil_tmp13 ;
1171  struct device  const  *__cil_tmp14 ;
1172  unsigned long __cil_tmp15 ;
1173  unsigned long __cil_tmp16 ;
1174  struct mutex *__cil_tmp17 ;
1175  int __cil_tmp18 ;
1176  unsigned long __cil_tmp19 ;
1177  unsigned long __cil_tmp20 ;
1178  bool __cil_tmp21 ;
1179  int __cil_tmp22 ;
1180  unsigned long __cil_tmp23 ;
1181  unsigned long __cil_tmp24 ;
1182  int __cil_tmp25 ;
1183  unsigned long __cil_tmp26 ;
1184  unsigned long __cil_tmp27 ;
1185  struct regulator_bulk_data *__cil_tmp28 ;
1186  unsigned long __cil_tmp29 ;
1187  unsigned long __cil_tmp30 ;
1188  int __cil_tmp31 ;
1189  unsigned long __cil_tmp32 ;
1190  unsigned long __cil_tmp33 ;
1191  struct regulator_bulk_data *__cil_tmp34 ;
1192  unsigned long __cil_tmp35 ;
1193  unsigned long __cil_tmp36 ;
1194  struct device  const  *__cil_tmp37 ;
1195  unsigned long __cil_tmp38 ;
1196  unsigned long __cil_tmp39 ;
1197  struct mutex *__cil_tmp40 ;
1198
1199  {
1200  {
1201#line 74
1202  __cil_tmp13 = (struct device  const  *)dev;
1203#line 74
1204  tmp = dev_get_drvdata(__cil_tmp13);
1205#line 74
1206  data = (struct userspace_consumer_data *)tmp;
1207#line 82
1208  tmp___2 = sysfs_streq(buf, "enabled\n");
1209  }
1210#line 82
1211  if ((int )tmp___2) {
1212#line 83
1213    enabled = (bool )1;
1214  } else {
1215    {
1216#line 82
1217    tmp___3 = sysfs_streq(buf, "1");
1218    }
1219#line 82
1220    if ((int )tmp___3) {
1221#line 83
1222      enabled = (bool )1;
1223    } else {
1224      {
1225#line 84
1226      tmp___0 = sysfs_streq(buf, "disabled\n");
1227      }
1228#line 84
1229      if ((int )tmp___0) {
1230#line 85
1231        enabled = (bool )0;
1232      } else {
1233        {
1234#line 84
1235        tmp___1 = sysfs_streq(buf, "0");
1236        }
1237#line 84
1238        if ((int )tmp___1) {
1239#line 85
1240          enabled = (bool )0;
1241        } else {
1242          {
1243#line 87
1244          __cil_tmp14 = (struct device  const  *)dev;
1245#line 87
1246          dev_err(__cil_tmp14, "Configuring invalid mode\n");
1247          }
1248#line 88
1249          return ((ssize_t )count);
1250        }
1251      }
1252    }
1253  }
1254  {
1255#line 91
1256  __cil_tmp15 = (unsigned long )data;
1257#line 91
1258  __cil_tmp16 = __cil_tmp15 + 8;
1259#line 91
1260  __cil_tmp17 = (struct mutex *)__cil_tmp16;
1261#line 91
1262  mutex_lock_nested(__cil_tmp17, 0U);
1263  }
1264  {
1265#line 92
1266  __cil_tmp18 = (int )enabled;
1267#line 92
1268  __cil_tmp19 = (unsigned long )data;
1269#line 92
1270  __cil_tmp20 = __cil_tmp19 + 176;
1271#line 92
1272  __cil_tmp21 = *((bool *)__cil_tmp20);
1273#line 92
1274  __cil_tmp22 = (int )__cil_tmp21;
1275#line 92
1276  if (__cil_tmp22 != __cil_tmp18) {
1277#line 93
1278    if ((int )enabled) {
1279      {
1280#line 94
1281      __cil_tmp23 = (unsigned long )data;
1282#line 94
1283      __cil_tmp24 = __cil_tmp23 + 180;
1284#line 94
1285      __cil_tmp25 = *((int *)__cil_tmp24);
1286#line 94
1287      __cil_tmp26 = (unsigned long )data;
1288#line 94
1289      __cil_tmp27 = __cil_tmp26 + 184;
1290#line 94
1291      __cil_tmp28 = *((struct regulator_bulk_data **)__cil_tmp27);
1292#line 94
1293      ret = regulator_bulk_enable(__cil_tmp25, __cil_tmp28);
1294      }
1295    } else {
1296      {
1297#line 97
1298      __cil_tmp29 = (unsigned long )data;
1299#line 97
1300      __cil_tmp30 = __cil_tmp29 + 180;
1301#line 97
1302      __cil_tmp31 = *((int *)__cil_tmp30);
1303#line 97
1304      __cil_tmp32 = (unsigned long )data;
1305#line 97
1306      __cil_tmp33 = __cil_tmp32 + 184;
1307#line 97
1308      __cil_tmp34 = *((struct regulator_bulk_data **)__cil_tmp33);
1309#line 97
1310      ret = regulator_bulk_disable(__cil_tmp31, __cil_tmp34);
1311      }
1312    }
1313#line 100
1314    if (ret == 0) {
1315#line 101
1316      __cil_tmp35 = (unsigned long )data;
1317#line 101
1318      __cil_tmp36 = __cil_tmp35 + 176;
1319#line 101
1320      *((bool *)__cil_tmp36) = enabled;
1321    } else {
1322      {
1323#line 103
1324      __cil_tmp37 = (struct device  const  *)dev;
1325#line 103
1326      dev_err(__cil_tmp37, "Failed to configure state: %d\n", ret);
1327      }
1328    }
1329  } else {
1330
1331  }
1332  }
1333  {
1334#line 105
1335  __cil_tmp38 = (unsigned long )data;
1336#line 105
1337  __cil_tmp39 = __cil_tmp38 + 8;
1338#line 105
1339  __cil_tmp40 = (struct mutex *)__cil_tmp39;
1340#line 105
1341  mutex_unlock(__cil_tmp40);
1342  }
1343#line 107
1344  return ((ssize_t )count);
1345}
1346}
1347#line 110 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12251/dscv_tempdir/dscv/ri/43_1a/drivers/regulator/userspace-consumer.c.p"
1348static struct device_attribute dev_attr_name  =    {{"name", (umode_t )292U, (struct lock_class_key *)0, {{{(char)0}, {(char)0}, {(char)0},
1349                                                           {(char)0}, {(char)0}, {(char)0},
1350                                                           {(char)0}, {(char)0}}}},
1351    & reg_show_name, (ssize_t (*)(struct device * , struct device_attribute * , char const   * ,
1352                                  size_t  ))0};
1353#line 111 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12251/dscv_tempdir/dscv/ri/43_1a/drivers/regulator/userspace-consumer.c.p"
1354static struct device_attribute dev_attr_state  =    {{"state", (umode_t )420U, (struct lock_class_key *)0, {{{(char)0}, {(char)0},
1355                                                            {(char)0}, {(char)0},
1356                                                            {(char)0}, {(char)0},
1357                                                            {(char)0}, {(char)0}}}},
1358    & reg_show_state, & reg_set_state};
1359#line 113 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12251/dscv_tempdir/dscv/ri/43_1a/drivers/regulator/userspace-consumer.c.p"
1360static struct attribute *attributes[3U]  = {      & dev_attr_name.attr,      & dev_attr_state.attr,      (struct attribute *)0};
1361#line 119 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12251/dscv_tempdir/dscv/ri/43_1a/drivers/regulator/userspace-consumer.c.p"
1362static struct attribute_group  const  attr_group  =    {(char const   *)0, (umode_t (*)(struct kobject * , struct attribute * , int  ))0,
1363    (struct attribute **)(& attributes)};
1364#line 123 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12251/dscv_tempdir/dscv/ri/43_1a/drivers/regulator/userspace-consumer.c.p"
1365static int regulator_userspace_consumer_probe(struct platform_device *pdev ) 
1366{ struct regulator_userspace_consumer_data *pdata ;
1367  struct userspace_consumer_data *drvdata ;
1368  int ret ;
1369  void *tmp ;
1370  struct lock_class_key __key ;
1371  unsigned long __cil_tmp7 ;
1372  unsigned long __cil_tmp8 ;
1373  unsigned long __cil_tmp9 ;
1374  void *__cil_tmp10 ;
1375  struct regulator_userspace_consumer_data *__cil_tmp11 ;
1376  unsigned long __cil_tmp12 ;
1377  unsigned long __cil_tmp13 ;
1378  struct userspace_consumer_data *__cil_tmp14 ;
1379  unsigned long __cil_tmp15 ;
1380  unsigned long __cil_tmp16 ;
1381  unsigned long __cil_tmp17 ;
1382  unsigned long __cil_tmp18 ;
1383  unsigned long __cil_tmp19 ;
1384  unsigned long __cil_tmp20 ;
1385  unsigned long __cil_tmp21 ;
1386  unsigned long __cil_tmp22 ;
1387  unsigned long __cil_tmp23 ;
1388  unsigned long __cil_tmp24 ;
1389  unsigned long __cil_tmp25 ;
1390  unsigned long __cil_tmp26 ;
1391  struct mutex *__cil_tmp27 ;
1392  unsigned long __cil_tmp28 ;
1393  unsigned long __cil_tmp29 ;
1394  struct device *__cil_tmp30 ;
1395  unsigned long __cil_tmp31 ;
1396  unsigned long __cil_tmp32 ;
1397  int __cil_tmp33 ;
1398  unsigned long __cil_tmp34 ;
1399  unsigned long __cil_tmp35 ;
1400  struct regulator_bulk_data *__cil_tmp36 ;
1401  unsigned long __cil_tmp37 ;
1402  unsigned long __cil_tmp38 ;
1403  struct device *__cil_tmp39 ;
1404  struct device  const  *__cil_tmp40 ;
1405  unsigned long __cil_tmp41 ;
1406  unsigned long __cil_tmp42 ;
1407  unsigned long __cil_tmp43 ;
1408  struct kobject *__cil_tmp44 ;
1409  unsigned long __cil_tmp45 ;
1410  unsigned long __cil_tmp46 ;
1411  bool __cil_tmp47 ;
1412  unsigned long __cil_tmp48 ;
1413  unsigned long __cil_tmp49 ;
1414  int __cil_tmp50 ;
1415  unsigned long __cil_tmp51 ;
1416  unsigned long __cil_tmp52 ;
1417  struct regulator_bulk_data *__cil_tmp53 ;
1418  unsigned long __cil_tmp54 ;
1419  unsigned long __cil_tmp55 ;
1420  struct device *__cil_tmp56 ;
1421  struct device  const  *__cil_tmp57 ;
1422  unsigned long __cil_tmp58 ;
1423  unsigned long __cil_tmp59 ;
1424  unsigned long __cil_tmp60 ;
1425  unsigned long __cil_tmp61 ;
1426  void *__cil_tmp62 ;
1427  unsigned long __cil_tmp63 ;
1428  unsigned long __cil_tmp64 ;
1429  unsigned long __cil_tmp65 ;
1430  struct kobject *__cil_tmp66 ;
1431  unsigned long __cil_tmp67 ;
1432  unsigned long __cil_tmp68 ;
1433  int __cil_tmp69 ;
1434  unsigned long __cil_tmp70 ;
1435  unsigned long __cil_tmp71 ;
1436  struct regulator_bulk_data *__cil_tmp72 ;
1437  void const   *__cil_tmp73 ;
1438
1439  {
1440#line 129
1441  __cil_tmp7 = 16 + 280;
1442#line 129
1443  __cil_tmp8 = (unsigned long )pdev;
1444#line 129
1445  __cil_tmp9 = __cil_tmp8 + __cil_tmp7;
1446#line 129
1447  __cil_tmp10 = *((void **)__cil_tmp9);
1448#line 129
1449  pdata = (struct regulator_userspace_consumer_data *)__cil_tmp10;
1450  {
1451#line 130
1452  __cil_tmp11 = (struct regulator_userspace_consumer_data *)0;
1453#line 130
1454  __cil_tmp12 = (unsigned long )__cil_tmp11;
1455#line 130
1456  __cil_tmp13 = (unsigned long )pdata;
1457#line 130
1458  if (__cil_tmp13 == __cil_tmp12) {
1459#line 131
1460    return (-22);
1461  } else {
1462
1463  }
1464  }
1465  {
1466#line 133
1467  tmp = kzalloc(192UL, 208U);
1468#line 133
1469  drvdata = (struct userspace_consumer_data *)tmp;
1470  }
1471  {
1472#line 134
1473  __cil_tmp14 = (struct userspace_consumer_data *)0;
1474#line 134
1475  __cil_tmp15 = (unsigned long )__cil_tmp14;
1476#line 134
1477  __cil_tmp16 = (unsigned long )drvdata;
1478#line 134
1479  if (__cil_tmp16 == __cil_tmp15) {
1480#line 135
1481    return (-12);
1482  } else {
1483
1484  }
1485  }
1486  {
1487#line 137
1488  *((char const   **)drvdata) = *((char const   **)pdata);
1489#line 138
1490  __cil_tmp17 = (unsigned long )drvdata;
1491#line 138
1492  __cil_tmp18 = __cil_tmp17 + 180;
1493#line 138
1494  __cil_tmp19 = (unsigned long )pdata;
1495#line 138
1496  __cil_tmp20 = __cil_tmp19 + 8;
1497#line 138
1498  *((int *)__cil_tmp18) = *((int *)__cil_tmp20);
1499#line 139
1500  __cil_tmp21 = (unsigned long )drvdata;
1501#line 139
1502  __cil_tmp22 = __cil_tmp21 + 184;
1503#line 139
1504  __cil_tmp23 = (unsigned long )pdata;
1505#line 139
1506  __cil_tmp24 = __cil_tmp23 + 16;
1507#line 139
1508  *((struct regulator_bulk_data **)__cil_tmp22) = *((struct regulator_bulk_data **)__cil_tmp24);
1509#line 141
1510  __cil_tmp25 = (unsigned long )drvdata;
1511#line 141
1512  __cil_tmp26 = __cil_tmp25 + 8;
1513#line 141
1514  __cil_tmp27 = (struct mutex *)__cil_tmp26;
1515#line 141
1516  __mutex_init(__cil_tmp27, "&drvdata->lock", & __key);
1517#line 143
1518  __cil_tmp28 = (unsigned long )pdev;
1519#line 143
1520  __cil_tmp29 = __cil_tmp28 + 16;
1521#line 143
1522  __cil_tmp30 = (struct device *)__cil_tmp29;
1523#line 143
1524  __cil_tmp31 = (unsigned long )drvdata;
1525#line 143
1526  __cil_tmp32 = __cil_tmp31 + 180;
1527#line 143
1528  __cil_tmp33 = *((int *)__cil_tmp32);
1529#line 143
1530  __cil_tmp34 = (unsigned long )drvdata;
1531#line 143
1532  __cil_tmp35 = __cil_tmp34 + 184;
1533#line 143
1534  __cil_tmp36 = *((struct regulator_bulk_data **)__cil_tmp35);
1535#line 143
1536  ret = regulator_bulk_get(__cil_tmp30, __cil_tmp33, __cil_tmp36);
1537  }
1538#line 145
1539  if (ret != 0) {
1540    {
1541#line 146
1542    __cil_tmp37 = (unsigned long )pdev;
1543#line 146
1544    __cil_tmp38 = __cil_tmp37 + 16;
1545#line 146
1546    __cil_tmp39 = (struct device *)__cil_tmp38;
1547#line 146
1548    __cil_tmp40 = (struct device  const  *)__cil_tmp39;
1549#line 146
1550    dev_err(__cil_tmp40, "Failed to get supplies: %d\n", ret);
1551    }
1552#line 147
1553    goto err_alloc_supplies;
1554  } else {
1555
1556  }
1557  {
1558#line 150
1559  __cil_tmp41 = 16 + 16;
1560#line 150
1561  __cil_tmp42 = (unsigned long )pdev;
1562#line 150
1563  __cil_tmp43 = __cil_tmp42 + __cil_tmp41;
1564#line 150
1565  __cil_tmp44 = (struct kobject *)__cil_tmp43;
1566#line 150
1567  ret = sysfs_create_group(__cil_tmp44, & attr_group);
1568  }
1569#line 151
1570  if (ret != 0) {
1571#line 152
1572    goto err_create_attrs;
1573  } else {
1574
1575  }
1576  {
1577#line 154
1578  __cil_tmp45 = (unsigned long )pdata;
1579#line 154
1580  __cil_tmp46 = __cil_tmp45 + 24;
1581#line 154
1582  __cil_tmp47 = *((bool *)__cil_tmp46);
1583#line 154
1584  if ((int )__cil_tmp47) {
1585    {
1586#line 155
1587    __cil_tmp48 = (unsigned long )drvdata;
1588#line 155
1589    __cil_tmp49 = __cil_tmp48 + 180;
1590#line 155
1591    __cil_tmp50 = *((int *)__cil_tmp49);
1592#line 155
1593    __cil_tmp51 = (unsigned long )drvdata;
1594#line 155
1595    __cil_tmp52 = __cil_tmp51 + 184;
1596#line 155
1597    __cil_tmp53 = *((struct regulator_bulk_data **)__cil_tmp52);
1598#line 155
1599    ret = regulator_bulk_enable(__cil_tmp50, __cil_tmp53);
1600    }
1601#line 157
1602    if (ret != 0) {
1603      {
1604#line 158
1605      __cil_tmp54 = (unsigned long )pdev;
1606#line 158
1607      __cil_tmp55 = __cil_tmp54 + 16;
1608#line 158
1609      __cil_tmp56 = (struct device *)__cil_tmp55;
1610#line 158
1611      __cil_tmp57 = (struct device  const  *)__cil_tmp56;
1612#line 158
1613      dev_err(__cil_tmp57, "Failed to set initial state: %d\n", ret);
1614      }
1615#line 160
1616      goto err_enable;
1617    } else {
1618
1619    }
1620  } else {
1621
1622  }
1623  }
1624  {
1625#line 164
1626  __cil_tmp58 = (unsigned long )drvdata;
1627#line 164
1628  __cil_tmp59 = __cil_tmp58 + 176;
1629#line 164
1630  __cil_tmp60 = (unsigned long )pdata;
1631#line 164
1632  __cil_tmp61 = __cil_tmp60 + 24;
1633#line 164
1634  *((bool *)__cil_tmp59) = *((bool *)__cil_tmp61);
1635#line 165
1636  __cil_tmp62 = (void *)drvdata;
1637#line 165
1638  platform_set_drvdata(pdev, __cil_tmp62);
1639  }
1640#line 167
1641  return (0);
1642  err_enable: 
1643  {
1644#line 170
1645  __cil_tmp63 = 16 + 16;
1646#line 170
1647  __cil_tmp64 = (unsigned long )pdev;
1648#line 170
1649  __cil_tmp65 = __cil_tmp64 + __cil_tmp63;
1650#line 170
1651  __cil_tmp66 = (struct kobject *)__cil_tmp65;
1652#line 170
1653  sysfs_remove_group(__cil_tmp66, & attr_group);
1654  }
1655  err_create_attrs: 
1656  {
1657#line 173
1658  __cil_tmp67 = (unsigned long )drvdata;
1659#line 173
1660  __cil_tmp68 = __cil_tmp67 + 180;
1661#line 173
1662  __cil_tmp69 = *((int *)__cil_tmp68);
1663#line 173
1664  __cil_tmp70 = (unsigned long )drvdata;
1665#line 173
1666  __cil_tmp71 = __cil_tmp70 + 184;
1667#line 173
1668  __cil_tmp72 = *((struct regulator_bulk_data **)__cil_tmp71);
1669#line 173
1670  regulator_bulk_free(__cil_tmp69, __cil_tmp72);
1671  }
1672  err_alloc_supplies: 
1673  {
1674#line 176
1675  __cil_tmp73 = (void const   *)drvdata;
1676#line 176
1677  kfree(__cil_tmp73);
1678  }
1679#line 177
1680  return (ret);
1681}
1682}
1683#line 180 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12251/dscv_tempdir/dscv/ri/43_1a/drivers/regulator/userspace-consumer.c.p"
1684static int regulator_userspace_consumer_remove(struct platform_device *pdev ) 
1685{ struct userspace_consumer_data *data ;
1686  void *tmp ;
1687  struct platform_device  const  *__cil_tmp4 ;
1688  unsigned long __cil_tmp5 ;
1689  unsigned long __cil_tmp6 ;
1690  unsigned long __cil_tmp7 ;
1691  struct kobject *__cil_tmp8 ;
1692  unsigned long __cil_tmp9 ;
1693  unsigned long __cil_tmp10 ;
1694  bool __cil_tmp11 ;
1695  unsigned long __cil_tmp12 ;
1696  unsigned long __cil_tmp13 ;
1697  int __cil_tmp14 ;
1698  unsigned long __cil_tmp15 ;
1699  unsigned long __cil_tmp16 ;
1700  struct regulator_bulk_data *__cil_tmp17 ;
1701  unsigned long __cil_tmp18 ;
1702  unsigned long __cil_tmp19 ;
1703  int __cil_tmp20 ;
1704  unsigned long __cil_tmp21 ;
1705  unsigned long __cil_tmp22 ;
1706  struct regulator_bulk_data *__cil_tmp23 ;
1707  void const   *__cil_tmp24 ;
1708
1709  {
1710  {
1711#line 182
1712  __cil_tmp4 = (struct platform_device  const  *)pdev;
1713#line 182
1714  tmp = platform_get_drvdata(__cil_tmp4);
1715#line 182
1716  data = (struct userspace_consumer_data *)tmp;
1717#line 184
1718  __cil_tmp5 = 16 + 16;
1719#line 184
1720  __cil_tmp6 = (unsigned long )pdev;
1721#line 184
1722  __cil_tmp7 = __cil_tmp6 + __cil_tmp5;
1723#line 184
1724  __cil_tmp8 = (struct kobject *)__cil_tmp7;
1725#line 184
1726  sysfs_remove_group(__cil_tmp8, & attr_group);
1727  }
1728  {
1729#line 186
1730  __cil_tmp9 = (unsigned long )data;
1731#line 186
1732  __cil_tmp10 = __cil_tmp9 + 176;
1733#line 186
1734  __cil_tmp11 = *((bool *)__cil_tmp10);
1735#line 186
1736  if ((int )__cil_tmp11) {
1737    {
1738#line 187
1739    __cil_tmp12 = (unsigned long )data;
1740#line 187
1741    __cil_tmp13 = __cil_tmp12 + 180;
1742#line 187
1743    __cil_tmp14 = *((int *)__cil_tmp13);
1744#line 187
1745    __cil_tmp15 = (unsigned long )data;
1746#line 187
1747    __cil_tmp16 = __cil_tmp15 + 184;
1748#line 187
1749    __cil_tmp17 = *((struct regulator_bulk_data **)__cil_tmp16);
1750#line 187
1751    regulator_bulk_disable(__cil_tmp14, __cil_tmp17);
1752    }
1753  } else {
1754
1755  }
1756  }
1757  {
1758#line 189
1759  __cil_tmp18 = (unsigned long )data;
1760#line 189
1761  __cil_tmp19 = __cil_tmp18 + 180;
1762#line 189
1763  __cil_tmp20 = *((int *)__cil_tmp19);
1764#line 189
1765  __cil_tmp21 = (unsigned long )data;
1766#line 189
1767  __cil_tmp22 = __cil_tmp21 + 184;
1768#line 189
1769  __cil_tmp23 = *((struct regulator_bulk_data **)__cil_tmp22);
1770#line 189
1771  regulator_bulk_free(__cil_tmp20, __cil_tmp23);
1772#line 190
1773  __cil_tmp24 = (void const   *)data;
1774#line 190
1775  kfree(__cil_tmp24);
1776  }
1777#line 192
1778  return (0);
1779}
1780}
1781#line 225
1782extern void ldv_check_final_state(void) ;
1783#line 228
1784extern void ldv_check_return_value(int  ) ;
1785#line 231
1786extern void ldv_initialize(void) ;
1787#line 234
1788extern int __VERIFIER_nondet_int(void) ;
1789#line 237 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12251/dscv_tempdir/dscv/ri/43_1a/drivers/regulator/userspace-consumer.c.p"
1790int LDV_IN_INTERRUPT  ;
1791#line 240 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12251/dscv_tempdir/dscv/ri/43_1a/drivers/regulator/userspace-consumer.c.p"
1792void main(void) 
1793{ struct platform_device *var_group1 ;
1794  int res_regulator_userspace_consumer_probe_3 ;
1795  int ldv_s_regulator_userspace_consumer_driver_platform_driver ;
1796  int tmp ;
1797  int tmp___0 ;
1798
1799  {
1800  {
1801#line 272
1802  ldv_s_regulator_userspace_consumer_driver_platform_driver = 0;
1803#line 262
1804  LDV_IN_INTERRUPT = 1;
1805#line 271
1806  ldv_initialize();
1807  }
1808#line 275
1809  goto ldv_15454;
1810  ldv_15453: 
1811  {
1812#line 279
1813  tmp = __VERIFIER_nondet_int();
1814  }
1815#line 281
1816  if (tmp == 0) {
1817#line 281
1818    goto case_0;
1819  } else
1820#line 300
1821  if (tmp == 1) {
1822#line 300
1823    goto case_1;
1824  } else {
1825    {
1826#line 316
1827    goto switch_default;
1828#line 279
1829    if (0) {
1830      case_0: /* CIL Label */ ;
1831#line 284
1832      if (ldv_s_regulator_userspace_consumer_driver_platform_driver == 0) {
1833        {
1834#line 289
1835        res_regulator_userspace_consumer_probe_3 = regulator_userspace_consumer_probe(var_group1);
1836#line 290
1837        ldv_check_return_value(res_regulator_userspace_consumer_probe_3);
1838        }
1839#line 291
1840        if (res_regulator_userspace_consumer_probe_3 != 0) {
1841#line 292
1842          goto ldv_module_exit;
1843        } else {
1844
1845        }
1846#line 293
1847        ldv_s_regulator_userspace_consumer_driver_platform_driver = ldv_s_regulator_userspace_consumer_driver_platform_driver + 1;
1848      } else {
1849
1850      }
1851#line 299
1852      goto ldv_15450;
1853      case_1: /* CIL Label */ ;
1854#line 303
1855      if (ldv_s_regulator_userspace_consumer_driver_platform_driver == 1) {
1856        {
1857#line 308
1858        regulator_userspace_consumer_remove(var_group1);
1859#line 309
1860        ldv_s_regulator_userspace_consumer_driver_platform_driver = 0;
1861        }
1862      } else {
1863
1864      }
1865#line 315
1866      goto ldv_15450;
1867      switch_default: /* CIL Label */ ;
1868#line 316
1869      goto ldv_15450;
1870    } else {
1871      switch_break: /* CIL Label */ ;
1872    }
1873    }
1874  }
1875  ldv_15450: ;
1876  ldv_15454: 
1877  {
1878#line 275
1879  tmp___0 = __VERIFIER_nondet_int();
1880  }
1881#line 275
1882  if (tmp___0 != 0) {
1883#line 277
1884    goto ldv_15453;
1885  } else
1886#line 275
1887  if (ldv_s_regulator_userspace_consumer_driver_platform_driver != 0) {
1888#line 277
1889    goto ldv_15453;
1890  } else {
1891#line 279
1892    goto ldv_15455;
1893  }
1894  ldv_15455: ;
1895  ldv_module_exit: ;
1896  {
1897#line 325
1898  ldv_check_final_state();
1899  }
1900#line 328
1901  return;
1902}
1903}
1904#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12251/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
1905void ldv_blast_assert(void) 
1906{ 
1907
1908  {
1909  ERROR: ;
1910#line 6
1911  goto ERROR;
1912}
1913}
1914#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12251/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
1915extern int __VERIFIER_nondet_int(void) ;
1916#line 349 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12251/dscv_tempdir/dscv/ri/43_1a/drivers/regulator/userspace-consumer.c.p"
1917int ldv_spin  =    0;
1918#line 353 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12251/dscv_tempdir/dscv/ri/43_1a/drivers/regulator/userspace-consumer.c.p"
1919void ldv_check_alloc_flags(gfp_t flags ) 
1920{ 
1921
1922  {
1923#line 356
1924  if (ldv_spin != 0) {
1925#line 356
1926    if (flags != 32U) {
1927      {
1928#line 356
1929      ldv_blast_assert();
1930      }
1931    } else {
1932
1933    }
1934  } else {
1935
1936  }
1937#line 359
1938  return;
1939}
1940}
1941#line 359
1942extern struct page *ldv_some_page(void) ;
1943#line 362 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12251/dscv_tempdir/dscv/ri/43_1a/drivers/regulator/userspace-consumer.c.p"
1944struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) 
1945{ struct page *tmp ;
1946
1947  {
1948#line 365
1949  if (ldv_spin != 0) {
1950#line 365
1951    if (flags != 32U) {
1952      {
1953#line 365
1954      ldv_blast_assert();
1955      }
1956    } else {
1957
1958    }
1959  } else {
1960
1961  }
1962  {
1963#line 367
1964  tmp = ldv_some_page();
1965  }
1966#line 367
1967  return (tmp);
1968}
1969}
1970#line 371 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12251/dscv_tempdir/dscv/ri/43_1a/drivers/regulator/userspace-consumer.c.p"
1971void ldv_check_alloc_nonatomic(void) 
1972{ 
1973
1974  {
1975#line 374
1976  if (ldv_spin != 0) {
1977    {
1978#line 374
1979    ldv_blast_assert();
1980    }
1981  } else {
1982
1983  }
1984#line 377
1985  return;
1986}
1987}
1988#line 378 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12251/dscv_tempdir/dscv/ri/43_1a/drivers/regulator/userspace-consumer.c.p"
1989void ldv_spin_lock(void) 
1990{ 
1991
1992  {
1993#line 381
1994  ldv_spin = 1;
1995#line 382
1996  return;
1997}
1998}
1999#line 385 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12251/dscv_tempdir/dscv/ri/43_1a/drivers/regulator/userspace-consumer.c.p"
2000void ldv_spin_unlock(void) 
2001{ 
2002
2003  {
2004#line 388
2005  ldv_spin = 0;
2006#line 389
2007  return;
2008}
2009}
2010#line 392 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12251/dscv_tempdir/dscv/ri/43_1a/drivers/regulator/userspace-consumer.c.p"
2011int ldv_spin_trylock(void) 
2012{ int is_lock ;
2013
2014  {
2015  {
2016#line 397
2017  is_lock = __VERIFIER_nondet_int();
2018  }
2019#line 399
2020  if (is_lock != 0) {
2021#line 402
2022    return (0);
2023  } else {
2024#line 407
2025    ldv_spin = 1;
2026#line 409
2027    return (1);
2028  }
2029}
2030}
2031#line 576 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12251/dscv_tempdir/dscv/ri/43_1a/drivers/regulator/userspace-consumer.c.p"
2032void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) 
2033{ 
2034
2035  {
2036  {
2037#line 582
2038  ldv_check_alloc_flags(ldv_func_arg2);
2039#line 584
2040  kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
2041  }
2042#line 585
2043  return ((void *)0);
2044}
2045}
2046#line 587 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12251/dscv_tempdir/dscv/ri/43_1a/drivers/regulator/userspace-consumer.c.p"
2047__inline static void *kzalloc(size_t size , gfp_t flags ) 
2048{ void *tmp ;
2049
2050  {
2051  {
2052#line 593
2053  ldv_check_alloc_flags(flags);
2054#line 594
2055  tmp = __VERIFIER_nondet_pointer();
2056  }
2057#line 594
2058  return (tmp);
2059}
2060}