ClabureDB

1/* Generated by CIL v. 1.3.7 */ 2/* print_CIL_Input is true */ 3 4#line 20 "include/asm-generic/int-ll64.h" 5typedef unsigned char __u8; 6#line 23 "include/asm-generic/int-ll64.h" 7typedef unsigned short __u16; 8#line 25 "include/asm-generic/int-ll64.h" 9typedef int __s32; 10#line 26 "include/asm-generic/int-ll64.h" 11typedef unsigned int __u32; 12#line 30 "include/asm-generic/int-ll64.h" 13typedef unsigned long long __u64; 14#line 43 "include/asm-generic/int-ll64.h" 15typedef unsigned char u8; 16#line 45 "include/asm-generic/int-ll64.h" 17typedef short s16; 18#line 46 "include/asm-generic/int-ll64.h" 19typedef unsigned short u16; 20#line 48 "include/asm-generic/int-ll64.h" 21typedef int s32; 22#line 49 "include/asm-generic/int-ll64.h" 23typedef unsigned int u32; 24#line 51 "include/asm-generic/int-ll64.h" 25typedef long long s64; 26#line 52 "include/asm-generic/int-ll64.h" 27typedef unsigned long long u64; 28#line 14 "include/asm-generic/posix_types.h" 29typedef long __kernel_long_t; 30#line 15 "include/asm-generic/posix_types.h" 31typedef unsigned long __kernel_ulong_t; 32#line 31 "include/asm-generic/posix_types.h" 33typedef int __kernel_pid_t; 34#line 52 "include/asm-generic/posix_types.h" 35typedef unsigned int __kernel_uid32_t; 36#line 53 "include/asm-generic/posix_types.h" 37typedef unsigned int __kernel_gid32_t; 38#line 75 "include/asm-generic/posix_types.h" 39typedef __kernel_ulong_t __kernel_size_t; 40#line 76 "include/asm-generic/posix_types.h" 41typedef __kernel_long_t __kernel_ssize_t; 42#line 91 "include/asm-generic/posix_types.h" 43typedef long long __kernel_loff_t; 44#line 92 "include/asm-generic/posix_types.h" 45typedef __kernel_long_t __kernel_time_t; 46#line 93 "include/asm-generic/posix_types.h" 47typedef __kernel_long_t __kernel_clock_t; 48#line 94 "include/asm-generic/posix_types.h" 49typedef int __kernel_timer_t; 50#line 95 "include/asm-generic/posix_types.h" 51typedef int __kernel_clockid_t; 52#line 21 "include/linux/types.h" 53typedef __u32 __kernel_dev_t; 54#line 24 "include/linux/types.h" 55typedef __kernel_dev_t dev_t; 56#line 27 "include/linux/types.h" 57typedef unsigned short umode_t; 58#line 30 "include/linux/types.h" 59typedef __kernel_pid_t pid_t; 60#line 35 "include/linux/types.h" 61typedef __kernel_clockid_t clockid_t; 62#line 38 "include/linux/types.h" 63typedef _Bool bool; 64#line 40 "include/linux/types.h" 65typedef __kernel_uid32_t uid_t; 66#line 41 "include/linux/types.h" 67typedef __kernel_gid32_t gid_t; 68#line 54 "include/linux/types.h" 69typedef __kernel_loff_t loff_t; 70#line 63 "include/linux/types.h" 71typedef __kernel_size_t size_t; 72#line 68 "include/linux/types.h" 73typedef __kernel_ssize_t ssize_t; 74#line 78 "include/linux/types.h" 75typedef __kernel_time_t time_t; 76#line 111 "include/linux/types.h" 77typedef __s32 int32_t; 78#line 117 "include/linux/types.h" 79typedef __u32 uint32_t; 80#line 202 "include/linux/types.h" 81typedef unsigned int gfp_t; 82#line 221 "include/linux/types.h" 83struct __anonstruct_atomic_t_6 { 84 int counter ; 85}; 86#line 221 "include/linux/types.h" 87typedef struct __anonstruct_atomic_t_6 atomic_t; 88#line 226 "include/linux/types.h" 89struct __anonstruct_atomic64_t_7 { 90 long counter ; 91}; 92#line 226 "include/linux/types.h" 93typedef struct __anonstruct_atomic64_t_7 atomic64_t; 94#line 227 "include/linux/types.h" 95struct list_head { 96 struct list_head *next ; 97 struct list_head *prev ; 98}; 99#line 232 100struct hlist_node; 101#line 232 "include/linux/types.h" 102struct hlist_head { 103 struct hlist_node *first ; 104}; 105#line 236 "include/linux/types.h" 106struct hlist_node { 107 struct hlist_node *next ; 108 struct hlist_node **pprev ; 109}; 110#line 247 "include/linux/types.h" 111struct rcu_head { 112 struct rcu_head *next ; 113 void (*func)(struct rcu_head * ) ; 114}; 115#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h" 116struct module; 117#line 55 118struct module; 119#line 146 "include/linux/init.h" 120typedef void (*ctor_fn_t)(void); 121#line 305 "include/linux/printk.h" 122struct _ddebug { 123 char const *modname ; 124 char const *function ; 125 char const *filename ; 126 char const *format ; 127 unsigned int lineno : 18 ; 128 unsigned char flags ; 129}; 130#line 46 "include/linux/dynamic_debug.h" 131struct device; 132#line 46 133struct device; 134#line 57 135struct completion; 136#line 57 137struct completion; 138#line 58 139struct pt_regs; 140#line 58 141struct pt_regs; 142#line 348 "include/linux/kernel.h" 143struct pid; 144#line 348 145struct pid; 146#line 112 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/stat.h" 147struct timespec; 148#line 112 149struct timespec; 150#line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h" 151struct page; 152#line 58 153struct page; 154#line 26 "include/asm-generic/getorder.h" 155struct task_struct; 156#line 26 157struct task_struct; 158#line 28 159struct mm_struct; 160#line 28 161struct mm_struct; 162#line 268 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/segment.h" 163struct pt_regs { 164 unsigned long r15 ; 165 unsigned long r14 ; 166 unsigned long r13 ; 167 unsigned long r12 ; 168 unsigned long bp ; 169 unsigned long bx ; 170 unsigned long r11 ; 171 unsigned long r10 ; 172 unsigned long r9 ; 173 unsigned long r8 ; 174 unsigned long ax ; 175 unsigned long cx ; 176 unsigned long dx ; 177 unsigned long si ; 178 unsigned long di ; 179 unsigned long orig_ax ; 180 unsigned long ip ; 181 unsigned long cs ; 182 unsigned long flags ; 183 unsigned long sp ; 184 unsigned long ss ; 185}; 186#line 125 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h" 187struct __anonstruct_ldv_2180_13 { 188 unsigned int a ; 189 unsigned int b ; 190}; 191#line 125 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h" 192struct __anonstruct_ldv_2195_14 { 193 u16 limit0 ; 194 u16 base0 ; 195 unsigned char base1 ; 196 unsigned char type : 4 ; 197 unsigned char s : 1 ; 198 unsigned char dpl : 2 ; 199 unsigned char p : 1 ; 200 unsigned char limit : 4 ; 201 unsigned char avl : 1 ; 202 unsigned char l : 1 ; 203 unsigned char d : 1 ; 204 unsigned char g : 1 ; 205 unsigned char base2 ; 206}; 207#line 125 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h" 208union __anonunion_ldv_2196_12 { 209 struct __anonstruct_ldv_2180_13 ldv_2180 ; 210 struct __anonstruct_ldv_2195_14 ldv_2195 ; 211}; 212#line 125 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h" 213struct desc_struct { 214 union __anonunion_ldv_2196_12 ldv_2196 ; 215}; 216#line 13 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h" 217typedef unsigned long pgdval_t; 218#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h" 219typedef unsigned long pgprotval_t; 220#line 18 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h" 221struct pgprot { 222 pgprotval_t pgprot ; 223}; 224#line 192 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h" 225typedef struct pgprot pgprot_t; 226#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h" 227struct __anonstruct_pgd_t_16 { 228 pgdval_t pgd ; 229}; 230#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h" 231typedef struct __anonstruct_pgd_t_16 pgd_t; 232#line 282 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h" 233typedef struct page *pgtable_t; 234#line 290 235struct file; 236#line 290 237struct file; 238#line 337 239struct thread_struct; 240#line 337 241struct thread_struct; 242#line 339 243struct cpumask; 244#line 339 245struct cpumask; 246#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h" 247struct arch_spinlock; 248#line 327 249struct arch_spinlock; 250#line 300 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h" 251struct kernel_vm86_regs { 252 struct pt_regs pt ; 253 unsigned short es ; 254 unsigned short __esh ; 255 unsigned short ds ; 256 unsigned short __dsh ; 257 unsigned short fs ; 258 unsigned short __fsh ; 259 unsigned short gs ; 260 unsigned short __gsh ; 261}; 262#line 203 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/vm86.h" 263union __anonunion_ldv_2824_19 { 264 struct pt_regs *regs ; 265 struct kernel_vm86_regs *vm86 ; 266}; 267#line 203 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/vm86.h" 268struct math_emu_info { 269 long ___orig_eip ; 270 union __anonunion_ldv_2824_19 ldv_2824 ; 271}; 272#line 306 "include/linux/bitmap.h" 273struct bug_entry { 274 int bug_addr_disp ; 275 int file_disp ; 276 unsigned short line ; 277 unsigned short flags ; 278}; 279#line 89 "include/linux/bug.h" 280struct cpumask { 281 unsigned long bits[64U] ; 282}; 283#line 14 "include/linux/cpumask.h" 284typedef struct cpumask cpumask_t; 285#line 637 "include/linux/cpumask.h" 286typedef struct cpumask *cpumask_var_t; 287#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h" 288struct static_key; 289#line 234 290struct static_key; 291#line 287 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h" 292struct i387_fsave_struct { 293 u32 cwd ; 294 u32 swd ; 295 u32 twd ; 296 u32 fip ; 297 u32 fcs ; 298 u32 foo ; 299 u32 fos ; 300 u32 st_space[20U] ; 301 u32 status ; 302}; 303#line 305 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h" 304struct __anonstruct_ldv_5180_24 { 305 u64 rip ; 306 u64 rdp ; 307}; 308#line 305 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h" 309struct __anonstruct_ldv_5186_25 { 310 u32 fip ; 311 u32 fcs ; 312 u32 foo ; 313 u32 fos ; 314}; 315#line 305 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h" 316union __anonunion_ldv_5187_23 { 317 struct __anonstruct_ldv_5180_24 ldv_5180 ; 318 struct __anonstruct_ldv_5186_25 ldv_5186 ; 319}; 320#line 305 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h" 321union __anonunion_ldv_5196_26 { 322 u32 padding1[12U] ; 323 u32 sw_reserved[12U] ; 324}; 325#line 305 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h" 326struct i387_fxsave_struct { 327 u16 cwd ; 328 u16 swd ; 329 u16 twd ; 330 u16 fop ; 331 union __anonunion_ldv_5187_23 ldv_5187 ; 332 u32 mxcsr ; 333 u32 mxcsr_mask ; 334 u32 st_space[32U] ; 335 u32 xmm_space[64U] ; 336 u32 padding[12U] ; 337 union __anonunion_ldv_5196_26 ldv_5196 ; 338}; 339#line 339 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h" 340struct i387_soft_struct { 341 u32 cwd ; 342 u32 swd ; 343 u32 twd ; 344 u32 fip ; 345 u32 fcs ; 346 u32 foo ; 347 u32 fos ; 348 u32 st_space[20U] ; 349 u8 ftop ; 350 u8 changed ; 351 u8 lookahead ; 352 u8 no_update ; 353 u8 rm ; 354 u8 alimit ; 355 struct math_emu_info *info ; 356 u32 entry_eip ; 357}; 358#line 360 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h" 359struct ymmh_struct { 360 u32 ymmh_space[64U] ; 361}; 362#line 365 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h" 363struct xsave_hdr_struct { 364 u64 xstate_bv ; 365 u64 reserved1[2U] ; 366 u64 reserved2[5U] ; 367}; 368#line 371 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h" 369struct xsave_struct { 370 struct i387_fxsave_struct i387 ; 371 struct xsave_hdr_struct xsave_hdr ; 372 struct ymmh_struct ymmh ; 373}; 374#line 377 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h" 375union thread_xstate { 376 struct i387_fsave_struct fsave ; 377 struct i387_fxsave_struct fxsave ; 378 struct i387_soft_struct soft ; 379 struct xsave_struct xsave ; 380}; 381#line 385 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h" 382struct fpu { 383 unsigned int last_cpu ; 384 unsigned int has_fpu ; 385 union thread_xstate *state ; 386}; 387#line 433 388struct kmem_cache; 389#line 434 390struct perf_event; 391#line 434 392struct perf_event; 393#line 435 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h" 394struct thread_struct { 395 struct desc_struct tls_array[3U] ; 396 unsigned long sp0 ; 397 unsigned long sp ; 398 unsigned long usersp ; 399 unsigned short es ; 400 unsigned short ds ; 401 unsigned short fsindex ; 402 unsigned short gsindex ; 403 unsigned long fs ; 404 unsigned long gs ; 405 struct perf_event *ptrace_bps[4U] ; 406 unsigned long debugreg6 ; 407 unsigned long ptrace_dr7 ; 408 unsigned long cr2 ; 409 unsigned long trap_nr ; 410 unsigned long error_code ; 411 struct fpu fpu ; 412 unsigned long *io_bitmap_ptr ; 413 unsigned long iopl ; 414 unsigned int io_bitmap_max ; 415}; 416#line 23 "include/asm-generic/atomic-long.h" 417typedef atomic64_t atomic_long_t; 418#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h" 419typedef u16 __ticket_t; 420#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h" 421typedef u32 __ticketpair_t; 422#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h" 423struct __raw_tickets { 424 __ticket_t head ; 425 __ticket_t tail ; 426}; 427#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h" 428union __anonunion_ldv_5907_29 { 429 __ticketpair_t head_tail ; 430 struct __raw_tickets tickets ; 431}; 432#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h" 433struct arch_spinlock { 434 union __anonunion_ldv_5907_29 ldv_5907 ; 435}; 436#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h" 437typedef struct arch_spinlock arch_spinlock_t; 438#line 34 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h" 439struct lockdep_map; 440#line 34 441struct lockdep_map; 442#line 55 "include/linux/debug_locks.h" 443struct stack_trace { 444 unsigned int nr_entries ; 445 unsigned int max_entries ; 446 unsigned long *entries ; 447 int skip ; 448}; 449#line 26 "include/linux/stacktrace.h" 450struct lockdep_subclass_key { 451 char __one_byte ; 452}; 453#line 53 "include/linux/lockdep.h" 454struct lock_class_key { 455 struct lockdep_subclass_key subkeys[8U] ; 456}; 457#line 59 "include/linux/lockdep.h" 458struct lock_class { 459 struct list_head hash_entry ; 460 struct list_head lock_entry ; 461 struct lockdep_subclass_key *key ; 462 unsigned int subclass ; 463 unsigned int dep_gen_id ; 464 unsigned long usage_mask ; 465 struct stack_trace usage_traces[13U] ; 466 struct list_head locks_after ; 467 struct list_head locks_before ; 468 unsigned int version ; 469 unsigned long ops ; 470 char const *name ; 471 int name_version ; 472 unsigned long contention_point[4U] ; 473 unsigned long contending_point[4U] ; 474}; 475#line 144 "include/linux/lockdep.h" 476struct lockdep_map { 477 struct lock_class_key *key ; 478 struct lock_class *class_cache[2U] ; 479 char const *name ; 480 int cpu ; 481 unsigned long ip ; 482}; 483#line 187 "include/linux/lockdep.h" 484struct held_lock { 485 u64 prev_chain_key ; 486 unsigned long acquire_ip ; 487 struct lockdep_map *instance ; 488 struct lockdep_map *nest_lock ; 489 u64 waittime_stamp ; 490 u64 holdtime_stamp ; 491 unsigned short class_idx : 13 ; 492 unsigned char irq_context : 2 ; 493 unsigned char trylock : 1 ; 494 unsigned char read : 2 ; 495 unsigned char check : 2 ; 496 unsigned char hardirqs_off : 1 ; 497 unsigned short references : 11 ; 498}; 499#line 556 "include/linux/lockdep.h" 500struct raw_spinlock { 501 arch_spinlock_t raw_lock ; 502 unsigned int magic ; 503 unsigned int owner_cpu ; 504 void *owner ; 505 struct lockdep_map dep_map ; 506}; 507#line 32 "include/linux/spinlock_types.h" 508typedef struct raw_spinlock raw_spinlock_t; 509#line 33 "include/linux/spinlock_types.h" 510struct __anonstruct_ldv_6122_33 { 511 u8 __padding[24U] ; 512 struct lockdep_map dep_map ; 513}; 514#line 33 "include/linux/spinlock_types.h" 515union __anonunion_ldv_6123_32 { 516 struct raw_spinlock rlock ; 517 struct __anonstruct_ldv_6122_33 ldv_6122 ; 518}; 519#line 33 "include/linux/spinlock_types.h" 520struct spinlock { 521 union __anonunion_ldv_6123_32 ldv_6123 ; 522}; 523#line 76 "include/linux/spinlock_types.h" 524typedef struct spinlock spinlock_t; 525#line 110 "include/linux/seqlock.h" 526struct seqcount { 527 unsigned int sequence ; 528}; 529#line 121 "include/linux/seqlock.h" 530typedef struct seqcount seqcount_t; 531#line 254 "include/linux/seqlock.h" 532struct timespec { 533 __kernel_time_t tv_sec ; 534 long tv_nsec ; 535}; 536#line 48 "include/linux/wait.h" 537struct __wait_queue_head { 538 spinlock_t lock ; 539 struct list_head task_list ; 540}; 541#line 53 "include/linux/wait.h" 542typedef struct __wait_queue_head wait_queue_head_t; 543#line 98 "include/linux/nodemask.h" 544struct __anonstruct_nodemask_t_36 { 545 unsigned long bits[16U] ; 546}; 547#line 98 "include/linux/nodemask.h" 548typedef struct __anonstruct_nodemask_t_36 nodemask_t; 549#line 670 "include/linux/mmzone.h" 550struct mutex { 551 atomic_t count ; 552 spinlock_t wait_lock ; 553 struct list_head wait_list ; 554 struct task_struct *owner ; 555 char const *name ; 556 void *magic ; 557 struct lockdep_map dep_map ; 558}; 559#line 63 "include/linux/mutex.h" 560struct mutex_waiter { 561 struct list_head list ; 562 struct task_struct *task ; 563 void *magic ; 564}; 565#line 171 566struct rw_semaphore; 567#line 171 568struct rw_semaphore; 569#line 172 "include/linux/mutex.h" 570struct rw_semaphore { 571 long count ; 572 raw_spinlock_t wait_lock ; 573 struct list_head wait_list ; 574 struct lockdep_map dep_map ; 575}; 576#line 128 "include/linux/rwsem.h" 577struct completion { 578 unsigned int done ; 579 wait_queue_head_t wait ; 580}; 581#line 312 "include/linux/jiffies.h" 582union ktime { 583 s64 tv64 ; 584}; 585#line 59 "include/linux/ktime.h" 586typedef union ktime ktime_t; 587#line 341 588struct tvec_base; 589#line 341 590struct tvec_base; 591#line 342 "include/linux/ktime.h" 592struct timer_list { 593 struct list_head entry ; 594 unsigned long expires ; 595 struct tvec_base *base ; 596 void (*function)(unsigned long ) ; 597 unsigned long data ; 598 int slack ; 599 int start_pid ; 600 void *start_site ; 601 char start_comm[16U] ; 602 struct lockdep_map lockdep_map ; 603}; 604#line 289 "include/linux/timer.h" 605struct hrtimer; 606#line 289 607struct hrtimer; 608#line 290 609enum hrtimer_restart; 610#line 302 611struct work_struct; 612#line 302 613struct work_struct; 614#line 45 "include/linux/workqueue.h" 615struct work_struct { 616 atomic_long_t data ; 617 struct list_head entry ; 618 void (*func)(struct work_struct * ) ; 619 struct lockdep_map lockdep_map ; 620}; 621#line 46 "include/linux/pm.h" 622struct pm_message { 623 int event ; 624}; 625#line 52 "include/linux/pm.h" 626typedef struct pm_message pm_message_t; 627#line 53 "include/linux/pm.h" 628struct dev_pm_ops { 629 int (*prepare)(struct device * ) ; 630 void (*complete)(struct device * ) ; 631 int (*suspend)(struct device * ) ; 632 int (*resume)(struct device * ) ; 633 int (*freeze)(struct device * ) ; 634 int (*thaw)(struct device * ) ; 635 int (*poweroff)(struct device * ) ; 636 int (*restore)(struct device * ) ; 637 int (*suspend_late)(struct device * ) ; 638 int (*resume_early)(struct device * ) ; 639 int (*freeze_late)(struct device * ) ; 640 int (*thaw_early)(struct device * ) ; 641 int (*poweroff_late)(struct device * ) ; 642 int (*restore_early)(struct device * ) ; 643 int (*suspend_noirq)(struct device * ) ; 644 int (*resume_noirq)(struct device * ) ; 645 int (*freeze_noirq)(struct device * ) ; 646 int (*thaw_noirq)(struct device * ) ; 647 int (*poweroff_noirq)(struct device * ) ; 648 int (*restore_noirq)(struct device * ) ; 649 int (*runtime_suspend)(struct device * ) ; 650 int (*runtime_resume)(struct device * ) ; 651 int (*runtime_idle)(struct device * ) ; 652}; 653#line 289 654enum rpm_status { 655 RPM_ACTIVE = 0, 656 RPM_RESUMING = 1, 657 RPM_SUSPENDED = 2, 658 RPM_SUSPENDING = 3 659} ; 660#line 296 661enum rpm_request { 662 RPM_REQ_NONE = 0, 663 RPM_REQ_IDLE = 1, 664 RPM_REQ_SUSPEND = 2, 665 RPM_REQ_AUTOSUSPEND = 3, 666 RPM_REQ_RESUME = 4 667} ; 668#line 304 669struct wakeup_source; 670#line 304 671struct wakeup_source; 672#line 494 "include/linux/pm.h" 673struct pm_subsys_data { 674 spinlock_t lock ; 675 unsigned int refcount ; 676}; 677#line 499 678struct dev_pm_qos_request; 679#line 499 680struct pm_qos_constraints; 681#line 499 "include/linux/pm.h" 682struct dev_pm_info { 683 pm_message_t power_state ; 684 unsigned char can_wakeup : 1 ; 685 unsigned char async_suspend : 1 ; 686 bool is_prepared ; 687 bool is_suspended ; 688 bool ignore_children ; 689 spinlock_t lock ; 690 struct list_head entry ; 691 struct completion completion ; 692 struct wakeup_source *wakeup ; 693 bool wakeup_path ; 694 struct timer_list suspend_timer ; 695 unsigned long timer_expires ; 696 struct work_struct work ; 697 wait_queue_head_t wait_queue ; 698 atomic_t usage_count ; 699 atomic_t child_count ; 700 unsigned char disable_depth : 3 ; 701 unsigned char idle_notification : 1 ; 702 unsigned char request_pending : 1 ; 703 unsigned char deferred_resume : 1 ; 704 unsigned char run_wake : 1 ; 705 unsigned char runtime_auto : 1 ; 706 unsigned char no_callbacks : 1 ; 707 unsigned char irq_safe : 1 ; 708 unsigned char use_autosuspend : 1 ; 709 unsigned char timer_autosuspends : 1 ; 710 enum rpm_request request ; 711 enum rpm_status runtime_status ; 712 int runtime_error ; 713 int autosuspend_delay ; 714 unsigned long last_busy ; 715 unsigned long active_jiffies ; 716 unsigned long suspended_jiffies ; 717 unsigned long accounting_timestamp ; 718 ktime_t suspend_time ; 719 s64 max_time_suspended_ns ; 720 struct dev_pm_qos_request *pq_req ; 721 struct pm_subsys_data *subsys_data ; 722 struct pm_qos_constraints *constraints ; 723}; 724#line 558 "include/linux/pm.h" 725struct dev_pm_domain { 726 struct dev_pm_ops ops ; 727}; 728#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h" 729struct __anonstruct_mm_context_t_101 { 730 void *ldt ; 731 int size ; 732 unsigned short ia32_compat ; 733 struct mutex lock ; 734 void *vdso ; 735}; 736#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h" 737typedef struct __anonstruct_mm_context_t_101 mm_context_t; 738#line 18 "include/asm-generic/pci_iomap.h" 739struct vm_area_struct; 740#line 18 741struct vm_area_struct; 742#line 835 "include/linux/sysctl.h" 743struct rb_node { 744 unsigned long rb_parent_color ; 745 struct rb_node *rb_right ; 746 struct rb_node *rb_left ; 747}; 748#line 108 "include/linux/rbtree.h" 749struct rb_root { 750 struct rb_node *rb_node ; 751}; 752#line 176 753struct nsproxy; 754#line 176 755struct nsproxy; 756#line 37 "include/linux/kmod.h" 757struct cred; 758#line 37 759struct cred; 760#line 18 "include/linux/elf.h" 761typedef __u64 Elf64_Addr; 762#line 19 "include/linux/elf.h" 763typedef __u16 Elf64_Half; 764#line 23 "include/linux/elf.h" 765typedef __u32 Elf64_Word; 766#line 24 "include/linux/elf.h" 767typedef __u64 Elf64_Xword; 768#line 193 "include/linux/elf.h" 769struct elf64_sym { 770 Elf64_Word st_name ; 771 unsigned char st_info ; 772 unsigned char st_other ; 773 Elf64_Half st_shndx ; 774 Elf64_Addr st_value ; 775 Elf64_Xword st_size ; 776}; 777#line 201 "include/linux/elf.h" 778typedef struct elf64_sym Elf64_Sym; 779#line 445 780struct sock; 781#line 445 782struct sock; 783#line 446 784struct kobject; 785#line 446 786struct kobject; 787#line 447 788enum kobj_ns_type { 789 KOBJ_NS_TYPE_NONE = 0, 790 KOBJ_NS_TYPE_NET = 1, 791 KOBJ_NS_TYPES = 2 792} ; 793#line 453 "include/linux/elf.h" 794struct kobj_ns_type_operations { 795 enum kobj_ns_type type ; 796 void *(*grab_current_ns)(void) ; 797 void const *(*netlink_ns)(struct sock * ) ; 798 void const *(*initial_ns)(void) ; 799 void (*drop_ns)(void * ) ; 800}; 801#line 57 "include/linux/kobject_ns.h" 802struct attribute { 803 char const *name ; 804 umode_t mode ; 805 struct lock_class_key *key ; 806 struct lock_class_key skey ; 807}; 808#line 33 "include/linux/sysfs.h" 809struct attribute_group { 810 char const *name ; 811 umode_t (*is_visible)(struct kobject * , struct attribute * , int ) ; 812 struct attribute **attrs ; 813}; 814#line 62 "include/linux/sysfs.h" 815struct bin_attribute { 816 struct attribute attr ; 817 size_t size ; 818 void *private ; 819 ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * , 820 loff_t , size_t ) ; 821 ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * , 822 loff_t , size_t ) ; 823 int (*mmap)(struct file * , struct kobject * , struct bin_attribute * , struct vm_area_struct * ) ; 824}; 825#line 98 "include/linux/sysfs.h" 826struct sysfs_ops { 827 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ; 828 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ; 829 void const *(*namespace)(struct kobject * , struct attribute const * ) ; 830}; 831#line 117 832struct sysfs_dirent; 833#line 117 834struct sysfs_dirent; 835#line 182 "include/linux/sysfs.h" 836struct kref { 837 atomic_t refcount ; 838}; 839#line 49 "include/linux/kobject.h" 840struct kset; 841#line 49 842struct kobj_type; 843#line 49 "include/linux/kobject.h" 844struct kobject { 845 char const *name ; 846 struct list_head entry ; 847 struct kobject *parent ; 848 struct kset *kset ; 849 struct kobj_type *ktype ; 850 struct sysfs_dirent *sd ; 851 struct kref kref ; 852 unsigned char state_initialized : 1 ; 853 unsigned char state_in_sysfs : 1 ; 854 unsigned char state_add_uevent_sent : 1 ; 855 unsigned char state_remove_uevent_sent : 1 ; 856 unsigned char uevent_suppress : 1 ; 857}; 858#line 107 "include/linux/kobject.h" 859struct kobj_type { 860 void (*release)(struct kobject * ) ; 861 struct sysfs_ops const *sysfs_ops ; 862 struct attribute **default_attrs ; 863 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject * ) ; 864 void const *(*namespace)(struct kobject * ) ; 865}; 866#line 115 "include/linux/kobject.h" 867struct kobj_uevent_env { 868 char *envp[32U] ; 869 int envp_idx ; 870 char buf[2048U] ; 871 int buflen ; 872}; 873#line 122 "include/linux/kobject.h" 874struct kset_uevent_ops { 875 int (* const filter)(struct kset * , struct kobject * ) ; 876 char const *(* const name)(struct kset * , struct kobject * ) ; 877 int (* const uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ; 878}; 879#line 139 "include/linux/kobject.h" 880struct kset { 881 struct list_head list ; 882 spinlock_t list_lock ; 883 struct kobject kobj ; 884 struct kset_uevent_ops const *uevent_ops ; 885}; 886#line 215 887struct kernel_param; 888#line 215 889struct kernel_param; 890#line 216 "include/linux/kobject.h" 891struct kernel_param_ops { 892 int (*set)(char const * , struct kernel_param const * ) ; 893 int (*get)(char * , struct kernel_param const * ) ; 894 void (*free)(void * ) ; 895}; 896#line 49 "include/linux/moduleparam.h" 897struct kparam_string; 898#line 49 899struct kparam_array; 900#line 49 "include/linux/moduleparam.h" 901union __anonunion_ldv_13363_134 { 902 void *arg ; 903 struct kparam_string const *str ; 904 struct kparam_array const *arr ; 905}; 906#line 49 "include/linux/moduleparam.h" 907struct kernel_param { 908 char const *name ; 909 struct kernel_param_ops const *ops ; 910 u16 perm ; 911 s16 level ; 912 union __anonunion_ldv_13363_134 ldv_13363 ; 913}; 914#line 61 "include/linux/moduleparam.h" 915struct kparam_string { 916 unsigned int maxlen ; 917 char *string ; 918}; 919#line 67 "include/linux/moduleparam.h" 920struct kparam_array { 921 unsigned int max ; 922 unsigned int elemsize ; 923 unsigned int *num ; 924 struct kernel_param_ops const *ops ; 925 void *elem ; 926}; 927#line 458 "include/linux/moduleparam.h" 928struct static_key { 929 atomic_t enabled ; 930}; 931#line 225 "include/linux/jump_label.h" 932struct tracepoint; 933#line 225 934struct tracepoint; 935#line 226 "include/linux/jump_label.h" 936struct tracepoint_func { 937 void *func ; 938 void *data ; 939}; 940#line 29 "include/linux/tracepoint.h" 941struct tracepoint { 942 char const *name ; 943 struct static_key key ; 944 void (*regfunc)(void) ; 945 void (*unregfunc)(void) ; 946 struct tracepoint_func *funcs ; 947}; 948#line 86 "include/linux/tracepoint.h" 949struct kernel_symbol { 950 unsigned long value ; 951 char const *name ; 952}; 953#line 27 "include/linux/export.h" 954struct mod_arch_specific { 955 956}; 957#line 34 "include/linux/module.h" 958struct module_param_attrs; 959#line 34 "include/linux/module.h" 960struct module_kobject { 961 struct kobject kobj ; 962 struct module *mod ; 963 struct kobject *drivers_dir ; 964 struct module_param_attrs *mp ; 965}; 966#line 43 "include/linux/module.h" 967struct module_attribute { 968 struct attribute attr ; 969 ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ; 970 ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const * , 971 size_t ) ; 972 void (*setup)(struct module * , char const * ) ; 973 int (*test)(struct module * ) ; 974 void (*free)(struct module * ) ; 975}; 976#line 69 977struct exception_table_entry; 978#line 69 979struct exception_table_entry; 980#line 198 981enum module_state { 982 MODULE_STATE_LIVE = 0, 983 MODULE_STATE_COMING = 1, 984 MODULE_STATE_GOING = 2 985} ; 986#line 204 "include/linux/module.h" 987struct module_ref { 988 unsigned long incs ; 989 unsigned long decs ; 990}; 991#line 219 992struct module_sect_attrs; 993#line 219 994struct module_notes_attrs; 995#line 219 996struct ftrace_event_call; 997#line 219 "include/linux/module.h" 998struct module { 999 enum module_state state ; 1000 struct list_head list ; 1001 char name[56U] ; 1002 struct module_kobject mkobj ; 1003 struct module_attribute *modinfo_attrs ; 1004 char const *version ; 1005 char const *srcversion ; 1006 struct kobject *holders_dir ; 1007 struct kernel_symbol const *syms ; 1008 unsigned long const *crcs ; 1009 unsigned int num_syms ; 1010 struct kernel_param *kp ; 1011 unsigned int num_kp ; 1012 unsigned int num_gpl_syms ; 1013 struct kernel_symbol const *gpl_syms ; 1014 unsigned long const *gpl_crcs ; 1015 struct kernel_symbol const *unused_syms ; 1016 unsigned long const *unused_crcs ; 1017 unsigned int num_unused_syms ; 1018 unsigned int num_unused_gpl_syms ; 1019 struct kernel_symbol const *unused_gpl_syms ; 1020 unsigned long const *unused_gpl_crcs ; 1021 struct kernel_symbol const *gpl_future_syms ; 1022 unsigned long const *gpl_future_crcs ; 1023 unsigned int num_gpl_future_syms ; 1024 unsigned int num_exentries ; 1025 struct exception_table_entry *extable ; 1026 int (*init)(void) ; 1027 void *module_init ; 1028 void *module_core ; 1029 unsigned int init_size ; 1030 unsigned int core_size ; 1031 unsigned int init_text_size ; 1032 unsigned int core_text_size ; 1033 unsigned int init_ro_size ; 1034 unsigned int core_ro_size ; 1035 struct mod_arch_specific arch ; 1036 unsigned int taints ; 1037 unsigned int num_bugs ; 1038 struct list_head bug_list ; 1039 struct bug_entry *bug_table ; 1040 Elf64_Sym *symtab ; 1041 Elf64_Sym *core_symtab ; 1042 unsigned int num_symtab ; 1043 unsigned int core_num_syms ; 1044 char *strtab ; 1045 char *core_strtab ; 1046 struct module_sect_attrs *sect_attrs ; 1047 struct module_notes_attrs *notes_attrs ; 1048 char *args ; 1049 void *percpu ; 1050 unsigned int percpu_size ; 1051 unsigned int num_tracepoints ; 1052 struct tracepoint * const *tracepoints_ptrs ; 1053 unsigned int num_trace_bprintk_fmt ; 1054 char const **trace_bprintk_fmt_start ; 1055 struct ftrace_event_call **trace_events ; 1056 unsigned int num_trace_events ; 1057 struct list_head source_list ; 1058 struct list_head target_list ; 1059 struct task_struct *waiter ; 1060 void (*exit)(void) ; 1061 struct module_ref *refptr ; 1062 ctor_fn_t (**ctors)(void) ; 1063 unsigned int num_ctors ; 1064}; 1065#line 88 "include/linux/kmemleak.h" 1066struct kmem_cache_cpu { 1067 void **freelist ; 1068 unsigned long tid ; 1069 struct page *page ; 1070 struct page *partial ; 1071 int node ; 1072 unsigned int stat[26U] ; 1073}; 1074#line 55 "include/linux/slub_def.h" 1075struct kmem_cache_node { 1076 spinlock_t list_lock ; 1077 unsigned long nr_partial ; 1078 struct list_head partial ; 1079 atomic_long_t nr_slabs ; 1080 atomic_long_t total_objects ; 1081 struct list_head full ; 1082}; 1083#line 66 "include/linux/slub_def.h" 1084struct kmem_cache_order_objects { 1085 unsigned long x ; 1086}; 1087#line 76 "include/linux/slub_def.h" 1088struct kmem_cache { 1089 struct kmem_cache_cpu *cpu_slab ; 1090 unsigned long flags ; 1091 unsigned long min_partial ; 1092 int size ; 1093 int objsize ; 1094 int offset ; 1095 int cpu_partial ; 1096 struct kmem_cache_order_objects oo ; 1097 struct kmem_cache_order_objects max ; 1098 struct kmem_cache_order_objects min ; 1099 gfp_t allocflags ; 1100 int refcount ; 1101 void (*ctor)(void * ) ; 1102 int inuse ; 1103 int align ; 1104 int reserved ; 1105 char const *name ; 1106 struct list_head list ; 1107 struct kobject kobj ; 1108 int remote_node_defrag_ratio ; 1109 struct kmem_cache_node *node[1024U] ; 1110}; 1111#line 215 "include/linux/mod_devicetable.h" 1112struct of_device_id { 1113 char name[32U] ; 1114 char type[32U] ; 1115 char compatible[128U] ; 1116 void *data ; 1117}; 1118#line 584 1119struct klist_node; 1120#line 584 1121struct klist_node; 1122#line 37 "include/linux/klist.h" 1123struct klist_node { 1124 void *n_klist ; 1125 struct list_head n_node ; 1126 struct kref n_ref ; 1127}; 1128#line 67 1129struct dma_map_ops; 1130#line 67 "include/linux/klist.h" 1131struct dev_archdata { 1132 void *acpi_handle ; 1133 struct dma_map_ops *dma_ops ; 1134 void *iommu ; 1135}; 1136#line 17 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h" 1137struct device_private; 1138#line 17 1139struct device_private; 1140#line 18 1141struct device_driver; 1142#line 18 1143struct device_driver; 1144#line 19 1145struct driver_private; 1146#line 19 1147struct driver_private; 1148#line 20 1149struct class; 1150#line 20 1151struct class; 1152#line 21 1153struct subsys_private; 1154#line 21 1155struct subsys_private; 1156#line 22 1157struct bus_type; 1158#line 22 1159struct bus_type; 1160#line 23 1161struct device_node; 1162#line 23 1163struct device_node; 1164#line 24 1165struct iommu_ops; 1166#line 24 1167struct iommu_ops; 1168#line 25 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h" 1169struct bus_attribute { 1170 struct attribute attr ; 1171 ssize_t (*show)(struct bus_type * , char * ) ; 1172 ssize_t (*store)(struct bus_type * , char const * , size_t ) ; 1173}; 1174#line 51 "include/linux/device.h" 1175struct device_attribute; 1176#line 51 1177struct driver_attribute; 1178#line 51 "include/linux/device.h" 1179struct bus_type { 1180 char const *name ; 1181 char const *dev_name ; 1182 struct device *dev_root ; 1183 struct bus_attribute *bus_attrs ; 1184 struct device_attribute *dev_attrs ; 1185 struct driver_attribute *drv_attrs ; 1186 int (*match)(struct device * , struct device_driver * ) ; 1187 int (*uevent)(struct device * , struct kobj_uevent_env * ) ; 1188 int (*probe)(struct device * ) ; 1189 int (*remove)(struct device * ) ; 1190 void (*shutdown)(struct device * ) ; 1191 int (*suspend)(struct device * , pm_message_t ) ; 1192 int (*resume)(struct device * ) ; 1193 struct dev_pm_ops const *pm ; 1194 struct iommu_ops *iommu_ops ; 1195 struct subsys_private *p ; 1196}; 1197#line 125 1198struct device_type; 1199#line 182 "include/linux/device.h" 1200struct device_driver { 1201 char const *name ; 1202 struct bus_type *bus ; 1203 struct module *owner ; 1204 char const *mod_name ; 1205 bool suppress_bind_attrs ; 1206 struct of_device_id const *of_match_table ; 1207 int (*probe)(struct device * ) ; 1208 int (*remove)(struct device * ) ; 1209 void (*shutdown)(struct device * ) ; 1210 int (*suspend)(struct device * , pm_message_t ) ; 1211 int (*resume)(struct device * ) ; 1212 struct attribute_group const **groups ; 1213 struct dev_pm_ops const *pm ; 1214 struct driver_private *p ; 1215}; 1216#line 245 "include/linux/device.h" 1217struct driver_attribute { 1218 struct attribute attr ; 1219 ssize_t (*show)(struct device_driver * , char * ) ; 1220 ssize_t (*store)(struct device_driver * , char const * , size_t ) ; 1221}; 1222#line 299 1223struct class_attribute; 1224#line 299 "include/linux/device.h" 1225struct class { 1226 char const *name ; 1227 struct module *owner ; 1228 struct class_attribute *class_attrs ; 1229 struct device_attribute *dev_attrs ; 1230 struct bin_attribute *dev_bin_attrs ; 1231 struct kobject *dev_kobj ; 1232 int (*dev_uevent)(struct device * , struct kobj_uevent_env * ) ; 1233 char *(*devnode)(struct device * , umode_t * ) ; 1234 void (*class_release)(struct class * ) ; 1235 void (*dev_release)(struct device * ) ; 1236 int (*suspend)(struct device * , pm_message_t ) ; 1237 int (*resume)(struct device * ) ; 1238 struct kobj_ns_type_operations const *ns_type ; 1239 void const *(*namespace)(struct device * ) ; 1240 struct dev_pm_ops const *pm ; 1241 struct subsys_private *p ; 1242}; 1243#line 394 "include/linux/device.h" 1244struct class_attribute { 1245 struct attribute attr ; 1246 ssize_t (*show)(struct class * , struct class_attribute * , char * ) ; 1247 ssize_t (*store)(struct class * , struct class_attribute * , char const * , size_t ) ; 1248 void const *(*namespace)(struct class * , struct class_attribute const * ) ; 1249}; 1250#line 447 "include/linux/device.h" 1251struct device_type { 1252 char const *name ; 1253 struct attribute_group const **groups ; 1254 int (*uevent)(struct device * , struct kobj_uevent_env * ) ; 1255 char *(*devnode)(struct device * , umode_t * ) ; 1256 void (*release)(struct device * ) ; 1257 struct dev_pm_ops const *pm ; 1258}; 1259#line 474 "include/linux/device.h" 1260struct device_attribute { 1261 struct attribute attr ; 1262 ssize_t (*show)(struct device * , struct device_attribute * , char * ) ; 1263 ssize_t (*store)(struct device * , struct device_attribute * , char const * , 1264 size_t ) ; 1265}; 1266#line 557 "include/linux/device.h" 1267struct device_dma_parameters { 1268 unsigned int max_segment_size ; 1269 unsigned long segment_boundary_mask ; 1270}; 1271#line 567 1272struct dma_coherent_mem; 1273#line 567 "include/linux/device.h" 1274struct device { 1275 struct device *parent ; 1276 struct device_private *p ; 1277 struct kobject kobj ; 1278 char const *init_name ; 1279 struct device_type const *type ; 1280 struct mutex mutex ; 1281 struct bus_type *bus ; 1282 struct device_driver *driver ; 1283 void *platform_data ; 1284 struct dev_pm_info power ; 1285 struct dev_pm_domain *pm_domain ; 1286 int numa_node ; 1287 u64 *dma_mask ; 1288 u64 coherent_dma_mask ; 1289 struct device_dma_parameters *dma_parms ; 1290 struct list_head dma_pools ; 1291 struct dma_coherent_mem *dma_mem ; 1292 struct dev_archdata archdata ; 1293 struct device_node *of_node ; 1294 dev_t devt ; 1295 u32 id ; 1296 spinlock_t devres_lock ; 1297 struct list_head devres_head ; 1298 struct klist_node knode_class ; 1299 struct class *class ; 1300 struct attribute_group const **groups ; 1301 void (*release)(struct device * ) ; 1302}; 1303#line 681 "include/linux/device.h" 1304struct wakeup_source { 1305 char const *name ; 1306 struct list_head entry ; 1307 spinlock_t lock ; 1308 struct timer_list timer ; 1309 unsigned long timer_expires ; 1310 ktime_t total_time ; 1311 ktime_t max_time ; 1312 ktime_t last_time ; 1313 unsigned long event_count ; 1314 unsigned long active_count ; 1315 unsigned long relax_count ; 1316 unsigned long hit_count ; 1317 unsigned char active : 1 ; 1318}; 1319#line 93 "include/linux/capability.h" 1320struct kernel_cap_struct { 1321 __u32 cap[2U] ; 1322}; 1323#line 96 "include/linux/capability.h" 1324typedef struct kernel_cap_struct kernel_cap_t; 1325#line 105 1326struct user_namespace; 1327#line 105 1328struct user_namespace; 1329#line 554 1330struct prio_tree_node; 1331#line 554 "include/linux/capability.h" 1332struct raw_prio_tree_node { 1333 struct prio_tree_node *left ; 1334 struct prio_tree_node *right ; 1335 struct prio_tree_node *parent ; 1336}; 1337#line 19 "include/linux/prio_tree.h" 1338struct prio_tree_node { 1339 struct prio_tree_node *left ; 1340 struct prio_tree_node *right ; 1341 struct prio_tree_node *parent ; 1342 unsigned long start ; 1343 unsigned long last ; 1344}; 1345#line 116 1346struct address_space; 1347#line 116 1348struct address_space; 1349#line 117 "include/linux/prio_tree.h" 1350union __anonunion_ldv_15299_138 { 1351 unsigned long index ; 1352 void *freelist ; 1353}; 1354#line 117 "include/linux/prio_tree.h" 1355struct __anonstruct_ldv_15309_142 { 1356 unsigned short inuse ; 1357 unsigned short objects : 15 ; 1358 unsigned char frozen : 1 ; 1359}; 1360#line 117 "include/linux/prio_tree.h" 1361union __anonunion_ldv_15310_141 { 1362 atomic_t _mapcount ; 1363 struct __anonstruct_ldv_15309_142 ldv_15309 ; 1364}; 1365#line 117 "include/linux/prio_tree.h" 1366struct __anonstruct_ldv_15312_140 { 1367 union __anonunion_ldv_15310_141 ldv_15310 ; 1368 atomic_t _count ; 1369}; 1370#line 117 "include/linux/prio_tree.h" 1371union __anonunion_ldv_15313_139 { 1372 unsigned long counters ; 1373 struct __anonstruct_ldv_15312_140 ldv_15312 ; 1374}; 1375#line 117 "include/linux/prio_tree.h" 1376struct __anonstruct_ldv_15314_137 { 1377 union __anonunion_ldv_15299_138 ldv_15299 ; 1378 union __anonunion_ldv_15313_139 ldv_15313 ; 1379}; 1380#line 117 "include/linux/prio_tree.h" 1381struct __anonstruct_ldv_15321_144 { 1382 struct page *next ; 1383 int pages ; 1384 int pobjects ; 1385}; 1386#line 117 "include/linux/prio_tree.h" 1387union __anonunion_ldv_15322_143 { 1388 struct list_head lru ; 1389 struct __anonstruct_ldv_15321_144 ldv_15321 ; 1390}; 1391#line 117 "include/linux/prio_tree.h" 1392union __anonunion_ldv_15327_145 { 1393 unsigned long private ; 1394 struct kmem_cache *slab ; 1395 struct page *first_page ; 1396}; 1397#line 117 "include/linux/prio_tree.h" 1398struct page { 1399 unsigned long flags ; 1400 struct address_space *mapping ; 1401 struct __anonstruct_ldv_15314_137 ldv_15314 ; 1402 union __anonunion_ldv_15322_143 ldv_15322 ; 1403 union __anonunion_ldv_15327_145 ldv_15327 ; 1404 unsigned long debug_flags ; 1405}; 1406#line 192 "include/linux/mm_types.h" 1407struct __anonstruct_vm_set_147 { 1408 struct list_head list ; 1409 void *parent ; 1410 struct vm_area_struct *head ; 1411}; 1412#line 192 "include/linux/mm_types.h" 1413union __anonunion_shared_146 { 1414 struct __anonstruct_vm_set_147 vm_set ; 1415 struct raw_prio_tree_node prio_tree_node ; 1416}; 1417#line 192 1418struct anon_vma; 1419#line 192 1420struct vm_operations_struct; 1421#line 192 1422struct mempolicy; 1423#line 192 "include/linux/mm_types.h" 1424struct vm_area_struct { 1425 struct mm_struct *vm_mm ; 1426 unsigned long vm_start ; 1427 unsigned long vm_end ; 1428 struct vm_area_struct *vm_next ; 1429 struct vm_area_struct *vm_prev ; 1430 pgprot_t vm_page_prot ; 1431 unsigned long vm_flags ; 1432 struct rb_node vm_rb ; 1433 union __anonunion_shared_146 shared ; 1434 struct list_head anon_vma_chain ; 1435 struct anon_vma *anon_vma ; 1436 struct vm_operations_struct const *vm_ops ; 1437 unsigned long vm_pgoff ; 1438 struct file *vm_file ; 1439 void *vm_private_data ; 1440 struct mempolicy *vm_policy ; 1441}; 1442#line 255 "include/linux/mm_types.h" 1443struct core_thread { 1444 struct task_struct *task ; 1445 struct core_thread *next ; 1446}; 1447#line 261 "include/linux/mm_types.h" 1448struct core_state { 1449 atomic_t nr_threads ; 1450 struct core_thread dumper ; 1451 struct completion startup ; 1452}; 1453#line 274 "include/linux/mm_types.h" 1454struct mm_rss_stat { 1455 atomic_long_t count[3U] ; 1456}; 1457#line 287 1458struct linux_binfmt; 1459#line 287 1460struct mmu_notifier_mm; 1461#line 287 "include/linux/mm_types.h" 1462struct mm_struct { 1463 struct vm_area_struct *mmap ; 1464 struct rb_root mm_rb ; 1465 struct vm_area_struct *mmap_cache ; 1466 unsigned long (*get_unmapped_area)(struct file * , unsigned long , unsigned long , 1467 unsigned long , unsigned long ) ; 1468 void (*unmap_area)(struct mm_struct * , unsigned long ) ; 1469 unsigned long mmap_base ; 1470 unsigned long task_size ; 1471 unsigned long cached_hole_size ; 1472 unsigned long free_area_cache ; 1473 pgd_t *pgd ; 1474 atomic_t mm_users ; 1475 atomic_t mm_count ; 1476 int map_count ; 1477 spinlock_t page_table_lock ; 1478 struct rw_semaphore mmap_sem ; 1479 struct list_head mmlist ; 1480 unsigned long hiwater_rss ; 1481 unsigned long hiwater_vm ; 1482 unsigned long total_vm ; 1483 unsigned long locked_vm ; 1484 unsigned long pinned_vm ; 1485 unsigned long shared_vm ; 1486 unsigned long exec_vm ; 1487 unsigned long stack_vm ; 1488 unsigned long reserved_vm ; 1489 unsigned long def_flags ; 1490 unsigned long nr_ptes ; 1491 unsigned long start_code ; 1492 unsigned long end_code ; 1493 unsigned long start_data ; 1494 unsigned long end_data ; 1495 unsigned long start_brk ; 1496 unsigned long brk ; 1497 unsigned long start_stack ; 1498 unsigned long arg_start ; 1499 unsigned long arg_end ; 1500 unsigned long env_start ; 1501 unsigned long env_end ; 1502 unsigned long saved_auxv[44U] ; 1503 struct mm_rss_stat rss_stat ; 1504 struct linux_binfmt *binfmt ; 1505 cpumask_var_t cpu_vm_mask_var ; 1506 mm_context_t context ; 1507 unsigned int faultstamp ; 1508 unsigned int token_priority ; 1509 unsigned int last_interval ; 1510 unsigned long flags ; 1511 struct core_state *core_state ; 1512 spinlock_t ioctx_lock ; 1513 struct hlist_head ioctx_list ; 1514 struct task_struct *owner ; 1515 struct file *exe_file ; 1516 unsigned long num_exe_file_vmas ; 1517 struct mmu_notifier_mm *mmu_notifier_mm ; 1518 pgtable_t pmd_huge_pte ; 1519 struct cpumask cpumask_allocation ; 1520}; 1521#line 7 "include/asm-generic/cputime.h" 1522typedef unsigned long cputime_t; 1523#line 98 "include/linux/sem.h" 1524struct sem_undo_list; 1525#line 98 "include/linux/sem.h" 1526struct sysv_sem { 1527 struct sem_undo_list *undo_list ; 1528}; 1529#line 107 1530struct siginfo; 1531#line 107 1532struct siginfo; 1533#line 32 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h" 1534struct __anonstruct_sigset_t_148 { 1535 unsigned long sig[1U] ; 1536}; 1537#line 32 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h" 1538typedef struct __anonstruct_sigset_t_148 sigset_t; 1539#line 17 "include/asm-generic/signal-defs.h" 1540typedef void __signalfn_t(int ); 1541#line 18 "include/asm-generic/signal-defs.h" 1542typedef __signalfn_t *__sighandler_t; 1543#line 20 "include/asm-generic/signal-defs.h" 1544typedef void __restorefn_t(void); 1545#line 21 "include/asm-generic/signal-defs.h" 1546typedef __restorefn_t *__sigrestore_t; 1547#line 126 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h" 1548struct sigaction { 1549 __sighandler_t sa_handler ; 1550 unsigned long sa_flags ; 1551 __sigrestore_t sa_restorer ; 1552 sigset_t sa_mask ; 1553}; 1554#line 173 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h" 1555struct k_sigaction { 1556 struct sigaction sa ; 1557}; 1558#line 185 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h" 1559union sigval { 1560 int sival_int ; 1561 void *sival_ptr ; 1562}; 1563#line 10 "include/asm-generic/siginfo.h" 1564typedef union sigval sigval_t; 1565#line 11 "include/asm-generic/siginfo.h" 1566struct __anonstruct__kill_150 { 1567 __kernel_pid_t _pid ; 1568 __kernel_uid32_t _uid ; 1569}; 1570#line 11 "include/asm-generic/siginfo.h" 1571struct __anonstruct__timer_151 { 1572 __kernel_timer_t _tid ; 1573 int _overrun ; 1574 char _pad[0U] ; 1575 sigval_t _sigval ; 1576 int _sys_private ; 1577}; 1578#line 11 "include/asm-generic/siginfo.h" 1579struct __anonstruct__rt_152 { 1580 __kernel_pid_t _pid ; 1581 __kernel_uid32_t _uid ; 1582 sigval_t _sigval ; 1583}; 1584#line 11 "include/asm-generic/siginfo.h" 1585struct __anonstruct__sigchld_153 { 1586 __kernel_pid_t _pid ; 1587 __kernel_uid32_t _uid ; 1588 int _status ; 1589 __kernel_clock_t _utime ; 1590 __kernel_clock_t _stime ; 1591}; 1592#line 11 "include/asm-generic/siginfo.h" 1593struct __anonstruct__sigfault_154 { 1594 void *_addr ; 1595 short _addr_lsb ; 1596}; 1597#line 11 "include/asm-generic/siginfo.h" 1598struct __anonstruct__sigpoll_155 { 1599 long _band ; 1600 int _fd ; 1601}; 1602#line 11 "include/asm-generic/siginfo.h" 1603union __anonunion__sifields_149 { 1604 int _pad[28U] ; 1605 struct __anonstruct__kill_150 _kill ; 1606 struct __anonstruct__timer_151 _timer ; 1607 struct __anonstruct__rt_152 _rt ; 1608 struct __anonstruct__sigchld_153 _sigchld ; 1609 struct __anonstruct__sigfault_154 _sigfault ; 1610 struct __anonstruct__sigpoll_155 _sigpoll ; 1611}; 1612#line 11 "include/asm-generic/siginfo.h" 1613struct siginfo { 1614 int si_signo ; 1615 int si_errno ; 1616 int si_code ; 1617 union __anonunion__sifields_149 _sifields ; 1618}; 1619#line 102 "include/asm-generic/siginfo.h" 1620typedef struct siginfo siginfo_t; 1621#line 14 "include/linux/signal.h" 1622struct user_struct; 1623#line 24 "include/linux/signal.h" 1624struct sigpending { 1625 struct list_head list ; 1626 sigset_t signal ; 1627}; 1628#line 395 1629struct pid_namespace; 1630#line 395 "include/linux/signal.h" 1631struct upid { 1632 int nr ; 1633 struct pid_namespace *ns ; 1634 struct hlist_node pid_chain ; 1635}; 1636#line 56 "include/linux/pid.h" 1637struct pid { 1638 atomic_t count ; 1639 unsigned int level ; 1640 struct hlist_head tasks[3U] ; 1641 struct rcu_head rcu ; 1642 struct upid numbers[1U] ; 1643}; 1644#line 68 "include/linux/pid.h" 1645struct pid_link { 1646 struct hlist_node node ; 1647 struct pid *pid ; 1648}; 1649#line 10 "include/linux/seccomp.h" 1650struct __anonstruct_seccomp_t_158 { 1651 int mode ; 1652}; 1653#line 10 "include/linux/seccomp.h" 1654typedef struct __anonstruct_seccomp_t_158 seccomp_t; 1655#line 427 "include/linux/rculist.h" 1656struct plist_head { 1657 struct list_head node_list ; 1658}; 1659#line 84 "include/linux/plist.h" 1660struct plist_node { 1661 int prio ; 1662 struct list_head prio_list ; 1663 struct list_head node_list ; 1664}; 1665#line 20 "include/linux/rtmutex.h" 1666struct rt_mutex { 1667 raw_spinlock_t wait_lock ; 1668 struct plist_head wait_list ; 1669 struct task_struct *owner ; 1670 int save_state ; 1671 char const *name ; 1672 char const *file ; 1673 int line ; 1674 void *magic ; 1675}; 1676#line 38 1677struct rt_mutex_waiter; 1678#line 38 1679struct rt_mutex_waiter; 1680#line 41 "include/linux/resource.h" 1681struct rlimit { 1682 unsigned long rlim_cur ; 1683 unsigned long rlim_max ; 1684}; 1685#line 85 "include/linux/resource.h" 1686struct timerqueue_node { 1687 struct rb_node node ; 1688 ktime_t expires ; 1689}; 1690#line 12 "include/linux/timerqueue.h" 1691struct timerqueue_head { 1692 struct rb_root head ; 1693 struct timerqueue_node *next ; 1694}; 1695#line 50 1696struct hrtimer_clock_base; 1697#line 50 1698struct hrtimer_clock_base; 1699#line 51 1700struct hrtimer_cpu_base; 1701#line 51 1702struct hrtimer_cpu_base; 1703#line 60 1704enum hrtimer_restart { 1705 HRTIMER_NORESTART = 0, 1706 HRTIMER_RESTART = 1 1707} ; 1708#line 65 "include/linux/timerqueue.h" 1709struct hrtimer { 1710 struct timerqueue_node node ; 1711 ktime_t _softexpires ; 1712 enum hrtimer_restart (*function)(struct hrtimer * ) ; 1713 struct hrtimer_clock_base *base ; 1714 unsigned long state ; 1715 int start_pid ; 1716 void *start_site ; 1717 char start_comm[16U] ; 1718}; 1719#line 132 "include/linux/hrtimer.h" 1720struct hrtimer_clock_base { 1721 struct hrtimer_cpu_base *cpu_base ; 1722 int index ; 1723 clockid_t clockid ; 1724 struct timerqueue_head active ; 1725 ktime_t resolution ; 1726 ktime_t (*get_time)(void) ; 1727 ktime_t softirq_time ; 1728 ktime_t offset ; 1729}; 1730#line 162 "include/linux/hrtimer.h" 1731struct hrtimer_cpu_base { 1732 raw_spinlock_t lock ; 1733 unsigned long active_bases ; 1734 ktime_t expires_next ; 1735 int hres_active ; 1736 int hang_detected ; 1737 unsigned long nr_events ; 1738 unsigned long nr_retries ; 1739 unsigned long nr_hangs ; 1740 ktime_t max_hang_time ; 1741 struct hrtimer_clock_base clock_base[3U] ; 1742}; 1743#line 452 "include/linux/hrtimer.h" 1744struct task_io_accounting { 1745 u64 rchar ; 1746 u64 wchar ; 1747 u64 syscr ; 1748 u64 syscw ; 1749 u64 read_bytes ; 1750 u64 write_bytes ; 1751 u64 cancelled_write_bytes ; 1752}; 1753#line 45 "include/linux/task_io_accounting.h" 1754struct latency_record { 1755 unsigned long backtrace[12U] ; 1756 unsigned int count ; 1757 unsigned long time ; 1758 unsigned long max ; 1759}; 1760#line 29 "include/linux/key.h" 1761typedef int32_t key_serial_t; 1762#line 32 "include/linux/key.h" 1763typedef uint32_t key_perm_t; 1764#line 33 1765struct key; 1766#line 33 1767struct key; 1768#line 34 1769struct signal_struct; 1770#line 34 1771struct signal_struct; 1772#line 35 1773struct key_type; 1774#line 35 1775struct key_type; 1776#line 37 1777struct keyring_list; 1778#line 37 1779struct keyring_list; 1780#line 115 1781struct key_user; 1782#line 115 "include/linux/key.h" 1783union __anonunion_ldv_16563_159 { 1784 time_t expiry ; 1785 time_t revoked_at ; 1786}; 1787#line 115 "include/linux/key.h" 1788union __anonunion_type_data_160 { 1789 struct list_head link ; 1790 unsigned long x[2U] ; 1791 void *p[2U] ; 1792 int reject_error ; 1793}; 1794#line 115 "include/linux/key.h" 1795union __anonunion_payload_161 { 1796 unsigned long value ; 1797 void *rcudata ; 1798 void *data ; 1799 struct keyring_list *subscriptions ; 1800}; 1801#line 115 "include/linux/key.h" 1802struct key { 1803 atomic_t usage ; 1804 key_serial_t serial ; 1805 struct rb_node serial_node ; 1806 struct key_type *type ; 1807 struct rw_semaphore sem ; 1808 struct key_user *user ; 1809 void *security ; 1810 union __anonunion_ldv_16563_159 ldv_16563 ; 1811 uid_t uid ; 1812 gid_t gid ; 1813 key_perm_t perm ; 1814 unsigned short quotalen ; 1815 unsigned short datalen ; 1816 unsigned long flags ; 1817 char *description ; 1818 union __anonunion_type_data_160 type_data ; 1819 union __anonunion_payload_161 payload ; 1820}; 1821#line 316 1822struct audit_context; 1823#line 316 1824struct audit_context; 1825#line 28 "include/linux/selinux.h" 1826struct group_info { 1827 atomic_t usage ; 1828 int ngroups ; 1829 int nblocks ; 1830 gid_t small_block[32U] ; 1831 gid_t *blocks[0U] ; 1832}; 1833#line 77 "include/linux/cred.h" 1834struct thread_group_cred { 1835 atomic_t usage ; 1836 pid_t tgid ; 1837 spinlock_t lock ; 1838 struct key *session_keyring ; 1839 struct key *process_keyring ; 1840 struct rcu_head rcu ; 1841}; 1842#line 91 "include/linux/cred.h" 1843struct cred { 1844 atomic_t usage ; 1845 atomic_t subscribers ; 1846 void *put_addr ; 1847 unsigned int magic ; 1848 uid_t uid ; 1849 gid_t gid ; 1850 uid_t suid ; 1851 gid_t sgid ; 1852 uid_t euid ; 1853 gid_t egid ; 1854 uid_t fsuid ; 1855 gid_t fsgid ; 1856 unsigned int securebits ; 1857 kernel_cap_t cap_inheritable ; 1858 kernel_cap_t cap_permitted ; 1859 kernel_cap_t cap_effective ; 1860 kernel_cap_t cap_bset ; 1861 unsigned char jit_keyring ; 1862 struct key *thread_keyring ; 1863 struct key *request_key_auth ; 1864 struct thread_group_cred *tgcred ; 1865 void *security ; 1866 struct user_struct *user ; 1867 struct user_namespace *user_ns ; 1868 struct group_info *group_info ; 1869 struct rcu_head rcu ; 1870}; 1871#line 264 1872struct llist_node; 1873#line 64 "include/linux/llist.h" 1874struct llist_node { 1875 struct llist_node *next ; 1876}; 1877#line 185 1878struct futex_pi_state; 1879#line 185 1880struct futex_pi_state; 1881#line 186 1882struct robust_list_head; 1883#line 186 1884struct robust_list_head; 1885#line 187 1886struct bio_list; 1887#line 187 1888struct bio_list; 1889#line 188 1890struct fs_struct; 1891#line 188 1892struct fs_struct; 1893#line 189 1894struct perf_event_context; 1895#line 189 1896struct perf_event_context; 1897#line 190 1898struct blk_plug; 1899#line 190 1900struct blk_plug; 1901#line 149 "include/linux/sched.h" 1902struct cfs_rq; 1903#line 149 1904struct cfs_rq; 1905#line 406 "include/linux/sched.h" 1906struct sighand_struct { 1907 atomic_t count ; 1908 struct k_sigaction action[64U] ; 1909 spinlock_t siglock ; 1910 wait_queue_head_t signalfd_wqh ; 1911}; 1912#line 449 "include/linux/sched.h" 1913struct pacct_struct { 1914 int ac_flag ; 1915 long ac_exitcode ; 1916 unsigned long ac_mem ; 1917 cputime_t ac_utime ; 1918 cputime_t ac_stime ; 1919 unsigned long ac_minflt ; 1920 unsigned long ac_majflt ; 1921}; 1922#line 457 "include/linux/sched.h" 1923struct cpu_itimer { 1924 cputime_t expires ; 1925 cputime_t incr ; 1926 u32 error ; 1927 u32 incr_error ; 1928}; 1929#line 464 "include/linux/sched.h" 1930struct task_cputime { 1931 cputime_t utime ; 1932 cputime_t stime ; 1933 unsigned long long sum_exec_runtime ; 1934}; 1935#line 481 "include/linux/sched.h" 1936struct thread_group_cputimer { 1937 struct task_cputime cputime ; 1938 int running ; 1939 raw_spinlock_t lock ; 1940}; 1941#line 517 1942struct autogroup; 1943#line 517 1944struct autogroup; 1945#line 518 1946struct tty_struct; 1947#line 518 1948struct taskstats; 1949#line 518 1950struct tty_audit_buf; 1951#line 518 "include/linux/sched.h" 1952struct signal_struct { 1953 atomic_t sigcnt ; 1954 atomic_t live ; 1955 int nr_threads ; 1956 wait_queue_head_t wait_chldexit ; 1957 struct task_struct *curr_target ; 1958 struct sigpending shared_pending ; 1959 int group_exit_code ; 1960 int notify_count ; 1961 struct task_struct *group_exit_task ; 1962 int group_stop_count ; 1963 unsigned int flags ; 1964 unsigned char is_child_subreaper : 1 ; 1965 unsigned char has_child_subreaper : 1 ; 1966 struct list_head posix_timers ; 1967 struct hrtimer real_timer ; 1968 struct pid *leader_pid ; 1969 ktime_t it_real_incr ; 1970 struct cpu_itimer it[2U] ; 1971 struct thread_group_cputimer cputimer ; 1972 struct task_cputime cputime_expires ; 1973 struct list_head cpu_timers[3U] ; 1974 struct pid *tty_old_pgrp ; 1975 int leader ; 1976 struct tty_struct *tty ; 1977 struct autogroup *autogroup ; 1978 cputime_t utime ; 1979 cputime_t stime ; 1980 cputime_t cutime ; 1981 cputime_t cstime ; 1982 cputime_t gtime ; 1983 cputime_t cgtime ; 1984 cputime_t prev_utime ; 1985 cputime_t prev_stime ; 1986 unsigned long nvcsw ; 1987 unsigned long nivcsw ; 1988 unsigned long cnvcsw ; 1989 unsigned long cnivcsw ; 1990 unsigned long min_flt ; 1991 unsigned long maj_flt ; 1992 unsigned long cmin_flt ; 1993 unsigned long cmaj_flt ; 1994 unsigned long inblock ; 1995 unsigned long oublock ; 1996 unsigned long cinblock ; 1997 unsigned long coublock ; 1998 unsigned long maxrss ; 1999 unsigned long cmaxrss ; 2000 struct task_io_accounting ioac ; 2001 unsigned long long sum_sched_runtime ; 2002 struct rlimit rlim[16U] ; 2003 struct pacct_struct pacct ; 2004 struct taskstats *stats ; 2005 unsigned int audit_tty ; 2006 struct tty_audit_buf *tty_audit_buf ; 2007 struct rw_semaphore group_rwsem ; 2008 int oom_adj ; 2009 int oom_score_adj ; 2010 int oom_score_adj_min ; 2011 struct mutex cred_guard_mutex ; 2012}; 2013#line 699 "include/linux/sched.h" 2014struct user_struct { 2015 atomic_t __count ; 2016 atomic_t processes ; 2017 atomic_t files ; 2018 atomic_t sigpending ; 2019 atomic_t inotify_watches ; 2020 atomic_t inotify_devs ; 2021 atomic_t fanotify_listeners ; 2022 atomic_long_t epoll_watches ; 2023 unsigned long mq_bytes ; 2024 unsigned long locked_shm ; 2025 struct key *uid_keyring ; 2026 struct key *session_keyring ; 2027 struct hlist_node uidhash_node ; 2028 uid_t uid ; 2029 struct user_namespace *user_ns ; 2030 atomic_long_t locked_vm ; 2031}; 2032#line 744 2033struct backing_dev_info; 2034#line 744 2035struct backing_dev_info; 2036#line 745 2037struct reclaim_state; 2038#line 745 2039struct reclaim_state; 2040#line 746 "include/linux/sched.h" 2041struct sched_info { 2042 unsigned long pcount ; 2043 unsigned long long run_delay ; 2044 unsigned long long last_arrival ; 2045 unsigned long long last_queued ; 2046}; 2047#line 760 "include/linux/sched.h" 2048struct task_delay_info { 2049 spinlock_t lock ; 2050 unsigned int flags ; 2051 struct timespec blkio_start ; 2052 struct timespec blkio_end ; 2053 u64 blkio_delay ; 2054 u64 swapin_delay ; 2055 u32 blkio_count ; 2056 u32 swapin_count ; 2057 struct timespec freepages_start ; 2058 struct timespec freepages_end ; 2059 u64 freepages_delay ; 2060 u32 freepages_count ; 2061}; 2062#line 1069 2063struct io_context; 2064#line 1069 2065struct io_context; 2066#line 1097 2067struct pipe_inode_info; 2068#line 1097 2069struct pipe_inode_info; 2070#line 1099 2071struct rq; 2072#line 1099 2073struct rq; 2074#line 1100 "include/linux/sched.h" 2075struct sched_class { 2076 struct sched_class const *next ; 2077 void (*enqueue_task)(struct rq * , struct task_struct * , int ) ; 2078 void (*dequeue_task)(struct rq * , struct task_struct * , int ) ; 2079 void (*yield_task)(struct rq * ) ; 2080 bool (*yield_to_task)(struct rq * , struct task_struct * , bool ) ; 2081 void (*check_preempt_curr)(struct rq * , struct task_struct * , int ) ; 2082 struct task_struct *(*pick_next_task)(struct rq * ) ; 2083 void (*put_prev_task)(struct rq * , struct task_struct * ) ; 2084 int (*select_task_rq)(struct task_struct * , int , int ) ; 2085 void (*pre_schedule)(struct rq * , struct task_struct * ) ; 2086 void (*post_schedule)(struct rq * ) ; 2087 void (*task_waking)(struct task_struct * ) ; 2088 void (*task_woken)(struct rq * , struct task_struct * ) ; 2089 void (*set_cpus_allowed)(struct task_struct * , struct cpumask const * ) ; 2090 void (*rq_online)(struct rq * ) ; 2091 void (*rq_offline)(struct rq * ) ; 2092 void (*set_curr_task)(struct rq * ) ; 2093 void (*task_tick)(struct rq * , struct task_struct * , int ) ; 2094 void (*task_fork)(struct task_struct * ) ; 2095 void (*switched_from)(struct rq * , struct task_struct * ) ; 2096 void (*switched_to)(struct rq * , struct task_struct * ) ; 2097 void (*prio_changed)(struct rq * , struct task_struct * , int ) ; 2098 unsigned int (*get_rr_interval)(struct rq * , struct task_struct * ) ; 2099 void (*task_move_group)(struct task_struct * , int ) ; 2100}; 2101#line 1165 "include/linux/sched.h" 2102struct load_weight { 2103 unsigned long weight ; 2104 unsigned long inv_weight ; 2105}; 2106#line 1170 "include/linux/sched.h" 2107struct sched_statistics { 2108 u64 wait_start ; 2109 u64 wait_max ; 2110 u64 wait_count ; 2111 u64 wait_sum ; 2112 u64 iowait_count ; 2113 u64 iowait_sum ; 2114 u64 sleep_start ; 2115 u64 sleep_max ; 2116 s64 sum_sleep_runtime ; 2117 u64 block_start ; 2118 u64 block_max ; 2119 u64 exec_max ; 2120 u64 slice_max ; 2121 u64 nr_migrations_cold ; 2122 u64 nr_failed_migrations_affine ; 2123 u64 nr_failed_migrations_running ; 2124 u64 nr_failed_migrations_hot ; 2125 u64 nr_forced_migrations ; 2126 u64 nr_wakeups ; 2127 u64 nr_wakeups_sync ; 2128 u64 nr_wakeups_migrate ; 2129 u64 nr_wakeups_local ; 2130 u64 nr_wakeups_remote ; 2131 u64 nr_wakeups_affine ; 2132 u64 nr_wakeups_affine_attempts ; 2133 u64 nr_wakeups_passive ; 2134 u64 nr_wakeups_idle ; 2135}; 2136#line 1205 "include/linux/sched.h" 2137struct sched_entity { 2138 struct load_weight load ; 2139 struct rb_node run_node ; 2140 struct list_head group_node ; 2141 unsigned int on_rq ; 2142 u64 exec_start ; 2143 u64 sum_exec_runtime ; 2144 u64 vruntime ; 2145 u64 prev_sum_exec_runtime ; 2146 u64 nr_migrations ; 2147 struct sched_statistics statistics ; 2148 struct sched_entity *parent ; 2149 struct cfs_rq *cfs_rq ; 2150 struct cfs_rq *my_q ; 2151}; 2152#line 1231 2153struct rt_rq; 2154#line 1231 "include/linux/sched.h" 2155struct sched_rt_entity { 2156 struct list_head run_list ; 2157 unsigned long timeout ; 2158 unsigned int time_slice ; 2159 int nr_cpus_allowed ; 2160 struct sched_rt_entity *back ; 2161 struct sched_rt_entity *parent ; 2162 struct rt_rq *rt_rq ; 2163 struct rt_rq *my_q ; 2164}; 2165#line 1255 2166struct mem_cgroup; 2167#line 1255 "include/linux/sched.h" 2168struct memcg_batch_info { 2169 int do_batch ; 2170 struct mem_cgroup *memcg ; 2171 unsigned long nr_pages ; 2172 unsigned long memsw_nr_pages ; 2173}; 2174#line 1616 2175struct files_struct; 2176#line 1616 2177struct css_set; 2178#line 1616 2179struct compat_robust_list_head; 2180#line 1616 "include/linux/sched.h" 2181struct task_struct { 2182 long volatile state ; 2183 void *stack ; 2184 atomic_t usage ; 2185 unsigned int flags ; 2186 unsigned int ptrace ; 2187 struct llist_node wake_entry ; 2188 int on_cpu ; 2189 int on_rq ; 2190 int prio ; 2191 int static_prio ; 2192 int normal_prio ; 2193 unsigned int rt_priority ; 2194 struct sched_class const *sched_class ; 2195 struct sched_entity se ; 2196 struct sched_rt_entity rt ; 2197 struct hlist_head preempt_notifiers ; 2198 unsigned char fpu_counter ; 2199 unsigned int policy ; 2200 cpumask_t cpus_allowed ; 2201 struct sched_info sched_info ; 2202 struct list_head tasks ; 2203 struct plist_node pushable_tasks ; 2204 struct mm_struct *mm ; 2205 struct mm_struct *active_mm ; 2206 unsigned char brk_randomized : 1 ; 2207 int exit_state ; 2208 int exit_code ; 2209 int exit_signal ; 2210 int pdeath_signal ; 2211 unsigned int jobctl ; 2212 unsigned int personality ; 2213 unsigned char did_exec : 1 ; 2214 unsigned char in_execve : 1 ; 2215 unsigned char in_iowait : 1 ; 2216 unsigned char sched_reset_on_fork : 1 ; 2217 unsigned char sched_contributes_to_load : 1 ; 2218 unsigned char irq_thread : 1 ; 2219 pid_t pid ; 2220 pid_t tgid ; 2221 unsigned long stack_canary ; 2222 struct task_struct *real_parent ; 2223 struct task_struct *parent ; 2224 struct list_head children ; 2225 struct list_head sibling ; 2226 struct task_struct *group_leader ; 2227 struct list_head ptraced ; 2228 struct list_head ptrace_entry ; 2229 struct pid_link pids[3U] ; 2230 struct list_head thread_group ; 2231 struct completion *vfork_done ; 2232 int *set_child_tid ; 2233 int *clear_child_tid ; 2234 cputime_t utime ; 2235 cputime_t stime ; 2236 cputime_t utimescaled ; 2237 cputime_t stimescaled ; 2238 cputime_t gtime ; 2239 cputime_t prev_utime ; 2240 cputime_t prev_stime ; 2241 unsigned long nvcsw ; 2242 unsigned long nivcsw ; 2243 struct timespec start_time ; 2244 struct timespec real_start_time ; 2245 unsigned long min_flt ; 2246 unsigned long maj_flt ; 2247 struct task_cputime cputime_expires ; 2248 struct list_head cpu_timers[3U] ; 2249 struct cred const *real_cred ; 2250 struct cred const *cred ; 2251 struct cred *replacement_session_keyring ; 2252 char comm[16U] ; 2253 int link_count ; 2254 int total_link_count ; 2255 struct sysv_sem sysvsem ; 2256 unsigned long last_switch_count ; 2257 struct thread_struct thread ; 2258 struct fs_struct *fs ; 2259 struct files_struct *files ; 2260 struct nsproxy *nsproxy ; 2261 struct signal_struct *signal ; 2262 struct sighand_struct *sighand ; 2263 sigset_t blocked ; 2264 sigset_t real_blocked ; 2265 sigset_t saved_sigmask ; 2266 struct sigpending pending ; 2267 unsigned long sas_ss_sp ; 2268 size_t sas_ss_size ; 2269 int (*notifier)(void * ) ; 2270 void *notifier_data ; 2271 sigset_t *notifier_mask ; 2272 struct audit_context *audit_context ; 2273 uid_t loginuid ; 2274 unsigned int sessionid ; 2275 seccomp_t seccomp ; 2276 u32 parent_exec_id ; 2277 u32 self_exec_id ; 2278 spinlock_t alloc_lock ; 2279 raw_spinlock_t pi_lock ; 2280 struct plist_head pi_waiters ; 2281 struct rt_mutex_waiter *pi_blocked_on ; 2282 struct mutex_waiter *blocked_on ; 2283 unsigned int irq_events ; 2284 unsigned long hardirq_enable_ip ; 2285 unsigned long hardirq_disable_ip ; 2286 unsigned int hardirq_enable_event ; 2287 unsigned int hardirq_disable_event ; 2288 int hardirqs_enabled ; 2289 int hardirq_context ; 2290 unsigned long softirq_disable_ip ; 2291 unsigned long softirq_enable_ip ; 2292 unsigned int softirq_disable_event ; 2293 unsigned int softirq_enable_event ; 2294 int softirqs_enabled ; 2295 int softirq_context ; 2296 u64 curr_chain_key ; 2297 int lockdep_depth ; 2298 unsigned int lockdep_recursion ; 2299 struct held_lock held_locks[48U] ; 2300 gfp_t lockdep_reclaim_gfp ; 2301 void *journal_info ; 2302 struct bio_list *bio_list ; 2303 struct blk_plug *plug ; 2304 struct reclaim_state *reclaim_state ; 2305 struct backing_dev_info *backing_dev_info ; 2306 struct io_context *io_context ; 2307 unsigned long ptrace_message ; 2308 siginfo_t *last_siginfo ; 2309 struct task_io_accounting ioac ; 2310 u64 acct_rss_mem1 ; 2311 u64 acct_vm_mem1 ; 2312 cputime_t acct_timexpd ; 2313 nodemask_t mems_allowed ; 2314 seqcount_t mems_allowed_seq ; 2315 int cpuset_mem_spread_rotor ; 2316 int cpuset_slab_spread_rotor ; 2317 struct css_set *cgroups ; 2318 struct list_head cg_list ; 2319 struct robust_list_head *robust_list ; 2320 struct compat_robust_list_head *compat_robust_list ; 2321 struct list_head pi_state_list ; 2322 struct futex_pi_state *pi_state_cache ; 2323 struct perf_event_context *perf_event_ctxp[2U] ; 2324 struct mutex perf_event_mutex ; 2325 struct list_head perf_event_list ; 2326 struct mempolicy *mempolicy ; 2327 short il_next ; 2328 short pref_node_fork ; 2329 struct rcu_head rcu ; 2330 struct pipe_inode_info *splice_pipe ; 2331 struct task_delay_info *delays ; 2332 int make_it_fail ; 2333 int nr_dirtied ; 2334 int nr_dirtied_pause ; 2335 unsigned long dirty_paused_when ; 2336 int latency_record_count ; 2337 struct latency_record latency_record[32U] ; 2338 unsigned long timer_slack_ns ; 2339 unsigned long default_timer_slack_ns ; 2340 struct list_head *scm_work_list ; 2341 unsigned long trace ; 2342 unsigned long trace_recursion ; 2343 struct memcg_batch_info memcg_batch ; 2344 atomic_t ptrace_bp_refcnt ; 2345}; 2346#line 28 "include/linux/of.h" 2347typedef u32 phandle; 2348#line 30 "include/linux/of.h" 2349struct property { 2350 char *name ; 2351 int length ; 2352 void *value ; 2353 struct property *next ; 2354 unsigned long _flags ; 2355 unsigned int unique_id ; 2356}; 2357#line 39 2358struct proc_dir_entry; 2359#line 39 "include/linux/of.h" 2360struct device_node { 2361 char const *name ; 2362 char const *type ; 2363 phandle phandle ; 2364 char *full_name ; 2365 struct property *properties ; 2366 struct property *deadprops ; 2367 struct device_node *parent ; 2368 struct device_node *child ; 2369 struct device_node *sibling ; 2370 struct device_node *next ; 2371 struct device_node *allnext ; 2372 struct proc_dir_entry *pde ; 2373 struct kref kref ; 2374 unsigned long _flags ; 2375 void *data ; 2376}; 2377#line 41 "include/linux/i2c.h" 2378struct i2c_msg; 2379#line 41 2380struct i2c_msg; 2381#line 42 2382struct i2c_algorithm; 2383#line 42 2384struct i2c_algorithm; 2385#line 43 2386struct i2c_adapter; 2387#line 43 2388struct i2c_adapter; 2389#line 46 2390union i2c_smbus_data; 2391#line 46 2392union i2c_smbus_data; 2393#line 336 "include/linux/i2c.h" 2394struct i2c_algorithm { 2395 int (*master_xfer)(struct i2c_adapter * , struct i2c_msg * , int ) ; 2396 int (*smbus_xfer)(struct i2c_adapter * , u16 , unsigned short , char , u8 , 2397 int , union i2c_smbus_data * ) ; 2398 u32 (*functionality)(struct i2c_adapter * ) ; 2399}; 2400#line 368 "include/linux/i2c.h" 2401struct i2c_adapter { 2402 struct module *owner ; 2403 unsigned int class ; 2404 struct i2c_algorithm const *algo ; 2405 void *algo_data ; 2406 struct rt_mutex bus_lock ; 2407 int timeout ; 2408 int retries ; 2409 struct device dev ; 2410 int nr ; 2411 char name[48U] ; 2412 struct completion dev_released ; 2413 struct mutex userspace_clients_lock ; 2414 struct list_head userspace_clients ; 2415}; 2416#line 486 "include/linux/i2c.h" 2417struct i2c_msg { 2418 __u16 addr ; 2419 __u16 flags ; 2420 __u16 len ; 2421 __u8 *buf ; 2422}; 2423#line 551 "include/linux/i2c.h" 2424union i2c_smbus_data { 2425 __u8 byte ; 2426 __u16 word ; 2427 __u8 block[34U] ; 2428}; 2429#line 59 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p" 2430struct stub_chip { 2431 u8 pointer ; 2432 u16 words[256U] ; 2433}; 2434#line 1 "<compiler builtins>" 2435long __builtin_expect(long , long ) ; 2436#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p" 2437void ldv_spin_lock(void) ; 2438#line 3 2439void ldv_spin_unlock(void) ; 2440#line 4 2441int ldv_spin_trylock(void) ; 2442#line 101 "include/linux/printk.h" 2443extern int printk(char const * , ...) ; 2444#line 50 "include/linux/dynamic_debug.h" 2445extern int __dynamic_dev_dbg(struct _ddebug * , struct device const * , char const * 2446 , ...) ; 2447#line 26 "include/linux/export.h" 2448extern struct module __this_module ; 2449#line 161 "include/linux/slab.h" 2450extern void kfree(void const * ) ; 2451#line 220 "include/linux/slub_def.h" 2452extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t ) ; 2453#line 223 2454void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ; 2455#line 353 "include/linux/slab.h" 2456__inline static void *kzalloc(size_t size , gfp_t flags ) ; 2457#line 10 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p" 2458extern void *__VERIFIER_nondet_pointer(void) ; 2459#line 11 2460void ldv_check_alloc_flags(gfp_t flags ) ; 2461#line 12 2462void ldv_check_alloc_nonatomic(void) ; 2463#line 14 2464struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ; 2465#line 446 "include/linux/i2c.h" 2466extern int i2c_add_adapter(struct i2c_adapter * ) ; 2467#line 447 2468extern int i2c_del_adapter(struct i2c_adapter * ) ; 2469#line 51 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p" 2470static unsigned short chip_addr[10U] ; 2471#line 56 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p" 2472static unsigned long functionality = 209649664UL; 2473#line 66 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p" 2474static struct stub_chip *stub_chips ; 2475#line 69 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p" 2476static s32 stub_xfer(struct i2c_adapter *adap , u16 addr , unsigned short flags , 2477 char read_write , u8 command , int size , union i2c_smbus_data *data ) 2478{ s32 ret ; 2479 int i ; 2480 int len ; 2481 struct stub_chip *chip ; 2482 struct _ddebug descriptor ; 2483 long tmp ; 2484 struct _ddebug descriptor___0 ; 2485 long tmp___0 ; 2486 u8 tmp___1 ; 2487 struct _ddebug descriptor___1 ; 2488 long tmp___2 ; 2489 struct _ddebug descriptor___2 ; 2490 long tmp___3 ; 2491 struct _ddebug descriptor___3 ; 2492 long tmp___4 ; 2493 struct _ddebug descriptor___4 ; 2494 long tmp___5 ; 2495 struct _ddebug descriptor___5 ; 2496 long tmp___6 ; 2497 struct _ddebug descriptor___6 ; 2498 long tmp___7 ; 2499 struct _ddebug descriptor___7 ; 2500 long tmp___8 ; 2501 struct _ddebug descriptor___8 ; 2502 long tmp___9 ; 2503 int __cil_tmp33 ; 2504 unsigned long __cil_tmp34 ; 2505 unsigned long __cil_tmp35 ; 2506 unsigned short __cil_tmp36 ; 2507 int __cil_tmp37 ; 2508 unsigned long __cil_tmp38 ; 2509 unsigned long __cil_tmp39 ; 2510 unsigned long __cil_tmp40 ; 2511 unsigned short __cil_tmp41 ; 2512 unsigned int __cil_tmp42 ; 2513 struct stub_chip *__cil_tmp43 ; 2514 unsigned long __cil_tmp44 ; 2515 unsigned long __cil_tmp45 ; 2516 struct _ddebug *__cil_tmp46 ; 2517 unsigned long __cil_tmp47 ; 2518 unsigned long __cil_tmp48 ; 2519 unsigned long __cil_tmp49 ; 2520 unsigned long __cil_tmp50 ; 2521 unsigned long __cil_tmp51 ; 2522 unsigned long __cil_tmp52 ; 2523 unsigned char __cil_tmp53 ; 2524 long __cil_tmp54 ; 2525 long __cil_tmp55 ; 2526 unsigned long __cil_tmp56 ; 2527 unsigned long __cil_tmp57 ; 2528 struct device *__cil_tmp58 ; 2529 struct device const *__cil_tmp59 ; 2530 int __cil_tmp60 ; 2531 signed char __cil_tmp61 ; 2532 int __cil_tmp62 ; 2533 struct _ddebug *__cil_tmp63 ; 2534 unsigned long __cil_tmp64 ; 2535 unsigned long __cil_tmp65 ; 2536 unsigned long __cil_tmp66 ; 2537 unsigned long __cil_tmp67 ; 2538 unsigned long __cil_tmp68 ; 2539 unsigned long __cil_tmp69 ; 2540 unsigned char __cil_tmp70 ; 2541 long __cil_tmp71 ; 2542 long __cil_tmp72 ; 2543 unsigned long __cil_tmp73 ; 2544 unsigned long __cil_tmp74 ; 2545 struct device *__cil_tmp75 ; 2546 struct device const *__cil_tmp76 ; 2547 int __cil_tmp77 ; 2548 int __cil_tmp78 ; 2549 u8 __cil_tmp79 ; 2550 int __cil_tmp80 ; 2551 int __cil_tmp81 ; 2552 unsigned long __cil_tmp82 ; 2553 unsigned long __cil_tmp83 ; 2554 unsigned long __cil_tmp84 ; 2555 unsigned long __cil_tmp85 ; 2556 u16 __cil_tmp86 ; 2557 struct _ddebug *__cil_tmp87 ; 2558 unsigned long __cil_tmp88 ; 2559 unsigned long __cil_tmp89 ; 2560 unsigned long __cil_tmp90 ; 2561 unsigned long __cil_tmp91 ; 2562 unsigned long __cil_tmp92 ; 2563 unsigned long __cil_tmp93 ; 2564 unsigned char __cil_tmp94 ; 2565 long __cil_tmp95 ; 2566 long __cil_tmp96 ; 2567 unsigned long __cil_tmp97 ; 2568 unsigned long __cil_tmp98 ; 2569 struct device *__cil_tmp99 ; 2570 struct device const *__cil_tmp100 ; 2571 int __cil_tmp101 ; 2572 __u8 __cil_tmp102 ; 2573 int __cil_tmp103 ; 2574 signed char __cil_tmp104 ; 2575 int __cil_tmp105 ; 2576 int __cil_tmp106 ; 2577 unsigned long __cil_tmp107 ; 2578 unsigned long __cil_tmp108 ; 2579 unsigned long __cil_tmp109 ; 2580 unsigned long __cil_tmp110 ; 2581 int __cil_tmp111 ; 2582 unsigned long __cil_tmp112 ; 2583 unsigned long __cil_tmp113 ; 2584 unsigned long __cil_tmp114 ; 2585 unsigned long __cil_tmp115 ; 2586 u16 __cil_tmp116 ; 2587 unsigned int __cil_tmp117 ; 2588 unsigned int __cil_tmp118 ; 2589 int __cil_tmp119 ; 2590 unsigned long __cil_tmp120 ; 2591 unsigned long __cil_tmp121 ; 2592 unsigned long __cil_tmp122 ; 2593 unsigned long __cil_tmp123 ; 2594 __u8 __cil_tmp124 ; 2595 u16 __cil_tmp125 ; 2596 int __cil_tmp126 ; 2597 int __cil_tmp127 ; 2598 unsigned long __cil_tmp128 ; 2599 unsigned long __cil_tmp129 ; 2600 unsigned long __cil_tmp130 ; 2601 unsigned long __cil_tmp131 ; 2602 u16 __cil_tmp132 ; 2603 int __cil_tmp133 ; 2604 int __cil_tmp134 ; 2605 struct _ddebug *__cil_tmp135 ; 2606 unsigned long __cil_tmp136 ; 2607 unsigned long __cil_tmp137 ; 2608 unsigned long __cil_tmp138 ; 2609 unsigned long __cil_tmp139 ; 2610 unsigned long __cil_tmp140 ; 2611 unsigned long __cil_tmp141 ; 2612 unsigned char __cil_tmp142 ; 2613 long __cil_tmp143 ; 2614 long __cil_tmp144 ; 2615 unsigned long __cil_tmp145 ; 2616 unsigned long __cil_tmp146 ; 2617 struct device *__cil_tmp147 ; 2618 struct device const *__cil_tmp148 ; 2619 int __cil_tmp149 ; 2620 __u8 __cil_tmp150 ; 2621 int __cil_tmp151 ; 2622 int __cil_tmp152 ; 2623 int __cil_tmp153 ; 2624 unsigned long __cil_tmp154 ; 2625 unsigned long __cil_tmp155 ; 2626 unsigned long __cil_tmp156 ; 2627 unsigned long __cil_tmp157 ; 2628 u16 __cil_tmp158 ; 2629 struct _ddebug *__cil_tmp159 ; 2630 unsigned long __cil_tmp160 ; 2631 unsigned long __cil_tmp161 ; 2632 unsigned long __cil_tmp162 ; 2633 unsigned long __cil_tmp163 ; 2634 unsigned long __cil_tmp164 ; 2635 unsigned long __cil_tmp165 ; 2636 unsigned char __cil_tmp166 ; 2637 long __cil_tmp167 ; 2638 long __cil_tmp168 ; 2639 unsigned long __cil_tmp169 ; 2640 unsigned long __cil_tmp170 ; 2641 struct device *__cil_tmp171 ; 2642 struct device const *__cil_tmp172 ; 2643 int __cil_tmp173 ; 2644 __u8 __cil_tmp174 ; 2645 int __cil_tmp175 ; 2646 int __cil_tmp176 ; 2647 unsigned int __cil_tmp177 ; 2648 unsigned int __cil_tmp178 ; 2649 signed char __cil_tmp179 ; 2650 int __cil_tmp180 ; 2651 int __cil_tmp181 ; 2652 unsigned long __cil_tmp182 ; 2653 unsigned long __cil_tmp183 ; 2654 unsigned long __cil_tmp184 ; 2655 unsigned long __cil_tmp185 ; 2656 struct _ddebug *__cil_tmp186 ; 2657 unsigned long __cil_tmp187 ; 2658 unsigned long __cil_tmp188 ; 2659 unsigned long __cil_tmp189 ; 2660 unsigned long __cil_tmp190 ; 2661 unsigned long __cil_tmp191 ; 2662 unsigned long __cil_tmp192 ; 2663 unsigned char __cil_tmp193 ; 2664 long __cil_tmp194 ; 2665 long __cil_tmp195 ; 2666 unsigned long __cil_tmp196 ; 2667 unsigned long __cil_tmp197 ; 2668 struct device *__cil_tmp198 ; 2669 struct device const *__cil_tmp199 ; 2670 int __cil_tmp200 ; 2671 __u16 __cil_tmp201 ; 2672 int __cil_tmp202 ; 2673 int __cil_tmp203 ; 2674 int __cil_tmp204 ; 2675 unsigned long __cil_tmp205 ; 2676 unsigned long __cil_tmp206 ; 2677 unsigned long __cil_tmp207 ; 2678 unsigned long __cil_tmp208 ; 2679 struct _ddebug *__cil_tmp209 ; 2680 unsigned long __cil_tmp210 ; 2681 unsigned long __cil_tmp211 ; 2682 unsigned long __cil_tmp212 ; 2683 unsigned long __cil_tmp213 ; 2684 unsigned long __cil_tmp214 ; 2685 unsigned long __cil_tmp215 ; 2686 unsigned char __cil_tmp216 ; 2687 long __cil_tmp217 ; 2688 long __cil_tmp218 ; 2689 unsigned long __cil_tmp219 ; 2690 unsigned long __cil_tmp220 ; 2691 struct device *__cil_tmp221 ; 2692 struct device const *__cil_tmp222 ; 2693 int __cil_tmp223 ; 2694 __u16 __cil_tmp224 ; 2695 int __cil_tmp225 ; 2696 int __cil_tmp226 ; 2697 unsigned long __cil_tmp227 ; 2698 unsigned long __cil_tmp228 ; 2699 unsigned long __cil_tmp229 ; 2700 unsigned long __cil_tmp230 ; 2701 __u8 __cil_tmp231 ; 2702 signed char __cil_tmp232 ; 2703 int __cil_tmp233 ; 2704 int __cil_tmp234 ; 2705 int __cil_tmp235 ; 2706 unsigned long __cil_tmp236 ; 2707 unsigned long __cil_tmp237 ; 2708 unsigned long __cil_tmp238 ; 2709 unsigned long __cil_tmp239 ; 2710 int __cil_tmp240 ; 2711 int __cil_tmp241 ; 2712 unsigned long __cil_tmp242 ; 2713 unsigned long __cil_tmp243 ; 2714 unsigned long __cil_tmp244 ; 2715 unsigned long __cil_tmp245 ; 2716 u16 __cil_tmp246 ; 2717 unsigned int __cil_tmp247 ; 2718 unsigned int __cil_tmp248 ; 2719 int __cil_tmp249 ; 2720 int __cil_tmp250 ; 2721 unsigned long __cil_tmp251 ; 2722 unsigned long __cil_tmp252 ; 2723 unsigned long __cil_tmp253 ; 2724 unsigned long __cil_tmp254 ; 2725 int __cil_tmp255 ; 2726 unsigned long __cil_tmp256 ; 2727 unsigned long __cil_tmp257 ; 2728 unsigned long __cil_tmp258 ; 2729 unsigned long __cil_tmp259 ; 2730 __u8 __cil_tmp260 ; 2731 u16 __cil_tmp261 ; 2732 int __cil_tmp262 ; 2733 int __cil_tmp263 ; 2734 int __cil_tmp264 ; 2735 unsigned long __cil_tmp265 ; 2736 unsigned long __cil_tmp266 ; 2737 unsigned long __cil_tmp267 ; 2738 unsigned long __cil_tmp268 ; 2739 u16 __cil_tmp269 ; 2740 int __cil_tmp270 ; 2741 int __cil_tmp271 ; 2742 struct _ddebug *__cil_tmp272 ; 2743 unsigned long __cil_tmp273 ; 2744 unsigned long __cil_tmp274 ; 2745 unsigned long __cil_tmp275 ; 2746 unsigned long __cil_tmp276 ; 2747 unsigned long __cil_tmp277 ; 2748 unsigned long __cil_tmp278 ; 2749 unsigned char __cil_tmp279 ; 2750 long __cil_tmp280 ; 2751 long __cil_tmp281 ; 2752 unsigned long __cil_tmp282 ; 2753 unsigned long __cil_tmp283 ; 2754 struct device *__cil_tmp284 ; 2755 struct device const *__cil_tmp285 ; 2756 int __cil_tmp286 ; 2757 int __cil_tmp287 ; 2758 int __cil_tmp288 ; 2759 unsigned long __cil_tmp289 ; 2760 unsigned long __cil_tmp290 ; 2761 unsigned long __cil_tmp291 ; 2762 unsigned long __cil_tmp292 ; 2763 int __cil_tmp293 ; 2764 int __cil_tmp294 ; 2765 unsigned long __cil_tmp295 ; 2766 unsigned long __cil_tmp296 ; 2767 unsigned long __cil_tmp297 ; 2768 unsigned long __cil_tmp298 ; 2769 u16 __cil_tmp299 ; 2770 struct _ddebug *__cil_tmp300 ; 2771 unsigned long __cil_tmp301 ; 2772 unsigned long __cil_tmp302 ; 2773 unsigned long __cil_tmp303 ; 2774 unsigned long __cil_tmp304 ; 2775 unsigned long __cil_tmp305 ; 2776 unsigned long __cil_tmp306 ; 2777 unsigned char __cil_tmp307 ; 2778 long __cil_tmp308 ; 2779 long __cil_tmp309 ; 2780 unsigned long __cil_tmp310 ; 2781 unsigned long __cil_tmp311 ; 2782 struct device *__cil_tmp312 ; 2783 struct device const *__cil_tmp313 ; 2784 int __cil_tmp314 ; 2785 int __cil_tmp315 ; 2786 struct _ddebug *__cil_tmp316 ; 2787 unsigned long __cil_tmp317 ; 2788 unsigned long __cil_tmp318 ; 2789 unsigned long __cil_tmp319 ; 2790 unsigned long __cil_tmp320 ; 2791 unsigned long __cil_tmp321 ; 2792 unsigned long __cil_tmp322 ; 2793 unsigned char __cil_tmp323 ; 2794 long __cil_tmp324 ; 2795 long __cil_tmp325 ; 2796 unsigned long __cil_tmp326 ; 2797 unsigned long __cil_tmp327 ; 2798 struct device *__cil_tmp328 ; 2799 struct device const *__cil_tmp329 ; 2800 2801 { 2802#line 74 2803 chip = (struct stub_chip *)0; 2804#line 77 2805 i = 0; 2806#line 77 2807 goto ldv_18807; 2808 ldv_18806: ; 2809 { 2810#line 78 2811 __cil_tmp33 = (int )addr; 2812#line 78 2813 __cil_tmp34 = i * 2UL; 2814#line 78 2815 __cil_tmp35 = (unsigned long )(chip_addr) + __cil_tmp34; 2816#line 78 2817 __cil_tmp36 = *((unsigned short *)__cil_tmp35); 2818#line 78 2819 __cil_tmp37 = (int )__cil_tmp36; 2820#line 78 2821 if (__cil_tmp37 == __cil_tmp33) { 2822#line 79 2823 __cil_tmp38 = (unsigned long )i; 2824#line 79 2825 chip = stub_chips + __cil_tmp38; 2826#line 80 2827 goto ldv_18805; 2828 } else { 2829 2830 } 2831 } 2832#line 77 2833 i = i + 1; 2834 ldv_18807: ; 2835#line 77 2836 if (i <= 9) { 2837 { 2838#line 77 2839 __cil_tmp39 = i * 2UL; 2840#line 77 2841 __cil_tmp40 = (unsigned long )(chip_addr) + __cil_tmp39; 2842#line 77 2843 __cil_tmp41 = *((unsigned short *)__cil_tmp40); 2844#line 77 2845 __cil_tmp42 = (unsigned int )__cil_tmp41; 2846#line 77 2847 if (__cil_tmp42 != 0U) { 2848#line 78 2849 goto ldv_18806; 2850 } else { 2851#line 80 2852 goto ldv_18805; 2853 } 2854 } 2855 } else { 2856#line 80 2857 goto ldv_18805; 2858 } 2859 ldv_18805: ; 2860 { 2861#line 83 2862 __cil_tmp43 = (struct stub_chip *)0; 2863#line 83 2864 __cil_tmp44 = (unsigned long )__cil_tmp43; 2865#line 83 2866 __cil_tmp45 = (unsigned long )chip; 2867#line 83 2868 if (__cil_tmp45 == __cil_tmp44) { 2869#line 84 2870 return (-19); 2871 } else { 2872 2873 } 2874 } 2875#line 88 2876 if (size == 0) { 2877#line 88 2878 goto case_0; 2879 } else 2880#line 93 2881 if (size == 1) { 2882#line 93 2883 goto case_1; 2884 } else 2885#line 109 2886 if (size == 2) { 2887#line 109 2888 goto case_2; 2889 } else 2890#line 127 2891 if (size == 3) { 2892#line 127 2893 goto case_3; 2894 } else 2895#line 143 2896 if (size == 8) { 2897#line 143 2898 goto case_8; 2899 } else { 2900 { 2901#line 166 2902 goto switch_default; 2903#line 86 2904 if (0) { 2905 case_0: /* CIL Label */ 2906 { 2907#line 89 2908 __cil_tmp46 = & descriptor; 2909#line 89 2910 *((char const **)__cil_tmp46) = "i2c_stub"; 2911#line 89 2912 __cil_tmp47 = (unsigned long )(& descriptor) + 8; 2913#line 89 2914 *((char const **)__cil_tmp47) = "stub_xfer"; 2915#line 89 2916 __cil_tmp48 = (unsigned long )(& descriptor) + 16; 2917#line 89 2918 *((char const **)__cil_tmp48) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p"; 2919#line 89 2920 __cil_tmp49 = (unsigned long )(& descriptor) + 24; 2921#line 89 2922 *((char const **)__cil_tmp49) = "smbus quick - addr 0x%02x\n"; 2923#line 89 2924 __cil_tmp50 = (unsigned long )(& descriptor) + 32; 2925#line 89 2926 *((unsigned int *)__cil_tmp50) = 89U; 2927#line 89 2928 __cil_tmp51 = (unsigned long )(& descriptor) + 35; 2929#line 89 2930 *((unsigned char *)__cil_tmp51) = (unsigned char)1; 2931#line 89 2932 __cil_tmp52 = (unsigned long )(& descriptor) + 35; 2933#line 89 2934 __cil_tmp53 = *((unsigned char *)__cil_tmp52); 2935#line 89 2936 __cil_tmp54 = (long )__cil_tmp53; 2937#line 89 2938 __cil_tmp55 = __cil_tmp54 & 1L; 2939#line 89 2940 tmp = __builtin_expect(__cil_tmp55, 0L); 2941 } 2942#line 89 2943 if (tmp != 0L) { 2944 { 2945#line 89 2946 __cil_tmp56 = (unsigned long )adap; 2947#line 89 2948 __cil_tmp57 = __cil_tmp56 + 176; 2949#line 89 2950 __cil_tmp58 = (struct device *)__cil_tmp57; 2951#line 89 2952 __cil_tmp59 = (struct device const *)__cil_tmp58; 2953#line 89 2954 __cil_tmp60 = (int )addr; 2955#line 89 2956 __dynamic_dev_dbg(& descriptor, __cil_tmp59, "smbus quick - addr 0x%02x\n", 2957 __cil_tmp60); 2958 } 2959 } else { 2960 2961 } 2962#line 90 2963 ret = 0; 2964#line 91 2965 goto ldv_18811; 2966 case_1: /* CIL Label */ ; 2967 { 2968#line 94 2969 __cil_tmp61 = (signed char )read_write; 2970#line 94 2971 __cil_tmp62 = (int )__cil_tmp61; 2972#line 94 2973 if (__cil_tmp62 == 0) { 2974 { 2975#line 95 2976 *((u8 *)chip) = command; 2977#line 96 2978 __cil_tmp63 = & descriptor___0; 2979#line 96 2980 *((char const **)__cil_tmp63) = "i2c_stub"; 2981#line 96 2982 __cil_tmp64 = (unsigned long )(& descriptor___0) + 8; 2983#line 96 2984 *((char const **)__cil_tmp64) = "stub_xfer"; 2985#line 96 2986 __cil_tmp65 = (unsigned long )(& descriptor___0) + 16; 2987#line 96 2988 *((char const **)__cil_tmp65) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p"; 2989#line 96 2990 __cil_tmp66 = (unsigned long )(& descriptor___0) + 24; 2991#line 96 2992 *((char const **)__cil_tmp66) = "smbus byte - addr 0x%02x, wrote 0x%02x.\n"; 2993#line 96 2994 __cil_tmp67 = (unsigned long )(& descriptor___0) + 32; 2995#line 96 2996 *((unsigned int *)__cil_tmp67) = 98U; 2997#line 96 2998 __cil_tmp68 = (unsigned long )(& descriptor___0) + 35; 2999#line 96 3000 *((unsigned char *)__cil_tmp68) = (unsigned char)1; 3001#line 96 3002 __cil_tmp69 = (unsigned long )(& descriptor___0) + 35; 3003#line 96 3004 __cil_tmp70 = *((unsigned char *)__cil_tmp69); 3005#line 96 3006 __cil_tmp71 = (long )__cil_tmp70; 3007#line 96 3008 __cil_tmp72 = __cil_tmp71 & 1L; 3009#line 96 3010 tmp___0 = __builtin_expect(__cil_tmp72, 0L); 3011 } 3012#line 96 3013 if (tmp___0 != 0L) { 3014 { 3015#line 96 3016 __cil_tmp73 = (unsigned long )adap; 3017#line 96 3018 __cil_tmp74 = __cil_tmp73 + 176; 3019#line 96 3020 __cil_tmp75 = (struct device *)__cil_tmp74; 3021#line 96 3022 __cil_tmp76 = (struct device const *)__cil_tmp75; 3023#line 96 3024 __cil_tmp77 = (int )addr; 3025#line 96 3026 __cil_tmp78 = (int )command; 3027#line 96 3028 __dynamic_dev_dbg(& descriptor___0, __cil_tmp76, "smbus byte - addr 0x%02x, wrote 0x%02x.\n", 3029 __cil_tmp77, __cil_tmp78); 3030 } 3031 } else { 3032 3033 } 3034 } else { 3035 { 3036#line 100 3037 tmp___1 = *((u8 *)chip); 3038#line 100 3039 __cil_tmp79 = *((u8 *)chip); 3040#line 100 3041 __cil_tmp80 = (int )__cil_tmp79; 3042#line 100 3043 __cil_tmp81 = __cil_tmp80 + 1; 3044#line 100 3045 *((u8 *)chip) = (u8 )__cil_tmp81; 3046#line 100 3047 __cil_tmp82 = tmp___1 * 2UL; 3048#line 100 3049 __cil_tmp83 = 2 + __cil_tmp82; 3050#line 100 3051 __cil_tmp84 = (unsigned long )chip; 3052#line 100 3053 __cil_tmp85 = __cil_tmp84 + __cil_tmp83; 3054#line 100 3055 __cil_tmp86 = *((u16 *)__cil_tmp85); 3056#line 100 3057 *((__u8 *)data) = (__u8 )__cil_tmp86; 3058#line 101 3059 __cil_tmp87 = & descriptor___1; 3060#line 101 3061 *((char const **)__cil_tmp87) = "i2c_stub"; 3062#line 101 3063 __cil_tmp88 = (unsigned long )(& descriptor___1) + 8; 3064#line 101 3065 *((char const **)__cil_tmp88) = "stub_xfer"; 3066#line 101 3067 __cil_tmp89 = (unsigned long )(& descriptor___1) + 16; 3068#line 101 3069 *((char const **)__cil_tmp89) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p"; 3070#line 101 3071 __cil_tmp90 = (unsigned long )(& descriptor___1) + 24; 3072#line 101 3073 *((char const **)__cil_tmp90) = "smbus byte - addr 0x%02x, read 0x%02x.\n"; 3074#line 101 3075 __cil_tmp91 = (unsigned long )(& descriptor___1) + 32; 3076#line 101 3077 *((unsigned int *)__cil_tmp91) = 103U; 3078#line 101 3079 __cil_tmp92 = (unsigned long )(& descriptor___1) + 35; 3080#line 101 3081 *((unsigned char *)__cil_tmp92) = (unsigned char)1; 3082#line 101 3083 __cil_tmp93 = (unsigned long )(& descriptor___1) + 35; 3084#line 101 3085 __cil_tmp94 = *((unsigned char *)__cil_tmp93); 3086#line 101 3087 __cil_tmp95 = (long )__cil_tmp94; 3088#line 101 3089 __cil_tmp96 = __cil_tmp95 & 1L; 3090#line 101 3091 tmp___2 = __builtin_expect(__cil_tmp96, 0L); 3092 } 3093#line 101 3094 if (tmp___2 != 0L) { 3095 { 3096#line 101 3097 __cil_tmp97 = (unsigned long )adap; 3098#line 101 3099 __cil_tmp98 = __cil_tmp97 + 176; 3100#line 101 3101 __cil_tmp99 = (struct device *)__cil_tmp98; 3102#line 101 3103 __cil_tmp100 = (struct device const *)__cil_tmp99; 3104#line 101 3105 __cil_tmp101 = (int )addr; 3106#line 101 3107 __cil_tmp102 = *((__u8 *)data); 3108#line 101 3109 __cil_tmp103 = (int )__cil_tmp102; 3110#line 101 3111 __dynamic_dev_dbg(& descriptor___1, __cil_tmp100, "smbus byte - addr 0x%02x, read 0x%02x.\n", 3112 __cil_tmp101, __cil_tmp103); 3113 } 3114 } else { 3115 3116 } 3117 } 3118 } 3119#line 106 3120 ret = 0; 3121#line 107 3122 goto ldv_18811; 3123 case_2: /* CIL Label */ ; 3124 { 3125#line 110 3126 __cil_tmp104 = (signed char )read_write; 3127#line 110 3128 __cil_tmp105 = (int )__cil_tmp104; 3129#line 110 3130 if (__cil_tmp105 == 0) { 3131 { 3132#line 111 3133 __cil_tmp106 = (int )command; 3134#line 111 3135 __cil_tmp107 = __cil_tmp106 * 2UL; 3136#line 111 3137 __cil_tmp108 = 2 + __cil_tmp107; 3138#line 111 3139 __cil_tmp109 = (unsigned long )chip; 3140#line 111 3141 __cil_tmp110 = __cil_tmp109 + __cil_tmp108; 3142#line 111 3143 __cil_tmp111 = (int )command; 3144#line 111 3145 __cil_tmp112 = __cil_tmp111 * 2UL; 3146#line 111 3147 __cil_tmp113 = 2 + __cil_tmp112; 3148#line 111 3149 __cil_tmp114 = (unsigned long )chip; 3150#line 111 3151 __cil_tmp115 = __cil_tmp114 + __cil_tmp113; 3152#line 111 3153 __cil_tmp116 = *((u16 *)__cil_tmp115); 3154#line 111 3155 __cil_tmp117 = (unsigned int )__cil_tmp116; 3156#line 111 3157 __cil_tmp118 = __cil_tmp117 & 65280U; 3158#line 111 3159 *((u16 *)__cil_tmp110) = (u16 )__cil_tmp118; 3160#line 112 3161 __cil_tmp119 = (int )command; 3162#line 112 3163 __cil_tmp120 = __cil_tmp119 * 2UL; 3164#line 112 3165 __cil_tmp121 = 2 + __cil_tmp120; 3166#line 112 3167 __cil_tmp122 = (unsigned long )chip; 3168#line 112 3169 __cil_tmp123 = __cil_tmp122 + __cil_tmp121; 3170#line 112 3171 __cil_tmp124 = *((__u8 *)data); 3172#line 112 3173 __cil_tmp125 = (u16 )__cil_tmp124; 3174#line 112 3175 __cil_tmp126 = (int )__cil_tmp125; 3176#line 112 3177 __cil_tmp127 = (int )command; 3178#line 112 3179 __cil_tmp128 = __cil_tmp127 * 2UL; 3180#line 112 3181 __cil_tmp129 = 2 + __cil_tmp128; 3182#line 112 3183 __cil_tmp130 = (unsigned long )chip; 3184#line 112 3185 __cil_tmp131 = __cil_tmp130 + __cil_tmp129; 3186#line 112 3187 __cil_tmp132 = *((u16 *)__cil_tmp131); 3188#line 112 3189 __cil_tmp133 = (int )__cil_tmp132; 3190#line 112 3191 __cil_tmp134 = __cil_tmp133 | __cil_tmp126; 3192#line 112 3193 *((u16 *)__cil_tmp123) = (u16 )__cil_tmp134; 3194#line 113 3195 __cil_tmp135 = & descriptor___2; 3196#line 113 3197 *((char const **)__cil_tmp135) = "i2c_stub"; 3198#line 113 3199 __cil_tmp136 = (unsigned long )(& descriptor___2) + 8; 3200#line 113 3201 *((char const **)__cil_tmp136) = "stub_xfer"; 3202#line 113 3203 __cil_tmp137 = (unsigned long )(& descriptor___2) + 16; 3204#line 113 3205 *((char const **)__cil_tmp137) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p"; 3206#line 113 3207 __cil_tmp138 = (unsigned long )(& descriptor___2) + 24; 3208#line 113 3209 *((char const **)__cil_tmp138) = "smbus byte data - addr 0x%02x, wrote 0x%02x at 0x%02x.\n"; 3210#line 113 3211 __cil_tmp139 = (unsigned long )(& descriptor___2) + 32; 3212#line 113 3213 *((unsigned int *)__cil_tmp139) = 115U; 3214#line 113 3215 __cil_tmp140 = (unsigned long )(& descriptor___2) + 35; 3216#line 113 3217 *((unsigned char *)__cil_tmp140) = (unsigned char)1; 3218#line 113 3219 __cil_tmp141 = (unsigned long )(& descriptor___2) + 35; 3220#line 113 3221 __cil_tmp142 = *((unsigned char *)__cil_tmp141); 3222#line 113 3223 __cil_tmp143 = (long )__cil_tmp142; 3224#line 113 3225 __cil_tmp144 = __cil_tmp143 & 1L; 3226#line 113 3227 tmp___3 = __builtin_expect(__cil_tmp144, 0L); 3228 } 3229#line 113 3230 if (tmp___3 != 0L) { 3231 { 3232#line 113 3233 __cil_tmp145 = (unsigned long )adap; 3234#line 113 3235 __cil_tmp146 = __cil_tmp145 + 176; 3236#line 113 3237 __cil_tmp147 = (struct device *)__cil_tmp146; 3238#line 113 3239 __cil_tmp148 = (struct device const *)__cil_tmp147; 3240#line 113 3241 __cil_tmp149 = (int )addr; 3242#line 113 3243 __cil_tmp150 = *((__u8 *)data); 3244#line 113 3245 __cil_tmp151 = (int )__cil_tmp150; 3246#line 113 3247 __cil_tmp152 = (int )command; 3248#line 113 3249 __dynamic_dev_dbg(& descriptor___2, __cil_tmp148, "smbus byte data - addr 0x%02x, wrote 0x%02x at 0x%02x.\n", 3250 __cil_tmp149, __cil_tmp151, __cil_tmp152); 3251 } 3252 } else { 3253 3254 } 3255 } else { 3256 { 3257#line 117 3258 __cil_tmp153 = (int )command; 3259#line 117 3260 __cil_tmp154 = __cil_tmp153 * 2UL; 3261#line 117 3262 __cil_tmp155 = 2 + __cil_tmp154; 3263#line 117 3264 __cil_tmp156 = (unsigned long )chip; 3265#line 117 3266 __cil_tmp157 = __cil_tmp156 + __cil_tmp155; 3267#line 117 3268 __cil_tmp158 = *((u16 *)__cil_tmp157); 3269#line 117 3270 *((__u8 *)data) = (__u8 )__cil_tmp158; 3271#line 118 3272 __cil_tmp159 = & descriptor___3; 3273#line 118 3274 *((char const **)__cil_tmp159) = "i2c_stub"; 3275#line 118 3276 __cil_tmp160 = (unsigned long )(& descriptor___3) + 8; 3277#line 118 3278 *((char const **)__cil_tmp160) = "stub_xfer"; 3279#line 118 3280 __cil_tmp161 = (unsigned long )(& descriptor___3) + 16; 3281#line 118 3282 *((char const **)__cil_tmp161) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p"; 3283#line 118 3284 __cil_tmp162 = (unsigned long )(& descriptor___3) + 24; 3285#line 118 3286 *((char const **)__cil_tmp162) = "smbus byte data - addr 0x%02x, read 0x%02x at 0x%02x.\n"; 3287#line 118 3288 __cil_tmp163 = (unsigned long )(& descriptor___3) + 32; 3289#line 118 3290 *((unsigned int *)__cil_tmp163) = 120U; 3291#line 118 3292 __cil_tmp164 = (unsigned long )(& descriptor___3) + 35; 3293#line 118 3294 *((unsigned char *)__cil_tmp164) = (unsigned char)1; 3295#line 118 3296 __cil_tmp165 = (unsigned long )(& descriptor___3) + 35; 3297#line 118 3298 __cil_tmp166 = *((unsigned char *)__cil_tmp165); 3299#line 118 3300 __cil_tmp167 = (long )__cil_tmp166; 3301#line 118 3302 __cil_tmp168 = __cil_tmp167 & 1L; 3303#line 118 3304 tmp___4 = __builtin_expect(__cil_tmp168, 0L); 3305 } 3306#line 118 3307 if (tmp___4 != 0L) { 3308 { 3309#line 118 3310 __cil_tmp169 = (unsigned long )adap; 3311#line 118 3312 __cil_tmp170 = __cil_tmp169 + 176; 3313#line 118 3314 __cil_tmp171 = (struct device *)__cil_tmp170; 3315#line 118 3316 __cil_tmp172 = (struct device const *)__cil_tmp171; 3317#line 118 3318 __cil_tmp173 = (int )addr; 3319#line 118 3320 __cil_tmp174 = *((__u8 *)data); 3321#line 118 3322 __cil_tmp175 = (int )__cil_tmp174; 3323#line 118 3324 __cil_tmp176 = (int )command; 3325#line 118 3326 __dynamic_dev_dbg(& descriptor___3, __cil_tmp172, "smbus byte data - addr 0x%02x, read 0x%02x at 0x%02x.\n", 3327 __cil_tmp173, __cil_tmp175, __cil_tmp176); 3328 } 3329 } else { 3330 3331 } 3332 } 3333 } 3334#line 122 3335 __cil_tmp177 = (unsigned int )command; 3336#line 122 3337 __cil_tmp178 = __cil_tmp177 + 1U; 3338#line 122 3339 *((u8 *)chip) = (u8 )__cil_tmp178; 3340#line 124 3341 ret = 0; 3342#line 125 3343 goto ldv_18811; 3344 case_3: /* CIL Label */ ; 3345 { 3346#line 128 3347 __cil_tmp179 = (signed char )read_write; 3348#line 128 3349 __cil_tmp180 = (int )__cil_tmp179; 3350#line 128 3351 if (__cil_tmp180 == 0) { 3352 { 3353#line 129 3354 __cil_tmp181 = (int )command; 3355#line 129 3356 __cil_tmp182 = __cil_tmp181 * 2UL; 3357#line 129 3358 __cil_tmp183 = 2 + __cil_tmp182; 3359#line 129 3360 __cil_tmp184 = (unsigned long )chip; 3361#line 129 3362 __cil_tmp185 = __cil_tmp184 + __cil_tmp183; 3363#line 129 3364 *((u16 *)__cil_tmp185) = *((__u16 *)data); 3365#line 130 3366 __cil_tmp186 = & descriptor___4; 3367#line 130 3368 *((char const **)__cil_tmp186) = "i2c_stub"; 3369#line 130 3370 __cil_tmp187 = (unsigned long )(& descriptor___4) + 8; 3371#line 130 3372 *((char const **)__cil_tmp187) = "stub_xfer"; 3373#line 130 3374 __cil_tmp188 = (unsigned long )(& descriptor___4) + 16; 3375#line 130 3376 *((char const **)__cil_tmp188) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p"; 3377#line 130 3378 __cil_tmp189 = (unsigned long )(& descriptor___4) + 24; 3379#line 130 3380 *((char const **)__cil_tmp189) = "smbus word data - addr 0x%02x, wrote 0x%04x at 0x%02x.\n"; 3381#line 130 3382 __cil_tmp190 = (unsigned long )(& descriptor___4) + 32; 3383#line 130 3384 *((unsigned int *)__cil_tmp190) = 132U; 3385#line 130 3386 __cil_tmp191 = (unsigned long )(& descriptor___4) + 35; 3387#line 130 3388 *((unsigned char *)__cil_tmp191) = (unsigned char)1; 3389#line 130 3390 __cil_tmp192 = (unsigned long )(& descriptor___4) + 35; 3391#line 130 3392 __cil_tmp193 = *((unsigned char *)__cil_tmp192); 3393#line 130 3394 __cil_tmp194 = (long )__cil_tmp193; 3395#line 130 3396 __cil_tmp195 = __cil_tmp194 & 1L; 3397#line 130 3398 tmp___5 = __builtin_expect(__cil_tmp195, 0L); 3399 } 3400#line 130 3401 if (tmp___5 != 0L) { 3402 { 3403#line 130 3404 __cil_tmp196 = (unsigned long )adap; 3405#line 130 3406 __cil_tmp197 = __cil_tmp196 + 176; 3407#line 130 3408 __cil_tmp198 = (struct device *)__cil_tmp197; 3409#line 130 3410 __cil_tmp199 = (struct device const *)__cil_tmp198; 3411#line 130 3412 __cil_tmp200 = (int )addr; 3413#line 130 3414 __cil_tmp201 = *((__u16 *)data); 3415#line 130 3416 __cil_tmp202 = (int )__cil_tmp201; 3417#line 130 3418 __cil_tmp203 = (int )command; 3419#line 130 3420 __dynamic_dev_dbg(& descriptor___4, __cil_tmp199, "smbus word data - addr 0x%02x, wrote 0x%04x at 0x%02x.\n", 3421 __cil_tmp200, __cil_tmp202, __cil_tmp203); 3422 } 3423 } else { 3424 3425 } 3426 } else { 3427 { 3428#line 134 3429 __cil_tmp204 = (int )command; 3430#line 134 3431 __cil_tmp205 = __cil_tmp204 * 2UL; 3432#line 134 3433 __cil_tmp206 = 2 + __cil_tmp205; 3434#line 134 3435 __cil_tmp207 = (unsigned long )chip; 3436#line 134 3437 __cil_tmp208 = __cil_tmp207 + __cil_tmp206; 3438#line 134 3439 *((__u16 *)data) = *((u16 *)__cil_tmp208); 3440#line 135 3441 __cil_tmp209 = & descriptor___5; 3442#line 135 3443 *((char const **)__cil_tmp209) = "i2c_stub"; 3444#line 135 3445 __cil_tmp210 = (unsigned long )(& descriptor___5) + 8; 3446#line 135 3447 *((char const **)__cil_tmp210) = "stub_xfer"; 3448#line 135 3449 __cil_tmp211 = (unsigned long )(& descriptor___5) + 16; 3450#line 135 3451 *((char const **)__cil_tmp211) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p"; 3452#line 135 3453 __cil_tmp212 = (unsigned long )(& descriptor___5) + 24; 3454#line 135 3455 *((char const **)__cil_tmp212) = "smbus word data - addr 0x%02x, read 0x%04x at 0x%02x.\n"; 3456#line 135 3457 __cil_tmp213 = (unsigned long )(& descriptor___5) + 32; 3458#line 135 3459 *((unsigned int *)__cil_tmp213) = 137U; 3460#line 135 3461 __cil_tmp214 = (unsigned long )(& descriptor___5) + 35; 3462#line 135 3463 *((unsigned char *)__cil_tmp214) = (unsigned char)1; 3464#line 135 3465 __cil_tmp215 = (unsigned long )(& descriptor___5) + 35; 3466#line 135 3467 __cil_tmp216 = *((unsigned char *)__cil_tmp215); 3468#line 135 3469 __cil_tmp217 = (long )__cil_tmp216; 3470#line 135 3471 __cil_tmp218 = __cil_tmp217 & 1L; 3472#line 135 3473 tmp___6 = __builtin_expect(__cil_tmp218, 0L); 3474 } 3475#line 135 3476 if (tmp___6 != 0L) { 3477 { 3478#line 135 3479 __cil_tmp219 = (unsigned long )adap; 3480#line 135 3481 __cil_tmp220 = __cil_tmp219 + 176; 3482#line 135 3483 __cil_tmp221 = (struct device *)__cil_tmp220; 3484#line 135 3485 __cil_tmp222 = (struct device const *)__cil_tmp221; 3486#line 135 3487 __cil_tmp223 = (int )addr; 3488#line 135 3489 __cil_tmp224 = *((__u16 *)data); 3490#line 135 3491 __cil_tmp225 = (int )__cil_tmp224; 3492#line 135 3493 __cil_tmp226 = (int )command; 3494#line 135 3495 __dynamic_dev_dbg(& descriptor___5, __cil_tmp222, "smbus word data - addr 0x%02x, read 0x%04x at 0x%02x.\n", 3496 __cil_tmp223, __cil_tmp225, __cil_tmp226); 3497 } 3498 } else { 3499 3500 } 3501 } 3502 } 3503#line 140 3504 ret = 0; 3505#line 141 3506 goto ldv_18811; 3507 case_8: /* CIL Label */ 3508#line 144 3509 __cil_tmp227 = 0 * 1UL; 3510#line 144 3511 __cil_tmp228 = 0 + __cil_tmp227; 3512#line 144 3513 __cil_tmp229 = (unsigned long )data; 3514#line 144 3515 __cil_tmp230 = __cil_tmp229 + __cil_tmp228; 3516#line 144 3517 __cil_tmp231 = *((__u8 *)__cil_tmp230); 3518#line 144 3519 len = (int )__cil_tmp231; 3520 { 3521#line 145 3522 __cil_tmp232 = (signed char )read_write; 3523#line 145 3524 __cil_tmp233 = (int )__cil_tmp232; 3525#line 145 3526 if (__cil_tmp233 == 0) { 3527#line 146 3528 i = 0; 3529#line 146 3530 goto ldv_18823; 3531 ldv_18822: 3532#line 147 3533 __cil_tmp234 = (int )command; 3534#line 147 3535 __cil_tmp235 = __cil_tmp234 + i; 3536#line 147 3537 __cil_tmp236 = __cil_tmp235 * 2UL; 3538#line 147 3539 __cil_tmp237 = 2 + __cil_tmp236; 3540#line 147 3541 __cil_tmp238 = (unsigned long )chip; 3542#line 147 3543 __cil_tmp239 = __cil_tmp238 + __cil_tmp237; 3544#line 147 3545 __cil_tmp240 = (int )command; 3546#line 147 3547 __cil_tmp241 = __cil_tmp240 + i; 3548#line 147 3549 __cil_tmp242 = __cil_tmp241 * 2UL; 3550#line 147 3551 __cil_tmp243 = 2 + __cil_tmp242; 3552#line 147 3553 __cil_tmp244 = (unsigned long )chip; 3554#line 147 3555 __cil_tmp245 = __cil_tmp244 + __cil_tmp243; 3556#line 147 3557 __cil_tmp246 = *((u16 *)__cil_tmp245); 3558#line 147 3559 __cil_tmp247 = (unsigned int )__cil_tmp246; 3560#line 147 3561 __cil_tmp248 = __cil_tmp247 & 65280U; 3562#line 147 3563 *((u16 *)__cil_tmp239) = (u16 )__cil_tmp248; 3564#line 148 3565 __cil_tmp249 = (int )command; 3566#line 148 3567 __cil_tmp250 = __cil_tmp249 + i; 3568#line 148 3569 __cil_tmp251 = __cil_tmp250 * 2UL; 3570#line 148 3571 __cil_tmp252 = 2 + __cil_tmp251; 3572#line 148 3573 __cil_tmp253 = (unsigned long )chip; 3574#line 148 3575 __cil_tmp254 = __cil_tmp253 + __cil_tmp252; 3576#line 148 3577 __cil_tmp255 = i + 1; 3578#line 148 3579 __cil_tmp256 = __cil_tmp255 * 1UL; 3580#line 148 3581 __cil_tmp257 = 0 + __cil_tmp256; 3582#line 148 3583 __cil_tmp258 = (unsigned long )data; 3584#line 148 3585 __cil_tmp259 = __cil_tmp258 + __cil_tmp257; 3586#line 148 3587 __cil_tmp260 = *((__u8 *)__cil_tmp259); 3588#line 148 3589 __cil_tmp261 = (u16 )__cil_tmp260; 3590#line 148 3591 __cil_tmp262 = (int )__cil_tmp261; 3592#line 148 3593 __cil_tmp263 = (int )command; 3594#line 148 3595 __cil_tmp264 = __cil_tmp263 + i; 3596#line 148 3597 __cil_tmp265 = __cil_tmp264 * 2UL; 3598#line 148 3599 __cil_tmp266 = 2 + __cil_tmp265; 3600#line 148 3601 __cil_tmp267 = (unsigned long )chip; 3602#line 148 3603 __cil_tmp268 = __cil_tmp267 + __cil_tmp266; 3604#line 148 3605 __cil_tmp269 = *((u16 *)__cil_tmp268); 3606#line 148 3607 __cil_tmp270 = (int )__cil_tmp269; 3608#line 148 3609 __cil_tmp271 = __cil_tmp270 | __cil_tmp262; 3610#line 148 3611 *((u16 *)__cil_tmp254) = (u16 )__cil_tmp271; 3612#line 146 3613 i = i + 1; 3614 ldv_18823: ; 3615#line 146 3616 if (i < len) { 3617#line 147 3618 goto ldv_18822; 3619 } else { 3620#line 149 3621 goto ldv_18824; 3622 } 3623 ldv_18824: 3624 { 3625#line 150 3626 __cil_tmp272 = & descriptor___6; 3627#line 150 3628 *((char const **)__cil_tmp272) = "i2c_stub"; 3629#line 150 3630 __cil_tmp273 = (unsigned long )(& descriptor___6) + 8; 3631#line 150 3632 *((char const **)__cil_tmp273) = "stub_xfer"; 3633#line 150 3634 __cil_tmp274 = (unsigned long )(& descriptor___6) + 16; 3635#line 150 3636 *((char const **)__cil_tmp274) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p"; 3637#line 150 3638 __cil_tmp275 = (unsigned long )(& descriptor___6) + 24; 3639#line 150 3640 *((char const **)__cil_tmp275) = "i2c block data - addr 0x%02x, wrote %d bytes at 0x%02x.\n"; 3641#line 150 3642 __cil_tmp276 = (unsigned long )(& descriptor___6) + 32; 3643#line 150 3644 *((unsigned int *)__cil_tmp276) = 152U; 3645#line 150 3646 __cil_tmp277 = (unsigned long )(& descriptor___6) + 35; 3647#line 150 3648 *((unsigned char *)__cil_tmp277) = (unsigned char)1; 3649#line 150 3650 __cil_tmp278 = (unsigned long )(& descriptor___6) + 35; 3651#line 150 3652 __cil_tmp279 = *((unsigned char *)__cil_tmp278); 3653#line 150 3654 __cil_tmp280 = (long )__cil_tmp279; 3655#line 150 3656 __cil_tmp281 = __cil_tmp280 & 1L; 3657#line 150 3658 tmp___7 = __builtin_expect(__cil_tmp281, 0L); 3659 } 3660#line 150 3661 if (tmp___7 != 0L) { 3662 { 3663#line 150 3664 __cil_tmp282 = (unsigned long )adap; 3665#line 150 3666 __cil_tmp283 = __cil_tmp282 + 176; 3667#line 150 3668 __cil_tmp284 = (struct device *)__cil_tmp283; 3669#line 150 3670 __cil_tmp285 = (struct device const *)__cil_tmp284; 3671#line 150 3672 __cil_tmp286 = (int )addr; 3673#line 150 3674 __cil_tmp287 = (int )command; 3675#line 150 3676 __dynamic_dev_dbg(& descriptor___6, __cil_tmp285, "i2c block data - addr 0x%02x, wrote %d bytes at 0x%02x.\n", 3677 __cil_tmp286, len, __cil_tmp287); 3678 } 3679 } else { 3680 3681 } 3682 } else { 3683#line 154 3684 i = 0; 3685#line 154 3686 goto ldv_18827; 3687 ldv_18826: 3688#line 155 3689 __cil_tmp288 = i + 1; 3690#line 155 3691 __cil_tmp289 = __cil_tmp288 * 1UL; 3692#line 155 3693 __cil_tmp290 = 0 + __cil_tmp289; 3694#line 155 3695 __cil_tmp291 = (unsigned long )data; 3696#line 155 3697 __cil_tmp292 = __cil_tmp291 + __cil_tmp290; 3698#line 155 3699 __cil_tmp293 = (int )command; 3700#line 155 3701 __cil_tmp294 = __cil_tmp293 + i; 3702#line 155 3703 __cil_tmp295 = __cil_tmp294 * 2UL; 3704#line 155 3705 __cil_tmp296 = 2 + __cil_tmp295; 3706#line 155 3707 __cil_tmp297 = (unsigned long )chip; 3708#line 155 3709 __cil_tmp298 = __cil_tmp297 + __cil_tmp296; 3710#line 155 3711 __cil_tmp299 = *((u16 *)__cil_tmp298); 3712#line 155 3713 *((__u8 *)__cil_tmp292) = (__u8 )__cil_tmp299; 3714#line 154 3715 i = i + 1; 3716 ldv_18827: ; 3717#line 154 3718 if (i < len) { 3719#line 155 3720 goto ldv_18826; 3721 } else { 3722#line 157 3723 goto ldv_18828; 3724 } 3725 ldv_18828: 3726 { 3727#line 158 3728 __cil_tmp300 = & descriptor___7; 3729#line 158 3730 *((char const **)__cil_tmp300) = "i2c_stub"; 3731#line 158 3732 __cil_tmp301 = (unsigned long )(& descriptor___7) + 8; 3733#line 158 3734 *((char const **)__cil_tmp301) = "stub_xfer"; 3735#line 158 3736 __cil_tmp302 = (unsigned long )(& descriptor___7) + 16; 3737#line 158 3738 *((char const **)__cil_tmp302) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p"; 3739#line 158 3740 __cil_tmp303 = (unsigned long )(& descriptor___7) + 24; 3741#line 158 3742 *((char const **)__cil_tmp303) = "i2c block data - addr 0x%02x, read %d bytes at 0x%02x.\n"; 3743#line 158 3744 __cil_tmp304 = (unsigned long )(& descriptor___7) + 32; 3745#line 158 3746 *((unsigned int *)__cil_tmp304) = 160U; 3747#line 158 3748 __cil_tmp305 = (unsigned long )(& descriptor___7) + 35; 3749#line 158 3750 *((unsigned char *)__cil_tmp305) = (unsigned char)1; 3751#line 158 3752 __cil_tmp306 = (unsigned long )(& descriptor___7) + 35; 3753#line 158 3754 __cil_tmp307 = *((unsigned char *)__cil_tmp306); 3755#line 158 3756 __cil_tmp308 = (long )__cil_tmp307; 3757#line 158 3758 __cil_tmp309 = __cil_tmp308 & 1L; 3759#line 158 3760 tmp___8 = __builtin_expect(__cil_tmp309, 0L); 3761 } 3762#line 158 3763 if (tmp___8 != 0L) { 3764 { 3765#line 158 3766 __cil_tmp310 = (unsigned long )adap; 3767#line 158 3768 __cil_tmp311 = __cil_tmp310 + 176; 3769#line 158 3770 __cil_tmp312 = (struct device *)__cil_tmp311; 3771#line 158 3772 __cil_tmp313 = (struct device const *)__cil_tmp312; 3773#line 158 3774 __cil_tmp314 = (int )addr; 3775#line 158 3776 __cil_tmp315 = (int )command; 3777#line 158 3778 __dynamic_dev_dbg(& descriptor___7, __cil_tmp313, "i2c block data - addr 0x%02x, read %d bytes at 0x%02x.\n", 3779 __cil_tmp314, len, __cil_tmp315); 3780 } 3781 } else { 3782 3783 } 3784 } 3785 } 3786#line 163 3787 ret = 0; 3788#line 164 3789 goto ldv_18811; 3790 switch_default: /* CIL Label */ 3791 { 3792#line 167 3793 __cil_tmp316 = & descriptor___8; 3794#line 167 3795 *((char const **)__cil_tmp316) = "i2c_stub"; 3796#line 167 3797 __cil_tmp317 = (unsigned long )(& descriptor___8) + 8; 3798#line 167 3799 *((char const **)__cil_tmp317) = "stub_xfer"; 3800#line 167 3801 __cil_tmp318 = (unsigned long )(& descriptor___8) + 16; 3802#line 167 3803 *((char const **)__cil_tmp318) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p"; 3804#line 167 3805 __cil_tmp319 = (unsigned long )(& descriptor___8) + 24; 3806#line 167 3807 *((char const **)__cil_tmp319) = "Unsupported I2C/SMBus command\n"; 3808#line 167 3809 __cil_tmp320 = (unsigned long )(& descriptor___8) + 32; 3810#line 167 3811 *((unsigned int *)__cil_tmp320) = 167U; 3812#line 167 3813 __cil_tmp321 = (unsigned long )(& descriptor___8) + 35; 3814#line 167 3815 *((unsigned char *)__cil_tmp321) = (unsigned char)1; 3816#line 167 3817 __cil_tmp322 = (unsigned long )(& descriptor___8) + 35; 3818#line 167 3819 __cil_tmp323 = *((unsigned char *)__cil_tmp322); 3820#line 167 3821 __cil_tmp324 = (long )__cil_tmp323; 3822#line 167 3823 __cil_tmp325 = __cil_tmp324 & 1L; 3824#line 167 3825 tmp___9 = __builtin_expect(__cil_tmp325, 0L); 3826 } 3827#line 167 3828 if (tmp___9 != 0L) { 3829 { 3830#line 167 3831 __cil_tmp326 = (unsigned long )adap; 3832#line 167 3833 __cil_tmp327 = __cil_tmp326 + 176; 3834#line 167 3835 __cil_tmp328 = (struct device *)__cil_tmp327; 3836#line 167 3837 __cil_tmp329 = (struct device const *)__cil_tmp328; 3838#line 167 3839 __dynamic_dev_dbg(& descriptor___8, __cil_tmp329, "Unsupported I2C/SMBus command\n"); 3840 } 3841 } else { 3842 3843 } 3844#line 168 3845 ret = -95; 3846#line 169 3847 goto ldv_18811; 3848 } else { 3849 switch_break: /* CIL Label */ ; 3850 } 3851 } 3852 } 3853 ldv_18811: ; 3854#line 172 3855 return (ret); 3856} 3857} 3858#line 175 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p" 3859static u32 stub_func(struct i2c_adapter *adapter ) 3860{ unsigned long *__cil_tmp2 ; 3861 unsigned long __cil_tmp3 ; 3862 u32 __cil_tmp4 ; 3863 3864 { 3865 { 3866#line 177 3867 __cil_tmp2 = & functionality; 3868#line 177 3869 __cil_tmp3 = *__cil_tmp2; 3870#line 177 3871 __cil_tmp4 = (u32 )__cil_tmp3; 3872#line 177 3873 return (__cil_tmp4 & 209649664U); 3874 } 3875} 3876} 3877#line 180 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p" 3878static struct i2c_algorithm const smbus_algorithm = {(int (*)(struct i2c_adapter * , struct i2c_msg * , int ))0, & stub_xfer, & stub_func}; 3879#line 185 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p" 3880static struct i2c_adapter stub_adapter = 3881#line 185 3882 {& __this_module, 129U, & smbus_algorithm, (void *)0, {{{{0U}}, 0U, 0U, (void *)0, 3883 {(struct lock_class_key *)0, 3884 {(struct lock_class *)0, 3885 (struct lock_class *)0}, 3886 (char const *)0, 0, 3887 0UL}}, {{(struct list_head *)0, 3888 (struct list_head *)0}}, 3889 (struct task_struct *)0, 3890 0, (char const *)0, (char const *)0, 3891 0, (void *)0}, 0, 0, {(struct device *)0, 3892 (struct device_private *)0, 3893 {(char const *)0, 3894 {(struct list_head *)0, 3895 (struct list_head *)0}, 3896 (struct kobject *)0, 3897 (struct kset *)0, 3898 (struct kobj_type *)0, 3899 (struct sysfs_dirent *)0, 3900 {{0}}, 3901 (unsigned char)0, 3902 (unsigned char)0, 3903 (unsigned char)0, 3904 (unsigned char)0, 3905 (unsigned char)0}, 3906 (char const *)0, 3907 (struct device_type const *)0, 3908 {{0}, 3909 {{{{{0U}}, 3910 0U, 3911 0U, 3912 (void *)0, 3913 {(struct lock_class_key *)0, 3914 {(struct lock_class *)0, 3915 (struct lock_class *)0}, 3916 (char const *)0, 3917 0, 3918 0UL}}}}, 3919 {(struct list_head *)0, 3920 (struct list_head *)0}, 3921 (struct task_struct *)0, 3922 (char const *)0, 3923 (void *)0, 3924 {(struct lock_class_key *)0, 3925 {(struct lock_class *)0, 3926 (struct lock_class *)0}, 3927 (char const *)0, 3928 0, 3929 0UL}}, 3930 (struct bus_type *)0, 3931 (struct device_driver *)0, 3932 (void *)0, 3933 {{0}, 3934 (unsigned char)0, 3935 (unsigned char)0, 3936 (_Bool)0, 3937 (_Bool)0, 3938 (_Bool)0, 3939 {{{{{0U}}, 3940 0U, 3941 0U, 3942 (void *)0, 3943 {(struct lock_class_key *)0, 3944 {(struct lock_class *)0, 3945 (struct lock_class *)0}, 3946 (char const *)0, 3947 0, 3948 0UL}}}}, 3949 {(struct list_head *)0, 3950 (struct list_head *)0}, 3951 {0U, 3952 {{{{{{0U}}, 3953 0U, 3954 0U, 3955 (void *)0, 3956 {(struct lock_class_key *)0, 3957 {(struct lock_class *)0, 3958 (struct lock_class *)0}, 3959 (char const *)0, 3960 0, 3961 0UL}}}}, 3962 {(struct list_head *)0, 3963 (struct list_head *)0}}}, 3964 (struct wakeup_source *)0, 3965 (_Bool)0, 3966 {{(struct list_head *)0, 3967 (struct list_head *)0}, 3968 0UL, 3969 (struct tvec_base *)0, 3970 (void (*)(unsigned long ))0, 3971 0UL, 3972 0, 3973 0, 3974 (void *)0, 3975 {(char)0, 3976 (char)0, 3977 (char)0, 3978 (char)0, 3979 (char)0, 3980 (char)0, 3981 (char)0, 3982 (char)0, 3983 (char)0, 3984 (char)0, 3985 (char)0, 3986 (char)0, 3987 (char)0, 3988 (char)0, 3989 (char)0, 3990 (char)0}, 3991 {(struct lock_class_key *)0, 3992 {(struct lock_class *)0, 3993 (struct lock_class *)0}, 3994 (char const *)0, 3995 0, 3996 0UL}}, 3997 0UL, 3998 {{0L}, 3999 {(struct list_head *)0, 4000 (struct list_head *)0}, 4001 (void (*)(struct work_struct * ))0, 4002 {(struct lock_class_key *)0, 4003 {(struct lock_class *)0, 4004 (struct lock_class *)0}, 4005 (char const *)0, 4006 0, 4007 0UL}}, 4008 {{{{{{0U}}, 4009 0U, 4010 0U, 4011 (void *)0, 4012 {(struct lock_class_key *)0, 4013 {(struct lock_class *)0, 4014 (struct lock_class *)0}, 4015 (char const *)0, 4016 0, 4017 0UL}}}}, 4018 {(struct list_head *)0, 4019 (struct list_head *)0}}, 4020 {0}, 4021 {0}, 4022 (unsigned char)0, 4023 (unsigned char)0, 4024 (unsigned char)0, 4025 (unsigned char)0, 4026 (unsigned char)0, 4027 (unsigned char)0, 4028 (unsigned char)0, 4029 (unsigned char)0, 4030 (unsigned char)0, 4031 (unsigned char)0, 4032 0, 4033 0, 4034 0, 4035 0, 4036 0UL, 4037 0UL, 4038 0UL, 4039 0UL, 4040 {0LL}, 4041 0LL, 4042 (struct dev_pm_qos_request *)0, 4043 (struct pm_subsys_data *)0, 4044 (struct pm_qos_constraints *)0}, 4045 (struct dev_pm_domain *)0, 4046 0, 4047 (u64 *)0, 4048 0ULL, 4049 (struct device_dma_parameters *)0, 4050 {(struct list_head *)0, 4051 (struct list_head *)0}, 4052 (struct dma_coherent_mem *)0, 4053 {(void *)0, 4054 (struct dma_map_ops *)0, 4055 (void *)0}, 4056 (struct device_node *)0, 4057 0U, 4058 0U, 4059 {{{{{0U}}, 4060 0U, 4061 0U, 4062 (void *)0, 4063 {(struct lock_class_key *)0, 4064 {(struct lock_class *)0, 4065 (struct lock_class *)0}, 4066 (char const *)0, 4067 0, 4068 0UL}}}}, 4069 {(struct list_head *)0, 4070 (struct list_head *)0}, 4071 {(void *)0, 4072 {(struct list_head *)0, 4073 (struct list_head *)0}, 4074 {{0}}}, 4075 (struct class *)0, 4076 (struct attribute_group const **)0, 4077 (void (*)(struct device * ))0}, 4078 0, {(char )'S', (char )'M', (char )'B', (char )'u', (char )'s', (char )' ', (char )'s', 4079 (char )'t', (char )'u', (char )'b', (char )' ', (char )'d', (char )'r', (char )'i', 4080 (char )'v', (char )'e', (char )'r', (char )'\000'}, {0U, {{{{{{0U}}, 0U, 0U, 4081 (void *)0, {(struct lock_class_key *)0, 4082 {(struct lock_class *)0, 4083 (struct lock_class *)0}, 4084 (char const *)0, 4085 0, 4086 0UL}}}}, 4087 {(struct list_head *)0, 4088 (struct list_head *)0}}}, 4089 {{0}, {{{{{0U}}, 0U, 0U, (void *)0, {(struct lock_class_key *)0, {(struct lock_class *)0, 4090 (struct lock_class *)0}, 4091 (char const *)0, 0, 0UL}}}}, {(struct list_head *)0, 4092 (struct list_head *)0}, 4093 (struct task_struct *)0, (char const *)0, (void *)0, {(struct lock_class_key *)0, 4094 {(struct lock_class *)0, 4095 (struct lock_class *)0}, 4096 (char const *)0, 0, 4097 0UL}}, {(struct list_head *)0, 4098 (struct list_head *)0}}; 4099#line 192 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p" 4100static int i2c_stub_init(void) 4101{ int i ; 4102 int ret ; 4103 void *tmp ; 4104 unsigned long __cil_tmp4 ; 4105 unsigned long __cil_tmp5 ; 4106 unsigned short __cil_tmp6 ; 4107 unsigned int __cil_tmp7 ; 4108 unsigned long __cil_tmp8 ; 4109 unsigned long __cil_tmp9 ; 4110 unsigned short __cil_tmp10 ; 4111 unsigned int __cil_tmp11 ; 4112 unsigned long __cil_tmp12 ; 4113 unsigned long __cil_tmp13 ; 4114 unsigned short __cil_tmp14 ; 4115 int __cil_tmp15 ; 4116 unsigned long __cil_tmp16 ; 4117 unsigned long __cil_tmp17 ; 4118 unsigned short __cil_tmp18 ; 4119 unsigned int __cil_tmp19 ; 4120 unsigned long __cil_tmp20 ; 4121 unsigned long __cil_tmp21 ; 4122 unsigned short __cil_tmp22 ; 4123 int __cil_tmp23 ; 4124 unsigned long __cil_tmp24 ; 4125 unsigned long __cil_tmp25 ; 4126 unsigned short __cil_tmp26 ; 4127 int __cil_tmp27 ; 4128 unsigned long __cil_tmp28 ; 4129 unsigned long __cil_tmp29 ; 4130 unsigned short __cil_tmp30 ; 4131 unsigned int __cil_tmp31 ; 4132 unsigned long __cil_tmp32 ; 4133 unsigned long __cil_tmp33 ; 4134 struct stub_chip *__cil_tmp34 ; 4135 unsigned long __cil_tmp35 ; 4136 unsigned long __cil_tmp36 ; 4137 void const *__cil_tmp37 ; 4138 4139 { 4140 { 4141#line 196 4142 __cil_tmp4 = 0 * 2UL; 4143#line 196 4144 __cil_tmp5 = (unsigned long )(chip_addr) + __cil_tmp4; 4145#line 196 4146 __cil_tmp6 = *((unsigned short *)__cil_tmp5); 4147#line 196 4148 __cil_tmp7 = (unsigned int )__cil_tmp6; 4149#line 196 4150 if (__cil_tmp7 == 0U) { 4151 { 4152#line 197 4153 printk("<3>i2c-stub: Please specify a chip address\n"); 4154 } 4155#line 198 4156 return (-19); 4157 } else { 4158 4159 } 4160 } 4161#line 201 4162 i = 0; 4163#line 201 4164 goto ldv_18843; 4165 ldv_18842: ; 4166 { 4167#line 202 4168 __cil_tmp8 = i * 2UL; 4169#line 202 4170 __cil_tmp9 = (unsigned long )(chip_addr) + __cil_tmp8; 4171#line 202 4172 __cil_tmp10 = *((unsigned short *)__cil_tmp9); 4173#line 202 4174 __cil_tmp11 = (unsigned int )__cil_tmp10; 4175#line 202 4176 if (__cil_tmp11 <= 2U) { 4177 { 4178#line 203 4179 __cil_tmp12 = i * 2UL; 4180#line 203 4181 __cil_tmp13 = (unsigned long )(chip_addr) + __cil_tmp12; 4182#line 203 4183 __cil_tmp14 = *((unsigned short *)__cil_tmp13); 4184#line 203 4185 __cil_tmp15 = (int )__cil_tmp14; 4186#line 203 4187 printk("<3>i2c-stub: Invalid chip address 0x%02x\n", __cil_tmp15); 4188 } 4189#line 205 4190 return (-22); 4191 } else { 4192 { 4193#line 202 4194 __cil_tmp16 = i * 2UL; 4195#line 202 4196 __cil_tmp17 = (unsigned long )(chip_addr) + __cil_tmp16; 4197#line 202 4198 __cil_tmp18 = *((unsigned short *)__cil_tmp17); 4199#line 202 4200 __cil_tmp19 = (unsigned int )__cil_tmp18; 4201#line 202 4202 if (__cil_tmp19 > 119U) { 4203 { 4204#line 203 4205 __cil_tmp20 = i * 2UL; 4206#line 203 4207 __cil_tmp21 = (unsigned long )(chip_addr) + __cil_tmp20; 4208#line 203 4209 __cil_tmp22 = *((unsigned short *)__cil_tmp21); 4210#line 203 4211 __cil_tmp23 = (int )__cil_tmp22; 4212#line 203 4213 printk("<3>i2c-stub: Invalid chip address 0x%02x\n", __cil_tmp23); 4214 } 4215#line 205 4216 return (-22); 4217 } else { 4218 4219 } 4220 } 4221 } 4222 } 4223 { 4224#line 208 4225 __cil_tmp24 = i * 2UL; 4226#line 208 4227 __cil_tmp25 = (unsigned long )(chip_addr) + __cil_tmp24; 4228#line 208 4229 __cil_tmp26 = *((unsigned short *)__cil_tmp25); 4230#line 208 4231 __cil_tmp27 = (int )__cil_tmp26; 4232#line 208 4233 printk("<6>i2c-stub: Virtual chip at 0x%02x\n", __cil_tmp27); 4234#line 201 4235 i = i + 1; 4236 } 4237 ldv_18843: ; 4238#line 201 4239 if (i <= 9) { 4240 { 4241#line 201 4242 __cil_tmp28 = i * 2UL; 4243#line 201 4244 __cil_tmp29 = (unsigned long )(chip_addr) + __cil_tmp28; 4245#line 201 4246 __cil_tmp30 = *((unsigned short *)__cil_tmp29); 4247#line 201 4248 __cil_tmp31 = (unsigned int )__cil_tmp30; 4249#line 201 4250 if (__cil_tmp31 != 0U) { 4251#line 202 4252 goto ldv_18842; 4253 } else { 4254#line 204 4255 goto ldv_18844; 4256 } 4257 } 4258 } else { 4259#line 204 4260 goto ldv_18844; 4261 } 4262 ldv_18844: 4263 { 4264#line 213 4265 __cil_tmp32 = (unsigned long )i; 4266#line 213 4267 __cil_tmp33 = __cil_tmp32 * 514UL; 4268#line 213 4269 tmp = kzalloc(__cil_tmp33, 208U); 4270#line 213 4271 stub_chips = (struct stub_chip *)tmp; 4272 } 4273 { 4274#line 214 4275 __cil_tmp34 = (struct stub_chip *)0; 4276#line 214 4277 __cil_tmp35 = (unsigned long )__cil_tmp34; 4278#line 214 4279 __cil_tmp36 = (unsigned long )stub_chips; 4280#line 214 4281 if (__cil_tmp36 == __cil_tmp35) { 4282 { 4283#line 215 4284 printk("<3>i2c-stub: Out of memory\n"); 4285 } 4286#line 216 4287 return (-12); 4288 } else { 4289 4290 } 4291 } 4292 { 4293#line 219 4294 ret = i2c_add_adapter(& stub_adapter); 4295 } 4296#line 220 4297 if (ret != 0) { 4298 { 4299#line 221 4300 __cil_tmp37 = (void const *)stub_chips; 4301#line 221 4302 kfree(__cil_tmp37); 4303 } 4304 } else { 4305 4306 } 4307#line 222 4308 return (ret); 4309} 4310} 4311#line 225 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p" 4312static void i2c_stub_exit(void) 4313{ void const *__cil_tmp1 ; 4314 4315 { 4316 { 4317#line 227 4318 i2c_del_adapter(& stub_adapter); 4319#line 228 4320 __cil_tmp1 = (void const *)stub_chips; 4321#line 228 4322 kfree(__cil_tmp1); 4323 } 4324#line 229 4325 return; 4326} 4327} 4328#line 255 4329extern void ldv_check_final_state(void) ; 4330#line 261 4331extern void ldv_initialize(void) ; 4332#line 264 4333extern int __VERIFIER_nondet_int(void) ; 4334#line 267 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p" 4335int LDV_IN_INTERRUPT ; 4336#line 270 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p" 4337void main(void) 4338{ struct i2c_adapter *var_group1 ; 4339 u16 var_stub_xfer_0_p1 ; 4340 unsigned int var_stub_xfer_0_p2 ; 4341 char var_stub_xfer_0_p3 ; 4342 u8 var_stub_xfer_0_p4 ; 4343 int var_stub_xfer_0_p5 ; 4344 union i2c_smbus_data *var_stub_xfer_0_p6 ; 4345 int tmp ; 4346 int tmp___0 ; 4347 int tmp___1 ; 4348 int __cil_tmp11 ; 4349 u16 __cil_tmp12 ; 4350 unsigned short __cil_tmp13 ; 4351 int __cil_tmp14 ; 4352 unsigned short __cil_tmp15 ; 4353 int __cil_tmp16 ; 4354 char __cil_tmp17 ; 4355 int __cil_tmp18 ; 4356 u8 __cil_tmp19 ; 4357 4358 { 4359 { 4360#line 314 4361 LDV_IN_INTERRUPT = 1; 4362#line 323 4363 ldv_initialize(); 4364#line 335 4365 tmp = i2c_stub_init(); 4366 } 4367#line 335 4368 if (tmp != 0) { 4369#line 336 4370 goto ldv_final; 4371 } else { 4372 4373 } 4374#line 340 4375 goto ldv_18886; 4376 ldv_18885: 4377 { 4378#line 343 4379 tmp___0 = __VERIFIER_nondet_int(); 4380 } 4381#line 345 4382 if (tmp___0 == 0) { 4383#line 345 4384 goto case_0; 4385 } else 4386#line 367 4387 if (tmp___0 == 1) { 4388#line 367 4389 goto case_1; 4390 } else { 4391 { 4392#line 389 4393 goto switch_default; 4394#line 343 4395 if (0) { 4396 case_0: /* CIL Label */ 4397 { 4398#line 359 4399 stub_func(var_group1); 4400 } 4401#line 366 4402 goto ldv_18882; 4403 case_1: /* CIL Label */ 4404 { 4405#line 381 4406 __cil_tmp11 = (int )var_stub_xfer_0_p1; 4407#line 381 4408 __cil_tmp12 = (u16 )__cil_tmp11; 4409#line 381 4410 __cil_tmp13 = (unsigned short )var_stub_xfer_0_p2; 4411#line 381 4412 __cil_tmp14 = (int )__cil_tmp13; 4413#line 381 4414 __cil_tmp15 = (unsigned short )__cil_tmp14; 4415#line 381 4416 __cil_tmp16 = (int )var_stub_xfer_0_p3; 4417#line 381 4418 __cil_tmp17 = (char )__cil_tmp16; 4419#line 381 4420 __cil_tmp18 = (int )var_stub_xfer_0_p4; 4421#line 381 4422 __cil_tmp19 = (u8 )__cil_tmp18; 4423#line 381 4424 stub_xfer(var_group1, __cil_tmp12, __cil_tmp15, __cil_tmp17, __cil_tmp19, var_stub_xfer_0_p5, 4425 var_stub_xfer_0_p6); 4426 } 4427#line 388 4428 goto ldv_18882; 4429 switch_default: /* CIL Label */ ; 4430#line 389 4431 goto ldv_18882; 4432 } else { 4433 switch_break: /* CIL Label */ ; 4434 } 4435 } 4436 } 4437 ldv_18882: ; 4438 ldv_18886: 4439 { 4440#line 340 4441 tmp___1 = __VERIFIER_nondet_int(); 4442 } 4443#line 340 4444 if (tmp___1 != 0) { 4445#line 341 4446 goto ldv_18885; 4447 } else { 4448#line 343 4449 goto ldv_18887; 4450 } 4451 ldv_18887: ; 4452 { 4453#line 407 4454 i2c_stub_exit(); 4455 } 4456 ldv_final: 4457 { 4458#line 410 4459 ldv_check_final_state(); 4460 } 4461#line 413 4462 return; 4463} 4464} 4465#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h" 4466void ldv_blast_assert(void) 4467{ 4468 4469 { 4470 ERROR: ; 4471#line 6 4472 goto ERROR; 4473} 4474} 4475#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h" 4476extern int __VERIFIER_nondet_int(void) ; 4477#line 434 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p" 4478int ldv_spin = 0; 4479#line 438 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p" 4480void ldv_check_alloc_flags(gfp_t flags ) 4481{ 4482 4483 { 4484#line 441 4485 if (ldv_spin != 0) { 4486#line 441 4487 if (flags != 32U) { 4488 { 4489#line 441 4490 ldv_blast_assert(); 4491 } 4492 } else { 4493 4494 } 4495 } else { 4496 4497 } 4498#line 444 4499 return; 4500} 4501} 4502#line 444 4503extern struct page *ldv_some_page(void) ; 4504#line 447 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p" 4505struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) 4506{ struct page *tmp ; 4507 4508 { 4509#line 450 4510 if (ldv_spin != 0) { 4511#line 450 4512 if (flags != 32U) { 4513 { 4514#line 450 4515 ldv_blast_assert(); 4516 } 4517 } else { 4518 4519 } 4520 } else { 4521 4522 } 4523 { 4524#line 452 4525 tmp = ldv_some_page(); 4526 } 4527#line 452 4528 return (tmp); 4529} 4530} 4531#line 456 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p" 4532void ldv_check_alloc_nonatomic(void) 4533{ 4534 4535 { 4536#line 459 4537 if (ldv_spin != 0) { 4538 { 4539#line 459 4540 ldv_blast_assert(); 4541 } 4542 } else { 4543 4544 } 4545#line 462 4546 return; 4547} 4548} 4549#line 463 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p" 4550void ldv_spin_lock(void) 4551{ 4552 4553 { 4554#line 466 4555 ldv_spin = 1; 4556#line 467 4557 return; 4558} 4559} 4560#line 470 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p" 4561void ldv_spin_unlock(void) 4562{ 4563 4564 { 4565#line 473 4566 ldv_spin = 0; 4567#line 474 4568 return; 4569} 4570} 4571#line 477 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p" 4572int ldv_spin_trylock(void) 4573{ int is_lock ; 4574 4575 { 4576 { 4577#line 482 4578 is_lock = __VERIFIER_nondet_int(); 4579 } 4580#line 484 4581 if (is_lock != 0) { 4582#line 487 4583 return (0); 4584 } else { 4585#line 492 4586 ldv_spin = 1; 4587#line 494 4588 return (1); 4589 } 4590} 4591} 4592#line 661 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p" 4593void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) 4594{ 4595 4596 { 4597 { 4598#line 667 4599 ldv_check_alloc_flags(ldv_func_arg2); 4600#line 669 4601 kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2); 4602 } 4603#line 670 4604 return ((void *)0); 4605} 4606} 4607#line 672 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p" 4608__inline static void *kzalloc(size_t size , gfp_t flags ) 4609{ void *tmp ; 4610 4611 { 4612 { 4613#line 678 4614 ldv_check_alloc_flags(flags); 4615#line 679 4616 tmp = __VERIFIER_nondet_pointer(); 4617 } 4618#line 679 4619 return (tmp); 4620} 4621}

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

ClabureDB: Classified Bug-Reports Database

Project: SV-COMP 2013

Showing error 889

Source: