Showing error 726

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--w1--slaves--w1_bq27000.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 1527
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 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 56 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
  68struct module;
  69#line 56
  70struct module;
  71#line 146 "include/linux/init.h"
  72typedef void (*ctor_fn_t)(void);
  73#line 47 "include/linux/dynamic_debug.h"
  74struct device;
  75#line 47
  76struct device;
  77#line 135 "include/linux/kernel.h"
  78struct completion;
  79#line 135
  80struct completion;
  81#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
  82struct task_struct;
  83#line 20
  84struct task_struct;
  85#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
  86struct task_struct;
  87#line 295 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
  88struct file;
  89#line 295
  90struct file;
  91#line 52 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
  92struct task_struct;
  93#line 329
  94struct arch_spinlock;
  95#line 329
  96struct arch_spinlock;
  97#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
  98struct task_struct;
  99#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
 100struct task_struct;
 101#line 10 "include/asm-generic/bug.h"
 102struct bug_entry {
 103   int bug_addr_disp ;
 104   int file_disp ;
 105   unsigned short line ;
 106   unsigned short flags ;
 107};
 108#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
 109struct static_key;
 110#line 234
 111struct static_key;
 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 20 "/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 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 124union __anonunion____missing_field_name_36 {
 125   __ticketpair_t head_tail ;
 126   struct __raw_tickets tickets ;
 127};
 128#line 20 "/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____missing_field_name_36 __annonCompField17 ;
 131};
 132#line 20 "/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 12 "include/linux/lockdep.h"
 135struct task_struct;
 136#line 20 "include/linux/spinlock_types.h"
 137struct raw_spinlock {
 138   arch_spinlock_t raw_lock ;
 139   unsigned int magic ;
 140   unsigned int owner_cpu ;
 141   void *owner ;
 142};
 143#line 64 "include/linux/spinlock_types.h"
 144union __anonunion____missing_field_name_39 {
 145   struct raw_spinlock rlock ;
 146};
 147#line 64 "include/linux/spinlock_types.h"
 148struct spinlock {
 149   union __anonunion____missing_field_name_39 __annonCompField19 ;
 150};
 151#line 64 "include/linux/spinlock_types.h"
 152typedef struct spinlock spinlock_t;
 153#line 49 "include/linux/wait.h"
 154struct __wait_queue_head {
 155   spinlock_t lock ;
 156   struct list_head task_list ;
 157};
 158#line 53 "include/linux/wait.h"
 159typedef struct __wait_queue_head wait_queue_head_t;
 160#line 55
 161struct task_struct;
 162#line 48 "include/linux/mutex.h"
 163struct mutex {
 164   atomic_t count ;
 165   spinlock_t wait_lock ;
 166   struct list_head wait_list ;
 167   struct task_struct *owner ;
 168   char const   *name ;
 169   void *magic ;
 170};
 171#line 25 "include/linux/completion.h"
 172struct completion {
 173   unsigned int done ;
 174   wait_queue_head_t wait ;
 175};
 176#line 18 "include/linux/ioport.h"
 177struct resource {
 178   resource_size_t start ;
 179   resource_size_t end ;
 180   char const   *name ;
 181   unsigned long flags ;
 182   struct resource *parent ;
 183   struct resource *sibling ;
 184   struct resource *child ;
 185};
 186#line 202
 187struct device;
 188#line 103 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mpspec.h"
 189struct device;
 190#line 46 "include/linux/ktime.h"
 191union ktime {
 192   s64 tv64 ;
 193};
 194#line 59 "include/linux/ktime.h"
 195typedef union ktime ktime_t;
 196#line 10 "include/linux/timer.h"
 197struct tvec_base;
 198#line 10
 199struct tvec_base;
 200#line 12 "include/linux/timer.h"
 201struct timer_list {
 202   struct list_head entry ;
 203   unsigned long expires ;
 204   struct tvec_base *base ;
 205   void (*function)(unsigned long  ) ;
 206   unsigned long data ;
 207   int slack ;
 208   int start_pid ;
 209   void *start_site ;
 210   char start_comm[16] ;
 211};
 212#line 17 "include/linux/workqueue.h"
 213struct work_struct;
 214#line 17
 215struct work_struct;
 216#line 79 "include/linux/workqueue.h"
 217struct work_struct {
 218   atomic_long_t data ;
 219   struct list_head entry ;
 220   void (*func)(struct work_struct *work ) ;
 221};
 222#line 42 "include/linux/pm.h"
 223struct device;
 224#line 50 "include/linux/pm.h"
 225struct pm_message {
 226   int event ;
 227};
 228#line 50 "include/linux/pm.h"
 229typedef struct pm_message pm_message_t;
 230#line 264 "include/linux/pm.h"
 231struct dev_pm_ops {
 232   int (*prepare)(struct device *dev ) ;
 233   void (*complete)(struct device *dev ) ;
 234   int (*suspend)(struct device *dev ) ;
 235   int (*resume)(struct device *dev ) ;
 236   int (*freeze)(struct device *dev ) ;
 237   int (*thaw)(struct device *dev ) ;
 238   int (*poweroff)(struct device *dev ) ;
 239   int (*restore)(struct device *dev ) ;
 240   int (*suspend_late)(struct device *dev ) ;
 241   int (*resume_early)(struct device *dev ) ;
 242   int (*freeze_late)(struct device *dev ) ;
 243   int (*thaw_early)(struct device *dev ) ;
 244   int (*poweroff_late)(struct device *dev ) ;
 245   int (*restore_early)(struct device *dev ) ;
 246   int (*suspend_noirq)(struct device *dev ) ;
 247   int (*resume_noirq)(struct device *dev ) ;
 248   int (*freeze_noirq)(struct device *dev ) ;
 249   int (*thaw_noirq)(struct device *dev ) ;
 250   int (*poweroff_noirq)(struct device *dev ) ;
 251   int (*restore_noirq)(struct device *dev ) ;
 252   int (*runtime_suspend)(struct device *dev ) ;
 253   int (*runtime_resume)(struct device *dev ) ;
 254   int (*runtime_idle)(struct device *dev ) ;
 255};
 256#line 458
 257enum rpm_status {
 258    RPM_ACTIVE = 0,
 259    RPM_RESUMING = 1,
 260    RPM_SUSPENDED = 2,
 261    RPM_SUSPENDING = 3
 262} ;
 263#line 480
 264enum rpm_request {
 265    RPM_REQ_NONE = 0,
 266    RPM_REQ_IDLE = 1,
 267    RPM_REQ_SUSPEND = 2,
 268    RPM_REQ_AUTOSUSPEND = 3,
 269    RPM_REQ_RESUME = 4
 270} ;
 271#line 488
 272struct wakeup_source;
 273#line 488
 274struct wakeup_source;
 275#line 495 "include/linux/pm.h"
 276struct pm_subsys_data {
 277   spinlock_t lock ;
 278   unsigned int refcount ;
 279};
 280#line 506
 281struct dev_pm_qos_request;
 282#line 506
 283struct pm_qos_constraints;
 284#line 506 "include/linux/pm.h"
 285struct dev_pm_info {
 286   pm_message_t power_state ;
 287   unsigned int can_wakeup : 1 ;
 288   unsigned int async_suspend : 1 ;
 289   bool is_prepared : 1 ;
 290   bool is_suspended : 1 ;
 291   bool ignore_children : 1 ;
 292   spinlock_t lock ;
 293   struct list_head entry ;
 294   struct completion completion ;
 295   struct wakeup_source *wakeup ;
 296   bool wakeup_path : 1 ;
 297   struct timer_list suspend_timer ;
 298   unsigned long timer_expires ;
 299   struct work_struct work ;
 300   wait_queue_head_t wait_queue ;
 301   atomic_t usage_count ;
 302   atomic_t child_count ;
 303   unsigned int disable_depth : 3 ;
 304   unsigned int idle_notification : 1 ;
 305   unsigned int request_pending : 1 ;
 306   unsigned int deferred_resume : 1 ;
 307   unsigned int run_wake : 1 ;
 308   unsigned int runtime_auto : 1 ;
 309   unsigned int no_callbacks : 1 ;
 310   unsigned int irq_safe : 1 ;
 311   unsigned int use_autosuspend : 1 ;
 312   unsigned int timer_autosuspends : 1 ;
 313   enum rpm_request request ;
 314   enum rpm_status runtime_status ;
 315   int runtime_error ;
 316   int autosuspend_delay ;
 317   unsigned long last_busy ;
 318   unsigned long active_jiffies ;
 319   unsigned long suspended_jiffies ;
 320   unsigned long accounting_timestamp ;
 321   ktime_t suspend_time ;
 322   s64 max_time_suspended_ns ;
 323   struct dev_pm_qos_request *pq_req ;
 324   struct pm_subsys_data *subsys_data ;
 325   struct pm_qos_constraints *constraints ;
 326};
 327#line 564 "include/linux/pm.h"
 328struct dev_pm_domain {
 329   struct dev_pm_ops ops ;
 330};
 331#line 8 "include/linux/vmalloc.h"
 332struct vm_area_struct;
 333#line 8
 334struct vm_area_struct;
 335#line 10 "include/linux/gfp.h"
 336struct vm_area_struct;
 337#line 29 "include/linux/sysctl.h"
 338struct completion;
 339#line 49 "include/linux/kmod.h"
 340struct file;
 341#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
 342struct task_struct;
 343#line 18 "include/linux/elf.h"
 344typedef __u64 Elf64_Addr;
 345#line 19 "include/linux/elf.h"
 346typedef __u16 Elf64_Half;
 347#line 23 "include/linux/elf.h"
 348typedef __u32 Elf64_Word;
 349#line 24 "include/linux/elf.h"
 350typedef __u64 Elf64_Xword;
 351#line 194 "include/linux/elf.h"
 352struct elf64_sym {
 353   Elf64_Word st_name ;
 354   unsigned char st_info ;
 355   unsigned char st_other ;
 356   Elf64_Half st_shndx ;
 357   Elf64_Addr st_value ;
 358   Elf64_Xword st_size ;
 359};
 360#line 194 "include/linux/elf.h"
 361typedef struct elf64_sym Elf64_Sym;
 362#line 438
 363struct file;
 364#line 20 "include/linux/kobject_ns.h"
 365struct sock;
 366#line 20
 367struct sock;
 368#line 21
 369struct kobject;
 370#line 21
 371struct kobject;
 372#line 27
 373enum kobj_ns_type {
 374    KOBJ_NS_TYPE_NONE = 0,
 375    KOBJ_NS_TYPE_NET = 1,
 376    KOBJ_NS_TYPES = 2
 377} ;
 378#line 40 "include/linux/kobject_ns.h"
 379struct kobj_ns_type_operations {
 380   enum kobj_ns_type type ;
 381   void *(*grab_current_ns)(void) ;
 382   void const   *(*netlink_ns)(struct sock *sk ) ;
 383   void const   *(*initial_ns)(void) ;
 384   void (*drop_ns)(void * ) ;
 385};
 386#line 22 "include/linux/sysfs.h"
 387struct kobject;
 388#line 23
 389struct module;
 390#line 24
 391enum kobj_ns_type;
 392#line 26 "include/linux/sysfs.h"
 393struct attribute {
 394   char const   *name ;
 395   umode_t mode ;
 396};
 397#line 56 "include/linux/sysfs.h"
 398struct attribute_group {
 399   char const   *name ;
 400   umode_t (*is_visible)(struct kobject * , struct attribute * , int  ) ;
 401   struct attribute **attrs ;
 402};
 403#line 85
 404struct file;
 405#line 86
 406struct vm_area_struct;
 407#line 88 "include/linux/sysfs.h"
 408struct bin_attribute {
 409   struct attribute attr ;
 410   size_t size ;
 411   void *private ;
 412   ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 413                   loff_t  , size_t  ) ;
 414   ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 415                    loff_t  , size_t  ) ;
 416   int (*mmap)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ) ;
 417};
 418#line 112 "include/linux/sysfs.h"
 419struct sysfs_ops {
 420   ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
 421   ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
 422   void const   *(*namespace)(struct kobject * , struct attribute  const  * ) ;
 423};
 424#line 118
 425struct sysfs_dirent;
 426#line 118
 427struct sysfs_dirent;
 428#line 22 "include/linux/kref.h"
 429struct kref {
 430   atomic_t refcount ;
 431};
 432#line 60 "include/linux/kobject.h"
 433struct kset;
 434#line 60
 435struct kobj_type;
 436#line 60 "include/linux/kobject.h"
 437struct kobject {
 438   char const   *name ;
 439   struct list_head entry ;
 440   struct kobject *parent ;
 441   struct kset *kset ;
 442   struct kobj_type *ktype ;
 443   struct sysfs_dirent *sd ;
 444   struct kref kref ;
 445   unsigned int state_initialized : 1 ;
 446   unsigned int state_in_sysfs : 1 ;
 447   unsigned int state_add_uevent_sent : 1 ;
 448   unsigned int state_remove_uevent_sent : 1 ;
 449   unsigned int uevent_suppress : 1 ;
 450};
 451#line 108 "include/linux/kobject.h"
 452struct kobj_type {
 453   void (*release)(struct kobject *kobj ) ;
 454   struct sysfs_ops  const  *sysfs_ops ;
 455   struct attribute **default_attrs ;
 456   struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject *kobj ) ;
 457   void const   *(*namespace)(struct kobject *kobj ) ;
 458};
 459#line 116 "include/linux/kobject.h"
 460struct kobj_uevent_env {
 461   char *envp[32] ;
 462   int envp_idx ;
 463   char buf[2048] ;
 464   int buflen ;
 465};
 466#line 123 "include/linux/kobject.h"
 467struct kset_uevent_ops {
 468   int (* const  filter)(struct kset *kset , struct kobject *kobj ) ;
 469   char const   *(* const  name)(struct kset *kset , struct kobject *kobj ) ;
 470   int (* const  uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
 471};
 472#line 140
 473struct sock;
 474#line 159 "include/linux/kobject.h"
 475struct kset {
 476   struct list_head list ;
 477   spinlock_t list_lock ;
 478   struct kobject kobj ;
 479   struct kset_uevent_ops  const  *uevent_ops ;
 480};
 481#line 39 "include/linux/moduleparam.h"
 482struct kernel_param;
 483#line 39
 484struct kernel_param;
 485#line 41 "include/linux/moduleparam.h"
 486struct kernel_param_ops {
 487   int (*set)(char const   *val , struct kernel_param  const  *kp ) ;
 488   int (*get)(char *buffer , struct kernel_param  const  *kp ) ;
 489   void (*free)(void *arg ) ;
 490};
 491#line 50
 492struct kparam_string;
 493#line 50
 494struct kparam_array;
 495#line 50 "include/linux/moduleparam.h"
 496union __anonunion____missing_field_name_199 {
 497   void *arg ;
 498   struct kparam_string  const  *str ;
 499   struct kparam_array  const  *arr ;
 500};
 501#line 50 "include/linux/moduleparam.h"
 502struct kernel_param {
 503   char const   *name ;
 504   struct kernel_param_ops  const  *ops ;
 505   u16 perm ;
 506   s16 level ;
 507   union __anonunion____missing_field_name_199 __annonCompField32 ;
 508};
 509#line 63 "include/linux/moduleparam.h"
 510struct kparam_string {
 511   unsigned int maxlen ;
 512   char *string ;
 513};
 514#line 69 "include/linux/moduleparam.h"
 515struct kparam_array {
 516   unsigned int max ;
 517   unsigned int elemsize ;
 518   unsigned int *num ;
 519   struct kernel_param_ops  const  *ops ;
 520   void *elem ;
 521};
 522#line 445
 523struct module;
 524#line 80 "include/linux/jump_label.h"
 525struct module;
 526#line 143 "include/linux/jump_label.h"
 527struct static_key {
 528   atomic_t enabled ;
 529};
 530#line 22 "include/linux/tracepoint.h"
 531struct module;
 532#line 23
 533struct tracepoint;
 534#line 23
 535struct tracepoint;
 536#line 25 "include/linux/tracepoint.h"
 537struct tracepoint_func {
 538   void *func ;
 539   void *data ;
 540};
 541#line 30 "include/linux/tracepoint.h"
 542struct tracepoint {
 543   char const   *name ;
 544   struct static_key key ;
 545   void (*regfunc)(void) ;
 546   void (*unregfunc)(void) ;
 547   struct tracepoint_func *funcs ;
 548};
 549#line 19 "include/linux/export.h"
 550struct kernel_symbol {
 551   unsigned long value ;
 552   char const   *name ;
 553};
 554#line 8 "include/asm-generic/module.h"
 555struct mod_arch_specific {
 556
 557};
 558#line 35 "include/linux/module.h"
 559struct module;
 560#line 37
 561struct module_param_attrs;
 562#line 37 "include/linux/module.h"
 563struct module_kobject {
 564   struct kobject kobj ;
 565   struct module *mod ;
 566   struct kobject *drivers_dir ;
 567   struct module_param_attrs *mp ;
 568};
 569#line 44 "include/linux/module.h"
 570struct module_attribute {
 571   struct attribute attr ;
 572   ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
 573   ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const   * ,
 574                    size_t count ) ;
 575   void (*setup)(struct module * , char const   * ) ;
 576   int (*test)(struct module * ) ;
 577   void (*free)(struct module * ) ;
 578};
 579#line 71
 580struct exception_table_entry;
 581#line 71
 582struct exception_table_entry;
 583#line 199
 584enum module_state {
 585    MODULE_STATE_LIVE = 0,
 586    MODULE_STATE_COMING = 1,
 587    MODULE_STATE_GOING = 2
 588} ;
 589#line 215 "include/linux/module.h"
 590struct module_ref {
 591   unsigned long incs ;
 592   unsigned long decs ;
 593} __attribute__((__aligned__((2) *  (sizeof(unsigned long )) ))) ;
 594#line 220
 595struct module_sect_attrs;
 596#line 220
 597struct module_notes_attrs;
 598#line 220
 599struct ftrace_event_call;
 600#line 220 "include/linux/module.h"
 601struct module {
 602   enum module_state state ;
 603   struct list_head list ;
 604   char name[64UL - sizeof(unsigned long )] ;
 605   struct module_kobject mkobj ;
 606   struct module_attribute *modinfo_attrs ;
 607   char const   *version ;
 608   char const   *srcversion ;
 609   struct kobject *holders_dir ;
 610   struct kernel_symbol  const  *syms ;
 611   unsigned long const   *crcs ;
 612   unsigned int num_syms ;
 613   struct kernel_param *kp ;
 614   unsigned int num_kp ;
 615   unsigned int num_gpl_syms ;
 616   struct kernel_symbol  const  *gpl_syms ;
 617   unsigned long const   *gpl_crcs ;
 618   struct kernel_symbol  const  *unused_syms ;
 619   unsigned long const   *unused_crcs ;
 620   unsigned int num_unused_syms ;
 621   unsigned int num_unused_gpl_syms ;
 622   struct kernel_symbol  const  *unused_gpl_syms ;
 623   unsigned long const   *unused_gpl_crcs ;
 624   struct kernel_symbol  const  *gpl_future_syms ;
 625   unsigned long const   *gpl_future_crcs ;
 626   unsigned int num_gpl_future_syms ;
 627   unsigned int num_exentries ;
 628   struct exception_table_entry *extable ;
 629   int (*init)(void) ;
 630   void *module_init ;
 631   void *module_core ;
 632   unsigned int init_size ;
 633   unsigned int core_size ;
 634   unsigned int init_text_size ;
 635   unsigned int core_text_size ;
 636   unsigned int init_ro_size ;
 637   unsigned int core_ro_size ;
 638   struct mod_arch_specific arch ;
 639   unsigned int taints ;
 640   unsigned int num_bugs ;
 641   struct list_head bug_list ;
 642   struct bug_entry *bug_table ;
 643   Elf64_Sym *symtab ;
 644   Elf64_Sym *core_symtab ;
 645   unsigned int num_symtab ;
 646   unsigned int core_num_syms ;
 647   char *strtab ;
 648   char *core_strtab ;
 649   struct module_sect_attrs *sect_attrs ;
 650   struct module_notes_attrs *notes_attrs ;
 651   char *args ;
 652   void *percpu ;
 653   unsigned int percpu_size ;
 654   unsigned int num_tracepoints ;
 655   struct tracepoint * const  *tracepoints_ptrs ;
 656   unsigned int num_trace_bprintk_fmt ;
 657   char const   **trace_bprintk_fmt_start ;
 658   struct ftrace_event_call **trace_events ;
 659   unsigned int num_trace_events ;
 660   struct list_head source_list ;
 661   struct list_head target_list ;
 662   struct task_struct *waiter ;
 663   void (*exit)(void) ;
 664   struct module_ref *refptr ;
 665   ctor_fn_t *ctors ;
 666   unsigned int num_ctors ;
 667};
 668#line 19 "include/linux/klist.h"
 669struct klist_node;
 670#line 19
 671struct klist_node;
 672#line 39 "include/linux/klist.h"
 673struct klist_node {
 674   void *n_klist ;
 675   struct list_head n_node ;
 676   struct kref n_ref ;
 677};
 678#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 679struct dma_map_ops;
 680#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 681struct dev_archdata {
 682   void *acpi_handle ;
 683   struct dma_map_ops *dma_ops ;
 684   void *iommu ;
 685};
 686#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 687struct pdev_archdata {
 688
 689};
 690#line 28 "include/linux/device.h"
 691struct device;
 692#line 29
 693struct device_private;
 694#line 29
 695struct device_private;
 696#line 30
 697struct device_driver;
 698#line 30
 699struct device_driver;
 700#line 31
 701struct driver_private;
 702#line 31
 703struct driver_private;
 704#line 32
 705struct module;
 706#line 33
 707struct class;
 708#line 33
 709struct class;
 710#line 34
 711struct subsys_private;
 712#line 34
 713struct subsys_private;
 714#line 35
 715struct bus_type;
 716#line 35
 717struct bus_type;
 718#line 36
 719struct device_node;
 720#line 36
 721struct device_node;
 722#line 37
 723struct iommu_ops;
 724#line 37
 725struct iommu_ops;
 726#line 39 "include/linux/device.h"
 727struct bus_attribute {
 728   struct attribute attr ;
 729   ssize_t (*show)(struct bus_type *bus , char *buf ) ;
 730   ssize_t (*store)(struct bus_type *bus , char const   *buf , size_t count ) ;
 731};
 732#line 89
 733struct device_attribute;
 734#line 89
 735struct driver_attribute;
 736#line 89 "include/linux/device.h"
 737struct bus_type {
 738   char const   *name ;
 739   char const   *dev_name ;
 740   struct device *dev_root ;
 741   struct bus_attribute *bus_attrs ;
 742   struct device_attribute *dev_attrs ;
 743   struct driver_attribute *drv_attrs ;
 744   int (*match)(struct device *dev , struct device_driver *drv ) ;
 745   int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
 746   int (*probe)(struct device *dev ) ;
 747   int (*remove)(struct device *dev ) ;
 748   void (*shutdown)(struct device *dev ) ;
 749   int (*suspend)(struct device *dev , pm_message_t state ) ;
 750   int (*resume)(struct device *dev ) ;
 751   struct dev_pm_ops  const  *pm ;
 752   struct iommu_ops *iommu_ops ;
 753   struct subsys_private *p ;
 754};
 755#line 127
 756struct device_type;
 757#line 214
 758struct of_device_id;
 759#line 214 "include/linux/device.h"
 760struct device_driver {
 761   char const   *name ;
 762   struct bus_type *bus ;
 763   struct module *owner ;
 764   char const   *mod_name ;
 765   bool suppress_bind_attrs ;
 766   struct of_device_id  const  *of_match_table ;
 767   int (*probe)(struct device *dev ) ;
 768   int (*remove)(struct device *dev ) ;
 769   void (*shutdown)(struct device *dev ) ;
 770   int (*suspend)(struct device *dev , pm_message_t state ) ;
 771   int (*resume)(struct device *dev ) ;
 772   struct attribute_group  const  **groups ;
 773   struct dev_pm_ops  const  *pm ;
 774   struct driver_private *p ;
 775};
 776#line 249 "include/linux/device.h"
 777struct driver_attribute {
 778   struct attribute attr ;
 779   ssize_t (*show)(struct device_driver *driver , char *buf ) ;
 780   ssize_t (*store)(struct device_driver *driver , char const   *buf , size_t count ) ;
 781};
 782#line 330
 783struct class_attribute;
 784#line 330 "include/linux/device.h"
 785struct class {
 786   char const   *name ;
 787   struct module *owner ;
 788   struct class_attribute *class_attrs ;
 789   struct device_attribute *dev_attrs ;
 790   struct bin_attribute *dev_bin_attrs ;
 791   struct kobject *dev_kobj ;
 792   int (*dev_uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
 793   char *(*devnode)(struct device *dev , umode_t *mode ) ;
 794   void (*class_release)(struct class *class ) ;
 795   void (*dev_release)(struct device *dev ) ;
 796   int (*suspend)(struct device *dev , pm_message_t state ) ;
 797   int (*resume)(struct device *dev ) ;
 798   struct kobj_ns_type_operations  const  *ns_type ;
 799   void const   *(*namespace)(struct device *dev ) ;
 800   struct dev_pm_ops  const  *pm ;
 801   struct subsys_private *p ;
 802};
 803#line 397 "include/linux/device.h"
 804struct class_attribute {
 805   struct attribute attr ;
 806   ssize_t (*show)(struct class *class , struct class_attribute *attr , char *buf ) ;
 807   ssize_t (*store)(struct class *class , struct class_attribute *attr , char const   *buf ,
 808                    size_t count ) ;
 809   void const   *(*namespace)(struct class *class , struct class_attribute  const  *attr ) ;
 810};
 811#line 465 "include/linux/device.h"
 812struct device_type {
 813   char const   *name ;
 814   struct attribute_group  const  **groups ;
 815   int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
 816   char *(*devnode)(struct device *dev , umode_t *mode ) ;
 817   void (*release)(struct device *dev ) ;
 818   struct dev_pm_ops  const  *pm ;
 819};
 820#line 476 "include/linux/device.h"
 821struct device_attribute {
 822   struct attribute attr ;
 823   ssize_t (*show)(struct device *dev , struct device_attribute *attr , char *buf ) ;
 824   ssize_t (*store)(struct device *dev , struct device_attribute *attr , char const   *buf ,
 825                    size_t count ) ;
 826};
 827#line 559 "include/linux/device.h"
 828struct device_dma_parameters {
 829   unsigned int max_segment_size ;
 830   unsigned long segment_boundary_mask ;
 831};
 832#line 627
 833struct dma_coherent_mem;
 834#line 627 "include/linux/device.h"
 835struct device {
 836   struct device *parent ;
 837   struct device_private *p ;
 838   struct kobject kobj ;
 839   char const   *init_name ;
 840   struct device_type  const  *type ;
 841   struct mutex mutex ;
 842   struct bus_type *bus ;
 843   struct device_driver *driver ;
 844   void *platform_data ;
 845   struct dev_pm_info power ;
 846   struct dev_pm_domain *pm_domain ;
 847   int numa_node ;
 848   u64 *dma_mask ;
 849   u64 coherent_dma_mask ;
 850   struct device_dma_parameters *dma_parms ;
 851   struct list_head dma_pools ;
 852   struct dma_coherent_mem *dma_mem ;
 853   struct dev_archdata archdata ;
 854   struct device_node *of_node ;
 855   dev_t devt ;
 856   u32 id ;
 857   spinlock_t devres_lock ;
 858   struct list_head devres_head ;
 859   struct klist_node knode_class ;
 860   struct class *class ;
 861   struct attribute_group  const  **groups ;
 862   void (*release)(struct device *dev ) ;
 863};
 864#line 43 "include/linux/pm_wakeup.h"
 865struct wakeup_source {
 866   char const   *name ;
 867   struct list_head entry ;
 868   spinlock_t lock ;
 869   struct timer_list timer ;
 870   unsigned long timer_expires ;
 871   ktime_t total_time ;
 872   ktime_t max_time ;
 873   ktime_t last_time ;
 874   unsigned long event_count ;
 875   unsigned long active_count ;
 876   unsigned long relax_count ;
 877   unsigned long hit_count ;
 878   unsigned int active : 1 ;
 879};
 880#line 12 "include/linux/mod_devicetable.h"
 881typedef unsigned long kernel_ulong_t;
 882#line 219 "include/linux/mod_devicetable.h"
 883struct of_device_id {
 884   char name[32] ;
 885   char type[32] ;
 886   char compatible[128] ;
 887   void *data ;
 888};
 889#line 506 "include/linux/mod_devicetable.h"
 890struct platform_device_id {
 891   char name[20] ;
 892   kernel_ulong_t driver_data  __attribute__((__aligned__(sizeof(kernel_ulong_t )))) ;
 893};
 894#line 17 "include/linux/platform_device.h"
 895struct mfd_cell;
 896#line 17
 897struct mfd_cell;
 898#line 19 "include/linux/platform_device.h"
 899struct platform_device {
 900   char const   *name ;
 901   int id ;
 902   struct device dev ;
 903   u32 num_resources ;
 904   struct resource *resource ;
 905   struct platform_device_id  const  *id_entry ;
 906   struct mfd_cell *mfd_cell ;
 907   struct pdev_archdata archdata ;
 908};
 909#line 14 "include/linux/power/bq27x00_battery.h"
 910struct bq27000_platform_data {
 911   char const   *name ;
 912   int (*read)(struct device *dev , unsigned int  ) ;
 913};
 914#line 25 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1.h"
 915struct w1_reg_num {
 916   __u64 family : 8 ;
 917   __u64 id : 48 ;
 918   __u64 crc : 8 ;
 919};
 920#line 46 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1_family.h"
 921struct w1_slave;
 922#line 46
 923struct w1_slave;
 924#line 48 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1_family.h"
 925struct w1_family_ops {
 926   int (*add_slave)(struct w1_slave * ) ;
 927   void (*remove_slave)(struct w1_slave * ) ;
 928};
 929#line 54 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1_family.h"
 930struct w1_family {
 931   struct list_head family_entry ;
 932   u8 fid ;
 933   struct w1_family_ops *fops ;
 934   atomic_t refcnt ;
 935};
 936#line 62 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1.h"
 937struct w1_master;
 938#line 62 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1.h"
 939struct w1_slave {
 940   struct module *owner ;
 941   unsigned char name[32] ;
 942   struct list_head w1_slave_entry ;
 943   struct w1_reg_num reg_num ;
 944   atomic_t refcnt ;
 945   u8 rom[9] ;
 946   u32 flags ;
 947   int ttl ;
 948   struct w1_master *master ;
 949   struct w1_family *family ;
 950   void *family_data ;
 951   struct device dev ;
 952   struct completion released ;
 953};
 954#line 90 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1.h"
 955struct w1_bus_master {
 956   void *data ;
 957   u8 (*read_bit)(void * ) ;
 958   void (*write_bit)(void * , u8  ) ;
 959   u8 (*touch_bit)(void * , u8  ) ;
 960   u8 (*read_byte)(void * ) ;
 961   void (*write_byte)(void * , u8  ) ;
 962   u8 (*read_block)(void * , u8 * , int  ) ;
 963   void (*write_block)(void * , u8 const   * , int  ) ;
 964   u8 (*triplet)(void * , u8  ) ;
 965   u8 (*reset_bus)(void * ) ;
 966   u8 (*set_pullup)(void * , int  ) ;
 967   void (*search)(void * , struct w1_master * , u8  , void (*)(struct w1_master * ,
 968                                                               u64  ) ) ;
 969};
 970#line 158 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1.h"
 971struct w1_master {
 972   struct list_head w1_master_entry ;
 973   struct module *owner ;
 974   unsigned char name[32] ;
 975   struct list_head slist ;
 976   int max_slave_count ;
 977   int slave_count ;
 978   unsigned long attempts ;
 979   int slave_ttl ;
 980   int initialized ;
 981   u32 id ;
 982   int search_count ;
 983   atomic_t refcnt ;
 984   void *priv ;
 985   int priv_size ;
 986   int enable_pullup ;
 987   int pullup_duration ;
 988   struct task_struct *thread ;
 989   struct mutex mutex ;
 990   struct device_driver *driver ;
 991   struct device dev ;
 992   struct w1_bus_master *bus_master ;
 993   u32 seq ;
 994};
 995#line 1 "<compiler builtins>"
 996long __builtin_expect(long val , long res ) ;
 997#line 152 "include/linux/mutex.h"
 998void mutex_lock(struct mutex *lock ) ;
 999#line 153
1000int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) ;
1001#line 154
1002int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) ;
1003#line 168
1004int mutex_trylock(struct mutex *lock ) ;
1005#line 169
1006void mutex_unlock(struct mutex *lock ) ;
1007#line 170
1008int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
1009#line 356 "include/linux/moduleparam.h"
1010extern struct kernel_param_ops param_ops_int ;
1011#line 67 "include/linux/module.h"
1012int init_module(void) ;
1013#line 68
1014void cleanup_module(void) ;
1015#line 792 "include/linux/device.h"
1016extern void *dev_get_drvdata(struct device  const  *dev ) ;
1017#line 793
1018extern int dev_set_drvdata(struct device *dev , void *data ) ;
1019#line 40 "include/linux/platform_device.h"
1020extern void platform_device_unregister(struct platform_device * ) ;
1021#line 155
1022extern struct platform_device *platform_device_alloc(char const   *name , int id ) ;
1023#line 159
1024extern int platform_device_add_data(struct platform_device *pdev , void const   *data ,
1025                                    size_t size ) ;
1026#line 160
1027extern int platform_device_add(struct platform_device *pdev ) ;
1028#line 69 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1_family.h"
1029extern void w1_unregister_family(struct w1_family * ) ;
1030#line 70
1031extern int w1_register_family(struct w1_family * ) ;
1032#line 211 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1.h"
1033extern void w1_write_8(struct w1_master * , u8  ) ;
1034#line 212
1035extern u8 w1_read_8(struct w1_master * ) ;
1036#line 28 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_bq27000.c.common.c"
1037static int F_ID  ;
1038#line 30 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_bq27000.c.common.c"
1039static int w1_bq27000_read(struct device *dev , unsigned int reg ) 
1040{ u8 val ;
1041  struct w1_slave *sl ;
1042  struct device  const  *__mptr ;
1043  struct device *__cil_tmp6 ;
1044  struct w1_slave *__cil_tmp7 ;
1045  unsigned long __cil_tmp8 ;
1046  unsigned long __cil_tmp9 ;
1047  struct device *__cil_tmp10 ;
1048  unsigned int __cil_tmp11 ;
1049  char *__cil_tmp12 ;
1050  char *__cil_tmp13 ;
1051  unsigned long __cil_tmp14 ;
1052  unsigned long __cil_tmp15 ;
1053  struct w1_master *__cil_tmp16 ;
1054  unsigned long __cil_tmp17 ;
1055  unsigned long __cil_tmp18 ;
1056  struct mutex *__cil_tmp19 ;
1057  unsigned long __cil_tmp20 ;
1058  unsigned long __cil_tmp21 ;
1059  struct w1_master *__cil_tmp22 ;
1060  u8 __cil_tmp23 ;
1061  unsigned long __cil_tmp24 ;
1062  unsigned long __cil_tmp25 ;
1063  struct w1_master *__cil_tmp26 ;
1064  unsigned long __cil_tmp27 ;
1065  unsigned long __cil_tmp28 ;
1066  struct w1_master *__cil_tmp29 ;
1067  unsigned long __cil_tmp30 ;
1068  unsigned long __cil_tmp31 ;
1069  struct mutex *__cil_tmp32 ;
1070
1071  {
1072  {
1073#line 33
1074  __cil_tmp6 = *((struct device **)dev);
1075#line 33
1076  __mptr = (struct device  const  *)__cil_tmp6;
1077#line 33
1078  __cil_tmp7 = (struct w1_slave *)0;
1079#line 33
1080  __cil_tmp8 = (unsigned long )__cil_tmp7;
1081#line 33
1082  __cil_tmp9 = __cil_tmp8 + 112;
1083#line 33
1084  __cil_tmp10 = (struct device *)__cil_tmp9;
1085#line 33
1086  __cil_tmp11 = (unsigned int )__cil_tmp10;
1087#line 33
1088  __cil_tmp12 = (char *)__mptr;
1089#line 33
1090  __cil_tmp13 = __cil_tmp12 - __cil_tmp11;
1091#line 33
1092  sl = (struct w1_slave *)__cil_tmp13;
1093#line 35
1094  __cil_tmp14 = (unsigned long )sl;
1095#line 35
1096  __cil_tmp15 = __cil_tmp14 + 88;
1097#line 35
1098  __cil_tmp16 = *((struct w1_master **)__cil_tmp15);
1099#line 35
1100  __cil_tmp17 = (unsigned long )__cil_tmp16;
1101#line 35
1102  __cil_tmp18 = __cil_tmp17 + 144;
1103#line 35
1104  __cil_tmp19 = (struct mutex *)__cil_tmp18;
1105#line 35
1106  mutex_lock(__cil_tmp19);
1107#line 36
1108  __cil_tmp20 = (unsigned long )sl;
1109#line 36
1110  __cil_tmp21 = __cil_tmp20 + 88;
1111#line 36
1112  __cil_tmp22 = *((struct w1_master **)__cil_tmp21);
1113#line 36
1114  __cil_tmp23 = (u8 )reg;
1115#line 36
1116  w1_write_8(__cil_tmp22, __cil_tmp23);
1117#line 37
1118  __cil_tmp24 = (unsigned long )sl;
1119#line 37
1120  __cil_tmp25 = __cil_tmp24 + 88;
1121#line 37
1122  __cil_tmp26 = *((struct w1_master **)__cil_tmp25);
1123#line 37
1124  val = w1_read_8(__cil_tmp26);
1125#line 38
1126  __cil_tmp27 = (unsigned long )sl;
1127#line 38
1128  __cil_tmp28 = __cil_tmp27 + 88;
1129#line 38
1130  __cil_tmp29 = *((struct w1_master **)__cil_tmp28);
1131#line 38
1132  __cil_tmp30 = (unsigned long )__cil_tmp29;
1133#line 38
1134  __cil_tmp31 = __cil_tmp30 + 144;
1135#line 38
1136  __cil_tmp32 = (struct mutex *)__cil_tmp31;
1137#line 38
1138  mutex_unlock(__cil_tmp32);
1139  }
1140#line 40
1141  return ((int )val);
1142}
1143}
1144#line 43 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_bq27000.c.common.c"
1145static struct bq27000_platform_data bq27000_battery_info  =    {"bq27000-battery", & w1_bq27000_read};
1146#line 48 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_bq27000.c.common.c"
1147static int w1_bq27000_add_slave(struct w1_slave *sl ) 
1148{ int ret ;
1149  struct platform_device *pdev ;
1150  void const   *__cil_tmp4 ;
1151  unsigned long __cil_tmp5 ;
1152  unsigned long __cil_tmp6 ;
1153  unsigned long __cil_tmp7 ;
1154  unsigned long __cil_tmp8 ;
1155  unsigned long __cil_tmp9 ;
1156  unsigned long __cil_tmp10 ;
1157  struct device *__cil_tmp11 ;
1158  void *__cil_tmp12 ;
1159
1160  {
1161  {
1162#line 53
1163  pdev = platform_device_alloc("bq27000-battery", -1);
1164  }
1165#line 54
1166  if (! pdev) {
1167#line 55
1168    ret = -12;
1169#line 56
1170    return (ret);
1171  } else {
1172
1173  }
1174  {
1175#line 58
1176  __cil_tmp4 = (void const   *)(& bq27000_battery_info);
1177#line 58
1178  ret = platform_device_add_data(pdev, __cil_tmp4, 16UL);
1179#line 61
1180  __cil_tmp5 = (unsigned long )pdev;
1181#line 61
1182  __cil_tmp6 = __cil_tmp5 + 16;
1183#line 61
1184  __cil_tmp7 = (unsigned long )sl;
1185#line 61
1186  __cil_tmp8 = __cil_tmp7 + 112;
1187#line 61
1188  *((struct device **)__cil_tmp6) = (struct device *)__cil_tmp8;
1189#line 63
1190  ret = platform_device_add(pdev);
1191  }
1192#line 64
1193  if (ret) {
1194#line 65
1195    goto pdev_add_failed;
1196  } else {
1197
1198  }
1199  {
1200#line 67
1201  __cil_tmp9 = (unsigned long )sl;
1202#line 67
1203  __cil_tmp10 = __cil_tmp9 + 112;
1204#line 67
1205  __cil_tmp11 = (struct device *)__cil_tmp10;
1206#line 67
1207  __cil_tmp12 = (void *)pdev;
1208#line 67
1209  dev_set_drvdata(__cil_tmp11, __cil_tmp12);
1210  }
1211#line 69
1212  goto success;
1213  pdev_add_failed: 
1214  {
1215#line 72
1216  platform_device_unregister(pdev);
1217  }
1218  success: 
1219#line 74
1220  return (ret);
1221}
1222}
1223#line 77 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_bq27000.c.common.c"
1224static void w1_bq27000_remove_slave(struct w1_slave *sl ) 
1225{ struct platform_device *pdev ;
1226  void *tmp ;
1227  unsigned long __cil_tmp4 ;
1228  unsigned long __cil_tmp5 ;
1229  struct device *__cil_tmp6 ;
1230  struct device  const  *__cil_tmp7 ;
1231
1232  {
1233  {
1234#line 79
1235  __cil_tmp4 = (unsigned long )sl;
1236#line 79
1237  __cil_tmp5 = __cil_tmp4 + 112;
1238#line 79
1239  __cil_tmp6 = (struct device *)__cil_tmp5;
1240#line 79
1241  __cil_tmp7 = (struct device  const  *)__cil_tmp6;
1242#line 79
1243  tmp = dev_get_drvdata(__cil_tmp7);
1244#line 79
1245  pdev = (struct platform_device *)tmp;
1246#line 81
1247  platform_device_unregister(pdev);
1248  }
1249#line 82
1250  return;
1251}
1252}
1253#line 84 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_bq27000.c.common.c"
1254static struct w1_family_ops w1_bq27000_fops  =    {& w1_bq27000_add_slave, & w1_bq27000_remove_slave};
1255#line 89 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_bq27000.c.common.c"
1256static struct w1_family w1_bq27000_family  =    {{(struct list_head *)0, (struct list_head *)0}, (u8 )1, & w1_bq27000_fops, {0}};
1257#line 94
1258static int w1_bq27000_init(void)  __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
1259#line 94 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_bq27000.c.common.c"
1260static int w1_bq27000_init(void) 
1261{ int tmp ;
1262  int *__cil_tmp2 ;
1263  unsigned long __cil_tmp3 ;
1264  int *__cil_tmp4 ;
1265  int __cil_tmp5 ;
1266
1267  {
1268  {
1269#line 96
1270  __cil_tmp2 = & F_ID;
1271#line 96
1272  if (*__cil_tmp2) {
1273#line 97
1274    __cil_tmp3 = (unsigned long )(& w1_bq27000_family) + 16;
1275#line 97
1276    __cil_tmp4 = & F_ID;
1277#line 97
1278    __cil_tmp5 = *__cil_tmp4;
1279#line 97
1280    *((u8 *)__cil_tmp3) = (u8 )__cil_tmp5;
1281  } else {
1282
1283  }
1284  }
1285  {
1286#line 99
1287  tmp = w1_register_family(& w1_bq27000_family);
1288  }
1289#line 99
1290  return (tmp);
1291}
1292}
1293#line 102
1294static void w1_bq27000_exit(void)  __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
1295#line 102 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_bq27000.c.common.c"
1296static void w1_bq27000_exit(void) 
1297{ 
1298
1299  {
1300  {
1301#line 104
1302  w1_unregister_family(& w1_bq27000_family);
1303  }
1304#line 105
1305  return;
1306}
1307}
1308#line 108 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_bq27000.c.common.c"
1309int init_module(void) 
1310{ int tmp ;
1311
1312  {
1313  {
1314#line 108
1315  tmp = w1_bq27000_init();
1316  }
1317#line 108
1318  return (tmp);
1319}
1320}
1321#line 109 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_bq27000.c.common.c"
1322void cleanup_module(void) 
1323{ 
1324
1325  {
1326  {
1327#line 109
1328  w1_bq27000_exit();
1329  }
1330#line 109
1331  return;
1332}
1333}
1334#line 111 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_bq27000.c.common.c"
1335static char const   __param_str_F_ID[5]  = {      (char const   )'F',      (char const   )'_',      (char const   )'I',      (char const   )'D', 
1336        (char const   )'\000'};
1337#line 111 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_bq27000.c.common.c"
1338static struct kernel_param  const  __param_F_ID  __attribute__((__used__, __unused__,
1339__section__("__param"), __aligned__(sizeof(void *))))  =    {__param_str_F_ID, (struct kernel_param_ops  const  *)(& param_ops_int), (u16 )256,
1340    (s16 )0, {(void *)(& F_ID)}};
1341#line 111 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_bq27000.c.common.c"
1342static char const   __mod_F_IDtype111[18]  __attribute__((__used__, __unused__, __section__(".modinfo"),
1343__aligned__(1)))  = 
1344#line 111
1345  {      (char const   )'p',      (char const   )'a',      (char const   )'r',      (char const   )'m', 
1346        (char const   )'t',      (char const   )'y',      (char const   )'p',      (char const   )'e', 
1347        (char const   )'=',      (char const   )'F',      (char const   )'_',      (char const   )'I', 
1348        (char const   )'D',      (char const   )':',      (char const   )'i',      (char const   )'n', 
1349        (char const   )'t',      (char const   )'\000'};
1350#line 112 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_bq27000.c.common.c"
1351static char const   __mod_F_ID112[41]  __attribute__((__used__, __unused__, __section__(".modinfo"),
1352__aligned__(1)))  = 
1353#line 112
1354  {      (char const   )'p',      (char const   )'a',      (char const   )'r',      (char const   )'m', 
1355        (char const   )'=',      (char const   )'F',      (char const   )'_',      (char const   )'I', 
1356        (char const   )'D',      (char const   )':',      (char const   )'1',      (char const   )'-', 
1357        (char const   )'w',      (char const   )'i',      (char const   )'r',      (char const   )'e', 
1358        (char const   )' ',      (char const   )'s',      (char const   )'l',      (char const   )'a', 
1359        (char const   )'v',      (char const   )'e',      (char const   )' ',      (char const   )'F', 
1360        (char const   )'I',      (char const   )'D',      (char const   )' ',      (char const   )'f', 
1361        (char const   )'o',      (char const   )'r',      (char const   )' ',      (char const   )'B', 
1362        (char const   )'Q',      (char const   )' ',      (char const   )'d',      (char const   )'e', 
1363        (char const   )'v',      (char const   )'i',      (char const   )'c',      (char const   )'e', 
1364        (char const   )'\000'};
1365#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_bq27000.c.common.c"
1366static char const   __mod_license114[12]  __attribute__((__used__, __unused__, __section__(".modinfo"),
1367__aligned__(1)))  = 
1368#line 114
1369  {      (char const   )'l',      (char const   )'i',      (char const   )'c',      (char const   )'e', 
1370        (char const   )'n',      (char const   )'s',      (char const   )'e',      (char const   )'=', 
1371        (char const   )'G',      (char const   )'P',      (char const   )'L',      (char const   )'\000'};
1372#line 115 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_bq27000.c.common.c"
1373static char const   __mod_author115[29]  __attribute__((__used__, __unused__, __section__(".modinfo"),
1374__aligned__(1)))  = 
1375#line 115
1376  {      (char const   )'a',      (char const   )'u',      (char const   )'t',      (char const   )'h', 
1377        (char const   )'o',      (char const   )'r',      (char const   )'=',      (char const   )'T', 
1378        (char const   )'e',      (char const   )'x',      (char const   )'a',      (char const   )'s', 
1379        (char const   )' ',      (char const   )'I',      (char const   )'n',      (char const   )'s', 
1380        (char const   )'t',      (char const   )'r',      (char const   )'u',      (char const   )'m', 
1381        (char const   )'e',      (char const   )'n',      (char const   )'t',      (char const   )'s', 
1382        (char const   )' ',      (char const   )'L',      (char const   )'t',      (char const   )'d', 
1383        (char const   )'\000'};
1384#line 116 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_bq27000.c.common.c"
1385static char const   __mod_description116[65]  __attribute__((__used__, __unused__,
1386__section__(".modinfo"), __aligned__(1)))  = 
1387#line 116
1388  {      (char const   )'d',      (char const   )'e',      (char const   )'s',      (char const   )'c', 
1389        (char const   )'r',      (char const   )'i',      (char const   )'p',      (char const   )'t', 
1390        (char const   )'i',      (char const   )'o',      (char const   )'n',      (char const   )'=', 
1391        (char const   )'H',      (char const   )'D',      (char const   )'Q',      (char const   )'/', 
1392        (char const   )'1',      (char const   )'-',      (char const   )'w',      (char const   )'i', 
1393        (char const   )'r',      (char const   )'e',      (char const   )' ',      (char const   )'s', 
1394        (char const   )'l',      (char const   )'a',      (char const   )'v',      (char const   )'e', 
1395        (char const   )' ',      (char const   )'d',      (char const   )'r',      (char const   )'i', 
1396        (char const   )'v',      (char const   )'e',      (char const   )'r',      (char const   )' ', 
1397        (char const   )'b',      (char const   )'q',      (char const   )'2',      (char const   )'7', 
1398        (char const   )'0',      (char const   )'0',      (char const   )'0',      (char const   )' ', 
1399        (char const   )'b',      (char const   )'a',      (char const   )'t',      (char const   )'t', 
1400        (char const   )'e',      (char const   )'r',      (char const   )'y',      (char const   )' ', 
1401        (char const   )'m',      (char const   )'o',      (char const   )'n',      (char const   )'i', 
1402        (char const   )'t',      (char const   )'o',      (char const   )'r',      (char const   )' ', 
1403        (char const   )'c',      (char const   )'h',      (char const   )'i',      (char const   )'p', 
1404        (char const   )'\000'};
1405#line 134
1406void ldv_check_final_state(void) ;
1407#line 140
1408extern void ldv_initialize(void) ;
1409#line 143
1410extern int __VERIFIER_nondet_int(void) ;
1411#line 146 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_bq27000.c.common.c"
1412int LDV_IN_INTERRUPT  ;
1413#line 149 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_bq27000.c.common.c"
1414void main(void) 
1415{ struct device *var_group1 ;
1416  unsigned int var_w1_bq27000_read_0_p1 ;
1417  struct w1_slave *var_group2 ;
1418  int tmp ;
1419  int tmp___0 ;
1420  int tmp___1 ;
1421
1422  {
1423  {
1424#line 186
1425  LDV_IN_INTERRUPT = 1;
1426#line 195
1427  ldv_initialize();
1428#line 204
1429  tmp = w1_bq27000_init();
1430  }
1431#line 204
1432  if (tmp) {
1433#line 205
1434    goto ldv_final;
1435  } else {
1436
1437  }
1438  {
1439#line 211
1440  while (1) {
1441    while_continue: /* CIL Label */ ;
1442    {
1443#line 211
1444    tmp___1 = __VERIFIER_nondet_int();
1445    }
1446#line 211
1447    if (tmp___1) {
1448
1449    } else {
1450#line 211
1451      goto while_break;
1452    }
1453    {
1454#line 214
1455    tmp___0 = __VERIFIER_nondet_int();
1456    }
1457#line 216
1458    if (tmp___0 == 0) {
1459#line 216
1460      goto case_0;
1461    } else
1462#line 235
1463    if (tmp___0 == 1) {
1464#line 235
1465      goto case_1;
1466    } else
1467#line 254
1468    if (tmp___0 == 2) {
1469#line 254
1470      goto case_2;
1471    } else {
1472      {
1473#line 273
1474      goto switch_default;
1475#line 214
1476      if (0) {
1477        case_0: /* CIL Label */ 
1478        {
1479#line 227
1480        w1_bq27000_read(var_group1, var_w1_bq27000_read_0_p1);
1481        }
1482#line 234
1483        goto switch_break;
1484        case_1: /* CIL Label */ 
1485        {
1486#line 246
1487        w1_bq27000_add_slave(var_group2);
1488        }
1489#line 253
1490        goto switch_break;
1491        case_2: /* CIL Label */ 
1492        {
1493#line 265
1494        w1_bq27000_remove_slave(var_group2);
1495        }
1496#line 272
1497        goto switch_break;
1498        switch_default: /* CIL Label */ 
1499#line 273
1500        goto switch_break;
1501      } else {
1502        switch_break: /* CIL Label */ ;
1503      }
1504      }
1505    }
1506  }
1507  while_break: /* CIL Label */ ;
1508  }
1509  {
1510#line 288
1511  w1_bq27000_exit();
1512  }
1513  ldv_final: 
1514  {
1515#line 291
1516  ldv_check_final_state();
1517  }
1518#line 294
1519  return;
1520}
1521}
1522#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
1523void ldv_blast_assert(void) 
1524{ 
1525
1526  {
1527  ERROR: 
1528#line 6
1529  goto ERROR;
1530}
1531}
1532#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
1533extern int __VERIFIER_nondet_int(void) ;
1534#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1535int ldv_mutex  =    1;
1536#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1537int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) 
1538{ int nondetermined ;
1539
1540  {
1541#line 29
1542  if (ldv_mutex == 1) {
1543
1544  } else {
1545    {
1546#line 29
1547    ldv_blast_assert();
1548    }
1549  }
1550  {
1551#line 32
1552  nondetermined = __VERIFIER_nondet_int();
1553  }
1554#line 35
1555  if (nondetermined) {
1556#line 38
1557    ldv_mutex = 2;
1558#line 40
1559    return (0);
1560  } else {
1561#line 45
1562    return (-4);
1563  }
1564}
1565}
1566#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1567int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) 
1568{ int nondetermined ;
1569
1570  {
1571#line 57
1572  if (ldv_mutex == 1) {
1573
1574  } else {
1575    {
1576#line 57
1577    ldv_blast_assert();
1578    }
1579  }
1580  {
1581#line 60
1582  nondetermined = __VERIFIER_nondet_int();
1583  }
1584#line 63
1585  if (nondetermined) {
1586#line 66
1587    ldv_mutex = 2;
1588#line 68
1589    return (0);
1590  } else {
1591#line 73
1592    return (-4);
1593  }
1594}
1595}
1596#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1597int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) 
1598{ int atomic_value_after_dec ;
1599
1600  {
1601#line 83
1602  if (ldv_mutex == 1) {
1603
1604  } else {
1605    {
1606#line 83
1607    ldv_blast_assert();
1608    }
1609  }
1610  {
1611#line 86
1612  atomic_value_after_dec = __VERIFIER_nondet_int();
1613  }
1614#line 89
1615  if (atomic_value_after_dec == 0) {
1616#line 92
1617    ldv_mutex = 2;
1618#line 94
1619    return (1);
1620  } else {
1621
1622  }
1623#line 98
1624  return (0);
1625}
1626}
1627#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1628void mutex_lock(struct mutex *lock ) 
1629{ 
1630
1631  {
1632#line 108
1633  if (ldv_mutex == 1) {
1634
1635  } else {
1636    {
1637#line 108
1638    ldv_blast_assert();
1639    }
1640  }
1641#line 110
1642  ldv_mutex = 2;
1643#line 111
1644  return;
1645}
1646}
1647#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1648int mutex_trylock(struct mutex *lock ) 
1649{ int nondetermined ;
1650
1651  {
1652#line 121
1653  if (ldv_mutex == 1) {
1654
1655  } else {
1656    {
1657#line 121
1658    ldv_blast_assert();
1659    }
1660  }
1661  {
1662#line 124
1663  nondetermined = __VERIFIER_nondet_int();
1664  }
1665#line 127
1666  if (nondetermined) {
1667#line 130
1668    ldv_mutex = 2;
1669#line 132
1670    return (1);
1671  } else {
1672#line 137
1673    return (0);
1674  }
1675}
1676}
1677#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1678void mutex_unlock(struct mutex *lock ) 
1679{ 
1680
1681  {
1682#line 147
1683  if (ldv_mutex == 2) {
1684
1685  } else {
1686    {
1687#line 147
1688    ldv_blast_assert();
1689    }
1690  }
1691#line 149
1692  ldv_mutex = 1;
1693#line 150
1694  return;
1695}
1696}
1697#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1698void ldv_check_final_state(void) 
1699{ 
1700
1701  {
1702#line 156
1703  if (ldv_mutex == 1) {
1704
1705  } else {
1706    {
1707#line 156
1708    ldv_blast_assert();
1709    }
1710  }
1711#line 157
1712  return;
1713}
1714}
1715#line 303 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12353/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_bq27000.c.common.c"
1716long s__builtin_expect(long val , long res ) 
1717{ 
1718
1719  {
1720#line 304
1721  return (val);
1722}
1723}