ClabureDB

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

User:	Jiri Slaby
Error type:	Reachable Error Location
Error type description:	A specified error location is reachable in some program path
File location:	ldv-linux-3.4/43_1a_cilled_safe_ok_nondet_linux-43_1a-drivers--w1--slaves--w1_ds2408.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file:	3357
Project:	SV-COMP 2013
Project version:	2.6.28
Tools:	Manual Work
Entered:	2013-01-17 16:57:54 UTC

ClabureDB: Classified Bug-Reports Database

Project: SV-COMP 2013

Showing error 1336

Source: