Showing error 179

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