Showing error 814

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--hwmon--asus_atk0110.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 11861
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

    1/* Generated by CIL v. 1.3.7 */
    2/* print_CIL_Input is true */
    3
    4#line 19 "include/asm-generic/int-ll64.h"
    5typedef signed char __s8;
    6#line 20 "include/asm-generic/int-ll64.h"
    7typedef unsigned char __u8;
    8#line 22 "include/asm-generic/int-ll64.h"
    9typedef short __s16;
   10#line 23 "include/asm-generic/int-ll64.h"
   11typedef unsigned short __u16;
   12#line 25 "include/asm-generic/int-ll64.h"
   13typedef int __s32;
   14#line 26 "include/asm-generic/int-ll64.h"
   15typedef unsigned int __u32;
   16#line 29 "include/asm-generic/int-ll64.h"
   17typedef long long __s64;
   18#line 30 "include/asm-generic/int-ll64.h"
   19typedef unsigned long long __u64;
   20#line 43 "include/asm-generic/int-ll64.h"
   21typedef unsigned char u8;
   22#line 45 "include/asm-generic/int-ll64.h"
   23typedef short s16;
   24#line 46 "include/asm-generic/int-ll64.h"
   25typedef unsigned short u16;
   26#line 48 "include/asm-generic/int-ll64.h"
   27typedef int s32;
   28#line 49 "include/asm-generic/int-ll64.h"
   29typedef unsigned int u32;
   30#line 51 "include/asm-generic/int-ll64.h"
   31typedef long long s64;
   32#line 52 "include/asm-generic/int-ll64.h"
   33typedef unsigned long long u64;
   34#line 14 "include/asm-generic/posix_types.h"
   35typedef long __kernel_long_t;
   36#line 15 "include/asm-generic/posix_types.h"
   37typedef unsigned long __kernel_ulong_t;
   38#line 27 "include/asm-generic/posix_types.h"
   39typedef __kernel_ulong_t __kernel_nlink_t;
   40#line 31 "include/asm-generic/posix_types.h"
   41typedef int __kernel_pid_t;
   42#line 52 "include/asm-generic/posix_types.h"
   43typedef unsigned int __kernel_uid32_t;
   44#line 53 "include/asm-generic/posix_types.h"
   45typedef unsigned int __kernel_gid32_t;
   46#line 75 "include/asm-generic/posix_types.h"
   47typedef __kernel_ulong_t __kernel_size_t;
   48#line 76 "include/asm-generic/posix_types.h"
   49typedef __kernel_long_t __kernel_ssize_t;
   50#line 90 "include/asm-generic/posix_types.h"
   51typedef __kernel_long_t __kernel_off_t;
   52#line 91 "include/asm-generic/posix_types.h"
   53typedef long long __kernel_loff_t;
   54#line 92 "include/asm-generic/posix_types.h"
   55typedef __kernel_long_t __kernel_time_t;
   56#line 93 "include/asm-generic/posix_types.h"
   57typedef __kernel_long_t __kernel_clock_t;
   58#line 94 "include/asm-generic/posix_types.h"
   59typedef int __kernel_timer_t;
   60#line 95 "include/asm-generic/posix_types.h"
   61typedef int __kernel_clockid_t;
   62#line 21 "include/linux/types.h"
   63typedef __u32 __kernel_dev_t;
   64#line 24 "include/linux/types.h"
   65typedef __kernel_dev_t dev_t;
   66#line 27 "include/linux/types.h"
   67typedef unsigned short umode_t;
   68#line 28 "include/linux/types.h"
   69typedef __kernel_nlink_t nlink_t;
   70#line 29 "include/linux/types.h"
   71typedef __kernel_off_t off_t;
   72#line 30 "include/linux/types.h"
   73typedef __kernel_pid_t pid_t;
   74#line 35 "include/linux/types.h"
   75typedef __kernel_clockid_t clockid_t;
   76#line 38 "include/linux/types.h"
   77typedef _Bool bool;
   78#line 40 "include/linux/types.h"
   79typedef __kernel_uid32_t uid_t;
   80#line 41 "include/linux/types.h"
   81typedef __kernel_gid32_t gid_t;
   82#line 54 "include/linux/types.h"
   83typedef __kernel_loff_t loff_t;
   84#line 63 "include/linux/types.h"
   85typedef __kernel_size_t size_t;
   86#line 68 "include/linux/types.h"
   87typedef __kernel_ssize_t ssize_t;
   88#line 78 "include/linux/types.h"
   89typedef __kernel_time_t time_t;
   90#line 111 "include/linux/types.h"
   91typedef __s32 int32_t;
   92#line 117 "include/linux/types.h"
   93typedef __u32 uint32_t;
   94#line 142 "include/linux/types.h"
   95typedef unsigned long sector_t;
   96#line 143 "include/linux/types.h"
   97typedef unsigned long blkcnt_t;
   98#line 202 "include/linux/types.h"
   99typedef unsigned int gfp_t;
  100#line 203 "include/linux/types.h"
  101typedef unsigned int fmode_t;
  102#line 221 "include/linux/types.h"
  103struct __anonstruct_atomic_t_6 {
  104   int counter ;
  105};
  106#line 221 "include/linux/types.h"
  107typedef struct __anonstruct_atomic_t_6 atomic_t;
  108#line 226 "include/linux/types.h"
  109struct __anonstruct_atomic64_t_7 {
  110   long counter ;
  111};
  112#line 226 "include/linux/types.h"
  113typedef struct __anonstruct_atomic64_t_7 atomic64_t;
  114#line 227 "include/linux/types.h"
  115struct list_head {
  116   struct list_head *next ;
  117   struct list_head *prev ;
  118};
  119#line 232
  120struct hlist_node;
  121#line 232 "include/linux/types.h"
  122struct hlist_head {
  123   struct hlist_node *first ;
  124};
  125#line 236 "include/linux/types.h"
  126struct hlist_node {
  127   struct hlist_node *next ;
  128   struct hlist_node **pprev ;
  129};
  130#line 247 "include/linux/types.h"
  131struct rcu_head {
  132   struct rcu_head *next ;
  133   void (*func)(struct rcu_head * ) ;
  134};
  135#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
  136struct module;
  137#line 55
  138struct module;
  139#line 146 "include/linux/init.h"
  140typedef void (*ctor_fn_t)(void);
  141#line 305 "include/linux/printk.h"
  142struct _ddebug {
  143   char const   *modname ;
  144   char const   *function ;
  145   char const   *filename ;
  146   char const   *format ;
  147   unsigned int lineno : 18 ;
  148   unsigned char flags ;
  149};
  150#line 46 "include/linux/dynamic_debug.h"
  151struct device;
  152#line 46
  153struct device;
  154#line 57
  155struct completion;
  156#line 57
  157struct completion;
  158#line 58
  159struct pt_regs;
  160#line 58
  161struct pt_regs;
  162#line 348 "include/linux/kernel.h"
  163struct pid;
  164#line 348
  165struct pid;
  166#line 112 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/stat.h"
  167struct timespec;
  168#line 112
  169struct timespec;
  170#line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
  171struct page;
  172#line 58
  173struct page;
  174#line 26 "include/asm-generic/getorder.h"
  175struct task_struct;
  176#line 26
  177struct task_struct;
  178#line 28
  179struct mm_struct;
  180#line 28
  181struct mm_struct;
  182#line 268 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/segment.h"
  183struct pt_regs {
  184   unsigned long r15 ;
  185   unsigned long r14 ;
  186   unsigned long r13 ;
  187   unsigned long r12 ;
  188   unsigned long bp ;
  189   unsigned long bx ;
  190   unsigned long r11 ;
  191   unsigned long r10 ;
  192   unsigned long r9 ;
  193   unsigned long r8 ;
  194   unsigned long ax ;
  195   unsigned long cx ;
  196   unsigned long dx ;
  197   unsigned long si ;
  198   unsigned long di ;
  199   unsigned long orig_ax ;
  200   unsigned long ip ;
  201   unsigned long cs ;
  202   unsigned long flags ;
  203   unsigned long sp ;
  204   unsigned long ss ;
  205};
  206#line 125 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
  207struct __anonstruct_ldv_2180_13 {
  208   unsigned int a ;
  209   unsigned int b ;
  210};
  211#line 125 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
  212struct __anonstruct_ldv_2195_14 {
  213   u16 limit0 ;
  214   u16 base0 ;
  215   unsigned char base1 ;
  216   unsigned char type : 4 ;
  217   unsigned char s : 1 ;
  218   unsigned char dpl : 2 ;
  219   unsigned char p : 1 ;
  220   unsigned char limit : 4 ;
  221   unsigned char avl : 1 ;
  222   unsigned char l : 1 ;
  223   unsigned char d : 1 ;
  224   unsigned char g : 1 ;
  225   unsigned char base2 ;
  226};
  227#line 125 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
  228union __anonunion_ldv_2196_12 {
  229   struct __anonstruct_ldv_2180_13 ldv_2180 ;
  230   struct __anonstruct_ldv_2195_14 ldv_2195 ;
  231};
  232#line 125 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
  233struct desc_struct {
  234   union __anonunion_ldv_2196_12 ldv_2196 ;
  235};
  236#line 13 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
  237typedef unsigned long pgdval_t;
  238#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
  239typedef unsigned long pgprotval_t;
  240#line 18 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
  241struct pgprot {
  242   pgprotval_t pgprot ;
  243};
  244#line 192 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
  245typedef struct pgprot pgprot_t;
  246#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
  247struct __anonstruct_pgd_t_16 {
  248   pgdval_t pgd ;
  249};
  250#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
  251typedef struct __anonstruct_pgd_t_16 pgd_t;
  252#line 282 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
  253typedef struct page *pgtable_t;
  254#line 290
  255struct file;
  256#line 290
  257struct file;
  258#line 305
  259struct seq_file;
  260#line 305
  261struct seq_file;
  262#line 337
  263struct thread_struct;
  264#line 337
  265struct thread_struct;
  266#line 339
  267struct cpumask;
  268#line 339
  269struct cpumask;
  270#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
  271struct arch_spinlock;
  272#line 327
  273struct arch_spinlock;
  274#line 300 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
  275struct kernel_vm86_regs {
  276   struct pt_regs pt ;
  277   unsigned short es ;
  278   unsigned short __esh ;
  279   unsigned short ds ;
  280   unsigned short __dsh ;
  281   unsigned short fs ;
  282   unsigned short __fsh ;
  283   unsigned short gs ;
  284   unsigned short __gsh ;
  285};
  286#line 203 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/vm86.h"
  287union __anonunion_ldv_2824_19 {
  288   struct pt_regs *regs ;
  289   struct kernel_vm86_regs *vm86 ;
  290};
  291#line 203 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/vm86.h"
  292struct math_emu_info {
  293   long ___orig_eip ;
  294   union __anonunion_ldv_2824_19 ldv_2824 ;
  295};
  296#line 306 "include/linux/bitmap.h"
  297struct bug_entry {
  298   int bug_addr_disp ;
  299   int file_disp ;
  300   unsigned short line ;
  301   unsigned short flags ;
  302};
  303#line 89 "include/linux/bug.h"
  304struct cpumask {
  305   unsigned long bits[64U] ;
  306};
  307#line 14 "include/linux/cpumask.h"
  308typedef struct cpumask cpumask_t;
  309#line 637 "include/linux/cpumask.h"
  310typedef struct cpumask *cpumask_var_t;
  311#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
  312struct static_key;
  313#line 234
  314struct static_key;
  315#line 153 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
  316struct seq_operations;
  317#line 287 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
  318struct i387_fsave_struct {
  319   u32 cwd ;
  320   u32 swd ;
  321   u32 twd ;
  322   u32 fip ;
  323   u32 fcs ;
  324   u32 foo ;
  325   u32 fos ;
  326   u32 st_space[20U] ;
  327   u32 status ;
  328};
  329#line 305 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
  330struct __anonstruct_ldv_5180_24 {
  331   u64 rip ;
  332   u64 rdp ;
  333};
  334#line 305 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
  335struct __anonstruct_ldv_5186_25 {
  336   u32 fip ;
  337   u32 fcs ;
  338   u32 foo ;
  339   u32 fos ;
  340};
  341#line 305 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
  342union __anonunion_ldv_5187_23 {
  343   struct __anonstruct_ldv_5180_24 ldv_5180 ;
  344   struct __anonstruct_ldv_5186_25 ldv_5186 ;
  345};
  346#line 305 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
  347union __anonunion_ldv_5196_26 {
  348   u32 padding1[12U] ;
  349   u32 sw_reserved[12U] ;
  350};
  351#line 305 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
  352struct i387_fxsave_struct {
  353   u16 cwd ;
  354   u16 swd ;
  355   u16 twd ;
  356   u16 fop ;
  357   union __anonunion_ldv_5187_23 ldv_5187 ;
  358   u32 mxcsr ;
  359   u32 mxcsr_mask ;
  360   u32 st_space[32U] ;
  361   u32 xmm_space[64U] ;
  362   u32 padding[12U] ;
  363   union __anonunion_ldv_5196_26 ldv_5196 ;
  364};
  365#line 339 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
  366struct i387_soft_struct {
  367   u32 cwd ;
  368   u32 swd ;
  369   u32 twd ;
  370   u32 fip ;
  371   u32 fcs ;
  372   u32 foo ;
  373   u32 fos ;
  374   u32 st_space[20U] ;
  375   u8 ftop ;
  376   u8 changed ;
  377   u8 lookahead ;
  378   u8 no_update ;
  379   u8 rm ;
  380   u8 alimit ;
  381   struct math_emu_info *info ;
  382   u32 entry_eip ;
  383};
  384#line 360 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
  385struct ymmh_struct {
  386   u32 ymmh_space[64U] ;
  387};
  388#line 365 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
  389struct xsave_hdr_struct {
  390   u64 xstate_bv ;
  391   u64 reserved1[2U] ;
  392   u64 reserved2[5U] ;
  393};
  394#line 371 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
  395struct xsave_struct {
  396   struct i387_fxsave_struct i387 ;
  397   struct xsave_hdr_struct xsave_hdr ;
  398   struct ymmh_struct ymmh ;
  399};
  400#line 377 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
  401union thread_xstate {
  402   struct i387_fsave_struct fsave ;
  403   struct i387_fxsave_struct fxsave ;
  404   struct i387_soft_struct soft ;
  405   struct xsave_struct xsave ;
  406};
  407#line 385 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
  408struct fpu {
  409   unsigned int last_cpu ;
  410   unsigned int has_fpu ;
  411   union thread_xstate *state ;
  412};
  413#line 433
  414struct kmem_cache;
  415#line 434
  416struct perf_event;
  417#line 434
  418struct perf_event;
  419#line 435 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
  420struct thread_struct {
  421   struct desc_struct tls_array[3U] ;
  422   unsigned long sp0 ;
  423   unsigned long sp ;
  424   unsigned long usersp ;
  425   unsigned short es ;
  426   unsigned short ds ;
  427   unsigned short fsindex ;
  428   unsigned short gsindex ;
  429   unsigned long fs ;
  430   unsigned long gs ;
  431   struct perf_event *ptrace_bps[4U] ;
  432   unsigned long debugreg6 ;
  433   unsigned long ptrace_dr7 ;
  434   unsigned long cr2 ;
  435   unsigned long trap_nr ;
  436   unsigned long error_code ;
  437   struct fpu fpu ;
  438   unsigned long *io_bitmap_ptr ;
  439   unsigned long iopl ;
  440   unsigned int io_bitmap_max ;
  441};
  442#line 23 "include/asm-generic/atomic-long.h"
  443typedef atomic64_t atomic_long_t;
  444#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
  445typedef u16 __ticket_t;
  446#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
  447typedef u32 __ticketpair_t;
  448#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
  449struct __raw_tickets {
  450   __ticket_t head ;
  451   __ticket_t tail ;
  452};
  453#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
  454union __anonunion_ldv_5907_29 {
  455   __ticketpair_t head_tail ;
  456   struct __raw_tickets tickets ;
  457};
  458#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
  459struct arch_spinlock {
  460   union __anonunion_ldv_5907_29 ldv_5907 ;
  461};
  462#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
  463typedef struct arch_spinlock arch_spinlock_t;
  464#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
  465struct __anonstruct_ldv_5914_31 {
  466   u32 read ;
  467   s32 write ;
  468};
  469#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
  470union __anonunion_arch_rwlock_t_30 {
  471   s64 lock ;
  472   struct __anonstruct_ldv_5914_31 ldv_5914 ;
  473};
  474#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
  475typedef union __anonunion_arch_rwlock_t_30 arch_rwlock_t;
  476#line 34
  477struct lockdep_map;
  478#line 34
  479struct lockdep_map;
  480#line 55 "include/linux/debug_locks.h"
  481struct stack_trace {
  482   unsigned int nr_entries ;
  483   unsigned int max_entries ;
  484   unsigned long *entries ;
  485   int skip ;
  486};
  487#line 26 "include/linux/stacktrace.h"
  488struct lockdep_subclass_key {
  489   char __one_byte ;
  490};
  491#line 53 "include/linux/lockdep.h"
  492struct lock_class_key {
  493   struct lockdep_subclass_key subkeys[8U] ;
  494};
  495#line 59 "include/linux/lockdep.h"
  496struct lock_class {
  497   struct list_head hash_entry ;
  498   struct list_head lock_entry ;
  499   struct lockdep_subclass_key *key ;
  500   unsigned int subclass ;
  501   unsigned int dep_gen_id ;
  502   unsigned long usage_mask ;
  503   struct stack_trace usage_traces[13U] ;
  504   struct list_head locks_after ;
  505   struct list_head locks_before ;
  506   unsigned int version ;
  507   unsigned long ops ;
  508   char const   *name ;
  509   int name_version ;
  510   unsigned long contention_point[4U] ;
  511   unsigned long contending_point[4U] ;
  512};
  513#line 144 "include/linux/lockdep.h"
  514struct lockdep_map {
  515   struct lock_class_key *key ;
  516   struct lock_class *class_cache[2U] ;
  517   char const   *name ;
  518   int cpu ;
  519   unsigned long ip ;
  520};
  521#line 187 "include/linux/lockdep.h"
  522struct held_lock {
  523   u64 prev_chain_key ;
  524   unsigned long acquire_ip ;
  525   struct lockdep_map *instance ;
  526   struct lockdep_map *nest_lock ;
  527   u64 waittime_stamp ;
  528   u64 holdtime_stamp ;
  529   unsigned short class_idx : 13 ;
  530   unsigned char irq_context : 2 ;
  531   unsigned char trylock : 1 ;
  532   unsigned char read : 2 ;
  533   unsigned char check : 2 ;
  534   unsigned char hardirqs_off : 1 ;
  535   unsigned short references : 11 ;
  536};
  537#line 556 "include/linux/lockdep.h"
  538struct raw_spinlock {
  539   arch_spinlock_t raw_lock ;
  540   unsigned int magic ;
  541   unsigned int owner_cpu ;
  542   void *owner ;
  543   struct lockdep_map dep_map ;
  544};
  545#line 32 "include/linux/spinlock_types.h"
  546typedef struct raw_spinlock raw_spinlock_t;
  547#line 33 "include/linux/spinlock_types.h"
  548struct __anonstruct_ldv_6122_33 {
  549   u8 __padding[24U] ;
  550   struct lockdep_map dep_map ;
  551};
  552#line 33 "include/linux/spinlock_types.h"
  553union __anonunion_ldv_6123_32 {
  554   struct raw_spinlock rlock ;
  555   struct __anonstruct_ldv_6122_33 ldv_6122 ;
  556};
  557#line 33 "include/linux/spinlock_types.h"
  558struct spinlock {
  559   union __anonunion_ldv_6123_32 ldv_6123 ;
  560};
  561#line 76 "include/linux/spinlock_types.h"
  562typedef struct spinlock spinlock_t;
  563#line 23 "include/linux/rwlock_types.h"
  564struct __anonstruct_rwlock_t_34 {
  565   arch_rwlock_t raw_lock ;
  566   unsigned int magic ;
  567   unsigned int owner_cpu ;
  568   void *owner ;
  569   struct lockdep_map dep_map ;
  570};
  571#line 23 "include/linux/rwlock_types.h"
  572typedef struct __anonstruct_rwlock_t_34 rwlock_t;
  573#line 110 "include/linux/seqlock.h"
  574struct seqcount {
  575   unsigned int sequence ;
  576};
  577#line 121 "include/linux/seqlock.h"
  578typedef struct seqcount seqcount_t;
  579#line 254 "include/linux/seqlock.h"
  580struct timespec {
  581   __kernel_time_t tv_sec ;
  582   long tv_nsec ;
  583};
  584#line 286 "include/linux/time.h"
  585struct kstat {
  586   u64 ino ;
  587   dev_t dev ;
  588   umode_t mode ;
  589   unsigned int nlink ;
  590   uid_t uid ;
  591   gid_t gid ;
  592   dev_t rdev ;
  593   loff_t size ;
  594   struct timespec atime ;
  595   struct timespec mtime ;
  596   struct timespec ctime ;
  597   unsigned long blksize ;
  598   unsigned long long blocks ;
  599};
  600#line 48 "include/linux/wait.h"
  601struct __wait_queue_head {
  602   spinlock_t lock ;
  603   struct list_head task_list ;
  604};
  605#line 53 "include/linux/wait.h"
  606typedef struct __wait_queue_head wait_queue_head_t;
  607#line 98 "include/linux/nodemask.h"
  608struct __anonstruct_nodemask_t_36 {
  609   unsigned long bits[16U] ;
  610};
  611#line 98 "include/linux/nodemask.h"
  612typedef struct __anonstruct_nodemask_t_36 nodemask_t;
  613#line 670 "include/linux/mmzone.h"
  614struct mutex {
  615   atomic_t count ;
  616   spinlock_t wait_lock ;
  617   struct list_head wait_list ;
  618   struct task_struct *owner ;
  619   char const   *name ;
  620   void *magic ;
  621   struct lockdep_map dep_map ;
  622};
  623#line 63 "include/linux/mutex.h"
  624struct mutex_waiter {
  625   struct list_head list ;
  626   struct task_struct *task ;
  627   void *magic ;
  628};
  629#line 171
  630struct rw_semaphore;
  631#line 171
  632struct rw_semaphore;
  633#line 172 "include/linux/mutex.h"
  634struct rw_semaphore {
  635   long count ;
  636   raw_spinlock_t wait_lock ;
  637   struct list_head wait_list ;
  638   struct lockdep_map dep_map ;
  639};
  640#line 128 "include/linux/rwsem.h"
  641struct completion {
  642   unsigned int done ;
  643   wait_queue_head_t wait ;
  644};
  645#line 312 "include/linux/jiffies.h"
  646union ktime {
  647   s64 tv64 ;
  648};
  649#line 59 "include/linux/ktime.h"
  650typedef union ktime ktime_t;
  651#line 341
  652struct tvec_base;
  653#line 341
  654struct tvec_base;
  655#line 342 "include/linux/ktime.h"
  656struct timer_list {
  657   struct list_head entry ;
  658   unsigned long expires ;
  659   struct tvec_base *base ;
  660   void (*function)(unsigned long  ) ;
  661   unsigned long data ;
  662   int slack ;
  663   int start_pid ;
  664   void *start_site ;
  665   char start_comm[16U] ;
  666   struct lockdep_map lockdep_map ;
  667};
  668#line 289 "include/linux/timer.h"
  669struct hrtimer;
  670#line 289
  671struct hrtimer;
  672#line 290
  673enum hrtimer_restart;
  674#line 302
  675struct work_struct;
  676#line 302
  677struct work_struct;
  678#line 45 "include/linux/workqueue.h"
  679struct work_struct {
  680   atomic_long_t data ;
  681   struct list_head entry ;
  682   void (*func)(struct work_struct * ) ;
  683   struct lockdep_map lockdep_map ;
  684};
  685#line 86 "include/linux/workqueue.h"
  686struct delayed_work {
  687   struct work_struct work ;
  688   struct timer_list timer ;
  689};
  690#line 46 "include/linux/pm.h"
  691struct pm_message {
  692   int event ;
  693};
  694#line 52 "include/linux/pm.h"
  695typedef struct pm_message pm_message_t;
  696#line 53 "include/linux/pm.h"
  697struct dev_pm_ops {
  698   int (*prepare)(struct device * ) ;
  699   void (*complete)(struct device * ) ;
  700   int (*suspend)(struct device * ) ;
  701   int (*resume)(struct device * ) ;
  702   int (*freeze)(struct device * ) ;
  703   int (*thaw)(struct device * ) ;
  704   int (*poweroff)(struct device * ) ;
  705   int (*restore)(struct device * ) ;
  706   int (*suspend_late)(struct device * ) ;
  707   int (*resume_early)(struct device * ) ;
  708   int (*freeze_late)(struct device * ) ;
  709   int (*thaw_early)(struct device * ) ;
  710   int (*poweroff_late)(struct device * ) ;
  711   int (*restore_early)(struct device * ) ;
  712   int (*suspend_noirq)(struct device * ) ;
  713   int (*resume_noirq)(struct device * ) ;
  714   int (*freeze_noirq)(struct device * ) ;
  715   int (*thaw_noirq)(struct device * ) ;
  716   int (*poweroff_noirq)(struct device * ) ;
  717   int (*restore_noirq)(struct device * ) ;
  718   int (*runtime_suspend)(struct device * ) ;
  719   int (*runtime_resume)(struct device * ) ;
  720   int (*runtime_idle)(struct device * ) ;
  721};
  722#line 289
  723enum rpm_status {
  724    RPM_ACTIVE = 0,
  725    RPM_RESUMING = 1,
  726    RPM_SUSPENDED = 2,
  727    RPM_SUSPENDING = 3
  728} ;
  729#line 296
  730enum rpm_request {
  731    RPM_REQ_NONE = 0,
  732    RPM_REQ_IDLE = 1,
  733    RPM_REQ_SUSPEND = 2,
  734    RPM_REQ_AUTOSUSPEND = 3,
  735    RPM_REQ_RESUME = 4
  736} ;
  737#line 304
  738struct wakeup_source;
  739#line 304
  740struct wakeup_source;
  741#line 494 "include/linux/pm.h"
  742struct pm_subsys_data {
  743   spinlock_t lock ;
  744   unsigned int refcount ;
  745};
  746#line 499
  747struct dev_pm_qos_request;
  748#line 499
  749struct pm_qos_constraints;
  750#line 499 "include/linux/pm.h"
  751struct dev_pm_info {
  752   pm_message_t power_state ;
  753   unsigned char can_wakeup : 1 ;
  754   unsigned char async_suspend : 1 ;
  755   bool is_prepared ;
  756   bool is_suspended ;
  757   bool ignore_children ;
  758   spinlock_t lock ;
  759   struct list_head entry ;
  760   struct completion completion ;
  761   struct wakeup_source *wakeup ;
  762   bool wakeup_path ;
  763   struct timer_list suspend_timer ;
  764   unsigned long timer_expires ;
  765   struct work_struct work ;
  766   wait_queue_head_t wait_queue ;
  767   atomic_t usage_count ;
  768   atomic_t child_count ;
  769   unsigned char disable_depth : 3 ;
  770   unsigned char idle_notification : 1 ;
  771   unsigned char request_pending : 1 ;
  772   unsigned char deferred_resume : 1 ;
  773   unsigned char run_wake : 1 ;
  774   unsigned char runtime_auto : 1 ;
  775   unsigned char no_callbacks : 1 ;
  776   unsigned char irq_safe : 1 ;
  777   unsigned char use_autosuspend : 1 ;
  778   unsigned char timer_autosuspends : 1 ;
  779   enum rpm_request request ;
  780   enum rpm_status runtime_status ;
  781   int runtime_error ;
  782   int autosuspend_delay ;
  783   unsigned long last_busy ;
  784   unsigned long active_jiffies ;
  785   unsigned long suspended_jiffies ;
  786   unsigned long accounting_timestamp ;
  787   ktime_t suspend_time ;
  788   s64 max_time_suspended_ns ;
  789   struct dev_pm_qos_request *pq_req ;
  790   struct pm_subsys_data *subsys_data ;
  791   struct pm_qos_constraints *constraints ;
  792};
  793#line 558 "include/linux/pm.h"
  794struct dev_pm_domain {
  795   struct dev_pm_ops ops ;
  796};
  797#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
  798struct __anonstruct_mm_context_t_101 {
  799   void *ldt ;
  800   int size ;
  801   unsigned short ia32_compat ;
  802   struct mutex lock ;
  803   void *vdso ;
  804};
  805#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
  806typedef struct __anonstruct_mm_context_t_101 mm_context_t;
  807#line 18 "include/asm-generic/pci_iomap.h"
  808struct vm_area_struct;
  809#line 18
  810struct vm_area_struct;
  811#line 835 "include/linux/sysctl.h"
  812struct rb_node {
  813   unsigned long rb_parent_color ;
  814   struct rb_node *rb_right ;
  815   struct rb_node *rb_left ;
  816};
  817#line 108 "include/linux/rbtree.h"
  818struct rb_root {
  819   struct rb_node *rb_node ;
  820};
  821#line 176
  822struct nsproxy;
  823#line 176
  824struct nsproxy;
  825#line 37 "include/linux/kmod.h"
  826struct cred;
  827#line 37
  828struct cred;
  829#line 18 "include/linux/elf.h"
  830typedef __u64 Elf64_Addr;
  831#line 19 "include/linux/elf.h"
  832typedef __u16 Elf64_Half;
  833#line 23 "include/linux/elf.h"
  834typedef __u32 Elf64_Word;
  835#line 24 "include/linux/elf.h"
  836typedef __u64 Elf64_Xword;
  837#line 193 "include/linux/elf.h"
  838struct elf64_sym {
  839   Elf64_Word st_name ;
  840   unsigned char st_info ;
  841   unsigned char st_other ;
  842   Elf64_Half st_shndx ;
  843   Elf64_Addr st_value ;
  844   Elf64_Xword st_size ;
  845};
  846#line 201 "include/linux/elf.h"
  847typedef struct elf64_sym Elf64_Sym;
  848#line 445
  849struct sock;
  850#line 445
  851struct sock;
  852#line 446
  853struct kobject;
  854#line 446
  855struct kobject;
  856#line 447
  857enum kobj_ns_type {
  858    KOBJ_NS_TYPE_NONE = 0,
  859    KOBJ_NS_TYPE_NET = 1,
  860    KOBJ_NS_TYPES = 2
  861} ;
  862#line 453 "include/linux/elf.h"
  863struct kobj_ns_type_operations {
  864   enum kobj_ns_type type ;
  865   void *(*grab_current_ns)(void) ;
  866   void const   *(*netlink_ns)(struct sock * ) ;
  867   void const   *(*initial_ns)(void) ;
  868   void (*drop_ns)(void * ) ;
  869};
  870#line 57 "include/linux/kobject_ns.h"
  871struct attribute {
  872   char const   *name ;
  873   umode_t mode ;
  874   struct lock_class_key *key ;
  875   struct lock_class_key skey ;
  876};
  877#line 33 "include/linux/sysfs.h"
  878struct attribute_group {
  879   char const   *name ;
  880   umode_t (*is_visible)(struct kobject * , struct attribute * , int  ) ;
  881   struct attribute **attrs ;
  882};
  883#line 62 "include/linux/sysfs.h"
  884struct bin_attribute {
  885   struct attribute attr ;
  886   size_t size ;
  887   void *private ;
  888   ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
  889                   loff_t  , size_t  ) ;
  890   ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
  891                    loff_t  , size_t  ) ;
  892   int (*mmap)(struct file * , struct kobject * , struct bin_attribute * , struct vm_area_struct * ) ;
  893};
  894#line 98 "include/linux/sysfs.h"
  895struct sysfs_ops {
  896   ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
  897   ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
  898   void const   *(*namespace)(struct kobject * , struct attribute  const  * ) ;
  899};
  900#line 117
  901struct sysfs_dirent;
  902#line 117
  903struct sysfs_dirent;
  904#line 182 "include/linux/sysfs.h"
  905struct kref {
  906   atomic_t refcount ;
  907};
  908#line 49 "include/linux/kobject.h"
  909struct kset;
  910#line 49
  911struct kobj_type;
  912#line 49 "include/linux/kobject.h"
  913struct kobject {
  914   char const   *name ;
  915   struct list_head entry ;
  916   struct kobject *parent ;
  917   struct kset *kset ;
  918   struct kobj_type *ktype ;
  919   struct sysfs_dirent *sd ;
  920   struct kref kref ;
  921   unsigned char state_initialized : 1 ;
  922   unsigned char state_in_sysfs : 1 ;
  923   unsigned char state_add_uevent_sent : 1 ;
  924   unsigned char state_remove_uevent_sent : 1 ;
  925   unsigned char uevent_suppress : 1 ;
  926};
  927#line 107 "include/linux/kobject.h"
  928struct kobj_type {
  929   void (*release)(struct kobject * ) ;
  930   struct sysfs_ops  const  *sysfs_ops ;
  931   struct attribute **default_attrs ;
  932   struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject * ) ;
  933   void const   *(*namespace)(struct kobject * ) ;
  934};
  935#line 115 "include/linux/kobject.h"
  936struct kobj_uevent_env {
  937   char *envp[32U] ;
  938   int envp_idx ;
  939   char buf[2048U] ;
  940   int buflen ;
  941};
  942#line 122 "include/linux/kobject.h"
  943struct kset_uevent_ops {
  944   int (* const  filter)(struct kset * , struct kobject * ) ;
  945   char const   *(* const  name)(struct kset * , struct kobject * ) ;
  946   int (* const  uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
  947};
  948#line 139 "include/linux/kobject.h"
  949struct kset {
  950   struct list_head list ;
  951   spinlock_t list_lock ;
  952   struct kobject kobj ;
  953   struct kset_uevent_ops  const  *uevent_ops ;
  954};
  955#line 215
  956struct kernel_param;
  957#line 215
  958struct kernel_param;
  959#line 216 "include/linux/kobject.h"
  960struct kernel_param_ops {
  961   int (*set)(char const   * , struct kernel_param  const  * ) ;
  962   int (*get)(char * , struct kernel_param  const  * ) ;
  963   void (*free)(void * ) ;
  964};
  965#line 49 "include/linux/moduleparam.h"
  966struct kparam_string;
  967#line 49
  968struct kparam_array;
  969#line 49 "include/linux/moduleparam.h"
  970union __anonunion_ldv_13363_134 {
  971   void *arg ;
  972   struct kparam_string  const  *str ;
  973   struct kparam_array  const  *arr ;
  974};
  975#line 49 "include/linux/moduleparam.h"
  976struct kernel_param {
  977   char const   *name ;
  978   struct kernel_param_ops  const  *ops ;
  979   u16 perm ;
  980   s16 level ;
  981   union __anonunion_ldv_13363_134 ldv_13363 ;
  982};
  983#line 61 "include/linux/moduleparam.h"
  984struct kparam_string {
  985   unsigned int maxlen ;
  986   char *string ;
  987};
  988#line 67 "include/linux/moduleparam.h"
  989struct kparam_array {
  990   unsigned int max ;
  991   unsigned int elemsize ;
  992   unsigned int *num ;
  993   struct kernel_param_ops  const  *ops ;
  994   void *elem ;
  995};
  996#line 458 "include/linux/moduleparam.h"
  997struct static_key {
  998   atomic_t enabled ;
  999};
 1000#line 225 "include/linux/jump_label.h"
 1001struct tracepoint;
 1002#line 225
 1003struct tracepoint;
 1004#line 226 "include/linux/jump_label.h"
 1005struct tracepoint_func {
 1006   void *func ;
 1007   void *data ;
 1008};
 1009#line 29 "include/linux/tracepoint.h"
 1010struct tracepoint {
 1011   char const   *name ;
 1012   struct static_key key ;
 1013   void (*regfunc)(void) ;
 1014   void (*unregfunc)(void) ;
 1015   struct tracepoint_func *funcs ;
 1016};
 1017#line 86 "include/linux/tracepoint.h"
 1018struct kernel_symbol {
 1019   unsigned long value ;
 1020   char const   *name ;
 1021};
 1022#line 27 "include/linux/export.h"
 1023struct mod_arch_specific {
 1024
 1025};
 1026#line 34 "include/linux/module.h"
 1027struct module_param_attrs;
 1028#line 34 "include/linux/module.h"
 1029struct module_kobject {
 1030   struct kobject kobj ;
 1031   struct module *mod ;
 1032   struct kobject *drivers_dir ;
 1033   struct module_param_attrs *mp ;
 1034};
 1035#line 43 "include/linux/module.h"
 1036struct module_attribute {
 1037   struct attribute attr ;
 1038   ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
 1039   ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const   * ,
 1040                    size_t  ) ;
 1041   void (*setup)(struct module * , char const   * ) ;
 1042   int (*test)(struct module * ) ;
 1043   void (*free)(struct module * ) ;
 1044};
 1045#line 69
 1046struct exception_table_entry;
 1047#line 69
 1048struct exception_table_entry;
 1049#line 198
 1050enum module_state {
 1051    MODULE_STATE_LIVE = 0,
 1052    MODULE_STATE_COMING = 1,
 1053    MODULE_STATE_GOING = 2
 1054} ;
 1055#line 204 "include/linux/module.h"
 1056struct module_ref {
 1057   unsigned long incs ;
 1058   unsigned long decs ;
 1059};
 1060#line 219
 1061struct module_sect_attrs;
 1062#line 219
 1063struct module_notes_attrs;
 1064#line 219
 1065struct ftrace_event_call;
 1066#line 219 "include/linux/module.h"
 1067struct module {
 1068   enum module_state state ;
 1069   struct list_head list ;
 1070   char name[56U] ;
 1071   struct module_kobject mkobj ;
 1072   struct module_attribute *modinfo_attrs ;
 1073   char const   *version ;
 1074   char const   *srcversion ;
 1075   struct kobject *holders_dir ;
 1076   struct kernel_symbol  const  *syms ;
 1077   unsigned long const   *crcs ;
 1078   unsigned int num_syms ;
 1079   struct kernel_param *kp ;
 1080   unsigned int num_kp ;
 1081   unsigned int num_gpl_syms ;
 1082   struct kernel_symbol  const  *gpl_syms ;
 1083   unsigned long const   *gpl_crcs ;
 1084   struct kernel_symbol  const  *unused_syms ;
 1085   unsigned long const   *unused_crcs ;
 1086   unsigned int num_unused_syms ;
 1087   unsigned int num_unused_gpl_syms ;
 1088   struct kernel_symbol  const  *unused_gpl_syms ;
 1089   unsigned long const   *unused_gpl_crcs ;
 1090   struct kernel_symbol  const  *gpl_future_syms ;
 1091   unsigned long const   *gpl_future_crcs ;
 1092   unsigned int num_gpl_future_syms ;
 1093   unsigned int num_exentries ;
 1094   struct exception_table_entry *extable ;
 1095   int (*init)(void) ;
 1096   void *module_init ;
 1097   void *module_core ;
 1098   unsigned int init_size ;
 1099   unsigned int core_size ;
 1100   unsigned int init_text_size ;
 1101   unsigned int core_text_size ;
 1102   unsigned int init_ro_size ;
 1103   unsigned int core_ro_size ;
 1104   struct mod_arch_specific arch ;
 1105   unsigned int taints ;
 1106   unsigned int num_bugs ;
 1107   struct list_head bug_list ;
 1108   struct bug_entry *bug_table ;
 1109   Elf64_Sym *symtab ;
 1110   Elf64_Sym *core_symtab ;
 1111   unsigned int num_symtab ;
 1112   unsigned int core_num_syms ;
 1113   char *strtab ;
 1114   char *core_strtab ;
 1115   struct module_sect_attrs *sect_attrs ;
 1116   struct module_notes_attrs *notes_attrs ;
 1117   char *args ;
 1118   void *percpu ;
 1119   unsigned int percpu_size ;
 1120   unsigned int num_tracepoints ;
 1121   struct tracepoint * const  *tracepoints_ptrs ;
 1122   unsigned int num_trace_bprintk_fmt ;
 1123   char const   **trace_bprintk_fmt_start ;
 1124   struct ftrace_event_call **trace_events ;
 1125   unsigned int num_trace_events ;
 1126   struct list_head source_list ;
 1127   struct list_head target_list ;
 1128   struct task_struct *waiter ;
 1129   void (*exit)(void) ;
 1130   struct module_ref *refptr ;
 1131   ctor_fn_t (**ctors)(void) ;
 1132   unsigned int num_ctors ;
 1133};
 1134#line 88 "include/linux/kmemleak.h"
 1135struct kmem_cache_cpu {
 1136   void **freelist ;
 1137   unsigned long tid ;
 1138   struct page *page ;
 1139   struct page *partial ;
 1140   int node ;
 1141   unsigned int stat[26U] ;
 1142};
 1143#line 55 "include/linux/slub_def.h"
 1144struct kmem_cache_node {
 1145   spinlock_t list_lock ;
 1146   unsigned long nr_partial ;
 1147   struct list_head partial ;
 1148   atomic_long_t nr_slabs ;
 1149   atomic_long_t total_objects ;
 1150   struct list_head full ;
 1151};
 1152#line 66 "include/linux/slub_def.h"
 1153struct kmem_cache_order_objects {
 1154   unsigned long x ;
 1155};
 1156#line 76 "include/linux/slub_def.h"
 1157struct kmem_cache {
 1158   struct kmem_cache_cpu *cpu_slab ;
 1159   unsigned long flags ;
 1160   unsigned long min_partial ;
 1161   int size ;
 1162   int objsize ;
 1163   int offset ;
 1164   int cpu_partial ;
 1165   struct kmem_cache_order_objects oo ;
 1166   struct kmem_cache_order_objects max ;
 1167   struct kmem_cache_order_objects min ;
 1168   gfp_t allocflags ;
 1169   int refcount ;
 1170   void (*ctor)(void * ) ;
 1171   int inuse ;
 1172   int align ;
 1173   int reserved ;
 1174   char const   *name ;
 1175   struct list_head list ;
 1176   struct kobject kobj ;
 1177   int remote_node_defrag_ratio ;
 1178   struct kmem_cache_node *node[1024U] ;
 1179};
 1180#line 18 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p"
 1181struct block_device;
 1182#line 18
 1183struct block_device;
 1184#line 93 "include/linux/bit_spinlock.h"
 1185struct hlist_bl_node;
 1186#line 93 "include/linux/bit_spinlock.h"
 1187struct hlist_bl_head {
 1188   struct hlist_bl_node *first ;
 1189};
 1190#line 36 "include/linux/list_bl.h"
 1191struct hlist_bl_node {
 1192   struct hlist_bl_node *next ;
 1193   struct hlist_bl_node **pprev ;
 1194};
 1195#line 114 "include/linux/rculist_bl.h"
 1196struct nameidata;
 1197#line 114
 1198struct nameidata;
 1199#line 115
 1200struct path;
 1201#line 115
 1202struct path;
 1203#line 116
 1204struct vfsmount;
 1205#line 116
 1206struct vfsmount;
 1207#line 117 "include/linux/rculist_bl.h"
 1208struct qstr {
 1209   unsigned int hash ;
 1210   unsigned int len ;
 1211   unsigned char const   *name ;
 1212};
 1213#line 72 "include/linux/dcache.h"
 1214struct inode;
 1215#line 72
 1216struct dentry_operations;
 1217#line 72
 1218struct super_block;
 1219#line 72 "include/linux/dcache.h"
 1220union __anonunion_d_u_135 {
 1221   struct list_head d_child ;
 1222   struct rcu_head d_rcu ;
 1223};
 1224#line 72 "include/linux/dcache.h"
 1225struct dentry {
 1226   unsigned int d_flags ;
 1227   seqcount_t d_seq ;
 1228   struct hlist_bl_node d_hash ;
 1229   struct dentry *d_parent ;
 1230   struct qstr d_name ;
 1231   struct inode *d_inode ;
 1232   unsigned char d_iname[32U] ;
 1233   unsigned int d_count ;
 1234   spinlock_t d_lock ;
 1235   struct dentry_operations  const  *d_op ;
 1236   struct super_block *d_sb ;
 1237   unsigned long d_time ;
 1238   void *d_fsdata ;
 1239   struct list_head d_lru ;
 1240   union __anonunion_d_u_135 d_u ;
 1241   struct list_head d_subdirs ;
 1242   struct list_head d_alias ;
 1243};
 1244#line 123 "include/linux/dcache.h"
 1245struct dentry_operations {
 1246   int (*d_revalidate)(struct dentry * , struct nameidata * ) ;
 1247   int (*d_hash)(struct dentry  const  * , struct inode  const  * , struct qstr * ) ;
 1248   int (*d_compare)(struct dentry  const  * , struct inode  const  * , struct dentry  const  * ,
 1249                    struct inode  const  * , unsigned int  , char const   * , struct qstr  const  * ) ;
 1250   int (*d_delete)(struct dentry  const  * ) ;
 1251   void (*d_release)(struct dentry * ) ;
 1252   void (*d_prune)(struct dentry * ) ;
 1253   void (*d_iput)(struct dentry * , struct inode * ) ;
 1254   char *(*d_dname)(struct dentry * , char * , int  ) ;
 1255   struct vfsmount *(*d_automount)(struct path * ) ;
 1256   int (*d_manage)(struct dentry * , bool  ) ;
 1257};
 1258#line 402 "include/linux/dcache.h"
 1259struct path {
 1260   struct vfsmount *mnt ;
 1261   struct dentry *dentry ;
 1262};
 1263#line 58 "include/linux/radix-tree.h"
 1264struct radix_tree_node;
 1265#line 58 "include/linux/radix-tree.h"
 1266struct radix_tree_root {
 1267   unsigned int height ;
 1268   gfp_t gfp_mask ;
 1269   struct radix_tree_node *rnode ;
 1270};
 1271#line 377
 1272struct prio_tree_node;
 1273#line 377 "include/linux/radix-tree.h"
 1274struct raw_prio_tree_node {
 1275   struct prio_tree_node *left ;
 1276   struct prio_tree_node *right ;
 1277   struct prio_tree_node *parent ;
 1278};
 1279#line 19 "include/linux/prio_tree.h"
 1280struct prio_tree_node {
 1281   struct prio_tree_node *left ;
 1282   struct prio_tree_node *right ;
 1283   struct prio_tree_node *parent ;
 1284   unsigned long start ;
 1285   unsigned long last ;
 1286};
 1287#line 27 "include/linux/prio_tree.h"
 1288struct prio_tree_root {
 1289   struct prio_tree_node *prio_tree_node ;
 1290   unsigned short index_bits ;
 1291   unsigned short raw ;
 1292};
 1293#line 111
 1294enum pid_type {
 1295    PIDTYPE_PID = 0,
 1296    PIDTYPE_PGID = 1,
 1297    PIDTYPE_SID = 2,
 1298    PIDTYPE_MAX = 3
 1299} ;
 1300#line 118
 1301struct pid_namespace;
 1302#line 118 "include/linux/prio_tree.h"
 1303struct upid {
 1304   int nr ;
 1305   struct pid_namespace *ns ;
 1306   struct hlist_node pid_chain ;
 1307};
 1308#line 56 "include/linux/pid.h"
 1309struct pid {
 1310   atomic_t count ;
 1311   unsigned int level ;
 1312   struct hlist_head tasks[3U] ;
 1313   struct rcu_head rcu ;
 1314   struct upid numbers[1U] ;
 1315};
 1316#line 68 "include/linux/pid.h"
 1317struct pid_link {
 1318   struct hlist_node node ;
 1319   struct pid *pid ;
 1320};
 1321#line 93 "include/linux/capability.h"
 1322struct kernel_cap_struct {
 1323   __u32 cap[2U] ;
 1324};
 1325#line 96 "include/linux/capability.h"
 1326typedef struct kernel_cap_struct kernel_cap_t;
 1327#line 104
 1328struct user_namespace;
 1329#line 104
 1330struct user_namespace;
 1331#line 45 "include/linux/semaphore.h"
 1332struct fiemap_extent {
 1333   __u64 fe_logical ;
 1334   __u64 fe_physical ;
 1335   __u64 fe_length ;
 1336   __u64 fe_reserved64[2U] ;
 1337   __u32 fe_flags ;
 1338   __u32 fe_reserved[3U] ;
 1339};
 1340#line 38 "include/linux/fiemap.h"
 1341struct shrink_control {
 1342   gfp_t gfp_mask ;
 1343   unsigned long nr_to_scan ;
 1344};
 1345#line 14 "include/linux/shrinker.h"
 1346struct shrinker {
 1347   int (*shrink)(struct shrinker * , struct shrink_control * ) ;
 1348   int seeks ;
 1349   long batch ;
 1350   struct list_head list ;
 1351   atomic_long_t nr_in_batch ;
 1352};
 1353#line 43
 1354enum migrate_mode {
 1355    MIGRATE_ASYNC = 0,
 1356    MIGRATE_SYNC_LIGHT = 1,
 1357    MIGRATE_SYNC = 2
 1358} ;
 1359#line 49
 1360struct export_operations;
 1361#line 49
 1362struct export_operations;
 1363#line 51
 1364struct iovec;
 1365#line 51
 1366struct iovec;
 1367#line 52
 1368struct kiocb;
 1369#line 52
 1370struct kiocb;
 1371#line 53
 1372struct pipe_inode_info;
 1373#line 53
 1374struct pipe_inode_info;
 1375#line 54
 1376struct poll_table_struct;
 1377#line 54
 1378struct poll_table_struct;
 1379#line 55
 1380struct kstatfs;
 1381#line 55
 1382struct kstatfs;
 1383#line 435 "include/linux/fs.h"
 1384struct iattr {
 1385   unsigned int ia_valid ;
 1386   umode_t ia_mode ;
 1387   uid_t ia_uid ;
 1388   gid_t ia_gid ;
 1389   loff_t ia_size ;
 1390   struct timespec ia_atime ;
 1391   struct timespec ia_mtime ;
 1392   struct timespec ia_ctime ;
 1393   struct file *ia_file ;
 1394};
 1395#line 119 "include/linux/quota.h"
 1396struct if_dqinfo {
 1397   __u64 dqi_bgrace ;
 1398   __u64 dqi_igrace ;
 1399   __u32 dqi_flags ;
 1400   __u32 dqi_valid ;
 1401};
 1402#line 176 "include/linux/percpu_counter.h"
 1403struct fs_disk_quota {
 1404   __s8 d_version ;
 1405   __s8 d_flags ;
 1406   __u16 d_fieldmask ;
 1407   __u32 d_id ;
 1408   __u64 d_blk_hardlimit ;
 1409   __u64 d_blk_softlimit ;
 1410   __u64 d_ino_hardlimit ;
 1411   __u64 d_ino_softlimit ;
 1412   __u64 d_bcount ;
 1413   __u64 d_icount ;
 1414   __s32 d_itimer ;
 1415   __s32 d_btimer ;
 1416   __u16 d_iwarns ;
 1417   __u16 d_bwarns ;
 1418   __s32 d_padding2 ;
 1419   __u64 d_rtb_hardlimit ;
 1420   __u64 d_rtb_softlimit ;
 1421   __u64 d_rtbcount ;
 1422   __s32 d_rtbtimer ;
 1423   __u16 d_rtbwarns ;
 1424   __s16 d_padding3 ;
 1425   char d_padding4[8U] ;
 1426};
 1427#line 75 "include/linux/dqblk_xfs.h"
 1428struct fs_qfilestat {
 1429   __u64 qfs_ino ;
 1430   __u64 qfs_nblks ;
 1431   __u32 qfs_nextents ;
 1432};
 1433#line 150 "include/linux/dqblk_xfs.h"
 1434typedef struct fs_qfilestat fs_qfilestat_t;
 1435#line 151 "include/linux/dqblk_xfs.h"
 1436struct fs_quota_stat {
 1437   __s8 qs_version ;
 1438   __u16 qs_flags ;
 1439   __s8 qs_pad ;
 1440   fs_qfilestat_t qs_uquota ;
 1441   fs_qfilestat_t qs_gquota ;
 1442   __u32 qs_incoredqs ;
 1443   __s32 qs_btimelimit ;
 1444   __s32 qs_itimelimit ;
 1445   __s32 qs_rtbtimelimit ;
 1446   __u16 qs_bwarnlimit ;
 1447   __u16 qs_iwarnlimit ;
 1448};
 1449#line 165
 1450struct dquot;
 1451#line 165
 1452struct dquot;
 1453#line 185 "include/linux/quota.h"
 1454typedef __kernel_uid32_t qid_t;
 1455#line 186 "include/linux/quota.h"
 1456typedef long long qsize_t;
 1457#line 189 "include/linux/quota.h"
 1458struct mem_dqblk {
 1459   qsize_t dqb_bhardlimit ;
 1460   qsize_t dqb_bsoftlimit ;
 1461   qsize_t dqb_curspace ;
 1462   qsize_t dqb_rsvspace ;
 1463   qsize_t dqb_ihardlimit ;
 1464   qsize_t dqb_isoftlimit ;
 1465   qsize_t dqb_curinodes ;
 1466   time_t dqb_btime ;
 1467   time_t dqb_itime ;
 1468};
 1469#line 211
 1470struct quota_format_type;
 1471#line 211
 1472struct quota_format_type;
 1473#line 212 "include/linux/quota.h"
 1474struct mem_dqinfo {
 1475   struct quota_format_type *dqi_format ;
 1476   int dqi_fmt_id ;
 1477   struct list_head dqi_dirty_list ;
 1478   unsigned long dqi_flags ;
 1479   unsigned int dqi_bgrace ;
 1480   unsigned int dqi_igrace ;
 1481   qsize_t dqi_maxblimit ;
 1482   qsize_t dqi_maxilimit ;
 1483   void *dqi_priv ;
 1484};
 1485#line 275 "include/linux/quota.h"
 1486struct dquot {
 1487   struct hlist_node dq_hash ;
 1488   struct list_head dq_inuse ;
 1489   struct list_head dq_free ;
 1490   struct list_head dq_dirty ;
 1491   struct mutex dq_lock ;
 1492   atomic_t dq_count ;
 1493   wait_queue_head_t dq_wait_unused ;
 1494   struct super_block *dq_sb ;
 1495   unsigned int dq_id ;
 1496   loff_t dq_off ;
 1497   unsigned long dq_flags ;
 1498   short dq_type ;
 1499   struct mem_dqblk dq_dqb ;
 1500};
 1501#line 303 "include/linux/quota.h"
 1502struct quota_format_ops {
 1503   int (*check_quota_file)(struct super_block * , int  ) ;
 1504   int (*read_file_info)(struct super_block * , int  ) ;
 1505   int (*write_file_info)(struct super_block * , int  ) ;
 1506   int (*free_file_info)(struct super_block * , int  ) ;
 1507   int (*read_dqblk)(struct dquot * ) ;
 1508   int (*commit_dqblk)(struct dquot * ) ;
 1509   int (*release_dqblk)(struct dquot * ) ;
 1510};
 1511#line 314 "include/linux/quota.h"
 1512struct dquot_operations {
 1513   int (*write_dquot)(struct dquot * ) ;
 1514   struct dquot *(*alloc_dquot)(struct super_block * , int  ) ;
 1515   void (*destroy_dquot)(struct dquot * ) ;
 1516   int (*acquire_dquot)(struct dquot * ) ;
 1517   int (*release_dquot)(struct dquot * ) ;
 1518   int (*mark_dirty)(struct dquot * ) ;
 1519   int (*write_info)(struct super_block * , int  ) ;
 1520   qsize_t *(*get_reserved_space)(struct inode * ) ;
 1521};
 1522#line 328 "include/linux/quota.h"
 1523struct quotactl_ops {
 1524   int (*quota_on)(struct super_block * , int  , int  , struct path * ) ;
 1525   int (*quota_on_meta)(struct super_block * , int  , int  ) ;
 1526   int (*quota_off)(struct super_block * , int  ) ;
 1527   int (*quota_sync)(struct super_block * , int  , int  ) ;
 1528   int (*get_info)(struct super_block * , int  , struct if_dqinfo * ) ;
 1529   int (*set_info)(struct super_block * , int  , struct if_dqinfo * ) ;
 1530   int (*get_dqblk)(struct super_block * , int  , qid_t  , struct fs_disk_quota * ) ;
 1531   int (*set_dqblk)(struct super_block * , int  , qid_t  , struct fs_disk_quota * ) ;
 1532   int (*get_xstate)(struct super_block * , struct fs_quota_stat * ) ;
 1533   int (*set_xstate)(struct super_block * , unsigned int  , int  ) ;
 1534};
 1535#line 344 "include/linux/quota.h"
 1536struct quota_format_type {
 1537   int qf_fmt_id ;
 1538   struct quota_format_ops  const  *qf_ops ;
 1539   struct module *qf_owner ;
 1540   struct quota_format_type *qf_next ;
 1541};
 1542#line 390 "include/linux/quota.h"
 1543struct quota_info {
 1544   unsigned int flags ;
 1545   struct mutex dqio_mutex ;
 1546   struct mutex dqonoff_mutex ;
 1547   struct rw_semaphore dqptr_sem ;
 1548   struct inode *files[2U] ;
 1549   struct mem_dqinfo info[2U] ;
 1550   struct quota_format_ops  const  *ops[2U] ;
 1551};
 1552#line 421
 1553struct address_space;
 1554#line 421
 1555struct address_space;
 1556#line 422
 1557struct writeback_control;
 1558#line 422
 1559struct writeback_control;
 1560#line 585 "include/linux/fs.h"
 1561union __anonunion_arg_138 {
 1562   char *buf ;
 1563   void *data ;
 1564};
 1565#line 585 "include/linux/fs.h"
 1566struct __anonstruct_read_descriptor_t_137 {
 1567   size_t written ;
 1568   size_t count ;
 1569   union __anonunion_arg_138 arg ;
 1570   int error ;
 1571};
 1572#line 585 "include/linux/fs.h"
 1573typedef struct __anonstruct_read_descriptor_t_137 read_descriptor_t;
 1574#line 588 "include/linux/fs.h"
 1575struct address_space_operations {
 1576   int (*writepage)(struct page * , struct writeback_control * ) ;
 1577   int (*readpage)(struct file * , struct page * ) ;
 1578   int (*writepages)(struct address_space * , struct writeback_control * ) ;
 1579   int (*set_page_dirty)(struct page * ) ;
 1580   int (*readpages)(struct file * , struct address_space * , struct list_head * ,
 1581                    unsigned int  ) ;
 1582   int (*write_begin)(struct file * , struct address_space * , loff_t  , unsigned int  ,
 1583                      unsigned int  , struct page ** , void ** ) ;
 1584   int (*write_end)(struct file * , struct address_space * , loff_t  , unsigned int  ,
 1585                    unsigned int  , struct page * , void * ) ;
 1586   sector_t (*bmap)(struct address_space * , sector_t  ) ;
 1587   void (*invalidatepage)(struct page * , unsigned long  ) ;
 1588   int (*releasepage)(struct page * , gfp_t  ) ;
 1589   void (*freepage)(struct page * ) ;
 1590   ssize_t (*direct_IO)(int  , struct kiocb * , struct iovec  const  * , loff_t  ,
 1591                        unsigned long  ) ;
 1592   int (*get_xip_mem)(struct address_space * , unsigned long  , int  , void ** , unsigned long * ) ;
 1593   int (*migratepage)(struct address_space * , struct page * , struct page * , enum migrate_mode  ) ;
 1594   int (*launder_page)(struct page * ) ;
 1595   int (*is_partially_uptodate)(struct page * , read_descriptor_t * , unsigned long  ) ;
 1596   int (*error_remove_page)(struct address_space * , struct page * ) ;
 1597};
 1598#line 642
 1599struct backing_dev_info;
 1600#line 642
 1601struct backing_dev_info;
 1602#line 643 "include/linux/fs.h"
 1603struct address_space {
 1604   struct inode *host ;
 1605   struct radix_tree_root page_tree ;
 1606   spinlock_t tree_lock ;
 1607   unsigned int i_mmap_writable ;
 1608   struct prio_tree_root i_mmap ;
 1609   struct list_head i_mmap_nonlinear ;
 1610   struct mutex i_mmap_mutex ;
 1611   unsigned long nrpages ;
 1612   unsigned long writeback_index ;
 1613   struct address_space_operations  const  *a_ops ;
 1614   unsigned long flags ;
 1615   struct backing_dev_info *backing_dev_info ;
 1616   spinlock_t private_lock ;
 1617   struct list_head private_list ;
 1618   struct address_space *assoc_mapping ;
 1619};
 1620#line 664
 1621struct request_queue;
 1622#line 664
 1623struct request_queue;
 1624#line 665
 1625struct hd_struct;
 1626#line 665
 1627struct gendisk;
 1628#line 665 "include/linux/fs.h"
 1629struct block_device {
 1630   dev_t bd_dev ;
 1631   int bd_openers ;
 1632   struct inode *bd_inode ;
 1633   struct super_block *bd_super ;
 1634   struct mutex bd_mutex ;
 1635   struct list_head bd_inodes ;
 1636   void *bd_claiming ;
 1637   void *bd_holder ;
 1638   int bd_holders ;
 1639   bool bd_write_holder ;
 1640   struct list_head bd_holder_disks ;
 1641   struct block_device *bd_contains ;
 1642   unsigned int bd_block_size ;
 1643   struct hd_struct *bd_part ;
 1644   unsigned int bd_part_count ;
 1645   int bd_invalidated ;
 1646   struct gendisk *bd_disk ;
 1647   struct request_queue *bd_queue ;
 1648   struct list_head bd_list ;
 1649   unsigned long bd_private ;
 1650   int bd_fsfreeze_count ;
 1651   struct mutex bd_fsfreeze_mutex ;
 1652};
 1653#line 737
 1654struct posix_acl;
 1655#line 737
 1656struct posix_acl;
 1657#line 738
 1658struct inode_operations;
 1659#line 738 "include/linux/fs.h"
 1660union __anonunion_ldv_15748_139 {
 1661   unsigned int const   i_nlink ;
 1662   unsigned int __i_nlink ;
 1663};
 1664#line 738 "include/linux/fs.h"
 1665union __anonunion_ldv_15767_140 {
 1666   struct list_head i_dentry ;
 1667   struct rcu_head i_rcu ;
 1668};
 1669#line 738
 1670struct file_operations;
 1671#line 738
 1672struct file_lock;
 1673#line 738
 1674struct cdev;
 1675#line 738 "include/linux/fs.h"
 1676union __anonunion_ldv_15785_141 {
 1677   struct pipe_inode_info *i_pipe ;
 1678   struct block_device *i_bdev ;
 1679   struct cdev *i_cdev ;
 1680};
 1681#line 738 "include/linux/fs.h"
 1682struct inode {
 1683   umode_t i_mode ;
 1684   unsigned short i_opflags ;
 1685   uid_t i_uid ;
 1686   gid_t i_gid ;
 1687   unsigned int i_flags ;
 1688   struct posix_acl *i_acl ;
 1689   struct posix_acl *i_default_acl ;
 1690   struct inode_operations  const  *i_op ;
 1691   struct super_block *i_sb ;
 1692   struct address_space *i_mapping ;
 1693   void *i_security ;
 1694   unsigned long i_ino ;
 1695   union __anonunion_ldv_15748_139 ldv_15748 ;
 1696   dev_t i_rdev ;
 1697   struct timespec i_atime ;
 1698   struct timespec i_mtime ;
 1699   struct timespec i_ctime ;
 1700   spinlock_t i_lock ;
 1701   unsigned short i_bytes ;
 1702   blkcnt_t i_blocks ;
 1703   loff_t i_size ;
 1704   unsigned long i_state ;
 1705   struct mutex i_mutex ;
 1706   unsigned long dirtied_when ;
 1707   struct hlist_node i_hash ;
 1708   struct list_head i_wb_list ;
 1709   struct list_head i_lru ;
 1710   struct list_head i_sb_list ;
 1711   union __anonunion_ldv_15767_140 ldv_15767 ;
 1712   atomic_t i_count ;
 1713   unsigned int i_blkbits ;
 1714   u64 i_version ;
 1715   atomic_t i_dio_count ;
 1716   atomic_t i_writecount ;
 1717   struct file_operations  const  *i_fop ;
 1718   struct file_lock *i_flock ;
 1719   struct address_space i_data ;
 1720   struct dquot *i_dquot[2U] ;
 1721   struct list_head i_devices ;
 1722   union __anonunion_ldv_15785_141 ldv_15785 ;
 1723   __u32 i_generation ;
 1724   __u32 i_fsnotify_mask ;
 1725   struct hlist_head i_fsnotify_marks ;
 1726   atomic_t i_readcount ;
 1727   void *i_private ;
 1728};
 1729#line 941 "include/linux/fs.h"
 1730struct fown_struct {
 1731   rwlock_t lock ;
 1732   struct pid *pid ;
 1733   enum pid_type pid_type ;
 1734   uid_t uid ;
 1735   uid_t euid ;
 1736   int signum ;
 1737};
 1738#line 949 "include/linux/fs.h"
 1739struct file_ra_state {
 1740   unsigned long start ;
 1741   unsigned int size ;
 1742   unsigned int async_size ;
 1743   unsigned int ra_pages ;
 1744   unsigned int mmap_miss ;
 1745   loff_t prev_pos ;
 1746};
 1747#line 972 "include/linux/fs.h"
 1748union __anonunion_f_u_142 {
 1749   struct list_head fu_list ;
 1750   struct rcu_head fu_rcuhead ;
 1751};
 1752#line 972 "include/linux/fs.h"
 1753struct file {
 1754   union __anonunion_f_u_142 f_u ;
 1755   struct path f_path ;
 1756   struct file_operations  const  *f_op ;
 1757   spinlock_t f_lock ;
 1758   int f_sb_list_cpu ;
 1759   atomic_long_t f_count ;
 1760   unsigned int f_flags ;
 1761   fmode_t f_mode ;
 1762   loff_t f_pos ;
 1763   struct fown_struct f_owner ;
 1764   struct cred  const  *f_cred ;
 1765   struct file_ra_state f_ra ;
 1766   u64 f_version ;
 1767   void *f_security ;
 1768   void *private_data ;
 1769   struct list_head f_ep_links ;
 1770   struct list_head f_tfile_llink ;
 1771   struct address_space *f_mapping ;
 1772   unsigned long f_mnt_write_state ;
 1773};
 1774#line 1111
 1775struct files_struct;
 1776#line 1111 "include/linux/fs.h"
 1777typedef struct files_struct *fl_owner_t;
 1778#line 1112 "include/linux/fs.h"
 1779struct file_lock_operations {
 1780   void (*fl_copy_lock)(struct file_lock * , struct file_lock * ) ;
 1781   void (*fl_release_private)(struct file_lock * ) ;
 1782};
 1783#line 1117 "include/linux/fs.h"
 1784struct lock_manager_operations {
 1785   int (*lm_compare_owner)(struct file_lock * , struct file_lock * ) ;
 1786   void (*lm_notify)(struct file_lock * ) ;
 1787   int (*lm_grant)(struct file_lock * , struct file_lock * , int  ) ;
 1788   void (*lm_release_private)(struct file_lock * ) ;
 1789   void (*lm_break)(struct file_lock * ) ;
 1790   int (*lm_change)(struct file_lock ** , int  ) ;
 1791};
 1792#line 1134
 1793struct nlm_lockowner;
 1794#line 1134
 1795struct nlm_lockowner;
 1796#line 1135 "include/linux/fs.h"
 1797struct nfs_lock_info {
 1798   u32 state ;
 1799   struct nlm_lockowner *owner ;
 1800   struct list_head list ;
 1801};
 1802#line 14 "include/linux/nfs_fs_i.h"
 1803struct nfs4_lock_state;
 1804#line 14
 1805struct nfs4_lock_state;
 1806#line 15 "include/linux/nfs_fs_i.h"
 1807struct nfs4_lock_info {
 1808   struct nfs4_lock_state *owner ;
 1809};
 1810#line 19
 1811struct fasync_struct;
 1812#line 19 "include/linux/nfs_fs_i.h"
 1813struct __anonstruct_afs_144 {
 1814   struct list_head link ;
 1815   int state ;
 1816};
 1817#line 19 "include/linux/nfs_fs_i.h"
 1818union __anonunion_fl_u_143 {
 1819   struct nfs_lock_info nfs_fl ;
 1820   struct nfs4_lock_info nfs4_fl ;
 1821   struct __anonstruct_afs_144 afs ;
 1822};
 1823#line 19 "include/linux/nfs_fs_i.h"
 1824struct file_lock {
 1825   struct file_lock *fl_next ;
 1826   struct list_head fl_link ;
 1827   struct list_head fl_block ;
 1828   fl_owner_t fl_owner ;
 1829   unsigned int fl_flags ;
 1830   unsigned char fl_type ;
 1831   unsigned int fl_pid ;
 1832   struct pid *fl_nspid ;
 1833   wait_queue_head_t fl_wait ;
 1834   struct file *fl_file ;
 1835   loff_t fl_start ;
 1836   loff_t fl_end ;
 1837   struct fasync_struct *fl_fasync ;
 1838   unsigned long fl_break_time ;
 1839   unsigned long fl_downgrade_time ;
 1840   struct file_lock_operations  const  *fl_ops ;
 1841   struct lock_manager_operations  const  *fl_lmops ;
 1842   union __anonunion_fl_u_143 fl_u ;
 1843};
 1844#line 1221 "include/linux/fs.h"
 1845struct fasync_struct {
 1846   spinlock_t fa_lock ;
 1847   int magic ;
 1848   int fa_fd ;
 1849   struct fasync_struct *fa_next ;
 1850   struct file *fa_file ;
 1851   struct rcu_head fa_rcu ;
 1852};
 1853#line 1417
 1854struct file_system_type;
 1855#line 1417
 1856struct super_operations;
 1857#line 1417
 1858struct xattr_handler;
 1859#line 1417
 1860struct mtd_info;
 1861#line 1417 "include/linux/fs.h"
 1862struct super_block {
 1863   struct list_head s_list ;
 1864   dev_t s_dev ;
 1865   unsigned char s_dirt ;
 1866   unsigned char s_blocksize_bits ;
 1867   unsigned long s_blocksize ;
 1868   loff_t s_maxbytes ;
 1869   struct file_system_type *s_type ;
 1870   struct super_operations  const  *s_op ;
 1871   struct dquot_operations  const  *dq_op ;
 1872   struct quotactl_ops  const  *s_qcop ;
 1873   struct export_operations  const  *s_export_op ;
 1874   unsigned long s_flags ;
 1875   unsigned long s_magic ;
 1876   struct dentry *s_root ;
 1877   struct rw_semaphore s_umount ;
 1878   struct mutex s_lock ;
 1879   int s_count ;
 1880   atomic_t s_active ;
 1881   void *s_security ;
 1882   struct xattr_handler  const  **s_xattr ;
 1883   struct list_head s_inodes ;
 1884   struct hlist_bl_head s_anon ;
 1885   struct list_head *s_files ;
 1886   struct list_head s_mounts ;
 1887   struct list_head s_dentry_lru ;
 1888   int s_nr_dentry_unused ;
 1889   spinlock_t s_inode_lru_lock ;
 1890   struct list_head s_inode_lru ;
 1891   int s_nr_inodes_unused ;
 1892   struct block_device *s_bdev ;
 1893   struct backing_dev_info *s_bdi ;
 1894   struct mtd_info *s_mtd ;
 1895   struct hlist_node s_instances ;
 1896   struct quota_info s_dquot ;
 1897   int s_frozen ;
 1898   wait_queue_head_t s_wait_unfrozen ;
 1899   char s_id[32U] ;
 1900   u8 s_uuid[16U] ;
 1901   void *s_fs_info ;
 1902   unsigned int s_max_links ;
 1903   fmode_t s_mode ;
 1904   u32 s_time_gran ;
 1905   struct mutex s_vfs_rename_mutex ;
 1906   char *s_subtype ;
 1907   char *s_options ;
 1908   struct dentry_operations  const  *s_d_op ;
 1909   int cleancache_poolid ;
 1910   struct shrinker s_shrink ;
 1911   atomic_long_t s_remove_count ;
 1912   int s_readonly_remount ;
 1913};
 1914#line 1563 "include/linux/fs.h"
 1915struct fiemap_extent_info {
 1916   unsigned int fi_flags ;
 1917   unsigned int fi_extents_mapped ;
 1918   unsigned int fi_extents_max ;
 1919   struct fiemap_extent *fi_extents_start ;
 1920};
 1921#line 1602 "include/linux/fs.h"
 1922struct file_operations {
 1923   struct module *owner ;
 1924   loff_t (*llseek)(struct file * , loff_t  , int  ) ;
 1925   ssize_t (*read)(struct file * , char * , size_t  , loff_t * ) ;
 1926   ssize_t (*write)(struct file * , char const   * , size_t  , loff_t * ) ;
 1927   ssize_t (*aio_read)(struct kiocb * , struct iovec  const  * , unsigned long  ,
 1928                       loff_t  ) ;
 1929   ssize_t (*aio_write)(struct kiocb * , struct iovec  const  * , unsigned long  ,
 1930                        loff_t  ) ;
 1931   int (*readdir)(struct file * , void * , int (*)(void * , char const   * , int  ,
 1932                                                   loff_t  , u64  , unsigned int  ) ) ;
 1933   unsigned int (*poll)(struct file * , struct poll_table_struct * ) ;
 1934   long (*unlocked_ioctl)(struct file * , unsigned int  , unsigned long  ) ;
 1935   long (*compat_ioctl)(struct file * , unsigned int  , unsigned long  ) ;
 1936   int (*mmap)(struct file * , struct vm_area_struct * ) ;
 1937   int (*open)(struct inode * , struct file * ) ;
 1938   int (*flush)(struct file * , fl_owner_t  ) ;
 1939   int (*release)(struct inode * , struct file * ) ;
 1940   int (*fsync)(struct file * , loff_t  , loff_t  , int  ) ;
 1941   int (*aio_fsync)(struct kiocb * , int  ) ;
 1942   int (*fasync)(int  , struct file * , int  ) ;
 1943   int (*lock)(struct file * , int  , struct file_lock * ) ;
 1944   ssize_t (*sendpage)(struct file * , struct page * , int  , size_t  , loff_t * ,
 1945                       int  ) ;
 1946   unsigned long (*get_unmapped_area)(struct file * , unsigned long  , unsigned long  ,
 1947                                      unsigned long  , unsigned long  ) ;
 1948   int (*check_flags)(int  ) ;
 1949   int (*flock)(struct file * , int  , struct file_lock * ) ;
 1950   ssize_t (*splice_write)(struct pipe_inode_info * , struct file * , loff_t * , size_t  ,
 1951                           unsigned int  ) ;
 1952   ssize_t (*splice_read)(struct file * , loff_t * , struct pipe_inode_info * , size_t  ,
 1953                          unsigned int  ) ;
 1954   int (*setlease)(struct file * , long  , struct file_lock ** ) ;
 1955   long (*fallocate)(struct file * , int  , loff_t  , loff_t  ) ;
 1956};
 1957#line 1637 "include/linux/fs.h"
 1958struct inode_operations {
 1959   struct dentry *(*lookup)(struct inode * , struct dentry * , struct nameidata * ) ;
 1960   void *(*follow_link)(struct dentry * , struct nameidata * ) ;
 1961   int (*permission)(struct inode * , int  ) ;
 1962   struct posix_acl *(*get_acl)(struct inode * , int  ) ;
 1963   int (*readlink)(struct dentry * , char * , int  ) ;
 1964   void (*put_link)(struct dentry * , struct nameidata * , void * ) ;
 1965   int (*create)(struct inode * , struct dentry * , umode_t  , struct nameidata * ) ;
 1966   int (*link)(struct dentry * , struct inode * , struct dentry * ) ;
 1967   int (*unlink)(struct inode * , struct dentry * ) ;
 1968   int (*symlink)(struct inode * , struct dentry * , char const   * ) ;
 1969   int (*mkdir)(struct inode * , struct dentry * , umode_t  ) ;
 1970   int (*rmdir)(struct inode * , struct dentry * ) ;
 1971   int (*mknod)(struct inode * , struct dentry * , umode_t  , dev_t  ) ;
 1972   int (*rename)(struct inode * , struct dentry * , struct inode * , struct dentry * ) ;
 1973   void (*truncate)(struct inode * ) ;
 1974   int (*setattr)(struct dentry * , struct iattr * ) ;
 1975   int (*getattr)(struct vfsmount * , struct dentry * , struct kstat * ) ;
 1976   int (*setxattr)(struct dentry * , char const   * , void const   * , size_t  , int  ) ;
 1977   ssize_t (*getxattr)(struct dentry * , char const   * , void * , size_t  ) ;
 1978   ssize_t (*listxattr)(struct dentry * , char * , size_t  ) ;
 1979   int (*removexattr)(struct dentry * , char const   * ) ;
 1980   void (*truncate_range)(struct inode * , loff_t  , loff_t  ) ;
 1981   int (*fiemap)(struct inode * , struct fiemap_extent_info * , u64  , u64  ) ;
 1982};
 1983#line 1682 "include/linux/fs.h"
 1984struct super_operations {
 1985   struct inode *(*alloc_inode)(struct super_block * ) ;
 1986   void (*destroy_inode)(struct inode * ) ;
 1987   void (*dirty_inode)(struct inode * , int  ) ;
 1988   int (*write_inode)(struct inode * , struct writeback_control * ) ;
 1989   int (*drop_inode)(struct inode * ) ;
 1990   void (*evict_inode)(struct inode * ) ;
 1991   void (*put_super)(struct super_block * ) ;
 1992   void (*write_super)(struct super_block * ) ;
 1993   int (*sync_fs)(struct super_block * , int  ) ;
 1994   int (*freeze_fs)(struct super_block * ) ;
 1995   int (*unfreeze_fs)(struct super_block * ) ;
 1996   int (*statfs)(struct dentry * , struct kstatfs * ) ;
 1997   int (*remount_fs)(struct super_block * , int * , char * ) ;
 1998   void (*umount_begin)(struct super_block * ) ;
 1999   int (*show_options)(struct seq_file * , struct dentry * ) ;
 2000   int (*show_devname)(struct seq_file * , struct dentry * ) ;
 2001   int (*show_path)(struct seq_file * , struct dentry * ) ;
 2002   int (*show_stats)(struct seq_file * , struct dentry * ) ;
 2003   ssize_t (*quota_read)(struct super_block * , int  , char * , size_t  , loff_t  ) ;
 2004   ssize_t (*quota_write)(struct super_block * , int  , char const   * , size_t  ,
 2005                          loff_t  ) ;
 2006   int (*bdev_try_to_free_page)(struct super_block * , struct page * , gfp_t  ) ;
 2007   int (*nr_cached_objects)(struct super_block * ) ;
 2008   void (*free_cached_objects)(struct super_block * , int  ) ;
 2009};
 2010#line 1834 "include/linux/fs.h"
 2011struct file_system_type {
 2012   char const   *name ;
 2013   int fs_flags ;
 2014   struct dentry *(*mount)(struct file_system_type * , int  , char const   * , void * ) ;
 2015   void (*kill_sb)(struct super_block * ) ;
 2016   struct module *owner ;
 2017   struct file_system_type *next ;
 2018   struct hlist_head fs_supers ;
 2019   struct lock_class_key s_lock_key ;
 2020   struct lock_class_key s_umount_key ;
 2021   struct lock_class_key s_vfs_rename_key ;
 2022   struct lock_class_key i_lock_key ;
 2023   struct lock_class_key i_mutex_key ;
 2024   struct lock_class_key i_mutex_dir_key ;
 2025};
 2026#line 2674 "include/linux/fs.h"
 2027struct seq_file {
 2028   char *buf ;
 2029   size_t size ;
 2030   size_t from ;
 2031   size_t count ;
 2032   loff_t index ;
 2033   loff_t read_pos ;
 2034   u64 version ;
 2035   struct mutex lock ;
 2036   struct seq_operations  const  *op ;
 2037   int poll_event ;
 2038   void *private ;
 2039};
 2040#line 30 "include/linux/seq_file.h"
 2041struct seq_operations {
 2042   void *(*start)(struct seq_file * , loff_t * ) ;
 2043   void (*stop)(struct seq_file * , void * ) ;
 2044   void *(*next)(struct seq_file * , void * , loff_t * ) ;
 2045   int (*show)(struct seq_file * , void * ) ;
 2046};
 2047#line 12 "include/linux/mod_devicetable.h"
 2048typedef unsigned long kernel_ulong_t;
 2049#line 181 "include/linux/mod_devicetable.h"
 2050struct acpi_device_id {
 2051   __u8 id[16U] ;
 2052   kernel_ulong_t driver_data ;
 2053};
 2054#line 215 "include/linux/mod_devicetable.h"
 2055struct of_device_id {
 2056   char name[32U] ;
 2057   char type[32U] ;
 2058   char compatible[128U] ;
 2059   void *data ;
 2060};
 2061#line 469 "include/linux/mod_devicetable.h"
 2062struct dmi_strmatch {
 2063   unsigned char slot ;
 2064   char substr[79U] ;
 2065};
 2066#line 476 "include/linux/mod_devicetable.h"
 2067struct dmi_system_id {
 2068   int (*callback)(struct dmi_system_id  const  * ) ;
 2069   char const   *ident ;
 2070   struct dmi_strmatch matches[4U] ;
 2071   void *driver_data ;
 2072};
 2073#line 55 "include/linux/sched.h"
 2074union __anonunion_ldv_18273_147 {
 2075   unsigned long index ;
 2076   void *freelist ;
 2077};
 2078#line 55 "include/linux/sched.h"
 2079struct __anonstruct_ldv_18283_151 {
 2080   unsigned short inuse ;
 2081   unsigned short objects : 15 ;
 2082   unsigned char frozen : 1 ;
 2083};
 2084#line 55 "include/linux/sched.h"
 2085union __anonunion_ldv_18284_150 {
 2086   atomic_t _mapcount ;
 2087   struct __anonstruct_ldv_18283_151 ldv_18283 ;
 2088};
 2089#line 55 "include/linux/sched.h"
 2090struct __anonstruct_ldv_18286_149 {
 2091   union __anonunion_ldv_18284_150 ldv_18284 ;
 2092   atomic_t _count ;
 2093};
 2094#line 55 "include/linux/sched.h"
 2095union __anonunion_ldv_18287_148 {
 2096   unsigned long counters ;
 2097   struct __anonstruct_ldv_18286_149 ldv_18286 ;
 2098};
 2099#line 55 "include/linux/sched.h"
 2100struct __anonstruct_ldv_18288_146 {
 2101   union __anonunion_ldv_18273_147 ldv_18273 ;
 2102   union __anonunion_ldv_18287_148 ldv_18287 ;
 2103};
 2104#line 55 "include/linux/sched.h"
 2105struct __anonstruct_ldv_18295_153 {
 2106   struct page *next ;
 2107   int pages ;
 2108   int pobjects ;
 2109};
 2110#line 55 "include/linux/sched.h"
 2111union __anonunion_ldv_18296_152 {
 2112   struct list_head lru ;
 2113   struct __anonstruct_ldv_18295_153 ldv_18295 ;
 2114};
 2115#line 55 "include/linux/sched.h"
 2116union __anonunion_ldv_18301_154 {
 2117   unsigned long private ;
 2118   struct kmem_cache *slab ;
 2119   struct page *first_page ;
 2120};
 2121#line 55 "include/linux/sched.h"
 2122struct page {
 2123   unsigned long flags ;
 2124   struct address_space *mapping ;
 2125   struct __anonstruct_ldv_18288_146 ldv_18288 ;
 2126   union __anonunion_ldv_18296_152 ldv_18296 ;
 2127   union __anonunion_ldv_18301_154 ldv_18301 ;
 2128   unsigned long debug_flags ;
 2129};
 2130#line 192 "include/linux/mm_types.h"
 2131struct __anonstruct_vm_set_156 {
 2132   struct list_head list ;
 2133   void *parent ;
 2134   struct vm_area_struct *head ;
 2135};
 2136#line 192 "include/linux/mm_types.h"
 2137union __anonunion_shared_155 {
 2138   struct __anonstruct_vm_set_156 vm_set ;
 2139   struct raw_prio_tree_node prio_tree_node ;
 2140};
 2141#line 192
 2142struct anon_vma;
 2143#line 192
 2144struct vm_operations_struct;
 2145#line 192
 2146struct mempolicy;
 2147#line 192 "include/linux/mm_types.h"
 2148struct vm_area_struct {
 2149   struct mm_struct *vm_mm ;
 2150   unsigned long vm_start ;
 2151   unsigned long vm_end ;
 2152   struct vm_area_struct *vm_next ;
 2153   struct vm_area_struct *vm_prev ;
 2154   pgprot_t vm_page_prot ;
 2155   unsigned long vm_flags ;
 2156   struct rb_node vm_rb ;
 2157   union __anonunion_shared_155 shared ;
 2158   struct list_head anon_vma_chain ;
 2159   struct anon_vma *anon_vma ;
 2160   struct vm_operations_struct  const  *vm_ops ;
 2161   unsigned long vm_pgoff ;
 2162   struct file *vm_file ;
 2163   void *vm_private_data ;
 2164   struct mempolicy *vm_policy ;
 2165};
 2166#line 255 "include/linux/mm_types.h"
 2167struct core_thread {
 2168   struct task_struct *task ;
 2169   struct core_thread *next ;
 2170};
 2171#line 261 "include/linux/mm_types.h"
 2172struct core_state {
 2173   atomic_t nr_threads ;
 2174   struct core_thread dumper ;
 2175   struct completion startup ;
 2176};
 2177#line 274 "include/linux/mm_types.h"
 2178struct mm_rss_stat {
 2179   atomic_long_t count[3U] ;
 2180};
 2181#line 287
 2182struct linux_binfmt;
 2183#line 287
 2184struct mmu_notifier_mm;
 2185#line 287 "include/linux/mm_types.h"
 2186struct mm_struct {
 2187   struct vm_area_struct *mmap ;
 2188   struct rb_root mm_rb ;
 2189   struct vm_area_struct *mmap_cache ;
 2190   unsigned long (*get_unmapped_area)(struct file * , unsigned long  , unsigned long  ,
 2191                                      unsigned long  , unsigned long  ) ;
 2192   void (*unmap_area)(struct mm_struct * , unsigned long  ) ;
 2193   unsigned long mmap_base ;
 2194   unsigned long task_size ;
 2195   unsigned long cached_hole_size ;
 2196   unsigned long free_area_cache ;
 2197   pgd_t *pgd ;
 2198   atomic_t mm_users ;
 2199   atomic_t mm_count ;
 2200   int map_count ;
 2201   spinlock_t page_table_lock ;
 2202   struct rw_semaphore mmap_sem ;
 2203   struct list_head mmlist ;
 2204   unsigned long hiwater_rss ;
 2205   unsigned long hiwater_vm ;
 2206   unsigned long total_vm ;
 2207   unsigned long locked_vm ;
 2208   unsigned long pinned_vm ;
 2209   unsigned long shared_vm ;
 2210   unsigned long exec_vm ;
 2211   unsigned long stack_vm ;
 2212   unsigned long reserved_vm ;
 2213   unsigned long def_flags ;
 2214   unsigned long nr_ptes ;
 2215   unsigned long start_code ;
 2216   unsigned long end_code ;
 2217   unsigned long start_data ;
 2218   unsigned long end_data ;
 2219   unsigned long start_brk ;
 2220   unsigned long brk ;
 2221   unsigned long start_stack ;
 2222   unsigned long arg_start ;
 2223   unsigned long arg_end ;
 2224   unsigned long env_start ;
 2225   unsigned long env_end ;
 2226   unsigned long saved_auxv[44U] ;
 2227   struct mm_rss_stat rss_stat ;
 2228   struct linux_binfmt *binfmt ;
 2229   cpumask_var_t cpu_vm_mask_var ;
 2230   mm_context_t context ;
 2231   unsigned int faultstamp ;
 2232   unsigned int token_priority ;
 2233   unsigned int last_interval ;
 2234   unsigned long flags ;
 2235   struct core_state *core_state ;
 2236   spinlock_t ioctx_lock ;
 2237   struct hlist_head ioctx_list ;
 2238   struct task_struct *owner ;
 2239   struct file *exe_file ;
 2240   unsigned long num_exe_file_vmas ;
 2241   struct mmu_notifier_mm *mmu_notifier_mm ;
 2242   pgtable_t pmd_huge_pte ;
 2243   struct cpumask cpumask_allocation ;
 2244};
 2245#line 7 "include/asm-generic/cputime.h"
 2246typedef unsigned long cputime_t;
 2247#line 98 "include/linux/sem.h"
 2248struct sem_undo_list;
 2249#line 98 "include/linux/sem.h"
 2250struct sysv_sem {
 2251   struct sem_undo_list *undo_list ;
 2252};
 2253#line 107
 2254struct siginfo;
 2255#line 107
 2256struct siginfo;
 2257#line 32 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
 2258struct __anonstruct_sigset_t_157 {
 2259   unsigned long sig[1U] ;
 2260};
 2261#line 32 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
 2262typedef struct __anonstruct_sigset_t_157 sigset_t;
 2263#line 17 "include/asm-generic/signal-defs.h"
 2264typedef void __signalfn_t(int  );
 2265#line 18 "include/asm-generic/signal-defs.h"
 2266typedef __signalfn_t *__sighandler_t;
 2267#line 20 "include/asm-generic/signal-defs.h"
 2268typedef void __restorefn_t(void);
 2269#line 21 "include/asm-generic/signal-defs.h"
 2270typedef __restorefn_t *__sigrestore_t;
 2271#line 126 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
 2272struct sigaction {
 2273   __sighandler_t sa_handler ;
 2274   unsigned long sa_flags ;
 2275   __sigrestore_t sa_restorer ;
 2276   sigset_t sa_mask ;
 2277};
 2278#line 173 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
 2279struct k_sigaction {
 2280   struct sigaction sa ;
 2281};
 2282#line 185 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
 2283union sigval {
 2284   int sival_int ;
 2285   void *sival_ptr ;
 2286};
 2287#line 10 "include/asm-generic/siginfo.h"
 2288typedef union sigval sigval_t;
 2289#line 11 "include/asm-generic/siginfo.h"
 2290struct __anonstruct__kill_159 {
 2291   __kernel_pid_t _pid ;
 2292   __kernel_uid32_t _uid ;
 2293};
 2294#line 11 "include/asm-generic/siginfo.h"
 2295struct __anonstruct__timer_160 {
 2296   __kernel_timer_t _tid ;
 2297   int _overrun ;
 2298   char _pad[0U] ;
 2299   sigval_t _sigval ;
 2300   int _sys_private ;
 2301};
 2302#line 11 "include/asm-generic/siginfo.h"
 2303struct __anonstruct__rt_161 {
 2304   __kernel_pid_t _pid ;
 2305   __kernel_uid32_t _uid ;
 2306   sigval_t _sigval ;
 2307};
 2308#line 11 "include/asm-generic/siginfo.h"
 2309struct __anonstruct__sigchld_162 {
 2310   __kernel_pid_t _pid ;
 2311   __kernel_uid32_t _uid ;
 2312   int _status ;
 2313   __kernel_clock_t _utime ;
 2314   __kernel_clock_t _stime ;
 2315};
 2316#line 11 "include/asm-generic/siginfo.h"
 2317struct __anonstruct__sigfault_163 {
 2318   void *_addr ;
 2319   short _addr_lsb ;
 2320};
 2321#line 11 "include/asm-generic/siginfo.h"
 2322struct __anonstruct__sigpoll_164 {
 2323   long _band ;
 2324   int _fd ;
 2325};
 2326#line 11 "include/asm-generic/siginfo.h"
 2327union __anonunion__sifields_158 {
 2328   int _pad[28U] ;
 2329   struct __anonstruct__kill_159 _kill ;
 2330   struct __anonstruct__timer_160 _timer ;
 2331   struct __anonstruct__rt_161 _rt ;
 2332   struct __anonstruct__sigchld_162 _sigchld ;
 2333   struct __anonstruct__sigfault_163 _sigfault ;
 2334   struct __anonstruct__sigpoll_164 _sigpoll ;
 2335};
 2336#line 11 "include/asm-generic/siginfo.h"
 2337struct siginfo {
 2338   int si_signo ;
 2339   int si_errno ;
 2340   int si_code ;
 2341   union __anonunion__sifields_158 _sifields ;
 2342};
 2343#line 102 "include/asm-generic/siginfo.h"
 2344typedef struct siginfo siginfo_t;
 2345#line 14 "include/linux/signal.h"
 2346struct user_struct;
 2347#line 24 "include/linux/signal.h"
 2348struct sigpending {
 2349   struct list_head list ;
 2350   sigset_t signal ;
 2351};
 2352#line 10 "include/linux/seccomp.h"
 2353struct __anonstruct_seccomp_t_167 {
 2354   int mode ;
 2355};
 2356#line 10 "include/linux/seccomp.h"
 2357typedef struct __anonstruct_seccomp_t_167 seccomp_t;
 2358#line 26 "include/linux/seccomp.h"
 2359struct plist_head {
 2360   struct list_head node_list ;
 2361};
 2362#line 84 "include/linux/plist.h"
 2363struct plist_node {
 2364   int prio ;
 2365   struct list_head prio_list ;
 2366   struct list_head node_list ;
 2367};
 2368#line 38 "include/linux/rtmutex.h"
 2369struct rt_mutex_waiter;
 2370#line 38
 2371struct rt_mutex_waiter;
 2372#line 41 "include/linux/resource.h"
 2373struct rlimit {
 2374   unsigned long rlim_cur ;
 2375   unsigned long rlim_max ;
 2376};
 2377#line 85 "include/linux/resource.h"
 2378struct timerqueue_node {
 2379   struct rb_node node ;
 2380   ktime_t expires ;
 2381};
 2382#line 12 "include/linux/timerqueue.h"
 2383struct timerqueue_head {
 2384   struct rb_root head ;
 2385   struct timerqueue_node *next ;
 2386};
 2387#line 50
 2388struct hrtimer_clock_base;
 2389#line 50
 2390struct hrtimer_clock_base;
 2391#line 51
 2392struct hrtimer_cpu_base;
 2393#line 51
 2394struct hrtimer_cpu_base;
 2395#line 60
 2396enum hrtimer_restart {
 2397    HRTIMER_NORESTART = 0,
 2398    HRTIMER_RESTART = 1
 2399} ;
 2400#line 65 "include/linux/timerqueue.h"
 2401struct hrtimer {
 2402   struct timerqueue_node node ;
 2403   ktime_t _softexpires ;
 2404   enum hrtimer_restart (*function)(struct hrtimer * ) ;
 2405   struct hrtimer_clock_base *base ;
 2406   unsigned long state ;
 2407   int start_pid ;
 2408   void *start_site ;
 2409   char start_comm[16U] ;
 2410};
 2411#line 132 "include/linux/hrtimer.h"
 2412struct hrtimer_clock_base {
 2413   struct hrtimer_cpu_base *cpu_base ;
 2414   int index ;
 2415   clockid_t clockid ;
 2416   struct timerqueue_head active ;
 2417   ktime_t resolution ;
 2418   ktime_t (*get_time)(void) ;
 2419   ktime_t softirq_time ;
 2420   ktime_t offset ;
 2421};
 2422#line 162 "include/linux/hrtimer.h"
 2423struct hrtimer_cpu_base {
 2424   raw_spinlock_t lock ;
 2425   unsigned long active_bases ;
 2426   ktime_t expires_next ;
 2427   int hres_active ;
 2428   int hang_detected ;
 2429   unsigned long nr_events ;
 2430   unsigned long nr_retries ;
 2431   unsigned long nr_hangs ;
 2432   ktime_t max_hang_time ;
 2433   struct hrtimer_clock_base clock_base[3U] ;
 2434};
 2435#line 452 "include/linux/hrtimer.h"
 2436struct task_io_accounting {
 2437   u64 rchar ;
 2438   u64 wchar ;
 2439   u64 syscr ;
 2440   u64 syscw ;
 2441   u64 read_bytes ;
 2442   u64 write_bytes ;
 2443   u64 cancelled_write_bytes ;
 2444};
 2445#line 45 "include/linux/task_io_accounting.h"
 2446struct latency_record {
 2447   unsigned long backtrace[12U] ;
 2448   unsigned int count ;
 2449   unsigned long time ;
 2450   unsigned long max ;
 2451};
 2452#line 29 "include/linux/key.h"
 2453typedef int32_t key_serial_t;
 2454#line 32 "include/linux/key.h"
 2455typedef uint32_t key_perm_t;
 2456#line 33
 2457struct key;
 2458#line 33
 2459struct key;
 2460#line 34
 2461struct signal_struct;
 2462#line 34
 2463struct signal_struct;
 2464#line 35
 2465struct key_type;
 2466#line 35
 2467struct key_type;
 2468#line 37
 2469struct keyring_list;
 2470#line 37
 2471struct keyring_list;
 2472#line 115
 2473struct key_user;
 2474#line 115 "include/linux/key.h"
 2475union __anonunion_ldv_19340_168 {
 2476   time_t expiry ;
 2477   time_t revoked_at ;
 2478};
 2479#line 115 "include/linux/key.h"
 2480union __anonunion_type_data_169 {
 2481   struct list_head link ;
 2482   unsigned long x[2U] ;
 2483   void *p[2U] ;
 2484   int reject_error ;
 2485};
 2486#line 115 "include/linux/key.h"
 2487union __anonunion_payload_170 {
 2488   unsigned long value ;
 2489   void *rcudata ;
 2490   void *data ;
 2491   struct keyring_list *subscriptions ;
 2492};
 2493#line 115 "include/linux/key.h"
 2494struct key {
 2495   atomic_t usage ;
 2496   key_serial_t serial ;
 2497   struct rb_node serial_node ;
 2498   struct key_type *type ;
 2499   struct rw_semaphore sem ;
 2500   struct key_user *user ;
 2501   void *security ;
 2502   union __anonunion_ldv_19340_168 ldv_19340 ;
 2503   uid_t uid ;
 2504   gid_t gid ;
 2505   key_perm_t perm ;
 2506   unsigned short quotalen ;
 2507   unsigned short datalen ;
 2508   unsigned long flags ;
 2509   char *description ;
 2510   union __anonunion_type_data_169 type_data ;
 2511   union __anonunion_payload_170 payload ;
 2512};
 2513#line 316
 2514struct audit_context;
 2515#line 316
 2516struct audit_context;
 2517#line 27 "include/linux/selinux.h"
 2518struct group_info {
 2519   atomic_t usage ;
 2520   int ngroups ;
 2521   int nblocks ;
 2522   gid_t small_block[32U] ;
 2523   gid_t *blocks[0U] ;
 2524};
 2525#line 77 "include/linux/cred.h"
 2526struct thread_group_cred {
 2527   atomic_t usage ;
 2528   pid_t tgid ;
 2529   spinlock_t lock ;
 2530   struct key *session_keyring ;
 2531   struct key *process_keyring ;
 2532   struct rcu_head rcu ;
 2533};
 2534#line 91 "include/linux/cred.h"
 2535struct cred {
 2536   atomic_t usage ;
 2537   atomic_t subscribers ;
 2538   void *put_addr ;
 2539   unsigned int magic ;
 2540   uid_t uid ;
 2541   gid_t gid ;
 2542   uid_t suid ;
 2543   gid_t sgid ;
 2544   uid_t euid ;
 2545   gid_t egid ;
 2546   uid_t fsuid ;
 2547   gid_t fsgid ;
 2548   unsigned int securebits ;
 2549   kernel_cap_t cap_inheritable ;
 2550   kernel_cap_t cap_permitted ;
 2551   kernel_cap_t cap_effective ;
 2552   kernel_cap_t cap_bset ;
 2553   unsigned char jit_keyring ;
 2554   struct key *thread_keyring ;
 2555   struct key *request_key_auth ;
 2556   struct thread_group_cred *tgcred ;
 2557   void *security ;
 2558   struct user_struct *user ;
 2559   struct user_namespace *user_ns ;
 2560   struct group_info *group_info ;
 2561   struct rcu_head rcu ;
 2562};
 2563#line 264
 2564struct llist_node;
 2565#line 64 "include/linux/llist.h"
 2566struct llist_node {
 2567   struct llist_node *next ;
 2568};
 2569#line 185
 2570struct futex_pi_state;
 2571#line 185
 2572struct futex_pi_state;
 2573#line 186
 2574struct robust_list_head;
 2575#line 186
 2576struct robust_list_head;
 2577#line 187
 2578struct bio_list;
 2579#line 187
 2580struct bio_list;
 2581#line 188
 2582struct fs_struct;
 2583#line 188
 2584struct fs_struct;
 2585#line 189
 2586struct perf_event_context;
 2587#line 189
 2588struct perf_event_context;
 2589#line 190
 2590struct blk_plug;
 2591#line 190
 2592struct blk_plug;
 2593#line 149 "include/linux/sched.h"
 2594struct cfs_rq;
 2595#line 149
 2596struct cfs_rq;
 2597#line 44 "include/linux/aio_abi.h"
 2598struct io_event {
 2599   __u64 data ;
 2600   __u64 obj ;
 2601   __s64 res ;
 2602   __s64 res2 ;
 2603};
 2604#line 106 "include/linux/aio_abi.h"
 2605struct iovec {
 2606   void *iov_base ;
 2607   __kernel_size_t iov_len ;
 2608};
 2609#line 54 "include/linux/uio.h"
 2610struct kioctx;
 2611#line 54
 2612struct kioctx;
 2613#line 55 "include/linux/uio.h"
 2614union __anonunion_ki_obj_171 {
 2615   void *user ;
 2616   struct task_struct *tsk ;
 2617};
 2618#line 55
 2619struct eventfd_ctx;
 2620#line 55 "include/linux/uio.h"
 2621struct kiocb {
 2622   struct list_head ki_run_list ;
 2623   unsigned long ki_flags ;
 2624   int ki_users ;
 2625   unsigned int ki_key ;
 2626   struct file *ki_filp ;
 2627   struct kioctx *ki_ctx ;
 2628   int (*ki_cancel)(struct kiocb * , struct io_event * ) ;
 2629   ssize_t (*ki_retry)(struct kiocb * ) ;
 2630   void (*ki_dtor)(struct kiocb * ) ;
 2631   union __anonunion_ki_obj_171 ki_obj ;
 2632   __u64 ki_user_data ;
 2633   loff_t ki_pos ;
 2634   void *private ;
 2635   unsigned short ki_opcode ;
 2636   size_t ki_nbytes ;
 2637   char *ki_buf ;
 2638   size_t ki_left ;
 2639   struct iovec ki_inline_vec ;
 2640   struct iovec *ki_iovec ;
 2641   unsigned long ki_nr_segs ;
 2642   unsigned long ki_cur_seg ;
 2643   struct list_head ki_list ;
 2644   struct list_head ki_batch ;
 2645   struct eventfd_ctx *ki_eventfd ;
 2646};
 2647#line 162 "include/linux/aio.h"
 2648struct aio_ring_info {
 2649   unsigned long mmap_base ;
 2650   unsigned long mmap_size ;
 2651   struct page **ring_pages ;
 2652   spinlock_t ring_lock ;
 2653   long nr_pages ;
 2654   unsigned int nr ;
 2655   unsigned int tail ;
 2656   struct page *internal_pages[8U] ;
 2657};
 2658#line 178 "include/linux/aio.h"
 2659struct kioctx {
 2660   atomic_t users ;
 2661   int dead ;
 2662   struct mm_struct *mm ;
 2663   unsigned long user_id ;
 2664   struct hlist_node list ;
 2665   wait_queue_head_t wait ;
 2666   spinlock_t ctx_lock ;
 2667   int reqs_active ;
 2668   struct list_head active_reqs ;
 2669   struct list_head run_list ;
 2670   unsigned int max_reqs ;
 2671   struct aio_ring_info ring_info ;
 2672   struct delayed_work wq ;
 2673   struct rcu_head rcu_head ;
 2674};
 2675#line 406 "include/linux/sched.h"
 2676struct sighand_struct {
 2677   atomic_t count ;
 2678   struct k_sigaction action[64U] ;
 2679   spinlock_t siglock ;
 2680   wait_queue_head_t signalfd_wqh ;
 2681};
 2682#line 449 "include/linux/sched.h"
 2683struct pacct_struct {
 2684   int ac_flag ;
 2685   long ac_exitcode ;
 2686   unsigned long ac_mem ;
 2687   cputime_t ac_utime ;
 2688   cputime_t ac_stime ;
 2689   unsigned long ac_minflt ;
 2690   unsigned long ac_majflt ;
 2691};
 2692#line 457 "include/linux/sched.h"
 2693struct cpu_itimer {
 2694   cputime_t expires ;
 2695   cputime_t incr ;
 2696   u32 error ;
 2697   u32 incr_error ;
 2698};
 2699#line 464 "include/linux/sched.h"
 2700struct task_cputime {
 2701   cputime_t utime ;
 2702   cputime_t stime ;
 2703   unsigned long long sum_exec_runtime ;
 2704};
 2705#line 481 "include/linux/sched.h"
 2706struct thread_group_cputimer {
 2707   struct task_cputime cputime ;
 2708   int running ;
 2709   raw_spinlock_t lock ;
 2710};
 2711#line 517
 2712struct autogroup;
 2713#line 517
 2714struct autogroup;
 2715#line 518
 2716struct tty_struct;
 2717#line 518
 2718struct taskstats;
 2719#line 518
 2720struct tty_audit_buf;
 2721#line 518 "include/linux/sched.h"
 2722struct signal_struct {
 2723   atomic_t sigcnt ;
 2724   atomic_t live ;
 2725   int nr_threads ;
 2726   wait_queue_head_t wait_chldexit ;
 2727   struct task_struct *curr_target ;
 2728   struct sigpending shared_pending ;
 2729   int group_exit_code ;
 2730   int notify_count ;
 2731   struct task_struct *group_exit_task ;
 2732   int group_stop_count ;
 2733   unsigned int flags ;
 2734   unsigned char is_child_subreaper : 1 ;
 2735   unsigned char has_child_subreaper : 1 ;
 2736   struct list_head posix_timers ;
 2737   struct hrtimer real_timer ;
 2738   struct pid *leader_pid ;
 2739   ktime_t it_real_incr ;
 2740   struct cpu_itimer it[2U] ;
 2741   struct thread_group_cputimer cputimer ;
 2742   struct task_cputime cputime_expires ;
 2743   struct list_head cpu_timers[3U] ;
 2744   struct pid *tty_old_pgrp ;
 2745   int leader ;
 2746   struct tty_struct *tty ;
 2747   struct autogroup *autogroup ;
 2748   cputime_t utime ;
 2749   cputime_t stime ;
 2750   cputime_t cutime ;
 2751   cputime_t cstime ;
 2752   cputime_t gtime ;
 2753   cputime_t cgtime ;
 2754   cputime_t prev_utime ;
 2755   cputime_t prev_stime ;
 2756   unsigned long nvcsw ;
 2757   unsigned long nivcsw ;
 2758   unsigned long cnvcsw ;
 2759   unsigned long cnivcsw ;
 2760   unsigned long min_flt ;
 2761   unsigned long maj_flt ;
 2762   unsigned long cmin_flt ;
 2763   unsigned long cmaj_flt ;
 2764   unsigned long inblock ;
 2765   unsigned long oublock ;
 2766   unsigned long cinblock ;
 2767   unsigned long coublock ;
 2768   unsigned long maxrss ;
 2769   unsigned long cmaxrss ;
 2770   struct task_io_accounting ioac ;
 2771   unsigned long long sum_sched_runtime ;
 2772   struct rlimit rlim[16U] ;
 2773   struct pacct_struct pacct ;
 2774   struct taskstats *stats ;
 2775   unsigned int audit_tty ;
 2776   struct tty_audit_buf *tty_audit_buf ;
 2777   struct rw_semaphore group_rwsem ;
 2778   int oom_adj ;
 2779   int oom_score_adj ;
 2780   int oom_score_adj_min ;
 2781   struct mutex cred_guard_mutex ;
 2782};
 2783#line 699 "include/linux/sched.h"
 2784struct user_struct {
 2785   atomic_t __count ;
 2786   atomic_t processes ;
 2787   atomic_t files ;
 2788   atomic_t sigpending ;
 2789   atomic_t inotify_watches ;
 2790   atomic_t inotify_devs ;
 2791   atomic_t fanotify_listeners ;
 2792   atomic_long_t epoll_watches ;
 2793   unsigned long mq_bytes ;
 2794   unsigned long locked_shm ;
 2795   struct key *uid_keyring ;
 2796   struct key *session_keyring ;
 2797   struct hlist_node uidhash_node ;
 2798   uid_t uid ;
 2799   struct user_namespace *user_ns ;
 2800   atomic_long_t locked_vm ;
 2801};
 2802#line 744
 2803struct reclaim_state;
 2804#line 744
 2805struct reclaim_state;
 2806#line 745 "include/linux/sched.h"
 2807struct sched_info {
 2808   unsigned long pcount ;
 2809   unsigned long long run_delay ;
 2810   unsigned long long last_arrival ;
 2811   unsigned long long last_queued ;
 2812};
 2813#line 760 "include/linux/sched.h"
 2814struct task_delay_info {
 2815   spinlock_t lock ;
 2816   unsigned int flags ;
 2817   struct timespec blkio_start ;
 2818   struct timespec blkio_end ;
 2819   u64 blkio_delay ;
 2820   u64 swapin_delay ;
 2821   u32 blkio_count ;
 2822   u32 swapin_count ;
 2823   struct timespec freepages_start ;
 2824   struct timespec freepages_end ;
 2825   u64 freepages_delay ;
 2826   u32 freepages_count ;
 2827};
 2828#line 1069
 2829struct io_context;
 2830#line 1069
 2831struct io_context;
 2832#line 1098
 2833struct rq;
 2834#line 1098
 2835struct rq;
 2836#line 1099 "include/linux/sched.h"
 2837struct sched_class {
 2838   struct sched_class  const  *next ;
 2839   void (*enqueue_task)(struct rq * , struct task_struct * , int  ) ;
 2840   void (*dequeue_task)(struct rq * , struct task_struct * , int  ) ;
 2841   void (*yield_task)(struct rq * ) ;
 2842   bool (*yield_to_task)(struct rq * , struct task_struct * , bool  ) ;
 2843   void (*check_preempt_curr)(struct rq * , struct task_struct * , int  ) ;
 2844   struct task_struct *(*pick_next_task)(struct rq * ) ;
 2845   void (*put_prev_task)(struct rq * , struct task_struct * ) ;
 2846   int (*select_task_rq)(struct task_struct * , int  , int  ) ;
 2847   void (*pre_schedule)(struct rq * , struct task_struct * ) ;
 2848   void (*post_schedule)(struct rq * ) ;
 2849   void (*task_waking)(struct task_struct * ) ;
 2850   void (*task_woken)(struct rq * , struct task_struct * ) ;
 2851   void (*set_cpus_allowed)(struct task_struct * , struct cpumask  const  * ) ;
 2852   void (*rq_online)(struct rq * ) ;
 2853   void (*rq_offline)(struct rq * ) ;
 2854   void (*set_curr_task)(struct rq * ) ;
 2855   void (*task_tick)(struct rq * , struct task_struct * , int  ) ;
 2856   void (*task_fork)(struct task_struct * ) ;
 2857   void (*switched_from)(struct rq * , struct task_struct * ) ;
 2858   void (*switched_to)(struct rq * , struct task_struct * ) ;
 2859   void (*prio_changed)(struct rq * , struct task_struct * , int  ) ;
 2860   unsigned int (*get_rr_interval)(struct rq * , struct task_struct * ) ;
 2861   void (*task_move_group)(struct task_struct * , int  ) ;
 2862};
 2863#line 1165 "include/linux/sched.h"
 2864struct load_weight {
 2865   unsigned long weight ;
 2866   unsigned long inv_weight ;
 2867};
 2868#line 1170 "include/linux/sched.h"
 2869struct sched_statistics {
 2870   u64 wait_start ;
 2871   u64 wait_max ;
 2872   u64 wait_count ;
 2873   u64 wait_sum ;
 2874   u64 iowait_count ;
 2875   u64 iowait_sum ;
 2876   u64 sleep_start ;
 2877   u64 sleep_max ;
 2878   s64 sum_sleep_runtime ;
 2879   u64 block_start ;
 2880   u64 block_max ;
 2881   u64 exec_max ;
 2882   u64 slice_max ;
 2883   u64 nr_migrations_cold ;
 2884   u64 nr_failed_migrations_affine ;
 2885   u64 nr_failed_migrations_running ;
 2886   u64 nr_failed_migrations_hot ;
 2887   u64 nr_forced_migrations ;
 2888   u64 nr_wakeups ;
 2889   u64 nr_wakeups_sync ;
 2890   u64 nr_wakeups_migrate ;
 2891   u64 nr_wakeups_local ;
 2892   u64 nr_wakeups_remote ;
 2893   u64 nr_wakeups_affine ;
 2894   u64 nr_wakeups_affine_attempts ;
 2895   u64 nr_wakeups_passive ;
 2896   u64 nr_wakeups_idle ;
 2897};
 2898#line 1205 "include/linux/sched.h"
 2899struct sched_entity {
 2900   struct load_weight load ;
 2901   struct rb_node run_node ;
 2902   struct list_head group_node ;
 2903   unsigned int on_rq ;
 2904   u64 exec_start ;
 2905   u64 sum_exec_runtime ;
 2906   u64 vruntime ;
 2907   u64 prev_sum_exec_runtime ;
 2908   u64 nr_migrations ;
 2909   struct sched_statistics statistics ;
 2910   struct sched_entity *parent ;
 2911   struct cfs_rq *cfs_rq ;
 2912   struct cfs_rq *my_q ;
 2913};
 2914#line 1231
 2915struct rt_rq;
 2916#line 1231 "include/linux/sched.h"
 2917struct sched_rt_entity {
 2918   struct list_head run_list ;
 2919   unsigned long timeout ;
 2920   unsigned int time_slice ;
 2921   int nr_cpus_allowed ;
 2922   struct sched_rt_entity *back ;
 2923   struct sched_rt_entity *parent ;
 2924   struct rt_rq *rt_rq ;
 2925   struct rt_rq *my_q ;
 2926};
 2927#line 1255
 2928struct mem_cgroup;
 2929#line 1255 "include/linux/sched.h"
 2930struct memcg_batch_info {
 2931   int do_batch ;
 2932   struct mem_cgroup *memcg ;
 2933   unsigned long nr_pages ;
 2934   unsigned long memsw_nr_pages ;
 2935};
 2936#line 1616
 2937struct css_set;
 2938#line 1616
 2939struct compat_robust_list_head;
 2940#line 1616 "include/linux/sched.h"
 2941struct task_struct {
 2942   long volatile   state ;
 2943   void *stack ;
 2944   atomic_t usage ;
 2945   unsigned int flags ;
 2946   unsigned int ptrace ;
 2947   struct llist_node wake_entry ;
 2948   int on_cpu ;
 2949   int on_rq ;
 2950   int prio ;
 2951   int static_prio ;
 2952   int normal_prio ;
 2953   unsigned int rt_priority ;
 2954   struct sched_class  const  *sched_class ;
 2955   struct sched_entity se ;
 2956   struct sched_rt_entity rt ;
 2957   struct hlist_head preempt_notifiers ;
 2958   unsigned char fpu_counter ;
 2959   unsigned int policy ;
 2960   cpumask_t cpus_allowed ;
 2961   struct sched_info sched_info ;
 2962   struct list_head tasks ;
 2963   struct plist_node pushable_tasks ;
 2964   struct mm_struct *mm ;
 2965   struct mm_struct *active_mm ;
 2966   unsigned char brk_randomized : 1 ;
 2967   int exit_state ;
 2968   int exit_code ;
 2969   int exit_signal ;
 2970   int pdeath_signal ;
 2971   unsigned int jobctl ;
 2972   unsigned int personality ;
 2973   unsigned char did_exec : 1 ;
 2974   unsigned char in_execve : 1 ;
 2975   unsigned char in_iowait : 1 ;
 2976   unsigned char sched_reset_on_fork : 1 ;
 2977   unsigned char sched_contributes_to_load : 1 ;
 2978   unsigned char irq_thread : 1 ;
 2979   pid_t pid ;
 2980   pid_t tgid ;
 2981   unsigned long stack_canary ;
 2982   struct task_struct *real_parent ;
 2983   struct task_struct *parent ;
 2984   struct list_head children ;
 2985   struct list_head sibling ;
 2986   struct task_struct *group_leader ;
 2987   struct list_head ptraced ;
 2988   struct list_head ptrace_entry ;
 2989   struct pid_link pids[3U] ;
 2990   struct list_head thread_group ;
 2991   struct completion *vfork_done ;
 2992   int *set_child_tid ;
 2993   int *clear_child_tid ;
 2994   cputime_t utime ;
 2995   cputime_t stime ;
 2996   cputime_t utimescaled ;
 2997   cputime_t stimescaled ;
 2998   cputime_t gtime ;
 2999   cputime_t prev_utime ;
 3000   cputime_t prev_stime ;
 3001   unsigned long nvcsw ;
 3002   unsigned long nivcsw ;
 3003   struct timespec start_time ;
 3004   struct timespec real_start_time ;
 3005   unsigned long min_flt ;
 3006   unsigned long maj_flt ;
 3007   struct task_cputime cputime_expires ;
 3008   struct list_head cpu_timers[3U] ;
 3009   struct cred  const  *real_cred ;
 3010   struct cred  const  *cred ;
 3011   struct cred *replacement_session_keyring ;
 3012   char comm[16U] ;
 3013   int link_count ;
 3014   int total_link_count ;
 3015   struct sysv_sem sysvsem ;
 3016   unsigned long last_switch_count ;
 3017   struct thread_struct thread ;
 3018   struct fs_struct *fs ;
 3019   struct files_struct *files ;
 3020   struct nsproxy *nsproxy ;
 3021   struct signal_struct *signal ;
 3022   struct sighand_struct *sighand ;
 3023   sigset_t blocked ;
 3024   sigset_t real_blocked ;
 3025   sigset_t saved_sigmask ;
 3026   struct sigpending pending ;
 3027   unsigned long sas_ss_sp ;
 3028   size_t sas_ss_size ;
 3029   int (*notifier)(void * ) ;
 3030   void *notifier_data ;
 3031   sigset_t *notifier_mask ;
 3032   struct audit_context *audit_context ;
 3033   uid_t loginuid ;
 3034   unsigned int sessionid ;
 3035   seccomp_t seccomp ;
 3036   u32 parent_exec_id ;
 3037   u32 self_exec_id ;
 3038   spinlock_t alloc_lock ;
 3039   raw_spinlock_t pi_lock ;
 3040   struct plist_head pi_waiters ;
 3041   struct rt_mutex_waiter *pi_blocked_on ;
 3042   struct mutex_waiter *blocked_on ;
 3043   unsigned int irq_events ;
 3044   unsigned long hardirq_enable_ip ;
 3045   unsigned long hardirq_disable_ip ;
 3046   unsigned int hardirq_enable_event ;
 3047   unsigned int hardirq_disable_event ;
 3048   int hardirqs_enabled ;
 3049   int hardirq_context ;
 3050   unsigned long softirq_disable_ip ;
 3051   unsigned long softirq_enable_ip ;
 3052   unsigned int softirq_disable_event ;
 3053   unsigned int softirq_enable_event ;
 3054   int softirqs_enabled ;
 3055   int softirq_context ;
 3056   u64 curr_chain_key ;
 3057   int lockdep_depth ;
 3058   unsigned int lockdep_recursion ;
 3059   struct held_lock held_locks[48U] ;
 3060   gfp_t lockdep_reclaim_gfp ;
 3061   void *journal_info ;
 3062   struct bio_list *bio_list ;
 3063   struct blk_plug *plug ;
 3064   struct reclaim_state *reclaim_state ;
 3065   struct backing_dev_info *backing_dev_info ;
 3066   struct io_context *io_context ;
 3067   unsigned long ptrace_message ;
 3068   siginfo_t *last_siginfo ;
 3069   struct task_io_accounting ioac ;
 3070   u64 acct_rss_mem1 ;
 3071   u64 acct_vm_mem1 ;
 3072   cputime_t acct_timexpd ;
 3073   nodemask_t mems_allowed ;
 3074   seqcount_t mems_allowed_seq ;
 3075   int cpuset_mem_spread_rotor ;
 3076   int cpuset_slab_spread_rotor ;
 3077   struct css_set *cgroups ;
 3078   struct list_head cg_list ;
 3079   struct robust_list_head *robust_list ;
 3080   struct compat_robust_list_head *compat_robust_list ;
 3081   struct list_head pi_state_list ;
 3082   struct futex_pi_state *pi_state_cache ;
 3083   struct perf_event_context *perf_event_ctxp[2U] ;
 3084   struct mutex perf_event_mutex ;
 3085   struct list_head perf_event_list ;
 3086   struct mempolicy *mempolicy ;
 3087   short il_next ;
 3088   short pref_node_fork ;
 3089   struct rcu_head rcu ;
 3090   struct pipe_inode_info *splice_pipe ;
 3091   struct task_delay_info *delays ;
 3092   int make_it_fail ;
 3093   int nr_dirtied ;
 3094   int nr_dirtied_pause ;
 3095   unsigned long dirty_paused_when ;
 3096   int latency_record_count ;
 3097   struct latency_record latency_record[32U] ;
 3098   unsigned long timer_slack_ns ;
 3099   unsigned long default_timer_slack_ns ;
 3100   struct list_head *scm_work_list ;
 3101   unsigned long trace ;
 3102   unsigned long trace_recursion ;
 3103   struct memcg_batch_info memcg_batch ;
 3104   atomic_t ptrace_bp_refcnt ;
 3105};
 3106#line 161 "include/acpi/actypes.h"
 3107typedef u64 acpi_size;
 3108#line 162 "include/acpi/actypes.h"
 3109typedef u64 acpi_io_address;
 3110#line 371 "include/acpi/actypes.h"
 3111typedef u32 acpi_status;
 3112#line 373 "include/acpi/actypes.h"
 3113typedef char *acpi_string;
 3114#line 374 "include/acpi/actypes.h"
 3115typedef void *acpi_handle;
 3116#line 556 "include/acpi/actypes.h"
 3117typedef u32 acpi_object_type;
 3118#line 807 "include/acpi/actypes.h"
 3119struct __anonstruct_integer_173 {
 3120   acpi_object_type type ;
 3121   u64 value ;
 3122};
 3123#line 807 "include/acpi/actypes.h"
 3124struct __anonstruct_string_174 {
 3125   acpi_object_type type ;
 3126   u32 length ;
 3127   char *pointer ;
 3128};
 3129#line 807 "include/acpi/actypes.h"
 3130struct __anonstruct_buffer_175 {
 3131   acpi_object_type type ;
 3132   u32 length ;
 3133   u8 *pointer ;
 3134};
 3135#line 807 "include/acpi/actypes.h"
 3136struct __anonstruct_package_176 {
 3137   acpi_object_type type ;
 3138   u32 count ;
 3139   union acpi_object *elements ;
 3140};
 3141#line 807 "include/acpi/actypes.h"
 3142struct __anonstruct_reference_177 {
 3143   acpi_object_type type ;
 3144   acpi_object_type actual_type ;
 3145   acpi_handle handle ;
 3146};
 3147#line 807 "include/acpi/actypes.h"
 3148struct __anonstruct_processor_178 {
 3149   acpi_object_type type ;
 3150   u32 proc_id ;
 3151   acpi_io_address pblk_address ;
 3152   u32 pblk_length ;
 3153};
 3154#line 807 "include/acpi/actypes.h"
 3155struct __anonstruct_power_resource_179 {
 3156   acpi_object_type type ;
 3157   u32 system_level ;
 3158   u32 resource_order ;
 3159};
 3160#line 807 "include/acpi/actypes.h"
 3161union acpi_object {
 3162   acpi_object_type type ;
 3163   struct __anonstruct_integer_173 integer ;
 3164   struct __anonstruct_string_174 string ;
 3165   struct __anonstruct_buffer_175 buffer ;
 3166   struct __anonstruct_package_176 package ;
 3167   struct __anonstruct_reference_177 reference ;
 3168   struct __anonstruct_processor_178 processor ;
 3169   struct __anonstruct_power_resource_179 power_resource ;
 3170};
 3171#line 860 "include/acpi/actypes.h"
 3172struct acpi_object_list {
 3173   u32 count ;
 3174   union acpi_object *pointer ;
 3175};
 3176#line 868 "include/acpi/actypes.h"
 3177struct acpi_buffer {
 3178   acpi_size length ;
 3179   void *pointer ;
 3180};
 3181#line 530 "include/acpi/acpixf.h"
 3182struct klist_node;
 3183#line 530
 3184struct klist_node;
 3185#line 37 "include/linux/klist.h"
 3186struct klist_node {
 3187   void *n_klist ;
 3188   struct list_head n_node ;
 3189   struct kref n_ref ;
 3190};
 3191#line 67
 3192struct dma_map_ops;
 3193#line 67 "include/linux/klist.h"
 3194struct dev_archdata {
 3195   void *acpi_handle ;
 3196   struct dma_map_ops *dma_ops ;
 3197   void *iommu ;
 3198};
 3199#line 17 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 3200struct device_private;
 3201#line 17
 3202struct device_private;
 3203#line 18
 3204struct device_driver;
 3205#line 18
 3206struct device_driver;
 3207#line 19
 3208struct driver_private;
 3209#line 19
 3210struct driver_private;
 3211#line 20
 3212struct class;
 3213#line 20
 3214struct class;
 3215#line 21
 3216struct subsys_private;
 3217#line 21
 3218struct subsys_private;
 3219#line 22
 3220struct bus_type;
 3221#line 22
 3222struct bus_type;
 3223#line 23
 3224struct device_node;
 3225#line 23
 3226struct device_node;
 3227#line 24
 3228struct iommu_ops;
 3229#line 24
 3230struct iommu_ops;
 3231#line 25 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 3232struct bus_attribute {
 3233   struct attribute attr ;
 3234   ssize_t (*show)(struct bus_type * , char * ) ;
 3235   ssize_t (*store)(struct bus_type * , char const   * , size_t  ) ;
 3236};
 3237#line 51 "include/linux/device.h"
 3238struct device_attribute;
 3239#line 51
 3240struct driver_attribute;
 3241#line 51 "include/linux/device.h"
 3242struct bus_type {
 3243   char const   *name ;
 3244   char const   *dev_name ;
 3245   struct device *dev_root ;
 3246   struct bus_attribute *bus_attrs ;
 3247   struct device_attribute *dev_attrs ;
 3248   struct driver_attribute *drv_attrs ;
 3249   int (*match)(struct device * , struct device_driver * ) ;
 3250   int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
 3251   int (*probe)(struct device * ) ;
 3252   int (*remove)(struct device * ) ;
 3253   void (*shutdown)(struct device * ) ;
 3254   int (*suspend)(struct device * , pm_message_t  ) ;
 3255   int (*resume)(struct device * ) ;
 3256   struct dev_pm_ops  const  *pm ;
 3257   struct iommu_ops *iommu_ops ;
 3258   struct subsys_private *p ;
 3259};
 3260#line 125
 3261struct device_type;
 3262#line 182 "include/linux/device.h"
 3263struct device_driver {
 3264   char const   *name ;
 3265   struct bus_type *bus ;
 3266   struct module *owner ;
 3267   char const   *mod_name ;
 3268   bool suppress_bind_attrs ;
 3269   struct of_device_id  const  *of_match_table ;
 3270   int (*probe)(struct device * ) ;
 3271   int (*remove)(struct device * ) ;
 3272   void (*shutdown)(struct device * ) ;
 3273   int (*suspend)(struct device * , pm_message_t  ) ;
 3274   int (*resume)(struct device * ) ;
 3275   struct attribute_group  const  **groups ;
 3276   struct dev_pm_ops  const  *pm ;
 3277   struct driver_private *p ;
 3278};
 3279#line 245 "include/linux/device.h"
 3280struct driver_attribute {
 3281   struct attribute attr ;
 3282   ssize_t (*show)(struct device_driver * , char * ) ;
 3283   ssize_t (*store)(struct device_driver * , char const   * , size_t  ) ;
 3284};
 3285#line 299
 3286struct class_attribute;
 3287#line 299 "include/linux/device.h"
 3288struct class {
 3289   char const   *name ;
 3290   struct module *owner ;
 3291   struct class_attribute *class_attrs ;
 3292   struct device_attribute *dev_attrs ;
 3293   struct bin_attribute *dev_bin_attrs ;
 3294   struct kobject *dev_kobj ;
 3295   int (*dev_uevent)(struct device * , struct kobj_uevent_env * ) ;
 3296   char *(*devnode)(struct device * , umode_t * ) ;
 3297   void (*class_release)(struct class * ) ;
 3298   void (*dev_release)(struct device * ) ;
 3299   int (*suspend)(struct device * , pm_message_t  ) ;
 3300   int (*resume)(struct device * ) ;
 3301   struct kobj_ns_type_operations  const  *ns_type ;
 3302   void const   *(*namespace)(struct device * ) ;
 3303   struct dev_pm_ops  const  *pm ;
 3304   struct subsys_private *p ;
 3305};
 3306#line 394 "include/linux/device.h"
 3307struct class_attribute {
 3308   struct attribute attr ;
 3309   ssize_t (*show)(struct class * , struct class_attribute * , char * ) ;
 3310   ssize_t (*store)(struct class * , struct class_attribute * , char const   * , size_t  ) ;
 3311   void const   *(*namespace)(struct class * , struct class_attribute  const  * ) ;
 3312};
 3313#line 447 "include/linux/device.h"
 3314struct device_type {
 3315   char const   *name ;
 3316   struct attribute_group  const  **groups ;
 3317   int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
 3318   char *(*devnode)(struct device * , umode_t * ) ;
 3319   void (*release)(struct device * ) ;
 3320   struct dev_pm_ops  const  *pm ;
 3321};
 3322#line 474 "include/linux/device.h"
 3323struct device_attribute {
 3324   struct attribute attr ;
 3325   ssize_t (*show)(struct device * , struct device_attribute * , char * ) ;
 3326   ssize_t (*store)(struct device * , struct device_attribute * , char const   * ,
 3327                    size_t  ) ;
 3328};
 3329#line 557 "include/linux/device.h"
 3330struct device_dma_parameters {
 3331   unsigned int max_segment_size ;
 3332   unsigned long segment_boundary_mask ;
 3333};
 3334#line 567
 3335struct dma_coherent_mem;
 3336#line 567 "include/linux/device.h"
 3337struct device {
 3338   struct device *parent ;
 3339   struct device_private *p ;
 3340   struct kobject kobj ;
 3341   char const   *init_name ;
 3342   struct device_type  const  *type ;
 3343   struct mutex mutex ;
 3344   struct bus_type *bus ;
 3345   struct device_driver *driver ;
 3346   void *platform_data ;
 3347   struct dev_pm_info power ;
 3348   struct dev_pm_domain *pm_domain ;
 3349   int numa_node ;
 3350   u64 *dma_mask ;
 3351   u64 coherent_dma_mask ;
 3352   struct device_dma_parameters *dma_parms ;
 3353   struct list_head dma_pools ;
 3354   struct dma_coherent_mem *dma_mem ;
 3355   struct dev_archdata archdata ;
 3356   struct device_node *of_node ;
 3357   dev_t devt ;
 3358   u32 id ;
 3359   spinlock_t devres_lock ;
 3360   struct list_head devres_head ;
 3361   struct klist_node knode_class ;
 3362   struct class *class ;
 3363   struct attribute_group  const  **groups ;
 3364   void (*release)(struct device * ) ;
 3365};
 3366#line 681 "include/linux/device.h"
 3367struct wakeup_source {
 3368   char const   *name ;
 3369   struct list_head entry ;
 3370   spinlock_t lock ;
 3371   struct timer_list timer ;
 3372   unsigned long timer_expires ;
 3373   ktime_t total_time ;
 3374   ktime_t max_time ;
 3375   ktime_t last_time ;
 3376   unsigned long event_count ;
 3377   unsigned long active_count ;
 3378   unsigned long relax_count ;
 3379   unsigned long hit_count ;
 3380   unsigned char active : 1 ;
 3381};
 3382#line 991 "include/linux/device.h"
 3383struct acpi_handle_list {
 3384   u32 count ;
 3385   acpi_handle handles[10U] ;
 3386};
 3387#line 46 "include/linux/proc_fs.h"
 3388typedef int read_proc_t(char * , char ** , off_t  , int  , int * , void * );
 3389#line 48 "include/linux/proc_fs.h"
 3390typedef int write_proc_t(struct file * , char const   * , unsigned long  , void * );
 3391#line 49 "include/linux/proc_fs.h"
 3392struct proc_dir_entry {
 3393   unsigned int low_ino ;
 3394   umode_t mode ;
 3395   nlink_t nlink ;
 3396   uid_t uid ;
 3397   gid_t gid ;
 3398   loff_t size ;
 3399   struct inode_operations  const  *proc_iops ;
 3400   struct file_operations  const  *proc_fops ;
 3401   struct proc_dir_entry *next ;
 3402   struct proc_dir_entry *parent ;
 3403   struct proc_dir_entry *subdir ;
 3404   void *data ;
 3405   read_proc_t *read_proc ;
 3406   write_proc_t *write_proc ;
 3407   atomic_t count ;
 3408   int pde_users ;
 3409   struct completion *pde_unload_completion ;
 3410   struct list_head pde_openers ;
 3411   spinlock_t pde_unload_lock ;
 3412   u8 namelen ;
 3413   char name[0U] ;
 3414};
 3415#line 60 "include/acpi/acpi_bus.h"
 3416enum acpi_bus_removal_type {
 3417    ACPI_BUS_REMOVAL_NORMAL = 0,
 3418    ACPI_BUS_REMOVAL_EJECT = 1,
 3419    ACPI_BUS_REMOVAL_SUPRISE = 2,
 3420    ACPI_BUS_REMOVAL_TYPE_COUNT = 3
 3421} ;
 3422#line 77
 3423struct acpi_driver;
 3424#line 77
 3425struct acpi_driver;
 3426#line 78
 3427struct acpi_device;
 3428#line 78
 3429struct acpi_device;
 3430#line 95 "include/acpi/acpi_bus.h"
 3431struct acpi_bus_ops {
 3432   unsigned char acpi_op_add : 1 ;
 3433   unsigned char acpi_op_start : 1 ;
 3434};
 3435#line 100 "include/acpi/acpi_bus.h"
 3436struct acpi_device_ops {
 3437   int (*add)(struct acpi_device * ) ;
 3438   int (*remove)(struct acpi_device * , int  ) ;
 3439   int (*start)(struct acpi_device * ) ;
 3440   int (*suspend)(struct acpi_device * , pm_message_t  ) ;
 3441   int (*resume)(struct acpi_device * ) ;
 3442   int (*bind)(struct acpi_device * ) ;
 3443   int (*unbind)(struct acpi_device * ) ;
 3444   void (*notify)(struct acpi_device * , u32  ) ;
 3445};
 3446#line 111 "include/acpi/acpi_bus.h"
 3447struct acpi_driver {
 3448   char name[80U] ;
 3449   char class[80U] ;
 3450   struct acpi_device_id  const  *ids ;
 3451   unsigned int flags ;
 3452   struct acpi_device_ops ops ;
 3453   struct device_driver drv ;
 3454   struct module *owner ;
 3455};
 3456#line 123 "include/acpi/acpi_bus.h"
 3457struct acpi_device_status {
 3458   unsigned char present : 1 ;
 3459   unsigned char enabled : 1 ;
 3460   unsigned char show_in_ui : 1 ;
 3461   unsigned char functional : 1 ;
 3462   unsigned char battery_present : 1 ;
 3463   unsigned int reserved : 27 ;
 3464};
 3465#line 139 "include/acpi/acpi_bus.h"
 3466struct acpi_device_flags {
 3467   unsigned char dynamic_status : 1 ;
 3468   unsigned char bus_address : 1 ;
 3469   unsigned char removable : 1 ;
 3470   unsigned char ejectable : 1 ;
 3471   unsigned char lockable : 1 ;
 3472   unsigned char suprise_removal_ok : 1 ;
 3473   unsigned char power_manageable : 1 ;
 3474   unsigned char performance_manageable : 1 ;
 3475   unsigned int reserved : 24 ;
 3476};
 3477#line 153 "include/acpi/acpi_bus.h"
 3478struct acpi_device_dir {
 3479   struct proc_dir_entry *entry ;
 3480};
 3481#line 164 "include/acpi/acpi_bus.h"
 3482typedef char acpi_bus_id[8U];
 3483#line 165 "include/acpi/acpi_bus.h"
 3484typedef unsigned long acpi_bus_address;
 3485#line 166 "include/acpi/acpi_bus.h"
 3486typedef char acpi_device_name[40U];
 3487#line 167 "include/acpi/acpi_bus.h"
 3488typedef char acpi_device_class[20U];
 3489#line 173 "include/acpi/acpi_bus.h"
 3490struct acpi_device_pnp {
 3491   acpi_bus_id bus_id ;
 3492   acpi_bus_address bus_address ;
 3493   char *unique_id ;
 3494   struct list_head ids ;
 3495   acpi_device_name device_name ;
 3496   acpi_device_class device_class ;
 3497};
 3498#line 186 "include/acpi/acpi_bus.h"
 3499struct acpi_device_power_flags {
 3500   unsigned char explicit_get : 1 ;
 3501   unsigned char power_resources : 1 ;
 3502   unsigned char inrush_current : 1 ;
 3503   unsigned char power_removed : 1 ;
 3504   unsigned int reserved : 28 ;
 3505};
 3506#line 198 "include/acpi/acpi_bus.h"
 3507struct __anonstruct_flags_180 {
 3508   unsigned char valid : 1 ;
 3509   unsigned char explicit_set : 1 ;
 3510   unsigned char reserved : 6 ;
 3511};
 3512#line 198 "include/acpi/acpi_bus.h"
 3513struct acpi_device_power_state {
 3514   struct __anonstruct_flags_180 flags ;
 3515   int power ;
 3516   int latency ;
 3517   struct acpi_handle_list resources ;
 3518};
 3519#line 209 "include/acpi/acpi_bus.h"
 3520struct acpi_device_power {
 3521   int state ;
 3522   struct acpi_device_power_flags flags ;
 3523   struct acpi_device_power_state states[5U] ;
 3524};
 3525#line 215 "include/acpi/acpi_bus.h"
 3526struct acpi_device_perf_flags {
 3527   u8 reserved ;
 3528};
 3529#line 221 "include/acpi/acpi_bus.h"
 3530struct __anonstruct_flags_181 {
 3531   unsigned char valid : 1 ;
 3532   unsigned char reserved : 7 ;
 3533};
 3534#line 221 "include/acpi/acpi_bus.h"
 3535struct acpi_device_perf_state {
 3536   struct __anonstruct_flags_181 flags ;
 3537   u8 power ;
 3538   u8 performance ;
 3539   int latency ;
 3540};
 3541#line 231 "include/acpi/acpi_bus.h"
 3542struct acpi_device_perf {
 3543   int state ;
 3544   struct acpi_device_perf_flags flags ;
 3545   int state_count ;
 3546   struct acpi_device_perf_state *states ;
 3547};
 3548#line 238 "include/acpi/acpi_bus.h"
 3549struct acpi_device_wakeup_flags {
 3550   unsigned char valid : 1 ;
 3551   unsigned char run_wake : 1 ;
 3552   unsigned char notifier_present : 1 ;
 3553};
 3554#line 245 "include/acpi/acpi_bus.h"
 3555struct acpi_device_wakeup {
 3556   acpi_handle gpe_device ;
 3557   u64 gpe_number ;
 3558   u64 sleep_state ;
 3559   struct acpi_handle_list resources ;
 3560   struct acpi_device_wakeup_flags flags ;
 3561   int prepare_count ;
 3562};
 3563#line 254 "include/acpi/acpi_bus.h"
 3564struct acpi_device {
 3565   int device_type ;
 3566   acpi_handle handle ;
 3567   struct acpi_device *parent ;
 3568   struct list_head children ;
 3569   struct list_head node ;
 3570   struct list_head wakeup_list ;
 3571   struct acpi_device_status status ;
 3572   struct acpi_device_flags flags ;
 3573   struct acpi_device_pnp pnp ;
 3574   struct acpi_device_power power ;
 3575   struct acpi_device_wakeup wakeup ;
 3576   struct acpi_device_perf performance ;
 3577   struct acpi_device_dir dir ;
 3578   struct acpi_device_ops ops ;
 3579   struct acpi_driver *driver ;
 3580   void *driver_data ;
 3581   struct device dev ;
 3582   struct acpi_bus_ops bus_ops ;
 3583   enum acpi_bus_removal_type removal_type ;
 3584};
 3585#line 49 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p"
 3586enum atk_pack_member {
 3587    HWMON_PACK_FLAGS = 0,
 3588    HWMON_PACK_NAME = 1,
 3589    HWMON_PACK_LIMIT1 = 2,
 3590    HWMON_PACK_LIMIT2 = 3,
 3591    HWMON_PACK_ENABLE = 4
 3592} ;
 3593#line 57 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p"
 3594struct __anonstruct_debugfs_182 {
 3595   struct dentry *root ;
 3596   u32 id ;
 3597};
 3598#line 57 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p"
 3599struct atk_data {
 3600   struct device *hwmon_dev ;
 3601   acpi_handle atk_handle ;
 3602   struct acpi_device *acpi_dev ;
 3603   bool old_interface ;
 3604   acpi_handle rtmp_handle ;
 3605   acpi_handle rvlt_handle ;
 3606   acpi_handle rfan_handle ;
 3607   acpi_handle enumerate_handle ;
 3608   acpi_handle read_handle ;
 3609   acpi_handle write_handle ;
 3610   bool disable_ec ;
 3611   int voltage_count ;
 3612   int temperature_count ;
 3613   int fan_count ;
 3614   struct list_head sensor_list ;
 3615   struct __anonstruct_debugfs_182 debugfs ;
 3616};
 3617#line 156 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p"
 3618struct atk_sensor_data {
 3619   struct list_head list ;
 3620   struct atk_data *data ;
 3621   struct device_attribute label_attr ;
 3622   struct device_attribute input_attr ;
 3623   struct device_attribute limit1_attr ;
 3624   struct device_attribute limit2_attr ;
 3625   char label_attr_name[16U] ;
 3626   char input_attr_name[16U] ;
 3627   char limit1_attr_name[16U] ;
 3628   char limit2_attr_name[16U] ;
 3629   u64 id ;
 3630   u64 type ;
 3631   u64 limit1 ;
 3632   u64 limit2 ;
 3633   u64 cached_value ;
 3634   unsigned long last_updated ;
 3635   bool is_valid ;
 3636   char const   *acpi_name ;
 3637};
 3638#line 179 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p"
 3639struct atk_acpi_ret_buffer {
 3640   u32 flags ;
 3641   u32 value ;
 3642   u8 data[0U] ;
 3643};
 3644#line 191 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p"
 3645struct atk_acpi_input_buf {
 3646   u32 id ;
 3647   u32 param1 ;
 3648   u32 param2 ;
 3649};
 3650#line 1 "<compiler builtins>"
 3651long __builtin_expect(long  , long  ) ;
 3652#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p"
 3653void ldv_spin_lock(void) ;
 3654#line 3
 3655void ldv_spin_unlock(void) ;
 3656#line 4
 3657int ldv_spin_trylock(void) ;
 3658#line 101 "include/linux/printk.h"
 3659extern int printk(char const   *  , ...) ;
 3660#line 50 "include/linux/dynamic_debug.h"
 3661extern int __dynamic_dev_dbg(struct _ddebug * , struct device  const  * , char const   * 
 3662                             , ...) ;
 3663#line 320 "include/linux/kernel.h"
 3664extern int sprintf(char * , char const   *  , ...) ;
 3665#line 323
 3666extern int snprintf(char * , size_t  , char const   *  , ...) ;
 3667#line 24 "include/linux/list.h"
 3668__inline static void INIT_LIST_HEAD(struct list_head *list ) 
 3669{ unsigned long __cil_tmp2 ;
 3670  unsigned long __cil_tmp3 ;
 3671
 3672  {
 3673#line 26
 3674  *((struct list_head **)list) = list;
 3675#line 27
 3676  __cil_tmp2 = (unsigned long )list;
 3677#line 27
 3678  __cil_tmp3 = __cil_tmp2 + 8;
 3679#line 27
 3680  *((struct list_head **)__cil_tmp3) = list;
 3681#line 28
 3682  return;
 3683}
 3684}
 3685#line 47
 3686extern void __list_add(struct list_head * , struct list_head * , struct list_head * ) ;
 3687#line 60 "include/linux/list.h"
 3688__inline static void list_add(struct list_head *new , struct list_head *head ) 
 3689{ struct list_head *__cil_tmp3 ;
 3690
 3691  {
 3692  {
 3693#line 62
 3694  __cil_tmp3 = *((struct list_head **)head);
 3695#line 62
 3696  __list_add(new, head, __cil_tmp3);
 3697  }
 3698#line 63
 3699  return;
 3700}
 3701}
 3702#line 61 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/string_64.h"
 3703extern size_t strlen(char const   * ) ;
 3704#line 119 "include/linux/string.h"
 3705extern char *kstrdup(char const   * , gfp_t  ) ;
 3706#line 22 "include/linux/err.h"
 3707__inline static void *ERR_PTR(long error ) 
 3708{ 
 3709
 3710  {
 3711#line 24
 3712  return ((void *)error);
 3713}
 3714}
 3715#line 27 "include/linux/err.h"
 3716__inline static long PTR_ERR(void const   *ptr ) 
 3717{ 
 3718
 3719  {
 3720#line 29
 3721  return ((long )ptr);
 3722}
 3723}
 3724#line 32 "include/linux/err.h"
 3725__inline static long IS_ERR(void const   *ptr ) 
 3726{ long tmp ;
 3727  unsigned long __cil_tmp3 ;
 3728  int __cil_tmp4 ;
 3729  long __cil_tmp5 ;
 3730
 3731  {
 3732  {
 3733#line 34
 3734  __cil_tmp3 = (unsigned long )ptr;
 3735#line 34
 3736  __cil_tmp4 = __cil_tmp3 > 0xfffffffffffff000UL;
 3737#line 34
 3738  __cil_tmp5 = (long )__cil_tmp4;
 3739#line 34
 3740  tmp = __builtin_expect(__cil_tmp5, 0L);
 3741  }
 3742#line 34
 3743  return (tmp);
 3744}
 3745}
 3746#line 82 "include/linux/jiffies.h"
 3747extern unsigned long volatile   jiffies ;
 3748#line 26 "include/linux/export.h"
 3749extern struct module __this_module ;
 3750#line 161 "include/linux/slab.h"
 3751extern void kfree(void const   * ) ;
 3752#line 220 "include/linux/slub_def.h"
 3753extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t  ) ;
 3754#line 223
 3755void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
 3756#line 353 "include/linux/slab.h"
 3757__inline static void *kzalloc(size_t size , gfp_t flags ) ;
 3758#line 10 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p"
 3759extern void *__VERIFIER_nondet_pointer(void) ;
 3760#line 11
 3761void ldv_check_alloc_flags(gfp_t flags ) ;
 3762#line 12
 3763void ldv_check_alloc_nonatomic(void) ;
 3764#line 14
 3765struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
 3766#line 2402 "include/linux/fs.h"
 3767extern loff_t no_llseek(struct file * , loff_t  , int  ) ;
 3768#line 2403
 3769extern loff_t generic_file_llseek(struct file * , loff_t  , int  ) ;
 3770#line 2407
 3771extern int nonseekable_open(struct inode * , struct file * ) ;
 3772#line 2540
 3773extern ssize_t simple_read_from_buffer(void * , size_t  , loff_t * , void const   * ,
 3774                                       size_t  ) ;
 3775#line 2634 "include/linux/fs.h"
 3776__inline static void __simple_attr_check_format(char const   *fmt  , ...) 
 3777{ 
 3778
 3779  {
 3780#line 2636
 3781  return;
 3782}
 3783}
 3784#line 2639
 3785extern int simple_attr_open(struct inode * , struct file * , int (*)(void * , u64 * ) ,
 3786                            int (*)(void * , u64  ) , char const   * ) ;
 3787#line 2642
 3788extern int simple_attr_release(struct inode * , struct file * ) ;
 3789#line 2643
 3790extern ssize_t simple_attr_read(struct file * , char * , size_t  , loff_t * ) ;
 3791#line 2645
 3792extern ssize_t simple_attr_write(struct file * , char const   * , size_t  , loff_t * ) ;
 3793#line 49 "include/linux/debugfs.h"
 3794extern struct dentry *debugfs_create_file(char const   * , umode_t  , struct dentry * ,
 3795                                          void * , struct file_operations  const  * ) ;
 3796#line 53
 3797extern struct dentry *debugfs_create_dir(char const   * , struct dentry * ) ;
 3798#line 59
 3799extern void debugfs_remove_recursive(struct dentry * ) ;
 3800#line 76
 3801extern struct dentry *debugfs_create_x32(char const   * , umode_t  , struct dentry * ,
 3802                                         u32 * ) ;
 3803#line 19 "include/linux/hwmon.h"
 3804extern struct device *hwmon_device_register(struct device * ) ;
 3805#line 21
 3806extern void hwmon_device_unregister(struct device * ) ;
 3807#line 96 "include/linux/dmi.h"
 3808extern int dmi_check_system(struct dmi_system_id  const  * ) ;
 3809#line 134 "include/acpi/acpixf.h"
 3810extern char const   *acpi_format_exception(acpi_status  ) ;
 3811#line 212
 3812extern acpi_status acpi_get_handle(acpi_handle  , acpi_string  , acpi_handle ** ) ;
 3813#line 230
 3814extern acpi_status acpi_evaluate_object(acpi_handle  , acpi_string  , struct acpi_object_list * ,
 3815                                        struct acpi_buffer * ) ;
 3816#line 236
 3817extern acpi_status acpi_evaluate_object_typed(acpi_handle  , acpi_string  , struct acpi_object_list * ,
 3818                                              struct acpi_buffer * , acpi_object_type  ) ;
 3819#line 507 "include/linux/device.h"
 3820extern int device_create_file(struct device * , struct device_attribute  const  * ) ;
 3821#line 509
 3822extern void device_remove_file(struct device * , struct device_attribute  const  * ) ;
 3823#line 892
 3824extern int dev_err(struct device  const  * , char const   *  , ...) ;
 3825#line 894
 3826extern int dev_warn(struct device  const  * , char const   *  , ...) ;
 3827#line 898
 3828extern int _dev_info(struct device  const  * , char const   *  , ...) ;
 3829#line 45 "include/acpi/acpi_bus.h"
 3830extern acpi_status acpi_evaluate_integer(acpi_handle  , acpi_string  , struct acpi_object_list * ,
 3831                                         unsigned long long * ) ;
 3832#line 336
 3833extern int acpi_bus_register_driver(struct acpi_driver * ) ;
 3834#line 337
 3835extern void acpi_bus_unregister_driver(struct acpi_driver * ) ;
 3836#line 248 "include/linux/acpi.h"
 3837extern int acpi_resources_are_enforced(void) ;
 3838#line 41 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p"
 3839static bool new_if  ;
 3840#line 45 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p"
 3841static struct dmi_system_id  const  atk_force_new_if[2U]  = {      {(int (*)(struct dmi_system_id  const  * ))0, "Asus Sabertooth X58", {{(unsigned char)10,
 3842                                                                            {(char )'S',
 3843                                                                             (char )'A',
 3844                                                                             (char )'B',
 3845                                                                             (char )'E',
 3846                                                                             (char )'R',
 3847                                                                             (char )'T',
 3848                                                                             (char )'O',
 3849                                                                             (char )'O',
 3850                                                                             (char )'T',
 3851                                                                             (char )'H',
 3852                                                                             (char )' ',
 3853                                                                             (char )'X',
 3854                                                                             (char )'5',
 3855                                                                             (char )'8',
 3856                                                                             (char )'\000'}},
 3857                                                                           {(unsigned char)0,
 3858                                                                            {(char)0,
 3859                                                                             (char)0,
 3860                                                                             (char)0,
 3861                                                                             (char)0,
 3862                                                                             (char)0,
 3863                                                                             (char)0,
 3864                                                                             (char)0,
 3865                                                                             (char)0,
 3866                                                                             (char)0,
 3867                                                                             (char)0,
 3868                                                                             (char)0,
 3869                                                                             (char)0,
 3870                                                                             (char)0,
 3871                                                                             (char)0,
 3872                                                                             (char)0,
 3873                                                                             (char)0,
 3874                                                                             (char)0,
 3875                                                                             (char)0,
 3876                                                                             (char)0,
 3877                                                                             (char)0,
 3878                                                                             (char)0,
 3879                                                                             (char)0,
 3880                                                                             (char)0,
 3881                                                                             (char)0,
 3882                                                                             (char)0,
 3883                                                                             (char)0,
 3884                                                                             (char)0,
 3885                                                                             (char)0,
 3886                                                                             (char)0,
 3887                                                                             (char)0,
 3888                                                                             (char)0,
 3889                                                                             (char)0,
 3890                                                                             (char)0,
 3891                                                                             (char)0,
 3892                                                                             (char)0,
 3893                                                                             (char)0,
 3894                                                                             (char)0,
 3895                                                                             (char)0,
 3896                                                                             (char)0,
 3897                                                                             (char)0,
 3898                                                                             (char)0,
 3899                                                                             (char)0,
 3900                                                                             (char)0,
 3901                                                                             (char)0,
 3902                                                                             (char)0,
 3903                                                                             (char)0,
 3904                                                                             (char)0,
 3905                                                                             (char)0,
 3906                                                                             (char)0,
 3907                                                                             (char)0,
 3908                                                                             (char)0,
 3909                                                                             (char)0,
 3910                                                                             (char)0,
 3911                                                                             (char)0,
 3912                                                                             (char)0,
 3913                                                                             (char)0,
 3914                                                                             (char)0,
 3915                                                                             (char)0,
 3916                                                                             (char)0,
 3917                                                                             (char)0,
 3918                                                                             (char)0,
 3919                                                                             (char)0,
 3920                                                                             (char)0,
 3921                                                                             (char)0,
 3922                                                                             (char)0,
 3923                                                                             (char)0,
 3924                                                                             (char)0,
 3925                                                                             (char)0,
 3926                                                                             (char)0,
 3927                                                                             (char)0,
 3928                                                                             (char)0,
 3929                                                                             (char)0,
 3930                                                                             (char)0,
 3931                                                                             (char)0,
 3932                                                                             (char)0,
 3933                                                                             (char)0,
 3934                                                                             (char)0,
 3935                                                                             (char)0,
 3936                                                                             (char)0}},
 3937                                                                           {(unsigned char)0,
 3938                                                                            {(char)0,
 3939                                                                             (char)0,
 3940                                                                             (char)0,
 3941                                                                             (char)0,
 3942                                                                             (char)0,
 3943                                                                             (char)0,
 3944                                                                             (char)0,
 3945                                                                             (char)0,
 3946                                                                             (char)0,
 3947                                                                             (char)0,
 3948                                                                             (char)0,
 3949                                                                             (char)0,
 3950                                                                             (char)0,
 3951                                                                             (char)0,
 3952                                                                             (char)0,
 3953                                                                             (char)0,
 3954                                                                             (char)0,
 3955                                                                             (char)0,
 3956                                                                             (char)0,
 3957                                                                             (char)0,
 3958                                                                             (char)0,
 3959                                                                             (char)0,
 3960                                                                             (char)0,
 3961                                                                             (char)0,
 3962                                                                             (char)0,
 3963                                                                             (char)0,
 3964                                                                             (char)0,
 3965                                                                             (char)0,
 3966                                                                             (char)0,
 3967                                                                             (char)0,
 3968                                                                             (char)0,
 3969                                                                             (char)0,
 3970                                                                             (char)0,
 3971                                                                             (char)0,
 3972                                                                             (char)0,
 3973                                                                             (char)0,
 3974                                                                             (char)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                                                                             (char)0,
 3992                                                                             (char)0,
 3993                                                                             (char)0,
 3994                                                                             (char)0,
 3995                                                                             (char)0,
 3996                                                                             (char)0,
 3997                                                                             (char)0,
 3998                                                                             (char)0,
 3999                                                                             (char)0,
 4000                                                                             (char)0,
 4001                                                                             (char)0,
 4002                                                                             (char)0,
 4003                                                                             (char)0,
 4004                                                                             (char)0,
 4005                                                                             (char)0,
 4006                                                                             (char)0,
 4007                                                                             (char)0,
 4008                                                                             (char)0,
 4009                                                                             (char)0,
 4010                                                                             (char)0,
 4011                                                                             (char)0,
 4012                                                                             (char)0,
 4013                                                                             (char)0,
 4014                                                                             (char)0,
 4015                                                                             (char)0,
 4016                                                                             (char)0}},
 4017                                                                           {(unsigned char)0,
 4018                                                                            {(char)0,
 4019                                                                             (char)0,
 4020                                                                             (char)0,
 4021                                                                             (char)0,
 4022                                                                             (char)0,
 4023                                                                             (char)0,
 4024                                                                             (char)0,
 4025                                                                             (char)0,
 4026                                                                             (char)0,
 4027                                                                             (char)0,
 4028                                                                             (char)0,
 4029                                                                             (char)0,
 4030                                                                             (char)0,
 4031                                                                             (char)0,
 4032                                                                             (char)0,
 4033                                                                             (char)0,
 4034                                                                             (char)0,
 4035                                                                             (char)0,
 4036                                                                             (char)0,
 4037                                                                             (char)0,
 4038                                                                             (char)0,
 4039                                                                             (char)0,
 4040                                                                             (char)0,
 4041                                                                             (char)0,
 4042                                                                             (char)0,
 4043                                                                             (char)0,
 4044                                                                             (char)0,
 4045                                                                             (char)0,
 4046                                                                             (char)0,
 4047                                                                             (char)0,
 4048                                                                             (char)0,
 4049                                                                             (char)0,
 4050                                                                             (char)0,
 4051                                                                             (char)0,
 4052                                                                             (char)0,
 4053                                                                             (char)0,
 4054                                                                             (char)0,
 4055                                                                             (char)0,
 4056                                                                             (char)0,
 4057                                                                             (char)0,
 4058                                                                             (char)0,
 4059                                                                             (char)0,
 4060                                                                             (char)0,
 4061                                                                             (char)0,
 4062                                                                             (char)0,
 4063                                                                             (char)0,
 4064                                                                             (char)0,
 4065                                                                             (char)0,
 4066                                                                             (char)0,
 4067                                                                             (char)0,
 4068                                                                             (char)0,
 4069                                                                             (char)0,
 4070                                                                             (char)0,
 4071                                                                             (char)0,
 4072                                                                             (char)0,
 4073                                                                             (char)0,
 4074                                                                             (char)0,
 4075                                                                             (char)0,
 4076                                                                             (char)0,
 4077                                                                             (char)0,
 4078                                                                             (char)0,
 4079                                                                             (char)0,
 4080                                                                             (char)0,
 4081                                                                             (char)0,
 4082                                                                             (char)0,
 4083                                                                             (char)0,
 4084                                                                             (char)0,
 4085                                                                             (char)0,
 4086                                                                             (char)0,
 4087                                                                             (char)0,
 4088                                                                             (char)0,
 4089                                                                             (char)0,
 4090                                                                             (char)0,
 4091                                                                             (char)0,
 4092                                                                             (char)0,
 4093                                                                             (char)0,
 4094                                                                             (char)0,
 4095                                                                             (char)0,
 4096                                                                             (char)0}}},
 4097      (void *)0}, 
 4098        {(int (*)(struct dmi_system_id  const  * ))0, (char const   *)0, {{(unsigned char)0,
 4099                                                                        {(char)0,
 4100                                                                         (char)0,
 4101                                                                         (char)0,
 4102                                                                         (char)0,
 4103                                                                         (char)0,
 4104                                                                         (char)0,
 4105                                                                         (char)0,
 4106                                                                         (char)0,
 4107                                                                         (char)0,
 4108                                                                         (char)0,
 4109                                                                         (char)0,
 4110                                                                         (char)0,
 4111                                                                         (char)0,
 4112                                                                         (char)0,
 4113                                                                         (char)0,
 4114                                                                         (char)0,
 4115                                                                         (char)0,
 4116                                                                         (char)0,
 4117                                                                         (char)0,
 4118                                                                         (char)0,
 4119                                                                         (char)0,
 4120                                                                         (char)0,
 4121                                                                         (char)0,
 4122                                                                         (char)0,
 4123                                                                         (char)0,
 4124                                                                         (char)0,
 4125                                                                         (char)0,
 4126                                                                         (char)0,
 4127                                                                         (char)0,
 4128                                                                         (char)0,
 4129                                                                         (char)0,
 4130                                                                         (char)0,
 4131                                                                         (char)0,
 4132                                                                         (char)0,
 4133                                                                         (char)0,
 4134                                                                         (char)0,
 4135                                                                         (char)0,
 4136                                                                         (char)0,
 4137                                                                         (char)0,
 4138                                                                         (char)0,
 4139                                                                         (char)0,
 4140                                                                         (char)0,
 4141                                                                         (char)0,
 4142                                                                         (char)0,
 4143                                                                         (char)0,
 4144                                                                         (char)0,
 4145                                                                         (char)0,
 4146                                                                         (char)0,
 4147                                                                         (char)0,
 4148                                                                         (char)0,
 4149                                                                         (char)0,
 4150                                                                         (char)0,
 4151                                                                         (char)0,
 4152                                                                         (char)0,
 4153                                                                         (char)0,
 4154                                                                         (char)0,
 4155                                                                         (char)0,
 4156                                                                         (char)0,
 4157                                                                         (char)0,
 4158                                                                         (char)0,
 4159                                                                         (char)0,
 4160                                                                         (char)0,
 4161                                                                         (char)0,
 4162                                                                         (char)0,
 4163                                                                         (char)0,
 4164                                                                         (char)0,
 4165                                                                         (char)0,
 4166                                                                         (char)0,
 4167                                                                         (char)0,
 4168                                                                         (char)0,
 4169                                                                         (char)0,
 4170                                                                         (char)0,
 4171                                                                         (char)0,
 4172                                                                         (char)0,
 4173                                                                         (char)0,
 4174                                                                         (char)0,
 4175                                                                         (char)0,
 4176                                                                         (char)0,
 4177                                                                         (char)0}},
 4178                                                                       {(unsigned char)0,
 4179                                                                        {(char)0,
 4180                                                                         (char)0,
 4181                                                                         (char)0,
 4182                                                                         (char)0,
 4183                                                                         (char)0,
 4184                                                                         (char)0,
 4185                                                                         (char)0,
 4186                                                                         (char)0,
 4187                                                                         (char)0,
 4188                                                                         (char)0,
 4189                                                                         (char)0,
 4190                                                                         (char)0,
 4191                                                                         (char)0,
 4192                                                                         (char)0,
 4193                                                                         (char)0,
 4194                                                                         (char)0,
 4195                                                                         (char)0,
 4196                                                                         (char)0,
 4197                                                                         (char)0,
 4198                                                                         (char)0,
 4199                                                                         (char)0,
 4200                                                                         (char)0,
 4201                                                                         (char)0,
 4202                                                                         (char)0,
 4203                                                                         (char)0,
 4204                                                                         (char)0,
 4205                                                                         (char)0,
 4206                                                                         (char)0,
 4207                                                                         (char)0,
 4208                                                                         (char)0,
 4209                                                                         (char)0,
 4210                                                                         (char)0,
 4211                                                                         (char)0,
 4212                                                                         (char)0,
 4213                                                                         (char)0,
 4214                                                                         (char)0,
 4215                                                                         (char)0,
 4216                                                                         (char)0,
 4217                                                                         (char)0,
 4218                                                                         (char)0,
 4219                                                                         (char)0,
 4220                                                                         (char)0,
 4221                                                                         (char)0,
 4222                                                                         (char)0,
 4223                                                                         (char)0,
 4224                                                                         (char)0,
 4225                                                                         (char)0,
 4226                                                                         (char)0,
 4227                                                                         (char)0,
 4228                                                                         (char)0,
 4229                                                                         (char)0,
 4230                                                                         (char)0,
 4231                                                                         (char)0,
 4232                                                                         (char)0,
 4233                                                                         (char)0,
 4234                                                                         (char)0,
 4235                                                                         (char)0,
 4236                                                                         (char)0,
 4237                                                                         (char)0,
 4238                                                                         (char)0,
 4239                                                                         (char)0,
 4240                                                                         (char)0,
 4241                                                                         (char)0,
 4242                                                                         (char)0,
 4243                                                                         (char)0,
 4244                                                                         (char)0,
 4245                                                                         (char)0,
 4246                                                                         (char)0,
 4247                                                                         (char)0,
 4248                                                                         (char)0,
 4249                                                                         (char)0,
 4250                                                                         (char)0,
 4251                                                                         (char)0,
 4252                                                                         (char)0,
 4253                                                                         (char)0,
 4254                                                                         (char)0,
 4255                                                                         (char)0,
 4256                                                                         (char)0,
 4257                                                                         (char)0}},
 4258                                                                       {(unsigned char)0,
 4259                                                                        {(char)0,
 4260                                                                         (char)0,
 4261                                                                         (char)0,
 4262                                                                         (char)0,
 4263                                                                         (char)0,
 4264                                                                         (char)0,
 4265                                                                         (char)0,
 4266                                                                         (char)0,
 4267                                                                         (char)0,
 4268                                                                         (char)0,
 4269                                                                         (char)0,
 4270                                                                         (char)0,
 4271                                                                         (char)0,
 4272                                                                         (char)0,
 4273                                                                         (char)0,
 4274                                                                         (char)0,
 4275                                                                         (char)0,
 4276                                                                         (char)0,
 4277                                                                         (char)0,
 4278                                                                         (char)0,
 4279                                                                         (char)0,
 4280                                                                         (char)0,
 4281                                                                         (char)0,
 4282                                                                         (char)0,
 4283                                                                         (char)0,
 4284                                                                         (char)0,
 4285                                                                         (char)0,
 4286                                                                         (char)0,
 4287                                                                         (char)0,
 4288                                                                         (char)0,
 4289                                                                         (char)0,
 4290                                                                         (char)0,
 4291                                                                         (char)0,
 4292                                                                         (char)0,
 4293                                                                         (char)0,
 4294                                                                         (char)0,
 4295                                                                         (char)0,
 4296                                                                         (char)0,
 4297                                                                         (char)0,
 4298                                                                         (char)0,
 4299                                                                         (char)0,
 4300                                                                         (char)0,
 4301                                                                         (char)0,
 4302                                                                         (char)0,
 4303                                                                         (char)0,
 4304                                                                         (char)0,
 4305                                                                         (char)0,
 4306                                                                         (char)0,
 4307                                                                         (char)0,
 4308                                                                         (char)0,
 4309                                                                         (char)0,
 4310                                                                         (char)0,
 4311                                                                         (char)0,
 4312                                                                         (char)0,
 4313                                                                         (char)0,
 4314                                                                         (char)0,
 4315                                                                         (char)0,
 4316                                                                         (char)0,
 4317                                                                         (char)0,
 4318                                                                         (char)0,
 4319                                                                         (char)0,
 4320                                                                         (char)0,
 4321                                                                         (char)0,
 4322                                                                         (char)0,
 4323                                                                         (char)0,
 4324                                                                         (char)0,
 4325                                                                         (char)0,
 4326                                                                         (char)0,
 4327                                                                         (char)0,
 4328                                                                         (char)0,
 4329                                                                         (char)0,
 4330                                                                         (char)0,
 4331                                                                         (char)0,
 4332                                                                         (char)0,
 4333                                                                         (char)0,
 4334                                                                         (char)0,
 4335                                                                         (char)0,
 4336                                                                         (char)0,
 4337                                                                         (char)0}},
 4338                                                                       {(unsigned char)0,
 4339                                                                        {(char)0,
 4340                                                                         (char)0,
 4341                                                                         (char)0,
 4342                                                                         (char)0,
 4343                                                                         (char)0,
 4344                                                                         (char)0,
 4345                                                                         (char)0,
 4346                                                                         (char)0,
 4347                                                                         (char)0,
 4348                                                                         (char)0,
 4349                                                                         (char)0,
 4350                                                                         (char)0,
 4351                                                                         (char)0,
 4352                                                                         (char)0,
 4353                                                                         (char)0,
 4354                                                                         (char)0,
 4355                                                                         (char)0,
 4356                                                                         (char)0,
 4357                                                                         (char)0,
 4358                                                                         (char)0,
 4359                                                                         (char)0,
 4360                                                                         (char)0,
 4361                                                                         (char)0,
 4362                                                                         (char)0,
 4363                                                                         (char)0,
 4364                                                                         (char)0,
 4365                                                                         (char)0,
 4366                                                                         (char)0,
 4367                                                                         (char)0,
 4368                                                                         (char)0,
 4369                                                                         (char)0,
 4370                                                                         (char)0,
 4371                                                                         (char)0,
 4372                                                                         (char)0,
 4373                                                                         (char)0,
 4374                                                                         (char)0,
 4375                                                                         (char)0,
 4376                                                                         (char)0,
 4377                                                                         (char)0,
 4378                                                                         (char)0,
 4379                                                                         (char)0,
 4380                                                                         (char)0,
 4381                                                                         (char)0,
 4382                                                                         (char)0,
 4383                                                                         (char)0,
 4384                                                                         (char)0,
 4385                                                                         (char)0,
 4386                                                                         (char)0,
 4387                                                                         (char)0,
 4388                                                                         (char)0,
 4389                                                                         (char)0,
 4390                                                                         (char)0,
 4391                                                                         (char)0,
 4392                                                                         (char)0,
 4393                                                                         (char)0,
 4394                                                                         (char)0,
 4395                                                                         (char)0,
 4396                                                                         (char)0,
 4397                                                                         (char)0,
 4398                                                                         (char)0,
 4399                                                                         (char)0,
 4400                                                                         (char)0,
 4401                                                                         (char)0,
 4402                                                                         (char)0,
 4403                                                                         (char)0,
 4404                                                                         (char)0,
 4405                                                                         (char)0,
 4406                                                                         (char)0,
 4407                                                                         (char)0,
 4408                                                                         (char)0,
 4409                                                                         (char)0,
 4410                                                                         (char)0,
 4411                                                                         (char)0,
 4412                                                                         (char)0,
 4413                                                                         (char)0,
 4414                                                                         (char)0,
 4415                                                                         (char)0,
 4416                                                                         (char)0,
 4417                                                                         (char)0}}},
 4418      (void *)0}};
 4419#line 151 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p"
 4420static struct acpi_device_id  const  atk_ids[2U]  = {      {{(__u8 )'A', (__u8 )'T', (__u8 )'K', (__u8 )'0', (__u8 )'1', (__u8 )'1', (__u8 )'0',
 4421       (__u8 )'\000', (unsigned char)0, (unsigned char)0, (unsigned char)0, (unsigned char)0,
 4422       (unsigned char)0, (unsigned char)0, (unsigned char)0, (unsigned char)0}, 0UL}, 
 4423        {{(__u8 )'\000',
 4424       (unsigned char)0, (unsigned char)0, (unsigned char)0, (unsigned char)0, (unsigned char)0,
 4425       (unsigned char)0, (unsigned char)0, (unsigned char)0, (unsigned char)0, (unsigned char)0,
 4426       (unsigned char)0, (unsigned char)0, (unsigned char)0, (unsigned char)0, (unsigned char)0},
 4427      0UL}};
 4428#line 155 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p"
 4429struct acpi_device_id  const  __mod_acpi_device_table  ;
 4430#line 199
 4431static int atk_add(struct acpi_device *device ) ;
 4432#line 200
 4433static int atk_remove(struct acpi_device *device , int type ) ;
 4434#line 201
 4435static void atk_print_sensor(struct atk_data *data , union acpi_object *obj ) ;
 4436#line 202
 4437static int atk_read_value(struct atk_sensor_data *sensor , u64 *value ) ;
 4438#line 203
 4439static void atk_free_sensors(struct atk_data *data ) ;
 4440#line 205 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p"
 4441static struct acpi_driver atk_driver  =    {{(char )'A', (char )'T', (char )'K', (char )'0', (char )'1', (char )'1', (char )'0',
 4442     (char )'\000'}, {(char )'h', (char )'w', (char )'m', (char )'o', (char )'n',
 4443                      (char )'\000'}, (struct acpi_device_id  const  *)(& atk_ids),
 4444    0U, {& atk_add, & atk_remove, (int (*)(struct acpi_device * ))0, (int (*)(struct acpi_device * ,
 4445                                                                              pm_message_t  ))0,
 4446         (int (*)(struct acpi_device * ))0, (int (*)(struct acpi_device * ))0, (int (*)(struct acpi_device * ))0,
 4447         (void (*)(struct acpi_device * , u32  ))0}, {(char const   *)0, (struct bus_type *)0,
 4448                                                      (struct module *)0, (char const   *)0,
 4449                                                      (_Bool)0, (struct of_device_id  const  *)0,
 4450                                                      (int (*)(struct device * ))0,
 4451                                                      (int (*)(struct device * ))0,
 4452                                                      (void (*)(struct device * ))0,
 4453                                                      (int (*)(struct device * , pm_message_t  ))0,
 4454                                                      (int (*)(struct device * ))0,
 4455                                                      (struct attribute_group  const  **)0,
 4456                                                      (struct dev_pm_ops  const  *)0,
 4457                                                      (struct driver_private *)0},
 4458    (struct module *)0};
 4459#line 227 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p"
 4460static ssize_t atk_input_show(struct device *dev , struct device_attribute *attr ,
 4461                              char *buf ) 
 4462{ struct atk_sensor_data *s ;
 4463  struct device_attribute  const  *__mptr ;
 4464  u64 value ;
 4465  int err ;
 4466  int tmp ;
 4467  struct atk_sensor_data *__cil_tmp9 ;
 4468  unsigned long __cil_tmp10 ;
 4469  unsigned long __cil_tmp11 ;
 4470  u64 __cil_tmp12 ;
 4471  u64 *__cil_tmp13 ;
 4472  u64 *__cil_tmp14 ;
 4473  u64 __cil_tmp15 ;
 4474  u64 *__cil_tmp16 ;
 4475  u64 __cil_tmp17 ;
 4476
 4477  {
 4478  {
 4479#line 230
 4480  __mptr = (struct device_attribute  const  *)attr;
 4481#line 230
 4482  __cil_tmp9 = (struct atk_sensor_data *)__mptr;
 4483#line 230
 4484  s = __cil_tmp9 + 0xffffffffffffffb8UL;
 4485#line 234
 4486  err = atk_read_value(s, & value);
 4487  }
 4488#line 235
 4489  if (err != 0) {
 4490#line 236
 4491    return ((ssize_t )err);
 4492  } else {
 4493
 4494  }
 4495  {
 4496#line 238
 4497  __cil_tmp10 = (unsigned long )s;
 4498#line 238
 4499  __cil_tmp11 = __cil_tmp10 + 288;
 4500#line 238
 4501  __cil_tmp12 = *((u64 *)__cil_tmp11);
 4502#line 238
 4503  if (__cil_tmp12 == 196608ULL) {
 4504#line 240
 4505    __cil_tmp13 = & value;
 4506#line 240
 4507    __cil_tmp14 = & value;
 4508#line 240
 4509    __cil_tmp15 = *__cil_tmp14;
 4510#line 240
 4511    *__cil_tmp13 = __cil_tmp15 * 100ULL;
 4512  } else {
 4513
 4514  }
 4515  }
 4516  {
 4517#line 242
 4518  __cil_tmp16 = & value;
 4519#line 242
 4520  __cil_tmp17 = *__cil_tmp16;
 4521#line 242
 4522  tmp = sprintf(buf, "%llu\n", __cil_tmp17);
 4523  }
 4524#line 242
 4525  return ((ssize_t )tmp);
 4526}
 4527}
 4528#line 245 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p"
 4529static ssize_t atk_label_show(struct device *dev , struct device_attribute *attr ,
 4530                              char *buf ) 
 4531{ struct atk_sensor_data *s ;
 4532  struct device_attribute  const  *__mptr ;
 4533  int tmp ;
 4534  struct atk_sensor_data *__cil_tmp7 ;
 4535  unsigned long __cil_tmp8 ;
 4536  unsigned long __cil_tmp9 ;
 4537  char const   *__cil_tmp10 ;
 4538
 4539  {
 4540  {
 4541#line 248
 4542  __mptr = (struct device_attribute  const  *)attr;
 4543#line 248
 4544  __cil_tmp7 = (struct atk_sensor_data *)__mptr;
 4545#line 248
 4546  s = __cil_tmp7 + 0xffffffffffffffe8UL;
 4547#line 250
 4548  __cil_tmp8 = (unsigned long )s;
 4549#line 250
 4550  __cil_tmp9 = __cil_tmp8 + 336;
 4551#line 250
 4552  __cil_tmp10 = *((char const   **)__cil_tmp9);
 4553#line 250
 4554  tmp = sprintf(buf, "%s\n", __cil_tmp10);
 4555  }
 4556#line 250
 4557  return ((ssize_t )tmp);
 4558}
 4559}
 4560#line 253 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p"
 4561static ssize_t atk_limit1_show(struct device *dev , struct device_attribute *attr ,
 4562                               char *buf ) 
 4563{ struct atk_sensor_data *s ;
 4564  struct device_attribute  const  *__mptr ;
 4565  u64 value ;
 4566  int tmp ;
 4567  struct atk_sensor_data *__cil_tmp8 ;
 4568  unsigned long __cil_tmp9 ;
 4569  unsigned long __cil_tmp10 ;
 4570  unsigned long __cil_tmp11 ;
 4571  unsigned long __cil_tmp12 ;
 4572  u64 __cil_tmp13 ;
 4573
 4574  {
 4575#line 256
 4576  __mptr = (struct device_attribute  const  *)attr;
 4577#line 256
 4578  __cil_tmp8 = (struct atk_sensor_data *)__mptr;
 4579#line 256
 4580  s = __cil_tmp8 + 0xffffffffffffff88UL;
 4581#line 257
 4582  __cil_tmp9 = (unsigned long )s;
 4583#line 257
 4584  __cil_tmp10 = __cil_tmp9 + 296;
 4585#line 257
 4586  value = *((u64 *)__cil_tmp10);
 4587  {
 4588#line 259
 4589  __cil_tmp11 = (unsigned long )s;
 4590#line 259
 4591  __cil_tmp12 = __cil_tmp11 + 288;
 4592#line 259
 4593  __cil_tmp13 = *((u64 *)__cil_tmp12);
 4594#line 259
 4595  if (__cil_tmp13 == 196608ULL) {
 4596#line 260
 4597    value = value * 100ULL;
 4598  } else {
 4599
 4600  }
 4601  }
 4602  {
 4603#line 262
 4604  tmp = sprintf(buf, "%lld\n", value);
 4605  }
 4606#line 262
 4607  return ((ssize_t )tmp);
 4608}
 4609}
 4610#line 265 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p"
 4611static ssize_t atk_limit2_show(struct device *dev , struct device_attribute *attr ,
 4612                               char *buf ) 
 4613{ struct atk_sensor_data *s ;
 4614  struct device_attribute  const  *__mptr ;
 4615  u64 value ;
 4616  int tmp ;
 4617  struct atk_sensor_data *__cil_tmp8 ;
 4618  unsigned long __cil_tmp9 ;
 4619  unsigned long __cil_tmp10 ;
 4620  unsigned long __cil_tmp11 ;
 4621  unsigned long __cil_tmp12 ;
 4622  u64 __cil_tmp13 ;
 4623
 4624  {
 4625#line 268
 4626  __mptr = (struct device_attribute  const  *)attr;
 4627#line 268
 4628  __cil_tmp8 = (struct atk_sensor_data *)__mptr;
 4629#line 268
 4630  s = __cil_tmp8 + 0xffffffffffffff58UL;
 4631#line 269
 4632  __cil_tmp9 = (unsigned long )s;
 4633#line 269
 4634  __cil_tmp10 = __cil_tmp9 + 304;
 4635#line 269
 4636  value = *((u64 *)__cil_tmp10);
 4637  {
 4638#line 271
 4639  __cil_tmp11 = (unsigned long )s;
 4640#line 271
 4641  __cil_tmp12 = __cil_tmp11 + 288;
 4642#line 271
 4643  __cil_tmp13 = *((u64 *)__cil_tmp12);
 4644#line 271
 4645  if (__cil_tmp13 == 196608ULL) {
 4646#line 272
 4647    value = value * 100ULL;
 4648  } else {
 4649
 4650  }
 4651  }
 4652  {
 4653#line 274
 4654  tmp = sprintf(buf, "%lld\n", value);
 4655  }
 4656#line 274
 4657  return ((ssize_t )tmp);
 4658}
 4659}
 4660#line 277 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p"
 4661static ssize_t atk_name_show(struct device *dev , struct device_attribute *attr ,
 4662                             char *buf ) 
 4663{ int tmp ;
 4664
 4665  {
 4666  {
 4667#line 280
 4668  tmp = sprintf(buf, "atk0110\n");
 4669  }
 4670#line 280
 4671  return ((ssize_t )tmp);
 4672}
 4673}
 4674#line 282 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p"
 4675static struct device_attribute atk_name_attr  =    {{"name", (umode_t )292U, (struct lock_class_key *)0, {{{(char)0}, {(char)0}, {(char)0},
 4676                                                           {(char)0}, {(char)0}, {(char)0},
 4677                                                           {(char)0}, {(char)0}}}},
 4678    & atk_name_show, (ssize_t (*)(struct device * , struct device_attribute * , char const   * ,
 4679                                  size_t  ))0};
 4680#line 285 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p"
 4681static void atk_init_attribute(struct device_attribute *attr , char *name , ssize_t (*show)(struct device * ,
 4682                                                                                            struct device_attribute * ,
 4683                                                                                            char * ) ) 
 4684{ struct lock_class_key __key ;
 4685  unsigned long __cil_tmp5 ;
 4686  unsigned long __cil_tmp6 ;
 4687  unsigned long __cil_tmp7 ;
 4688  unsigned long __cil_tmp8 ;
 4689  unsigned long __cil_tmp9 ;
 4690  unsigned long __cil_tmp10 ;
 4691  unsigned long __cil_tmp11 ;
 4692  unsigned long __cil_tmp12 ;
 4693  unsigned long __cil_tmp13 ;
 4694  unsigned long __cil_tmp14 ;
 4695
 4696  {
 4697#line 288
 4698  __cil_tmp5 = 0 + 16;
 4699#line 288
 4700  __cil_tmp6 = (unsigned long )attr;
 4701#line 288
 4702  __cil_tmp7 = __cil_tmp6 + __cil_tmp5;
 4703#line 288
 4704  *((struct lock_class_key **)__cil_tmp7) = & __key;
 4705#line 289
 4706  *((char const   **)attr) = (char const   *)name;
 4707#line 290
 4708  __cil_tmp8 = 0 + 8;
 4709#line 290
 4710  __cil_tmp9 = (unsigned long )attr;
 4711#line 290
 4712  __cil_tmp10 = __cil_tmp9 + __cil_tmp8;
 4713#line 290
 4714  *((umode_t *)__cil_tmp10) = (umode_t )292U;
 4715#line 291
 4716  __cil_tmp11 = (unsigned long )attr;
 4717#line 291
 4718  __cil_tmp12 = __cil_tmp11 + 32;
 4719#line 291
 4720  *((ssize_t (**)(struct device * , struct device_attribute * , char * ))__cil_tmp12) = show;
 4721#line 292
 4722  __cil_tmp13 = (unsigned long )attr;
 4723#line 292
 4724  __cil_tmp14 = __cil_tmp13 + 40;
 4725#line 292
 4726  *((ssize_t (**)(struct device * , struct device_attribute * , char const   * , size_t  ))__cil_tmp14) = (ssize_t (*)(struct device * ,
 4727                                                                                                                       struct device_attribute * ,
 4728                                                                                                                       char const   * ,
 4729                                                                                                                       size_t  ))0;
 4730#line 293
 4731  return;
 4732}
 4733}
 4734#line 296 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p"
 4735static union acpi_object *atk_get_pack_member(struct atk_data *data , union acpi_object *pack ,
 4736                                              enum atk_pack_member m ) 
 4737{ bool old_if ;
 4738  int offset ;
 4739  unsigned long __cil_tmp6 ;
 4740  unsigned long __cil_tmp7 ;
 4741  unsigned int __cil_tmp8 ;
 4742  unsigned long __cil_tmp9 ;
 4743  unsigned long __cil_tmp10 ;
 4744  unsigned long __cil_tmp11 ;
 4745  unsigned long __cil_tmp12 ;
 4746  union acpi_object *__cil_tmp13 ;
 4747
 4748  {
 4749#line 300
 4750  __cil_tmp6 = (unsigned long )data;
 4751#line 300
 4752  __cil_tmp7 = __cil_tmp6 + 24;
 4753#line 300
 4754  old_if = *((bool *)__cil_tmp7);
 4755  {
 4756#line 303
 4757  __cil_tmp8 = (unsigned int )m;
 4758#line 304
 4759  if ((int )__cil_tmp8 == 0) {
 4760#line 304
 4761    goto case_0;
 4762  } else
 4763#line 307
 4764  if ((int )__cil_tmp8 == 1) {
 4765#line 307
 4766    goto case_1;
 4767  } else
 4768#line 310
 4769  if ((int )__cil_tmp8 == 2) {
 4770#line 310
 4771    goto case_2;
 4772  } else
 4773#line 314
 4774  if ((int )__cil_tmp8 == 3) {
 4775#line 314
 4776    goto case_3;
 4777  } else
 4778#line 318
 4779  if ((int )__cil_tmp8 == 4) {
 4780#line 318
 4781    goto case_4;
 4782  } else {
 4783    {
 4784#line 322
 4785    goto switch_default;
 4786#line 303
 4787    if (0) {
 4788      case_0: /* CIL Label */ 
 4789#line 305
 4790      offset = 0;
 4791#line 306
 4792      goto ldv_25001;
 4793      case_1: /* CIL Label */ 
 4794#line 308
 4795      offset = 1;
 4796#line 309
 4797      goto ldv_25001;
 4798      case_2: /* CIL Label */ ;
 4799#line 311
 4800      if ((int )old_if) {
 4801#line 311
 4802        offset = 2;
 4803      } else {
 4804#line 311
 4805        offset = 4;
 4806      }
 4807#line 313
 4808      goto ldv_25001;
 4809      case_3: /* CIL Label */ ;
 4810#line 315
 4811      if ((int )old_if) {
 4812#line 315
 4813        offset = 3;
 4814      } else {
 4815#line 315
 4816        offset = 5;
 4817      }
 4818#line 317
 4819      goto ldv_25001;
 4820      case_4: /* CIL Label */ ;
 4821#line 319
 4822      if ((int )old_if) {
 4823#line 319
 4824        offset = 4;
 4825      } else {
 4826#line 319
 4827        offset = 6;
 4828      }
 4829#line 321
 4830      goto ldv_25001;
 4831      switch_default: /* CIL Label */ ;
 4832#line 323
 4833      return ((union acpi_object *)0);
 4834    } else {
 4835      switch_break: /* CIL Label */ ;
 4836    }
 4837    }
 4838  }
 4839  }
 4840  ldv_25001: ;
 4841  {
 4842#line 326
 4843  __cil_tmp9 = (unsigned long )offset;
 4844#line 326
 4845  __cil_tmp10 = 0 + 8;
 4846#line 326
 4847  __cil_tmp11 = (unsigned long )pack;
 4848#line 326
 4849  __cil_tmp12 = __cil_tmp11 + __cil_tmp10;
 4850#line 326
 4851  __cil_tmp13 = *((union acpi_object **)__cil_tmp12);
 4852#line 326
 4853  return (__cil_tmp13 + __cil_tmp9);
 4854  }
 4855}
 4856}
 4857#line 346 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p"
 4858static int validate_hwmon_pack(struct atk_data *data , union acpi_object *obj ) 
 4859{ struct device *dev ;
 4860  union acpi_object *tmp ;
 4861  bool old_if ;
 4862  int expected_size ;
 4863  int tmp___0 ;
 4864  unsigned long __cil_tmp8 ;
 4865  unsigned long __cil_tmp9 ;
 4866  struct acpi_device *__cil_tmp10 ;
 4867  unsigned long __cil_tmp11 ;
 4868  unsigned long __cil_tmp12 ;
 4869  unsigned long __cil_tmp13 ;
 4870  unsigned long __cil_tmp14 ;
 4871  acpi_object_type __cil_tmp15 ;
 4872  struct device  const  *__cil_tmp16 ;
 4873  acpi_object_type __cil_tmp17 ;
 4874  u32 __cil_tmp18 ;
 4875  unsigned long __cil_tmp19 ;
 4876  unsigned long __cil_tmp20 ;
 4877  unsigned long __cil_tmp21 ;
 4878  u32 __cil_tmp22 ;
 4879  struct device  const  *__cil_tmp23 ;
 4880  unsigned long __cil_tmp24 ;
 4881  unsigned long __cil_tmp25 ;
 4882  unsigned long __cil_tmp26 ;
 4883  u32 __cil_tmp27 ;
 4884  enum atk_pack_member __cil_tmp28 ;
 4885  acpi_object_type __cil_tmp29 ;
 4886  struct device  const  *__cil_tmp30 ;
 4887  acpi_object_type __cil_tmp31 ;
 4888  enum atk_pack_member __cil_tmp32 ;
 4889  acpi_object_type __cil_tmp33 ;
 4890  struct device  const  *__cil_tmp34 ;
 4891  acpi_object_type __cil_tmp35 ;
 4892  enum atk_pack_member __cil_tmp36 ;
 4893  acpi_object_type __cil_tmp37 ;
 4894  struct device  const  *__cil_tmp38 ;
 4895  acpi_object_type __cil_tmp39 ;
 4896  enum atk_pack_member __cil_tmp40 ;
 4897  acpi_object_type __cil_tmp41 ;
 4898  struct device  const  *__cil_tmp42 ;
 4899  acpi_object_type __cil_tmp43 ;
 4900  enum atk_pack_member __cil_tmp44 ;
 4901  acpi_object_type __cil_tmp45 ;
 4902  struct device  const  *__cil_tmp46 ;
 4903  acpi_object_type __cil_tmp47 ;
 4904
 4905  {
 4906#line 348
 4907  __cil_tmp8 = (unsigned long )data;
 4908#line 348
 4909  __cil_tmp9 = __cil_tmp8 + 16;
 4910#line 348
 4911  __cil_tmp10 = *((struct acpi_device **)__cil_tmp9);
 4912#line 348
 4913  __cil_tmp11 = (unsigned long )__cil_tmp10;
 4914#line 348
 4915  __cil_tmp12 = __cil_tmp11 + 944;
 4916#line 348
 4917  dev = (struct device *)__cil_tmp12;
 4918#line 350
 4919  __cil_tmp13 = (unsigned long )data;
 4920#line 350
 4921  __cil_tmp14 = __cil_tmp13 + 24;
 4922#line 350
 4923  old_if = *((bool *)__cil_tmp14);
 4924#line 351
 4925  if ((int )old_if) {
 4926#line 351
 4927    tmp___0 = 5;
 4928  } else {
 4929#line 351
 4930    tmp___0 = 7;
 4931  }
 4932#line 351
 4933  expected_size = tmp___0;
 4934  {
 4935#line 354
 4936  __cil_tmp15 = *((acpi_object_type *)obj);
 4937#line 354
 4938  if (__cil_tmp15 != 4U) {
 4939    {
 4940#line 355
 4941    __cil_tmp16 = (struct device  const  *)dev;
 4942#line 355
 4943    __cil_tmp17 = *((acpi_object_type *)obj);
 4944#line 355
 4945    dev_warn(__cil_tmp16, "Invalid type: %d\n", __cil_tmp17);
 4946    }
 4947#line 356
 4948    return (-22);
 4949  } else {
 4950
 4951  }
 4952  }
 4953  {
 4954#line 359
 4955  __cil_tmp18 = (u32 )expected_size;
 4956#line 359
 4957  __cil_tmp19 = 0 + 4;
 4958#line 359
 4959  __cil_tmp20 = (unsigned long )obj;
 4960#line 359
 4961  __cil_tmp21 = __cil_tmp20 + __cil_tmp19;
 4962#line 359
 4963  __cil_tmp22 = *((u32 *)__cil_tmp21);
 4964#line 359
 4965  if (__cil_tmp22 != __cil_tmp18) {
 4966    {
 4967#line 360
 4968    __cil_tmp23 = (struct device  const  *)dev;
 4969#line 360
 4970    __cil_tmp24 = 0 + 4;
 4971#line 360
 4972    __cil_tmp25 = (unsigned long )obj;
 4973#line 360
 4974    __cil_tmp26 = __cil_tmp25 + __cil_tmp24;
 4975#line 360
 4976    __cil_tmp27 = *((u32 *)__cil_tmp26);
 4977#line 360
 4978    dev_warn(__cil_tmp23, "Invalid package size: %d, expected: %d\n", __cil_tmp27,
 4979             expected_size);
 4980    }
 4981#line 362
 4982    return (-22);
 4983  } else {
 4984
 4985  }
 4986  }
 4987  {
 4988#line 365
 4989  __cil_tmp28 = (enum atk_pack_member )0;
 4990#line 365
 4991  tmp = atk_get_pack_member(data, obj, __cil_tmp28);
 4992  }
 4993  {
 4994#line 366
 4995  __cil_tmp29 = *((acpi_object_type *)tmp);
 4996#line 366
 4997  if (__cil_tmp29 != 1U) {
 4998    {
 4999#line 367
 5000    __cil_tmp30 = (struct device  const  *)dev;
 5001#line 367
 5002    __cil_tmp31 = *((acpi_object_type *)tmp);
 5003#line 367
 5004    dev_warn(__cil_tmp30, "Invalid type (flag): %d\n", __cil_tmp31);
 5005    }
 5006#line 368
 5007    return (-22);
 5008  } else {
 5009
 5010  }
 5011  }
 5012  {
 5013#line 371
 5014  __cil_tmp32 = (enum atk_pack_member )1;
 5015#line 371
 5016  tmp = atk_get_pack_member(data, obj, __cil_tmp32);
 5017  }
 5018  {
 5019#line 372
 5020  __cil_tmp33 = *((acpi_object_type *)tmp);
 5021#line 372
 5022  if (__cil_tmp33 != 2U) {
 5023    {
 5024#line 373
 5025    __cil_tmp34 = (struct device  const  *)dev;
 5026#line 373
 5027    __cil_tmp35 = *((acpi_object_type *)tmp);
 5028#line 373
 5029    dev_warn(__cil_tmp34, "Invalid type (name): %d\n", __cil_tmp35);
 5030    }
 5031#line 374
 5032    return (-22);
 5033  } else {
 5034
 5035  }
 5036  }
 5037  {
 5038#line 392
 5039  __cil_tmp36 = (enum atk_pack_member )2;
 5040#line 392
 5041  tmp = atk_get_pack_member(data, obj, __cil_tmp36);
 5042  }
 5043  {
 5044#line 393
 5045  __cil_tmp37 = *((acpi_object_type *)tmp);
 5046#line 393
 5047  if (__cil_tmp37 != 1U) {
 5048    {
 5049#line 394
 5050    __cil_tmp38 = (struct device  const  *)dev;
 5051#line 394
 5052    __cil_tmp39 = *((acpi_object_type *)tmp);
 5053#line 394
 5054    dev_warn(__cil_tmp38, "Invalid type (limit1): %d\n", __cil_tmp39);
 5055    }
 5056#line 395
 5057    return (-22);
 5058  } else {
 5059
 5060  }
 5061  }
 5062  {
 5063#line 398
 5064  __cil_tmp40 = (enum atk_pack_member )3;
 5065#line 398
 5066  tmp = atk_get_pack_member(data, obj, __cil_tmp40);
 5067  }
 5068  {
 5069#line 399
 5070  __cil_tmp41 = *((acpi_object_type *)tmp);
 5071#line 399
 5072  if (__cil_tmp41 != 1U) {
 5073    {
 5074#line 400
 5075    __cil_tmp42 = (struct device  const  *)dev;
 5076#line 400
 5077    __cil_tmp43 = *((acpi_object_type *)tmp);
 5078#line 400
 5079    dev_warn(__cil_tmp42, "Invalid type (limit2): %d\n", __cil_tmp43);
 5080    }
 5081#line 401
 5082    return (-22);
 5083  } else {
 5084
 5085  }
 5086  }
 5087  {
 5088#line 404
 5089  __cil_tmp44 = (enum atk_pack_member )4;
 5090#line 404
 5091  tmp = atk_get_pack_member(data, obj, __cil_tmp44);
 5092  }
 5093  {
 5094#line 405
 5095  __cil_tmp45 = *((acpi_object_type *)tmp);
 5096#line 405
 5097  if (__cil_tmp45 != 1U) {
 5098    {
 5099#line 406
 5100    __cil_tmp46 = (struct device  const  *)dev;
 5101#line 406
 5102    __cil_tmp47 = *((acpi_object_type *)tmp);
 5103#line 406
 5104    dev_warn(__cil_tmp46, "Invalid type (enable): %d\n", __cil_tmp47);
 5105    }
 5106#line 407
 5107    return (-22);
 5108  } else {
 5109
 5110  }
 5111  }
 5112  {
 5113#line 410
 5114  atk_print_sensor(data, obj);
 5115  }
 5116#line 412
 5117  return (0);
 5118}
 5119}
 5120#line 416 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p"
 5121static char const   *atk_sensor_type(union acpi_object *flags ) 
 5122{ u64 type ;
 5123  char const   *what ;
 5124  unsigned long __cil_tmp4 ;
 5125  unsigned long __cil_tmp5 ;
 5126  unsigned long __cil_tmp6 ;
 5127  u64 __cil_tmp7 ;
 5128
 5129  {
 5130#line 418
 5131  __cil_tmp4 = 0 + 8;
 5132#line 418
 5133  __cil_tmp5 = (unsigned long )flags;
 5134#line 418
 5135  __cil_tmp6 = __cil_tmp5 + __cil_tmp4;
 5136#line 418
 5137  __cil_tmp7 = *((u64 *)__cil_tmp6);
 5138#line 418
 5139  type = __cil_tmp7 & 16711680ULL;
 5140#line 422
 5141  if ((int )type == 131072) {
 5142#line 422
 5143    goto case_131072;
 5144  } else
 5145#line 425
 5146  if ((int )type == 196608) {
 5147#line 425
 5148    goto case_196608;
 5149  } else
 5150#line 428
 5151  if ((int )type == 262144) {
 5152#line 428
 5153    goto case_262144;
 5154  } else {
 5155    {
 5156#line 431
 5157    goto switch_default;
 5158#line 421
 5159    if (0) {
 5160      case_131072: /* CIL Label */ 
 5161#line 423
 5162      what = "voltage";
 5163#line 424
 5164      goto ldv_25021;
 5165      case_196608: /* CIL Label */ 
 5166#line 426
 5167      what = "temperature";
 5168#line 427
 5169      goto ldv_25021;
 5170      case_262144: /* CIL Label */ 
 5171#line 429
 5172      what = "fan";
 5173#line 430
 5174      goto ldv_25021;
 5175      switch_default: /* CIL Label */ 
 5176#line 432
 5177      what = "unknown";
 5178#line 433
 5179      goto ldv_25021;
 5180    } else {
 5181      switch_break: /* CIL Label */ ;
 5182    }
 5183    }
 5184  }
 5185  ldv_25021: ;
 5186#line 436
 5187  return (what);
 5188}
 5189}
 5190#line 440 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p"
 5191static void atk_print_sensor(struct atk_data *data , union acpi_object *obj ) 
 5192{ struct device *dev ;
 5193  union acpi_object *flags ;
 5194  union acpi_object *name ;
 5195  union acpi_object *limit1 ;
 5196  union acpi_object *limit2 ;
 5197  union acpi_object *enable ;
 5198  char const   *what ;
 5199  struct _ddebug descriptor ;
 5200  char *tmp ;
 5201  long tmp___0 ;
 5202  unsigned long __cil_tmp13 ;
 5203  unsigned long __cil_tmp14 ;
 5204  struct acpi_device *__cil_tmp15 ;
 5205  unsigned long __cil_tmp16 ;
 5206  unsigned long __cil_tmp17 ;
 5207  enum atk_pack_member __cil_tmp18 ;
 5208  enum atk_pack_member __cil_tmp19 ;
 5209  enum atk_pack_member __cil_tmp20 ;
 5210  enum atk_pack_member __cil_tmp21 ;
 5211  enum atk_pack_member __cil_tmp22 ;
 5212  struct _ddebug *__cil_tmp23 ;
 5213  unsigned long __cil_tmp24 ;
 5214  unsigned long __cil_tmp25 ;
 5215  unsigned long __cil_tmp26 ;
 5216  unsigned long __cil_tmp27 ;
 5217  unsigned long __cil_tmp28 ;
 5218  unsigned long __cil_tmp29 ;
 5219  unsigned char __cil_tmp30 ;
 5220  long __cil_tmp31 ;
 5221  long __cil_tmp32 ;
 5222  unsigned long __cil_tmp33 ;
 5223  unsigned long __cil_tmp34 ;
 5224  unsigned long __cil_tmp35 ;
 5225  u64 __cil_tmp36 ;
 5226  struct device  const  *__cil_tmp37 ;
 5227  unsigned long __cil_tmp38 ;
 5228  unsigned long __cil_tmp39 ;
 5229  unsigned long __cil_tmp40 ;
 5230  u64 __cil_tmp41 ;
 5231  unsigned long __cil_tmp42 ;
 5232  unsigned long __cil_tmp43 ;
 5233  unsigned long __cil_tmp44 ;
 5234  char *__cil_tmp45 ;
 5235  unsigned long __cil_tmp46 ;
 5236  unsigned long __cil_tmp47 ;
 5237  unsigned long __cil_tmp48 ;
 5238  u64 __cil_tmp49 ;
 5239  unsigned long __cil_tmp50 ;
 5240  unsigned long __cil_tmp51 ;
 5241  unsigned long __cil_tmp52 ;
 5242  u64 __cil_tmp53 ;
 5243
 5244  {
 5245  {
 5246#line 443
 5247  __cil_tmp13 = (unsigned long )data;
 5248#line 443
 5249  __cil_tmp14 = __cil_tmp13 + 16;
 5250#line 443
 5251  __cil_tmp15 = *((struct acpi_device **)__cil_tmp14);
 5252#line 443
 5253  __cil_tmp16 = (unsigned long )__cil_tmp15;
 5254#line 443
 5255  __cil_tmp17 = __cil_tmp16 + 944;
 5256#line 443
 5257  dev = (struct device *)__cil_tmp17;
 5258#line 451
 5259  __cil_tmp18 = (enum atk_pack_member )0;
 5260#line 451
 5261  flags = atk_get_pack_member(data, obj, __cil_tmp18);
 5262#line 452
 5263  __cil_tmp19 = (enum atk_pack_member )1;
 5264#line 452
 5265  name = atk_get_pack_member(data, obj, __cil_tmp19);
 5266#line 453
 5267  __cil_tmp20 = (enum atk_pack_member )2;
 5268#line 453
 5269  limit1 = atk_get_pack_member(data, obj, __cil_tmp20);
 5270#line 454
 5271  __cil_tmp21 = (enum atk_pack_member )3;
 5272#line 454
 5273  limit2 = atk_get_pack_member(data, obj, __cil_tmp21);
 5274#line 455
 5275  __cil_tmp22 = (enum atk_pack_member )4;
 5276#line 455
 5277  enable = atk_get_pack_member(data, obj, __cil_tmp22);
 5278#line 457
 5279  what = atk_sensor_type(flags);
 5280#line 459
 5281  __cil_tmp23 = & descriptor;
 5282#line 459
 5283  *((char const   **)__cil_tmp23) = "asus_atk0110";
 5284#line 459
 5285  __cil_tmp24 = (unsigned long )(& descriptor) + 8;
 5286#line 459
 5287  *((char const   **)__cil_tmp24) = "atk_print_sensor";
 5288#line 459
 5289  __cil_tmp25 = (unsigned long )(& descriptor) + 16;
 5290#line 459
 5291  *((char const   **)__cil_tmp25) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p";
 5292#line 459
 5293  __cil_tmp26 = (unsigned long )(& descriptor) + 24;
 5294#line 459
 5295  *((char const   **)__cil_tmp26) = "%s: %#llx %s [%llu-%llu] %s\n";
 5296#line 459
 5297  __cil_tmp27 = (unsigned long )(& descriptor) + 32;
 5298#line 459
 5299  *((unsigned int *)__cil_tmp27) = 463U;
 5300#line 459
 5301  __cil_tmp28 = (unsigned long )(& descriptor) + 35;
 5302#line 459
 5303  *((unsigned char *)__cil_tmp28) = (unsigned char)1;
 5304#line 459
 5305  __cil_tmp29 = (unsigned long )(& descriptor) + 35;
 5306#line 459
 5307  __cil_tmp30 = *((unsigned char *)__cil_tmp29);
 5308#line 459
 5309  __cil_tmp31 = (long )__cil_tmp30;
 5310#line 459
 5311  __cil_tmp32 = __cil_tmp31 & 1L;
 5312#line 459
 5313  tmp___0 = __builtin_expect(__cil_tmp32, 0L);
 5314  }
 5315#line 459
 5316  if (tmp___0 != 0L) {
 5317    {
 5318#line 459
 5319    __cil_tmp33 = 0 + 8;
 5320#line 459
 5321    __cil_tmp34 = (unsigned long )enable;
 5322#line 459
 5323    __cil_tmp35 = __cil_tmp34 + __cil_tmp33;
 5324#line 459
 5325    __cil_tmp36 = *((u64 *)__cil_tmp35);
 5326#line 459
 5327    if (__cil_tmp36 != 0ULL) {
 5328#line 459
 5329      tmp = (char *)"enabled";
 5330    } else {
 5331#line 459
 5332      tmp = (char *)"disabled";
 5333    }
 5334    }
 5335    {
 5336#line 459
 5337    __cil_tmp37 = (struct device  const  *)dev;
 5338#line 459
 5339    __cil_tmp38 = 0 + 8;
 5340#line 459
 5341    __cil_tmp39 = (unsigned long )flags;
 5342#line 459
 5343    __cil_tmp40 = __cil_tmp39 + __cil_tmp38;
 5344#line 459
 5345    __cil_tmp41 = *((u64 *)__cil_tmp40);
 5346#line 459
 5347    __cil_tmp42 = 0 + 8;
 5348#line 459
 5349    __cil_tmp43 = (unsigned long )name;
 5350#line 459
 5351    __cil_tmp44 = __cil_tmp43 + __cil_tmp42;
 5352#line 459
 5353    __cil_tmp45 = *((char **)__cil_tmp44);
 5354#line 459
 5355    __cil_tmp46 = 0 + 8;
 5356#line 459
 5357    __cil_tmp47 = (unsigned long )limit1;
 5358#line 459
 5359    __cil_tmp48 = __cil_tmp47 + __cil_tmp46;
 5360#line 459
 5361    __cil_tmp49 = *((u64 *)__cil_tmp48);
 5362#line 459
 5363    __cil_tmp50 = 0 + 8;
 5364#line 459
 5365    __cil_tmp51 = (unsigned long )limit2;
 5366#line 459
 5367    __cil_tmp52 = __cil_tmp51 + __cil_tmp50;
 5368#line 459
 5369    __cil_tmp53 = *((u64 *)__cil_tmp52);
 5370#line 459
 5371    __dynamic_dev_dbg(& descriptor, __cil_tmp37, "%s: %#llx %s [%llu-%llu] %s\n",
 5372                      what, __cil_tmp41, __cil_tmp45, __cil_tmp49, __cil_tmp53, tmp);
 5373    }
 5374  } else {
 5375
 5376  }
 5377#line 461
 5378  return;
 5379}
 5380}
 5381#line 467 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p"
 5382static int atk_read_value_old(struct atk_sensor_data *sensor , u64 *value ) 
 5383{ struct atk_data *data ;
 5384  struct device *dev ;
 5385  struct acpi_object_list params ;
 5386  union acpi_object id ;
 5387  acpi_status status ;
 5388  acpi_handle method ;
 5389  char const   *tmp ;
 5390  unsigned long __cil_tmp10 ;
 5391  unsigned long __cil_tmp11 ;
 5392  unsigned long __cil_tmp12 ;
 5393  unsigned long __cil_tmp13 ;
 5394  struct acpi_device *__cil_tmp14 ;
 5395  unsigned long __cil_tmp15 ;
 5396  unsigned long __cil_tmp16 ;
 5397  unsigned long __cil_tmp17 ;
 5398  unsigned long __cil_tmp18 ;
 5399  u64 __cil_tmp19 ;
 5400  unsigned long __cil_tmp20 ;
 5401  unsigned long __cil_tmp21 ;
 5402  unsigned long __cil_tmp22 ;
 5403  unsigned long __cil_tmp23 ;
 5404  unsigned long __cil_tmp24 ;
 5405  unsigned long __cil_tmp25 ;
 5406  union acpi_object *__cil_tmp26 ;
 5407  unsigned long __cil_tmp27 ;
 5408  unsigned long __cil_tmp28 ;
 5409  unsigned long __cil_tmp29 ;
 5410  unsigned long __cil_tmp30 ;
 5411  struct acpi_object_list *__cil_tmp31 ;
 5412  unsigned long __cil_tmp32 ;
 5413  acpi_string __cil_tmp33 ;
 5414  struct device  const  *__cil_tmp34 ;
 5415
 5416  {
 5417#line 469
 5418  __cil_tmp10 = (unsigned long )sensor;
 5419#line 469
 5420  __cil_tmp11 = __cil_tmp10 + 16;
 5421#line 469
 5422  data = *((struct atk_data **)__cil_tmp11);
 5423#line 470
 5424  __cil_tmp12 = (unsigned long )data;
 5425#line 470
 5426  __cil_tmp13 = __cil_tmp12 + 16;
 5427#line 470
 5428  __cil_tmp14 = *((struct acpi_device **)__cil_tmp13);
 5429#line 470
 5430  __cil_tmp15 = (unsigned long )__cil_tmp14;
 5431#line 470
 5432  __cil_tmp16 = __cil_tmp15 + 944;
 5433#line 470
 5434  dev = (struct device *)__cil_tmp16;
 5435  {
 5436#line 476
 5437  __cil_tmp17 = (unsigned long )sensor;
 5438#line 476
 5439  __cil_tmp18 = __cil_tmp17 + 288;
 5440#line 476
 5441  __cil_tmp19 = *((u64 *)__cil_tmp18);
 5442#line 477
 5443  if ((int )__cil_tmp19 == 131072) {
 5444#line 477
 5445    goto case_131072;
 5446  } else
 5447#line 480
 5448  if ((int )__cil_tmp19 == 196608) {
 5449#line 480
 5450    goto case_196608;
 5451  } else
 5452#line 483
 5453  if ((int )__cil_tmp19 == 262144) {
 5454#line 483
 5455    goto case_262144;
 5456  } else {
 5457    {
 5458#line 486
 5459    goto switch_default;
 5460#line 476
 5461    if (0) {
 5462      case_131072: /* CIL Label */ 
 5463#line 478
 5464      __cil_tmp20 = (unsigned long )data;
 5465#line 478
 5466      __cil_tmp21 = __cil_tmp20 + 40;
 5467#line 478
 5468      method = *((acpi_handle *)__cil_tmp21);
 5469#line 479
 5470      goto ldv_25049;
 5471      case_196608: /* CIL Label */ 
 5472#line 481
 5473      __cil_tmp22 = (unsigned long )data;
 5474#line 481
 5475      __cil_tmp23 = __cil_tmp22 + 32;
 5476#line 481
 5477      method = *((acpi_handle *)__cil_tmp23);
 5478#line 482
 5479      goto ldv_25049;
 5480      case_262144: /* CIL Label */ 
 5481#line 484
 5482      __cil_tmp24 = (unsigned long )data;
 5483#line 484
 5484      __cil_tmp25 = __cil_tmp24 + 48;
 5485#line 484
 5486      method = *((acpi_handle *)__cil_tmp25);
 5487#line 485
 5488      goto ldv_25049;
 5489      switch_default: /* CIL Label */ ;
 5490#line 487
 5491      return (-22);
 5492    } else {
 5493      switch_break: /* CIL Label */ ;
 5494    }
 5495    }
 5496  }
 5497  }
 5498  ldv_25049: 
 5499  {
 5500#line 490
 5501  __cil_tmp26 = & id;
 5502#line 490
 5503  *((acpi_object_type *)__cil_tmp26) = 1U;
 5504#line 491
 5505  __cil_tmp27 = 0 + 8;
 5506#line 491
 5507  __cil_tmp28 = (unsigned long )(& id) + __cil_tmp27;
 5508#line 491
 5509  __cil_tmp29 = (unsigned long )sensor;
 5510#line 491
 5511  __cil_tmp30 = __cil_tmp29 + 280;
 5512#line 491
 5513  *((u64 *)__cil_tmp28) = *((u64 *)__cil_tmp30);
 5514#line 493
 5515  __cil_tmp31 = & params;
 5516#line 493
 5517  *((u32 *)__cil_tmp31) = 1U;
 5518#line 494
 5519  __cil_tmp32 = (unsigned long )(& params) + 8;
 5520#line 494
 5521  *((union acpi_object **)__cil_tmp32) = & id;
 5522#line 496
 5523  __cil_tmp33 = (acpi_string )0;
 5524#line 496
 5525  status = acpi_evaluate_integer(method, __cil_tmp33, & params, value);
 5526  }
 5527#line 497
 5528  if (status != 0U) {
 5529    {
 5530#line 498
 5531    tmp = acpi_format_exception(status);
 5532#line 498
 5533    __cil_tmp34 = (struct device  const  *)dev;
 5534#line 498
 5535    dev_warn(__cil_tmp34, "%s: ACPI exception: %s\n", "atk_read_value_old", tmp);
 5536    }
 5537#line 500
 5538    return (-5);
 5539  } else {
 5540
 5541  }
 5542#line 503
 5543  return (0);
 5544}
 5545}
 5546#line 506 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p"
 5547static union acpi_object *atk_ggrp(struct atk_data *data , u16 mux ) 
 5548{ struct device *dev ;
 5549  struct acpi_buffer buf ;
 5550  acpi_status ret ;
 5551  struct acpi_object_list params ;
 5552  union acpi_object id ;
 5553  union acpi_object *pack ;
 5554  char const   *tmp ;
 5555  void *tmp___0 ;
 5556  void *tmp___1 ;
 5557  void *tmp___2 ;
 5558  unsigned long __cil_tmp13 ;
 5559  unsigned long __cil_tmp14 ;
 5560  struct acpi_device *__cil_tmp15 ;
 5561  unsigned long __cil_tmp16 ;
 5562  unsigned long __cil_tmp17 ;
 5563  union acpi_object *__cil_tmp18 ;
 5564  unsigned long __cil_tmp19 ;
 5565  unsigned long __cil_tmp20 ;
 5566  struct acpi_object_list *__cil_tmp21 ;
 5567  unsigned long __cil_tmp22 ;
 5568  struct acpi_buffer *__cil_tmp23 ;
 5569  unsigned long __cil_tmp24 ;
 5570  unsigned long __cil_tmp25 ;
 5571  acpi_handle __cil_tmp26 ;
 5572  acpi_string __cil_tmp27 ;
 5573  struct device  const  *__cil_tmp28 ;
 5574  int __cil_tmp29 ;
 5575  unsigned long __cil_tmp30 ;
 5576  void *__cil_tmp31 ;
 5577  acpi_object_type __cil_tmp32 ;
 5578  void const   *__cil_tmp33 ;
 5579  unsigned long __cil_tmp34 ;
 5580  unsigned long __cil_tmp35 ;
 5581  unsigned long __cil_tmp36 ;
 5582  u32 __cil_tmp37 ;
 5583  struct device  const  *__cil_tmp38 ;
 5584  int __cil_tmp39 ;
 5585  void const   *__cil_tmp40 ;
 5586
 5587  {
 5588  {
 5589#line 508
 5590  __cil_tmp13 = (unsigned long )data;
 5591#line 508
 5592  __cil_tmp14 = __cil_tmp13 + 16;
 5593#line 508
 5594  __cil_tmp15 = *((struct acpi_device **)__cil_tmp14);
 5595#line 508
 5596  __cil_tmp16 = (unsigned long )__cil_tmp15;
 5597#line 508
 5598  __cil_tmp17 = __cil_tmp16 + 944;
 5599#line 508
 5600  dev = (struct device *)__cil_tmp17;
 5601#line 515
 5602  __cil_tmp18 = & id;
 5603#line 515
 5604  *((acpi_object_type *)__cil_tmp18) = 1U;
 5605#line 516
 5606  __cil_tmp19 = 0 + 8;
 5607#line 516
 5608  __cil_tmp20 = (unsigned long )(& id) + __cil_tmp19;
 5609#line 516
 5610  *((u64 *)__cil_tmp20) = (u64 )mux;
 5611#line 517
 5612  __cil_tmp21 = & params;
 5613#line 517
 5614  *((u32 *)__cil_tmp21) = 1U;
 5615#line 518
 5616  __cil_tmp22 = (unsigned long )(& params) + 8;
 5617#line 518
 5618  *((union acpi_object **)__cil_tmp22) = & id;
 5619#line 520
 5620  __cil_tmp23 = & buf;
 5621#line 520
 5622  *((acpi_size *)__cil_tmp23) = 0xffffffffffffffffULL;
 5623#line 521
 5624  __cil_tmp24 = (unsigned long )data;
 5625#line 521
 5626  __cil_tmp25 = __cil_tmp24 + 56;
 5627#line 521
 5628  __cil_tmp26 = *((acpi_handle *)__cil_tmp25);
 5629#line 521
 5630  __cil_tmp27 = (acpi_string )0;
 5631#line 521
 5632  ret = acpi_evaluate_object(__cil_tmp26, __cil_tmp27, & params, & buf);
 5633  }
 5634#line 522
 5635  if (ret != 0U) {
 5636    {
 5637#line 523
 5638    tmp = acpi_format_exception(ret);
 5639#line 523
 5640    __cil_tmp28 = (struct device  const  *)dev;
 5641#line 523
 5642    __cil_tmp29 = (int )mux;
 5643#line 523
 5644    dev_err(__cil_tmp28, "GGRP[%#x] ACPI exception: %s\n", __cil_tmp29, tmp);
 5645#line 525
 5646    tmp___0 = ERR_PTR(-5L);
 5647    }
 5648#line 525
 5649    return ((union acpi_object *)tmp___0);
 5650  } else {
 5651
 5652  }
 5653#line 527
 5654  __cil_tmp30 = (unsigned long )(& buf) + 8;
 5655#line 527
 5656  __cil_tmp31 = *((void **)__cil_tmp30);
 5657#line 527
 5658  pack = (union acpi_object *)__cil_tmp31;
 5659  {
 5660#line 528
 5661  __cil_tmp32 = *((acpi_object_type *)pack);
 5662#line 528
 5663  if (__cil_tmp32 != 4U) {
 5664    {
 5665#line 530
 5666    __cil_tmp33 = (void const   *)pack;
 5667#line 530
 5668    kfree(__cil_tmp33);
 5669#line 531
 5670    tmp___1 = ERR_PTR(-2L);
 5671    }
 5672#line 531
 5673    return ((union acpi_object *)tmp___1);
 5674  } else {
 5675
 5676  }
 5677  }
 5678  {
 5679#line 534
 5680  __cil_tmp34 = 0 + 4;
 5681#line 534
 5682  __cil_tmp35 = (unsigned long )pack;
 5683#line 534
 5684  __cil_tmp36 = __cil_tmp35 + __cil_tmp34;
 5685#line 534
 5686  __cil_tmp37 = *((u32 *)__cil_tmp36);
 5687#line 534
 5688  if (__cil_tmp37 == 0U) {
 5689    {
 5690#line 535
 5691    __cil_tmp38 = (struct device  const  *)dev;
 5692#line 535
 5693    __cil_tmp39 = (int )mux;
 5694#line 535
 5695    dev_err(__cil_tmp38, "GGRP[%#x] package is too small\n", __cil_tmp39);
 5696#line 536
 5697    __cil_tmp40 = (void const   *)pack;
 5698#line 536
 5699    kfree(__cil_tmp40);
 5700#line 537
 5701    tmp___2 = ERR_PTR(-5L);
 5702    }
 5703#line 537
 5704    return ((union acpi_object *)tmp___2);
 5705  } else {
 5706
 5707  }
 5708  }
 5709#line 539
 5710  return (pack);
 5711}
 5712}
 5713#line 542 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p"
 5714static union acpi_object *atk_gitm(struct atk_data *data , u64 id ) 
 5715{ struct device *dev ;
 5716  struct atk_acpi_input_buf buf ;
 5717  union acpi_object tmp ;
 5718  struct acpi_object_list params ;
 5719  struct acpi_buffer ret ;
 5720  union acpi_object *obj ;
 5721  acpi_status status ;
 5722  char const   *tmp___0 ;
 5723  void *tmp___1 ;
 5724  void *tmp___2 ;
 5725  unsigned long __cil_tmp13 ;
 5726  unsigned long __cil_tmp14 ;
 5727  struct acpi_device *__cil_tmp15 ;
 5728  unsigned long __cil_tmp16 ;
 5729  unsigned long __cil_tmp17 ;
 5730  struct atk_acpi_input_buf *__cil_tmp18 ;
 5731  unsigned long __cil_tmp19 ;
 5732  unsigned long __cil_tmp20 ;
 5733  union acpi_object *__cil_tmp21 ;
 5734  unsigned long __cil_tmp22 ;
 5735  unsigned long __cil_tmp23 ;
 5736  unsigned long __cil_tmp24 ;
 5737  unsigned long __cil_tmp25 ;
 5738  struct acpi_object_list *__cil_tmp26 ;
 5739  unsigned long __cil_tmp27 ;
 5740  struct acpi_buffer *__cil_tmp28 ;
 5741  unsigned long __cil_tmp29 ;
 5742  unsigned long __cil_tmp30 ;
 5743  acpi_handle __cil_tmp31 ;
 5744  acpi_string __cil_tmp32 ;
 5745  struct device  const  *__cil_tmp33 ;
 5746  unsigned long __cil_tmp34 ;
 5747  void *__cil_tmp35 ;
 5748  unsigned long __cil_tmp36 ;
 5749  unsigned long __cil_tmp37 ;
 5750  unsigned long __cil_tmp38 ;
 5751  u32 __cil_tmp39 ;
 5752  struct device  const  *__cil_tmp40 ;
 5753  unsigned long __cil_tmp41 ;
 5754  unsigned long __cil_tmp42 ;
 5755  unsigned long __cil_tmp43 ;
 5756  u32 __cil_tmp44 ;
 5757  void const   *__cil_tmp45 ;
 5758
 5759  {
 5760  {
 5761#line 544
 5762  __cil_tmp13 = (unsigned long )data;
 5763#line 544
 5764  __cil_tmp14 = __cil_tmp13 + 16;
 5765#line 544
 5766  __cil_tmp15 = *((struct acpi_device **)__cil_tmp14);
 5767#line 544
 5768  __cil_tmp16 = (unsigned long )__cil_tmp15;
 5769#line 544
 5770  __cil_tmp17 = __cil_tmp16 + 944;
 5771#line 544
 5772  dev = (struct device *)__cil_tmp17;
 5773#line 552
 5774  __cil_tmp18 = & buf;
 5775#line 552
 5776  *((u32 *)__cil_tmp18) = (u32 )id;
 5777#line 553
 5778  __cil_tmp19 = (unsigned long )(& buf) + 4;
 5779#line 553
 5780  *((u32 *)__cil_tmp19) = 0U;
 5781#line 554
 5782  __cil_tmp20 = (unsigned long )(& buf) + 8;
 5783#line 554
 5784  *((u32 *)__cil_tmp20) = 0U;
 5785#line 556
 5786  __cil_tmp21 = & tmp;
 5787#line 556
 5788  *((acpi_object_type *)__cil_tmp21) = 3U;
 5789#line 557
 5790  __cil_tmp22 = 0 + 8;
 5791#line 557
 5792  __cil_tmp23 = (unsigned long )(& tmp) + __cil_tmp22;
 5793#line 557
 5794  *((u8 **)__cil_tmp23) = (u8 *)(& buf);
 5795#line 558
 5796  __cil_tmp24 = 0 + 4;
 5797#line 558
 5798  __cil_tmp25 = (unsigned long )(& tmp) + __cil_tmp24;
 5799#line 558
 5800  *((u32 *)__cil_tmp25) = 12U;
 5801#line 560
 5802  __cil_tmp26 = & params;
 5803#line 560
 5804  *((u32 *)__cil_tmp26) = 1U;
 5805#line 561
 5806  __cil_tmp27 = (unsigned long )(& params) + 8;
 5807#line 561
 5808  *((union acpi_object **)__cil_tmp27) = & tmp;
 5809#line 563
 5810  __cil_tmp28 = & ret;
 5811#line 563
 5812  *((acpi_size *)__cil_tmp28) = 0xffffffffffffffffULL;
 5813#line 564
 5814  __cil_tmp29 = (unsigned long )data;
 5815#line 564
 5816  __cil_tmp30 = __cil_tmp29 + 64;
 5817#line 564
 5818  __cil_tmp31 = *((acpi_handle *)__cil_tmp30);
 5819#line 564
 5820  __cil_tmp32 = (acpi_string )0;
 5821#line 564
 5822  status = acpi_evaluate_object_typed(__cil_tmp31, __cil_tmp32, & params, & ret, 3U);
 5823  }
 5824#line 566
 5825  if (status != 0U) {
 5826    {
 5827#line 567
 5828    tmp___0 = acpi_format_exception(status);
 5829#line 567
 5830    __cil_tmp33 = (struct device  const  *)dev;
 5831#line 567
 5832    dev_warn(__cil_tmp33, "GITM[%#llx] ACPI exception: %s\n", id, tmp___0);
 5833#line 569
 5834    tmp___1 = ERR_PTR(-5L);
 5835    }
 5836#line 569
 5837    return ((union acpi_object *)tmp___1);
 5838  } else {
 5839
 5840  }
 5841#line 571
 5842  __cil_tmp34 = (unsigned long )(& ret) + 8;
 5843#line 571
 5844  __cil_tmp35 = *((void **)__cil_tmp34);
 5845#line 571
 5846  obj = (union acpi_object *)__cil_tmp35;
 5847  {
 5848#line 574
 5849  __cil_tmp36 = 0 + 4;
 5850#line 574
 5851  __cil_tmp37 = (unsigned long )obj;
 5852#line 574
 5853  __cil_tmp38 = __cil_tmp37 + __cil_tmp36;
 5854#line 574
 5855  __cil_tmp39 = *((u32 *)__cil_tmp38);
 5856#line 574
 5857  if (__cil_tmp39 <= 7U) {
 5858    {
 5859#line 575
 5860    __cil_tmp40 = (struct device  const  *)dev;
 5861#line 575
 5862    __cil_tmp41 = 0 + 4;
 5863#line 575
 5864    __cil_tmp42 = (unsigned long )obj;
 5865#line 575
 5866    __cil_tmp43 = __cil_tmp42 + __cil_tmp41;
 5867#line 575
 5868    __cil_tmp44 = *((u32 *)__cil_tmp43);
 5869#line 575
 5870    dev_warn(__cil_tmp40, "Unexpected ASBF length: %u\n", __cil_tmp44);
 5871#line 577
 5872    __cil_tmp45 = (void const   *)obj;
 5873#line 577
 5874    kfree(__cil_tmp45);
 5875#line 578
 5876    tmp___2 = ERR_PTR(-5L);
 5877    }
 5878#line 578
 5879    return ((union acpi_object *)tmp___2);
 5880  } else {
 5881
 5882  }
 5883  }
 5884#line 580
 5885  return (obj);
 5886}
 5887}
 5888#line 583 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p"
 5889static union acpi_object *atk_sitm(struct atk_data *data , struct atk_acpi_input_buf *buf ) 
 5890{ struct device *dev ;
 5891  struct acpi_object_list params ;
 5892  union acpi_object tmp ;
 5893  struct acpi_buffer ret ;
 5894  union acpi_object *obj ;
 5895  acpi_status status ;
 5896  char const   *tmp___0 ;
 5897  void *tmp___1 ;
 5898  void *tmp___2 ;
 5899  unsigned long __cil_tmp12 ;
 5900  unsigned long __cil_tmp13 ;
 5901  struct acpi_device *__cil_tmp14 ;
 5902  unsigned long __cil_tmp15 ;
 5903  unsigned long __cil_tmp16 ;
 5904  union acpi_object *__cil_tmp17 ;
 5905  unsigned long __cil_tmp18 ;
 5906  unsigned long __cil_tmp19 ;
 5907  unsigned long __cil_tmp20 ;
 5908  unsigned long __cil_tmp21 ;
 5909  struct acpi_object_list *__cil_tmp22 ;
 5910  unsigned long __cil_tmp23 ;
 5911  struct acpi_buffer *__cil_tmp24 ;
 5912  unsigned long __cil_tmp25 ;
 5913  unsigned long __cil_tmp26 ;
 5914  acpi_handle __cil_tmp27 ;
 5915  acpi_string __cil_tmp28 ;
 5916  struct device  const  *__cil_tmp29 ;
 5917  u32 __cil_tmp30 ;
 5918  unsigned long __cil_tmp31 ;
 5919  void *__cil_tmp32 ;
 5920  unsigned long __cil_tmp33 ;
 5921  unsigned long __cil_tmp34 ;
 5922  unsigned long __cil_tmp35 ;
 5923  u32 __cil_tmp36 ;
 5924  struct device  const  *__cil_tmp37 ;
 5925  unsigned long __cil_tmp38 ;
 5926  unsigned long __cil_tmp39 ;
 5927  unsigned long __cil_tmp40 ;
 5928  u32 __cil_tmp41 ;
 5929  void const   *__cil_tmp42 ;
 5930
 5931  {
 5932  {
 5933#line 586
 5934  __cil_tmp12 = (unsigned long )data;
 5935#line 586
 5936  __cil_tmp13 = __cil_tmp12 + 16;
 5937#line 586
 5938  __cil_tmp14 = *((struct acpi_device **)__cil_tmp13);
 5939#line 586
 5940  __cil_tmp15 = (unsigned long )__cil_tmp14;
 5941#line 586
 5942  __cil_tmp16 = __cil_tmp15 + 944;
 5943#line 586
 5944  dev = (struct device *)__cil_tmp16;
 5945#line 593
 5946  __cil_tmp17 = & tmp;
 5947#line 593
 5948  *((acpi_object_type *)__cil_tmp17) = 3U;
 5949#line 594
 5950  __cil_tmp18 = 0 + 8;
 5951#line 594
 5952  __cil_tmp19 = (unsigned long )(& tmp) + __cil_tmp18;
 5953#line 594
 5954  *((u8 **)__cil_tmp19) = (u8 *)buf;
 5955#line 595
 5956  __cil_tmp20 = 0 + 4;
 5957#line 595
 5958  __cil_tmp21 = (unsigned long )(& tmp) + __cil_tmp20;
 5959#line 595
 5960  *((u32 *)__cil_tmp21) = 12U;
 5961#line 597
 5962  __cil_tmp22 = & params;
 5963#line 597
 5964  *((u32 *)__cil_tmp22) = 1U;
 5965#line 598
 5966  __cil_tmp23 = (unsigned long )(& params) + 8;
 5967#line 598
 5968  *((union acpi_object **)__cil_tmp23) = & tmp;
 5969#line 600
 5970  __cil_tmp24 = & ret;
 5971#line 600
 5972  *((acpi_size *)__cil_tmp24) = 0xffffffffffffffffULL;
 5973#line 601
 5974  __cil_tmp25 = (unsigned long )data;
 5975#line 601
 5976  __cil_tmp26 = __cil_tmp25 + 72;
 5977#line 601
 5978  __cil_tmp27 = *((acpi_handle *)__cil_tmp26);
 5979#line 601
 5980  __cil_tmp28 = (acpi_string )0;
 5981#line 601
 5982  status = acpi_evaluate_object_typed(__cil_tmp27, __cil_tmp28, & params, & ret, 3U);
 5983  }
 5984#line 603
 5985  if (status != 0U) {
 5986    {
 5987#line 604
 5988    tmp___0 = acpi_format_exception(status);
 5989#line 604
 5990    __cil_tmp29 = (struct device  const  *)dev;
 5991#line 604
 5992    __cil_tmp30 = *((u32 *)buf);
 5993#line 604
 5994    dev_warn(__cil_tmp29, "SITM[%#x] ACPI exception: %s\n", __cil_tmp30, tmp___0);
 5995#line 606
 5996    tmp___1 = ERR_PTR(-5L);
 5997    }
 5998#line 606
 5999    return ((union acpi_object *)tmp___1);
 6000  } else {
 6001
 6002  }
 6003#line 608
 6004  __cil_tmp31 = (unsigned long )(& ret) + 8;
 6005#line 608
 6006  __cil_tmp32 = *((void **)__cil_tmp31);
 6007#line 608
 6008  obj = (union acpi_object *)__cil_tmp32;
 6009  {
 6010#line 611
 6011  __cil_tmp33 = 0 + 4;
 6012#line 611
 6013  __cil_tmp34 = (unsigned long )obj;
 6014#line 611
 6015  __cil_tmp35 = __cil_tmp34 + __cil_tmp33;
 6016#line 611
 6017  __cil_tmp36 = *((u32 *)__cil_tmp35);
 6018#line 611
 6019  if (__cil_tmp36 <= 7U) {
 6020    {
 6021#line 612
 6022    __cil_tmp37 = (struct device  const  *)dev;
 6023#line 612
 6024    __cil_tmp38 = 0 + 4;
 6025#line 612
 6026    __cil_tmp39 = (unsigned long )obj;
 6027#line 612
 6028    __cil_tmp40 = __cil_tmp39 + __cil_tmp38;
 6029#line 612
 6030    __cil_tmp41 = *((u32 *)__cil_tmp40);
 6031#line 612
 6032    dev_warn(__cil_tmp37, "Unexpected ASBF length: %u\n", __cil_tmp41);
 6033#line 614
 6034    __cil_tmp42 = (void const   *)obj;
 6035#line 614
 6036    kfree(__cil_tmp42);
 6037#line 615
 6038    tmp___2 = ERR_PTR(-5L);
 6039    }
 6040#line 615
 6041    return ((union acpi_object *)tmp___2);
 6042  } else {
 6043
 6044  }
 6045  }
 6046#line 617
 6047  return (obj);
 6048}
 6049}
 6050#line 620 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p"
 6051static int atk_read_value_new(struct atk_sensor_data *sensor , u64 *value ) 
 6052{ struct atk_data *data ;
 6053  struct device *dev ;
 6054  union acpi_object *obj ;
 6055  struct atk_acpi_ret_buffer *buf ;
 6056  int err ;
 6057  long tmp ;
 6058  long tmp___0 ;
 6059  unsigned long __cil_tmp10 ;
 6060  unsigned long __cil_tmp11 ;
 6061  unsigned long __cil_tmp12 ;
 6062  unsigned long __cil_tmp13 ;
 6063  struct acpi_device *__cil_tmp14 ;
 6064  unsigned long __cil_tmp15 ;
 6065  unsigned long __cil_tmp16 ;
 6066  unsigned long __cil_tmp17 ;
 6067  unsigned long __cil_tmp18 ;
 6068  u64 __cil_tmp19 ;
 6069  void const   *__cil_tmp20 ;
 6070  void const   *__cil_tmp21 ;
 6071  unsigned long __cil_tmp22 ;
 6072  unsigned long __cil_tmp23 ;
 6073  unsigned long __cil_tmp24 ;
 6074  u8 *__cil_tmp25 ;
 6075  u32 __cil_tmp26 ;
 6076  struct device  const  *__cil_tmp27 ;
 6077  unsigned long __cil_tmp28 ;
 6078  unsigned long __cil_tmp29 ;
 6079  u64 __cil_tmp30 ;
 6080  unsigned long __cil_tmp31 ;
 6081  unsigned long __cil_tmp32 ;
 6082  u32 __cil_tmp33 ;
 6083  void const   *__cil_tmp34 ;
 6084
 6085  {
 6086  {
 6087#line 622
 6088  __cil_tmp10 = (unsigned long )sensor;
 6089#line 622
 6090  __cil_tmp11 = __cil_tmp10 + 16;
 6091#line 622
 6092  data = *((struct atk_data **)__cil_tmp11);
 6093#line 623
 6094  __cil_tmp12 = (unsigned long )data;
 6095#line 623
 6096  __cil_tmp13 = __cil_tmp12 + 16;
 6097#line 623
 6098  __cil_tmp14 = *((struct acpi_device **)__cil_tmp13);
 6099#line 623
 6100  __cil_tmp15 = (unsigned long )__cil_tmp14;
 6101#line 623
 6102  __cil_tmp16 = __cil_tmp15 + 944;
 6103#line 623
 6104  dev = (struct device *)__cil_tmp16;
 6105#line 626
 6106  err = 0;
 6107#line 628
 6108  __cil_tmp17 = (unsigned long )sensor;
 6109#line 628
 6110  __cil_tmp18 = __cil_tmp17 + 280;
 6111#line 628
 6112  __cil_tmp19 = *((u64 *)__cil_tmp18);
 6113#line 628
 6114  obj = atk_gitm(data, __cil_tmp19);
 6115#line 629
 6116  __cil_tmp20 = (void const   *)obj;
 6117#line 629
 6118  tmp___0 = IS_ERR(__cil_tmp20);
 6119  }
 6120#line 629
 6121  if (tmp___0 != 0L) {
 6122    {
 6123#line 630
 6124    __cil_tmp21 = (void const   *)obj;
 6125#line 630
 6126    tmp = PTR_ERR(__cil_tmp21);
 6127    }
 6128#line 630
 6129    return ((int )tmp);
 6130  } else {
 6131
 6132  }
 6133#line 632
 6134  __cil_tmp22 = 0 + 8;
 6135#line 632
 6136  __cil_tmp23 = (unsigned long )obj;
 6137#line 632
 6138  __cil_tmp24 = __cil_tmp23 + __cil_tmp22;
 6139#line 632
 6140  __cil_tmp25 = *((u8 **)__cil_tmp24);
 6141#line 632
 6142  buf = (struct atk_acpi_ret_buffer *)__cil_tmp25;
 6143  {
 6144#line 633
 6145  __cil_tmp26 = *((u32 *)buf);
 6146#line 633
 6147  if (__cil_tmp26 == 0U) {
 6148    {
 6149#line 639
 6150    __cil_tmp27 = (struct device  const  *)dev;
 6151#line 639
 6152    __cil_tmp28 = (unsigned long )sensor;
 6153#line 639
 6154    __cil_tmp29 = __cil_tmp28 + 280;
 6155#line 639
 6156    __cil_tmp30 = *((u64 *)__cil_tmp29);
 6157#line 639
 6158    dev_warn(__cil_tmp27, "Read failed, sensor = %#llx\n", __cil_tmp30);
 6159#line 640
 6160    err = -5;
 6161    }
 6162#line 641
 6163    goto out;
 6164  } else {
 6165
 6166  }
 6167  }
 6168#line 644
 6169  __cil_tmp31 = (unsigned long )buf;
 6170#line 644
 6171  __cil_tmp32 = __cil_tmp31 + 4;
 6172#line 644
 6173  __cil_tmp33 = *((u32 *)__cil_tmp32);
 6174#line 644
 6175  *value = (u64 )__cil_tmp33;
 6176  out: 
 6177  {
 6178#line 646
 6179  __cil_tmp34 = (void const   *)obj;
 6180#line 646
 6181  kfree(__cil_tmp34);
 6182  }
 6183#line 647
 6184  return (err);
 6185}
 6186}
 6187#line 650 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p"
 6188static int atk_read_value(struct atk_sensor_data *sensor , u64 *value ) 
 6189{ int err ;
 6190  unsigned long __cil_tmp8 ;
 6191  unsigned long __cil_tmp9 ;
 6192  bool __cil_tmp10 ;
 6193  long __cil_tmp11 ;
 6194  unsigned long __cil_tmp12 ;
 6195  unsigned long __cil_tmp13 ;
 6196  unsigned long __cil_tmp14 ;
 6197  unsigned long __cil_tmp15 ;
 6198  long __cil_tmp16 ;
 6199  long __cil_tmp17 ;
 6200  unsigned long __cil_tmp18 ;
 6201  unsigned long __cil_tmp19 ;
 6202  struct atk_data *__cil_tmp20 ;
 6203  unsigned long __cil_tmp21 ;
 6204  unsigned long __cil_tmp22 ;
 6205  bool __cil_tmp23 ;
 6206  unsigned long __cil_tmp24 ;
 6207  unsigned long __cil_tmp25 ;
 6208  unsigned long __cil_tmp26 ;
 6209  unsigned long __cil_tmp27 ;
 6210  unsigned long __cil_tmp28 ;
 6211  unsigned long __cil_tmp29 ;
 6212  unsigned long __cil_tmp30 ;
 6213  unsigned long __cil_tmp31 ;
 6214
 6215  {
 6216  {
 6217#line 655
 6218  __cil_tmp8 = (unsigned long )sensor;
 6219#line 655
 6220  __cil_tmp9 = __cil_tmp8 + 328;
 6221#line 655
 6222  __cil_tmp10 = *((bool *)__cil_tmp9);
 6223#line 655
 6224  if (! __cil_tmp10) {
 6225#line 655
 6226    goto _L;
 6227  } else {
 6228    {
 6229#line 655
 6230    __cil_tmp11 = (long )jiffies;
 6231#line 655
 6232    __cil_tmp12 = (unsigned long )sensor;
 6233#line 655
 6234    __cil_tmp13 = __cil_tmp12 + 320;
 6235#line 655
 6236    __cil_tmp14 = *((unsigned long *)__cil_tmp13);
 6237#line 655
 6238    __cil_tmp15 = __cil_tmp14 + 250UL;
 6239#line 655
 6240    __cil_tmp16 = (long )__cil_tmp15;
 6241#line 655
 6242    __cil_tmp17 = __cil_tmp16 - __cil_tmp11;
 6243#line 655
 6244    if (__cil_tmp17 < 0L) {
 6245      _L: /* CIL Label */ 
 6246      {
 6247#line 656
 6248      __cil_tmp18 = (unsigned long )sensor;
 6249#line 656
 6250      __cil_tmp19 = __cil_tmp18 + 16;
 6251#line 656
 6252      __cil_tmp20 = *((struct atk_data **)__cil_tmp19);
 6253#line 656
 6254      __cil_tmp21 = (unsigned long )__cil_tmp20;
 6255#line 656
 6256      __cil_tmp22 = __cil_tmp21 + 24;
 6257#line 656
 6258      __cil_tmp23 = *((bool *)__cil_tmp22);
 6259#line 656
 6260      if ((int )__cil_tmp23) {
 6261        {
 6262#line 657
 6263        err = atk_read_value_old(sensor, value);
 6264        }
 6265      } else {
 6266        {
 6267#line 659
 6268        err = atk_read_value_new(sensor, value);
 6269        }
 6270      }
 6271      }
 6272#line 661
 6273      __cil_tmp24 = (unsigned long )sensor;
 6274#line 661
 6275      __cil_tmp25 = __cil_tmp24 + 328;
 6276#line 661
 6277      *((bool *)__cil_tmp25) = (bool )1;
 6278#line 662
 6279      __cil_tmp26 = (unsigned long )sensor;
 6280#line 662
 6281      __cil_tmp27 = __cil_tmp26 + 320;
 6282#line 662
 6283      *((unsigned long *)__cil_tmp27) = (unsigned long )jiffies;
 6284#line 663
 6285      __cil_tmp28 = (unsigned long )sensor;
 6286#line 663
 6287      __cil_tmp29 = __cil_tmp28 + 312;
 6288#line 663
 6289      *((u64 *)__cil_tmp29) = *value;
 6290    } else {
 6291#line 665
 6292      __cil_tmp30 = (unsigned long )sensor;
 6293#line 665
 6294      __cil_tmp31 = __cil_tmp30 + 312;
 6295#line 665
 6296      *value = *((u64 *)__cil_tmp31);
 6297#line 666
 6298      err = 0;
 6299    }
 6300    }
 6301  }
 6302  }
 6303#line 669
 6304  return (err);
 6305}
 6306}
 6307#line 673 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11038/dscv_tempdir/dscv/ri/43_1a/drivers/hwmon/asus_atk0110.c.p"
 6308static int atk_debugfs_gitm_get(void *p , u64 *val ) 
 6309{ struct atk_data *data ;
 6310  union acpi_object *ret ;
 6311  struct atk_acpi_ret_buffer *buf ;
 6312  int err ;
 6313  long tmp ;
 6314  long tmp___0 ;
 6315  acpi_handle __cil_tmp9 ;
 6316  unsigned long __cil_tmp10 ;
 6317  unsigned long __cil_tmp11 ;
 6318  unsigned long __cil_tmp12 ;
 6319  acpi_handle __cil_tmp13 ;
 6320  unsigned long __cil_tmp14 ;
 6321  unsigned long __cil_tmp15 ;
 6322  unsigned long __cil_tmp16 ;
 6323  unsigned long __cil_tmp17 ;
 6324  u32 __cil_tmp18 ;
 6325  unsigned long __cil_tmp19 ;
 6326  unsigned long __cil_tmp20 ;
 6327  unsigned long __cil_tmp21 ;
 6328  u32 __cil_tmp22 ;
 6329  u64 __cil_tmp23 ;
 6330  void const   *__cil_tmp24 ;
 6331  void const   *__cil_tmp25 ;
 6332  unsigned long __cil_tmp26 ;
 6333  unsigned long __cil_tmp27 ;
 6334  unsigned long __cil_tmp28 ;
 6335  u8 *__cil_tmp29 ;
 6336  u32 __cil_tmp30 ;
 6337  unsigned long __cil_tmp31 ;
 6338  unsigned long __cil_tmp32 ;
 6339  u32 __cil_tmp33 ;
 6340  void const   *__cil_tmp34 ;
 6341
 6342  {
 6343#line 675
 6344  data = (struct atk_data *)p;
 6345#line 678
 6346  err = 0;
 6347  {
 6348#line 680
 6349  __cil_tmp9 = (acpi_handle )0;
 6350#line 680
 6351  __cil_tmp10 = (unsigned long )__cil_tmp9;
 6352#line 680
 6353  __cil_tmp11 = (unsigned