Showing error 1277

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


Source:

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