ClabureDB: Classified Bug-Reports Database

   /* Generated by CIL v. 1.3.7 */
   /* print_CIL_Input is true */
   
   #line 23 "include/asm-generic/int-ll64.h"
   typedef unsigned short __u16;
   #line 26 "include/asm-generic/int-ll64.h"
   typedef unsigned int __u32;
   #line 30 "include/asm-generic/int-ll64.h"
   typedef unsigned long long __u64;
  #line 43 "include/asm-generic/int-ll64.h"
  typedef unsigned char u8;
  #line 45 "include/asm-generic/int-ll64.h"
  typedef short s16;
  #line 46 "include/asm-generic/int-ll64.h"
  typedef unsigned short u16;
  #line 49 "include/asm-generic/int-ll64.h"
  typedef unsigned int u32;
  #line 51 "include/asm-generic/int-ll64.h"
  typedef long long s64;
  #line 52 "include/asm-generic/int-ll64.h"
  typedef unsigned long long u64;
  #line 14 "include/asm-generic/posix_types.h"
  typedef long __kernel_long_t;
  #line 15 "include/asm-generic/posix_types.h"
  typedef unsigned long __kernel_ulong_t;
  #line 75 "include/asm-generic/posix_types.h"
  typedef __kernel_ulong_t __kernel_size_t;
  #line 76 "include/asm-generic/posix_types.h"
  typedef __kernel_long_t __kernel_ssize_t;
  #line 91 "include/asm-generic/posix_types.h"
  typedef long long __kernel_loff_t;
  #line 21 "include/linux/types.h"
  typedef __u32 __kernel_dev_t;
  #line 24 "include/linux/types.h"
  typedef __kernel_dev_t dev_t;
  #line 27 "include/linux/types.h"
  typedef unsigned short umode_t;
  #line 38 "include/linux/types.h"
  typedef _Bool bool;
  #line 54 "include/linux/types.h"
  typedef __kernel_loff_t loff_t;
  #line 63 "include/linux/types.h"
  typedef __kernel_size_t size_t;
  #line 68 "include/linux/types.h"
  typedef __kernel_ssize_t ssize_t;
  #line 202 "include/linux/types.h"
  typedef unsigned int gfp_t;
  #line 219 "include/linux/types.h"
  struct __anonstruct_atomic_t_7 {
     int counter ;
  };
  #line 219 "include/linux/types.h"
  typedef struct __anonstruct_atomic_t_7 atomic_t;
  #line 224 "include/linux/types.h"
  struct __anonstruct_atomic64_t_8 {
     long counter ;
  };
  #line 224 "include/linux/types.h"
  typedef struct __anonstruct_atomic64_t_8 atomic64_t;
  #line 229 "include/linux/types.h"
  struct list_head {
     struct list_head *next ;
     struct list_head *prev ;
  };
  #line 56 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
  struct module;
  #line 56
  struct module;
  #line 146 "include/linux/init.h"
  typedef void (*ctor_fn_t)(void);
  #line 47 "include/linux/dynamic_debug.h"
  struct device;
  #line 47
  struct device;
  #line 135 "include/linux/kernel.h"
  struct completion;
  #line 135
  struct completion;
  #line 18 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page.h"
  struct page;
  #line 18
  struct page;
  #line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
  struct task_struct;
  #line 20
  struct task_struct;
  #line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
  struct task_struct;
  #line 295 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
  struct file;
  #line 295
  struct file;
  #line 46 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
  struct page;
  #line 52
  struct task_struct;
  #line 329
  struct arch_spinlock;
  #line 329
 struct arch_spinlock;
 #line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
 struct task_struct;
 #line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
 struct task_struct;
 #line 10 "include/asm-generic/bug.h"
 struct bug_entry {
    int bug_addr_disp ;
    int file_disp ;
    unsigned short line ;
    unsigned short flags ;
 };
 #line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
 struct static_key;
 #line 234
 struct static_key;
 #line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 struct kmem_cache;
 #line 23 "include/asm-generic/atomic-long.h"
 typedef atomic64_t atomic_long_t;
 #line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 typedef u16 __ticket_t;
 #line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 typedef u32 __ticketpair_t;
 #line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 struct __raw_tickets {
    __ticket_t head ;
    __ticket_t tail ;
 };
 #line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 union __anonunion____missing_field_name_36 {
    __ticketpair_t head_tail ;
    struct __raw_tickets tickets ;
 };
 #line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 struct arch_spinlock {
    union __anonunion____missing_field_name_36 __annonCompField17 ;
 };
 #line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 typedef struct arch_spinlock arch_spinlock_t;
 #line 12 "include/linux/lockdep.h"
 struct task_struct;
 #line 20 "include/linux/spinlock_types.h"
 struct raw_spinlock {
    arch_spinlock_t raw_lock ;
    unsigned int magic ;
    unsigned int owner_cpu ;
    void *owner ;
 };
 #line 64 "include/linux/spinlock_types.h"
 union __anonunion____missing_field_name_39 {
    struct raw_spinlock rlock ;
 };
 #line 64 "include/linux/spinlock_types.h"
 struct spinlock {
    union __anonunion____missing_field_name_39 __annonCompField19 ;
 };
 #line 64 "include/linux/spinlock_types.h"
 typedef struct spinlock spinlock_t;
 #line 49 "include/linux/wait.h"
 struct __wait_queue_head {
    spinlock_t lock ;
    struct list_head task_list ;
 };
 #line 53 "include/linux/wait.h"
 typedef struct __wait_queue_head wait_queue_head_t;
 #line 55
 struct task_struct;
 #line 60 "include/linux/pageblock-flags.h"
 struct page;
 #line 48 "include/linux/mutex.h"
 struct mutex {
    atomic_t count ;
    spinlock_t wait_lock ;
    struct list_head wait_list ;
    struct task_struct *owner ;
    char const   *name ;
    void *magic ;
 };
 #line 25 "include/linux/completion.h"
 struct completion {
    unsigned int done ;
    wait_queue_head_t wait ;
 };
 #line 9 "include/linux/memory_hotplug.h"
 struct page;
 #line 202 "include/linux/ioport.h"
 struct device;
 #line 103 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mpspec.h"
 struct device;
 #line 46 "include/linux/ktime.h"
 union ktime {
    s64 tv64 ;
 };
 #line 59 "include/linux/ktime.h"
 typedef union ktime ktime_t;
 #line 10 "include/linux/timer.h"
 struct tvec_base;
 #line 10
 struct tvec_base;
 #line 12 "include/linux/timer.h"
 struct timer_list {
    struct list_head entry ;
    unsigned long expires ;
    struct tvec_base *base ;
    void (*function)(unsigned long  ) ;
    unsigned long data ;
    int slack ;
    int start_pid ;
    void *start_site ;
    char start_comm[16] ;
 };
 #line 17 "include/linux/workqueue.h"
 struct work_struct;
 #line 17
 struct work_struct;
 #line 79 "include/linux/workqueue.h"
 struct work_struct {
    atomic_long_t data ;
    struct list_head entry ;
    void (*func)(struct work_struct *work ) ;
 };
 #line 42 "include/linux/pm.h"
 struct device;
 #line 50 "include/linux/pm.h"
 struct pm_message {
    int event ;
 };
 #line 50 "include/linux/pm.h"
 typedef struct pm_message pm_message_t;
 #line 264 "include/linux/pm.h"
 struct dev_pm_ops {
    int (*prepare)(struct device *dev ) ;
    void (*complete)(struct device *dev ) ;
    int (*suspend)(struct device *dev ) ;
    int (*resume)(struct device *dev ) ;
    int (*freeze)(struct device *dev ) ;
    int (*thaw)(struct device *dev ) ;
    int (*poweroff)(struct device *dev ) ;
    int (*restore)(struct device *dev ) ;
    int (*suspend_late)(struct device *dev ) ;
    int (*resume_early)(struct device *dev ) ;
    int (*freeze_late)(struct device *dev ) ;
    int (*thaw_early)(struct device *dev ) ;
    int (*poweroff_late)(struct device *dev ) ;
    int (*restore_early)(struct device *dev ) ;
    int (*suspend_noirq)(struct device *dev ) ;
    int (*resume_noirq)(struct device *dev ) ;
    int (*freeze_noirq)(struct device *dev ) ;
    int (*thaw_noirq)(struct device *dev ) ;
    int (*poweroff_noirq)(struct device *dev ) ;
    int (*restore_noirq)(struct device *dev ) ;
    int (*runtime_suspend)(struct device *dev ) ;
    int (*runtime_resume)(struct device *dev ) ;
    int (*runtime_idle)(struct device *dev ) ;
 };
 #line 458
 enum rpm_status {
     RPM_ACTIVE = 0,
     RPM_RESUMING = 1,
     RPM_SUSPENDED = 2,
     RPM_SUSPENDING = 3
 } ;
 #line 480
 enum rpm_request {
     RPM_REQ_NONE = 0,
     RPM_REQ_IDLE = 1,
     RPM_REQ_SUSPEND = 2,
     RPM_REQ_AUTOSUSPEND = 3,
     RPM_REQ_RESUME = 4
 } ;
 #line 488
 struct wakeup_source;
 #line 488
 struct wakeup_source;
 #line 495 "include/linux/pm.h"
 struct pm_subsys_data {
    spinlock_t lock ;
    unsigned int refcount ;
 };
 #line 506
 struct dev_pm_qos_request;
 #line 506
 struct pm_qos_constraints;
 #line 506 "include/linux/pm.h"
 struct dev_pm_info {
    pm_message_t power_state ;
    unsigned int can_wakeup : 1 ;
    unsigned int async_suspend : 1 ;
    bool is_prepared : 1 ;
    bool is_suspended : 1 ;
    bool ignore_children : 1 ;
    spinlock_t lock ;
    struct list_head entry ;
    struct completion completion ;
    struct wakeup_source *wakeup ;
    bool wakeup_path : 1 ;
    struct timer_list suspend_timer ;
    unsigned long timer_expires ;
    struct work_struct work ;
    wait_queue_head_t wait_queue ;
    atomic_t usage_count ;
    atomic_t child_count ;
    unsigned int disable_depth : 3 ;
    unsigned int idle_notification : 1 ;
    unsigned int request_pending : 1 ;
    unsigned int deferred_resume : 1 ;
    unsigned int run_wake : 1 ;
    unsigned int runtime_auto : 1 ;
    unsigned int no_callbacks : 1 ;
    unsigned int irq_safe : 1 ;
    unsigned int use_autosuspend : 1 ;
    unsigned int timer_autosuspends : 1 ;
    enum rpm_request request ;
    enum rpm_status runtime_status ;
    int runtime_error ;
    int autosuspend_delay ;
    unsigned long last_busy ;
    unsigned long active_jiffies ;
    unsigned long suspended_jiffies ;
    unsigned long accounting_timestamp ;
    ktime_t suspend_time ;
    s64 max_time_suspended_ns ;
    struct dev_pm_qos_request *pq_req ;
    struct pm_subsys_data *subsys_data ;
    struct pm_qos_constraints *constraints ;
 };
 #line 564 "include/linux/pm.h"
 struct dev_pm_domain {
    struct dev_pm_ops ops ;
 };
 #line 8 "include/linux/vmalloc.h"
 struct vm_area_struct;
 #line 8
 struct vm_area_struct;
 #line 994 "include/linux/mmzone.h"
 struct page;
 #line 10 "include/linux/gfp.h"
 struct vm_area_struct;
 #line 29 "include/linux/sysctl.h"
 struct completion;
 #line 49 "include/linux/kmod.h"
 struct file;
 #line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
 struct task_struct;
 #line 18 "include/linux/elf.h"
 typedef __u64 Elf64_Addr;
 #line 19 "include/linux/elf.h"
 typedef __u16 Elf64_Half;
 #line 23 "include/linux/elf.h"
 typedef __u32 Elf64_Word;
 #line 24 "include/linux/elf.h"
 typedef __u64 Elf64_Xword;
 #line 194 "include/linux/elf.h"
 struct elf64_sym {
    Elf64_Word st_name ;
    unsigned char st_info ;
    unsigned char st_other ;
    Elf64_Half st_shndx ;
    Elf64_Addr st_value ;
    Elf64_Xword st_size ;
 };
 #line 194 "include/linux/elf.h"
 typedef struct elf64_sym Elf64_Sym;
 #line 438
 struct file;
 #line 20 "include/linux/kobject_ns.h"
 struct sock;
 #line 20
 struct sock;
 #line 21
 struct kobject;
 #line 21
 struct kobject;
 #line 27
 enum kobj_ns_type {
     KOBJ_NS_TYPE_NONE = 0,
     KOBJ_NS_TYPE_NET = 1,
     KOBJ_NS_TYPES = 2
 } ;
 #line 40 "include/linux/kobject_ns.h"
 struct kobj_ns_type_operations {
    enum kobj_ns_type type ;
    void *(*grab_current_ns)(void) ;
    void const   *(*netlink_ns)(struct sock *sk ) ;
    void const   *(*initial_ns)(void) ;
    void (*drop_ns)(void * ) ;
 };
 #line 22 "include/linux/sysfs.h"
 struct kobject;
 #line 23
 struct module;
 #line 24
 enum kobj_ns_type;
 #line 26 "include/linux/sysfs.h"
 struct attribute {
    char const   *name ;
    umode_t mode ;
 };
 #line 56 "include/linux/sysfs.h"
 struct attribute_group {
    char const   *name ;
    umode_t (*is_visible)(struct kobject * , struct attribute * , int  ) ;
    struct attribute **attrs ;
 };
 #line 85
 struct file;
 #line 86
 struct vm_area_struct;
 #line 88 "include/linux/sysfs.h"
 struct bin_attribute {
    struct attribute attr ;
    size_t size ;
    void *private ;
    ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
                    loff_t  , size_t  ) ;
    ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
                     loff_t  , size_t  ) ;
    int (*mmap)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ) ;
 };
 #line 112 "include/linux/sysfs.h"
 struct sysfs_ops {
    ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
    ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
    void const   *(*namespace)(struct kobject * , struct attribute  const  * ) ;
 };
 #line 118
 struct sysfs_dirent;
 #line 118
 struct sysfs_dirent;
 #line 22 "include/linux/kref.h"
 struct kref {
    atomic_t refcount ;
 };
 #line 60 "include/linux/kobject.h"
 struct kset;
 #line 60
 struct kobj_type;
 #line 60 "include/linux/kobject.h"
 struct kobject {
    char const   *name ;
    struct list_head entry ;
    struct kobject *parent ;
    struct kset *kset ;
    struct kobj_type *ktype ;
    struct sysfs_dirent *sd ;
    struct kref kref ;
    unsigned int state_initialized : 1 ;
    unsigned int state_in_sysfs : 1 ;
    unsigned int state_add_uevent_sent : 1 ;
    unsigned int state_remove_uevent_sent : 1 ;
    unsigned int uevent_suppress : 1 ;
 };
 #line 108 "include/linux/kobject.h"
 struct kobj_type {
    void (*release)(struct kobject *kobj ) ;
    struct sysfs_ops  const  *sysfs_ops ;
    struct attribute **default_attrs ;
    struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject *kobj ) ;
    void const   *(*namespace)(struct kobject *kobj ) ;
 };
 #line 116 "include/linux/kobject.h"
 struct kobj_uevent_env {
    char *envp[32] ;
    int envp_idx ;
    char buf[2048] ;
    int buflen ;
 };
 #line 123 "include/linux/kobject.h"
 struct kset_uevent_ops {
    int (* const  filter)(struct kset *kset , struct kobject *kobj ) ;
    char const   *(* const  name)(struct kset *kset , struct kobject *kobj ) ;
    int (* const  uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
 };
 #line 140
 struct sock;
 #line 159 "include/linux/kobject.h"
 struct kset {
    struct list_head list ;
    spinlock_t list_lock ;
    struct kobject kobj ;
    struct kset_uevent_ops  const  *uevent_ops ;
 };
 #line 39 "include/linux/moduleparam.h"
 struct kernel_param;
 #line 39
 struct kernel_param;
 #line 41 "include/linux/moduleparam.h"
 struct kernel_param_ops {
    int (*set)(char const   *val , struct kernel_param  const  *kp ) ;
    int (*get)(char *buffer , struct kernel_param  const  *kp ) ;
    void (*free)(void *arg ) ;
 };
 #line 50
 struct kparam_string;
 #line 50
 struct kparam_array;
 #line 50 "include/linux/moduleparam.h"
 union __anonunion____missing_field_name_199 {
    void *arg ;
    struct kparam_string  const  *str ;
    struct kparam_array  const  *arr ;
 };
 #line 50 "include/linux/moduleparam.h"
 struct kernel_param {
    char const   *name ;
    struct kernel_param_ops  const  *ops ;
    u16 perm ;
    s16 level ;
    union __anonunion____missing_field_name_199 __annonCompField32 ;
 };
 #line 63 "include/linux/moduleparam.h"
 struct kparam_string {
    unsigned int maxlen ;
    char *string ;
 };
 #line 69 "include/linux/moduleparam.h"
 struct kparam_array {
    unsigned int max ;
    unsigned int elemsize ;
    unsigned int *num ;
    struct kernel_param_ops  const  *ops ;
    void *elem ;
 };
 #line 445
 struct module;
 #line 80 "include/linux/jump_label.h"
 struct module;
 #line 143 "include/linux/jump_label.h"
 struct static_key {
    atomic_t enabled ;
 };
 #line 22 "include/linux/tracepoint.h"
 struct module;
 #line 23
 struct tracepoint;
 #line 23
 struct tracepoint;
 #line 25 "include/linux/tracepoint.h"
 struct tracepoint_func {
    void *func ;
    void *data ;
 };
 #line 30 "include/linux/tracepoint.h"
 struct tracepoint {
    char const   *name ;
    struct static_key key ;
    void (*regfunc)(void) ;
    void (*unregfunc)(void) ;
    struct tracepoint_func *funcs ;
 };
 #line 19 "include/linux/export.h"
 struct kernel_symbol {
    unsigned long value ;
    char const   *name ;
 };
 #line 8 "include/asm-generic/module.h"
 struct mod_arch_specific {
 
 };
 #line 35 "include/linux/module.h"
 struct module;
 #line 37
 struct module_param_attrs;
 #line 37 "include/linux/module.h"
 struct module_kobject {
    struct kobject kobj ;
    struct module *mod ;
    struct kobject *drivers_dir ;
    struct module_param_attrs *mp ;
 };
 #line 44 "include/linux/module.h"
 struct module_attribute {
    struct attribute attr ;
    ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
    ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const   * ,
                     size_t count ) ;
    void (*setup)(struct module * , char const   * ) ;
    int (*test)(struct module * ) ;
    void (*free)(struct module * ) ;
 };
 #line 71
 struct exception_table_entry;
 #line 71
 struct exception_table_entry;
 #line 199
 enum module_state {
     MODULE_STATE_LIVE = 0,
     MODULE_STATE_COMING = 1,
     MODULE_STATE_GOING = 2
 } ;
 #line 215 "include/linux/module.h"
 struct module_ref {
    unsigned long incs ;
    unsigned long decs ;
 } __attribute__((__aligned__((2) *  (sizeof(unsigned long )) ))) ;
 #line 220
 struct module_sect_attrs;
 #line 220
 struct module_notes_attrs;
 #line 220
 struct ftrace_event_call;
 #line 220 "include/linux/module.h"
 struct module {
    enum module_state state ;
    struct list_head list ;
    char name[64UL - sizeof(unsigned long )] ;
    struct module_kobject mkobj ;
    struct module_attribute *modinfo_attrs ;
    char const   *version ;
    char const   *srcversion ;
    struct kobject *holders_dir ;
    struct kernel_symbol  const  *syms ;
    unsigned long const   *crcs ;
    unsigned int num_syms ;
    struct kernel_param *kp ;
    unsigned int num_kp ;
    unsigned int num_gpl_syms ;
    struct kernel_symbol  const  *gpl_syms ;
    unsigned long const   *gpl_crcs ;
    struct kernel_symbol  const  *unused_syms ;
    unsigned long const   *unused_crcs ;
    unsigned int num_unused_syms ;
    unsigned int num_unused_gpl_syms ;
    struct kernel_symbol  const  *unused_gpl_syms ;
    unsigned long const   *unused_gpl_crcs ;
    struct kernel_symbol  const  *gpl_future_syms ;
    unsigned long const   *gpl_future_crcs ;
    unsigned int num_gpl_future_syms ;
    unsigned int num_exentries ;
    struct exception_table_entry *extable ;
    int (*init)(void) ;
    void *module_init ;
    void *module_core ;
    unsigned int init_size ;
    unsigned int core_size ;
    unsigned int init_text_size ;
    unsigned int core_text_size ;
    unsigned int init_ro_size ;
    unsigned int core_ro_size ;
    struct mod_arch_specific arch ;
    unsigned int taints ;
    unsigned int num_bugs ;
    struct list_head bug_list ;
    struct bug_entry *bug_table ;
    Elf64_Sym *symtab ;
    Elf64_Sym *core_symtab ;
    unsigned int num_symtab ;
    unsigned int core_num_syms ;
    char *strtab ;
    char *core_strtab ;
    struct module_sect_attrs *sect_attrs ;
    struct module_notes_attrs *notes_attrs ;
    char *args ;
    void *percpu ;
    unsigned int percpu_size ;
    unsigned int num_tracepoints ;
    struct tracepoint * const  *tracepoints_ptrs ;
    unsigned int num_trace_bprintk_fmt ;
    char const   **trace_bprintk_fmt_start ;
    struct ftrace_event_call **trace_events ;
    unsigned int num_trace_events ;
    struct list_head source_list ;
    struct list_head target_list ;
    struct task_struct *waiter ;
    void (*exit)(void) ;
    struct module_ref *refptr ;
    ctor_fn_t *ctors ;
    unsigned int num_ctors ;
 };
 #line 19 "include/linux/klist.h"
 struct klist_node;
 #line 19
 struct klist_node;
 #line 39 "include/linux/klist.h"
 struct klist_node {
    void *n_klist ;
    struct list_head n_node ;
    struct kref n_ref ;
 };
 #line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 struct dma_map_ops;
 #line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 struct dev_archdata {
    void *acpi_handle ;
    struct dma_map_ops *dma_ops ;
    void *iommu ;
 };
 #line 28 "include/linux/device.h"
 struct device;
 #line 29
 struct device_private;
 #line 29
 struct device_private;
 #line 30
 struct device_driver;
 #line 30
 struct device_driver;
 #line 31
 struct driver_private;
 #line 31
 struct driver_private;
 #line 32
 struct module;
 #line 33
 struct class;
 #line 33
 struct class;
 #line 34
 struct subsys_private;
 #line 34
 struct subsys_private;
 #line 35
 struct bus_type;
 #line 35
 struct bus_type;
 #line 36
 struct device_node;
 #line 36
 struct device_node;
 #line 37
 struct iommu_ops;
 #line 37
 struct iommu_ops;
 #line 39 "include/linux/device.h"
 struct bus_attribute {
    struct attribute attr ;
    ssize_t (*show)(struct bus_type *bus , char *buf ) ;
    ssize_t (*store)(struct bus_type *bus , char const   *buf , size_t count ) ;
 };
 #line 89
 struct device_attribute;
 #line 89
 struct driver_attribute;
 #line 89 "include/linux/device.h"
 struct bus_type {
    char const   *name ;
    char const   *dev_name ;
    struct device *dev_root ;
    struct bus_attribute *bus_attrs ;
    struct device_attribute *dev_attrs ;
    struct driver_attribute *drv_attrs ;
    int (*match)(struct device *dev , struct device_driver *drv ) ;
    int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
    int (*probe)(struct device *dev ) ;
    int (*remove)(struct device *dev ) ;
    void (*shutdown)(struct device *dev ) ;
    int (*suspend)(struct device *dev , pm_message_t state ) ;
    int (*resume)(struct device *dev ) ;
    struct dev_pm_ops  const  *pm ;
    struct iommu_ops *iommu_ops ;
    struct subsys_private *p ;
 };
 #line 127
 struct device_type;
 #line 214
 struct of_device_id;
 #line 214 "include/linux/device.h"
 struct device_driver {
    char const   *name ;
    struct bus_type *bus ;
    struct module *owner ;
    char const   *mod_name ;
    bool suppress_bind_attrs ;
    struct of_device_id  const  *of_match_table ;
    int (*probe)(struct device *dev ) ;
    int (*remove)(struct device *dev ) ;
    void (*shutdown)(struct device *dev ) ;
    int (*suspend)(struct device *dev , pm_message_t state ) ;
    int (*resume)(struct device *dev ) ;
    struct attribute_group  const  **groups ;
    struct dev_pm_ops  const  *pm ;
    struct driver_private *p ;
 };
 #line 249 "include/linux/device.h"
 struct driver_attribute {
    struct attribute attr ;
    ssize_t (*show)(struct device_driver *driver , char *buf ) ;
    ssize_t (*store)(struct device_driver *driver , char const   *buf , size_t count ) ;
 };
 #line 330
 struct class_attribute;
 #line 330 "include/linux/device.h"
 struct class {
    char const   *name ;
    struct module *owner ;
    struct class_attribute *class_attrs ;
    struct device_attribute *dev_attrs ;
    struct bin_attribute *dev_bin_attrs ;
    struct kobject *dev_kobj ;
    int (*dev_uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
    char *(*devnode)(struct device *dev , umode_t *mode ) ;
    void (*class_release)(struct class *class ) ;
    void (*dev_release)(struct device *dev ) ;
    int (*suspend)(struct device *dev , pm_message_t state ) ;
    int (*resume)(struct device *dev ) ;
    struct kobj_ns_type_operations  const  *ns_type ;
    void const   *(*namespace)(struct device *dev ) ;
    struct dev_pm_ops  const  *pm ;
    struct subsys_private *p ;
 };
 #line 397 "include/linux/device.h"
 struct class_attribute {
    struct attribute attr ;
    ssize_t (*show)(struct class *class , struct class_attribute *attr , char *buf ) ;
    ssize_t (*store)(struct class *class , struct class_attribute *attr , char const   *buf ,
                     size_t count ) ;
    void const   *(*namespace)(struct class *class , struct class_attribute  const  *attr ) ;
 };
 #line 465 "include/linux/device.h"
 struct device_type {
    char const   *name ;
    struct attribute_group  const  **groups ;
    int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
    char *(*devnode)(struct device *dev , umode_t *mode ) ;
    void (*release)(struct device *dev ) ;
    struct dev_pm_ops  const  *pm ;
 };
 #line 476 "include/linux/device.h"
 struct device_attribute {
    struct attribute attr ;
    ssize_t (*show)(struct device *dev , struct device_attribute *attr , char *buf ) ;
    ssize_t (*store)(struct device *dev , struct device_attribute *attr , char const   *buf ,
                     size_t count ) ;
 };
 #line 559 "include/linux/device.h"
 struct device_dma_parameters {
    unsigned int max_segment_size ;
    unsigned long segment_boundary_mask ;
 };
 #line 627
 struct dma_coherent_mem;
 #line 627 "include/linux/device.h"
 struct device {
    struct device *parent ;
    struct device_private *p ;
    struct kobject kobj ;
    char const   *init_name ;
    struct device_type  const  *type ;
    struct mutex mutex ;
    struct bus_type *bus ;
    struct device_driver *driver ;
    void *platform_data ;
    struct dev_pm_info power ;
    struct dev_pm_domain *pm_domain ;
    int numa_node ;
    u64 *dma_mask ;
    u64 coherent_dma_mask ;
    struct device_dma_parameters *dma_parms ;
    struct list_head dma_pools ;
    struct dma_coherent_mem *dma_mem ;
    struct dev_archdata archdata ;
    struct device_node *of_node ;
    dev_t devt ;
    u32 id ;
    spinlock_t devres_lock ;
    struct list_head devres_head ;
    struct klist_node knode_class ;
    struct class *class ;
    struct attribute_group  const  **groups ;
    void (*release)(struct device *dev ) ;
 };
 #line 43 "include/linux/pm_wakeup.h"
 struct wakeup_source {
    char const   *name ;
    struct list_head entry ;
    spinlock_t lock ;
    struct timer_list timer ;
    unsigned long timer_expires ;
    ktime_t total_time ;
    ktime_t max_time ;
    ktime_t last_time ;
    unsigned long event_count ;
    unsigned long active_count ;
    unsigned long relax_count ;
    unsigned long hit_count ;
    unsigned int active : 1 ;
 };
 #line 46 "include/linux/slub_def.h"
 struct kmem_cache_cpu {
    void **freelist ;
    unsigned long tid ;
    struct page *page ;
    struct page *partial ;
    int node ;
    unsigned int stat[26] ;
 };
 #line 57 "include/linux/slub_def.h"
 struct kmem_cache_node {
    spinlock_t list_lock ;
    unsigned long nr_partial ;
    struct list_head partial ;
    atomic_long_t nr_slabs ;
    atomic_long_t total_objects ;
    struct list_head full ;
 };
 #line 73 "include/linux/slub_def.h"
 struct kmem_cache_order_objects {
    unsigned long x ;
 };
 #line 80 "include/linux/slub_def.h"
 struct kmem_cache {
    struct kmem_cache_cpu *cpu_slab ;
    unsigned long flags ;
    unsigned long min_partial ;
    int size ;
    int objsize ;
    int offset ;
    int cpu_partial ;
    struct kmem_cache_order_objects oo ;
    struct kmem_cache_order_objects max ;
    struct kmem_cache_order_objects min ;
    gfp_t allocflags ;
    int refcount ;
    void (*ctor)(void * ) ;
    int inuse ;
    int align ;
    int reserved ;
    char const   *name ;
    struct list_head list ;
    struct kobject kobj ;
    int remote_node_defrag_ratio ;
    struct kmem_cache_node *node[1 << 10] ;
 };
 #line 25 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1.h"
 struct w1_reg_num {
    __u64 family : 8 ;
    __u64 id : 48 ;
    __u64 crc : 8 ;
 };
 #line 46 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1_family.h"
 struct w1_slave;
 #line 46
 struct w1_slave;
 #line 48 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1_family.h"
 struct w1_family_ops {
    int (*add_slave)(struct w1_slave * ) ;
    void (*remove_slave)(struct w1_slave * ) ;
 };
 #line 54 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1_family.h"
 struct w1_family {
    struct list_head family_entry ;
    u8 fid ;
    struct w1_family_ops *fops ;
    atomic_t refcnt ;
 };
 #line 62 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1.h"
 struct w1_master;
 #line 62 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1.h"
 struct w1_slave {
    struct module *owner ;
    unsigned char name[32] ;
    struct list_head w1_slave_entry ;
    struct w1_reg_num reg_num ;
    atomic_t refcnt ;
    u8 rom[9] ;
    u32 flags ;
    int ttl ;
    struct w1_master *master ;
    struct w1_family *family ;
    void *family_data ;
    struct device dev ;
    struct completion released ;
 };
 #line 90 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1.h"
 struct w1_bus_master {
    void *data ;
    u8 (*read_bit)(void * ) ;
    void (*write_bit)(void * , u8  ) ;
    u8 (*touch_bit)(void * , u8  ) ;
    u8 (*read_byte)(void * ) ;
    void (*write_byte)(void * , u8  ) ;
    u8 (*read_block)(void * , u8 * , int  ) ;
    void (*write_block)(void * , u8 const   * , int  ) ;
    u8 (*triplet)(void * , u8  ) ;
    u8 (*reset_bus)(void * ) ;
    u8 (*set_pullup)(void * , int  ) ;
    void (*search)(void * , struct w1_master * , u8  , void (*)(struct w1_master * ,
                                                                u64  ) ) ;
 };
 #line 158 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1.h"
 struct w1_master {
    struct list_head w1_master_entry ;
    struct module *owner ;
    unsigned char name[32] ;
    struct list_head slist ;
    int max_slave_count ;
    int slave_count ;
    unsigned long attempts ;
    int slave_ttl ;
    int initialized ;
    u32 id ;
    int search_count ;
    atomic_t refcnt ;
    void *priv ;
    int priv_size ;
    int enable_pullup ;
    int pullup_duration ;
    struct task_struct *thread ;
    struct mutex mutex ;
   struct device_driver *driver ;
   struct device dev ;
   struct w1_bus_master *bus_master ;
   u32 seq ;
};
#line 47 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12357/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2433.c.common.c"
struct w1_f23_data {
   u8 memory[512] ;
   u32 validcrc ;
};
#line 1 "<compiler builtins>"

#line 1
long __builtin_expect(long val , long res ) ;
#line 60 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/string_64.h"
extern int memcmp(void const   *cs , void const   *ct , unsigned long count ) ;
#line 152 "include/linux/mutex.h"
void mutex_lock(struct mutex *lock ) ;
#line 153
int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) ;
#line 154
int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) ;
#line 168
int mutex_trylock(struct mutex *lock ) ;
#line 169
void mutex_unlock(struct mutex *lock ) ;
#line 170
int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
#line 140 "include/linux/sysfs.h"
extern int __attribute__((__warn_unused_result__))  sysfs_create_bin_file(struct kobject *kobj ,
                                                                          struct bin_attribute  const  *attr ) ;
#line 142
extern void sysfs_remove_bin_file(struct kobject *kobj , struct bin_attribute  const  *attr ) ;
#line 67 "include/linux/module.h"
int init_module(void) ;
#line 68
void cleanup_module(void) ;
#line 891 "include/linux/device.h"
extern int ( /* format attribute */  dev_err)(struct device  const  *dev , char const   *fmt 
                                              , ...) ;
#line 46 "include/linux/delay.h"
extern void msleep(unsigned int msecs ) ;
#line 161 "include/linux/slab.h"
extern void kfree(void const   * ) ;
#line 221 "include/linux/slub_def.h"
extern void *__kmalloc(size_t size , gfp_t flags ) ;
#line 268
__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
                                                                    gfp_t flags )  __attribute__((__no_instrument_function__)) ;
#line 268 "include/linux/slub_def.h"
__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
                                                                    gfp_t flags ) 
{ void *tmp___2 ;

  {
  {
#line 283
  tmp___2 = __kmalloc(size, flags);
  }
#line 283
  return (tmp___2);
}
}
#line 349 "include/linux/slab.h"
__inline static void *kzalloc(size_t size , gfp_t flags )  __attribute__((__no_instrument_function__)) ;
#line 349 "include/linux/slab.h"
__inline static void *kzalloc(size_t size , gfp_t flags ) 
{ void *tmp ;
  unsigned int __cil_tmp4 ;

  {
  {
#line 351
  __cil_tmp4 = flags | 32768U;
#line 351
  tmp = kmalloc(size, __cil_tmp4);
  }
#line 351
  return (tmp);
}
}
#line 22 "include/linux/crc16.h"
extern u16 crc16(u16 crc , u8 const   *buffer , size_t len ) ;
#line 69 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1_family.h"
extern void w1_unregister_family(struct w1_family * ) ;
#line 70
extern int w1_register_family(struct w1_family * ) ;
#line 211 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1.h"
extern void w1_write_8(struct w1_master * , u8  ) ;
#line 213
extern int w1_reset_bus(struct w1_master * ) ;
#line 215
extern void w1_write_block(struct w1_master * , u8 const   * , int  ) ;
#line 217
extern u8 w1_read_block(struct w1_master * , u8 * , int  ) ;
#line 218
extern int w1_reset_select_slave(struct w1_slave *sl ) ;
#line 222
__inline static struct w1_slave *dev_to_w1_slave(struct device *dev )  __attribute__((__no_instrument_function__)) ;
#line 222 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1.h"
__inline static struct w1_slave *dev_to_w1_slave(struct device *dev ) 
{ struct device  const  *__mptr ;
  struct w1_slave *__cil_tmp3 ;
  unsigned long __cil_tmp4 ;
  unsigned long __cil_tmp5 ;
  struct device *__cil_tmp6 ;
  unsigned int __cil_tmp7 ;
  char *__cil_tmp8 ;
  char *__cil_tmp9 ;

  {
#line 224
  __mptr = (struct device  const  *)dev;
  {
#line 224
  __cil_tmp3 = (struct w1_slave *)0;
#line 224
  __cil_tmp4 = (unsigned long )__cil_tmp3;
#line 224
  __cil_tmp5 = __cil_tmp4 + 112;
#line 224
  __cil_tmp6 = (struct device *)__cil_tmp5;
#line 224
  __cil_tmp7 = (unsigned int )__cil_tmp6;
#line 224
  __cil_tmp8 = (char *)__mptr;
#line 224
  __cil_tmp9 = __cil_tmp8 - __cil_tmp7;
#line 224
  return ((struct w1_slave *)__cil_tmp9);
  }
}
}
#line 227
__inline static struct w1_slave *kobj_to_w1_slave(struct kobject *kobj )  __attribute__((__no_instrument_function__)) ;
#line 227 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1.h"
__inline static struct w1_slave *kobj_to_w1_slave(struct kobject *kobj ) 
{ struct kobject  const  *__mptr ;
  struct w1_slave *tmp ;
  struct device *__cil_tmp4 ;
  unsigned long __cil_tmp5 ;
  unsigned long __cil_tmp6 ;
  struct kobject *__cil_tmp7 ;
  unsigned int __cil_tmp8 ;
  char *__cil_tmp9 ;
  char *__cil_tmp10 ;
  struct device *__cil_tmp11 ;

  {
  {
#line 229
  __mptr = (struct kobject  const  *)kobj;
#line 229
  __cil_tmp4 = (struct device *)0;
#line 229
  __cil_tmp5 = (unsigned long )__cil_tmp4;
#line 229
  __cil_tmp6 = __cil_tmp5 + 16;
#line 229
  __cil_tmp7 = (struct kobject *)__cil_tmp6;
#line 229
  __cil_tmp8 = (unsigned int )__cil_tmp7;
#line 229
  __cil_tmp9 = (char *)__mptr;
#line 229
  __cil_tmp10 = __cil_tmp9 - __cil_tmp8;
#line 229
  __cil_tmp11 = (struct device *)__cil_tmp10;
#line 229
  tmp = dev_to_w1_slave(__cil_tmp11);
  }
#line 229
  return (tmp);
}
}
#line 30 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12357/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2433.c.common.c"
static char const   __mod_license30[12]  __attribute__((__used__, __unused__, __section__(".modinfo"),
__aligned__(1)))  = 
#line 30 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12357/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2433.c.common.c"
  {      (char const   )'l',      (char const   )'i',      (char const   )'c',      (char const   )'e', 
        (char const   )'n',      (char const   )'s',      (char const   )'e',      (char const   )'=', 
        (char const   )'G',      (char const   )'P',      (char const   )'L',      (char const   )'\000'};
#line 31 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12357/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2433.c.common.c"
static char const   __mod_author31[41]  __attribute__((__used__, __unused__, __section__(".modinfo"),
__aligned__(1)))  = 
#line 31
  {      (char const   )'a',      (char const   )'u',      (char const   )'t',      (char const   )'h', 
        (char const   )'o',      (char const   )'r',      (char const   )'=',      (char const   )'B', 
        (char const   )'e',      (char const   )'n',      (char const   )' ',      (char const   )'G', 
        (char const   )'a',      (char const   )'r',      (char const   )'d',      (char const   )'n', 
        (char const   )'e',      (char const   )'r',      (char const   )' ',      (char const   )'<', 
        (char const   )'b',      (char const   )'g',      (char const   )'a',      (char const   )'r', 
        (char const   )'d',      (char const   )'n',      (char const   )'e',      (char const   )'r', 
        (char const   )'@',      (char const   )'w',      (char const   )'a',      (char const   )'b', 
        (char const   )'t',      (char const   )'e',      (char const   )'c',      (char const   )'.', 
        (char const   )'c',      (char const   )'o',      (char const   )'m',      (char const   )'>', 
        (char const   )'\000'};
#line 32 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12357/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2433.c.common.c"
static char const   __mod_description32[55]  __attribute__((__used__, __unused__,
__section__(".modinfo"), __aligned__(1)))  = 
#line 32
  {      (char const   )'d',      (char const   )'e',      (char const   )'s',      (char const   )'c', 
        (char const   )'r',      (char const   )'i',      (char const   )'p',      (char const   )'t', 
        (char const   )'i',      (char const   )'o',      (char const   )'n',      (char const   )'=', 
        (char const   )'w',      (char const   )'1',      (char const   )' ',      (char const   )'f', 
        (char const   )'a',      (char const   )'m',      (char const   )'i',      (char const   )'l', 
        (char const   )'y',      (char const   )' ',      (char const   )'2',      (char const   )'3', 
        (char const   )' ',      (char const   )'d',      (char const   )'r',      (char const   )'i', 
        (char const   )'v',      (char const   )'e',      (char const   )'r',      (char const   )' ', 
        (char const   )'f',      (char const   )'o',      (char const   )'r',      (char const   )' ', 
        (char const   )'D',      (char const   )'S',      (char const   )'2',      (char const   )'4', 
        (char const   )'3',      (char const   )'3',      (char const   )',',      (char const   )' ', 
        (char const   )'4',      (char const   )'k',      (char const   )'b',      (char const   )' ', 
        (char const   )'E',      (char const   )'E',      (char const   )'P',      (char const   )'R', 
        (char const   )'O',      (char const   )'M',      (char const   )'\000'};
#line 56
__inline static size_t w1_f23_fix_count(loff_t off , size_t count , size_t size )  __attribute__((__no_instrument_function__)) ;
#line 56 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12357/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2433.c.common.c"
__inline static size_t w1_f23_fix_count(loff_t off , size_t count , size_t size ) 
{ loff_t __cil_tmp4 ;
  loff_t __cil_tmp5 ;
  loff_t __cil_tmp6 ;
  loff_t __cil_tmp7 ;
  loff_t __cil_tmp8 ;
  loff_t __cil_tmp9 ;

  {
  {
#line 58
  __cil_tmp4 = (loff_t )size;
#line 58
  if (off > __cil_tmp4) {
#line 59
    return ((size_t )0);
  } else {

  }
  }
  {
#line 61
  __cil_tmp5 = (loff_t )size;
#line 61
  __cil_tmp6 = (loff_t )count;
#line 61
  __cil_tmp7 = off + __cil_tmp6;
#line 61
  if (__cil_tmp7 > __cil_tmp5) {
    {
#line 62
    __cil_tmp8 = (loff_t )size;
#line 62
    __cil_tmp9 = __cil_tmp8 - off;
#line 62
    return ((size_t )__cil_tmp9);
    }
  } else {

  }
  }
#line 64
  return (count);
}
}
#line 68 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12357/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2433.c.common.c"
static int w1_f23_refresh_block(struct w1_slave *sl , struct w1_f23_data *data , int block ) 
{ u8 wrbuf[3] ;
  int off ;
  int tmp ;
  u16 tmp___0 ;
  int __cil_tmp8 ;
  unsigned int __cil_tmp9 ;
  unsigned long __cil_tmp10 ;
  unsigned long __cil_tmp11 ;
  u32 __cil_tmp12 ;
  unsigned long __cil_tmp13 ;
  unsigned long __cil_tmp14 ;
  unsigned long __cil_tmp15 ;
  unsigned long __cil_tmp16 ;
  unsigned long __cil_tmp17 ;
  unsigned long __cil_tmp18 ;
  int __cil_tmp19 ;
  unsigned long __cil_tmp20 ;
  unsigned long __cil_tmp21 ;
  int __cil_tmp22 ;
  unsigned long __cil_tmp23 ;
  unsigned long __cil_tmp24 ;
  struct w1_master *__cil_tmp25 ;
  unsigned long __cil_tmp26 ;
  unsigned long __cil_tmp27 ;
  u8 *__cil_tmp28 ;
  u8 const   *__cil_tmp29 ;
  unsigned long __cil_tmp30 ;
  unsigned long __cil_tmp31 ;
  struct w1_master *__cil_tmp32 ;
  unsigned long __cil_tmp33 ;
  unsigned long __cil_tmp34 ;
  unsigned long __cil_tmp35 ;
  unsigned long __cil_tmp36 ;
  u8 *__cil_tmp37 ;
  u16 __cil_tmp38 ;
  unsigned long __cil_tmp39 ;
  unsigned long __cil_tmp40 ;
  unsigned long __cil_tmp41 ;
  unsigned long __cil_tmp42 ;
  u8 *__cil_tmp43 ;
  u8 const   *__cil_tmp44 ;
  size_t __cil_tmp45 ;
  int __cil_tmp46 ;
  unsigned long __cil_tmp47 ;
  unsigned long __cil_tmp48 ;
  int __cil_tmp49 ;
  unsigned int __cil_tmp50 ;
  unsigned long __cil_tmp51 ;
  unsigned long __cil_tmp52 ;
  u32 __cil_tmp53 ;

  {
#line 72
  off = block * 32;
  {
#line 74
  __cil_tmp8 = 1 << block;
#line 74
  __cil_tmp9 = (unsigned int )__cil_tmp8;
#line 74
  __cil_tmp10 = (unsigned long )data;
#line 74
  __cil_tmp11 = __cil_tmp10 + 512;
#line 74
  __cil_tmp12 = *((u32 *)__cil_tmp11);
#line 74
  if (__cil_tmp12 & __cil_tmp9) {
#line 75
    return (0);
  } else {

  }
  }
  {
#line 77
  tmp = w1_reset_select_slave(sl);
  }
#line 77
  if (tmp) {
#line 78
    __cil_tmp13 = (unsigned long )data;
#line 78
    __cil_tmp14 = __cil_tmp13 + 512;
#line 78
    *((u32 *)__cil_tmp14) = (u32 )0;
#line 79
    return (-5);
  } else {

  }
  {
#line 82
  __cil_tmp15 = 0 * 1UL;
#line 82
  __cil_tmp16 = (unsigned long )(wrbuf) + __cil_tmp15;
#line 82
  *((u8 *)__cil_tmp16) = (u8 )240;
#line 83
  __cil_tmp17 = 1 * 1UL;
#line 83
  __cil_tmp18 = (unsigned long )(wrbuf) + __cil_tmp17;
#line 83
  __cil_tmp19 = off & 255;
#line 83
  *((u8 *)__cil_tmp18) = (u8 )__cil_tmp19;
#line 84
  __cil_tmp20 = 2 * 1UL;
#line 84
  __cil_tmp21 = (unsigned long )(wrbuf) + __cil_tmp20;
#line 84
  __cil_tmp22 = off >> 8;
#line 84
  *((u8 *)__cil_tmp21) = (u8 )__cil_tmp22;
#line 85
  __cil_tmp23 = (unsigned long )sl;
#line 85
  __cil_tmp24 = __cil_tmp23 + 88;
#line 85
  __cil_tmp25 = *((struct w1_master **)__cil_tmp24);
#line 85
  __cil_tmp26 = 0 * 1UL;
#line 85
  __cil_tmp27 = (unsigned long )(wrbuf) + __cil_tmp26;
#line 85
  __cil_tmp28 = (u8 *)__cil_tmp27;
#line 85
  __cil_tmp29 = (u8 const   *)__cil_tmp28;
#line 85
  w1_write_block(__cil_tmp25, __cil_tmp29, 3);
#line 86
  __cil_tmp30 = (unsigned long )sl;
#line 86
  __cil_tmp31 = __cil_tmp30 + 88;
#line 86
  __cil_tmp32 = *((struct w1_master **)__cil_tmp31);
#line 86
  __cil_tmp33 = off * 1UL;
#line 86
  __cil_tmp34 = 0 + __cil_tmp33;
#line 86
  __cil_tmp35 = (unsigned long )data;
#line 86
  __cil_tmp36 = __cil_tmp35 + __cil_tmp34;
#line 86
  __cil_tmp37 = (u8 *)__cil_tmp36;
#line 86
  w1_read_block(__cil_tmp32, __cil_tmp37, 32);
#line 89
  __cil_tmp38 = (u16 )0;
#line 89
  __cil_tmp39 = off * 1UL;
#line 89
  __cil_tmp40 = 0 + __cil_tmp39;
#line 89
  __cil_tmp41 = (unsigned long )data;
#line 89
  __cil_tmp42 = __cil_tmp41 + __cil_tmp40;
#line 89
  __cil_tmp43 = (u8 *)__cil_tmp42;
#line 89
  __cil_tmp44 = (u8 const   *)__cil_tmp43;
#line 89
  __cil_tmp45 = (size_t )32;
#line 89
  tmp___0 = crc16(__cil_tmp38, __cil_tmp44, __cil_tmp45);
  }
  {
#line 89
  __cil_tmp46 = (int )tmp___0;
#line 89
  if (__cil_tmp46 == 45057) {
#line 90
    __cil_tmp47 = (unsigned long )data;
#line 90
    __cil_tmp48 = __cil_tmp47 + 512;
#line 90
    __cil_tmp49 = 1 << block;
#line 90
    __cil_tmp50 = (unsigned int )__cil_tmp49;
#line 90
    __cil_tmp51 = (unsigned long )data;
#line 90
    __cil_tmp52 = __cil_tmp51 + 512;
#line 90
    __cil_tmp53 = *((u32 *)__cil_tmp52);
#line 90
    *((u32 *)__cil_tmp48) = __cil_tmp53 | __cil_tmp50;
  } else {

  }
  }
#line 92
  return (0);
}
}
#line 96 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12357/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2433.c.common.c"
static ssize_t w1_f23_read_bin(struct file *filp , struct kobject *kobj , struct bin_attribute *bin_attr ,
                               char *buf , loff_t off , size_t count ) 
{ struct w1_slave *sl ;
  struct w1_slave *tmp ;
  struct w1_f23_data *data ;
  int i ;
  int min_page ;
  int max_page ;
  int tmp___0 ;
  size_t __len ;
  void *__ret ;
  unsigned long __cil_tmp16 ;
  unsigned long __cil_tmp17 ;
  void *__cil_tmp18 ;
  size_t __cil_tmp19 ;
  unsigned long __cil_tmp20 ;
  unsigned long __cil_tmp21 ;
  struct w1_master *__cil_tmp22 ;
  unsigned long __cil_tmp23 ;
  unsigned long __cil_tmp24 ;
  struct mutex *__cil_tmp25 ;
  loff_t __cil_tmp26 ;
  loff_t __cil_tmp27 ;
  loff_t __cil_tmp28 ;
  loff_t __cil_tmp29 ;
  loff_t __cil_tmp30 ;
  void *__cil_tmp31 ;
  unsigned long __cil_tmp32 ;
  unsigned long __cil_tmp33 ;
  unsigned long __cil_tmp34 ;
  unsigned long __cil_tmp35 ;
  u8 *__cil_tmp36 ;
  void const   *__cil_tmp37 ;
  unsigned long __cil_tmp38 ;
  unsigned long __cil_tmp39 ;
  struct w1_master *__cil_tmp40 ;
  unsigned long __cil_tmp41 ;
  unsigned long __cil_tmp42 ;
  struct mutex *__cil_tmp43 ;

  {
  {
#line 100
  tmp = kobj_to_w1_slave(kobj);
#line 100
  sl = tmp;
#line 102
  __cil_tmp16 = (unsigned long )sl;
#line 102
  __cil_tmp17 = __cil_tmp16 + 104;
#line 102
  __cil_tmp18 = *((void **)__cil_tmp17);
#line 102
  data = (struct w1_f23_data *)__cil_tmp18;
#line 108
  __cil_tmp19 = (size_t )512;
#line 108
  count = w1_f23_fix_count(off, count, __cil_tmp19);
  }
#line 108
  if (count == 0UL) {
#line 109
    return ((ssize_t )0);
  } else {

  }
  {
#line 111
  __cil_tmp20 = (unsigned long )sl;
#line 111
  __cil_tmp21 = __cil_tmp20 + 88;
#line 111
  __cil_tmp22 = *((struct w1_master **)__cil_tmp21);
#line 111
  __cil_tmp23 = (unsigned long )__cil_tmp22;
#line 111
  __cil_tmp24 = __cil_tmp23 + 144;
#line 111
  __cil_tmp25 = (struct mutex *)__cil_tmp24;
#line 111
  mutex_lock(__cil_tmp25);
#line 115
  __cil_tmp26 = off >> 5;
#line 115
  min_page = (int )__cil_tmp26;
#line 116
  __cil_tmp27 = (loff_t )count;
#line 116
  __cil_tmp28 = off + __cil_tmp27;
#line 116
  __cil_tmp29 = __cil_tmp28 - 1LL;
#line 116
  __cil_tmp30 = __cil_tmp29 >> 5;
#line 116
  max_page = (int )__cil_tmp30;
#line 117
  i = min_page;
  }
  {
#line 117
  while (1) {
    while_continue: /* CIL Label */ ;
#line 117
    if (i <= max_page) {

    } else {
#line 117
      goto while_break;
    }
    {
#line 118
    tmp___0 = w1_f23_refresh_block(sl, data, i);
    }
#line 118
    if (tmp___0) {
#line 119
      count = (size_t )-5;
#line 120
      goto out_up;
    } else {

    }
#line 117
    i = i + 1;
  }
  while_break: /* CIL Label */ ;
  }
  {
#line 123
  __len = count;
#line 123
  __cil_tmp31 = (void *)buf;
#line 123
  __cil_tmp32 = off * 1UL;
#line 123
  __cil_tmp33 = 0 + __cil_tmp32;
#line 123
  __cil_tmp34 = (unsigned long )data;
#line 123
  __cil_tmp35 = __cil_tmp34 + __cil_tmp33;
#line 123
  __cil_tmp36 = (u8 *)__cil_tmp35;
#line 123
  __cil_tmp37 = (void const   *)__cil_tmp36;
#line 123
  __ret = __builtin_memcpy(__cil_tmp31, __cil_tmp37, __len);
  }
  out_up: 
  {
#line 142
  __cil_tmp38 = (unsigned long )sl;
#line 142
  __cil_tmp39 = __cil_tmp38 + 88;
#line 142
  __cil_tmp40 = *((struct w1_master **)__cil_tmp39);
#line 142
  __cil_tmp41 = (unsigned long )__cil_tmp40;
#line 142
  __cil_tmp42 = __cil_tmp41 + 144;
#line 142
  __cil_tmp43 = (struct mutex *)__cil_tmp42;
#line 142
  mutex_unlock(__cil_tmp43);
  }
#line 144
  return ((ssize_t )count);
}
}
#line 159 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12357/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2433.c.common.c"
static int w1_f23_write(struct w1_slave *sl , int addr , int len , u8 const   *data ) 
{ struct w1_f23_data *f23 ;
  u8 wrbuf[4] ;
  u8 rdbuf[35] ;
  u8 es ;
  int tmp ;
  int tmp___0 ;
  int tmp___1 ;
  int tmp___2 ;
  unsigned long __cil_tmp13 ;
  unsigned long __cil_tmp14 ;
  void *__cil_tmp15 ;
  int __cil_tmp16 ;
  int __cil_tmp17 ;
  int __cil_tmp18 ;
  unsigned long __cil_tmp19 ;
  unsigned long __cil_tmp20 ;
  unsigned long __cil_tmp21 ;
  unsigned long __cil_tmp22 ;
  int __cil_tmp23 ;
  unsigned long __cil_tmp24 ;
  unsigned long __cil_tmp25 ;
  int __cil_tmp26 ;
  unsigned long __cil_tmp27 ;
  unsigned long __cil_tmp28 ;
  struct w1_master *__cil_tmp29 ;
  unsigned long __cil_tmp30 ;
  unsigned long __cil_tmp31 ;
  u8 *__cil_tmp32 ;
  u8 const   *__cil_tmp33 ;
  unsigned long __cil_tmp34 ;
  unsigned long __cil_tmp35 ;
  struct w1_master *__cil_tmp36 ;
  unsigned long __cil_tmp37 ;
  unsigned long __cil_tmp38 ;
  struct w1_master *__cil_tmp39 ;
  u8 __cil_tmp40 ;
  unsigned long __cil_tmp41 ;
  unsigned long __cil_tmp42 ;
  struct w1_master *__cil_tmp43 ;
  unsigned long __cil_tmp44 ;
  unsigned long __cil_tmp45 ;
  u8 *__cil_tmp46 ;
  int __cil_tmp47 ;
  unsigned long __cil_tmp48 ;
  unsigned long __cil_tmp49 ;
  u8 __cil_tmp50 ;
  int __cil_tmp51 ;
  unsigned long __cil_tmp52 ;
  unsigned long __cil_tmp53 ;
  u8 __cil_tmp54 ;
  int __cil_tmp55 ;
  unsigned long __cil_tmp56 ;
  unsigned long __cil_tmp57 ;
  u8 __cil_tmp58 ;
  int __cil_tmp59 ;
  unsigned long __cil_tmp60 ;
  unsigned long __cil_tmp61 ;
  u8 __cil_tmp62 ;
  int __cil_tmp63 ;
  int __cil_tmp64 ;
  unsigned long __cil_tmp65 ;
  unsigned long __cil_tmp66 ;
  u8 __cil_tmp67 ;
  int __cil_tmp68 ;
  void const   *__cil_tmp69 ;
  unsigned long __cil_tmp70 ;
  unsigned long __cil_tmp71 ;
  u8 *__cil_tmp72 ;
  void const   *__cil_tmp73 ;
  unsigned long __cil_tmp74 ;
  unsigned long __cil_tmp75 ;
  unsigned long __cil_tmp76 ;
  unsigned long __cil_tmp77 ;
  unsigned long __cil_tmp78 ;
  unsigned long __cil_tmp79 ;
  unsigned long __cil_tmp80 ;
  struct w1_master *__cil_tmp81 ;
  unsigned long __cil_tmp82 ;
  unsigned long __cil_tmp83 ;
  u8 *__cil_tmp84 ;
  u8 const   *__cil_tmp85 ;
  unsigned long __cil_tmp86 ;
  unsigned long __cil_tmp87 ;
  struct w1_master *__cil_tmp88 ;
  unsigned long __cil_tmp89 ;
  unsigned long __cil_tmp90 ;
  int __cil_tmp91 ;
  int __cil_tmp92 ;
  int __cil_tmp93 ;
  unsigned int __cil_tmp94 ;
  unsigned long __cil_tmp95 ;
  unsigned long __cil_tmp96 ;
  u32 __cil_tmp97 ;

  {
  {
#line 162
  __cil_tmp13 = (unsigned long )sl;
#line 162
  __cil_tmp14 = __cil_tmp13 + 104;
#line 162
  __cil_tmp15 = *((void **)__cil_tmp14);
#line 162
  f23 = (struct w1_f23_data *)__cil_tmp15;
#line 166
  __cil_tmp16 = addr + len;
#line 166
  __cil_tmp17 = __cil_tmp16 - 1;
#line 166
  __cil_tmp18 = __cil_tmp17 & 31;
#line 166
  es = (u8 )__cil_tmp18;
#line 169
  tmp = w1_reset_select_slave(sl);
  }
#line 169
  if (tmp) {
#line 170
    return (-1);
  } else {

  }
  {
#line 172
  __cil_tmp19 = 0 * 1UL;
#line 172
  __cil_tmp20 = (unsigned long )(wrbuf) + __cil_tmp19;
#line 172
  *((u8 *)__cil_tmp20) = (u8 )15;
#line 173
  __cil_tmp21 = 1 * 1UL;
#line 173
  __cil_tmp22 = (unsigned long )(wrbuf) + __cil_tmp21;
#line 173
  __cil_tmp23 = addr & 255;
#line 173
  *((u8 *)__cil_tmp22) = (u8 )__cil_tmp23;
#line 174
  __cil_tmp24 = 2 * 1UL;
#line 174
  __cil_tmp25 = (unsigned long )(wrbuf) + __cil_tmp24;
#line 174
  __cil_tmp26 = addr >> 8;
#line 174
  *((u8 *)__cil_tmp25) = (u8 )__cil_tmp26;
#line 176
  __cil_tmp27 = (unsigned long )sl;
#line 176
  __cil_tmp28 = __cil_tmp27 + 88;
#line 176
  __cil_tmp29 = *((struct w1_master **)__cil_tmp28);
#line 176
  __cil_tmp30 = 0 * 1UL;
#line 176
  __cil_tmp31 = (unsigned long )(wrbuf) + __cil_tmp30;
#line 176
  __cil_tmp32 = (u8 *)__cil_tmp31;
#line 176
  __cil_tmp33 = (u8 const   *)__cil_tmp32;
#line 176
  w1_write_block(__cil_tmp29, __cil_tmp33, 3);
#line 177
  __cil_tmp34 = (unsigned long )sl;
#line 177
  __cil_tmp35 = __cil_tmp34 + 88;
#line 177
  __cil_tmp36 = *((struct w1_master **)__cil_tmp35);
#line 177
  w1_write_block(__cil_tmp36, data, len);
#line 180
  tmp___0 = w1_reset_select_slave(sl);
  }
#line 180
  if (tmp___0) {
#line 181
    return (-1);
  } else {

  }
  {
#line 183
  __cil_tmp37 = (unsigned long )sl;
#line 183
  __cil_tmp38 = __cil_tmp37 + 88;
#line 183
  __cil_tmp39 = *((struct w1_master **)__cil_tmp38);
#line 183
  __cil_tmp40 = (u8 )170;
#line 183
  w1_write_8(__cil_tmp39, __cil_tmp40);
#line 184
  __cil_tmp41 = (unsigned long )sl;
#line 184
  __cil_tmp42 = __cil_tmp41 + 88;
#line 184
  __cil_tmp43 = *((struct w1_master **)__cil_tmp42);
#line 184
  __cil_tmp44 = 0 * 1UL;
#line 184
  __cil_tmp45 = (unsigned long )(rdbuf) + __cil_tmp44;
#line 184
  __cil_tmp46 = (u8 *)__cil_tmp45;
#line 184
  __cil_tmp47 = len + 3;
#line 184
  w1_read_block(__cil_tmp43, __cil_tmp46, __cil_tmp47);
  }
  {
#line 187
  __cil_tmp48 = 1 * 1UL;
#line 187
  __cil_tmp49 = (unsigned long )(wrbuf) + __cil_tmp48;
#line 187
  __cil_tmp50 = *((u8 *)__cil_tmp49);
#line 187
  __cil_tmp51 = (int )__cil_tmp50;
#line 187
  __cil_tmp52 = 0 * 1UL;
#line 187
  __cil_tmp53 = (unsigned long )(rdbuf) + __cil_tmp52;
#line 187
  __cil_tmp54 = *((u8 *)__cil_tmp53);
#line 187
  __cil_tmp55 = (int )__cil_tmp54;
#line 187
  if (__cil_tmp55 != __cil_tmp51) {
#line 189
    return (-1);
  } else {
    {
#line 187
    __cil_tmp56 = 2 * 1UL;
#line 187
    __cil_tmp57 = (unsigned long )(wrbuf) + __cil_tmp56;
#line 187
    __cil_tmp58 = *((u8 *)__cil_tmp57);
#line 187
    __cil_tmp59 = (int )__cil_tmp58;
#line 187
    __cil_tmp60 = 1 * 1UL;
#line 187
    __cil_tmp61 = (unsigned long )(rdbuf) + __cil_tmp60;
#line 187
    __cil_tmp62 = *((u8 *)__cil_tmp61);
#line 187
    __cil_tmp63 = (int )__cil_tmp62;
#line 187
    if (__cil_tmp63 != __cil_tmp59) {
#line 189
      return (-1);
    } else {
      {
#line 187
      __cil_tmp64 = (int )es;
#line 187
      __cil_tmp65 = 2 * 1UL;
#line 187
      __cil_tmp66 = (unsigned long )(rdbuf) + __cil_tmp65;
#line 187
      __cil_tmp67 = *((u8 *)__cil_tmp66);
#line 187
      __cil_tmp68 = (int )__cil_tmp67;
#line 187
      if (__cil_tmp68 != __cil_tmp64) {
#line 189
        return (-1);
      } else {
        {
#line 187
        __cil_tmp69 = (void const   *)data;
#line 187
        __cil_tmp70 = 3 * 1UL;
#line 187
        __cil_tmp71 = (unsigned long )(rdbuf) + __cil_tmp70;
#line 187
        __cil_tmp72 = (u8 *)__cil_tmp71;
#line 187
        __cil_tmp73 = (void const   *)__cil_tmp72;
#line 187
        __cil_tmp74 = (unsigned long )len;
#line 187
        tmp___1 = memcmp(__cil_tmp69, __cil_tmp73, __cil_tmp74);
        }
#line 187
        if (tmp___1 != 0) {
#line 189
          return (-1);
        } else {

        }
      }
      }
    }
    }
  }
  }
  {
#line 192
  tmp___2 = w1_reset_select_slave(sl);
  }
#line 192
  if (tmp___2) {
#line 193
    return (-1);
  } else {

  }
  {
#line 195
  __cil_tmp75 = 0 * 1UL;
#line 195
  __cil_tmp76 = (unsigned long )(wrbuf) + __cil_tmp75;
#line 195
  *((u8 *)__cil_tmp76) = (u8 )85;
#line 196
  __cil_tmp77 = 3 * 1UL;
#line 196
  __cil_tmp78 = (unsigned long )(wrbuf) + __cil_tmp77;
#line 196
  *((u8 *)__cil_tmp78) = es;
#line 197
  __cil_tmp79 = (unsigned long )sl;
#line 197
  __cil_tmp80 = __cil_tmp79 + 88;
#line 197
  __cil_tmp81 = *((struct w1_master **)__cil_tmp80);
#line 197
  __cil_tmp82 = 0 * 1UL;
#line 197
  __cil_tmp83 = (unsigned long )(wrbuf) + __cil_tmp82;
#line 197
  __cil_tmp84 = (u8 *)__cil_tmp83;
#line 197
  __cil_tmp85 = (u8 const   *)__cil_tmp84;
#line 197
  w1_write_block(__cil_tmp81, __cil_tmp85, 4);
#line 200
  msleep(5U);
#line 203
  __cil_tmp86 = (unsigned long )sl;
#line 203
  __cil_tmp87 = __cil_tmp86 + 88;
#line 203
  __cil_tmp88 = *((struct w1_master **)__cil_tmp87);
#line 203
  w1_reset_bus(__cil_tmp88);
#line 205
  __cil_tmp89 = (unsigned long )f23;
#line 205
  __cil_tmp90 = __cil_tmp89 + 512;
#line 205
  __cil_tmp91 = addr >> 5;
#line 205
  __cil_tmp92 = 1 << __cil_tmp91;
#line 205
  __cil_tmp93 = ~ __cil_tmp92;
#line 205
  __cil_tmp94 = (unsigned int )__cil_tmp93;
#line 205
  __cil_tmp95 = (unsigned long )f23;
#line 205
  __cil_tmp96 = __cil_tmp95 + 512;
#line 205
  __cil_tmp97 = *((u32 *)__cil_tmp96);
#line 205
  *((u32 *)__cil_tmp90) = __cil_tmp97 & __cil_tmp94;
  }
#line 207
  return (0);
}
}
#line 210 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12357/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2433.c.common.c"
static ssize_t w1_f23_write_bin(struct file *filp , struct kobject *kobj , struct bin_attribute *bin_attr ,
                                char *buf , loff_t off , size_t count ) 
{ struct w1_slave *sl ;
  struct w1_slave *tmp ;
  int addr ;
  int len ;
  int idx ;
  u16 tmp___0 ;
  int tmp___1 ;
  size_t __cil_tmp14 ;
  unsigned long __cil_tmp15 ;
  unsigned long __cil_tmp16 ;
  struct device *__cil_tmp17 ;
  struct device  const  *__cil_tmp18 ;
  int __cil_tmp19 ;
  unsigned long __cil_tmp20 ;
  unsigned long __cil_tmp21 ;
  struct device *__cil_tmp22 ;
  struct device  const  *__cil_tmp23 ;
  int __cil_tmp24 ;
  size_t __cil_tmp25 ;
  u16 __cil_tmp26 ;
  char *__cil_tmp27 ;
  u8 const   *__cil_tmp28 ;
  size_t __cil_tmp29 ;
  int __cil_tmp30 ;
  unsigned long __cil_tmp31 ;
  unsigned long __cil_tmp32 ;
  struct device *__cil_tmp33 ;
  struct device  const  *__cil_tmp34 ;
  int __cil_tmp35 ;
  unsigned long __cil_tmp36 ;
  unsigned long __cil_tmp37 ;
  struct w1_master *__cil_tmp38 ;
  unsigned long __cil_tmp39 ;
  unsigned long __cil_tmp40 ;
  struct mutex *__cil_tmp41 ;
  size_t __cil_tmp42 ;
  loff_t __cil_tmp43 ;
  loff_t __cil_tmp44 ;
  int __cil_tmp45 ;
  size_t __cil_tmp46 ;
  size_t __cil_tmp47 ;
  size_t __cil_tmp48 ;
  size_t __cil_tmp49 ;
  size_t __cil_tmp50 ;
  char *__cil_tmp51 ;
  u8 const   *__cil_tmp52 ;
  unsigned long __cil_tmp53 ;
  unsigned long __cil_tmp54 ;
  struct w1_master *__cil_tmp55 ;
  unsigned long __cil_tmp56 ;
  unsigned long __cil_tmp57 ;
  struct mutex *__cil_tmp58 ;

  {
  {
#line 214
  tmp = kobj_to_w1_slave(kobj);
#line 214
  sl = tmp;
#line 217
  __cil_tmp14 = (size_t )512;
#line 217
  count = w1_f23_fix_count(off, count, __cil_tmp14);
  }
#line 217
  if (count == 0UL) {
#line 218
    return ((ssize_t )0);
  } else {

  }
#line 222
  if (off & 31LL) {
    {
#line 223
    __cil_tmp15 = (unsigned long )sl;
#line 223
    __cil_tmp16 = __cil_tmp15 + 112;
#line 223
    __cil_tmp17 = (struct device *)__cil_tmp16;
#line 223
    __cil_tmp18 = (struct device  const  *)__cil_tmp17;
#line 223
    __cil_tmp19 = (int )off;
#line 223
    dev_err(__cil_tmp18, "invalid offset/count off=%d cnt=%zd\n", __cil_tmp19, count);
    }
#line 225
    return ((ssize_t )-22);
  } else
#line 222
  if (count & 31UL) {
    {
#line 223
    __cil_tmp20 = (unsigned long )sl;
#line 223
    __cil_tmp21 = __cil_tmp20 + 112;
#line 223
    __cil_tmp22 = (struct device *)__cil_tmp21;
#line 223
    __cil_tmp23 = (struct device  const  *)__cil_tmp22;
#line 223
    __cil_tmp24 = (int )off;
#line 223
    dev_err(__cil_tmp23, "invalid offset/count off=%d cnt=%zd\n", __cil_tmp24, count);
    }
#line 225
    return ((ssize_t )-22);
  } else {

  }
#line 229
  idx = 0;
  {
#line 229
  while (1) {
    while_continue: /* CIL Label */ ;
    {
#line 229
    __cil_tmp25 = (size_t )idx;
#line 229
    if (__cil_tmp25 < count) {

    } else {
#line 229
      goto while_break;
    }
    }
    {
#line 230
    __cil_tmp26 = (u16 )0;
#line 230
    __cil_tmp27 = buf + idx;
#line 230
    __cil_tmp28 = (u8 const   *)__cil_tmp27;
#line 230
    __cil_tmp29 = (size_t )32;
#line 230
    tmp___0 = crc16(__cil_tmp26, __cil_tmp28, __cil_tmp29);
    }
    {
#line 230
    __cil_tmp30 = (int )tmp___0;
#line 230
    if (__cil_tmp30 != 45057) {
      {
#line 231
      __cil_tmp31 = (unsigned long )sl;
#line 231
      __cil_tmp32 = __cil_tmp31 + 112;
#line 231
      __cil_tmp33 = (struct device *)__cil_tmp32;
#line 231
      __cil_tmp34 = (struct device  const  *)__cil_tmp33;
#line 231
      __cil_tmp35 = (int )off;
#line 231
      dev_err(__cil_tmp34, "bad CRC at offset %d\n", __cil_tmp35);
      }
#line 232
      return ((ssize_t )-22);
    } else {

    }
    }
#line 229
    idx = idx + 32;
  }
  while_break: /* CIL Label */ ;
  }
  {
#line 237
  __cil_tmp36 = (unsigned long )sl;
#line 237
  __cil_tmp37 = __cil_tmp36 + 88;
#line 237
  __cil_tmp38 = *((struct w1_master **)__cil_tmp37);
#line 237
  __cil_tmp39 = (unsigned long )__cil_tmp38;
#line 237
  __cil_tmp40 = __cil_tmp39 + 144;
#line 237
  __cil_tmp41 = (struct mutex *)__cil_tmp40;
#line 237
  mutex_lock(__cil_tmp41);
#line 240
  idx = 0;
  }
  {
#line 241
  while (1) {
    while_continue___0: /* CIL Label */ ;
    {
#line 241
    __cil_tmp42 = (size_t )idx;
#line 241
    if (__cil_tmp42 < count) {

    } else {
#line 241
      goto while_break___0;
    }
    }
#line 242
    __cil_tmp43 = (loff_t )idx;
#line 242
    __cil_tmp44 = off + __cil_tmp43;
#line 242
    addr = (int )__cil_tmp44;
#line 243
    __cil_tmp45 = addr & 31;
#line 243
    len = 32 - __cil_tmp45;
    {
#line 244
    __cil_tmp46 = (size_t )idx;
#line 244
    __cil_tmp47 = count - __cil_tmp46;
#line 244
    __cil_tmp48 = (size_t )len;
#line 244
    if (__cil_tmp48 > __cil_tmp47) {
#line 245
      __cil_tmp49 = (size_t )idx;
#line 245
      __cil_tmp50 = count - __cil_tmp49;
#line 245
      len = (int )__cil_tmp50;
    } else {

    }
    }
    {
#line 247
    __cil_tmp51 = buf + idx;
#line 247
    __cil_tmp52 = (u8 const   *)__cil_tmp51;
#line 247
    tmp___1 = w1_f23_write(sl, addr, len, __cil_tmp52);
    }
#line 247
    if (tmp___1 < 0) {
#line 248
      count = (size_t )-5;
#line 249
      goto out_up;
    } else {

    }
#line 251
    idx = idx + len;
  }
  while_break___0: /* CIL Label */ ;
  }
  out_up: 
  {
#line 255
  __cil_tmp53 = (unsigned long )sl;
#line 255
  __cil_tmp54 = __cil_tmp53 + 88;
#line 255
  __cil_tmp55 = *((struct w1_master **)__cil_tmp54);
#line 255
  __cil_tmp56 = (unsigned long )__cil_tmp55;
#line 255
  __cil_tmp57 = __cil_tmp56 + 144;
#line 255
  __cil_tmp58 = (struct mutex *)__cil_tmp57;
#line 255
  mutex_unlock(__cil_tmp58);
  }
#line 257
  return ((ssize_t )count);
}
}
#line 260 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12357/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2433.c.common.c"
static struct bin_attribute w1_f23_bin_attr  =    {{"eeprom", (umode_t )420}, (size_t )512, (void *)0, & w1_f23_read_bin, & w1_f23_write_bin,
    (int (*)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ))0};
#line 270 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12357/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2433.c.common.c"
static int w1_f23_add_slave(struct w1_slave *sl ) 
{ int err ;
  struct w1_f23_data *data ;
  void *tmp ;
  unsigned long __cil_tmp5 ;
  unsigned long __cil_tmp6 ;
  unsigned long __cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  struct kobject *__cil_tmp10 ;
  struct bin_attribute  const  *__cil_tmp11 ;
  void const   *__cil_tmp12 ;

  {
  {
#line 276
  tmp = kzalloc(516UL, 208U);
#line 276
  data = (struct w1_f23_data *)tmp;
  }
#line 277
  if (! data) {
#line 278
    return (-12);
  } else {

  }
  {
#line 279
  __cil_tmp5 = (unsigned long )sl;
#line 279
  __cil_tmp6 = __cil_tmp5 + 104;
#line 279
  *((void **)__cil_tmp6) = (void *)data;
#line 283
  __cil_tmp7 = 112 + 16;
#line 283
  __cil_tmp8 = (unsigned long )sl;
#line 283
  __cil_tmp9 = __cil_tmp8 + __cil_tmp7;
#line 283
  __cil_tmp10 = (struct kobject *)__cil_tmp9;
#line 283
  __cil_tmp11 = (struct bin_attribute  const  *)(& w1_f23_bin_attr);
#line 283
  err = (int )sysfs_create_bin_file(__cil_tmp10, __cil_tmp11);
  }
#line 286
  if (err) {
    {
#line 287
    __cil_tmp12 = (void const   *)data;
#line 287
    kfree(__cil_tmp12);
    }
  } else {

  }
#line 290
  return (err);
}
}
#line 293 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12357/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2433.c.common.c"
static void w1_f23_remove_slave(struct w1_slave *sl ) 
{ unsigned long __cil_tmp2 ;
  unsigned long __cil_tmp3 ;
  void *__cil_tmp4 ;
  void const   *__cil_tmp5 ;
  unsigned long __cil_tmp6 ;
  unsigned long __cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  unsigned long __cil_tmp10 ;
  struct kobject *__cil_tmp11 ;
  struct bin_attribute  const  *__cil_tmp12 ;

  {
  {
#line 296
  __cil_tmp2 = (unsigned long )sl;
#line 296
  __cil_tmp3 = __cil_tmp2 + 104;
#line 296
  __cil_tmp4 = *((void **)__cil_tmp3);
#line 296
  __cil_tmp5 = (void const   *)__cil_tmp4;
#line 296
  kfree(__cil_tmp5);
#line 297
  __cil_tmp6 = (unsigned long )sl;
#line 297
  __cil_tmp7 = __cil_tmp6 + 104;
#line 297
  *((void **)__cil_tmp7) = (void *)0;
#line 299
  __cil_tmp8 = 112 + 16;
#line 299
  __cil_tmp9 = (unsigned long )sl;
#line 299
  __cil_tmp10 = __cil_tmp9 + __cil_tmp8;
#line 299
  __cil_tmp11 = (struct kobject *)__cil_tmp10;
#line 299
  __cil_tmp12 = (struct bin_attribute  const  *)(& w1_f23_bin_attr);
#line 299
  sysfs_remove_bin_file(__cil_tmp11, __cil_tmp12);
  }
#line 300
  return;
}
}
#line 302 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12357/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2433.c.common.c"
static struct w1_family_ops w1_f23_fops  =    {& w1_f23_add_slave, & w1_f23_remove_slave};
#line 307 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12357/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2433.c.common.c"
static struct w1_family w1_family_23  =    {{(struct list_head *)0, (struct list_head *)0}, (u8 )35, & w1_f23_fops, {0}};
#line 312
static int w1_f23_init(void)  __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
#line 312 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12357/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2433.c.common.c"
static int w1_f23_init(void) 
{ int tmp ;

  {
  {
#line 314
  tmp = w1_register_family(& w1_family_23);
  }
#line 314
  return (tmp);
}
}
#line 317
static void w1_f23_fini(void)  __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
#line 317 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12357/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2433.c.common.c"
static void w1_f23_fini(void) 
{ 

  {
  {
#line 319
  w1_unregister_family(& w1_family_23);
  }
#line 320
  return;
}
}
#line 322 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12357/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2433.c.common.c"
int init_module(void) 
{ int tmp ;

  {
  {
#line 322
  tmp = w1_f23_init();
  }
#line 322
  return (tmp);
}
}
#line 323 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12357/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2433.c.common.c"
void cleanup_module(void) 
{ 

  {
  {
#line 323
  w1_f23_fini();
  }
#line 323
  return;
}
}
#line 341
void ldv_check_final_state(void) ;
#line 347
extern void ldv_initialize(void) ;
#line 350
extern int __VERIFIER_nondet_int(void) ;
#line 353 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12357/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2433.c.common.c"
int LDV_IN_INTERRUPT  ;
#line 356 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12357/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2433.c.common.c"
void main(void) 
{ struct file *var_group1 ;
  struct kobject *var_group2 ;
  struct bin_attribute *var_w1_f23_read_bin_2_p2 ;
  char *var_w1_f23_read_bin_2_p3 ;
  loff_t var_w1_f23_read_bin_2_p4 ;
  size_t var_w1_f23_read_bin_2_p5 ;
  struct bin_attribute *var_w1_f23_write_bin_4_p2 ;
  char *var_w1_f23_write_bin_4_p3 ;
  loff_t var_w1_f23_write_bin_4_p4 ;
  size_t var_w1_f23_write_bin_4_p5 ;
  struct w1_slave *var_group3 ;
  int tmp ;
  int tmp___0 ;
  int tmp___1 ;

  {
  {
#line 534
  LDV_IN_INTERRUPT = 1;
#line 543
  ldv_initialize();
#line 584
  tmp = w1_f23_init();
  }
#line 584
  if (tmp) {
#line 585
    goto ldv_final;
  } else {

  }
  {
#line 591
  while (1) {
    while_continue: /* CIL Label */ ;
    {
#line 591
    tmp___1 = __VERIFIER_nondet_int();
    }
#line 591
    if (tmp___1) {

    } else {
#line 591
      goto while_break;
    }
    {
#line 594
    tmp___0 = __VERIFIER_nondet_int();
    }
#line 596
    if (tmp___0 == 0) {
#line 596
      goto case_0;
    } else
#line 643
    if (tmp___0 == 1) {
#line 643
      goto case_1;
    } else
#line 694
    if (tmp___0 == 2) {
#line 694
      goto case_2;
    } else
#line 743
    if (tmp___0 == 3) {
#line 743
      goto case_3;
    } else {
      {
#line 792
      goto switch_default;
#line 594
      if (0) {
        case_0: /* CIL Label */ 
        {
#line 621
        w1_f23_read_bin(var_group1, var_group2, var_w1_f23_read_bin_2_p2, var_w1_f23_read_bin_2_p3,
                        var_w1_f23_read_bin_2_p4, var_w1_f23_read_bin_2_p5);
        }
#line 642
        goto switch_break;
        case_1: /* CIL Label */ 
        {
#line 678
        w1_f23_write_bin(var_group1, var_group2, var_w1_f23_write_bin_4_p2, var_w1_f23_write_bin_4_p3,
                         var_w1_f23_write_bin_4_p4, var_w1_f23_write_bin_4_p5);
        }
#line 693
        goto switch_break;
        case_2: /* CIL Label */ 
        {
#line 731
        w1_f23_add_slave(var_group3);
        }
#line 742
        goto switch_break;
        case_3: /* CIL Label */ 
        {
#line 784
        w1_f23_remove_slave(var_group3);
        }
#line 791
        goto switch_break;
        switch_default: /* CIL Label */ 
#line 792
        goto switch_break;
      } else {
        switch_break: /* CIL Label */ ;
      }
      }
    }
  }
  while_break: /* CIL Label */ ;
  }
  {
#line 839
  w1_f23_fini();
  }
  ldv_final: 
  {
#line 842
  ldv_check_final_state();
  }
#line 845
  return;
}
}
#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12357/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
void ldv_blast_assert(void) 
{ 

  {
  ERROR: 
#line 6
  goto ERROR;
}
}
#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12357/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
extern int __VERIFIER_nondet_int(void) ;
#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12357/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
int ldv_mutex  =    1;
#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12357/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) 
{ int nondetermined ;

  {
#line 29
  if (ldv_mutex == 1) {

  } else {
    {
#line 29
    ldv_blast_assert();
    }
  }
  {
#line 32
  nondetermined = __VERIFIER_nondet_int();
  }
#line 35
  if (nondetermined) {
#line 38
    ldv_mutex = 2;
#line 40
    return (0);
  } else {
#line 45
    return (-4);
  }
}
}
#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12357/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) 
{ int nondetermined ;

  {
#line 57
  if (ldv_mutex == 1) {

  } else {
    {
#line 57
    ldv_blast_assert();
    }
  }
  {
#line 60
  nondetermined = __VERIFIER_nondet_int();
  }
#line 63
  if (nondetermined) {
#line 66
    ldv_mutex = 2;
#line 68
    return (0);
  } else {
#line 73
    return (-4);
  }
}
}
#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12357/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) 
{ int atomic_value_after_dec ;

  {
#line 83
  if (ldv_mutex == 1) {

  } else {
    {
#line 83
    ldv_blast_assert();
    }
  }
  {
#line 86
  atomic_value_after_dec = __VERIFIER_nondet_int();
  }
#line 89
  if (atomic_value_after_dec == 0) {
#line 92
    ldv_mutex = 2;
#line 94
    return (1);
  } else {

  }
#line 98
  return (0);
}
}
#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12357/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
void mutex_lock(struct mutex *lock ) 
{ 

  {
#line 108
  if (ldv_mutex == 1) {

  } else {
    {
#line 108
    ldv_blast_assert();
    }
  }
#line 110
  ldv_mutex = 2;
#line 111
  return;
}
}
#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12357/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
int mutex_trylock(struct mutex *lock ) 
{ int nondetermined ;

  {
#line 121
  if (ldv_mutex == 1) {

  } else {
    {
#line 121
    ldv_blast_assert();
    }
  }
  {
#line 124
  nondetermined = __VERIFIER_nondet_int();
  }
#line 127
  if (nondetermined) {
#line 130
    ldv_mutex = 2;
#line 132
    return (1);
  } else {
#line 137
    return (0);
  }
}
}
#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12357/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
void mutex_unlock(struct mutex *lock ) 
{ 

  {
#line 147
  if (ldv_mutex == 2) {

  } else {
    {
#line 147
    ldv_blast_assert();
    }
  }
#line 149
  ldv_mutex = 1;
#line 150
  return;
}
}
#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12357/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
void ldv_check_final_state(void) 
{ 

  {
#line 156
  if (ldv_mutex == 1) {

  } else {
    {
#line 156
    ldv_blast_assert();
    }
  }
#line 157
  return;
}
}
#line 854 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12357/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2433.c.common.c"
long s__builtin_expect(long val , long res ) 
{ 

  {
#line 855
  return (val);
}
}