Showing error 731

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_ds2760.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 2037
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 100 "include/linux/printk.h"
1026extern int ( /* format attribute */  printk)(char const   *fmt  , ...) ;
1027#line 152 "include/linux/mutex.h"
1028void mutex_lock(struct mutex *lock ) ;
1029#line 153
1030int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) ;
1031#line 154
1032int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) ;
1033#line 168
1034int mutex_trylock(struct mutex *lock ) ;
1035#line 169
1036void mutex_unlock(struct mutex *lock ) ;
1037#line 170
1038int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
1039#line 140 "include/linux/sysfs.h"
1040extern int __attribute__((__warn_unused_result__))  sysfs_create_bin_file(struct kobject *kobj ,
1041                                                                          struct bin_attribute  const  *attr ) ;
1042#line 142
1043extern void sysfs_remove_bin_file(struct kobject *kobj , struct bin_attribute  const  *attr ) ;
1044#line 67 "include/linux/module.h"
1045int init_module(void) ;
1046#line 68
1047void cleanup_module(void) ;
1048#line 792 "include/linux/device.h"
1049extern void *dev_get_drvdata(struct device  const  *dev ) ;
1050#line 793
1051extern int dev_set_drvdata(struct device *dev , void *data ) ;
1052#line 40 "include/linux/platform_device.h"
1053extern void platform_device_unregister(struct platform_device * ) ;
1054#line 155
1055extern struct platform_device *platform_device_alloc(char const   *name , int id ) ;
1056#line 160
1057extern int platform_device_add(struct platform_device *pdev ) ;
1058#line 146 "include/linux/idr.h"
1059extern void ida_destroy(struct ida *ida ) ;
1060#line 147
1061extern void ida_init(struct ida *ida ) ;
1062#line 149
1063extern int ida_simple_get(struct ida *ida , unsigned int start , unsigned int end ,
1064                          gfp_t gfp_mask ) ;
1065#line 151
1066extern void ida_simple_remove(struct ida *ida , unsigned int id ) ;
1067#line 69 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1_family.h"
1068extern void w1_unregister_family(struct w1_family * ) ;
1069#line 70
1070extern int w1_register_family(struct w1_family * ) ;
1071#line 211 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1.h"
1072extern void w1_write_8(struct w1_master * , u8  ) ;
1073#line 215
1074extern void w1_write_block(struct w1_master * , u8 const   * , int  ) ;
1075#line 217
1076extern u8 w1_read_block(struct w1_master * , u8 * , int  ) ;
1077#line 218
1078extern int w1_reset_select_slave(struct w1_slave *sl ) ;
1079#line 50 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/w1_ds2760.h"
1080int w1_ds2760_read(struct device *dev , char *buf , int addr , size_t count ) ;
1081#line 52
1082int w1_ds2760_write(struct device *dev , char *buf , int addr , size_t count ) ;
1083#line 54
1084int w1_ds2760_store_eeprom(struct device *dev , int addr ) ;
1085#line 55
1086int w1_ds2760_recall_eeprom(struct device *dev , int addr ) ;
1087#line 27 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1088static int w1_ds2760_io(struct device *dev , char *buf , int addr , size_t count ,
1089                        int io ) 
1090{ struct w1_slave *sl ;
1091  struct device  const  *__mptr ;
1092  u8 tmp ;
1093  int tmp___0 ;
1094  struct w1_slave *__cil_tmp10 ;
1095  unsigned long __cil_tmp11 ;
1096  unsigned long __cil_tmp12 ;
1097  struct device *__cil_tmp13 ;
1098  unsigned int __cil_tmp14 ;
1099  char *__cil_tmp15 ;
1100  char *__cil_tmp16 ;
1101  unsigned long __cil_tmp17 ;
1102  unsigned long __cil_tmp18 ;
1103  struct w1_master *__cil_tmp19 ;
1104  unsigned long __cil_tmp20 ;
1105  unsigned long __cil_tmp21 ;
1106  struct mutex *__cil_tmp22 ;
1107  size_t __cil_tmp23 ;
1108  size_t __cil_tmp24 ;
1109  int __cil_tmp25 ;
1110  unsigned long __cil_tmp26 ;
1111  unsigned long __cil_tmp27 ;
1112  struct w1_master *__cil_tmp28 ;
1113  u8 __cil_tmp29 ;
1114  unsigned long __cil_tmp30 ;
1115  unsigned long __cil_tmp31 ;
1116  struct w1_master *__cil_tmp32 ;
1117  u8 __cil_tmp33 ;
1118  unsigned long __cil_tmp34 ;
1119  unsigned long __cil_tmp35 ;
1120  struct w1_master *__cil_tmp36 ;
1121  u8 *__cil_tmp37 ;
1122  int __cil_tmp38 ;
1123  unsigned long __cil_tmp39 ;
1124  unsigned long __cil_tmp40 ;
1125  struct w1_master *__cil_tmp41 ;
1126  u8 __cil_tmp42 ;
1127  unsigned long __cil_tmp43 ;
1128  unsigned long __cil_tmp44 ;
1129  struct w1_master *__cil_tmp45 ;
1130  u8 __cil_tmp46 ;
1131  unsigned long __cil_tmp47 ;
1132  unsigned long __cil_tmp48 ;
1133  struct w1_master *__cil_tmp49 ;
1134  u8 const   *__cil_tmp50 ;
1135  int __cil_tmp51 ;
1136  unsigned long __cil_tmp52 ;
1137  unsigned long __cil_tmp53 ;
1138  struct w1_master *__cil_tmp54 ;
1139  unsigned long __cil_tmp55 ;
1140  unsigned long __cil_tmp56 ;
1141  struct mutex *__cil_tmp57 ;
1142
1143  {
1144#line 30
1145  __mptr = (struct device  const  *)dev;
1146#line 30
1147  __cil_tmp10 = (struct w1_slave *)0;
1148#line 30
1149  __cil_tmp11 = (unsigned long )__cil_tmp10;
1150#line 30
1151  __cil_tmp12 = __cil_tmp11 + 112;
1152#line 30
1153  __cil_tmp13 = (struct device *)__cil_tmp12;
1154#line 30
1155  __cil_tmp14 = (unsigned int )__cil_tmp13;
1156#line 30
1157  __cil_tmp15 = (char *)__mptr;
1158#line 30
1159  __cil_tmp16 = __cil_tmp15 - __cil_tmp14;
1160#line 30
1161  sl = (struct w1_slave *)__cil_tmp16;
1162#line 32
1163  if (! dev) {
1164#line 33
1165    return (0);
1166  } else {
1167
1168  }
1169  {
1170#line 35
1171  __cil_tmp17 = (unsigned long )sl;
1172#line 35
1173  __cil_tmp18 = __cil_tmp17 + 88;
1174#line 35
1175  __cil_tmp19 = *((struct w1_master **)__cil_tmp18);
1176#line 35
1177  __cil_tmp20 = (unsigned long )__cil_tmp19;
1178#line 35
1179  __cil_tmp21 = __cil_tmp20 + 144;
1180#line 35
1181  __cil_tmp22 = (struct mutex *)__cil_tmp21;
1182#line 35
1183  mutex_lock(__cil_tmp22);
1184  }
1185#line 37
1186  if (addr > 64) {
1187#line 38
1188    count = (size_t )0;
1189#line 39
1190    goto out;
1191  } else
1192#line 37
1193  if (addr < 0) {
1194#line 38
1195    count = (size_t )0;
1196#line 39
1197    goto out;
1198  } else {
1199
1200  }
1201  {
1202#line 41
1203  __cil_tmp23 = (size_t )addr;
1204#line 41
1205  __cil_tmp24 = __cil_tmp23 + count;
1206#line 41
1207  if (__cil_tmp24 > 64UL) {
1208#line 42
1209    __cil_tmp25 = 64 - addr;
1210#line 42
1211    count = (size_t )__cil_tmp25;
1212  } else {
1213
1214  }
1215  }
1216  {
1217#line 44
1218  tmp___0 = w1_reset_select_slave(sl);
1219  }
1220#line 44
1221  if (tmp___0) {
1222
1223  } else
1224#line 45
1225  if (! io) {
1226    {
1227#line 46
1228    __cil_tmp26 = (unsigned long )sl;
1229#line 46
1230    __cil_tmp27 = __cil_tmp26 + 88;
1231#line 46
1232    __cil_tmp28 = *((struct w1_master **)__cil_tmp27);
1233#line 46
1234    __cil_tmp29 = (u8 )105;
1235#line 46
1236    w1_write_8(__cil_tmp28, __cil_tmp29);
1237#line 47
1238    __cil_tmp30 = (unsigned long )sl;
1239#line 47
1240    __cil_tmp31 = __cil_tmp30 + 88;
1241#line 47
1242    __cil_tmp32 = *((struct w1_master **)__cil_tmp31);
1243#line 47
1244    __cil_tmp33 = (u8 )addr;
1245#line 47
1246    w1_write_8(__cil_tmp32, __cil_tmp33);
1247#line 48
1248    __cil_tmp34 = (unsigned long )sl;
1249#line 48
1250    __cil_tmp35 = __cil_tmp34 + 88;
1251#line 48
1252    __cil_tmp36 = *((struct w1_master **)__cil_tmp35);
1253#line 48
1254    __cil_tmp37 = (u8 *)buf;
1255#line 48
1256    __cil_tmp38 = (int )count;
1257#line 48
1258    tmp = w1_read_block(__cil_tmp36, __cil_tmp37, __cil_tmp38);
1259#line 48
1260    count = (size_t )tmp;
1261    }
1262  } else {
1263    {
1264#line 50
1265    __cil_tmp39 = (unsigned long )sl;
1266#line 50
1267    __cil_tmp40 = __cil_tmp39 + 88;
1268#line 50
1269    __cil_tmp41 = *((struct w1_master **)__cil_tmp40);
1270#line 50
1271    __cil_tmp42 = (u8 )108;
1272#line 50
1273    w1_write_8(__cil_tmp41, __cil_tmp42);
1274#line 51
1275    __cil_tmp43 = (unsigned long )sl;
1276#line 51
1277    __cil_tmp44 = __cil_tmp43 + 88;
1278#line 51
1279    __cil_tmp45 = *((struct w1_master **)__cil_tmp44);
1280#line 51
1281    __cil_tmp46 = (u8 )addr;
1282#line 51
1283    w1_write_8(__cil_tmp45, __cil_tmp46);
1284#line 52
1285    __cil_tmp47 = (unsigned long )sl;
1286#line 52
1287    __cil_tmp48 = __cil_tmp47 + 88;
1288#line 52
1289    __cil_tmp49 = *((struct w1_master **)__cil_tmp48);
1290#line 52
1291    __cil_tmp50 = (u8 const   *)buf;
1292#line 52
1293    __cil_tmp51 = (int )count;
1294#line 52
1295    w1_write_block(__cil_tmp49, __cil_tmp50, __cil_tmp51);
1296    }
1297  }
1298  out: 
1299  {
1300#line 58
1301  __cil_tmp52 = (unsigned long )sl;
1302#line 58
1303  __cil_tmp53 = __cil_tmp52 + 88;
1304#line 58
1305  __cil_tmp54 = *((struct w1_master **)__cil_tmp53);
1306#line 58
1307  __cil_tmp55 = (unsigned long )__cil_tmp54;
1308#line 58
1309  __cil_tmp56 = __cil_tmp55 + 144;
1310#line 58
1311  __cil_tmp57 = (struct mutex *)__cil_tmp56;
1312#line 58
1313  mutex_unlock(__cil_tmp57);
1314  }
1315#line 60
1316  return ((int )count);
1317}
1318}
1319#line 63 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1320int w1_ds2760_read(struct device *dev , char *buf , int addr , size_t count ) 
1321{ int tmp ;
1322
1323  {
1324  {
1325#line 65
1326  tmp = w1_ds2760_io(dev, buf, addr, count, 0);
1327  }
1328#line 65
1329  return (tmp);
1330}
1331}
1332#line 68 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1333int w1_ds2760_write(struct device *dev , char *buf , int addr , size_t count ) 
1334{ int tmp ;
1335
1336  {
1337  {
1338#line 70
1339  tmp = w1_ds2760_io(dev, buf, addr, count, 1);
1340  }
1341#line 70
1342  return (tmp);
1343}
1344}
1345#line 73 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1346static int w1_ds2760_eeprom_cmd(struct device *dev , int addr , int cmd ) 
1347{ struct w1_slave *sl ;
1348  struct device  const  *__mptr ;
1349  int tmp ;
1350  struct w1_slave *__cil_tmp7 ;
1351  unsigned long __cil_tmp8 ;
1352  unsigned long __cil_tmp9 ;
1353  struct device *__cil_tmp10 ;
1354  unsigned int __cil_tmp11 ;
1355  char *__cil_tmp12 ;
1356  char *__cil_tmp13 ;
1357  unsigned long __cil_tmp14 ;
1358  unsigned long __cil_tmp15 ;
1359  struct w1_master *__cil_tmp16 ;
1360  unsigned long __cil_tmp17 ;
1361  unsigned long __cil_tmp18 ;
1362  struct mutex *__cil_tmp19 ;
1363  unsigned long __cil_tmp20 ;
1364  unsigned long __cil_tmp21 ;
1365  struct w1_master *__cil_tmp22 ;
1366  u8 __cil_tmp23 ;
1367  unsigned long __cil_tmp24 ;
1368  unsigned long __cil_tmp25 ;
1369  struct w1_master *__cil_tmp26 ;
1370  u8 __cil_tmp27 ;
1371  unsigned long __cil_tmp28 ;
1372  unsigned long __cil_tmp29 ;
1373  struct w1_master *__cil_tmp30 ;
1374  unsigned long __cil_tmp31 ;
1375  unsigned long __cil_tmp32 ;
1376  struct mutex *__cil_tmp33 ;
1377
1378  {
1379#line 75
1380  __mptr = (struct device  const  *)dev;
1381#line 75
1382  __cil_tmp7 = (struct w1_slave *)0;
1383#line 75
1384  __cil_tmp8 = (unsigned long )__cil_tmp7;
1385#line 75
1386  __cil_tmp9 = __cil_tmp8 + 112;
1387#line 75
1388  __cil_tmp10 = (struct device *)__cil_tmp9;
1389#line 75
1390  __cil_tmp11 = (unsigned int )__cil_tmp10;
1391#line 75
1392  __cil_tmp12 = (char *)__mptr;
1393#line 75
1394  __cil_tmp13 = __cil_tmp12 - __cil_tmp11;
1395#line 75
1396  sl = (struct w1_slave *)__cil_tmp13;
1397#line 77
1398  if (! dev) {
1399#line 78
1400    return (-22);
1401  } else {
1402
1403  }
1404  {
1405#line 80
1406  __cil_tmp14 = (unsigned long )sl;
1407#line 80
1408  __cil_tmp15 = __cil_tmp14 + 88;
1409#line 80
1410  __cil_tmp16 = *((struct w1_master **)__cil_tmp15);
1411#line 80
1412  __cil_tmp17 = (unsigned long )__cil_tmp16;
1413#line 80
1414  __cil_tmp18 = __cil_tmp17 + 144;
1415#line 80
1416  __cil_tmp19 = (struct mutex *)__cil_tmp18;
1417#line 80
1418  mutex_lock(__cil_tmp19);
1419#line 82
1420  tmp = w1_reset_select_slave(sl);
1421  }
1422#line 82
1423  if (tmp == 0) {
1424    {
1425#line 83
1426    __cil_tmp20 = (unsigned long )sl;
1427#line 83
1428    __cil_tmp21 = __cil_tmp20 + 88;
1429#line 83
1430    __cil_tmp22 = *((struct w1_master **)__cil_tmp21);
1431#line 83
1432    __cil_tmp23 = (u8 )cmd;
1433#line 83
1434    w1_write_8(__cil_tmp22, __cil_tmp23);
1435#line 84
1436    __cil_tmp24 = (unsigned long )sl;
1437#line 84
1438    __cil_tmp25 = __cil_tmp24 + 88;
1439#line 84
1440    __cil_tmp26 = *((struct w1_master **)__cil_tmp25);
1441#line 84
1442    __cil_tmp27 = (u8 )addr;
1443#line 84
1444    w1_write_8(__cil_tmp26, __cil_tmp27);
1445    }
1446  } else {
1447
1448  }
1449  {
1450#line 87
1451  __cil_tmp28 = (unsigned long )sl;
1452#line 87
1453  __cil_tmp29 = __cil_tmp28 + 88;
1454#line 87
1455  __cil_tmp30 = *((struct w1_master **)__cil_tmp29);
1456#line 87
1457  __cil_tmp31 = (unsigned long )__cil_tmp30;
1458#line 87
1459  __cil_tmp32 = __cil_tmp31 + 144;
1460#line 87
1461  __cil_tmp33 = (struct mutex *)__cil_tmp32;
1462#line 87
1463  mutex_unlock(__cil_tmp33);
1464  }
1465#line 88
1466  return (0);
1467}
1468}
1469#line 91 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1470int w1_ds2760_store_eeprom(struct device *dev , int addr ) 
1471{ int tmp ;
1472
1473  {
1474  {
1475#line 93
1476  tmp = w1_ds2760_eeprom_cmd(dev, addr, 72);
1477  }
1478#line 93
1479  return (tmp);
1480}
1481}
1482#line 96 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1483int w1_ds2760_recall_eeprom(struct device *dev , int addr ) 
1484{ int tmp ;
1485
1486  {
1487  {
1488#line 98
1489  tmp = w1_ds2760_eeprom_cmd(dev, addr, 184);
1490  }
1491#line 98
1492  return (tmp);
1493}
1494}
1495#line 101 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1496static ssize_t w1_ds2760_read_bin(struct file *filp , struct kobject *kobj , struct bin_attribute *bin_attr ,
1497                                  char *buf , loff_t off , size_t count ) 
1498{ struct device *dev ;
1499  struct kobject  const  *__mptr ;
1500  int tmp ;
1501  struct device *__cil_tmp10 ;
1502  unsigned long __cil_tmp11 ;
1503  unsigned long __cil_tmp12 ;
1504  struct kobject *__cil_tmp13 ;
1505  unsigned int __cil_tmp14 ;
1506  char *__cil_tmp15 ;
1507  char *__cil_tmp16 ;
1508  int __cil_tmp17 ;
1509
1510  {
1511  {
1512#line 105
1513  __mptr = (struct kobject  const  *)kobj;
1514#line 105
1515  __cil_tmp10 = (struct device *)0;
1516#line 105
1517  __cil_tmp11 = (unsigned long )__cil_tmp10;
1518#line 105
1519  __cil_tmp12 = __cil_tmp11 + 16;
1520#line 105
1521  __cil_tmp13 = (struct kobject *)__cil_tmp12;
1522#line 105
1523  __cil_tmp14 = (unsigned int )__cil_tmp13;
1524#line 105
1525  __cil_tmp15 = (char *)__mptr;
1526#line 105
1527  __cil_tmp16 = __cil_tmp15 - __cil_tmp14;
1528#line 105
1529  dev = (struct device *)__cil_tmp16;
1530#line 106
1531  __cil_tmp17 = (int )off;
1532#line 106
1533  tmp = w1_ds2760_read(dev, buf, __cil_tmp17, count);
1534  }
1535#line 106
1536  return ((ssize_t )tmp);
1537}
1538}
1539#line 109 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1540static struct bin_attribute w1_ds2760_bin_attr  =    {{"w1_slave", (umode_t )292}, (size_t )64, (void *)0, & w1_ds2760_read_bin, (ssize_t (*)(struct file * ,
1541                                                                                            struct kobject * ,
1542                                                                                            struct bin_attribute * ,
1543                                                                                            char * ,
1544                                                                                            loff_t  ,
1545                                                                                            size_t  ))0,
1546    (int (*)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ))0};
1547#line 118 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1548static struct ida bat_ida  =    {{(struct idr_layer *)((void *)0), (struct idr_layer *)((void *)0), 0, 0, {{{{{(__ticketpair_t )0}},
1549                                                                                3735899821U,
1550                                                                                4294967295U,
1551                                                                                (void *)-1L}}}},
1552    (struct ida_bitmap *)((void *)0)};
1553#line 120 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1554static int w1_ds2760_add_slave(struct w1_slave *sl ) 
1555{ int ret ;
1556  int id ;
1557  struct platform_device *pdev ;
1558  unsigned long __cil_tmp5 ;
1559  unsigned long __cil_tmp6 ;
1560  unsigned long __cil_tmp7 ;
1561  unsigned long __cil_tmp8 ;
1562  unsigned long __cil_tmp9 ;
1563  unsigned long __cil_tmp10 ;
1564  unsigned long __cil_tmp11 ;
1565  struct kobject *__cil_tmp12 ;
1566  struct bin_attribute  const  *__cil_tmp13 ;
1567  unsigned long __cil_tmp14 ;
1568  unsigned long __cil_tmp15 ;
1569  struct device *__cil_tmp16 ;
1570  void *__cil_tmp17 ;
1571  unsigned int __cil_tmp18 ;
1572
1573  {
1574  {
1575#line 126
1576  id = ida_simple_get(& bat_ida, 0U, 0U, 208U);
1577  }
1578#line 127
1579  if (id < 0) {
1580#line 128
1581    ret = id;
1582#line 129
1583    goto noid;
1584  } else {
1585
1586  }
1587  {
1588#line 132
1589  pdev = platform_device_alloc("ds2760-battery", id);
1590  }
1591#line 133
1592  if (! pdev) {
1593#line 134
1594    ret = -12;
1595#line 135
1596    goto pdev_alloc_failed;
1597  } else {
1598
1599  }
1600  {
1601#line 137
1602  __cil_tmp5 = (unsigned long )pdev;
1603#line 137
1604  __cil_tmp6 = __cil_tmp5 + 16;
1605#line 137
1606  __cil_tmp7 = (unsigned long )sl;
1607#line 137
1608  __cil_tmp8 = __cil_tmp7 + 112;
1609#line 137
1610  *((struct device **)__cil_tmp6) = (struct device *)__cil_tmp8;
1611#line 139
1612  ret = platform_device_add(pdev);
1613  }
1614#line 140
1615  if (ret) {
1616#line 141
1617    goto bin_attr_failed;
1618  } else {
1619
1620  }
1621  {
1622#line 143
1623  __cil_tmp9 = 112 + 16;
1624#line 143
1625  __cil_tmp10 = (unsigned long )sl;
1626#line 143
1627  __cil_tmp11 = __cil_tmp10 + __cil_tmp9;
1628#line 143
1629  __cil_tmp12 = (struct kobject *)__cil_tmp11;
1630#line 143
1631  __cil_tmp13 = (struct bin_attribute  const  *)(& w1_ds2760_bin_attr);
1632#line 143
1633  ret = (int )sysfs_create_bin_file(__cil_tmp12, __cil_tmp13);
1634  }
1635#line 144
1636  if (ret) {
1637#line 145
1638    goto bin_attr_failed;
1639  } else {
1640
1641  }
1642  {
1643#line 147
1644  __cil_tmp14 = (unsigned long )sl;
1645#line 147
1646  __cil_tmp15 = __cil_tmp14 + 112;
1647#line 147
1648  __cil_tmp16 = (struct device *)__cil_tmp15;
1649#line 147
1650  __cil_tmp17 = (void *)pdev;
1651#line 147
1652  dev_set_drvdata(__cil_tmp16, __cil_tmp17);
1653  }
1654#line 149
1655  goto noid;
1656  bin_attr_failed: 
1657  {
1658#line 153
1659  platform_device_unregister(pdev);
1660  }
1661  pdev_alloc_failed: 
1662  {
1663#line 155
1664  __cil_tmp18 = (unsigned int )id;
1665#line 155
1666  ida_simple_remove(& bat_ida, __cil_tmp18);
1667  }
1668  noid: 
1669#line 158
1670  return (ret);
1671}
1672}
1673#line 161 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1674static void w1_ds2760_remove_slave(struct w1_slave *sl ) 
1675{ struct platform_device *pdev ;
1676  void *tmp ;
1677  int id ;
1678  unsigned long __cil_tmp5 ;
1679  unsigned long __cil_tmp6 ;
1680  struct device *__cil_tmp7 ;
1681  struct device  const  *__cil_tmp8 ;
1682  unsigned long __cil_tmp9 ;
1683  unsigned long __cil_tmp10 ;
1684  unsigned int __cil_tmp11 ;
1685  unsigned long __cil_tmp12 ;
1686  unsigned long __cil_tmp13 ;
1687  unsigned long __cil_tmp14 ;
1688  struct kobject *__cil_tmp15 ;
1689  struct bin_attribute  const  *__cil_tmp16 ;
1690
1691  {
1692  {
1693#line 163
1694  __cil_tmp5 = (unsigned long )sl;
1695#line 163
1696  __cil_tmp6 = __cil_tmp5 + 112;
1697#line 163
1698  __cil_tmp7 = (struct device *)__cil_tmp6;
1699#line 163
1700  __cil_tmp8 = (struct device  const  *)__cil_tmp7;
1701#line 163
1702  tmp = dev_get_drvdata(__cil_tmp8);
1703#line 163
1704  pdev = (struct platform_device *)tmp;
1705#line 164
1706  __cil_tmp9 = (unsigned long )pdev;
1707#line 164
1708  __cil_tmp10 = __cil_tmp9 + 8;
1709#line 164
1710  id = *((int *)__cil_tmp10);
1711#line 166
1712  platform_device_unregister(pdev);
1713#line 167
1714  __cil_tmp11 = (unsigned int )id;
1715#line 167
1716  ida_simple_remove(& bat_ida, __cil_tmp11);
1717#line 168
1718  __cil_tmp12 = 112 + 16;
1719#line 168
1720  __cil_tmp13 = (unsigned long )sl;
1721#line 168
1722  __cil_tmp14 = __cil_tmp13 + __cil_tmp12;
1723#line 168
1724  __cil_tmp15 = (struct kobject *)__cil_tmp14;
1725#line 168
1726  __cil_tmp16 = (struct bin_attribute  const  *)(& w1_ds2760_bin_attr);
1727#line 168
1728  sysfs_remove_bin_file(__cil_tmp15, __cil_tmp16);
1729  }
1730#line 169
1731  return;
1732}
1733}
1734#line 171 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1735static struct w1_family_ops w1_ds2760_fops  =    {& w1_ds2760_add_slave, & w1_ds2760_remove_slave};
1736#line 176 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1737static struct w1_family w1_ds2760_family  =    {{(struct list_head *)0, (struct list_head *)0}, (u8 )48, & w1_ds2760_fops, {0}};
1738#line 181
1739static int w1_ds2760_init(void)  __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
1740#line 181 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1741static int w1_ds2760_init(void) 
1742{ int tmp ;
1743
1744  {
1745  {
1746#line 183
1747  printk("<6>1-Wire driver for the DS2760 battery monitor  chip  - (c) 2004-2005, Szabolcs Gyurko\n");
1748#line 185
1749  ida_init(& bat_ida);
1750#line 186
1751  tmp = w1_register_family(& w1_ds2760_family);
1752  }
1753#line 186
1754  return (tmp);
1755}
1756}
1757#line 189
1758static void w1_ds2760_exit(void)  __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
1759#line 189 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1760static void w1_ds2760_exit(void) 
1761{ 
1762
1763  {
1764  {
1765#line 191
1766  w1_unregister_family(& w1_ds2760_family);
1767#line 192
1768  ida_destroy(& bat_ida);
1769  }
1770#line 193
1771  return;
1772}
1773}
1774#line 195
1775extern void *__crc_w1_ds2760_read  __attribute__((__weak__)) ;
1776#line 195 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1777static unsigned long const   __kcrctab_w1_ds2760_read  __attribute__((__used__, __unused__,
1778__section__("___kcrctab+w1_ds2760_read")))  =    (unsigned long const   )((unsigned long )(& __crc_w1_ds2760_read));
1779#line 195 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1780static char const   __kstrtab_w1_ds2760_read[15]  __attribute__((__section__("__ksymtab_strings"),
1781__aligned__(1)))  = 
1782#line 195
1783  {      (char const   )'w',      (char const   )'1',      (char const   )'_',      (char const   )'d', 
1784        (char const   )'s',      (char const   )'2',      (char const   )'7',      (char const   )'6', 
1785        (char const   )'0',      (char const   )'_',      (char const   )'r',      (char const   )'e', 
1786        (char const   )'a',      (char const   )'d',      (char const   )'\000'};
1787#line 195 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1788static struct kernel_symbol  const  __ksymtab_w1_ds2760_read  __attribute__((__used__,
1789__unused__, __section__("___ksymtab+w1_ds2760_read")))  =    {(unsigned long )(& w1_ds2760_read), __kstrtab_w1_ds2760_read};
1790#line 196
1791extern void *__crc_w1_ds2760_write  __attribute__((__weak__)) ;
1792#line 196 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1793static unsigned long const   __kcrctab_w1_ds2760_write  __attribute__((__used__, __unused__,
1794__section__("___kcrctab+w1_ds2760_write")))  =    (unsigned long const   )((unsigned long )(& __crc_w1_ds2760_write));
1795#line 196 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1796static char const   __kstrtab_w1_ds2760_write[16]  __attribute__((__section__("__ksymtab_strings"),
1797__aligned__(1)))  = 
1798#line 196
1799  {      (char const   )'w',      (char const   )'1',      (char const   )'_',      (char const   )'d', 
1800        (char const   )'s',      (char const   )'2',      (char const   )'7',      (char const   )'6', 
1801        (char const   )'0',      (char const   )'_',      (char const   )'w',      (char const   )'r', 
1802        (char const   )'i',      (char const   )'t',      (char const   )'e',      (char const   )'\000'};
1803#line 196 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1804static struct kernel_symbol  const  __ksymtab_w1_ds2760_write  __attribute__((__used__,
1805__unused__, __section__("___ksymtab+w1_ds2760_write")))  =    {(unsigned long )(& w1_ds2760_write), __kstrtab_w1_ds2760_write};
1806#line 197
1807extern void *__crc_w1_ds2760_store_eeprom  __attribute__((__weak__)) ;
1808#line 197 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1809static unsigned long const   __kcrctab_w1_ds2760_store_eeprom  __attribute__((__used__,
1810__unused__, __section__("___kcrctab+w1_ds2760_store_eeprom")))  =    (unsigned long const   )((unsigned long )(& __crc_w1_ds2760_store_eeprom));
1811#line 197 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1812static char const   __kstrtab_w1_ds2760_store_eeprom[23]  __attribute__((__section__("__ksymtab_strings"),
1813__aligned__(1)))  = 
1814#line 197
1815  {      (char const   )'w',      (char const   )'1',      (char const   )'_',      (char const   )'d', 
1816        (char const   )'s',      (char const   )'2',      (char const   )'7',      (char const   )'6', 
1817        (char const   )'0',      (char const   )'_',      (char const   )'s',      (char const   )'t', 
1818        (char const   )'o',      (char const   )'r',      (char const   )'e',      (char const   )'_', 
1819        (char const   )'e',      (char const   )'e',      (char const   )'p',      (char const   )'r', 
1820        (char const   )'o',      (char const   )'m',      (char const   )'\000'};
1821#line 197 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1822static struct kernel_symbol  const  __ksymtab_w1_ds2760_store_eeprom  __attribute__((__used__,
1823__unused__, __section__("___ksymtab+w1_ds2760_store_eeprom")))  =    {(unsigned long )(& w1_ds2760_store_eeprom), __kstrtab_w1_ds2760_store_eeprom};
1824#line 198
1825extern void *__crc_w1_ds2760_recall_eeprom  __attribute__((__weak__)) ;
1826#line 198 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1827static unsigned long const   __kcrctab_w1_ds2760_recall_eeprom  __attribute__((__used__,
1828__unused__, __section__("___kcrctab+w1_ds2760_recall_eeprom")))  =    (unsigned long const   )((unsigned long )(& __crc_w1_ds2760_recall_eeprom));
1829#line 198 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1830static char const   __kstrtab_w1_ds2760_recall_eeprom[24]  __attribute__((__section__("__ksymtab_strings"),
1831__aligned__(1)))  = 
1832#line 198
1833  {      (char const   )'w',      (char const   )'1',      (char const   )'_',      (char const   )'d', 
1834        (char const   )'s',      (char const   )'2',      (char const   )'7',      (char const   )'6', 
1835        (char const   )'0',      (char const   )'_',      (char const   )'r',      (char const   )'e', 
1836        (char const   )'c',      (char const   )'a',      (char const   )'l',      (char const   )'l', 
1837        (char const   )'_',      (char const   )'e',      (char const   )'e',      (char const   )'p', 
1838        (char const   )'r',      (char const   )'o',      (char const   )'m',      (char const   )'\000'};
1839#line 198 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1840static struct kernel_symbol  const  __ksymtab_w1_ds2760_recall_eeprom  __attribute__((__used__,
1841__unused__, __section__("___ksymtab+w1_ds2760_recall_eeprom")))  =    {(unsigned long )(& w1_ds2760_recall_eeprom), __kstrtab_w1_ds2760_recall_eeprom};
1842#line 200 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1843int init_module(void) 
1844{ int tmp ;
1845
1846  {
1847  {
1848#line 200
1849  tmp = w1_ds2760_init();
1850  }
1851#line 200
1852  return (tmp);
1853}
1854}
1855#line 201 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1856void cleanup_module(void) 
1857{ 
1858
1859  {
1860  {
1861#line 201
1862  w1_ds2760_exit();
1863  }
1864#line 201
1865  return;
1866}
1867}
1868#line 203 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1869static char const   __mod_license203[12]  __attribute__((__used__, __unused__, __section__(".modinfo"),
1870__aligned__(1)))  = 
1871#line 203
1872  {      (char const   )'l',      (char const   )'i',      (char const   )'c',      (char const   )'e', 
1873        (char const   )'n',      (char const   )'s',      (char const   )'e',      (char const   )'=', 
1874        (char const   )'G',      (char const   )'P',      (char const   )'L',      (char const   )'\000'};
1875#line 204 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1876static char const   __mod_author204[48]  __attribute__((__used__, __unused__, __section__(".modinfo"),
1877__aligned__(1)))  = 
1878#line 204
1879  {      (char const   )'a',      (char const   )'u',      (char const   )'t',      (char const   )'h', 
1880        (char const   )'o',      (char const   )'r',      (char const   )'=',      (char const   )'S', 
1881        (char const   )'z',      (char const   )'a',      (char const   )'b',      (char const   )'o', 
1882        (char const   )'l',      (char const   )'c',      (char const   )'s',      (char const   )' ', 
1883        (char const   )'G',      (char const   )'y',      (char const   )'u',      (char const   )'r', 
1884        (char const   )'k',      (char const   )'o',      (char const   )' ',      (char const   )'<', 
1885        (char const   )'s',      (char const   )'z',      (char const   )'a',      (char const   )'b', 
1886        (char const   )'o',      (char const   )'l',      (char const   )'c',      (char const   )'s', 
1887        (char const   )'.',      (char const   )'g',      (char const   )'y',      (char const   )'u', 
1888        (char const   )'r',      (char const   )'k',      (char const   )'o',      (char const   )'@', 
1889        (char const   )'t',      (char const   )'l',      (char const   )'t',      (char const   )'.', 
1890        (char const   )'h',      (char const   )'u',      (char const   )'>',      (char const   )'\000'};
1891#line 205 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1892static char const   __mod_description205[59]  __attribute__((__used__, __unused__,
1893__section__(".modinfo"), __aligned__(1)))  = 
1894#line 205
1895  {      (char const   )'d',      (char const   )'e',      (char const   )'s',      (char const   )'c', 
1896        (char const   )'r',      (char const   )'i',      (char const   )'p',      (char const   )'t', 
1897        (char const   )'i',      (char const   )'o',      (char const   )'n',      (char const   )'=', 
1898        (char const   )'1',      (char const   )'-',      (char const   )'w',      (char const   )'i', 
1899        (char const   )'r',      (char const   )'e',      (char const   )' ',      (char const   )'D', 
1900        (char const   )'r',      (char const   )'i',      (char const   )'v',      (char const   )'e', 
1901        (char const   )'r',      (char const   )' ',      (char const   )'D',      (char const   )'a', 
1902        (char const   )'l',      (char const   )'l',      (char const   )'a',      (char const   )'s', 
1903        (char const   )' ',      (char const   )'2',      (char const   )'7',      (char const   )'6', 
1904        (char const   )'0',      (char const   )' ',      (char const   )'b',      (char const   )'a', 
1905        (char const   )'t',      (char const   )'t',      (char const   )'e',      (char const   )'r', 
1906        (char const   )'y',      (char const   )' ',      (char const   )'m',      (char const   )'o', 
1907        (char const   )'n',      (char const   )'i',      (char const   )'t',      (char const   )'o', 
1908        (char const   )'r',      (char const   )' ',      (char const   )'c',      (char const   )'h', 
1909        (char const   )'i',      (char const   )'p',      (char const   )'\000'};
1910#line 223
1911void ldv_check_final_state(void) ;
1912#line 229
1913extern void ldv_initialize(void) ;
1914#line 232
1915extern int __VERIFIER_nondet_int(void) ;
1916#line 235 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1917int LDV_IN_INTERRUPT  ;
1918#line 238 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
1919void main(void) 
1920{ struct file *var_group1 ;
1921  struct kobject *var_group2 ;
1922  struct bin_attribute *var_w1_ds2760_read_bin_6_p2 ;
1923  char *var_w1_ds2760_read_bin_6_p3 ;
1924  loff_t var_w1_ds2760_read_bin_6_p4 ;
1925  size_t var_w1_ds2760_read_bin_6_p5 ;
1926  struct w1_slave *var_group3 ;
1927  int tmp ;
1928  int tmp___0 ;
1929  int tmp___1 ;
1930
1931  {
1932  {
1933#line 274
1934  LDV_IN_INTERRUPT = 1;
1935#line 283
1936  ldv_initialize();
1937#line 289
1938  tmp = w1_ds2760_init();
1939  }
1940#line 289
1941  if (tmp) {
1942#line 290
1943    goto ldv_final;
1944  } else {
1945
1946  }
1947  {
1948#line 296
1949  while (1) {
1950    while_continue: /* CIL Label */ ;
1951    {
1952#line 296
1953    tmp___1 = __VERIFIER_nondet_int();
1954    }
1955#line 296
1956    if (tmp___1) {
1957
1958    } else {
1959#line 296
1960      goto while_break;
1961    }
1962    {
1963#line 299
1964    tmp___0 = __VERIFIER_nondet_int();
1965    }
1966#line 301
1967    if (tmp___0 == 0) {
1968#line 301
1969      goto case_0;
1970    } else
1971#line 317
1972    if (tmp___0 == 1) {
1973#line 317
1974      goto case_1;
1975    } else
1976#line 333
1977    if (tmp___0 == 2) {
1978#line 333
1979      goto case_2;
1980    } else {
1981      {
1982#line 349
1983      goto switch_default;
1984#line 299
1985      if (0) {
1986        case_0: /* CIL Label */ 
1987        {
1988#line 309
1989        w1_ds2760_read_bin(var_group1, var_group2, var_w1_ds2760_read_bin_6_p2, var_w1_ds2760_read_bin_6_p3,
1990                           var_w1_ds2760_read_bin_6_p4, var_w1_ds2760_read_bin_6_p5);
1991        }
1992#line 316
1993        goto switch_break;
1994        case_1: /* CIL Label */ 
1995        {
1996#line 325
1997        w1_ds2760_add_slave(var_group3);
1998        }
1999#line 332
2000        goto switch_break;
2001        case_2: /* CIL Label */ 
2002        {
2003#line 341
2004        w1_ds2760_remove_slave(var_group3);
2005        }
2006#line 348
2007        goto switch_break;
2008        switch_default: /* CIL Label */ 
2009#line 349
2010        goto switch_break;
2011      } else {
2012        switch_break: /* CIL Label */ ;
2013      }
2014      }
2015    }
2016  }
2017  while_break: /* CIL Label */ ;
2018  }
2019  {
2020#line 361
2021  w1_ds2760_exit();
2022  }
2023  ldv_final: 
2024  {
2025#line 364
2026  ldv_check_final_state();
2027  }
2028#line 367
2029  return;
2030}
2031}
2032#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
2033void ldv_blast_assert(void) 
2034{ 
2035
2036  {
2037  ERROR: 
2038#line 6
2039  goto ERROR;
2040}
2041}
2042#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
2043extern int __VERIFIER_nondet_int(void) ;
2044#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2045int ldv_mutex  =    1;
2046#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2047int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) 
2048{ int nondetermined ;
2049
2050  {
2051#line 29
2052  if (ldv_mutex == 1) {
2053
2054  } else {
2055    {
2056#line 29
2057    ldv_blast_assert();
2058    }
2059  }
2060  {
2061#line 32
2062  nondetermined = __VERIFIER_nondet_int();
2063  }
2064#line 35
2065  if (nondetermined) {
2066#line 38
2067    ldv_mutex = 2;
2068#line 40
2069    return (0);
2070  } else {
2071#line 45
2072    return (-4);
2073  }
2074}
2075}
2076#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2077int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) 
2078{ int nondetermined ;
2079
2080  {
2081#line 57
2082  if (ldv_mutex == 1) {
2083
2084  } else {
2085    {
2086#line 57
2087    ldv_blast_assert();
2088    }
2089  }
2090  {
2091#line 60
2092  nondetermined = __VERIFIER_nondet_int();
2093  }
2094#line 63
2095  if (nondetermined) {
2096#line 66
2097    ldv_mutex = 2;
2098#line 68
2099    return (0);
2100  } else {
2101#line 73
2102    return (-4);
2103  }
2104}
2105}
2106#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2107int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) 
2108{ int atomic_value_after_dec ;
2109
2110  {
2111#line 83
2112  if (ldv_mutex == 1) {
2113
2114  } else {
2115    {
2116#line 83
2117    ldv_blast_assert();
2118    }
2119  }
2120  {
2121#line 86
2122  atomic_value_after_dec = __VERIFIER_nondet_int();
2123  }
2124#line 89
2125  if (atomic_value_after_dec == 0) {
2126#line 92
2127    ldv_mutex = 2;
2128#line 94
2129    return (1);
2130  } else {
2131
2132  }
2133#line 98
2134  return (0);
2135}
2136}
2137#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2138void mutex_lock(struct mutex *lock ) 
2139{ 
2140
2141  {
2142#line 108
2143  if (ldv_mutex == 1) {
2144
2145  } else {
2146    {
2147#line 108
2148    ldv_blast_assert();
2149    }
2150  }
2151#line 110
2152  ldv_mutex = 2;
2153#line 111
2154  return;
2155}
2156}
2157#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2158int mutex_trylock(struct mutex *lock ) 
2159{ int nondetermined ;
2160
2161  {
2162#line 121
2163  if (ldv_mutex == 1) {
2164
2165  } else {
2166    {
2167#line 121
2168    ldv_blast_assert();
2169    }
2170  }
2171  {
2172#line 124
2173  nondetermined = __VERIFIER_nondet_int();
2174  }
2175#line 127
2176  if (nondetermined) {
2177#line 130
2178    ldv_mutex = 2;
2179#line 132
2180    return (1);
2181  } else {
2182#line 137
2183    return (0);
2184  }
2185}
2186}
2187#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2188void mutex_unlock(struct mutex *lock ) 
2189{ 
2190
2191  {
2192#line 147
2193  if (ldv_mutex == 2) {
2194
2195  } else {
2196    {
2197#line 147
2198    ldv_blast_assert();
2199    }
2200  }
2201#line 149
2202  ldv_mutex = 1;
2203#line 150
2204  return;
2205}
2206}
2207#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2208void ldv_check_final_state(void) 
2209{ 
2210
2211  {
2212#line 156
2213  if (ldv_mutex == 1) {
2214
2215  } else {
2216    {
2217#line 156
2218    ldv_blast_assert();
2219    }
2220  }
2221#line 157
2222  return;
2223}
2224}
2225#line 376 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12358/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2760.c.common.c"
2226long s__builtin_expect(long val , long res ) 
2227{ 
2228
2229  {
2230#line 377
2231  return (val);
2232}
2233}