Showing error 119

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-video-aty-aty128fb.ko_safe.cil.out.i.pp.cil.c
Line in file: 12495
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

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