Showing error 180

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-char-ipmi-ipmi_watchdog.ko-safe.cil.out.i.pp.cil.c
Line in file: 9995
Project: SV-COMP 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC


Source:

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