Showing error 494

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-linux-3.4/32_1_cilled_safe_ok_nondet_linux-3.4-32_1-drivers--misc--eeprom--eeprom_93xx46.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 5481
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

   1/* Generated by CIL v. 1.3.7 */
   2/* print_CIL_Input is true */
   3
   4#line 23 "include/asm-generic/int-ll64.h"
   5typedef unsigned short __u16;
   6#line 25 "include/asm-generic/int-ll64.h"
   7typedef int __s32;
   8#line 26 "include/asm-generic/int-ll64.h"
   9typedef unsigned int __u32;
  10#line 30 "include/asm-generic/int-ll64.h"
  11typedef unsigned long long __u64;
  12#line 43 "include/asm-generic/int-ll64.h"
  13typedef unsigned char u8;
  14#line 45 "include/asm-generic/int-ll64.h"
  15typedef short s16;
  16#line 46 "include/asm-generic/int-ll64.h"
  17typedef unsigned short u16;
  18#line 49 "include/asm-generic/int-ll64.h"
  19typedef unsigned int u32;
  20#line 51 "include/asm-generic/int-ll64.h"
  21typedef long long s64;
  22#line 52 "include/asm-generic/int-ll64.h"
  23typedef unsigned long long u64;
  24#line 14 "include/asm-generic/posix_types.h"
  25typedef long __kernel_long_t;
  26#line 15 "include/asm-generic/posix_types.h"
  27typedef unsigned long __kernel_ulong_t;
  28#line 31 "include/asm-generic/posix_types.h"
  29typedef int __kernel_pid_t;
  30#line 52 "include/asm-generic/posix_types.h"
  31typedef unsigned int __kernel_uid32_t;
  32#line 53 "include/asm-generic/posix_types.h"
  33typedef unsigned int __kernel_gid32_t;
  34#line 75 "include/asm-generic/posix_types.h"
  35typedef __kernel_ulong_t __kernel_size_t;
  36#line 76 "include/asm-generic/posix_types.h"
  37typedef __kernel_long_t __kernel_ssize_t;
  38#line 91 "include/asm-generic/posix_types.h"
  39typedef long long __kernel_loff_t;
  40#line 92 "include/asm-generic/posix_types.h"
  41typedef __kernel_long_t __kernel_time_t;
  42#line 93 "include/asm-generic/posix_types.h"
  43typedef __kernel_long_t __kernel_clock_t;
  44#line 94 "include/asm-generic/posix_types.h"
  45typedef int __kernel_timer_t;
  46#line 95 "include/asm-generic/posix_types.h"
  47typedef int __kernel_clockid_t;
  48#line 21 "include/linux/types.h"
  49typedef __u32 __kernel_dev_t;
  50#line 24 "include/linux/types.h"
  51typedef __kernel_dev_t dev_t;
  52#line 27 "include/linux/types.h"
  53typedef unsigned short umode_t;
  54#line 30 "include/linux/types.h"
  55typedef __kernel_pid_t pid_t;
  56#line 35 "include/linux/types.h"
  57typedef __kernel_clockid_t clockid_t;
  58#line 38 "include/linux/types.h"
  59typedef _Bool bool;
  60#line 40 "include/linux/types.h"
  61typedef __kernel_uid32_t uid_t;
  62#line 41 "include/linux/types.h"
  63typedef __kernel_gid32_t gid_t;
  64#line 54 "include/linux/types.h"
  65typedef __kernel_loff_t loff_t;
  66#line 63 "include/linux/types.h"
  67typedef __kernel_size_t size_t;
  68#line 68 "include/linux/types.h"
  69typedef __kernel_ssize_t ssize_t;
  70#line 78 "include/linux/types.h"
  71typedef __kernel_time_t time_t;
  72#line 111 "include/linux/types.h"
  73typedef __s32 int32_t;
  74#line 117 "include/linux/types.h"
  75typedef __u32 uint32_t;
  76#line 155 "include/linux/types.h"
  77typedef u64 dma_addr_t;
  78#line 202 "include/linux/types.h"
  79typedef unsigned int gfp_t;
  80#line 219 "include/linux/types.h"
  81struct __anonstruct_atomic_t_7 {
  82   int counter ;
  83};
  84#line 219 "include/linux/types.h"
  85typedef struct __anonstruct_atomic_t_7 atomic_t;
  86#line 224 "include/linux/types.h"
  87struct __anonstruct_atomic64_t_8 {
  88   long counter ;
  89};
  90#line 224 "include/linux/types.h"
  91typedef struct __anonstruct_atomic64_t_8 atomic64_t;
  92#line 229 "include/linux/types.h"
  93struct list_head {
  94   struct list_head *next ;
  95   struct list_head *prev ;
  96};
  97#line 233
  98struct hlist_node;
  99#line 233 "include/linux/types.h"
 100struct hlist_head {
 101   struct hlist_node *first ;
 102};
 103#line 237 "include/linux/types.h"
 104struct hlist_node {
 105   struct hlist_node *next ;
 106   struct hlist_node **pprev ;
 107};
 108#line 253 "include/linux/types.h"
 109struct rcu_head {
 110   struct rcu_head *next ;
 111   void (*func)(struct rcu_head *head ) ;
 112};
 113#line 56 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
 114struct module;
 115#line 56
 116struct module;
 117#line 146 "include/linux/init.h"
 118typedef void (*ctor_fn_t)(void);
 119#line 9 "include/linux/dynamic_debug.h"
 120struct _ddebug {
 121   char const   *modname ;
 122   char const   *function ;
 123   char const   *filename ;
 124   char const   *format ;
 125   unsigned int lineno : 18 ;
 126   unsigned int flags : 8 ;
 127} __attribute__((__aligned__(8))) ;
 128#line 47
 129struct device;
 130#line 47
 131struct device;
 132#line 135 "include/linux/kernel.h"
 133struct completion;
 134#line 135
 135struct completion;
 136#line 136
 137struct pt_regs;
 138#line 136
 139struct pt_regs;
 140#line 349
 141struct pid;
 142#line 349
 143struct pid;
 144#line 202 "include/linux/ioport.h"
 145struct device;
 146#line 12 "include/linux/lockdep.h"
 147struct task_struct;
 148#line 12
 149struct task_struct;
 150#line 391 "include/linux/lockdep.h"
 151struct lock_class_key {
 152
 153};
 154#line 20 "include/linux/kobject_ns.h"
 155struct sock;
 156#line 20
 157struct sock;
 158#line 21
 159struct kobject;
 160#line 21
 161struct kobject;
 162#line 27
 163enum kobj_ns_type {
 164    KOBJ_NS_TYPE_NONE = 0,
 165    KOBJ_NS_TYPE_NET = 1,
 166    KOBJ_NS_TYPES = 2
 167} ;
 168#line 40 "include/linux/kobject_ns.h"
 169struct kobj_ns_type_operations {
 170   enum kobj_ns_type type ;
 171   void *(*grab_current_ns)(void) ;
 172   void const   *(*netlink_ns)(struct sock *sk ) ;
 173   void const   *(*initial_ns)(void) ;
 174   void (*drop_ns)(void * ) ;
 175};
 176#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 177struct task_struct;
 178#line 8
 179struct mm_struct;
 180#line 8
 181struct mm_struct;
 182#line 99 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
 183struct pt_regs {
 184   unsigned long r15 ;
 185   unsigned long r14 ;
 186   unsigned long r13 ;
 187   unsigned long r12 ;
 188   unsigned long bp ;
 189   unsigned long bx ;
 190   unsigned long r11 ;
 191   unsigned long r10 ;
 192   unsigned long r9 ;
 193   unsigned long r8 ;
 194   unsigned long ax ;
 195   unsigned long cx ;
 196   unsigned long dx ;
 197   unsigned long si ;
 198   unsigned long di ;
 199   unsigned long orig_ax ;
 200   unsigned long ip ;
 201   unsigned long cs ;
 202   unsigned long flags ;
 203   unsigned long sp ;
 204   unsigned long ss ;
 205};
 206#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 207struct __anonstruct____missing_field_name_11 {
 208   unsigned int a ;
 209   unsigned int b ;
 210};
 211#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 212struct __anonstruct____missing_field_name_12 {
 213   u16 limit0 ;
 214   u16 base0 ;
 215   unsigned int base1 : 8 ;
 216   unsigned int type : 4 ;
 217   unsigned int s : 1 ;
 218   unsigned int dpl : 2 ;
 219   unsigned int p : 1 ;
 220   unsigned int limit : 4 ;
 221   unsigned int avl : 1 ;
 222   unsigned int l : 1 ;
 223   unsigned int d : 1 ;
 224   unsigned int g : 1 ;
 225   unsigned int base2 : 8 ;
 226};
 227#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 228union __anonunion____missing_field_name_10 {
 229   struct __anonstruct____missing_field_name_11 __annonCompField4 ;
 230   struct __anonstruct____missing_field_name_12 __annonCompField5 ;
 231};
 232#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/desc_defs.h"
 233struct desc_struct {
 234   union __anonunion____missing_field_name_10 __annonCompField6 ;
 235} __attribute__((__packed__)) ;
 236#line 13 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
 237typedef unsigned long pgdval_t;
 238#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
 239typedef unsigned long pgprotval_t;
 240#line 192 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 241struct pgprot {
 242   pgprotval_t pgprot ;
 243};
 244#line 192 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 245typedef struct pgprot pgprot_t;
 246#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 247struct __anonstruct_pgd_t_16 {
 248   pgdval_t pgd ;
 249};
 250#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 251typedef struct __anonstruct_pgd_t_16 pgd_t;
 252#line 282
 253struct page;
 254#line 282 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 255typedef struct page *pgtable_t;
 256#line 295
 257struct file;
 258#line 295
 259struct file;
 260#line 46 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
 261struct page;
 262#line 47
 263struct thread_struct;
 264#line 47
 265struct thread_struct;
 266#line 50
 267struct mm_struct;
 268#line 51
 269struct desc_struct;
 270#line 52
 271struct task_struct;
 272#line 53
 273struct cpumask;
 274#line 53
 275struct cpumask;
 276#line 329
 277struct arch_spinlock;
 278#line 329
 279struct arch_spinlock;
 280#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
 281struct task_struct;
 282#line 141 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/vm86.h"
 283struct kernel_vm86_regs {
 284   struct pt_regs pt ;
 285   unsigned short es ;
 286   unsigned short __esh ;
 287   unsigned short ds ;
 288   unsigned short __dsh ;
 289   unsigned short fs ;
 290   unsigned short __fsh ;
 291   unsigned short gs ;
 292   unsigned short __gsh ;
 293};
 294#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/math_emu.h"
 295union __anonunion____missing_field_name_20 {
 296   struct pt_regs *regs ;
 297   struct kernel_vm86_regs *vm86 ;
 298};
 299#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/math_emu.h"
 300struct math_emu_info {
 301   long ___orig_eip ;
 302   union __anonunion____missing_field_name_20 __annonCompField7 ;
 303};
 304#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
 305struct task_struct;
 306#line 18 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page.h"
 307struct page;
 308#line 10 "include/asm-generic/bug.h"
 309struct bug_entry {
 310   int bug_addr_disp ;
 311   int file_disp ;
 312   unsigned short line ;
 313   unsigned short flags ;
 314};
 315#line 12 "include/linux/bug.h"
 316struct pt_regs;
 317#line 14 "include/linux/cpumask.h"
 318struct cpumask {
 319   unsigned long bits[((4096UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
 320};
 321#line 14 "include/linux/cpumask.h"
 322typedef struct cpumask cpumask_t;
 323#line 637 "include/linux/cpumask.h"
 324typedef struct cpumask *cpumask_var_t;
 325#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
 326struct static_key;
 327#line 234
 328struct static_key;
 329#line 11 "include/linux/personality.h"
 330struct pt_regs;
 331#line 290 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 332struct i387_fsave_struct {
 333   u32 cwd ;
 334   u32 swd ;
 335   u32 twd ;
 336   u32 fip ;
 337   u32 fcs ;
 338   u32 foo ;
 339   u32 fos ;
 340   u32 st_space[20] ;
 341   u32 status ;
 342};
 343#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 344struct __anonstruct____missing_field_name_27 {
 345   u64 rip ;
 346   u64 rdp ;
 347};
 348#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 349struct __anonstruct____missing_field_name_28 {
 350   u32 fip ;
 351   u32 fcs ;
 352   u32 foo ;
 353   u32 fos ;
 354};
 355#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 356union __anonunion____missing_field_name_26 {
 357   struct __anonstruct____missing_field_name_27 __annonCompField11 ;
 358   struct __anonstruct____missing_field_name_28 __annonCompField12 ;
 359};
 360#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 361union __anonunion____missing_field_name_29 {
 362   u32 padding1[12] ;
 363   u32 sw_reserved[12] ;
 364};
 365#line 306 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 366struct i387_fxsave_struct {
 367   u16 cwd ;
 368   u16 swd ;
 369   u16 twd ;
 370   u16 fop ;
 371   union __anonunion____missing_field_name_26 __annonCompField13 ;
 372   u32 mxcsr ;
 373   u32 mxcsr_mask ;
 374   u32 st_space[32] ;
 375   u32 xmm_space[64] ;
 376   u32 padding[12] ;
 377   union __anonunion____missing_field_name_29 __annonCompField14 ;
 378} __attribute__((__aligned__(16))) ;
 379#line 341 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 380struct i387_soft_struct {
 381   u32 cwd ;
 382   u32 swd ;
 383   u32 twd ;
 384   u32 fip ;
 385   u32 fcs ;
 386   u32 foo ;
 387   u32 fos ;
 388   u32 st_space[20] ;
 389   u8 ftop ;
 390   u8 changed ;
 391   u8 lookahead ;
 392   u8 no_update ;
 393   u8 rm ;
 394   u8 alimit ;
 395   struct math_emu_info *info ;
 396   u32 entry_eip ;
 397};
 398#line 361 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 399struct ymmh_struct {
 400   u32 ymmh_space[64] ;
 401};
 402#line 366 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 403struct xsave_hdr_struct {
 404   u64 xstate_bv ;
 405   u64 reserved1[2] ;
 406   u64 reserved2[5] ;
 407} __attribute__((__packed__)) ;
 408#line 372 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 409struct xsave_struct {
 410   struct i387_fxsave_struct i387 ;
 411   struct xsave_hdr_struct xsave_hdr ;
 412   struct ymmh_struct ymmh ;
 413} __attribute__((__packed__, __aligned__(64))) ;
 414#line 379 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 415union thread_xstate {
 416   struct i387_fsave_struct fsave ;
 417   struct i387_fxsave_struct fxsave ;
 418   struct i387_soft_struct soft ;
 419   struct xsave_struct xsave ;
 420};
 421#line 386 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 422struct fpu {
 423   unsigned int last_cpu ;
 424   unsigned int has_fpu ;
 425   union thread_xstate *state ;
 426};
 427#line 433
 428struct kmem_cache;
 429#line 435
 430struct perf_event;
 431#line 435
 432struct perf_event;
 433#line 437 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 434struct thread_struct {
 435   struct desc_struct tls_array[3] ;
 436   unsigned long sp0 ;
 437   unsigned long sp ;
 438   unsigned long usersp ;
 439   unsigned short es ;
 440   unsigned short ds ;
 441   unsigned short fsindex ;
 442   unsigned short gsindex ;
 443   unsigned long fs ;
 444   unsigned long gs ;
 445   struct perf_event *ptrace_bps[4] ;
 446   unsigned long debugreg6 ;
 447   unsigned long ptrace_dr7 ;
 448   unsigned long cr2 ;
 449   unsigned long trap_nr ;
 450   unsigned long error_code ;
 451   struct fpu fpu ;
 452   unsigned long *io_bitmap_ptr ;
 453   unsigned long iopl ;
 454   unsigned int io_bitmap_max ;
 455};
 456#line 23 "include/asm-generic/atomic-long.h"
 457typedef atomic64_t atomic_long_t;
 458#line 22 "include/linux/sysfs.h"
 459struct kobject;
 460#line 23
 461struct module;
 462#line 24
 463enum kobj_ns_type;
 464#line 26 "include/linux/sysfs.h"
 465struct attribute {
 466   char const   *name ;
 467   umode_t mode ;
 468};
 469#line 56 "include/linux/sysfs.h"
 470struct attribute_group {
 471   char const   *name ;
 472   umode_t (*is_visible)(struct kobject * , struct attribute * , int  ) ;
 473   struct attribute **attrs ;
 474};
 475#line 85
 476struct file;
 477#line 86
 478struct vm_area_struct;
 479#line 86
 480struct vm_area_struct;
 481#line 88 "include/linux/sysfs.h"
 482struct bin_attribute {
 483   struct attribute attr ;
 484   size_t size ;
 485   void *private ;
 486   ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 487                   loff_t  , size_t  ) ;
 488   ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 489                    loff_t  , size_t  ) ;
 490   int (*mmap)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ) ;
 491};
 492#line 112 "include/linux/sysfs.h"
 493struct sysfs_ops {
 494   ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
 495   ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
 496   void const   *(*namespace)(struct kobject * , struct attribute  const  * ) ;
 497};
 498#line 118
 499struct sysfs_dirent;
 500#line 118
 501struct sysfs_dirent;
 502#line 12 "include/linux/thread_info.h"
 503struct timespec;
 504#line 12
 505struct timespec;
 506#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
 507struct task_struct;
 508#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 509typedef u16 __ticket_t;
 510#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 511typedef u32 __ticketpair_t;
 512#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 513struct __raw_tickets {
 514   __ticket_t head ;
 515   __ticket_t tail ;
 516};
 517#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 518union __anonunion____missing_field_name_36 {
 519   __ticketpair_t head_tail ;
 520   struct __raw_tickets tickets ;
 521};
 522#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 523struct arch_spinlock {
 524   union __anonunion____missing_field_name_36 __annonCompField17 ;
 525};
 526#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 527typedef struct arch_spinlock arch_spinlock_t;
 528#line 20 "include/linux/spinlock_types.h"
 529struct raw_spinlock {
 530   arch_spinlock_t raw_lock ;
 531   unsigned int magic ;
 532   unsigned int owner_cpu ;
 533   void *owner ;
 534};
 535#line 20 "include/linux/spinlock_types.h"
 536typedef struct raw_spinlock raw_spinlock_t;
 537#line 64 "include/linux/spinlock_types.h"
 538union __anonunion____missing_field_name_39 {
 539   struct raw_spinlock rlock ;
 540};
 541#line 64 "include/linux/spinlock_types.h"
 542struct spinlock {
 543   union __anonunion____missing_field_name_39 __annonCompField19 ;
 544};
 545#line 64 "include/linux/spinlock_types.h"
 546typedef struct spinlock spinlock_t;
 547#line 22 "include/linux/kref.h"
 548struct kref {
 549   atomic_t refcount ;
 550};
 551#line 49 "include/linux/wait.h"
 552struct __wait_queue_head {
 553   spinlock_t lock ;
 554   struct list_head task_list ;
 555};
 556#line 53 "include/linux/wait.h"
 557typedef struct __wait_queue_head wait_queue_head_t;
 558#line 55
 559struct task_struct;
 560#line 60 "include/linux/kobject.h"
 561struct kset;
 562#line 60
 563struct kobj_type;
 564#line 60 "include/linux/kobject.h"
 565struct kobject {
 566   char const   *name ;
 567   struct list_head entry ;
 568   struct kobject *parent ;
 569   struct kset *kset ;
 570   struct kobj_type *ktype ;
 571   struct sysfs_dirent *sd ;
 572   struct kref kref ;
 573   unsigned int state_initialized : 1 ;
 574   unsigned int state_in_sysfs : 1 ;
 575   unsigned int state_add_uevent_sent : 1 ;
 576   unsigned int state_remove_uevent_sent : 1 ;
 577   unsigned int uevent_suppress : 1 ;
 578};
 579#line 108 "include/linux/kobject.h"
 580struct kobj_type {
 581   void (*release)(struct kobject *kobj ) ;
 582   struct sysfs_ops  const  *sysfs_ops ;
 583   struct attribute **default_attrs ;
 584   struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject *kobj ) ;
 585   void const   *(*namespace)(struct kobject *kobj ) ;
 586};
 587#line 116 "include/linux/kobject.h"
 588struct kobj_uevent_env {
 589   char *envp[32] ;
 590   int envp_idx ;
 591   char buf[2048] ;
 592   int buflen ;
 593};
 594#line 123 "include/linux/kobject.h"
 595struct kset_uevent_ops {
 596   int (* const  filter)(struct kset *kset , struct kobject *kobj ) ;
 597   char const   *(* const  name)(struct kset *kset , struct kobject *kobj ) ;
 598   int (* const  uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
 599};
 600#line 140
 601struct sock;
 602#line 159 "include/linux/kobject.h"
 603struct kset {
 604   struct list_head list ;
 605   spinlock_t list_lock ;
 606   struct kobject kobj ;
 607   struct kset_uevent_ops  const  *uevent_ops ;
 608};
 609#line 19 "include/linux/klist.h"
 610struct klist_node;
 611#line 19
 612struct klist_node;
 613#line 39 "include/linux/klist.h"
 614struct klist_node {
 615   void *n_klist ;
 616   struct list_head n_node ;
 617   struct kref n_ref ;
 618};
 619#line 48 "include/linux/mutex.h"
 620struct mutex {
 621   atomic_t count ;
 622   spinlock_t wait_lock ;
 623   struct list_head wait_list ;
 624   struct task_struct *owner ;
 625   char const   *name ;
 626   void *magic ;
 627};
 628#line 69 "include/linux/mutex.h"
 629struct mutex_waiter {
 630   struct list_head list ;
 631   struct task_struct *task ;
 632   void *magic ;
 633};
 634#line 119 "include/linux/seqlock.h"
 635struct seqcount {
 636   unsigned int sequence ;
 637};
 638#line 119 "include/linux/seqlock.h"
 639typedef struct seqcount seqcount_t;
 640#line 14 "include/linux/time.h"
 641struct timespec {
 642   __kernel_time_t tv_sec ;
 643   long tv_nsec ;
 644};
 645#line 46 "include/linux/ktime.h"
 646union ktime {
 647   s64 tv64 ;
 648};
 649#line 59 "include/linux/ktime.h"
 650typedef union ktime ktime_t;
 651#line 10 "include/linux/timer.h"
 652struct tvec_base;
 653#line 10
 654struct tvec_base;
 655#line 12 "include/linux/timer.h"
 656struct timer_list {
 657   struct list_head entry ;
 658   unsigned long expires ;
 659   struct tvec_base *base ;
 660   void (*function)(unsigned long  ) ;
 661   unsigned long data ;
 662   int slack ;
 663   int start_pid ;
 664   void *start_site ;
 665   char start_comm[16] ;
 666};
 667#line 289
 668struct hrtimer;
 669#line 289
 670struct hrtimer;
 671#line 290
 672enum hrtimer_restart;
 673#line 17 "include/linux/workqueue.h"
 674struct work_struct;
 675#line 17
 676struct work_struct;
 677#line 79 "include/linux/workqueue.h"
 678struct work_struct {
 679   atomic_long_t data ;
 680   struct list_head entry ;
 681   void (*func)(struct work_struct *work ) ;
 682};
 683#line 25 "include/linux/completion.h"
 684struct completion {
 685   unsigned int done ;
 686   wait_queue_head_t wait ;
 687};
 688#line 42 "include/linux/pm.h"
 689struct device;
 690#line 50 "include/linux/pm.h"
 691struct pm_message {
 692   int event ;
 693};
 694#line 50 "include/linux/pm.h"
 695typedef struct pm_message pm_message_t;
 696#line 264 "include/linux/pm.h"
 697struct dev_pm_ops {
 698   int (*prepare)(struct device *dev ) ;
 699   void (*complete)(struct device *dev ) ;
 700   int (*suspend)(struct device *dev ) ;
 701   int (*resume)(struct device *dev ) ;
 702   int (*freeze)(struct device *dev ) ;
 703   int (*thaw)(struct device *dev ) ;
 704   int (*poweroff)(struct device *dev ) ;
 705   int (*restore)(struct device *dev ) ;
 706   int (*suspend_late)(struct device *dev ) ;
 707   int (*resume_early)(struct device *dev ) ;
 708   int (*freeze_late)(struct device *dev ) ;
 709   int (*thaw_early)(struct device *dev ) ;
 710   int (*poweroff_late)(struct device *dev ) ;
 711   int (*restore_early)(struct device *dev ) ;
 712   int (*suspend_noirq)(struct device *dev ) ;
 713   int (*resume_noirq)(struct device *dev ) ;
 714   int (*freeze_noirq)(struct device *dev ) ;
 715   int (*thaw_noirq)(struct device *dev ) ;
 716   int (*poweroff_noirq)(struct device *dev ) ;
 717   int (*restore_noirq)(struct device *dev ) ;
 718   int (*runtime_suspend)(struct device *dev ) ;
 719   int (*runtime_resume)(struct device *dev ) ;
 720   int (*runtime_idle)(struct device *dev ) ;
 721};
 722#line 458
 723enum rpm_status {
 724    RPM_ACTIVE = 0,
 725    RPM_RESUMING = 1,
 726    RPM_SUSPENDED = 2,
 727    RPM_SUSPENDING = 3
 728} ;
 729#line 480
 730enum rpm_request {
 731    RPM_REQ_NONE = 0,
 732    RPM_REQ_IDLE = 1,
 733    RPM_REQ_SUSPEND = 2,
 734    RPM_REQ_AUTOSUSPEND = 3,
 735    RPM_REQ_RESUME = 4
 736} ;
 737#line 488
 738struct wakeup_source;
 739#line 488
 740struct wakeup_source;
 741#line 495 "include/linux/pm.h"
 742struct pm_subsys_data {
 743   spinlock_t lock ;
 744   unsigned int refcount ;
 745};
 746#line 506
 747struct dev_pm_qos_request;
 748#line 506
 749struct pm_qos_constraints;
 750#line 506 "include/linux/pm.h"
 751struct dev_pm_info {
 752   pm_message_t power_state ;
 753   unsigned int can_wakeup : 1 ;
 754   unsigned int async_suspend : 1 ;
 755   bool is_prepared : 1 ;
 756   bool is_suspended : 1 ;
 757   bool ignore_children : 1 ;
 758   spinlock_t lock ;
 759   struct list_head entry ;
 760   struct completion completion ;
 761   struct wakeup_source *wakeup ;
 762   bool wakeup_path : 1 ;
 763   struct timer_list suspend_timer ;
 764   unsigned long timer_expires ;
 765   struct work_struct work ;
 766   wait_queue_head_t wait_queue ;
 767   atomic_t usage_count ;
 768   atomic_t child_count ;
 769   unsigned int disable_depth : 3 ;
 770   unsigned int idle_notification : 1 ;
 771   unsigned int request_pending : 1 ;
 772   unsigned int deferred_resume : 1 ;
 773   unsigned int run_wake : 1 ;
 774   unsigned int runtime_auto : 1 ;
 775   unsigned int no_callbacks : 1 ;
 776   unsigned int irq_safe : 1 ;
 777   unsigned int use_autosuspend : 1 ;
 778   unsigned int timer_autosuspends : 1 ;
 779   enum rpm_request request ;
 780   enum rpm_status runtime_status ;
 781   int runtime_error ;
 782   int autosuspend_delay ;
 783   unsigned long last_busy ;
 784   unsigned long active_jiffies ;
 785   unsigned long suspended_jiffies ;
 786   unsigned long accounting_timestamp ;
 787   ktime_t suspend_time ;
 788   s64 max_time_suspended_ns ;
 789   struct dev_pm_qos_request *pq_req ;
 790   struct pm_subsys_data *subsys_data ;
 791   struct pm_qos_constraints *constraints ;
 792};
 793#line 564 "include/linux/pm.h"
 794struct dev_pm_domain {
 795   struct dev_pm_ops ops ;
 796};
 797#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 798struct dma_map_ops;
 799#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 800struct dev_archdata {
 801   void *acpi_handle ;
 802   struct dma_map_ops *dma_ops ;
 803   void *iommu ;
 804};
 805#line 28 "include/linux/device.h"
 806struct device;
 807#line 29
 808struct device_private;
 809#line 29
 810struct device_private;
 811#line 30
 812struct device_driver;
 813#line 30
 814struct device_driver;
 815#line 31
 816struct driver_private;
 817#line 31
 818struct driver_private;
 819#line 32
 820struct module;
 821#line 33
 822struct class;
 823#line 33
 824struct class;
 825#line 34
 826struct subsys_private;
 827#line 34
 828struct subsys_private;
 829#line 35
 830struct bus_type;
 831#line 35
 832struct bus_type;
 833#line 36
 834struct device_node;
 835#line 36
 836struct device_node;
 837#line 37
 838struct iommu_ops;
 839#line 37
 840struct iommu_ops;
 841#line 39 "include/linux/device.h"
 842struct bus_attribute {
 843   struct attribute attr ;
 844   ssize_t (*show)(struct bus_type *bus , char *buf ) ;
 845   ssize_t (*store)(struct bus_type *bus , char const   *buf , size_t count ) ;
 846};
 847#line 89
 848struct device_attribute;
 849#line 89
 850struct driver_attribute;
 851#line 89 "include/linux/device.h"
 852struct bus_type {
 853   char const   *name ;
 854   char const   *dev_name ;
 855   struct device *dev_root ;
 856   struct bus_attribute *bus_attrs ;
 857   struct device_attribute *dev_attrs ;
 858   struct driver_attribute *drv_attrs ;
 859   int (*match)(struct device *dev , struct device_driver *drv ) ;
 860   int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
 861   int (*probe)(struct device *dev ) ;
 862   int (*remove)(struct device *dev ) ;
 863   void (*shutdown)(struct device *dev ) ;
 864   int (*suspend)(struct device *dev , pm_message_t state ) ;
 865   int (*resume)(struct device *dev ) ;
 866   struct dev_pm_ops  const  *pm ;
 867   struct iommu_ops *iommu_ops ;
 868   struct subsys_private *p ;
 869};
 870#line 127
 871struct device_type;
 872#line 214
 873struct of_device_id;
 874#line 214 "include/linux/device.h"
 875struct device_driver {
 876   char const   *name ;
 877   struct bus_type *bus ;
 878   struct module *owner ;
 879   char const   *mod_name ;
 880   bool suppress_bind_attrs ;
 881   struct of_device_id  const  *of_match_table ;
 882   int (*probe)(struct device *dev ) ;
 883   int (*remove)(struct device *dev ) ;
 884   void (*shutdown)(struct device *dev ) ;
 885   int (*suspend)(struct device *dev , pm_message_t state ) ;
 886   int (*resume)(struct device *dev ) ;
 887   struct attribute_group  const  **groups ;
 888   struct dev_pm_ops  const  *pm ;
 889   struct driver_private *p ;
 890};
 891#line 249 "include/linux/device.h"
 892struct driver_attribute {
 893   struct attribute attr ;
 894   ssize_t (*show)(struct device_driver *driver , char *buf ) ;
 895   ssize_t (*store)(struct device_driver *driver , char const   *buf , size_t count ) ;
 896};
 897#line 330
 898struct class_attribute;
 899#line 330 "include/linux/device.h"
 900struct class {
 901   char const   *name ;
 902   struct module *owner ;
 903   struct class_attribute *class_attrs ;
 904   struct device_attribute *dev_attrs ;
 905   struct bin_attribute *dev_bin_attrs ;
 906   struct kobject *dev_kobj ;
 907   int (*dev_uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
 908   char *(*devnode)(struct device *dev , umode_t *mode ) ;
 909   void (*class_release)(struct class *class ) ;
 910   void (*dev_release)(struct device *dev ) ;
 911   int (*suspend)(struct device *dev , pm_message_t state ) ;
 912   int (*resume)(struct device *dev ) ;
 913   struct kobj_ns_type_operations  const  *ns_type ;
 914   void const   *(*namespace)(struct device *dev ) ;
 915   struct dev_pm_ops  const  *pm ;
 916   struct subsys_private *p ;
 917};
 918#line 397 "include/linux/device.h"
 919struct class_attribute {
 920   struct attribute attr ;
 921   ssize_t (*show)(struct class *class , struct class_attribute *attr , char *buf ) ;
 922   ssize_t (*store)(struct class *class , struct class_attribute *attr , char const   *buf ,
 923                    size_t count ) ;
 924   void const   *(*namespace)(struct class *class , struct class_attribute  const  *attr ) ;
 925};
 926#line 465 "include/linux/device.h"
 927struct device_type {
 928   char const   *name ;
 929   struct attribute_group  const  **groups ;
 930   int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
 931   char *(*devnode)(struct device *dev , umode_t *mode ) ;
 932   void (*release)(struct device *dev ) ;
 933   struct dev_pm_ops  const  *pm ;
 934};
 935#line 476 "include/linux/device.h"
 936struct device_attribute {
 937   struct attribute attr ;
 938   ssize_t (*show)(struct device *dev , struct device_attribute *attr , char *buf ) ;
 939   ssize_t (*store)(struct device *dev , struct device_attribute *attr , char const   *buf ,
 940                    size_t count ) ;
 941};
 942#line 559 "include/linux/device.h"
 943struct device_dma_parameters {
 944   unsigned int max_segment_size ;
 945   unsigned long segment_boundary_mask ;
 946};
 947#line 627
 948struct dma_coherent_mem;
 949#line 627 "include/linux/device.h"
 950struct device {
 951   struct device *parent ;
 952   struct device_private *p ;
 953   struct kobject kobj ;
 954   char const   *init_name ;
 955   struct device_type  const  *type ;
 956   struct mutex mutex ;
 957   struct bus_type *bus ;
 958   struct device_driver *driver ;
 959   void *platform_data ;
 960   struct dev_pm_info power ;
 961   struct dev_pm_domain *pm_domain ;
 962   int numa_node ;
 963   u64 *dma_mask ;
 964   u64 coherent_dma_mask ;
 965   struct device_dma_parameters *dma_parms ;
 966   struct list_head dma_pools ;
 967   struct dma_coherent_mem *dma_mem ;
 968   struct dev_archdata archdata ;
 969   struct device_node *of_node ;
 970   dev_t devt ;
 971   u32 id ;
 972   spinlock_t devres_lock ;
 973   struct list_head devres_head ;
 974   struct klist_node knode_class ;
 975   struct class *class ;
 976   struct attribute_group  const  **groups ;
 977   void (*release)(struct device *dev ) ;
 978};
 979#line 43 "include/linux/pm_wakeup.h"
 980struct wakeup_source {
 981   char const   *name ;
 982   struct list_head entry ;
 983   spinlock_t lock ;
 984   struct timer_list timer ;
 985   unsigned long timer_expires ;
 986   ktime_t total_time ;
 987   ktime_t max_time ;
 988   ktime_t last_time ;
 989   unsigned long event_count ;
 990   unsigned long active_count ;
 991   unsigned long relax_count ;
 992   unsigned long hit_count ;
 993   unsigned int active : 1 ;
 994};
 995#line 98 "include/linux/nodemask.h"
 996struct __anonstruct_nodemask_t_44 {
 997   unsigned long bits[(((unsigned long )(1 << 10) + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
 998};
 999#line 98 "include/linux/nodemask.h"
1000typedef struct __anonstruct_nodemask_t_44 nodemask_t;
1001#line 60 "include/linux/pageblock-flags.h"
1002struct page;
1003#line 19 "include/linux/rwsem.h"
1004struct rw_semaphore;
1005#line 19
1006struct rw_semaphore;
1007#line 25 "include/linux/rwsem.h"
1008struct rw_semaphore {
1009   long count ;
1010   raw_spinlock_t wait_lock ;
1011   struct list_head wait_list ;
1012};
1013#line 9 "include/linux/memory_hotplug.h"
1014struct page;
1015#line 103 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mpspec.h"
1016struct device;
1017#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
1018struct __anonstruct_mm_context_t_112 {
1019   void *ldt ;
1020   int size ;
1021   unsigned short ia32_compat ;
1022   struct mutex lock ;
1023   void *vdso ;
1024};
1025#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
1026typedef struct __anonstruct_mm_context_t_112 mm_context_t;
1027#line 8 "include/linux/vmalloc.h"
1028struct vm_area_struct;
1029#line 994 "include/linux/mmzone.h"
1030struct page;
1031#line 10 "include/linux/gfp.h"
1032struct vm_area_struct;
1033#line 29 "include/linux/sysctl.h"
1034struct completion;
1035#line 100 "include/linux/rbtree.h"
1036struct rb_node {
1037   unsigned long rb_parent_color ;
1038   struct rb_node *rb_right ;
1039   struct rb_node *rb_left ;
1040} __attribute__((__aligned__(sizeof(long )))) ;
1041#line 110 "include/linux/rbtree.h"
1042struct rb_root {
1043   struct rb_node *rb_node ;
1044};
1045#line 939 "include/linux/sysctl.h"
1046struct nsproxy;
1047#line 939
1048struct nsproxy;
1049#line 48 "include/linux/kmod.h"
1050struct cred;
1051#line 48
1052struct cred;
1053#line 49
1054struct file;
1055#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
1056struct task_struct;
1057#line 18 "include/linux/elf.h"
1058typedef __u64 Elf64_Addr;
1059#line 19 "include/linux/elf.h"
1060typedef __u16 Elf64_Half;
1061#line 23 "include/linux/elf.h"
1062typedef __u32 Elf64_Word;
1063#line 24 "include/linux/elf.h"
1064typedef __u64 Elf64_Xword;
1065#line 194 "include/linux/elf.h"
1066struct elf64_sym {
1067   Elf64_Word st_name ;
1068   unsigned char st_info ;
1069   unsigned char st_other ;
1070   Elf64_Half st_shndx ;
1071   Elf64_Addr st_value ;
1072   Elf64_Xword st_size ;
1073};
1074#line 194 "include/linux/elf.h"
1075typedef struct elf64_sym Elf64_Sym;
1076#line 438
1077struct file;
1078#line 39 "include/linux/moduleparam.h"
1079struct kernel_param;
1080#line 39
1081struct kernel_param;
1082#line 41 "include/linux/moduleparam.h"
1083struct kernel_param_ops {
1084   int (*set)(char const   *val , struct kernel_param  const  *kp ) ;
1085   int (*get)(char *buffer , struct kernel_param  const  *kp ) ;
1086   void (*free)(void *arg ) ;
1087};
1088#line 50
1089struct kparam_string;
1090#line 50
1091struct kparam_array;
1092#line 50 "include/linux/moduleparam.h"
1093union __anonunion____missing_field_name_199 {
1094   void *arg ;
1095   struct kparam_string  const  *str ;
1096   struct kparam_array  const  *arr ;
1097};
1098#line 50 "include/linux/moduleparam.h"
1099struct kernel_param {
1100   char const   *name ;
1101   struct kernel_param_ops  const  *ops ;
1102   u16 perm ;
1103   s16 level ;
1104   union __anonunion____missing_field_name_199 __annonCompField32 ;
1105};
1106#line 63 "include/linux/moduleparam.h"
1107struct kparam_string {
1108   unsigned int maxlen ;
1109   char *string ;
1110};
1111#line 69 "include/linux/moduleparam.h"
1112struct kparam_array {
1113   unsigned int max ;
1114   unsigned int elemsize ;
1115   unsigned int *num ;
1116   struct kernel_param_ops  const  *ops ;
1117   void *elem ;
1118};
1119#line 445
1120struct module;
1121#line 80 "include/linux/jump_label.h"
1122struct module;
1123#line 143 "include/linux/jump_label.h"
1124struct static_key {
1125   atomic_t enabled ;
1126};
1127#line 22 "include/linux/tracepoint.h"
1128struct module;
1129#line 23
1130struct tracepoint;
1131#line 23
1132struct tracepoint;
1133#line 25 "include/linux/tracepoint.h"
1134struct tracepoint_func {
1135   void *func ;
1136   void *data ;
1137};
1138#line 30 "include/linux/tracepoint.h"
1139struct tracepoint {
1140   char const   *name ;
1141   struct static_key key ;
1142   void (*regfunc)(void) ;
1143   void (*unregfunc)(void) ;
1144   struct tracepoint_func *funcs ;
1145};
1146#line 19 "include/linux/export.h"
1147struct kernel_symbol {
1148   unsigned long value ;
1149   char const   *name ;
1150};
1151#line 8 "include/asm-generic/module.h"
1152struct mod_arch_specific {
1153
1154};
1155#line 35 "include/linux/module.h"
1156struct module;
1157#line 37
1158struct module_param_attrs;
1159#line 37 "include/linux/module.h"
1160struct module_kobject {
1161   struct kobject kobj ;
1162   struct module *mod ;
1163   struct kobject *drivers_dir ;
1164   struct module_param_attrs *mp ;
1165};
1166#line 44 "include/linux/module.h"
1167struct module_attribute {
1168   struct attribute attr ;
1169   ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
1170   ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const   * ,
1171                    size_t count ) ;
1172   void (*setup)(struct module * , char const   * ) ;
1173   int (*test)(struct module * ) ;
1174   void (*free)(struct module * ) ;
1175};
1176#line 71
1177struct exception_table_entry;
1178#line 71
1179struct exception_table_entry;
1180#line 199
1181enum module_state {
1182    MODULE_STATE_LIVE = 0,
1183    MODULE_STATE_COMING = 1,
1184    MODULE_STATE_GOING = 2
1185} ;
1186#line 215 "include/linux/module.h"
1187struct module_ref {
1188   unsigned long incs ;
1189   unsigned long decs ;
1190} __attribute__((__aligned__((2) *  (sizeof(unsigned long )) ))) ;
1191#line 220
1192struct module_sect_attrs;
1193#line 220
1194struct module_notes_attrs;
1195#line 220
1196struct ftrace_event_call;
1197#line 220 "include/linux/module.h"
1198struct module {
1199   enum module_state state ;
1200   struct list_head list ;
1201   char name[64UL - sizeof(unsigned long )] ;
1202   struct module_kobject mkobj ;
1203   struct module_attribute *modinfo_attrs ;
1204   char const   *version ;
1205   char const   *srcversion ;
1206   struct kobject *holders_dir ;
1207   struct kernel_symbol  const  *syms ;
1208   unsigned long const   *crcs ;
1209   unsigned int num_syms ;
1210   struct kernel_param *kp ;
1211   unsigned int num_kp ;
1212   unsigned int num_gpl_syms ;
1213   struct kernel_symbol  const  *gpl_syms ;
1214   unsigned long const   *gpl_crcs ;
1215   struct kernel_symbol  const  *unused_syms ;
1216   unsigned long const   *unused_crcs ;
1217   unsigned int num_unused_syms ;
1218   unsigned int num_unused_gpl_syms ;
1219   struct kernel_symbol  const  *unused_gpl_syms ;
1220   unsigned long const   *unused_gpl_crcs ;
1221   struct kernel_symbol  const  *gpl_future_syms ;
1222   unsigned long const   *gpl_future_crcs ;
1223   unsigned int num_gpl_future_syms ;
1224   unsigned int num_exentries ;
1225   struct exception_table_entry *extable ;
1226   int (*init)(void) ;
1227   void *module_init ;
1228   void *module_core ;
1229   unsigned int init_size ;
1230   unsigned int core_size ;
1231   unsigned int init_text_size ;
1232   unsigned int core_text_size ;
1233   unsigned int init_ro_size ;
1234   unsigned int core_ro_size ;
1235   struct mod_arch_specific arch ;
1236   unsigned int taints ;
1237   unsigned int num_bugs ;
1238   struct list_head bug_list ;
1239   struct bug_entry *bug_table ;
1240   Elf64_Sym *symtab ;
1241   Elf64_Sym *core_symtab ;
1242   unsigned int num_symtab ;
1243   unsigned int core_num_syms ;
1244   char *strtab ;
1245   char *core_strtab ;
1246   struct module_sect_attrs *sect_attrs ;
1247   struct module_notes_attrs *notes_attrs ;
1248   char *args ;
1249   void *percpu ;
1250   unsigned int percpu_size ;
1251   unsigned int num_tracepoints ;
1252   struct tracepoint * const  *tracepoints_ptrs ;
1253   unsigned int num_trace_bprintk_fmt ;
1254   char const   **trace_bprintk_fmt_start ;
1255   struct ftrace_event_call **trace_events ;
1256   unsigned int num_trace_events ;
1257   struct list_head source_list ;
1258   struct list_head target_list ;
1259   struct task_struct *waiter ;
1260   void (*exit)(void) ;
1261   struct module_ref *refptr ;
1262   ctor_fn_t *ctors ;
1263   unsigned int num_ctors ;
1264};
1265#line 46 "include/linux/slub_def.h"
1266struct kmem_cache_cpu {
1267   void **freelist ;
1268   unsigned long tid ;
1269   struct page *page ;
1270   struct page *partial ;
1271   int node ;
1272   unsigned int stat[26] ;
1273};
1274#line 57 "include/linux/slub_def.h"
1275struct kmem_cache_node {
1276   spinlock_t list_lock ;
1277   unsigned long nr_partial ;
1278   struct list_head partial ;
1279   atomic_long_t nr_slabs ;
1280   atomic_long_t total_objects ;
1281   struct list_head full ;
1282};
1283#line 73 "include/linux/slub_def.h"
1284struct kmem_cache_order_objects {
1285   unsigned long x ;
1286};
1287#line 80 "include/linux/slub_def.h"
1288struct kmem_cache {
1289   struct kmem_cache_cpu *cpu_slab ;
1290   unsigned long flags ;
1291   unsigned long min_partial ;
1292   int size ;
1293   int objsize ;
1294   int offset ;
1295   int cpu_partial ;
1296   struct kmem_cache_order_objects oo ;
1297   struct kmem_cache_order_objects max ;
1298   struct kmem_cache_order_objects min ;
1299   gfp_t allocflags ;
1300   int refcount ;
1301   void (*ctor)(void * ) ;
1302   int inuse ;
1303   int align ;
1304   int reserved ;
1305   char const   *name ;
1306   struct list_head list ;
1307   struct kobject kobj ;
1308   int remote_node_defrag_ratio ;
1309   struct kmem_cache_node *node[1 << 10] ;
1310};
1311#line 12 "include/linux/mod_devicetable.h"
1312typedef unsigned long kernel_ulong_t;
1313#line 219 "include/linux/mod_devicetable.h"
1314struct of_device_id {
1315   char name[32] ;
1316   char type[32] ;
1317   char compatible[128] ;
1318   void *data ;
1319};
1320#line 442 "include/linux/mod_devicetable.h"
1321struct spi_device_id {
1322   char name[32] ;
1323   kernel_ulong_t driver_data  __attribute__((__aligned__(sizeof(kernel_ulong_t )))) ;
1324};
1325#line 18 "include/linux/capability.h"
1326struct task_struct;
1327#line 94 "include/linux/capability.h"
1328struct kernel_cap_struct {
1329   __u32 cap[2] ;
1330};
1331#line 94 "include/linux/capability.h"
1332typedef struct kernel_cap_struct kernel_cap_t;
1333#line 378
1334struct user_namespace;
1335#line 378
1336struct user_namespace;
1337#line 14 "include/linux/prio_tree.h"
1338struct prio_tree_node;
1339#line 14 "include/linux/prio_tree.h"
1340struct raw_prio_tree_node {
1341   struct prio_tree_node *left ;
1342   struct prio_tree_node *right ;
1343   struct prio_tree_node *parent ;
1344};
1345#line 20 "include/linux/prio_tree.h"
1346struct prio_tree_node {
1347   struct prio_tree_node *left ;
1348   struct prio_tree_node *right ;
1349   struct prio_tree_node *parent ;
1350   unsigned long start ;
1351   unsigned long last ;
1352};
1353#line 23 "include/linux/mm_types.h"
1354struct address_space;
1355#line 23
1356struct address_space;
1357#line 40 "include/linux/mm_types.h"
1358union __anonunion____missing_field_name_204 {
1359   unsigned long index ;
1360   void *freelist ;
1361};
1362#line 40 "include/linux/mm_types.h"
1363struct __anonstruct____missing_field_name_208 {
1364   unsigned int inuse : 16 ;
1365   unsigned int objects : 15 ;
1366   unsigned int frozen : 1 ;
1367};
1368#line 40 "include/linux/mm_types.h"
1369union __anonunion____missing_field_name_207 {
1370   atomic_t _mapcount ;
1371   struct __anonstruct____missing_field_name_208 __annonCompField34 ;
1372};
1373#line 40 "include/linux/mm_types.h"
1374struct __anonstruct____missing_field_name_206 {
1375   union __anonunion____missing_field_name_207 __annonCompField35 ;
1376   atomic_t _count ;
1377};
1378#line 40 "include/linux/mm_types.h"
1379union __anonunion____missing_field_name_205 {
1380   unsigned long counters ;
1381   struct __anonstruct____missing_field_name_206 __annonCompField36 ;
1382};
1383#line 40 "include/linux/mm_types.h"
1384struct __anonstruct____missing_field_name_203 {
1385   union __anonunion____missing_field_name_204 __annonCompField33 ;
1386   union __anonunion____missing_field_name_205 __annonCompField37 ;
1387};
1388#line 40 "include/linux/mm_types.h"
1389struct __anonstruct____missing_field_name_210 {
1390   struct page *next ;
1391   int pages ;
1392   int pobjects ;
1393};
1394#line 40 "include/linux/mm_types.h"
1395union __anonunion____missing_field_name_209 {
1396   struct list_head lru ;
1397   struct __anonstruct____missing_field_name_210 __annonCompField39 ;
1398};
1399#line 40 "include/linux/mm_types.h"
1400union __anonunion____missing_field_name_211 {
1401   unsigned long private ;
1402   struct kmem_cache *slab ;
1403   struct page *first_page ;
1404};
1405#line 40 "include/linux/mm_types.h"
1406struct page {
1407   unsigned long flags ;
1408   struct address_space *mapping ;
1409   struct __anonstruct____missing_field_name_203 __annonCompField38 ;
1410   union __anonunion____missing_field_name_209 __annonCompField40 ;
1411   union __anonunion____missing_field_name_211 __annonCompField41 ;
1412   unsigned long debug_flags ;
1413} __attribute__((__aligned__((2) *  (sizeof(unsigned long )) ))) ;
1414#line 200 "include/linux/mm_types.h"
1415struct __anonstruct_vm_set_213 {
1416   struct list_head list ;
1417   void *parent ;
1418   struct vm_area_struct *head ;
1419};
1420#line 200 "include/linux/mm_types.h"
1421union __anonunion_shared_212 {
1422   struct __anonstruct_vm_set_213 vm_set ;
1423   struct raw_prio_tree_node prio_tree_node ;
1424};
1425#line 200
1426struct anon_vma;
1427#line 200
1428struct vm_operations_struct;
1429#line 200
1430struct mempolicy;
1431#line 200 "include/linux/mm_types.h"
1432struct vm_area_struct {
1433   struct mm_struct *vm_mm ;
1434   unsigned long vm_start ;
1435   unsigned long vm_end ;
1436   struct vm_area_struct *vm_next ;
1437   struct vm_area_struct *vm_prev ;
1438   pgprot_t vm_page_prot ;
1439   unsigned long vm_flags ;
1440   struct rb_node vm_rb ;
1441   union __anonunion_shared_212 shared ;
1442   struct list_head anon_vma_chain ;
1443   struct anon_vma *anon_vma ;
1444   struct vm_operations_struct  const  *vm_ops ;
1445   unsigned long vm_pgoff ;
1446   struct file *vm_file ;
1447   void *vm_private_data ;
1448   struct mempolicy *vm_policy ;
1449};
1450#line 257 "include/linux/mm_types.h"
1451struct core_thread {
1452   struct task_struct *task ;
1453   struct core_thread *next ;
1454};
1455#line 262 "include/linux/mm_types.h"
1456struct core_state {
1457   atomic_t nr_threads ;
1458   struct core_thread dumper ;
1459   struct completion startup ;
1460};
1461#line 284 "include/linux/mm_types.h"
1462struct mm_rss_stat {
1463   atomic_long_t count[3] ;
1464};
1465#line 288
1466struct linux_binfmt;
1467#line 288
1468struct mmu_notifier_mm;
1469#line 288 "include/linux/mm_types.h"
1470struct mm_struct {
1471   struct vm_area_struct *mmap ;
1472   struct rb_root mm_rb ;
1473   struct vm_area_struct *mmap_cache ;
1474   unsigned long (*get_unmapped_area)(struct file *filp , unsigned long addr , unsigned long len ,
1475                                      unsigned long pgoff , unsigned long flags ) ;
1476   void (*unmap_area)(struct mm_struct *mm , unsigned long addr ) ;
1477   unsigned long mmap_base ;
1478   unsigned long task_size ;
1479   unsigned long cached_hole_size ;
1480   unsigned long free_area_cache ;
1481   pgd_t *pgd ;
1482   atomic_t mm_users ;
1483   atomic_t mm_count ;
1484   int map_count ;
1485   spinlock_t page_table_lock ;
1486   struct rw_semaphore mmap_sem ;
1487   struct list_head mmlist ;
1488   unsigned long hiwater_rss ;
1489   unsigned long hiwater_vm ;
1490   unsigned long total_vm ;
1491   unsigned long locked_vm ;
1492   unsigned long pinned_vm ;
1493   unsigned long shared_vm ;
1494   unsigned long exec_vm ;
1495   unsigned long stack_vm ;
1496   unsigned long reserved_vm ;
1497   unsigned long def_flags ;
1498   unsigned long nr_ptes ;
1499   unsigned long start_code ;
1500   unsigned long end_code ;
1501   unsigned long start_data ;
1502   unsigned long end_data ;
1503   unsigned long start_brk ;
1504   unsigned long brk ;
1505   unsigned long start_stack ;
1506   unsigned long arg_start ;
1507   unsigned long arg_end ;
1508   unsigned long env_start ;
1509   unsigned long env_end ;
1510   unsigned long saved_auxv[44] ;
1511   struct mm_rss_stat rss_stat ;
1512   struct linux_binfmt *binfmt ;
1513   cpumask_var_t cpu_vm_mask_var ;
1514   mm_context_t context ;
1515   unsigned int faultstamp ;
1516   unsigned int token_priority ;
1517   unsigned int last_interval ;
1518   unsigned long flags ;
1519   struct core_state *core_state ;
1520   spinlock_t ioctx_lock ;
1521   struct hlist_head ioctx_list ;
1522   struct task_struct *owner ;
1523   struct file *exe_file ;
1524   unsigned long num_exe_file_vmas ;
1525   struct mmu_notifier_mm *mmu_notifier_mm ;
1526   pgtable_t pmd_huge_pte ;
1527   struct cpumask cpumask_allocation ;
1528};
1529#line 7 "include/asm-generic/cputime.h"
1530typedef unsigned long cputime_t;
1531#line 84 "include/linux/sem.h"
1532struct task_struct;
1533#line 101
1534struct sem_undo_list;
1535#line 101 "include/linux/sem.h"
1536struct sysv_sem {
1537   struct sem_undo_list *undo_list ;
1538};
1539#line 10 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1540struct siginfo;
1541#line 10
1542struct siginfo;
1543#line 30 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1544struct __anonstruct_sigset_t_215 {
1545   unsigned long sig[1] ;
1546};
1547#line 30 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1548typedef struct __anonstruct_sigset_t_215 sigset_t;
1549#line 17 "include/asm-generic/signal-defs.h"
1550typedef void __signalfn_t(int  );
1551#line 18 "include/asm-generic/signal-defs.h"
1552typedef __signalfn_t *__sighandler_t;
1553#line 20 "include/asm-generic/signal-defs.h"
1554typedef void __restorefn_t(void);
1555#line 21 "include/asm-generic/signal-defs.h"
1556typedef __restorefn_t *__sigrestore_t;
1557#line 167 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1558struct sigaction {
1559   __sighandler_t sa_handler ;
1560   unsigned long sa_flags ;
1561   __sigrestore_t sa_restorer ;
1562   sigset_t sa_mask ;
1563};
1564#line 174 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1565struct k_sigaction {
1566   struct sigaction sa ;
1567};
1568#line 7 "include/asm-generic/siginfo.h"
1569union sigval {
1570   int sival_int ;
1571   void *sival_ptr ;
1572};
1573#line 7 "include/asm-generic/siginfo.h"
1574typedef union sigval sigval_t;
1575#line 48 "include/asm-generic/siginfo.h"
1576struct __anonstruct__kill_217 {
1577   __kernel_pid_t _pid ;
1578   __kernel_uid32_t _uid ;
1579};
1580#line 48 "include/asm-generic/siginfo.h"
1581struct __anonstruct__timer_218 {
1582   __kernel_timer_t _tid ;
1583   int _overrun ;
1584   char _pad[sizeof(__kernel_uid32_t ) - sizeof(int )] ;
1585   sigval_t _sigval ;
1586   int _sys_private ;
1587};
1588#line 48 "include/asm-generic/siginfo.h"
1589struct __anonstruct__rt_219 {
1590   __kernel_pid_t _pid ;
1591   __kernel_uid32_t _uid ;
1592   sigval_t _sigval ;
1593};
1594#line 48 "include/asm-generic/siginfo.h"
1595struct __anonstruct__sigchld_220 {
1596   __kernel_pid_t _pid ;
1597   __kernel_uid32_t _uid ;
1598   int _status ;
1599   __kernel_clock_t _utime ;
1600   __kernel_clock_t _stime ;
1601};
1602#line 48 "include/asm-generic/siginfo.h"
1603struct __anonstruct__sigfault_221 {
1604   void *_addr ;
1605   short _addr_lsb ;
1606};
1607#line 48 "include/asm-generic/siginfo.h"
1608struct __anonstruct__sigpoll_222 {
1609   long _band ;
1610   int _fd ;
1611};
1612#line 48 "include/asm-generic/siginfo.h"
1613union __anonunion__sifields_216 {
1614   int _pad[(128UL - 4UL * sizeof(int )) / sizeof(int )] ;
1615   struct __anonstruct__kill_217 _kill ;
1616   struct __anonstruct__timer_218 _timer ;
1617   struct __anonstruct__rt_219 _rt ;
1618   struct __anonstruct__sigchld_220 _sigchld ;
1619   struct __anonstruct__sigfault_221 _sigfault ;
1620   struct __anonstruct__sigpoll_222 _sigpoll ;
1621};
1622#line 48 "include/asm-generic/siginfo.h"
1623struct siginfo {
1624   int si_signo ;
1625   int si_errno ;
1626   int si_code ;
1627   union __anonunion__sifields_216 _sifields ;
1628};
1629#line 48 "include/asm-generic/siginfo.h"
1630typedef struct siginfo siginfo_t;
1631#line 288
1632struct siginfo;
1633#line 10 "include/linux/signal.h"
1634struct task_struct;
1635#line 18
1636struct user_struct;
1637#line 28 "include/linux/signal.h"
1638struct sigpending {
1639   struct list_head list ;
1640   sigset_t signal ;
1641};
1642#line 239
1643struct timespec;
1644#line 240
1645struct pt_regs;
1646#line 50 "include/linux/pid.h"
1647struct pid_namespace;
1648#line 50 "include/linux/pid.h"
1649struct upid {
1650   int nr ;
1651   struct pid_namespace *ns ;
1652   struct hlist_node pid_chain ;
1653};
1654#line 57 "include/linux/pid.h"
1655struct pid {
1656   atomic_t count ;
1657   unsigned int level ;
1658   struct hlist_head tasks[3] ;
1659   struct rcu_head rcu ;
1660   struct upid numbers[1] ;
1661};
1662#line 69 "include/linux/pid.h"
1663struct pid_link {
1664   struct hlist_node node ;
1665   struct pid *pid ;
1666};
1667#line 100
1668struct pid_namespace;
1669#line 10 "include/linux/seccomp.h"
1670struct __anonstruct_seccomp_t_225 {
1671   int mode ;
1672};
1673#line 10 "include/linux/seccomp.h"
1674typedef struct __anonstruct_seccomp_t_225 seccomp_t;
1675#line 81 "include/linux/plist.h"
1676struct plist_head {
1677   struct list_head node_list ;
1678};
1679#line 85 "include/linux/plist.h"
1680struct plist_node {
1681   int prio ;
1682   struct list_head prio_list ;
1683   struct list_head node_list ;
1684};
1685#line 40 "include/linux/rtmutex.h"
1686struct rt_mutex_waiter;
1687#line 40
1688struct rt_mutex_waiter;
1689#line 42 "include/linux/resource.h"
1690struct rlimit {
1691   unsigned long rlim_cur ;
1692   unsigned long rlim_max ;
1693};
1694#line 81
1695struct task_struct;
1696#line 8 "include/linux/timerqueue.h"
1697struct timerqueue_node {
1698   struct rb_node node ;
1699   ktime_t expires ;
1700};
1701#line 13 "include/linux/timerqueue.h"
1702struct timerqueue_head {
1703   struct rb_root head ;
1704   struct timerqueue_node *next ;
1705};
1706#line 27 "include/linux/hrtimer.h"
1707struct hrtimer_clock_base;
1708#line 27
1709struct hrtimer_clock_base;
1710#line 28
1711struct hrtimer_cpu_base;
1712#line 28
1713struct hrtimer_cpu_base;
1714#line 44
1715enum hrtimer_restart {
1716    HRTIMER_NORESTART = 0,
1717    HRTIMER_RESTART = 1
1718} ;
1719#line 108 "include/linux/hrtimer.h"
1720struct hrtimer {
1721   struct timerqueue_node node ;
1722   ktime_t _softexpires ;
1723   enum hrtimer_restart (*function)(struct hrtimer * ) ;
1724   struct hrtimer_clock_base *base ;
1725   unsigned long state ;
1726   int start_pid ;
1727   void *start_site ;
1728   char start_comm[16] ;
1729};
1730#line 145 "include/linux/hrtimer.h"
1731struct hrtimer_clock_base {
1732   struct hrtimer_cpu_base *cpu_base ;
1733   int index ;
1734   clockid_t clockid ;
1735   struct timerqueue_head active ;
1736   ktime_t resolution ;
1737   ktime_t (*get_time)(void) ;
1738   ktime_t softirq_time ;
1739   ktime_t offset ;
1740};
1741#line 178 "include/linux/hrtimer.h"
1742struct hrtimer_cpu_base {
1743   raw_spinlock_t lock ;
1744   unsigned long active_bases ;
1745   ktime_t expires_next ;
1746   int hres_active ;
1747   int hang_detected ;
1748   unsigned long nr_events ;
1749   unsigned long nr_retries ;
1750   unsigned long nr_hangs ;
1751   ktime_t max_hang_time ;
1752   struct hrtimer_clock_base clock_base[3] ;
1753};
1754#line 11 "include/linux/task_io_accounting.h"
1755struct task_io_accounting {
1756   u64 rchar ;
1757   u64 wchar ;
1758   u64 syscr ;
1759   u64 syscw ;
1760   u64 read_bytes ;
1761   u64 write_bytes ;
1762   u64 cancelled_write_bytes ;
1763};
1764#line 13 "include/linux/latencytop.h"
1765struct task_struct;
1766#line 20 "include/linux/latencytop.h"
1767struct latency_record {
1768   unsigned long backtrace[12] ;
1769   unsigned int count ;
1770   unsigned long time ;
1771   unsigned long max ;
1772};
1773#line 29 "include/linux/key.h"
1774typedef int32_t key_serial_t;
1775#line 32 "include/linux/key.h"
1776typedef uint32_t key_perm_t;
1777#line 34
1778struct key;
1779#line 34
1780struct key;
1781#line 75
1782struct user_struct;
1783#line 76
1784struct signal_struct;
1785#line 76
1786struct signal_struct;
1787#line 77
1788struct cred;
1789#line 79
1790struct key_type;
1791#line 79
1792struct key_type;
1793#line 81
1794struct keyring_list;
1795#line 81
1796struct keyring_list;
1797#line 124
1798struct key_user;
1799#line 124 "include/linux/key.h"
1800union __anonunion____missing_field_name_226 {
1801   time_t expiry ;
1802   time_t revoked_at ;
1803};
1804#line 124 "include/linux/key.h"
1805union __anonunion_type_data_227 {
1806   struct list_head link ;
1807   unsigned long x[2] ;
1808   void *p[2] ;
1809   int reject_error ;
1810};
1811#line 124 "include/linux/key.h"
1812union __anonunion_payload_228 {
1813   unsigned long value ;
1814   void *rcudata ;
1815   void *data ;
1816   struct keyring_list *subscriptions ;
1817};
1818#line 124 "include/linux/key.h"
1819struct key {
1820   atomic_t usage ;
1821   key_serial_t serial ;
1822   struct rb_node serial_node ;
1823   struct key_type *type ;
1824   struct rw_semaphore sem ;
1825   struct key_user *user ;
1826   void *security ;
1827   union __anonunion____missing_field_name_226 __annonCompField42 ;
1828   uid_t uid ;
1829   gid_t gid ;
1830   key_perm_t perm ;
1831   unsigned short quotalen ;
1832   unsigned short datalen ;
1833   unsigned long flags ;
1834   char *description ;
1835   union __anonunion_type_data_227 type_data ;
1836   union __anonunion_payload_228 payload ;
1837};
1838#line 18 "include/linux/selinux.h"
1839struct audit_context;
1840#line 18
1841struct audit_context;
1842#line 21 "include/linux/cred.h"
1843struct user_struct;
1844#line 22
1845struct cred;
1846#line 31 "include/linux/cred.h"
1847struct group_info {
1848   atomic_t usage ;
1849   int ngroups ;
1850   int nblocks ;
1851   gid_t small_block[32] ;
1852   gid_t *blocks[0] ;
1853};
1854#line 83 "include/linux/cred.h"
1855struct thread_group_cred {
1856   atomic_t usage ;
1857   pid_t tgid ;
1858   spinlock_t lock ;
1859   struct key *session_keyring ;
1860   struct key *process_keyring ;
1861   struct rcu_head rcu ;
1862};
1863#line 116 "include/linux/cred.h"
1864struct cred {
1865   atomic_t usage ;
1866   atomic_t subscribers ;
1867   void *put_addr ;
1868   unsigned int magic ;
1869   uid_t uid ;
1870   gid_t gid ;
1871   uid_t suid ;
1872   gid_t sgid ;
1873   uid_t euid ;
1874   gid_t egid ;
1875   uid_t fsuid ;
1876   gid_t fsgid ;
1877   unsigned int securebits ;
1878   kernel_cap_t cap_inheritable ;
1879   kernel_cap_t cap_permitted ;
1880   kernel_cap_t cap_effective ;
1881   kernel_cap_t cap_bset ;
1882   unsigned char jit_keyring ;
1883   struct key *thread_keyring ;
1884   struct key *request_key_auth ;
1885   struct thread_group_cred *tgcred ;
1886   void *security ;
1887   struct user_struct *user ;
1888   struct user_namespace *user_ns ;
1889   struct group_info *group_info ;
1890   struct rcu_head rcu ;
1891};
1892#line 61 "include/linux/llist.h"
1893struct llist_node;
1894#line 65 "include/linux/llist.h"
1895struct llist_node {
1896   struct llist_node *next ;
1897};
1898#line 97 "include/linux/sched.h"
1899struct futex_pi_state;
1900#line 97
1901struct futex_pi_state;
1902#line 98
1903struct robust_list_head;
1904#line 98
1905struct robust_list_head;
1906#line 99
1907struct bio_list;
1908#line 99
1909struct bio_list;
1910#line 100
1911struct fs_struct;
1912#line 100
1913struct fs_struct;
1914#line 101
1915struct perf_event_context;
1916#line 101
1917struct perf_event_context;
1918#line 102
1919struct blk_plug;
1920#line 102
1921struct blk_plug;
1922#line 151
1923struct cfs_rq;
1924#line 151
1925struct cfs_rq;
1926#line 259
1927struct task_struct;
1928#line 366
1929struct nsproxy;
1930#line 367
1931struct user_namespace;
1932#line 214 "include/linux/aio.h"
1933struct mm_struct;
1934#line 443 "include/linux/sched.h"
1935struct sighand_struct {
1936   atomic_t count ;
1937   struct k_sigaction action[64] ;
1938   spinlock_t siglock ;
1939   wait_queue_head_t signalfd_wqh ;
1940};
1941#line 450 "include/linux/sched.h"
1942struct pacct_struct {
1943   int ac_flag ;
1944   long ac_exitcode ;
1945   unsigned long ac_mem ;
1946   cputime_t ac_utime ;
1947   cputime_t ac_stime ;
1948   unsigned long ac_minflt ;
1949   unsigned long ac_majflt ;
1950};
1951#line 458 "include/linux/sched.h"
1952struct cpu_itimer {
1953   cputime_t expires ;
1954   cputime_t incr ;
1955   u32 error ;
1956   u32 incr_error ;
1957};
1958#line 476 "include/linux/sched.h"
1959struct task_cputime {
1960   cputime_t utime ;
1961   cputime_t stime ;
1962   unsigned long long sum_exec_runtime ;
1963};
1964#line 512 "include/linux/sched.h"
1965struct thread_group_cputimer {
1966   struct task_cputime cputime ;
1967   int running ;
1968   raw_spinlock_t lock ;
1969};
1970#line 519
1971struct autogroup;
1972#line 519
1973struct autogroup;
1974#line 528
1975struct tty_struct;
1976#line 528
1977struct taskstats;
1978#line 528
1979struct tty_audit_buf;
1980#line 528 "include/linux/sched.h"
1981struct signal_struct {
1982   atomic_t sigcnt ;
1983   atomic_t live ;
1984   int nr_threads ;
1985   wait_queue_head_t wait_chldexit ;
1986   struct task_struct *curr_target ;
1987   struct sigpending shared_pending ;
1988   int group_exit_code ;
1989   int notify_count ;
1990   struct task_struct *group_exit_task ;
1991   int group_stop_count ;
1992   unsigned int flags ;
1993   unsigned int is_child_subreaper : 1 ;
1994   unsigned int has_child_subreaper : 1 ;
1995   struct list_head posix_timers ;
1996   struct hrtimer real_timer ;
1997   struct pid *leader_pid ;
1998   ktime_t it_real_incr ;
1999   struct cpu_itimer it[2] ;
2000   struct thread_group_cputimer cputimer ;
2001   struct task_cputime cputime_expires ;
2002   struct list_head cpu_timers[3] ;
2003   struct pid *tty_old_pgrp ;
2004   int leader ;
2005   struct tty_struct *tty ;
2006   struct autogroup *autogroup ;
2007   cputime_t utime ;
2008   cputime_t stime ;
2009   cputime_t cutime ;
2010   cputime_t cstime ;
2011   cputime_t gtime ;
2012   cputime_t cgtime ;
2013   cputime_t prev_utime ;
2014   cputime_t prev_stime ;
2015   unsigned long nvcsw ;
2016   unsigned long nivcsw ;
2017   unsigned long cnvcsw ;
2018   unsigned long cnivcsw ;
2019   unsigned long min_flt ;
2020   unsigned long maj_flt ;
2021   unsigned long cmin_flt ;
2022   unsigned long cmaj_flt ;
2023   unsigned long inblock ;
2024   unsigned long oublock ;
2025   unsigned long cinblock ;
2026   unsigned long coublock ;
2027   unsigned long maxrss ;
2028   unsigned long cmaxrss ;
2029   struct task_io_accounting ioac ;
2030   unsigned long long sum_sched_runtime ;
2031   struct rlimit rlim[16] ;
2032   struct pacct_struct pacct ;
2033   struct taskstats *stats ;
2034   unsigned int audit_tty ;
2035   struct tty_audit_buf *tty_audit_buf ;
2036   struct rw_semaphore group_rwsem ;
2037   int oom_adj ;
2038   int oom_score_adj ;
2039   int oom_score_adj_min ;
2040   struct mutex cred_guard_mutex ;
2041};
2042#line 703 "include/linux/sched.h"
2043struct user_struct {
2044   atomic_t __count ;
2045   atomic_t processes ;
2046   atomic_t files ;
2047   atomic_t sigpending ;
2048   atomic_t inotify_watches ;
2049   atomic_t inotify_devs ;
2050   atomic_t fanotify_listeners ;
2051   atomic_long_t epoll_watches ;
2052   unsigned long mq_bytes ;
2053   unsigned long locked_shm ;
2054   struct key *uid_keyring ;
2055   struct key *session_keyring ;
2056   struct hlist_node uidhash_node ;
2057   uid_t uid ;
2058   struct user_namespace *user_ns ;
2059   atomic_long_t locked_vm ;
2060};
2061#line 747
2062struct backing_dev_info;
2063#line 747
2064struct backing_dev_info;
2065#line 748
2066struct reclaim_state;
2067#line 748
2068struct reclaim_state;
2069#line 751 "include/linux/sched.h"
2070struct sched_info {
2071   unsigned long pcount ;
2072   unsigned long long run_delay ;
2073   unsigned long long last_arrival ;
2074   unsigned long long last_queued ;
2075};
2076#line 763 "include/linux/sched.h"
2077struct task_delay_info {
2078   spinlock_t lock ;
2079   unsigned int flags ;
2080   struct timespec blkio_start ;
2081   struct timespec blkio_end ;
2082   u64 blkio_delay ;
2083   u64 swapin_delay ;
2084   u32 blkio_count ;
2085   u32 swapin_count ;
2086   struct timespec freepages_start ;
2087   struct timespec freepages_end ;
2088   u64 freepages_delay ;
2089   u32 freepages_count ;
2090};
2091#line 1088
2092struct io_context;
2093#line 1088
2094struct io_context;
2095#line 1097
2096struct audit_context;
2097#line 1098
2098struct mempolicy;
2099#line 1099
2100struct pipe_inode_info;
2101#line 1099
2102struct pipe_inode_info;
2103#line 1102
2104struct rq;
2105#line 1102
2106struct rq;
2107#line 1122 "include/linux/sched.h"
2108struct sched_class {
2109   struct sched_class  const  *next ;
2110   void (*enqueue_task)(struct rq *rq , struct task_struct *p , int flags ) ;
2111   void (*dequeue_task)(struct rq *rq , struct task_struct *p , int flags ) ;
2112   void (*yield_task)(struct rq *rq ) ;
2113   bool (*yield_to_task)(struct rq *rq , struct task_struct *p , bool preempt ) ;
2114   void (*check_preempt_curr)(struct rq *rq , struct task_struct *p , int flags ) ;
2115   struct task_struct *(*pick_next_task)(struct rq *rq ) ;
2116   void (*put_prev_task)(struct rq *rq , struct task_struct *p ) ;
2117   int (*select_task_rq)(struct task_struct *p , int sd_flag , int flags ) ;
2118   void (*pre_schedule)(struct rq *this_rq , struct task_struct *task ) ;
2119   void (*post_schedule)(struct rq *this_rq ) ;
2120   void (*task_waking)(struct task_struct *task ) ;
2121   void (*task_woken)(struct rq *this_rq , struct task_struct *task ) ;
2122   void (*set_cpus_allowed)(struct task_struct *p , struct cpumask  const  *newmask ) ;
2123   void (*rq_online)(struct rq *rq ) ;
2124   void (*rq_offline)(struct rq *rq ) ;
2125   void (*set_curr_task)(struct rq *rq ) ;
2126   void (*task_tick)(struct rq *rq , struct task_struct *p , int queued ) ;
2127   void (*task_fork)(struct task_struct *p ) ;
2128   void (*switched_from)(struct rq *this_rq , struct task_struct *task ) ;
2129   void (*switched_to)(struct rq *this_rq , struct task_struct *task ) ;
2130   void (*prio_changed)(struct rq *this_rq , struct task_struct *task , int oldprio ) ;
2131   unsigned int (*get_rr_interval)(struct rq *rq , struct task_struct *task ) ;
2132   void (*task_move_group)(struct task_struct *p , int on_rq ) ;
2133};
2134#line 1167 "include/linux/sched.h"
2135struct load_weight {
2136   unsigned long weight ;
2137   unsigned long inv_weight ;
2138};
2139#line 1172 "include/linux/sched.h"
2140struct sched_statistics {
2141   u64 wait_start ;
2142   u64 wait_max ;
2143   u64 wait_count ;
2144   u64 wait_sum ;
2145   u64 iowait_count ;
2146   u64 iowait_sum ;
2147   u64 sleep_start ;
2148   u64 sleep_max ;
2149   s64 sum_sleep_runtime ;
2150   u64 block_start ;
2151   u64 block_max ;
2152   u64 exec_max ;
2153   u64 slice_max ;
2154   u64 nr_migrations_cold ;
2155   u64 nr_failed_migrations_affine ;
2156   u64 nr_failed_migrations_running ;
2157   u64 nr_failed_migrations_hot ;
2158   u64 nr_forced_migrations ;
2159   u64 nr_wakeups ;
2160   u64 nr_wakeups_sync ;
2161   u64 nr_wakeups_migrate ;
2162   u64 nr_wakeups_local ;
2163   u64 nr_wakeups_remote ;
2164   u64 nr_wakeups_affine ;
2165   u64 nr_wakeups_affine_attempts ;
2166   u64 nr_wakeups_passive ;
2167   u64 nr_wakeups_idle ;
2168};
2169#line 1207 "include/linux/sched.h"
2170struct sched_entity {
2171   struct load_weight load ;
2172   struct rb_node run_node ;
2173   struct list_head group_node ;
2174   unsigned int on_rq ;
2175   u64 exec_start ;
2176   u64 sum_exec_runtime ;
2177   u64 vruntime ;
2178   u64 prev_sum_exec_runtime ;
2179   u64 nr_migrations ;
2180   struct sched_statistics statistics ;
2181   struct sched_entity *parent ;
2182   struct cfs_rq *cfs_rq ;
2183   struct cfs_rq *my_q ;
2184};
2185#line 1233
2186struct rt_rq;
2187#line 1233 "include/linux/sched.h"
2188struct sched_rt_entity {
2189   struct list_head run_list ;
2190   unsigned long timeout ;
2191   unsigned int time_slice ;
2192   int nr_cpus_allowed ;
2193   struct sched_rt_entity *back ;
2194   struct sched_rt_entity *parent ;
2195   struct rt_rq *rt_rq ;
2196   struct rt_rq *my_q ;
2197};
2198#line 1264
2199struct files_struct;
2200#line 1264
2201struct css_set;
2202#line 1264
2203struct compat_robust_list_head;
2204#line 1264
2205struct mem_cgroup;
2206#line 1264 "include/linux/sched.h"
2207struct memcg_batch_info {
2208   int do_batch ;
2209   struct mem_cgroup *memcg ;
2210   unsigned long nr_pages ;
2211   unsigned long memsw_nr_pages ;
2212};
2213#line 1264 "include/linux/sched.h"
2214struct task_struct {
2215   long volatile   state ;
2216   void *stack ;
2217   atomic_t usage ;
2218   unsigned int flags ;
2219   unsigned int ptrace ;
2220   struct llist_node wake_entry ;
2221   int on_cpu ;
2222   int on_rq ;
2223   int prio ;
2224   int static_prio ;
2225   int normal_prio ;
2226   unsigned int rt_priority ;
2227   struct sched_class  const  *sched_class ;
2228   struct sched_entity se ;
2229   struct sched_rt_entity rt ;
2230   struct hlist_head preempt_notifiers ;
2231   unsigned char fpu_counter ;
2232   unsigned int policy ;
2233   cpumask_t cpus_allowed ;
2234   struct sched_info sched_info ;
2235   struct list_head tasks ;
2236   struct plist_node pushable_tasks ;
2237   struct mm_struct *mm ;
2238   struct mm_struct *active_mm ;
2239   unsigned int brk_randomized : 1 ;
2240   int exit_state ;
2241   int exit_code ;
2242   int exit_signal ;
2243   int pdeath_signal ;
2244   unsigned int jobctl ;
2245   unsigned int personality ;
2246   unsigned int did_exec : 1 ;
2247   unsigned int in_execve : 1 ;
2248   unsigned int in_iowait : 1 ;
2249   unsigned int sched_reset_on_fork : 1 ;
2250   unsigned int sched_contributes_to_load : 1 ;
2251   unsigned int irq_thread : 1 ;
2252   pid_t pid ;
2253   pid_t tgid ;
2254   unsigned long stack_canary ;
2255   struct task_struct *real_parent ;
2256   struct task_struct *parent ;
2257   struct list_head children ;
2258   struct list_head sibling ;
2259   struct task_struct *group_leader ;
2260   struct list_head ptraced ;
2261   struct list_head ptrace_entry ;
2262   struct pid_link pids[3] ;
2263   struct list_head thread_group ;
2264   struct completion *vfork_done ;
2265   int *set_child_tid ;
2266   int *clear_child_tid ;
2267   cputime_t utime ;
2268   cputime_t stime ;
2269   cputime_t utimescaled ;
2270   cputime_t stimescaled ;
2271   cputime_t gtime ;
2272   cputime_t prev_utime ;
2273   cputime_t prev_stime ;
2274   unsigned long nvcsw ;
2275   unsigned long nivcsw ;
2276   struct timespec start_time ;
2277   struct timespec real_start_time ;
2278   unsigned long min_flt ;
2279   unsigned long maj_flt ;
2280   struct task_cputime cputime_expires ;
2281   struct list_head cpu_timers[3] ;
2282   struct cred  const  *real_cred ;
2283   struct cred  const  *cred ;
2284   struct cred *replacement_session_keyring ;
2285   char comm[16] ;
2286   int link_count ;
2287   int total_link_count ;
2288   struct sysv_sem sysvsem ;
2289   unsigned long last_switch_count ;
2290   struct thread_struct thread ;
2291   struct fs_struct *fs ;
2292   struct files_struct *files ;
2293   struct nsproxy *nsproxy ;
2294   struct signal_struct *signal ;
2295   struct sighand_struct *sighand ;
2296   sigset_t blocked ;
2297   sigset_t real_blocked ;
2298   sigset_t saved_sigmask ;
2299   struct sigpending pending ;
2300   unsigned long sas_ss_sp ;
2301   size_t sas_ss_size ;
2302   int (*notifier)(void *priv ) ;
2303   void *notifier_data ;
2304   sigset_t *notifier_mask ;
2305   struct audit_context *audit_context ;
2306   uid_t loginuid ;
2307   unsigned int sessionid ;
2308   seccomp_t seccomp ;
2309   u32 parent_exec_id ;
2310   u32 self_exec_id ;
2311   spinlock_t alloc_lock ;
2312   raw_spinlock_t pi_lock ;
2313   struct plist_head pi_waiters ;
2314   struct rt_mutex_waiter *pi_blocked_on ;
2315   struct mutex_waiter *blocked_on ;
2316   unsigned int irq_events ;
2317   unsigned long hardirq_enable_ip ;
2318   unsigned long hardirq_disable_ip ;
2319   unsigned int hardirq_enable_event ;
2320   unsigned int hardirq_disable_event ;
2321   int hardirqs_enabled ;
2322   int hardirq_context ;
2323   unsigned long softirq_disable_ip ;
2324   unsigned long softirq_enable_ip ;
2325   unsigned int softirq_disable_event ;
2326   unsigned int softirq_enable_event ;
2327   int softirqs_enabled ;
2328   int softirq_context ;
2329   void *journal_info ;
2330   struct bio_list *bio_list ;
2331   struct blk_plug *plug ;
2332   struct reclaim_state *reclaim_state ;
2333   struct backing_dev_info *backing_dev_info ;
2334   struct io_context *io_context ;
2335   unsigned long ptrace_message ;
2336   siginfo_t *last_siginfo ;
2337   struct task_io_accounting ioac ;
2338   u64 acct_rss_mem1 ;
2339   u64 acct_vm_mem1 ;
2340   cputime_t acct_timexpd ;
2341   nodemask_t mems_allowed ;
2342   seqcount_t mems_allowed_seq ;
2343   int cpuset_mem_spread_rotor ;
2344   int cpuset_slab_spread_rotor ;
2345   struct css_set *cgroups ;
2346   struct list_head cg_list ;
2347   struct robust_list_head *robust_list ;
2348   struct compat_robust_list_head *compat_robust_list ;
2349   struct list_head pi_state_list ;
2350   struct futex_pi_state *pi_state_cache ;
2351   struct perf_event_context *perf_event_ctxp[2] ;
2352   struct mutex perf_event_mutex ;
2353   struct list_head perf_event_list ;
2354   struct mempolicy *mempolicy ;
2355   short il_next ;
2356   short pref_node_fork ;
2357   struct rcu_head rcu ;
2358   struct pipe_inode_info *splice_pipe ;
2359   struct task_delay_info *delays ;
2360   int make_it_fail ;
2361   int nr_dirtied ;
2362   int nr_dirtied_pause ;
2363   unsigned long dirty_paused_when ;
2364   int latency_record_count ;
2365   struct latency_record latency_record[32] ;
2366   unsigned long timer_slack_ns ;
2367   unsigned long default_timer_slack_ns ;
2368   struct list_head *scm_work_list ;
2369   unsigned long trace ;
2370   unsigned long trace_recursion ;
2371   struct memcg_batch_info memcg_batch ;
2372   atomic_t ptrace_bp_refcnt ;
2373};
2374#line 1681
2375struct pid_namespace;
2376#line 55 "include/linux/kthread.h"
2377struct kthread_work;
2378#line 55
2379struct kthread_work;
2380#line 58 "include/linux/kthread.h"
2381struct kthread_worker {
2382   spinlock_t lock ;
2383   struct list_head work_list ;
2384   struct task_struct *task ;
2385};
2386#line 64 "include/linux/kthread.h"
2387struct kthread_work {
2388   struct list_head node ;
2389   void (*func)(struct kthread_work *work ) ;
2390   wait_queue_head_t done ;
2391   atomic_t flushing ;
2392   int queue_seq ;
2393   int done_seq ;
2394};
2395#line 70 "include/linux/spi/spi.h"
2396struct spi_master;
2397#line 70 "include/linux/spi/spi.h"
2398struct spi_device {
2399   struct device dev ;
2400   struct spi_master *master ;
2401   u32 max_speed_hz ;
2402   u8 chip_select ;
2403   u8 mode ;
2404   u8 bits_per_word ;
2405   int irq ;
2406   void *controller_state ;
2407   void *controller_data ;
2408   char modalias[32] ;
2409};
2410#line 145
2411struct spi_message;
2412#line 145
2413struct spi_message;
2414#line 176 "include/linux/spi/spi.h"
2415struct spi_driver {
2416   struct spi_device_id  const  *id_table ;
2417   int (*probe)(struct spi_device *spi ) ;
2418   int (*remove)(struct spi_device *spi ) ;
2419   void (*shutdown)(struct spi_device *spi ) ;
2420   int (*suspend)(struct spi_device *spi , pm_message_t mesg ) ;
2421   int (*resume)(struct spi_device *spi ) ;
2422   struct device_driver driver ;
2423};
2424#line 272 "include/linux/spi/spi.h"
2425struct spi_master {
2426   struct device dev ;
2427   struct list_head list ;
2428   s16 bus_num ;
2429   u16 num_chipselect ;
2430   u16 dma_alignment ;
2431   u16 mode_bits ;
2432   u16 flags ;
2433   spinlock_t bus_lock_spinlock ;
2434   struct mutex bus_lock_mutex ;
2435   bool bus_lock_flag ;
2436   int (*setup)(struct spi_device *spi ) ;
2437   int (*transfer)(struct spi_device *spi , struct spi_message *mesg ) ;
2438   void (*cleanup)(struct spi_device *spi ) ;
2439   bool queued ;
2440   struct kthread_worker kworker ;
2441   struct task_struct *kworker_task ;
2442   struct kthread_work pump_messages ;
2443   spinlock_t queue_lock ;
2444   struct list_head queue ;
2445   struct spi_message *cur_msg ;
2446   bool busy ;
2447   bool running ;
2448   bool rt ;
2449   int (*prepare_transfer_hardware)(struct spi_master *master ) ;
2450   int (*transfer_one_message)(struct spi_master *master , struct spi_message *mesg ) ;
2451   int (*unprepare_transfer_hardware)(struct spi_master *master ) ;
2452};
2453#line 492 "include/linux/spi/spi.h"
2454struct spi_transfer {
2455   void const   *tx_buf ;
2456   void *rx_buf ;
2457   unsigned int len ;
2458   dma_addr_t tx_dma ;
2459   dma_addr_t rx_dma ;
2460   unsigned int cs_change : 1 ;
2461   u8 bits_per_word ;
2462   u16 delay_usecs ;
2463   u32 speed_hz ;
2464   struct list_head transfer_list ;
2465};
2466#line 541 "include/linux/spi/spi.h"
2467struct spi_message {
2468   struct list_head transfers ;
2469   struct spi_device *spi ;
2470   unsigned int is_dma_mapped : 1 ;
2471   void (*complete)(void *context ) ;
2472   void *context ;
2473   unsigned int actual_length ;
2474   int status ;
2475   struct list_head queue ;
2476   void *state ;
2477};
2478#line 6 "include/linux/eeprom_93xx46.h"
2479struct eeprom_93xx46_platform_data {
2480   unsigned char flags ;
2481   void (*prepare)(void * ) ;
2482   void (*finish)(void * ) ;
2483};
2484#line 30 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/drivers/misc/eeprom/eeprom_93xx46.c.common.c"
2485struct eeprom_93xx46_dev {
2486   struct spi_device *spi ;
2487   struct eeprom_93xx46_platform_data *pdata ;
2488   struct bin_attribute bin ;
2489   struct mutex lock ;
2490   int addrlen ;
2491};
2492#line 1 "<compiler builtins>"
2493long __builtin_expect(long val , long res ) ;
2494#line 49 "include/linux/dynamic_debug.h"
2495extern int ( /* format attribute */  __dynamic_dev_dbg)(struct _ddebug *descriptor ,
2496                                                        struct device  const  *dev ,
2497                                                        char const   *fmt  , ...) ;
2498#line 334 "include/linux/kernel.h"
2499extern int ( /* format attribute */  sscanf)(char const   * , char const   *  , ...) ;
2500#line 10 "include/asm-generic/delay.h"
2501extern void __const_udelay(unsigned long xloops ) ;
2502#line 24 "include/linux/list.h"
2503__inline static void INIT_LIST_HEAD(struct list_head *list )  __attribute__((__no_instrument_function__)) ;
2504#line 24 "include/linux/list.h"
2505__inline static void INIT_LIST_HEAD(struct list_head *list ) 
2506{ unsigned long __cil_tmp2 ;
2507  unsigned long __cil_tmp3 ;
2508
2509  {
2510#line 26
2511  *((struct list_head **)list) = list;
2512#line 27
2513  __cil_tmp2 = (unsigned long )list;
2514#line 27
2515  __cil_tmp3 = __cil_tmp2 + 8;
2516#line 27
2517  *((struct list_head **)__cil_tmp3) = list;
2518#line 28
2519  return;
2520}
2521}
2522#line 47
2523extern void __list_add(struct list_head *new , struct list_head *prev , struct list_head *next ) ;
2524#line 74
2525__inline static void list_add_tail(struct list_head *new , struct list_head *head )  __attribute__((__no_instrument_function__)) ;
2526#line 74 "include/linux/list.h"
2527__inline static void list_add_tail(struct list_head *new , struct list_head *head ) 
2528{ unsigned long __cil_tmp3 ;
2529  unsigned long __cil_tmp4 ;
2530  struct list_head *__cil_tmp5 ;
2531
2532  {
2533  {
2534#line 76
2535  __cil_tmp3 = (unsigned long )head;
2536#line 76
2537  __cil_tmp4 = __cil_tmp3 + 8;
2538#line 76
2539  __cil_tmp5 = *((struct list_head **)__cil_tmp4);
2540#line 76
2541  __list_add(new, __cil_tmp5, head);
2542  }
2543#line 77
2544  return;
2545}
2546}
2547#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/string_64.h"
2548extern void *memset(void *s , int c , size_t n ) ;
2549#line 140 "include/linux/sysfs.h"
2550extern int __attribute__((__warn_unused_result__))  sysfs_create_bin_file(struct kobject *kobj ,
2551                                                                          struct bin_attribute  const  *attr ) ;
2552#line 142
2553extern void sysfs_remove_bin_file(struct kobject *kobj , struct bin_attribute  const  *attr ) ;
2554#line 115 "include/linux/mutex.h"
2555extern void __mutex_init(struct mutex *lock , char const   *name , struct lock_class_key *key ) ;
2556#line 152
2557void mutex_lock(struct mutex *lock ) ;
2558#line 153
2559int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) ;
2560#line 154
2561int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) ;
2562#line 168
2563int mutex_trylock(struct mutex *lock ) ;
2564#line 169
2565void mutex_unlock(struct mutex *lock ) ;
2566#line 170
2567int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
2568#line 239 "include/linux/device.h"
2569extern void driver_unregister(struct device_driver *drv ) ;
2570#line 507
2571extern int device_create_file(struct device *device , struct device_attribute  const  *entry ) ;
2572#line 509
2573extern void device_remove_file(struct device *dev , struct device_attribute  const  *attr ) ;
2574#line 792
2575extern void *dev_get_drvdata(struct device  const  *dev ) ;
2576#line 793
2577extern int dev_set_drvdata(struct device *dev , void *data ) ;
2578#line 855
2579extern struct device *get_device(struct device *dev ) ;
2580#line 891
2581extern int ( /* format attribute */  dev_err)(struct device  const  *dev , char const   *fmt 
2582                                              , ...) ;
2583#line 897
2584extern int ( /* format attribute */  _dev_info)(struct device  const  *dev , char const   *fmt 
2585                                                , ...) ;
2586#line 26 "include/linux/export.h"
2587extern struct module __this_module ;
2588#line 67 "include/linux/module.h"
2589int init_module(void) ;
2590#line 68
2591void cleanup_module(void) ;
2592#line 161 "include/linux/slab.h"
2593extern void kfree(void const   * ) ;
2594#line 221 "include/linux/slub_def.h"
2595extern void *__kmalloc(size_t size , gfp_t flags ) ;
2596#line 268
2597__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
2598                                                                    gfp_t flags )  __attribute__((__no_instrument_function__)) ;
2599#line 268 "include/linux/slub_def.h"
2600__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
2601                                                                    gfp_t flags ) 
2602{ void *tmp___2 ;
2603
2604  {
2605  {
2606#line 283
2607  tmp___2 = __kmalloc(size, flags);
2608  }
2609#line 283
2610  return (tmp___2);
2611}
2612}
2613#line 349 "include/linux/slab.h"
2614__inline static void *kzalloc(size_t size , gfp_t flags )  __attribute__((__no_instrument_function__)) ;
2615#line 349 "include/linux/slab.h"
2616__inline static void *kzalloc(size_t size , gfp_t flags ) 
2617{ void *tmp ;
2618  unsigned int __cil_tmp4 ;
2619
2620  {
2621  {
2622#line 351
2623  __cil_tmp4 = flags | 32768U;
2624#line 351
2625  tmp = kmalloc(size, __cil_tmp4);
2626  }
2627#line 351
2628  return (tmp);
2629}
2630}
2631#line 111 "include/linux/spi/spi.h"
2632__inline static struct spi_device *spi_dev_get(struct spi_device *spi )  __attribute__((__no_instrument_function__)) ;
2633#line 111 "include/linux/spi/spi.h"
2634__inline static struct spi_device *spi_dev_get(struct spi_device *spi ) 
2635{ struct spi_device *tmp___8 ;
2636  struct device *tmp___9 ;
2637  struct device *__cil_tmp5 ;
2638  void *__cil_tmp6 ;
2639  void *__cil_tmp7 ;
2640
2641  {
2642#line 113
2643  if (spi) {
2644    {
2645#line 113
2646    __cil_tmp5 = (struct device *)spi;
2647#line 113
2648    tmp___9 = get_device(__cil_tmp5);
2649    }
2650#line 113
2651    if (tmp___9) {
2652#line 113
2653      tmp___8 = spi;
2654    } else {
2655#line 113
2656      __cil_tmp6 = (void *)0;
2657#line 113
2658      tmp___8 = (struct spi_device *)__cil_tmp6;
2659    }
2660  } else {
2661#line 113
2662    __cil_tmp7 = (void *)0;
2663#line 113
2664    tmp___8 = (struct spi_device *)__cil_tmp7;
2665  }
2666#line 113
2667  return (tmp___8);
2668}
2669}
2670#line 191
2671extern int spi_register_driver(struct spi_driver *sdrv ) ;
2672#line 198
2673__inline static void spi_unregister_driver(struct spi_driver *sdrv )  __attribute__((__no_instrument_function__)) ;
2674#line 198 "include/linux/spi/spi.h"
2675__inline static void spi_unregister_driver(struct spi_driver *sdrv ) 
2676{ unsigned long __cil_tmp2 ;
2677  unsigned long __cil_tmp3 ;
2678  struct device_driver *__cil_tmp4 ;
2679
2680  {
2681#line 200
2682  if (sdrv) {
2683    {
2684#line 201
2685    __cil_tmp2 = (unsigned long )sdrv;
2686#line 201
2687    __cil_tmp3 = __cil_tmp2 + 48;
2688#line 201
2689    __cil_tmp4 = (struct device_driver *)__cil_tmp3;
2690#line 201
2691    driver_unregister(__cil_tmp4);
2692    }
2693  } else {
2694
2695  }
2696#line 202
2697  return;
2698}
2699}
2700#line 573
2701__inline static void spi_message_init(struct spi_message *m )  __attribute__((__no_instrument_function__)) ;
2702#line 573 "include/linux/spi/spi.h"
2703__inline static void spi_message_init(struct spi_message *m ) 
2704{ void *__cil_tmp2 ;
2705  struct list_head *__cil_tmp3 ;
2706
2707  {
2708  {
2709#line 575
2710  __cil_tmp2 = (void *)m;
2711#line 575
2712  memset(__cil_tmp2, 0, 80UL);
2713#line 576
2714  __cil_tmp3 = (struct list_head *)m;
2715#line 576
2716  INIT_LIST_HEAD(__cil_tmp3);
2717  }
2718#line 577
2719  return;
2720}
2721}
2722#line 579
2723__inline static void spi_message_add_tail(struct spi_transfer *t , struct spi_message *m )  __attribute__((__no_instrument_function__)) ;
2724#line 579 "include/linux/spi/spi.h"
2725__inline static void spi_message_add_tail(struct spi_transfer *t , struct spi_message *m ) 
2726{ unsigned long __cil_tmp3 ;
2727  unsigned long __cil_tmp4 ;
2728  struct list_head *__cil_tmp5 ;
2729  struct list_head *__cil_tmp6 ;
2730
2731  {
2732  {
2733#line 582
2734  __cil_tmp3 = (unsigned long )t;
2735#line 582
2736  __cil_tmp4 = __cil_tmp3 + 48;
2737#line 582
2738  __cil_tmp5 = (struct list_head *)__cil_tmp4;
2739#line 582
2740  __cil_tmp6 = (struct list_head *)m;
2741#line 582
2742  list_add_tail(__cil_tmp5, __cil_tmp6);
2743  }
2744#line 583
2745  return;
2746}
2747}
2748#line 630
2749extern int spi_sync(struct spi_device *spi , struct spi_message *message ) ;
2750#line 70 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/drivers/misc/eeprom/eeprom_93xx46.c.common.c"
2751static ssize_t eeprom_93xx46_bin_read(struct file *filp , struct kobject *kobj , struct bin_attribute *bin_attr ,
2752                                      char *buf , loff_t off , size_t count ) ;
2753#line 70 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/drivers/misc/eeprom/eeprom_93xx46.c.common.c"
2754static struct _ddebug  __attribute__((__aligned__(8))) descriptor  __attribute__((__used__,
2755__section__("__verbose")))  =    {"eeprom_93xx46", "eeprom_93xx46_bin_read", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/drivers/misc/eeprom/eeprom_93xx46.c.common.c",
2756    "read cmd 0x%x, %d Hz\n", 71U, 0U};
2757#line 38 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/drivers/misc/eeprom/eeprom_93xx46.c.common.c"
2758static ssize_t eeprom_93xx46_bin_read(struct file *filp , struct kobject *kobj , struct bin_attribute *bin_attr ,
2759                                      char *buf , loff_t off , size_t count ) 
2760{ struct eeprom_93xx46_dev *edev ;
2761  struct device *dev ;
2762  struct spi_message m ;
2763  struct spi_transfer t[2] ;
2764  int bits ;
2765  int ret ;
2766  u16 cmd_addr ;
2767  struct kobject  const  *__mptr ;
2768  void *tmp___7 ;
2769  long tmp___8 ;
2770  long tmp___9 ;
2771  long tmp___10 ;
2772  size_t tmp___11 ;
2773  struct device *__cil_tmp20 ;
2774  unsigned long __cil_tmp21 ;
2775  unsigned long __cil_tmp22 ;
2776  struct kobject *__cil_tmp23 ;
2777  unsigned int __cil_tmp24 ;
2778  char *__cil_tmp25 ;
2779  char *__cil_tmp26 ;
2780  struct device  const  *__cil_tmp27 ;
2781  unsigned long __cil_tmp28 ;
2782  unsigned long __cil_tmp29 ;
2783  unsigned long __cil_tmp30 ;
2784  size_t __cil_tmp31 ;
2785  loff_t __cil_tmp32 ;
2786  int __cil_tmp33 ;
2787  int __cil_tmp34 ;
2788  int __cil_tmp35 ;
2789  long __cil_tmp36 ;
2790  unsigned long __cil_tmp37 ;
2791  unsigned long __cil_tmp38 ;
2792  unsigned long __cil_tmp39 ;
2793  size_t __cil_tmp40 ;
2794  loff_t __cil_tmp41 ;
2795  loff_t __cil_tmp42 ;
2796  loff_t __cil_tmp43 ;
2797  unsigned long __cil_tmp44 ;
2798  unsigned long __cil_tmp45 ;
2799  unsigned long __cil_tmp46 ;
2800  size_t __cil_tmp47 ;
2801  loff_t __cil_tmp48 ;
2802  loff_t __cil_tmp49 ;
2803  int __cil_tmp50 ;
2804  int __cil_tmp51 ;
2805  int __cil_tmp52 ;
2806  long __cil_tmp53 ;
2807  u16 *__cil_tmp54 ;
2808  unsigned long __cil_tmp55 ;
2809  unsigned long __cil_tmp56 ;
2810  int __cil_tmp57 ;
2811  int __cil_tmp58 ;
2812  unsigned long __cil_tmp59 ;
2813  unsigned long __cil_tmp60 ;
2814  int __cil_tmp61 ;
2815  u16 *__cil_tmp62 ;
2816  long long __cil_tmp63 ;
2817  u16 *__cil_tmp64 ;
2818  u16 __cil_tmp65 ;
2819  long long __cil_tmp66 ;
2820  long long __cil_tmp67 ;
2821  u16 *__cil_tmp68 ;
2822  long long __cil_tmp69 ;
2823  u16 *__cil_tmp70 ;
2824  u16 __cil_tmp71 ;
2825  long long __cil_tmp72 ;
2826  long long __cil_tmp73 ;
2827  struct _ddebug  __attribute__((__aligned__(8))) *__cil_tmp74 ;
2828  unsigned int __cil_tmp75 ;
2829  unsigned int __cil_tmp76 ;
2830  int __cil_tmp77 ;
2831  int __cil_tmp78 ;
2832  long __cil_tmp79 ;
2833  struct spi_device *__cil_tmp80 ;
2834  struct device *__cil_tmp81 ;
2835  struct device  const  *__cil_tmp82 ;
2836  u16 *__cil_tmp83 ;
2837  u16 __cil_tmp84 ;
2838  int __cil_tmp85 ;
2839  struct spi_device *__cil_tmp86 ;
2840  unsigned long __cil_tmp87 ;
2841  unsigned long __cil_tmp88 ;
2842  u32 __cil_tmp89 ;
2843  unsigned long __cil_tmp90 ;
2844  unsigned long __cil_tmp91 ;
2845  struct spi_transfer *__cil_tmp92 ;
2846  void *__cil_tmp93 ;
2847  unsigned long __cil_tmp94 ;
2848  unsigned long __cil_tmp95 ;
2849  char *__cil_tmp96 ;
2850  unsigned long __cil_tmp97 ;
2851  unsigned long __cil_tmp98 ;
2852  unsigned long __cil_tmp99 ;
2853  unsigned long __cil_tmp100 ;
2854  unsigned long __cil_tmp101 ;
2855  unsigned long __cil_tmp102 ;
2856  unsigned long __cil_tmp103 ;
2857  unsigned long __cil_tmp104 ;
2858  struct spi_transfer *__cil_tmp105 ;
2859  unsigned long __cil_tmp106 ;
2860  unsigned long __cil_tmp107 ;
2861  unsigned long __cil_tmp108 ;
2862  unsigned long __cil_tmp109 ;
2863  unsigned long __cil_tmp110 ;
2864  unsigned long __cil_tmp111 ;
2865  unsigned long __cil_tmp112 ;
2866  unsigned long __cil_tmp113 ;
2867  unsigned long __cil_tmp114 ;
2868  unsigned long __cil_tmp115 ;
2869  unsigned long __cil_tmp116 ;
2870  struct spi_transfer *__cil_tmp117 ;
2871  unsigned long __cil_tmp118 ;
2872  unsigned long __cil_tmp119 ;
2873  struct mutex *__cil_tmp120 ;
2874  unsigned long __cil_tmp121 ;
2875  unsigned long __cil_tmp122 ;
2876  struct eeprom_93xx46_platform_data *__cil_tmp123 ;
2877  unsigned long __cil_tmp124 ;
2878  unsigned long __cil_tmp125 ;
2879  unsigned long __cil_tmp126 ;
2880  unsigned long __cil_tmp127 ;
2881  struct eeprom_93xx46_platform_data *__cil_tmp128 ;
2882  unsigned long __cil_tmp129 ;
2883  unsigned long __cil_tmp130 ;
2884  void (*__cil_tmp131)(void * ) ;
2885  void *__cil_tmp132 ;
2886  struct spi_device *__cil_tmp133 ;
2887  struct spi_device *__cil_tmp134 ;
2888  struct device *__cil_tmp135 ;
2889  struct device  const  *__cil_tmp136 ;
2890  int __cil_tmp137 ;
2891  unsigned long __cil_tmp138 ;
2892  unsigned long __cil_tmp139 ;
2893  struct eeprom_93xx46_platform_data *__cil_tmp140 ;
2894  unsigned long __cil_tmp141 ;
2895  unsigned long __cil_tmp142 ;
2896  unsigned long __cil_tmp143 ;
2897  unsigned long __cil_tmp144 ;
2898  struct eeprom_93xx46_platform_data *__cil_tmp145 ;
2899  unsigned long __cil_tmp146 ;
2900  unsigned long __cil_tmp147 ;
2901  void (*__cil_tmp148)(void * ) ;
2902  void *__cil_tmp149 ;
2903  unsigned long __cil_tmp150 ;
2904  unsigned long __cil_tmp151 ;
2905  struct mutex *__cil_tmp152 ;
2906
2907  {
2908  {
2909#line 50
2910  __mptr = (struct kobject  const  *)kobj;
2911#line 50
2912  __cil_tmp20 = (struct device *)0;
2913#line 50
2914  __cil_tmp21 = (unsigned long )__cil_tmp20;
2915#line 50
2916  __cil_tmp22 = __cil_tmp21 + 16;
2917#line 50
2918  __cil_tmp23 = (struct kobject *)__cil_tmp22;
2919#line 50
2920  __cil_tmp24 = (unsigned int )__cil_tmp23;
2921#line 50
2922  __cil_tmp25 = (char *)__mptr;
2923#line 50
2924  __cil_tmp26 = __cil_tmp25 - __cil_tmp24;
2925#line 50
2926  dev = (struct device *)__cil_tmp26;
2927#line 51
2928  __cil_tmp27 = (struct device  const  *)dev;
2929#line 51
2930  tmp___7 = dev_get_drvdata(__cil_tmp27);
2931#line 51
2932  edev = (struct eeprom_93xx46_dev *)tmp___7;
2933#line 53
2934  __cil_tmp28 = 16 + 16;
2935#line 53
2936  __cil_tmp29 = (unsigned long )edev;
2937#line 53
2938  __cil_tmp30 = __cil_tmp29 + __cil_tmp28;
2939#line 53
2940  __cil_tmp31 = *((size_t *)__cil_tmp30);
2941#line 53
2942  __cil_tmp32 = (loff_t )__cil_tmp31;
2943#line 53
2944  __cil_tmp33 = off >= __cil_tmp32;
2945#line 53
2946  __cil_tmp34 = ! __cil_tmp33;
2947#line 53
2948  __cil_tmp35 = ! __cil_tmp34;
2949#line 53
2950  __cil_tmp36 = (long )__cil_tmp35;
2951#line 53
2952  tmp___8 = __builtin_expect(__cil_tmp36, 0L);
2953  }
2954#line 53
2955  if (tmp___8) {
2956#line 54
2957    return ((ssize_t )0);
2958  } else {
2959
2960  }
2961  {
2962#line 55
2963  __cil_tmp37 = 16 + 16;
2964#line 55
2965  __cil_tmp38 = (unsigned long )edev;
2966#line 55
2967  __cil_tmp39 = __cil_tmp38 + __cil_tmp37;
2968#line 55
2969  __cil_tmp40 = *((size_t *)__cil_tmp39);
2970#line 55
2971  __cil_tmp41 = (loff_t )__cil_tmp40;
2972#line 55
2973  __cil_tmp42 = (loff_t )count;
2974#line 55
2975  __cil_tmp43 = off + __cil_tmp42;
2976#line 55
2977  if (__cil_tmp43 > __cil_tmp41) {
2978#line 56
2979    __cil_tmp44 = 16 + 16;
2980#line 56
2981    __cil_tmp45 = (unsigned long )edev;
2982#line 56
2983    __cil_tmp46 = __cil_tmp45 + __cil_tmp44;
2984#line 56
2985    __cil_tmp47 = *((size_t *)__cil_tmp46);
2986#line 56
2987    __cil_tmp48 = (loff_t )__cil_tmp47;
2988#line 56
2989    __cil_tmp49 = __cil_tmp48 - off;
2990#line 56
2991    count = (size_t )__cil_tmp49;
2992  } else {
2993
2994  }
2995  }
2996  {
2997#line 57
2998  __cil_tmp50 = ! count;
2999#line 57
3000  __cil_tmp51 = ! __cil_tmp50;
3001#line 57
3002  __cil_tmp52 = ! __cil_tmp51;
3003#line 57
3004  __cil_tmp53 = (long )__cil_tmp52;
3005#line 57
3006  tmp___9 = __builtin_expect(__cil_tmp53, 0L);
3007  }
3008#line 57
3009  if (tmp___9) {
3010#line 58
3011    return ((ssize_t )count);
3012  } else {
3013
3014  }
3015#line 60
3016  __cil_tmp54 = & cmd_addr;
3017#line 60
3018  __cil_tmp55 = (unsigned long )edev;
3019#line 60
3020  __cil_tmp56 = __cil_tmp55 + 144;
3021#line 60
3022  __cil_tmp57 = *((int *)__cil_tmp56);
3023#line 60
3024  __cil_tmp58 = 6 << __cil_tmp57;
3025#line 60
3026  *__cil_tmp54 = (u16 )__cil_tmp58;
3027  {
3028#line 62
3029  __cil_tmp59 = (unsigned long )edev;
3030#line 62
3031  __cil_tmp60 = __cil_tmp59 + 144;
3032#line 62
3033  __cil_tmp61 = *((int *)__cil_tmp60);
3034#line 62
3035  if (__cil_tmp61 == 7) {
3036#line 63
3037    __cil_tmp62 = & cmd_addr;
3038#line 63
3039    __cil_tmp63 = off & 127LL;
3040#line 63
3041    __cil_tmp64 = & cmd_addr;
3042#line 63
3043    __cil_tmp65 = *__cil_tmp64;
3044#line 63
3045    __cil_tmp66 = (long long )__cil_tmp65;
3046#line 63
3047    __cil_tmp67 = __cil_tmp66 | __cil_tmp63;
3048#line 63
3049    *__cil_tmp62 = (u16 )__cil_tmp67;
3050#line 64
3051    bits = 10;
3052  } else {
3053#line 66
3054    __cil_tmp68 = & cmd_addr;
3055#line 66
3056    __cil_tmp69 = off & 63LL;
3057#line 66
3058    __cil_tmp70 = & cmd_addr;
3059#line 66
3060    __cil_tmp71 = *__cil_tmp70;
3061#line 66
3062    __cil_tmp72 = (long long )__cil_tmp71;
3063#line 66
3064    __cil_tmp73 = __cil_tmp72 | __cil_tmp69;
3065#line 66
3066    *__cil_tmp68 = (u16 )__cil_tmp73;
3067#line 67
3068    bits = 9;
3069  }
3070  }
3071  {
3072#line 70
3073  while (1) {
3074    while_continue: /* CIL Label */ ;
3075    {
3076#line 70
3077    while (1) {
3078      while_continue___0: /* CIL Label */ ;
3079      {
3080#line 70
3081      __cil_tmp74 = & descriptor;
3082#line 70
3083      __cil_tmp75 = __cil_tmp74->flags;
3084#line 70
3085      __cil_tmp76 = __cil_tmp75 & 1U;
3086#line 70
3087      __cil_tmp77 = ! __cil_tmp76;
3088#line 70
3089      __cil_tmp78 = ! __cil_tmp77;
3090#line 70
3091      __cil_tmp79 = (long )__cil_tmp78;
3092#line 70
3093      tmp___10 = __builtin_expect(__cil_tmp79, 0L);
3094      }
3095#line 70
3096      if (tmp___10) {
3097        {
3098#line 70
3099        __cil_tmp80 = *((struct spi_device **)edev);
3100#line 70
3101        __cil_tmp81 = (struct device *)__cil_tmp80;
3102#line 70
3103        __cil_tmp82 = (struct device  const  *)__cil_tmp81;
3104#line 70
3105        __cil_tmp83 = & cmd_addr;
3106#line 70
3107        __cil_tmp84 = *__cil_tmp83;
3108#line 70
3109        __cil_tmp85 = (int )__cil_tmp84;
3110#line 70
3111        __cil_tmp86 = *((struct spi_device **)edev);
3112#line 70
3113        __cil_tmp87 = (unsigned long )__cil_tmp86;
3114#line 70
3115        __cil_tmp88 = __cil_tmp87 + 776;
3116#line 70
3117        __cil_tmp89 = *((u32 *)__cil_tmp88);
3118#line 70
3119        __dynamic_dev_dbg(& descriptor, __cil_tmp82, "read cmd 0x%x, %d Hz\n", __cil_tmp85,
3120                          __cil_tmp89);
3121        }
3122      } else {
3123
3124      }
3125#line 70
3126      goto while_break___0;
3127    }
3128    while_break___0: /* CIL Label */ ;
3129    }
3130#line 70
3131    goto while_break;
3132  }
3133  while_break: /* CIL Label */ ;
3134  }
3135  {
3136#line 73
3137  spi_message_init(& m);
3138#line 74
3139  __cil_tmp90 = 0 * 64UL;
3140#line 74
3141  __cil_tmp91 = (unsigned long )(t) + __cil_tmp90;
3142#line 74
3143  __cil_tmp92 = (struct spi_transfer *)__cil_tmp91;
3144#line 74
3145  __cil_tmp93 = (void *)__cil_tmp92;
3146#line 74
3147  memset(__cil_tmp93, 0, 128UL);
3148#line 76
3149  __cil_tmp94 = 0 * 64UL;
3150#line 76
3151  __cil_tmp95 = (unsigned long )(t) + __cil_tmp94;
3152#line 76
3153  __cil_tmp96 = (char *)(& cmd_addr);
3154#line 76
3155  *((void const   **)__cil_tmp95) = (void const   *)__cil_tmp96;
3156#line 77
3157  __cil_tmp97 = 0 * 64UL;
3158#line 77
3159  __cil_tmp98 = __cil_tmp97 + 16;
3160#line 77
3161  __cil_tmp99 = (unsigned long )(t) + __cil_tmp98;
3162#line 77
3163  *((unsigned int *)__cil_tmp99) = 2U;
3164#line 78
3165  __cil_tmp100 = 0 * 64UL;
3166#line 78
3167  __cil_tmp101 = __cil_tmp100 + 41;
3168#line 78
3169  __cil_tmp102 = (unsigned long )(t) + __cil_tmp101;
3170#line 78
3171  *((u8 *)__cil_tmp102) = (u8 )bits;
3172#line 79
3173  __cil_tmp103 = 0 * 64UL;
3174#line 79
3175  __cil_tmp104 = (unsigned long )(t) + __cil_tmp103;
3176#line 79
3177  __cil_tmp105 = (struct spi_transfer *)__cil_tmp104;
3178#line 79
3179  spi_message_add_tail(__cil_tmp105, & m);
3180#line 81
3181  __cil_tmp106 = 1 * 64UL;
3182#line 81
3183  __cil_tmp107 = __cil_tmp106 + 8;
3184#line 81
3185  __cil_tmp108 = (unsigned long )(t) + __cil_tmp107;
3186#line 81
3187  *((void **)__cil_tmp108) = (void *)buf;
3188#line 82
3189  __cil_tmp109 = 1 * 64UL;
3190#line 82
3191  __cil_tmp110 = __cil_tmp109 + 16;
3192#line 82
3193  __cil_tmp111 = (unsigned long )(t) + __cil_tmp110;
3194#line 82
3195  *((unsigned int *)__cil_tmp111) = (unsigned int )count;
3196#line 83
3197  __cil_tmp112 = 1 * 64UL;
3198#line 83
3199  __cil_tmp113 = __cil_tmp112 + 41;
3200#line 83
3201  __cil_tmp114 = (unsigned long )(t) + __cil_tmp113;
3202#line 83
3203  *((u8 *)__cil_tmp114) = (u8 )8;
3204#line 84
3205  __cil_tmp115 = 1 * 64UL;
3206#line 84
3207  __cil_tmp116 = (unsigned long )(t) + __cil_tmp115;
3208#line 84
3209  __cil_tmp117 = (struct spi_transfer *)__cil_tmp116;
3210#line 84
3211  spi_message_add_tail(__cil_tmp117, & m);
3212#line 86
3213  __cil_tmp118 = (unsigned long )edev;
3214#line 86
3215  __cil_tmp119 = __cil_tmp118 + 72;
3216#line 86
3217  __cil_tmp120 = (struct mutex *)__cil_tmp119;
3218#line 86
3219  mutex_lock(__cil_tmp120);
3220  }
3221  {
3222#line 88
3223  __cil_tmp121 = (unsigned long )edev;
3224#line 88
3225  __cil_tmp122 = __cil_tmp121 + 8;
3226#line 88
3227  __cil_tmp123 = *((struct eeprom_93xx46_platform_data **)__cil_tmp122);
3228#line 88
3229  __cil_tmp124 = (unsigned long )__cil_tmp123;
3230#line 88
3231  __cil_tmp125 = __cil_tmp124 + 8;
3232#line 88
3233  if (*((void (**)(void * ))__cil_tmp125)) {
3234    {
3235#line 89
3236    __cil_tmp126 = (unsigned long )edev;
3237#line 89
3238    __cil_tmp127 = __cil_tmp126 + 8;
3239#line 89
3240    __cil_tmp128 = *((struct eeprom_93xx46_platform_data **)__cil_tmp127);
3241#line 89
3242    __cil_tmp129 = (unsigned long )__cil_tmp128;
3243#line 89
3244    __cil_tmp130 = __cil_tmp129 + 8;
3245#line 89
3246    __cil_tmp131 = *((void (**)(void * ))__cil_tmp130);
3247#line 89
3248    __cil_tmp132 = (void *)edev;
3249#line 89
3250    (*__cil_tmp131)(__cil_tmp132);
3251    }
3252  } else {
3253
3254  }
3255  }
3256  {
3257#line 91
3258  __cil_tmp133 = *((struct spi_device **)edev);
3259#line 91
3260  ret = spi_sync(__cil_tmp133, & m);
3261#line 93
3262  __const_udelay(1250UL);
3263  }
3264#line 94
3265  if (ret) {
3266    {
3267#line 95
3268    __cil_tmp134 = *((struct spi_device **)edev);
3269#line 95
3270    __cil_tmp135 = (struct device *)__cil_tmp134;
3271#line 95
3272    __cil_tmp136 = (struct device  const  *)__cil_tmp135;
3273#line 95
3274    __cil_tmp137 = (int )off;
3275#line 95
3276    dev_err(__cil_tmp136, "read %zu bytes at %d: err. %d\n", count, __cil_tmp137,
3277            ret);
3278    }
3279  } else {
3280
3281  }
3282  {
3283#line 99
3284  __cil_tmp138 = (unsigned long )edev;
3285#line 99
3286  __cil_tmp139 = __cil_tmp138 + 8;
3287#line 99
3288  __cil_tmp140 = *((struct eeprom_93xx46_platform_data **)__cil_tmp139);
3289#line 99
3290  __cil_tmp141 = (unsigned long )__cil_tmp140;
3291#line 99
3292  __cil_tmp142 = __cil_tmp141 + 16;
3293#line 99
3294  if (*((void (**)(void * ))__cil_tmp142)) {
3295    {
3296#line 100
3297    __cil_tmp143 = (unsigned long )edev;
3298#line 100
3299    __cil_tmp144 = __cil_tmp143 + 8;
3300#line 100
3301    __cil_tmp145 = *((struct eeprom_93xx46_platform_data **)__cil_tmp144);
3302#line 100
3303    __cil_tmp146 = (unsigned long )__cil_tmp145;
3304#line 100
3305    __cil_tmp147 = __cil_tmp146 + 16;
3306#line 100
3307    __cil_tmp148 = *((void (**)(void * ))__cil_tmp147);
3308#line 100
3309    __cil_tmp149 = (void *)edev;
3310#line 100
3311    (*__cil_tmp148)(__cil_tmp149);
3312    }
3313  } else {
3314
3315  }
3316  }
3317  {
3318#line 102
3319  __cil_tmp150 = (unsigned long )edev;
3320#line 102
3321  __cil_tmp151 = __cil_tmp150 + 72;
3322#line 102
3323  __cil_tmp152 = (struct mutex *)__cil_tmp151;
3324#line 102
3325  mutex_unlock(__cil_tmp152);
3326#line 103
3327  tmp___11 = (size_t )ret;
3328  }
3329#line 103
3330  if (tmp___11) {
3331
3332  } else {
3333#line 103
3334    tmp___11 = count;
3335  }
3336#line 103
3337  return ((ssize_t )tmp___11);
3338}
3339}
3340#line 122
3341static int eeprom_93xx46_ew(struct eeprom_93xx46_dev *edev , int is_on ) ;
3342#line 122 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/drivers/misc/eeprom/eeprom_93xx46.c.common.c"
3343static struct _ddebug  __attribute__((__aligned__(8))) descriptor___0  __attribute__((__used__,
3344__section__("__verbose")))  =    {"eeprom_93xx46", "eeprom_93xx46_ew", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/drivers/misc/eeprom/eeprom_93xx46.c.common.c",
3345    "ew cmd 0x%04x\n", 122U, 0U};
3346#line 106 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/drivers/misc/eeprom/eeprom_93xx46.c.common.c"
3347static int eeprom_93xx46_ew(struct eeprom_93xx46_dev *edev , int is_on ) 
3348{ struct spi_message m ;
3349  struct spi_transfer t ;
3350  int bits ;
3351  int ret ;
3352  u16 cmd_addr ;
3353  int tmp___7 ;
3354  int tmp___8 ;
3355  long tmp___9 ;
3356  char const   *tmp___10 ;
3357  u16 *__cil_tmp12 ;
3358  unsigned long __cil_tmp13 ;
3359  unsigned long __cil_tmp14 ;
3360  int __cil_tmp15 ;
3361  int __cil_tmp16 ;
3362  unsigned long __cil_tmp17 ;
3363  unsigned long __cil_tmp18 ;
3364  int __cil_tmp19 ;
3365  u16 *__cil_tmp20 ;
3366  int __cil_tmp21 ;
3367  u16 *__cil_tmp22 ;
3368  u16 __cil_tmp23 ;
3369  int __cil_tmp24 ;
3370  int __cil_tmp25 ;
3371  u16 *__cil_tmp26 ;
3372  u16 *__cil_tmp27 ;
3373  u16 __cil_tmp28 ;
3374  int __cil_tmp29 ;
3375  int __cil_tmp30 ;
3376  struct _ddebug  __attribute__((__aligned__(8))) *__cil_tmp31 ;
3377  unsigned int __cil_tmp32 ;
3378  unsigned int __cil_tmp33 ;
3379  int __cil_tmp34 ;
3380  int __cil_tmp35 ;
3381  long __cil_tmp36 ;
3382  struct spi_device *__cil_tmp37 ;
3383  struct device *__cil_tmp38 ;
3384  struct device  const  *__cil_tmp39 ;
3385  u16 *__cil_tmp40 ;
3386  u16 __cil_tmp41 ;
3387  int __cil_tmp42 ;
3388  void *__cil_tmp43 ;
3389  struct spi_transfer *__cil_tmp44 ;
3390  unsigned long __cil_tmp45 ;
3391  unsigned long __cil_tmp46 ;
3392  unsigned long __cil_tmp47 ;
3393  unsigned long __cil_tmp48 ;
3394  struct mutex *__cil_tmp49 ;
3395  unsigned long __cil_tmp50 ;
3396  unsigned long __cil_tmp51 ;
3397  struct eeprom_93xx46_platform_data *__cil_tmp52 ;
3398  unsigned long __cil_tmp53 ;
3399  unsigned long __cil_tmp54 ;
3400  unsigned long __cil_tmp55 ;
3401  unsigned long __cil_tmp56 ;
3402  struct eeprom_93xx46_platform_data *__cil_tmp57 ;
3403  unsigned long __cil_tmp58 ;
3404  unsigned long __cil_tmp59 ;
3405  void (*__cil_tmp60)(void * ) ;
3406  void *__cil_tmp61 ;
3407  struct spi_device *__cil_tmp62 ;
3408  struct spi_device *__cil_tmp63 ;
3409  struct device *__cil_tmp64 ;
3410  struct device  const  *__cil_tmp65 ;
3411  unsigned long __cil_tmp66 ;
3412  unsigned long __cil_tmp67 ;
3413  struct eeprom_93xx46_platform_data *__cil_tmp68 ;
3414  unsigned long __cil_tmp69 ;
3415  unsigned long __cil_tmp70 ;
3416  unsigned long __cil_tmp71 ;
3417  unsigned long __cil_tmp72 ;
3418  struct eeprom_93xx46_platform_data *__cil_tmp73 ;
3419  unsigned long __cil_tmp74 ;
3420  unsigned long __cil_tmp75 ;
3421  void (*__cil_tmp76)(void * ) ;
3422  void *__cil_tmp77 ;
3423  unsigned long __cil_tmp78 ;
3424  unsigned long __cil_tmp79 ;
3425  struct mutex *__cil_tmp80 ;
3426
3427  {
3428#line 113
3429  __cil_tmp12 = & cmd_addr;
3430#line 113
3431  __cil_tmp13 = (unsigned long )edev;
3432#line 113
3433  __cil_tmp14 = __cil_tmp13 + 144;
3434#line 113
3435  __cil_tmp15 = *((int *)__cil_tmp14);
3436#line 113
3437  __cil_tmp16 = 4 << __cil_tmp15;
3438#line 113
3439  *__cil_tmp12 = (u16 )__cil_tmp16;
3440  {
3441#line 114
3442  __cil_tmp17 = (unsigned long )edev;
3443#line 114
3444  __cil_tmp18 = __cil_tmp17 + 144;
3445#line 114
3446  __cil_tmp19 = *((int *)__cil_tmp18);
3447#line 114
3448  if (__cil_tmp19 == 7) {
3449#line 115
3450    if (is_on) {
3451#line 115
3452      tmp___7 = 48;
3453    } else {
3454#line 115
3455      tmp___7 = 0;
3456    }
3457#line 115
3458    __cil_tmp20 = & cmd_addr;
3459#line 115
3460    __cil_tmp21 = tmp___7 << 1;
3461#line 115
3462    __cil_tmp22 = & cmd_addr;
3463#line 115
3464    __cil_tmp23 = *__cil_tmp22;
3465#line 115
3466    __cil_tmp24 = (int )__cil_tmp23;
3467#line 115
3468    __cil_tmp25 = __cil_tmp24 | __cil_tmp21;
3469#line 115
3470    *__cil_tmp20 = (u16 )__cil_tmp25;
3471#line 116
3472    bits = 10;
3473  } else {
3474#line 118
3475    if (is_on) {
3476#line 118
3477      tmp___8 = 48;
3478    } else {
3479#line 118
3480      tmp___8 = 0;
3481    }
3482#line 118
3483    __cil_tmp26 = & cmd_addr;
3484#line 118
3485    __cil_tmp27 = & cmd_addr;
3486#line 118
3487    __cil_tmp28 = *__cil_tmp27;
3488#line 118
3489    __cil_tmp29 = (int )__cil_tmp28;
3490#line 118
3491    __cil_tmp30 = __cil_tmp29 | tmp___8;
3492#line 118
3493    *__cil_tmp26 = (u16 )__cil_tmp30;
3494#line 119
3495    bits = 9;
3496  }
3497  }
3498  {
3499#line 122
3500  while (1) {
3501    while_continue: /* CIL Label */ ;
3502    {
3503#line 122
3504    while (1) {
3505      while_continue___0: /* CIL Label */ ;
3506      {
3507#line 122
3508      __cil_tmp31 = & descriptor___0;
3509#line 122
3510      __cil_tmp32 = __cil_tmp31->flags;
3511#line 122
3512      __cil_tmp33 = __cil_tmp32 & 1U;
3513#line 122
3514      __cil_tmp34 = ! __cil_tmp33;
3515#line 122
3516      __cil_tmp35 = ! __cil_tmp34;
3517#line 122
3518      __cil_tmp36 = (long )__cil_tmp35;
3519#line 122
3520      tmp___9 = __builtin_expect(__cil_tmp36, 0L);
3521      }
3522#line 122
3523      if (tmp___9) {
3524        {
3525#line 122
3526        __cil_tmp37 = *((struct spi_device **)edev);
3527#line 122
3528        __cil_tmp38 = (struct device *)__cil_tmp37;
3529#line 122
3530        __cil_tmp39 = (struct device  const  *)__cil_tmp38;
3531#line 122
3532        __cil_tmp40 = & cmd_addr;
3533#line 122
3534        __cil_tmp41 = *__cil_tmp40;
3535#line 122
3536        __cil_tmp42 = (int )__cil_tmp41;
3537#line 122
3538        __dynamic_dev_dbg(& descriptor___0, __cil_tmp39, "ew cmd 0x%04x\n", __cil_tmp42);
3539        }
3540      } else {
3541
3542      }
3543#line 122
3544      goto while_break___0;
3545    }
3546    while_break___0: /* CIL Label */ ;
3547    }
3548#line 122
3549    goto while_break;
3550  }
3551  while_break: /* CIL Label */ ;
3552  }
3553  {
3554#line 124
3555  spi_message_init(& m);
3556#line 125
3557  __cil_tmp43 = (void *)(& t);
3558#line 125
3559  memset(__cil_tmp43, 0, 64UL);
3560#line 127
3561  __cil_tmp44 = & t;
3562#line 127
3563  *((void const   **)__cil_tmp44) = (void const   *)(& cmd_addr);
3564#line 128
3565  __cil_tmp45 = (unsigned long )(& t) + 16;
3566#line 128
3567  *((unsigned int *)__cil_tmp45) = 2U;
3568#line 129
3569  __cil_tmp46 = (unsigned long )(& t) + 41;
3570#line 129
3571  *((u8 *)__cil_tmp46) = (u8 )bits;
3572#line 130
3573  spi_message_add_tail(& t, & m);
3574#line 132
3575  __cil_tmp47 = (unsigned long )edev;
3576#line 132
3577  __cil_tmp48 = __cil_tmp47 + 72;
3578#line 132
3579  __cil_tmp49 = (struct mutex *)__cil_tmp48;
3580#line 132
3581  mutex_lock(__cil_tmp49);
3582  }
3583  {
3584#line 134
3585  __cil_tmp50 = (unsigned long )edev;
3586#line 134
3587  __cil_tmp51 = __cil_tmp50 + 8;
3588#line 134
3589  __cil_tmp52 = *((struct eeprom_93xx46_platform_data **)__cil_tmp51);
3590#line 134
3591  __cil_tmp53 = (unsigned long )__cil_tmp52;
3592#line 134
3593  __cil_tmp54 = __cil_tmp53 + 8;
3594#line 134
3595  if (*((void (**)(void * ))__cil_tmp54)) {
3596    {
3597#line 135
3598    __cil_tmp55 = (unsigned long )edev;
3599#line 135
3600    __cil_tmp56 = __cil_tmp55 + 8;
3601#line 135
3602    __cil_tmp57 = *((struct eeprom_93xx46_platform_data **)__cil_tmp56);
3603#line 135
3604    __cil_tmp58 = (unsigned long )__cil_tmp57;
3605#line 135
3606    __cil_tmp59 = __cil_tmp58 + 8;
3607#line 135
3608    __cil_tmp60 = *((void (**)(void * ))__cil_tmp59);
3609#line 135
3610    __cil_tmp61 = (void *)edev;
3611#line 135
3612    (*__cil_tmp60)(__cil_tmp61);
3613    }
3614  } else {
3615
3616  }
3617  }
3618  {
3619#line 137
3620  __cil_tmp62 = *((struct spi_device **)edev);
3621#line 137
3622  ret = spi_sync(__cil_tmp62, & m);
3623#line 139
3624  __const_udelay(1250UL);
3625  }
3626#line 140
3627  if (ret) {
3628#line 141
3629    if (is_on) {
3630#line 141
3631      tmp___10 = "en";
3632    } else {
3633#line 141
3634      tmp___10 = "dis";
3635    }
3636    {
3637#line 141
3638    __cil_tmp63 = *((struct spi_device **)edev);
3639#line 141
3640    __cil_tmp64 = (struct device *)__cil_tmp63;
3641#line 141
3642    __cil_tmp65 = (struct device  const  *)__cil_tmp64;
3643#line 141
3644    dev_err(__cil_tmp65, "erase/write %sable error %d\n", tmp___10, ret);
3645    }
3646  } else {
3647
3648  }
3649  {
3650#line 144
3651  __cil_tmp66 = (unsigned long )edev;
3652#line 144
3653  __cil_tmp67 = __cil_tmp66 + 8;
3654#line 144
3655  __cil_tmp68 = *((struct eeprom_93xx46_platform_data **)__cil_tmp67);
3656#line 144
3657  __cil_tmp69 = (unsigned long )__cil_tmp68;
3658#line 144
3659  __cil_tmp70 = __cil_tmp69 + 16;
3660#line 144
3661  if (*((void (**)(void * ))__cil_tmp70)) {
3662    {
3663#line 145
3664    __cil_tmp71 = (unsigned long )edev;
3665#line 145
3666    __cil_tmp72 = __cil_tmp71 + 8;
3667#line 145
3668    __cil_tmp73 = *((struct eeprom_93xx46_platform_data **)__cil_tmp72);
3669#line 145
3670    __cil_tmp74 = (unsigned long )__cil_tmp73;
3671#line 145
3672    __cil_tmp75 = __cil_tmp74 + 16;
3673#line 145
3674    __cil_tmp76 = *((void (**)(void * ))__cil_tmp75);
3675#line 145
3676    __cil_tmp77 = (void *)edev;
3677#line 145
3678    (*__cil_tmp76)(__cil_tmp77);
3679    }
3680  } else {
3681
3682  }
3683  }
3684  {
3685#line 147
3686  __cil_tmp78 = (unsigned long )edev;
3687#line 147
3688  __cil_tmp79 = __cil_tmp78 + 72;
3689#line 147
3690  __cil_tmp80 = (struct mutex *)__cil_tmp79;
3691#line 147
3692  mutex_unlock(__cil_tmp80);
3693  }
3694#line 148
3695  return (ret);
3696}
3697}
3698#line 172
3699static ssize_t eeprom_93xx46_write_word(struct eeprom_93xx46_dev *edev , char const   *buf ,
3700                                        unsigned int off ) ;
3701#line 172 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/drivers/misc/eeprom/eeprom_93xx46.c.common.c"
3702static struct _ddebug  __attribute__((__aligned__(8))) descriptor___1  __attribute__((__used__,
3703__section__("__verbose")))  =    {"eeprom_93xx46", "eeprom_93xx46_write_word", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/drivers/misc/eeprom/eeprom_93xx46.c.common.c",
3704    "write cmd 0x%x\n", 172U, 0U};
3705#line 151 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/drivers/misc/eeprom/eeprom_93xx46.c.common.c"
3706static ssize_t eeprom_93xx46_write_word(struct eeprom_93xx46_dev *edev , char const   *buf ,
3707                                        unsigned int off ) 
3708{ struct spi_message m ;
3709  struct spi_transfer t[2] ;
3710  int bits ;
3711  int data_len ;
3712  int ret ;
3713  u16 cmd_addr ;
3714  long tmp___7 ;
3715  unsigned long __ms ;
3716  unsigned long tmp___8 ;
3717  u16 *__cil_tmp13 ;
3718  unsigned long __cil_tmp14 ;
3719  unsigned long __cil_tmp15 ;
3720  int __cil_tmp16 ;
3721  int __cil_tmp17 ;
3722  unsigned long __cil_tmp18 ;
3723  unsigned long __cil_tmp19 ;
3724  int __cil_tmp20 ;
3725  u16 *__cil_tmp21 ;
3726  unsigned int __cil_tmp22 ;
3727  u16 *__cil_tmp23 ;
3728  u16 __cil_tmp24 ;
3729  unsigned int __cil_tmp25 ;
3730  unsigned int __cil_tmp26 ;
3731  u16 *__cil_tmp27 ;
3732  unsigned int __cil_tmp28 ;
3733  u16 *__cil_tmp29 ;
3734  u16 __cil_tmp30 ;
3735  unsigned int __cil_tmp31 ;
3736  unsigned int __cil_tmp32 ;
3737  struct _ddebug  __attribute__((__aligned__(8))) *__cil_tmp33 ;
3738  unsigned int __cil_tmp34 ;
3739  unsigned int __cil_tmp35 ;
3740  int __cil_tmp36 ;
3741  int __cil_tmp37 ;
3742  long __cil_tmp38 ;
3743  struct spi_device *__cil_tmp39 ;
3744  struct device *__cil_tmp40 ;
3745  struct device  const  *__cil_tmp41 ;
3746  u16 *__cil_tmp42 ;
3747  u16 __cil_tmp43 ;
3748  int __cil_tmp44 ;
3749  unsigned long __cil_tmp45 ;
3750  unsigned long __cil_tmp46 ;
3751  struct spi_transfer *__cil_tmp47 ;
3752  void *__cil_tmp48 ;
3753  unsigned long __cil_tmp49 ;
3754  unsigned long __cil_tmp50 ;
3755  char *__cil_tmp51 ;
3756  unsigned long __cil_tmp52 ;
3757  unsigned long __cil_tmp53 ;
3758  unsigned long __cil_tmp54 ;
3759  unsigned long __cil_tmp55 ;
3760  unsigned long __cil_tmp56 ;
3761  unsigned long __cil_tmp57 ;
3762  unsigned long __cil_tmp58 ;
3763  unsigned long __cil_tmp59 ;
3764  struct spi_transfer *__cil_tmp60 ;
3765  unsigned long __cil_tmp61 ;
3766  unsigned long __cil_tmp62 ;
3767  unsigned long __cil_tmp63 ;
3768  unsigned long __cil_tmp64 ;
3769  unsigned long __cil_tmp65 ;
3770  unsigned long __cil_tmp66 ;
3771  unsigned long __cil_tmp67 ;
3772  unsigned long __cil_tmp68 ;
3773  unsigned long __cil_tmp69 ;
3774  unsigned long __cil_tmp70 ;
3775  struct spi_transfer *__cil_tmp71 ;
3776  struct spi_device *__cil_tmp72 ;
3777
3778  {
3779#line 160
3780  __cil_tmp13 = & cmd_addr;
3781#line 160
3782  __cil_tmp14 = (unsigned long )edev;
3783#line 160
3784  __cil_tmp15 = __cil_tmp14 + 144;
3785#line 160
3786  __cil_tmp16 = *((int *)__cil_tmp15);
3787#line 160
3788  __cil_tmp17 = 5 << __cil_tmp16;
3789#line 160
3790  *__cil_tmp13 = (u16 )__cil_tmp17;
3791  {
3792#line 162
3793  __cil_tmp18 = (unsigned long )edev;
3794#line 162
3795  __cil_tmp19 = __cil_tmp18 + 144;
3796#line 162
3797  __cil_tmp20 = *((int *)__cil_tmp19);
3798#line 162
3799  if (__cil_tmp20 == 7) {
3800#line 163
3801    __cil_tmp21 = & cmd_addr;
3802#line 163
3803    __cil_tmp22 = off & 127U;
3804#line 163
3805    __cil_tmp23 = & cmd_addr;
3806#line 163
3807    __cil_tmp24 = *__cil_tmp23;
3808#line 163
3809    __cil_tmp25 = (unsigned int )__cil_tmp24;
3810#line 163
3811    __cil_tmp26 = __cil_tmp25 | __cil_tmp22;
3812#line 163
3813    *__cil_tmp21 = (u16 )__cil_tmp26;
3814#line 164
3815    bits = 10;
3816#line 165
3817    data_len = 1;
3818  } else {
3819#line 167
3820    __cil_tmp27 = & cmd_addr;
3821#line 167
3822    __cil_tmp28 = off & 63U;
3823#line 167
3824    __cil_tmp29 = & cmd_addr;
3825#line 167
3826    __cil_tmp30 = *__cil_tmp29;
3827#line 167
3828    __cil_tmp31 = (unsigned int )__cil_tmp30;
3829#line 167
3830    __cil_tmp32 = __cil_tmp31 | __cil_tmp28;
3831#line 167
3832    *__cil_tmp27 = (u16 )__cil_tmp32;
3833#line 168
3834    bits = 9;
3835#line 169
3836    data_len = 2;
3837  }
3838  }
3839  {
3840#line 172
3841  while (1) {
3842    while_continue: /* CIL Label */ ;
3843    {
3844#line 172
3845    while (1) {
3846      while_continue___0: /* CIL Label */ ;
3847      {
3848#line 172
3849      __cil_tmp33 = & descriptor___1;
3850#line 172
3851      __cil_tmp34 = __cil_tmp33->flags;
3852#line 172
3853      __cil_tmp35 = __cil_tmp34 & 1U;
3854#line 172
3855      __cil_tmp36 = ! __cil_tmp35;
3856#line 172
3857      __cil_tmp37 = ! __cil_tmp36;
3858#line 172
3859      __cil_tmp38 = (long )__cil_tmp37;
3860#line 172
3861      tmp___7 = __builtin_expect(__cil_tmp38, 0L);
3862      }
3863#line 172
3864      if (tmp___7) {
3865        {
3866#line 172
3867        __cil_tmp39 = *((struct spi_device **)edev);
3868#line 172
3869        __cil_tmp40 = (struct device *)__cil_tmp39;
3870#line 172
3871        __cil_tmp41 = (struct device  const  *)__cil_tmp40;
3872#line 172
3873        __cil_tmp42 = & cmd_addr;
3874#line 172
3875        __cil_tmp43 = *__cil_tmp42;
3876#line 172
3877        __cil_tmp44 = (int )__cil_tmp43;
3878#line 172
3879        __dynamic_dev_dbg(& descriptor___1, __cil_tmp41, "write cmd 0x%x\n", __cil_tmp44);
3880        }
3881      } else {
3882
3883      }
3884#line 172
3885      goto while_break___0;
3886    }
3887    while_break___0: /* CIL Label */ ;
3888    }
3889#line 172
3890    goto while_break;
3891  }
3892  while_break: /* CIL Label */ ;
3893  }
3894  {
3895#line 174
3896  spi_message_init(& m);
3897#line 175
3898  __cil_tmp45 = 0 * 64UL;
3899#line 175
3900  __cil_tmp46 = (unsigned long )(t) + __cil_tmp45;
3901#line 175
3902  __cil_tmp47 = (struct spi_transfer *)__cil_tmp46;
3903#line 175
3904  __cil_tmp48 = (void *)__cil_tmp47;
3905#line 175
3906  memset(__cil_tmp48, 0, 128UL);
3907#line 177
3908  __cil_tmp49 = 0 * 64UL;
3909#line 177
3910  __cil_tmp50 = (unsigned long )(t) + __cil_tmp49;
3911#line 177
3912  __cil_tmp51 = (char *)(& cmd_addr);
3913#line 177
3914  *((void const   **)__cil_tmp50) = (void const   *)__cil_tmp51;
3915#line 178
3916  __cil_tmp52 = 0 * 64UL;
3917#line 178
3918  __cil_tmp53 = __cil_tmp52 + 16;
3919#line 178
3920  __cil_tmp54 = (unsigned long )(t) + __cil_tmp53;
3921#line 178
3922  *((unsigned int *)__cil_tmp54) = 2U;
3923#line 179
3924  __cil_tmp55 = 0 * 64UL;
3925#line 179
3926  __cil_tmp56 = __cil_tmp55 + 41;
3927#line 179
3928  __cil_tmp57 = (unsigned long )(t) + __cil_tmp56;
3929#line 179
3930  *((u8 *)__cil_tmp57) = (u8 )bits;
3931#line 180
3932  __cil_tmp58 = 0 * 64UL;
3933#line 180
3934  __cil_tmp59 = (unsigned long )(t) + __cil_tmp58;
3935#line 180
3936  __cil_tmp60 = (struct spi_transfer *)__cil_tmp59;
3937#line 180
3938  spi_message_add_tail(__cil_tmp60, & m);
3939#line 182
3940  __cil_tmp61 = 1 * 64UL;
3941#line 182
3942  __cil_tmp62 = (unsigned long )(t) + __cil_tmp61;
3943#line 182
3944  *((void const   **)__cil_tmp62) = (void const   *)buf;
3945#line 183
3946  __cil_tmp63 = 1 * 64UL;
3947#line 183
3948  __cil_tmp64 = __cil_tmp63 + 16;
3949#line 183
3950  __cil_tmp65 = (unsigned long )(t) + __cil_tmp64;
3951#line 183
3952  *((unsigned int *)__cil_tmp65) = (unsigned int )data_len;
3953#line 184
3954  __cil_tmp66 = 1 * 64UL;
3955#line 184
3956  __cil_tmp67 = __cil_tmp66 + 41;
3957#line 184
3958  __cil_tmp68 = (unsigned long )(t) + __cil_tmp67;
3959#line 184
3960  *((u8 *)__cil_tmp68) = (u8 )8;
3961#line 185
3962  __cil_tmp69 = 1 * 64UL;
3963#line 185
3964  __cil_tmp70 = (unsigned long )(t) + __cil_tmp69;
3965#line 185
3966  __cil_tmp71 = (struct spi_transfer *)__cil_tmp70;
3967#line 185
3968  spi_message_add_tail(__cil_tmp71, & m);
3969#line 187
3970  __cil_tmp72 = *((struct spi_device **)edev);
3971#line 187
3972  ret = spi_sync(__cil_tmp72, & m);
3973#line 189
3974  __ms = 6UL;
3975  }
3976  {
3977#line 189
3978  while (1) {
3979    while_continue___1: /* CIL Label */ ;
3980#line 189
3981    tmp___8 = __ms;
3982#line 189
3983    __ms = __ms - 1UL;
3984#line 189
3985    if (tmp___8) {
3986
3987    } else {
3988#line 189
3989      goto while_break___1;
3990    }
3991    {
3992#line 189
3993    __const_udelay(4295000UL);
3994    }
3995  }
3996  while_break___1: /* CIL Label */ ;
3997  }
3998#line 190
3999  return ((ssize_t )ret);
4000}
4001}
4002#line 193 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/drivers/misc/eeprom/eeprom_93xx46.c.common.c"
4003static ssize_t eeprom_93xx46_bin_write(struct file *filp , struct kobject *kobj ,
4004                                       struct bin_attribute *bin_attr , char *buf ,
4005                                       loff_t off , size_t count ) 
4006{ struct eeprom_93xx46_dev *edev ;
4007  struct device *dev ;
4008  int i ;
4009  int ret ;
4010  int step ;
4011  struct kobject  const  *__mptr ;
4012  void *tmp___7 ;
4013  long tmp___8 ;
4014  long tmp___9 ;
4015  ssize_t tmp___10 ;
4016  size_t tmp___11 ;
4017  struct device *__cil_tmp18 ;
4018  unsigned long __cil_tmp19 ;
4019  unsigned long __cil_tmp20 ;
4020  struct kobject *__cil_tmp21 ;
4021  unsigned int __cil_tmp22 ;
4022  char *__cil_tmp23 ;
4023  char *__cil_tmp24 ;
4024  struct device  const  *__cil_tmp25 ;
4025  unsigned long __cil_tmp26 ;
4026  unsigned long __cil_tmp27 ;
4027  unsigned long __cil_tmp28 ;
4028  size_t __cil_tmp29 ;
4029  loff_t __cil_tmp30 ;
4030  int __cil_tmp31 ;
4031  int __cil_tmp32 ;
4032  int __cil_tmp33 ;
4033  long __cil_tmp34 ;
4034  unsigned long __cil_tmp35 ;
4035  unsigned long __cil_tmp36 ;
4036  unsigned long __cil_tmp37 ;
4037  size_t __cil_tmp38 ;
4038  loff_t __cil_tmp39 ;
4039  loff_t __cil_tmp40 ;
4040  loff_t __cil_tmp41 ;
4041  unsigned long __cil_tmp42 ;
4042  unsigned long __cil_tmp43 ;
4043  unsigned long __cil_tmp44 ;
4044  size_t __cil_tmp45 ;
4045  loff_t __cil_tmp46 ;
4046  loff_t __cil_tmp47 ;
4047  int __cil_tmp48 ;
4048  int __cil_tmp49 ;
4049  int __cil_tmp50 ;
4050  long __cil_tmp51 ;
4051  unsigned long __cil_tmp52 ;
4052  unsigned long __cil_tmp53 ;
4053  int __cil_tmp54 ;
4054  unsigned long __cil_tmp55 ;
4055  unsigned long __cil_tmp56 ;
4056  struct mutex *__cil_tmp57 ;
4057  unsigned long __cil_tmp58 ;
4058  unsigned long __cil_tmp59 ;
4059  struct eeprom_93xx46_platform_data *__cil_tmp60 ;
4060  unsigned long __cil_tmp61 ;
4061  unsigned long __cil_tmp62 ;
4062  unsigned long __cil_tmp63 ;
4063  unsigned long __cil_tmp64 ;
4064  struct eeprom_93xx46_platform_data *__cil_tmp65 ;
4065  unsigned long __cil_tmp66 ;
4066  unsigned long __cil_tmp67 ;
4067  void (*__cil_tmp68)(void * ) ;
4068  void *__cil_tmp69 ;
4069  size_t __cil_tmp70 ;
4070  char *__cil_tmp71 ;
4071  char const   *__cil_tmp72 ;
4072  loff_t __cil_tmp73 ;
4073  loff_t __cil_tmp74 ;
4074  unsigned int __cil_tmp75 ;
4075  struct spi_device *__cil_tmp76 ;
4076  struct device *__cil_tmp77 ;
4077  struct device  const  *__cil_tmp78 ;
4078  int __cil_tmp79 ;
4079  int __cil_tmp80 ;
4080  unsigned long __cil_tmp81 ;
4081  unsigned long __cil_tmp82 ;
4082  struct eeprom_93xx46_platform_data *__cil_tmp83 ;
4083  unsigned long __cil_tmp84 ;
4084  unsigned long __cil_tmp85 ;
4085  unsigned long __cil_tmp86 ;
4086  unsigned long __cil_tmp87 ;
4087  struct eeprom_93xx46_platform_data *__cil_tmp88 ;
4088  unsigned long __cil_tmp89 ;
4089  unsigned long __cil_tmp90 ;
4090  void (*__cil_tmp91)(void * ) ;
4091  void *__cil_tmp92 ;
4092  unsigned long __cil_tmp93 ;
4093  unsigned long __cil_tmp94 ;
4094  struct mutex *__cil_tmp95 ;
4095
4096  {
4097  {
4098#line 200
4099  step = 1;
4100#line 202
4101  __mptr = (struct kobject  const  *)kobj;
4102#line 202
4103  __cil_tmp18 = (struct device *)0;
4104#line 202
4105  __cil_tmp19 = (unsigned long )__cil_tmp18;
4106#line 202
4107  __cil_tmp20 = __cil_tmp19 + 16;
4108#line 202
4109  __cil_tmp21 = (struct kobject *)__cil_tmp20;
4110#line 202
4111  __cil_tmp22 = (unsigned int )__cil_tmp21;
4112#line 202
4113  __cil_tmp23 = (char *)__mptr;
4114#line 202
4115  __cil_tmp24 = __cil_tmp23 - __cil_tmp22;
4116#line 202
4117  dev = (struct device *)__cil_tmp24;
4118#line 203
4119  __cil_tmp25 = (struct device  const  *)dev;
4120#line 203
4121  tmp___7 = dev_get_drvdata(__cil_tmp25);
4122#line 203
4123  edev = (struct eeprom_93xx46_dev *)tmp___7;
4124#line 205
4125  __cil_tmp26 = 16 + 16;
4126#line 205
4127  __cil_tmp27 = (unsigned long )edev;
4128#line 205
4129  __cil_tmp28 = __cil_tmp27 + __cil_tmp26;
4130#line 205
4131  __cil_tmp29 = *((size_t *)__cil_tmp28);
4132#line 205
4133  __cil_tmp30 = (loff_t )__cil_tmp29;
4134#line 205
4135  __cil_tmp31 = off >= __cil_tmp30;
4136#line 205
4137  __cil_tmp32 = ! __cil_tmp31;
4138#line 205
4139  __cil_tmp33 = ! __cil_tmp32;
4140#line 205
4141  __cil_tmp34 = (long )__cil_tmp33;
4142#line 205
4143  tmp___8 = __builtin_expect(__cil_tmp34, 0L);
4144  }
4145#line 205
4146  if (tmp___8) {
4147#line 206
4148    return ((ssize_t )0);
4149  } else {
4150
4151  }
4152  {
4153#line 207
4154  __cil_tmp35 = 16 + 16;
4155#line 207
4156  __cil_tmp36 = (unsigned long )edev;
4157#line 207
4158  __cil_tmp37 = __cil_tmp36 + __cil_tmp35;
4159#line 207
4160  __cil_tmp38 = *((size_t *)__cil_tmp37);
4161#line 207
4162  __cil_tmp39 = (loff_t )__cil_tmp38;
4163#line 207
4164  __cil_tmp40 = (loff_t )count;
4165#line 207
4166  __cil_tmp41 = off + __cil_tmp40;
4167#line 207
4168  if (__cil_tmp41 > __cil_tmp39) {
4169#line 208
4170    __cil_tmp42 = 16 + 16;
4171#line 208
4172    __cil_tmp43 = (unsigned long )edev;
4173#line 208
4174    __cil_tmp44 = __cil_tmp43 + __cil_tmp42;
4175#line 208
4176    __cil_tmp45 = *((size_t *)__cil_tmp44);
4177#line 208
4178    __cil_tmp46 = (loff_t )__cil_tmp45;
4179#line 208
4180    __cil_tmp47 = __cil_tmp46 - off;
4181#line 208
4182    count = (size_t )__cil_tmp47;
4183  } else {
4184
4185  }
4186  }
4187  {
4188#line 209
4189  __cil_tmp48 = ! count;
4190#line 209
4191  __cil_tmp49 = ! __cil_tmp48;
4192#line 209
4193  __cil_tmp50 = ! __cil_tmp49;
4194#line 209
4195  __cil_tmp51 = (long )__cil_tmp50;
4196#line 209
4197  tmp___9 = __builtin_expect(__cil_tmp51, 0L);
4198  }
4199#line 209
4200  if (tmp___9) {
4201#line 210
4202    return ((ssize_t )count);
4203  } else {
4204
4205  }
4206  {
4207#line 213
4208  __cil_tmp52 = (unsigned long )edev;
4209#line 213
4210  __cil_tmp53 = __cil_tmp52 + 144;
4211#line 213
4212  __cil_tmp54 = *((int *)__cil_tmp53);
4213#line 213
4214  if (__cil_tmp54 == 6) {
4215#line 214
4216    step = 2;
4217#line 215
4218    count = count & 0xfffffffffffffffeUL;
4219  } else {
4220
4221  }
4222  }
4223  {
4224#line 219
4225  ret = eeprom_93xx46_ew(edev, 1);
4226  }
4227#line 220
4228  if (ret) {
4229#line 221
4230    return ((ssize_t )ret);
4231  } else {
4232
4233  }
4234  {
4235#line 223
4236  __cil_tmp55 = (unsigned long )edev;
4237#line 223
4238  __cil_tmp56 = __cil_tmp55 + 72;
4239#line 223
4240  __cil_tmp57 = (struct mutex *)__cil_tmp56;
4241#line 223
4242  mutex_lock(__cil_tmp57);
4243  }
4244  {
4245#line 225
4246  __cil_tmp58 = (unsigned long )edev;
4247#line 225
4248  __cil_tmp59 = __cil_tmp58 + 8;
4249#line 225
4250  __cil_tmp60 = *((struct eeprom_93xx46_platform_data **)__cil_tmp59);
4251#line 225
4252  __cil_tmp61 = (unsigned long )__cil_tmp60;
4253#line 225
4254  __cil_tmp62 = __cil_tmp61 + 8;
4255#line 225
4256  if (*((void (**)(void * ))__cil_tmp62)) {
4257    {
4258#line 226
4259    __cil_tmp63 = (unsigned long )edev;
4260#line 226
4261    __cil_tmp64 = __cil_tmp63 + 8;
4262#line 226
4263    __cil_tmp65 = *((struct eeprom_93xx46_platform_data **)__cil_tmp64);
4264#line 226
4265    __cil_tmp66 = (unsigned long )__cil_tmp65;
4266#line 226
4267    __cil_tmp67 = __cil_tmp66 + 8;
4268#line 226
4269    __cil_tmp68 = *((void (**)(void * ))__cil_tmp67);
4270#line 226
4271    __cil_tmp69 = (void *)edev;
4272#line 226
4273    (*__cil_tmp68)(__cil_tmp69);
4274    }
4275  } else {
4276
4277  }
4278  }
4279#line 228
4280  i = 0;
4281  {
4282#line 228
4283  while (1) {
4284    while_continue: /* CIL Label */ ;
4285    {
4286#line 228
4287    __cil_tmp70 = (size_t )i;
4288#line 228
4289    if (__cil_tmp70 < count) {
4290
4291    } else {
4292#line 228
4293      goto while_break;
4294    }
4295    }
4296    {
4297#line 229
4298    __cil_tmp71 = buf + i;
4299#line 229
4300    __cil_tmp72 = (char const   *)__cil_tmp71;
4301#line 229
4302    __cil_tmp73 = (loff_t )i;
4303#line 229
4304    __cil_tmp74 = off + __cil_tmp73;
4305#line 229
4306    __cil_tmp75 = (unsigned int )__cil_tmp74;
4307#line 229
4308    tmp___10 = eeprom_93xx46_write_word(edev, __cil_tmp72, __cil_tmp75);
4309#line 229
4310    ret = (int )tmp___10;
4311    }
4312#line 230
4313    if (ret) {
4314      {
4315#line 231
4316      __cil_tmp76 = *((struct spi_device **)edev);
4317#line 231
4318      __cil_tmp77 = (struct device *)__cil_tmp76;
4319#line 231
4320      __cil_tmp78 = (struct device  const  *)__cil_tmp77;
4321#line 231
4322      __cil_tmp79 = (int )off;
4323#line 231
4324      __cil_tmp80 = __cil_tmp79 + i;
4325#line 231
4326      dev_err(__cil_tmp78, "write failed at %d: %d\n", __cil_tmp80, ret);
4327      }
4328#line 233
4329      goto while_break;
4330    } else {
4331
4332    }
4333#line 228
4334    i = i + step;
4335  }
4336  while_break: /* CIL Label */ ;
4337  }
4338  {
4339#line 237
4340  __cil_tmp81 = (unsigned long )edev;
4341#line 237
4342  __cil_tmp82 = __cil_tmp81 + 8;
4343#line 237
4344  __cil_tmp83 = *((struct eeprom_93xx46_platform_data **)__cil_tmp82);
4345#line 237
4346  __cil_tmp84 = (unsigned long )__cil_tmp83;
4347#line 237
4348  __cil_tmp85 = __cil_tmp84 + 16;
4349#line 237
4350  if (*((void (**)(void * ))__cil_tmp85)) {
4351    {
4352#line 238
4353    __cil_tmp86 = (unsigned long )edev;
4354#line 238
4355    __cil_tmp87 = __cil_tmp86 + 8;
4356#line 238
4357    __cil_tmp88 = *((struct eeprom_93xx46_platform_data **)__cil_tmp87);
4358#line 238
4359    __cil_tmp89 = (unsigned long )__cil_tmp88;
4360#line 238
4361    __cil_tmp90 = __cil_tmp89 + 16;
4362#line 238
4363    __cil_tmp91 = *((void (**)(void * ))__cil_tmp90);
4364#line 238
4365    __cil_tmp92 = (void *)edev;
4366#line 238
4367    (*__cil_tmp91)(__cil_tmp92);
4368    }
4369  } else {
4370
4371  }
4372  }
4373  {
4374#line 240
4375  __cil_tmp93 = (unsigned long )edev;
4376#line 240
4377  __cil_tmp94 = __cil_tmp93 + 72;
4378#line 240
4379  __cil_tmp95 = (struct mutex *)__cil_tmp94;
4380#line 240
4381  mutex_unlock(__cil_tmp95);
4382#line 243
4383  eeprom_93xx46_ew(edev, 0);
4384#line 244
4385  tmp___11 = (size_t )ret;
4386  }
4387#line 244
4388  if (tmp___11) {
4389
4390  } else {
4391#line 244
4392    tmp___11 = count;
4393  }
4394#line 244
4395  return ((ssize_t )tmp___11);
4396}
4397}
4398#line 247 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/drivers/misc/eeprom/eeprom_93xx46.c.common.c"
4399static int eeprom_93xx46_eral(struct eeprom_93xx46_dev *edev ) 
4400{ struct eeprom_93xx46_platform_data *pd ;
4401  struct spi_message m ;
4402  struct spi_transfer t ;
4403  int bits ;
4404  int ret ;
4405  u16 cmd_addr ;
4406  unsigned long __ms ;
4407  unsigned long tmp___7 ;
4408  unsigned long __cil_tmp10 ;
4409  unsigned long __cil_tmp11 ;
4410  u16 *__cil_tmp12 ;
4411  unsigned long __cil_tmp13 ;
4412  unsigned long __cil_tmp14 ;
4413  int __cil_tmp15 ;
4414  int __cil_tmp16 ;
4415  unsigned long __cil_tmp17 ;
4416  unsigned long __cil_tmp18 ;
4417  int __cil_tmp19 ;
4418  u16 *__cil_tmp20 ;
4419  int __cil_tmp21 ;
4420  u16 *__cil_tmp22 ;
4421  u16 __cil_tmp23 ;
4422  int __cil_tmp24 ;
4423  int __cil_tmp25 ;
4424  u16 *__cil_tmp26 ;
4425  u16 *__cil_tmp27 ;
4426  u16 __cil_tmp28 ;
4427  int __cil_tmp29 ;
4428  int __cil_tmp30 ;
4429  void *__cil_tmp31 ;
4430  struct spi_transfer *__cil_tmp32 ;
4431  unsigned long __cil_tmp33 ;
4432  unsigned long __cil_tmp34 ;
4433  unsigned long __cil_tmp35 ;
4434  unsigned long __cil_tmp36 ;
4435  struct mutex *__cil_tmp37 ;
4436  unsigned long __cil_tmp38 ;
4437  unsigned long __cil_tmp39 ;
4438  struct eeprom_93xx46_platform_data *__cil_tmp40 ;
4439  unsigned long __cil_tmp41 ;
4440  unsigned long __cil_tmp42 ;
4441  unsigned long __cil_tmp43 ;
4442  unsigned long __cil_tmp44 ;
4443  struct eeprom_93xx46_platform_data *__cil_tmp45 ;
4444  unsigned long __cil_tmp46 ;
4445  unsigned long __cil_tmp47 ;
4446  void (*__cil_tmp48)(void * ) ;
4447  void *__cil_tmp49 ;
4448  struct spi_device *__cil_tmp50 ;
4449  struct spi_device *__cil_tmp51 ;
4450  struct device *__cil_tmp52 ;
4451  struct device  const  *__cil_tmp53 ;
4452  unsigned long __cil_tmp54 ;
4453  unsigned long __cil_tmp55 ;
4454  unsigned long __cil_tmp56 ;
4455  unsigned long __cil_tmp57 ;
4456  void (*__cil_tmp58)(void * ) ;
4457  void *__cil_tmp59 ;
4458  unsigned long __cil_tmp60 ;
4459  unsigned long __cil_tmp61 ;
4460  struct mutex *__cil_tmp62 ;
4461
4462  {
4463#line 249
4464  __cil_tmp10 = (unsigned long )edev;
4465#line 249
4466  __cil_tmp11 = __cil_tmp10 + 8;
4467#line 249
4468  pd = *((struct eeprom_93xx46_platform_data **)__cil_tmp11);
4469#line 255
4470  __cil_tmp12 = & cmd_addr;
4471#line 255
4472  __cil_tmp13 = (unsigned long )edev;
4473#line 255
4474  __cil_tmp14 = __cil_tmp13 + 144;
4475#line 255
4476  __cil_tmp15 = *((int *)__cil_tmp14);
4477#line 255
4478  __cil_tmp16 = 4 << __cil_tmp15;
4479#line 255
4480  *__cil_tmp12 = (u16 )__cil_tmp16;
4481  {
4482#line 256
4483  __cil_tmp17 = (unsigned long )edev;
4484#line 256
4485  __cil_tmp18 = __cil_tmp17 + 144;
4486#line 256
4487  __cil_tmp19 = *((int *)__cil_tmp18);
4488#line 256
4489  if (__cil_tmp19 == 7) {
4490#line 257
4491    __cil_tmp20 = & cmd_addr;
4492#line 257
4493    __cil_tmp21 = 32 << 1;
4494#line 257
4495    __cil_tmp22 = & cmd_addr;
4496#line 257
4497    __cil_tmp23 = *__cil_tmp22;
4498#line 257
4499    __cil_tmp24 = (int )__cil_tmp23;
4500#line 257
4501    __cil_tmp25 = __cil_tmp24 | __cil_tmp21;
4502#line 257
4503    *__cil_tmp20 = (u16 )__cil_tmp25;
4504#line 258
4505    bits = 10;
4506  } else {
4507#line 260
4508    __cil_tmp26 = & cmd_addr;
4509#line 260
4510    __cil_tmp27 = & cmd_addr;
4511#line 260
4512    __cil_tmp28 = *__cil_tmp27;
4513#line 260
4514    __cil_tmp29 = (int )__cil_tmp28;
4515#line 260
4516    __cil_tmp30 = __cil_tmp29 | 32;
4517#line 260
4518    *__cil_tmp26 = (u16 )__cil_tmp30;
4519#line 261
4520    bits = 9;
4521  }
4522  }
4523  {
4524#line 264
4525  spi_message_init(& m);
4526#line 265
4527  __cil_tmp31 = (void *)(& t);
4528#line 265
4529  memset(__cil_tmp31, 0, 64UL);
4530#line 267
4531  __cil_tmp32 = & t;
4532#line 267
4533  *((void const   **)__cil_tmp32) = (void const   *)(& cmd_addr);
4534#line 268
4535  __cil_tmp33 = (unsigned long )(& t) + 16;
4536#line 268
4537  *((unsigned int *)__cil_tmp33) = 2U;
4538#line 269
4539  __cil_tmp34 = (unsigned long )(& t) + 41;
4540#line 269
4541  *((u8 *)__cil_tmp34) = (u8 )bits;
4542#line 270
4543  spi_message_add_tail(& t, & m);
4544#line 272
4545  __cil_tmp35 = (unsigned long )edev;
4546#line 272
4547  __cil_tmp36 = __cil_tmp35 + 72;
4548#line 272
4549  __cil_tmp37 = (struct mutex *)__cil_tmp36;
4550#line 272
4551  mutex_lock(__cil_tmp37);
4552  }
4553  {
4554#line 274
4555  __cil_tmp38 = (unsigned long )edev;
4556#line 274
4557  __cil_tmp39 = __cil_tmp38 + 8;
4558#line 274
4559  __cil_tmp40 = *((struct eeprom_93xx46_platform_data **)__cil_tmp39);
4560#line 274
4561  __cil_tmp41 = (unsigned long )__cil_tmp40;
4562#line 274
4563  __cil_tmp42 = __cil_tmp41 + 8;
4564#line 274
4565  if (*((void (**)(void * ))__cil_tmp42)) {
4566    {
4567#line 275
4568    __cil_tmp43 = (unsigned long )edev;
4569#line 275
4570    __cil_tmp44 = __cil_tmp43 + 8;
4571#line 275
4572    __cil_tmp45 = *((struct eeprom_93xx46_platform_data **)__cil_tmp44);
4573#line 275
4574    __cil_tmp46 = (unsigned long )__cil_tmp45;
4575#line 275
4576    __cil_tmp47 = __cil_tmp46 + 8;
4577#line 275
4578    __cil_tmp48 = *((void (**)(void * ))__cil_tmp47);
4579#line 275
4580    __cil_tmp49 = (void *)edev;
4581#line 275
4582    (*__cil_tmp48)(__cil_tmp49);
4583    }
4584  } else {
4585
4586  }
4587  }
4588  {
4589#line 277
4590  __cil_tmp50 = *((struct spi_device **)edev);
4591#line 277
4592  ret = spi_sync(__cil_tmp50, & m);
4593  }
4594#line 278
4595  if (ret) {
4596    {
4597#line 279
4598    __cil_tmp51 = *((struct spi_device **)edev);
4599#line 279
4600    __cil_tmp52 = (struct device *)__cil_tmp51;
4601#line 279
4602    __cil_tmp53 = (struct device  const  *)__cil_tmp52;
4603#line 279
4604    dev_err(__cil_tmp53, "erase error %d\n", ret);
4605    }
4606  } else {
4607
4608  }
4609#line 281
4610  __ms = 6UL;
4611  {
4612#line 281
4613  while (1) {
4614    while_continue: /* CIL Label */ ;
4615#line 281
4616    tmp___7 = __ms;
4617#line 281
4618    __ms = __ms - 1UL;
4619#line 281
4620    if (tmp___7) {
4621
4622    } else {
4623#line 281
4624      goto while_break;
4625    }
4626    {
4627#line 281
4628    __const_udelay(4295000UL);
4629    }
4630  }
4631  while_break: /* CIL Label */ ;
4632  }
4633  {
4634#line 283
4635  __cil_tmp54 = (unsigned long )pd;
4636#line 283
4637  __cil_tmp55 = __cil_tmp54 + 16;
4638#line 283
4639  if (*((void (**)(void * ))__cil_tmp55)) {
4640    {
4641#line 284
4642    __cil_tmp56 = (unsigned long )pd;
4643#line 284
4644    __cil_tmp57 = __cil_tmp56 + 16;
4645#line 284
4646    __cil_tmp58 = *((void (**)(void * ))__cil_tmp57);
4647#line 284
4648    __cil_tmp59 = (void *)edev;
4649#line 284
4650    (*__cil_tmp58)(__cil_tmp59);
4651    }
4652  } else {
4653
4654  }
4655  }
4656  {
4657#line 286
4658  __cil_tmp60 = (unsigned long )edev;
4659#line 286
4660  __cil_tmp61 = __cil_tmp60 + 72;
4661#line 286
4662  __cil_tmp62 = (struct mutex *)__cil_tmp61;
4663#line 286
4664  mutex_unlock(__cil_tmp62);
4665  }
4666#line 287
4667  return (ret);
4668}
4669}
4670#line 290 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/drivers/misc/eeprom/eeprom_93xx46.c.common.c"
4671static ssize_t eeprom_93xx46_store_erase(struct device *dev , struct device_attribute *attr ,
4672                                         char const   *buf , size_t count ) 
4673{ struct eeprom_93xx46_dev *edev ;
4674  void *tmp___7 ;
4675  int erase ;
4676  int ret ;
4677  struct device  const  *__cil_tmp9 ;
4678  int *__cil_tmp10 ;
4679  int *__cil_tmp11 ;
4680
4681  {
4682  {
4683#line 294
4684  __cil_tmp9 = (struct device  const  *)dev;
4685#line 294
4686  tmp___7 = dev_get_drvdata(__cil_tmp9);
4687#line 294
4688  edev = (struct eeprom_93xx46_dev *)tmp___7;
4689#line 295
4690  __cil_tmp10 = & erase;
4691#line 295
4692  *__cil_tmp10 = 0;
4693#line 297
4694  sscanf(buf, "%d", & erase);
4695  }
4696  {
4697#line 298
4698  __cil_tmp11 = & erase;
4699#line 298
4700  if (*__cil_tmp11) {
4701    {
4702#line 299
4703    ret = eeprom_93xx46_ew(edev, 1);
4704    }
4705#line 300
4706    if (ret) {
4707#line 301
4708      return ((ssize_t )ret);
4709    } else {
4710
4711    }
4712    {
4713#line 302
4714    ret = eeprom_93xx46_eral(edev);
4715    }
4716#line 303
4717    if (ret) {
4718#line 304
4719      return ((ssize_t )ret);
4720    } else {
4721
4722    }
4723    {
4724#line 305
4725    ret = eeprom_93xx46_ew(edev, 0);
4726    }
4727#line 306
4728    if (ret) {
4729#line 307
4730      return ((ssize_t )ret);
4731    } else {
4732
4733    }
4734  } else {
4735
4736  }
4737  }
4738#line 309
4739  return ((ssize_t )count);
4740}
4741}
4742#line 311 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/drivers/misc/eeprom/eeprom_93xx46.c.common.c"
4743static struct device_attribute dev_attr_erase  =    {{"erase", (umode_t )128}, (ssize_t (*)(struct device *dev , struct device_attribute *attr ,
4744                                           char *buf ))((void *)0), & eeprom_93xx46_store_erase};
4745#line 339 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/drivers/misc/eeprom/eeprom_93xx46.c.common.c"
4746static struct lock_class_key __key___3  ;
4747#line 313
4748static int eeprom_93xx46_probe(struct spi_device *spi )  __attribute__((__section__(".devinit.text"),
4749__no_instrument_function__)) ;
4750#line 313 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/drivers/misc/eeprom/eeprom_93xx46.c.common.c"
4751static int eeprom_93xx46_probe(struct spi_device *spi ) 
4752{ struct eeprom_93xx46_platform_data *pd ;
4753  struct eeprom_93xx46_dev *edev ;
4754  int err ;
4755  void *tmp___7 ;
4756  char const   *tmp___8 ;
4757  int tmp___9 ;
4758  int tmp___10 ;
4759  unsigned long __cil_tmp9 ;
4760  unsigned long __cil_tmp10 ;
4761  unsigned long __cil_tmp11 ;
4762  void *__cil_tmp12 ;
4763  struct device *__cil_tmp13 ;
4764  struct device  const  *__cil_tmp14 ;
4765  unsigned char __cil_tmp15 ;
4766  int __cil_tmp16 ;
4767  unsigned long __cil_tmp17 ;
4768  unsigned long __cil_tmp18 ;
4769  unsigned char __cil_tmp19 ;
4770  int __cil_tmp20 ;
4771  unsigned long __cil_tmp21 ;
4772  unsigned long __cil_tmp22 ;
4773  struct device *__cil_tmp23 ;
4774  struct device  const  *__cil_tmp24 ;
4775  unsigned long __cil_tmp25 ;
4776  unsigned long __cil_tmp26 ;
4777  struct mutex *__cil_tmp27 ;
4778  unsigned long __cil_tmp28 ;
4779  unsigned long __cil_tmp29 ;
4780  unsigned long __cil_tmp30 ;
4781  unsigned long __cil_tmp31 ;
4782  unsigned long __cil_tmp32 ;
4783  unsigned long __cil_tmp33 ;
4784  unsigned long __cil_tmp34 ;
4785  unsigned long __cil_tmp35 ;
4786  unsigned long __cil_tmp36 ;
4787  unsigned long __cil_tmp37 ;
4788  unsigned long __cil_tmp38 ;
4789  unsigned long __cil_tmp39 ;
4790  unsigned long __cil_tmp40 ;
4791  unsigned long __cil_tmp41 ;
4792  unsigned char __cil_tmp42 ;
4793  int __cil_tmp43 ;
4794  int __cil_tmp44 ;
4795  unsigned long __cil_tmp45 ;
4796  unsigned long __cil_tmp46 ;
4797  unsigned long __cil_tmp47 ;
4798  unsigned long __cil_tmp48 ;
4799  unsigned long __cil_tmp49 ;
4800  unsigned long __cil_tmp50 ;
4801  unsigned long __cil_tmp51 ;
4802  unsigned long __cil_tmp52 ;
4803  unsigned long __cil_tmp53 ;
4804  unsigned long __cil_tmp54 ;
4805  unsigned long __cil_tmp55 ;
4806  umode_t __cil_tmp56 ;
4807  int __cil_tmp57 ;
4808  int __cil_tmp58 ;
4809  unsigned long __cil_tmp59 ;
4810  unsigned long __cil_tmp60 ;
4811  unsigned long __cil_tmp61 ;
4812  struct kobject *__cil_tmp62 ;
4813  unsigned long __cil_tmp63 ;
4814  unsigned long __cil_tmp64 ;
4815  struct bin_attribute *__cil_tmp65 ;
4816  struct bin_attribute  const  *__cil_tmp66 ;
4817  unsigned char __cil_tmp67 ;
4818  int __cil_tmp68 ;
4819  unsigned char __cil_tmp69 ;
4820  int __cil_tmp70 ;
4821  struct device *__cil_tmp71 ;
4822  struct device  const  *__cil_tmp72 ;
4823  unsigned char __cil_tmp73 ;
4824  int __cil_tmp74 ;
4825  int __cil_tmp75 ;
4826  struct device *__cil_tmp76 ;
4827  struct device_attribute  const  *__cil_tmp77 ;
4828  struct device *__cil_tmp78 ;
4829  struct device  const  *__cil_tmp79 ;
4830  struct device *__cil_tmp80 ;
4831  void *__cil_tmp81 ;
4832  void const   *__cil_tmp82 ;
4833
4834  {
4835#line 319
4836  __cil_tmp9 = 0 + 184;
4837#line 319
4838  __cil_tmp10 = (unsigned long )spi;
4839#line 319
4840  __cil_tmp11 = __cil_tmp10 + __cil_tmp9;
4841#line 319
4842  __cil_tmp12 = *((void **)__cil_tmp11);
4843#line 319
4844  pd = (struct eeprom_93xx46_platform_data *)__cil_tmp12;
4845#line 320
4846  if (! pd) {
4847    {
4848#line 321
4849    __cil_tmp13 = (struct device *)spi;
4850#line 321
4851    __cil_tmp14 = (struct device  const  *)__cil_tmp13;
4852#line 321
4853    dev_err(__cil_tmp14, "missing platform data\n");
4854    }
4855#line 322
4856    return (-19);
4857  } else {
4858
4859  }
4860  {
4861#line 325
4862  tmp___7 = kzalloc(152UL, 208U);
4863#line 325
4864  edev = (struct eeprom_93xx46_dev *)tmp___7;
4865  }
4866#line 326
4867  if (! edev) {
4868#line 327
4869    return (-12);
4870  } else {
4871
4872  }
4873  {
4874#line 329
4875  __cil_tmp15 = *((unsigned char *)pd);
4876#line 329
4877  __cil_tmp16 = (int )__cil_tmp15;
4878#line 329
4879  if (__cil_tmp16 & 1) {
4880#line 330
4881    __cil_tmp17 = (unsigned long )edev;
4882#line 330
4883    __cil_tmp18 = __cil_tmp17 + 144;
4884#line 330
4885    *((int *)__cil_tmp18) = 7;
4886  } else {
4887    {
4888#line 331
4889    __cil_tmp19 = *((unsigned char *)pd);
4890#line 331
4891    __cil_tmp20 = (int )__cil_tmp19;
4892#line 331
4893    if (__cil_tmp20 & 2) {
4894#line 332
4895      __cil_tmp21 = (unsigned long )edev;
4896#line 332
4897      __cil_tmp22 = __cil_tmp21 + 144;
4898#line 332
4899      *((int *)__cil_tmp22) = 6;
4900    } else {
4901      {
4902#line 334
4903      __cil_tmp23 = (struct device *)spi;
4904#line 334
4905      __cil_tmp24 = (struct device  const  *)__cil_tmp23;
4906#line 334
4907      dev_err(__cil_tmp24, "unspecified address type\n");
4908#line 335
4909      err = -22;
4910      }
4911#line 336
4912      goto fail;
4913    }
4914    }
4915  }
4916  }
4917  {
4918#line 339
4919  while (1) {
4920    while_continue: /* CIL Label */ ;
4921    {
4922#line 339
4923    __cil_tmp25 = (unsigned long )edev;
4924#line 339
4925    __cil_tmp26 = __cil_tmp25 + 72;
4926#line 339
4927    __cil_tmp27 = (struct mutex *)__cil_tmp26;
4928#line 339
4929    __mutex_init(__cil_tmp27, "&edev->lock", & __key___3);
4930    }
4931#line 339
4932    goto while_break;
4933  }
4934  while_break: /* CIL Label */ ;
4935  }
4936  {
4937#line 341
4938  *((struct spi_device **)edev) = spi_dev_get(spi);
4939#line 342
4940  __cil_tmp28 = (unsigned long )edev;
4941#line 342
4942  __cil_tmp29 = __cil_tmp28 + 8;
4943#line 342
4944  *((struct eeprom_93xx46_platform_data **)__cil_tmp29) = pd;
4945  }
4946  {
4947#line 344
4948  while (1) {
4949    while_continue___0: /* CIL Label */ ;
4950#line 344
4951    goto while_break___0;
4952  }
4953  while_break___0: /* CIL Label */ ;
4954  }
4955#line 345
4956  __cil_tmp30 = (unsigned long )edev;
4957#line 345
4958  __cil_tmp31 = __cil_tmp30 + 16;
4959#line 345
4960  *((char const   **)__cil_tmp31) = "eeprom";
4961#line 346
4962  __cil_tmp32 = 0 + 8;
4963#line 346
4964  __cil_tmp33 = 16 + __cil_tmp32;
4965#line 346
4966  __cil_tmp34 = (unsigned long )edev;
4967#line 346
4968  __cil_tmp35 = __cil_tmp34 + __cil_tmp33;
4969#line 346
4970  *((umode_t *)__cil_tmp35) = (umode_t )256;
4971#line 347
4972  __cil_tmp36 = 16 + 32;
4973#line 347
4974  __cil_tmp37 = (unsigned long )edev;
4975#line 347
4976  __cil_tmp38 = __cil_tmp37 + __cil_tmp36;
4977#line 347
4978  *((ssize_t (**)(struct file * , struct kobject * , struct bin_attribute * , char * ,
4979                  loff_t  , size_t  ))__cil_tmp38) = & eeprom_93xx46_bin_read;
4980#line 348
4981  __cil_tmp39 = 16 + 16;
4982#line 348
4983  __cil_tmp40 = (unsigned long )edev;
4984#line 348
4985  __cil_tmp41 = __cil_tmp40 + __cil_tmp39;
4986#line 348
4987  *((size_t *)__cil_tmp41) = (size_t )128;
4988  {
4989#line 349
4990  __cil_tmp42 = *((unsigned char *)pd);
4991#line 349
4992  __cil_tmp43 = (int )__cil_tmp42;
4993#line 349
4994  __cil_tmp44 = __cil_tmp43 & 8;
4995#line 349
4996  if (! __cil_tmp44) {
4997#line 350
4998    __cil_tmp45 = 16 + 40;
4999#line 350
5000    __cil_tmp46 = (unsigned long )edev;
5001#line 350
5002    __cil_tmp47 = __cil_tmp46 + __cil_tmp45;
5003#line 350
5004    *((ssize_t (**)(struct file * , struct kobject * , struct bin_attribute * , char * ,
5005                    loff_t  , size_t  ))__cil_tmp47) = & eeprom_93xx46_bin_write;
5006#line 351
5007    __cil_tmp48 = 0 + 8;
5008#line 351
5009    __cil_tmp49 = 16 + __cil_tmp48;
5010#line 351
5011    __cil_tmp50 = (unsigned long )edev;
5012#line 351
5013    __cil_tmp51 = __cil_tmp50 + __cil_tmp49;
5014#line 351
5015    __cil_tmp52 = 0 + 8;
5016#line 351
5017    __cil_tmp53 = 16 + __cil_tmp52;
5018#line 351
5019    __cil_tmp54 = (unsigned long )edev;
5020#line 351
5021    __cil_tmp55 = __cil_tmp54 + __cil_tmp53;
5022#line 351
5023    __cil_tmp56 = *((umode_t *)__cil_tmp55);
5024#line 351
5025    __cil_tmp57 = (int )__cil_tmp56;
5026#line 351
5027    __cil_tmp58 = __cil_tmp57 | 128;
5028#line 351
5029    *((umode_t *)__cil_tmp51) = (umode_t )__cil_tmp58;
5030  } else {
5031
5032  }
5033  }
5034  {
5035#line 354
5036  __cil_tmp59 = 0 + 16;
5037#line 354
5038  __cil_tmp60 = (unsigned long )spi;
5039#line 354
5040  __cil_tmp61 = __cil_tmp60 + __cil_tmp59;
5041#line 354
5042  __cil_tmp62 = (struct kobject *)__cil_tmp61;
5043#line 354
5044  __cil_tmp63 = (unsigned long )edev;
5045#line 354
5046  __cil_tmp64 = __cil_tmp63 + 16;
5047#line 354
5048  __cil_tmp65 = (struct bin_attribute *)__cil_tmp64;
5049#line 354
5050  __cil_tmp66 = (struct bin_attribute  const  *)__cil_tmp65;
5051#line 354
5052  err = (int )sysfs_create_bin_file(__cil_tmp62, __cil_tmp66);
5053  }
5054#line 355
5055  if (err) {
5056#line 356
5057    goto fail;
5058  } else {
5059
5060  }
5061  {
5062#line 358
5063  __cil_tmp67 = *((unsigned char *)pd);
5064#line 358
5065  __cil_tmp68 = (int )__cil_tmp67;
5066#line 358
5067  if (__cil_tmp68 & 8) {
5068#line 358
5069    tmp___8 = "(readonly)";
5070  } else {
5071#line 358
5072    tmp___8 = "";
5073  }
5074  }
5075  {
5076#line 358
5077  __cil_tmp69 = *((unsigned char *)pd);
5078#line 358
5079  __cil_tmp70 = (int )__cil_tmp69;
5080#line 358
5081  if (__cil_tmp70 & 1) {
5082#line 358
5083    tmp___9 = 8;
5084  } else {
5085#line 358
5086    tmp___9 = 16;
5087  }
5088  }
5089  {
5090#line 358
5091  __cil_tmp71 = (struct device *)spi;
5092#line 358
5093  __cil_tmp72 = (struct device  const  *)__cil_tmp71;
5094#line 358
5095  _dev_info(__cil_tmp72, "%d-bit eeprom %s\n", tmp___9, tmp___8);
5096  }
5097  {
5098#line 362
5099  __cil_tmp73 = *((unsigned char *)pd);
5100#line 362
5101  __cil_tmp74 = (int )__cil_tmp73;
5102#line 362
5103  __cil_tmp75 = __cil_tmp74 & 8;
5104#line 362
5105  if (! __cil_tmp75) {
5106    {
5107#line 363
5108    __cil_tmp76 = (struct device *)spi;
5109#line 363
5110    __cil_tmp77 = (struct device_attribute  const  *)(& dev_attr_erase);
5111#line 363
5112    tmp___10 = device_create_file(__cil_tmp76, __cil_tmp77);
5113    }
5114#line 363
5115    if (tmp___10) {
5116      {
5117#line 364
5118      __cil_tmp78 = (struct device *)spi;
5119#line 364
5120      __cil_tmp79 = (struct device  const  *)__cil_tmp78;
5121#line 364
5122      dev_err(__cil_tmp79, "can\'t create erase interface\n");
5123      }
5124    } else {
5125
5126    }
5127  } else {
5128
5129  }
5130  }
5131  {
5132#line 367
5133  __cil_tmp80 = (struct device *)spi;
5134#line 367
5135  __cil_tmp81 = (void *)edev;
5136#line 367
5137  dev_set_drvdata(__cil_tmp80, __cil_tmp81);
5138  }
5139#line 368
5140  return (0);
5141  fail: 
5142  {
5143#line 370
5144  __cil_tmp82 = (void const   *)edev;
5145#line 370
5146  kfree(__cil_tmp82);
5147  }
5148#line 371
5149  return (err);
5150}
5151}
5152#line 374
5153static int eeprom_93xx46_remove(struct spi_device *spi )  __attribute__((__section__(".devexit.text"),
5154__no_instrument_function__)) ;
5155#line 374 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/drivers/misc/eeprom/eeprom_93xx46.c.common.c"
5156static int eeprom_93xx46_remove(struct spi_device *spi ) 
5157{ struct eeprom_93xx46_dev *edev ;
5158  void *tmp___7 ;
5159  struct device *__cil_tmp4 ;
5160  struct device  const  *__cil_tmp5 ;
5161  unsigned long __cil_tmp6 ;
5162  unsigned long __cil_tmp7 ;
5163  struct eeprom_93xx46_platform_data *__cil_tmp8 ;
5164  unsigned char __cil_tmp9 ;
5165  int __cil_tmp10 ;
5166  int __cil_tmp11 ;
5167  struct device *__cil_tmp12 ;
5168  struct device_attribute  const  *__cil_tmp13 ;
5169  unsigned long __cil_tmp14 ;
5170  unsigned long __cil_tmp15 ;
5171  unsigned long __cil_tmp16 ;
5172  struct kobject *__cil_tmp17 ;
5173  unsigned long __cil_tmp18 ;
5174  unsigned long __cil_tmp19 ;
5175  struct bin_attribute *__cil_tmp20 ;
5176  struct bin_attribute  const  *__cil_tmp21 ;
5177  struct device *__cil_tmp22 ;
5178  void *__cil_tmp23 ;
5179  void const   *__cil_tmp24 ;
5180
5181  {
5182  {
5183#line 376
5184  __cil_tmp4 = (struct device *)spi;
5185#line 376
5186  __cil_tmp5 = (struct device  const  *)__cil_tmp4;
5187#line 376
5188  tmp___7 = dev_get_drvdata(__cil_tmp5);
5189#line 376
5190  edev = (struct eeprom_93xx46_dev *)tmp___7;
5191  }
5192  {
5193#line 378
5194  __cil_tmp6 = (unsigned long )edev;
5195#line 378
5196  __cil_tmp7 = __cil_tmp6 + 8;
5197#line 378
5198  __cil_tmp8 = *((struct eeprom_93xx46_platform_data **)__cil_tmp7);
5199#line 378
5200  __cil_tmp9 = *((unsigned char *)__cil_tmp8);
5201#line 378
5202  __cil_tmp10 = (int )__cil_tmp9;
5203#line 378
5204  __cil_tmp11 = __cil_tmp10 & 8;
5205#line 378
5206  if (! __cil_tmp11) {
5207    {
5208#line 379
5209    __cil_tmp12 = (struct device *)spi;
5210#line 379
5211    __cil_tmp13 = (struct device_attribute  const  *)(& dev_attr_erase);
5212#line 379
5213    device_remove_file(__cil_tmp12, __cil_tmp13);
5214    }
5215  } else {
5216
5217  }
5218  }
5219  {
5220#line 381
5221  __cil_tmp14 = 0 + 16;
5222#line 381
5223  __cil_tmp15 = (unsigned long )spi;
5224#line 381
5225  __cil_tmp16 = __cil_tmp15 + __cil_tmp14;
5226#line 381
5227  __cil_tmp17 = (struct kobject *)__cil_tmp16;
5228#line 381
5229  __cil_tmp18 = (unsigned long )edev;
5230#line 381
5231  __cil_tmp19 = __cil_tmp18 + 16;
5232#line 381
5233  __cil_tmp20 = (struct bin_attribute *)__cil_tmp19;
5234#line 381
5235  __cil_tmp21 = (struct bin_attribute  const  *)__cil_tmp20;
5236#line 381
5237  sysfs_remove_bin_file(__cil_tmp17, __cil_tmp21);
5238#line 382
5239  __cil_tmp22 = (struct device *)spi;
5240#line 382
5241  __cil_tmp23 = (void *)0;
5242#line 382
5243  dev_set_drvdata(__cil_tmp22, __cil_tmp23);
5244#line 383
5245  __cil_tmp24 = (void const   *)edev;
5246#line 383
5247  kfree(__cil_tmp24);
5248  }
5249#line 384
5250  return (0);
5251}
5252}
5253#line 387 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/drivers/misc/eeprom/eeprom_93xx46.c.common.c"
5254static struct spi_driver eeprom_93xx46_driver  =    {(struct spi_device_id  const  *)0, & eeprom_93xx46_probe, & eeprom_93xx46_remove,
5255    (void (*)(struct spi_device *spi ))0, (int (*)(struct spi_device *spi , pm_message_t mesg ))0,
5256    (int (*)(struct spi_device *spi ))0, {"93xx46", (struct bus_type *)0, & __this_module,
5257                                          (char const   *)0, (_Bool)0, (struct of_device_id  const  *)0,
5258                                          (int (*)(struct device *dev ))0, (int (*)(struct device *dev ))0,
5259                                          (void (*)(struct device *dev ))0, (int (*)(struct device *dev ,
5260                                                                                     pm_message_t state ))0,
5261                                          (int (*)(struct device *dev ))0, (struct attribute_group  const  **)0,
5262                                          (struct dev_pm_ops  const  *)0, (struct driver_private *)0}};
5263#line 396
5264static int eeprom_93xx46_driver_init(void)  __attribute__((__section__(".init.text"),
5265__no_instrument_function__)) ;
5266#line 396 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/drivers/misc/eeprom/eeprom_93xx46.c.common.c"
5267static int eeprom_93xx46_driver_init(void) 
5268{ int tmp___7 ;
5269
5270  {
5271  {
5272#line 396
5273  tmp___7 = spi_register_driver(& eeprom_93xx46_driver);
5274  }
5275#line 396
5276  return (tmp___7);
5277}
5278}
5279#line 396 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/drivers/misc/eeprom/eeprom_93xx46.c.common.c"
5280int init_module(void) 
5281{ int tmp___7 ;
5282
5283  {
5284  {
5285#line 396
5286  tmp___7 = eeprom_93xx46_driver_init();
5287  }
5288#line 396
5289  return (tmp___7);
5290}
5291}
5292#line 396
5293static void eeprom_93xx46_driver_exit(void)  __attribute__((__section__(".exit.text"),
5294__no_instrument_function__)) ;
5295#line 396 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/drivers/misc/eeprom/eeprom_93xx46.c.common.c"
5296static void eeprom_93xx46_driver_exit(void) 
5297{ 
5298
5299  {
5300  {
5301#line 396
5302  spi_unregister_driver(& eeprom_93xx46_driver);
5303  }
5304#line 396
5305  return;
5306}
5307}
5308#line 396 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/drivers/misc/eeprom/eeprom_93xx46.c.common.c"
5309void cleanup_module(void) 
5310{ 
5311
5312  {
5313  {
5314#line 396
5315  eeprom_93xx46_driver_exit();
5316  }
5317#line 396
5318  return;
5319}
5320}
5321#line 398 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/drivers/misc/eeprom/eeprom_93xx46.c.common.c"
5322static char const   __mod_license398[12]  __attribute__((__used__, __unused__, __section__(".modinfo"),
5323__aligned__(1)))  = 
5324#line 398
5325  {      (char const   )'l',      (char const   )'i',      (char const   )'c',      (char const   )'e', 
5326        (char const   )'n',      (char const   )'s',      (char const   )'e',      (char const   )'=', 
5327        (char const   )'G',      (char const   )'P',      (char const   )'L',      (char const   )'\000'};
5328#line 399 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/drivers/misc/eeprom/eeprom_93xx46.c.common.c"
5329static char const   __mod_description399[38]  __attribute__((__used__, __unused__,
5330__section__(".modinfo"), __aligned__(1)))  = 
5331#line 399
5332  {      (char const   )'d',      (char const   )'e',      (char const   )'s',      (char const   )'c', 
5333        (char const   )'r',      (char const   )'i',      (char const   )'p',      (char const   )'t', 
5334        (char const   )'i',      (char const   )'o',      (char const   )'n',      (char const   )'=', 
5335        (char const   )'D',      (char const   )'r',      (char const   )'i',      (char const   )'v', 
5336        (char const   )'e',      (char const   )'r',      (char const   )' ',      (char const   )'f', 
5337        (char const   )'o',      (char const   )'r',      (char const   )' ',      (char const   )'9', 
5338        (char const   )'3',      (char const   )'x',      (char const   )'x',      (char const   )'4', 
5339        (char const   )'6',      (char const   )' ',      (char const   )'E',      (char const   )'E', 
5340        (char const   )'P',      (char const   )'R',      (char const   )'O',      (char const   )'M', 
5341        (char const   )'s',      (char const   )'\000'};
5342#line 400 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/drivers/misc/eeprom/eeprom_93xx46.c.common.c"
5343static char const   __mod_author400[42]  __attribute__((__used__, __unused__, __section__(".modinfo"),
5344__aligned__(1)))  = 
5345#line 400
5346  {      (char const   )'a',      (char const   )'u',      (char const   )'t',      (char const   )'h', 
5347        (char const   )'o',      (char const   )'r',      (char const   )'=',      (char const   )'A', 
5348        (char const   )'n',      (char const   )'a',      (char const   )'t',      (char const   )'o', 
5349        (char const   )'l',      (char const   )'i',      (char const   )'j',      (char const   )' ', 
5350        (char const   )'G',      (char const   )'u',      (char const   )'s',      (char const   )'t', 
5351        (char const   )'s',      (char const   )'c',      (char const   )'h',      (char const   )'i', 
5352        (char const   )'n',      (char const   )' ',      (char const   )'<',      (char const   )'a', 
5353        (char const   )'g',      (char const   )'u',      (char const   )'s',      (char const   )'t', 
5354        (char const   )'@',      (char const   )'d',      (char const   )'e',      (char const   )'n', 
5355        (char const   )'x',      (char const   )'.',      (char const   )'d',      (char const   )'e', 
5356        (char const   )'>',      (char const   )'\000'};
5357#line 401 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/drivers/misc/eeprom/eeprom_93xx46.c.common.c"
5358static char const   __mod_alias401[17]  __attribute__((__used__, __unused__, __section__(".modinfo"),
5359__aligned__(1)))  = 
5360#line 401
5361  {      (char const   )'a',      (char const   )'l',      (char const   )'i',      (char const   )'a', 
5362        (char const   )'s',      (char const   )'=',      (char const   )'s',      (char const   )'p', 
5363        (char const   )'i',      (char const   )':',      (char const   )'9',      (char const   )'3', 
5364        (char const   )'x',      (char const   )'x',      (char const   )'4',      (char const   )'6', 
5365        (char const   )'\000'};
5366#line 419
5367void ldv_check_final_state(void) ;
5368#line 422
5369extern void ldv_check_return_value(int res ) ;
5370#line 425
5371extern void ldv_initialize(void) ;
5372#line 428
5373extern int __VERIFIER_nondet_int(void) ;
5374#line 431 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/drivers/misc/eeprom/eeprom_93xx46.c.common.c"
5375int LDV_IN_INTERRUPT  ;
5376#line 453 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/drivers/misc/eeprom/eeprom_93xx46.c.common.c"
5377static int res_eeprom_93xx46_probe_6  ;
5378#line 434 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/drivers/misc/eeprom/eeprom_93xx46.c.common.c"
5379void main(void) 
5380{ struct spi_device *var_group1 ;
5381  int ldv_s_eeprom_93xx46_driver_spi_driver ;
5382  int tmp___7 ;
5383  int tmp___8 ;
5384  int __cil_tmp5 ;
5385
5386  {
5387  {
5388#line 461
5389  LDV_IN_INTERRUPT = 1;
5390#line 470
5391  ldv_initialize();
5392#line 471
5393  ldv_s_eeprom_93xx46_driver_spi_driver = 0;
5394  }
5395  {
5396#line 474
5397  while (1) {
5398    while_continue: /* CIL Label */ ;
5399    {
5400#line 474
5401    tmp___8 = __VERIFIER_nondet_int();
5402    }
5403#line 474
5404    if (tmp___8) {
5405
5406    } else {
5407      {
5408#line 474
5409      __cil_tmp5 = ldv_s_eeprom_93xx46_driver_spi_driver == 0;
5410#line 474
5411      if (! __cil_tmp5) {
5412
5413      } else {
5414#line 474
5415        goto while_break;
5416      }
5417      }
5418    }
5419    {
5420#line 478
5421    tmp___7 = __VERIFIER_nondet_int();
5422    }
5423#line 480
5424    if (tmp___7 == 0) {
5425#line 480
5426      goto case_0;
5427    } else {
5428      {
5429#line 506
5430      goto switch_default;
5431#line 478
5432      if (0) {
5433        case_0: /* CIL Label */ 
5434#line 483
5435        if (ldv_s_eeprom_93xx46_driver_spi_driver == 0) {
5436          {
5437#line 495
5438          res_eeprom_93xx46_probe_6 = eeprom_93xx46_probe(var_group1);
5439#line 496
5440          ldv_check_return_value(res_eeprom_93xx46_probe_6);
5441          }
5442#line 497
5443          if (res_eeprom_93xx46_probe_6) {
5444#line 498
5445            goto ldv_module_exit;
5446          } else {
5447
5448          }
5449#line 499
5450          ldv_s_eeprom_93xx46_driver_spi_driver = 0;
5451        } else {
5452
5453        }
5454#line 505
5455        goto switch_break;
5456        switch_default: /* CIL Label */ 
5457#line 506
5458        goto switch_break;
5459      } else {
5460        switch_break: /* CIL Label */ ;
5461      }
5462      }
5463    }
5464  }
5465  while_break: /* CIL Label */ ;
5466  }
5467  ldv_module_exit: 
5468  {
5469#line 515
5470  ldv_check_final_state();
5471  }
5472#line 518
5473  return;
5474}
5475}
5476#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
5477void ldv_blast_assert(void) 
5478{ 
5479
5480  {
5481  ERROR: 
5482#line 6
5483  goto ERROR;
5484}
5485}
5486#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
5487extern int __VERIFIER_nondet_int(void) ;
5488#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5489int ldv_mutex  =    1;
5490#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5491int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) 
5492{ int nondetermined ;
5493
5494  {
5495#line 29
5496  if (ldv_mutex == 1) {
5497
5498  } else {
5499    {
5500#line 29
5501    ldv_blast_assert();
5502    }
5503  }
5504  {
5505#line 32
5506  nondetermined = __VERIFIER_nondet_int();
5507  }
5508#line 35
5509  if (nondetermined) {
5510#line 38
5511    ldv_mutex = 2;
5512#line 40
5513    return (0);
5514  } else {
5515#line 45
5516    return (-4);
5517  }
5518}
5519}
5520#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5521int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) 
5522{ int nondetermined ;
5523
5524  {
5525#line 57
5526  if (ldv_mutex == 1) {
5527
5528  } else {
5529    {
5530#line 57
5531    ldv_blast_assert();
5532    }
5533  }
5534  {
5535#line 60
5536  nondetermined = __VERIFIER_nondet_int();
5537  }
5538#line 63
5539  if (nondetermined) {
5540#line 66
5541    ldv_mutex = 2;
5542#line 68
5543    return (0);
5544  } else {
5545#line 73
5546    return (-4);
5547  }
5548}
5549}
5550#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5551int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) 
5552{ int atomic_value_after_dec ;
5553
5554  {
5555#line 83
5556  if (ldv_mutex == 1) {
5557
5558  } else {
5559    {
5560#line 83
5561    ldv_blast_assert();
5562    }
5563  }
5564  {
5565#line 86
5566  atomic_value_after_dec = __VERIFIER_nondet_int();
5567  }
5568#line 89
5569  if (atomic_value_after_dec == 0) {
5570#line 92
5571    ldv_mutex = 2;
5572#line 94
5573    return (1);
5574  } else {
5575
5576  }
5577#line 98
5578  return (0);
5579}
5580}
5581#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5582void mutex_lock(struct mutex *lock ) 
5583{ 
5584
5585  {
5586#line 108
5587  if (ldv_mutex == 1) {
5588
5589  } else {
5590    {
5591#line 108
5592    ldv_blast_assert();
5593    }
5594  }
5595#line 110
5596  ldv_mutex = 2;
5597#line 111
5598  return;
5599}
5600}
5601#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5602int mutex_trylock(struct mutex *lock ) 
5603{ int nondetermined ;
5604
5605  {
5606#line 121
5607  if (ldv_mutex == 1) {
5608
5609  } else {
5610    {
5611#line 121
5612    ldv_blast_assert();
5613    }
5614  }
5615  {
5616#line 124
5617  nondetermined = __VERIFIER_nondet_int();
5618  }
5619#line 127
5620  if (nondetermined) {
5621#line 130
5622    ldv_mutex = 2;
5623#line 132
5624    return (1);
5625  } else {
5626#line 137
5627    return (0);
5628  }
5629}
5630}
5631#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5632void mutex_unlock(struct mutex *lock ) 
5633{ 
5634
5635  {
5636#line 147
5637  if (ldv_mutex == 2) {
5638
5639  } else {
5640    {
5641#line 147
5642    ldv_blast_assert();
5643    }
5644  }
5645#line 149
5646  ldv_mutex = 1;
5647#line 150
5648  return;
5649}
5650}
5651#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5652void ldv_check_final_state(void) 
5653{ 
5654
5655  {
5656#line 156
5657  if (ldv_mutex == 1) {
5658
5659  } else {
5660    {
5661#line 156
5662    ldv_blast_assert();
5663    }
5664  }
5665#line 157
5666  return;
5667}
5668}
5669#line 527 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4744/dscv_tempdir/dscv/ri/32_1/drivers/misc/eeprom/eeprom_93xx46.c.common.c"
5670long s__builtin_expect(long val , long res ) 
5671{ 
5672
5673  {
5674#line 528
5675  return (val);
5676}
5677}