Showing error 733

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