/* Generated by Frama-C */

#line 19  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/int-ll64.h"
typedef signed char __s8;

#line 20  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/int-ll64.h"
typedef unsigned char __u8;

#line 22  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/int-ll64.h"
typedef short __s16;

#line 23  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/int-ll64.h"
typedef unsigned short __u16;

#line 25  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/int-ll64.h"
typedef int __s32;

#line 26  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/int-ll64.h"
typedef unsigned int __u32;

#line 30  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/int-ll64.h"
typedef unsigned long long __u64;

#line 16  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/asm-generic/int-ll64.h"
typedef unsigned char u8;

#line 18  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/asm-generic/int-ll64.h"
typedef short s16;

#line 19  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/asm-generic/int-ll64.h"
typedef unsigned short u16;

#line 21  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/asm-generic/int-ll64.h"
typedef int s32;

#line 22  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/asm-generic/int-ll64.h"
typedef unsigned int u32;

#line 24  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/asm-generic/int-ll64.h"
typedef long long s64;

#line 25  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/asm-generic/int-ll64.h"
typedef unsigned long long u64;

#line 14  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/posix_types.h"
typedef long __kernel_long_t;

#line 15  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/posix_types.h"
typedef unsigned long __kernel_ulong_t;

#line 27  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/posix_types.h"
typedef int __kernel_pid_t;

#line 48  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/posix_types.h"
typedef unsigned int __kernel_uid32_t;

#line 49  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/posix_types.h"
typedef unsigned int __kernel_gid32_t;

#line 71  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/posix_types.h"
typedef __kernel_ulong_t __kernel_size_t;

#line 72  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/posix_types.h"
typedef __kernel_long_t __kernel_ssize_t;

#line 87  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/posix_types.h"
typedef long long __kernel_loff_t;

#line 88  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/posix_types.h"
typedef __kernel_long_t __kernel_time_t;

#line 89  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/posix_types.h"
typedef __kernel_long_t __kernel_clock_t;

#line 90  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/posix_types.h"
typedef int __kernel_timer_t;

#line 91  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/posix_types.h"
typedef int __kernel_clockid_t;

#line 32  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/linux/types.h"
typedef __u16 __le16;

#line 12  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/types.h"
typedef __u32 __kernel_dev_t;

#line 15  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/types.h"
typedef __kernel_dev_t dev_t;

#line 18  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/types.h"
typedef unsigned short umode_t;

#line 21  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/types.h"
typedef __kernel_pid_t pid_t;

#line 26  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/types.h"
typedef __kernel_clockid_t clockid_t;

#line 29  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/types.h"
typedef _Bool bool;

#line 31  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/types.h"
typedef __kernel_uid32_t uid_t;

#line 32  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/types.h"
typedef __kernel_gid32_t gid_t;

#line 45  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/types.h"
typedef __kernel_loff_t loff_t;

#line 54  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/types.h"
typedef __kernel_size_t size_t;

#line 59  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/types.h"
typedef __kernel_ssize_t ssize_t;

#line 69  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/types.h"
typedef __kernel_time_t time_t;

#line 102  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/types.h"
typedef __s32 int32_t;

#line 108  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/types.h"
typedef __u32 uint32_t;

#line 133  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/types.h"
typedef unsigned long sector_t;

#line 134  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/types.h"
typedef unsigned long blkcnt_t;

#line 157  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/types.h"
typedef unsigned int gfp_t;

#line 158  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/types.h"
typedef unsigned int fmode_t;

#line 159  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/types.h"
typedef unsigned int oom_flags_t;

#line 177  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/types.h"
struct __anonstruct_atomic_t_6 {
   int counter ;
};

#line 177  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/types.h"
typedef struct __anonstruct_atomic_t_6 atomic_t;

#line 182  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/types.h"
struct __anonstruct_atomic64_t_7 {
   long counter ;
};

#line 182  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/types.h"
typedef struct __anonstruct_atomic64_t_7 atomic64_t;

#line 183  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/types.h"
struct list_head {
   struct list_head *next ;
   struct list_head *prev ;
};

#line 188 
struct hlist_node;

#line 188  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/types.h"
struct hlist_head {
   struct hlist_node *first ;
};

#line 192  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/types.h"
struct hlist_node {
   struct hlist_node *next ;
   struct hlist_node **pprev ;
};

#line 203  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/types.h"
struct callback_head {
   struct callback_head *next ;
   void (*func)(struct callback_head *) ;
};

#line 14  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/35/vtg/ext-modules/linux/usb/register/register.ko/linux:usb:register/weaver/.tmp_register.c.aux"
struct device;

#line 23  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/linux/sysinfo.h"
struct kernel_symbol {
   unsigned long value ;
   char const *name ;
};

#line 33  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/export.h"
struct module;

#line 65  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/page_types.h"
struct pt_regs {
   unsigned long r15 ;
   unsigned long r14 ;
   unsigned long r13 ;
   unsigned long r12 ;
   unsigned long bp ;
   unsigned long bx ;
   unsigned long r11 ;
   unsigned long r10 ;
   unsigned long r9 ;
   unsigned long r8 ;
   unsigned long ax ;
   unsigned long cx ;
   unsigned long dx ;
   unsigned long si ;
   unsigned long di ;
   unsigned long orig_ax ;
   unsigned long ip ;
   unsigned long cs ;
   unsigned long flags ;
   unsigned long sp ;
   unsigned long ss ;
};

#line 59  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/ptrace.h"
struct __anonstruct_9 {
   unsigned int a ;
   unsigned int b ;
};

#line 59  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/ptrace.h"
struct __anonstruct_10 {
   u16 limit0 ;
   u16 base0 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(8))) base1 : 8 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(4))) type : 4 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) s : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(2))) dpl : 2 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) p : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(4))) limit : 4 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) avl : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) l : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) d : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) g : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(8))) base2 : 8 ;
};

#line 59  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/ptrace.h"
union __anonunion_8 {
   struct __anonstruct_9 __anonCompField___anonunion_8_4 ;
   struct __anonstruct_10 __anonCompField___anonunion_8_5 ;
};

#line 59  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/ptrace.h"
struct desc_struct {
   union __anonunion_8 __anonCompField_desc_struct_6 ;
};

#line 15  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/pgtable_64_types.h"
typedef unsigned long pgdval_t;

#line 16  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/pgtable_64_types.h"
typedef unsigned long pgprotval_t;

#line 20  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/pgtable_64_types.h"
struct pgprot {
   pgprotval_t pgprot ;
};

#line 243  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/pgtable_types.h"
typedef struct pgprot pgprot_t;

#line 245  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/pgtable_types.h"
struct __anonstruct_pgd_t_12 {
   pgdval_t pgd ;
};

#line 245  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/pgtable_types.h"
typedef struct __anonstruct_pgd_t_12 pgd_t;

#line 333 
struct page;

#line 333  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/pgtable_types.h"
typedef struct page *pgtable_t;

#line 341 
struct file;

#line 354 
struct seq_file;

#line 387 
struct thread_struct;

#line 389 
struct mm_struct;

#line 390 
struct task_struct;

#line 391 
struct cpumask;

#line 327  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/paravirt_types.h"
struct arch_spinlock;

#line 18  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/spinlock_types.h"
typedef u16 __ticket_t;

#line 19  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/spinlock_types.h"
typedef u32 __ticketpair_t;

#line 20  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/spinlock_types.h"
struct __raw_tickets {
   __ticket_t head ;
   __ticket_t tail ;
};

#line 32  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/spinlock_types.h"
union __anonunion_15 {
   __ticketpair_t head_tail ;
   struct __raw_tickets tickets ;
};

#line 32  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/spinlock_types.h"
struct arch_spinlock {
   union __anonunion_15 __anonCompField_arch_spinlock_7 ;
};

#line 33  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/spinlock_types.h"
typedef struct arch_spinlock arch_spinlock_t;

#line 33  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/rwlock.h"
struct __anonstruct_17 {
   u32 read ;
   s32 write ;
};

#line 33  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/rwlock.h"
union __anonunion_arch_rwlock_t_16 {
   s64 lock ;
   struct __anonstruct_17 __anonCompField___anonunion_arch_rwlock_t_16_8 ;
};

#line 33  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/rwlock.h"
typedef union __anonunion_arch_rwlock_t_16 arch_rwlock_t;

#line 142  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/init.h"
typedef void (*ctor_fn_t)(void);

#line 376  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/printk.h"
struct file_operations;

#line 388 
struct completion;

#line 416  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/kernel.h"
struct pid;

#line 527  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/percpu.h"
struct bug_entry {
   int bug_addr_disp ;
   int file_disp ;
   unsigned short line ;
   unsigned short flags ;
};

#line 102  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/bug.h"
struct timespec;

#line 127  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/uapi/asm/vm86.h"
struct kernel_vm86_regs {
   struct pt_regs pt ;
   unsigned short es ;
   unsigned short __esh ;
   unsigned short ds ;
   unsigned short __dsh ;
   unsigned short fs ;
   unsigned short __fsh ;
   unsigned short gs ;
   unsigned short __gsh ;
};

#line 79  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/vm86.h"
union __anonunion_22 {
   struct pt_regs *regs ;
   struct kernel_vm86_regs *vm86 ;
};

#line 79  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/vm86.h"
struct math_emu_info {
   long ___orig_eip ;
   union __anonunion_22 __anonCompField_math_emu_info_10 ;
};

#line 306  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/bitmap.h"
struct cpumask {
   unsigned long bits[128U] ;
};

#line 14  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/cpumask.h"
typedef struct cpumask cpumask_t;

#line 663  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/cpumask.h"
typedef struct cpumask *cpumask_var_t;

#line 195  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/paravirt.h"
struct static_key;

#line 162  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/processor.h"
struct seq_operations;

#line 294  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/processor.h"
struct i387_fsave_struct {
   u32 cwd ;
   u32 swd ;
   u32 twd ;
   u32 fip ;
   u32 fcs ;
   u32 foo ;
   u32 fos ;
   u32 st_space[20U] ;
   u32 status ;
};

#line 312  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/processor.h"
struct __anonstruct_27 {
   u64 rip ;
   u64 rdp ;
};

#line 312  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/processor.h"
struct __anonstruct_28 {
   u32 fip ;
   u32 fcs ;
   u32 foo ;
   u32 fos ;
};

#line 312  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/processor.h"
union __anonunion_26 {
   struct __anonstruct_27 __anonCompField___anonunion_26_14 ;
   struct __anonstruct_28 __anonCompField___anonunion_26_15 ;
};

#line 312  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/processor.h"
union __anonunion_29 {
   u32 padding1[12U] ;
   u32 sw_reserved[12U] ;
};

#line 312  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/processor.h"
struct i387_fxsave_struct {
   u16 cwd ;
   u16 swd ;
   u16 twd ;
   u16 fop ;
   union __anonunion_26 __anonCompField_i387_fxsave_struct_16 ;
   u32 mxcsr ;
   u32 mxcsr_mask ;
   u32 st_space[32U] ;
   u32 xmm_space[64U] ;
   u32 padding[12U] ;
   union __anonunion_29 __anonCompField_i387_fxsave_struct_17 ;
};

#line 346  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/processor.h"
struct i387_soft_struct {
   u32 cwd ;
   u32 swd ;
   u32 twd ;
   u32 fip ;
   u32 fcs ;
   u32 foo ;
   u32 fos ;
   u32 st_space[20U] ;
   u8 ftop ;
   u8 changed ;
   u8 lookahead ;
   u8 no_update ;
   u8 rm ;
   u8 alimit ;
   struct math_emu_info *info ;
   u32 entry_eip ;
};

#line 367  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/processor.h"
struct ymmh_struct {
   u32 ymmh_space[64U] ;
};

#line 372  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/processor.h"
struct lwp_struct {
   u8 reserved[128U] ;
};

#line 377  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/processor.h"
struct bndregs_struct {
   u64 bndregs[8U] ;
};

#line 381  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/processor.h"
struct bndcsr_struct {
   u64 cfg_reg_u ;
   u64 status_reg ;
};

#line 386  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/processor.h"
struct xsave_hdr_struct {
   u64 xstate_bv ;
   u64 reserved1[2U] ;
   u64 reserved2[5U] ;
};

#line 392  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/processor.h"
struct xsave_struct {
   struct i387_fxsave_struct i387 ;
   struct xsave_hdr_struct xsave_hdr ;
   struct ymmh_struct ymmh ;
   struct lwp_struct lwp ;
   struct bndregs_struct bndregs ;
   struct bndcsr_struct bndcsr ;
};

#line 401  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/processor.h"
union thread_xstate {
   struct i387_fsave_struct fsave ;
   struct i387_fxsave_struct fxsave ;
   struct i387_soft_struct soft ;
   struct xsave_struct xsave ;
};

#line 409  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/processor.h"
struct fpu {
   unsigned int last_cpu ;
   unsigned int has_fpu ;
   union thread_xstate *state ;
};

#line 457 
struct perf_event;

#line 458  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/processor.h"
struct thread_struct {
   struct desc_struct tls_array[3U] ;
   unsigned long sp0 ;
   unsigned long sp ;
   unsigned long usersp ;
   unsigned short es ;
   unsigned short ds ;
   unsigned short fsindex ;
   unsigned short gsindex ;
   unsigned long fs ;
   unsigned long gs ;
   struct perf_event *ptrace_bps[4U] ;
   unsigned long debugreg6 ;
   unsigned long ptrace_dr7 ;
   unsigned long cr2 ;
   unsigned long trap_nr ;
   unsigned long error_code ;
   struct fpu fpu ;
   unsigned long *io_bitmap_ptr ;
   unsigned long iopl ;
   unsigned int io_bitmap_max ;
   unsigned char fpu_counter ;
};

#line 23  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/asm-generic/atomic-long.h"
typedef atomic64_t atomic_long_t;

#line 152  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/barrier.h"
struct lockdep_map;

#line 55  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/debug_locks.h"
struct stack_trace {
   unsigned int nr_entries ;
   unsigned int max_entries ;
   unsigned long *entries ;
   int skip ;
};

#line 26  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/stacktrace.h"
struct lockdep_subclass_key {
   char __one_byte ;
};

#line 53  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/lockdep.h"
struct lock_class_key {
   struct lockdep_subclass_key subkeys[8U] ;
};

#line 59  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/lockdep.h"
struct lock_class {
   struct list_head hash_entry ;
   struct list_head lock_entry ;
   struct lockdep_subclass_key *key ;
   unsigned int subclass ;
   unsigned int dep_gen_id ;
   unsigned long usage_mask ;
   struct stack_trace usage_traces[13U] ;
   struct list_head locks_after ;
   struct list_head locks_before ;
   unsigned int version ;
   unsigned long ops ;
   char const *name ;
   int name_version ;
   unsigned long contention_point[4U] ;
   unsigned long contending_point[4U] ;
};

#line 144  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/lockdep.h"
struct lockdep_map {
   struct lock_class_key *key ;
   struct lock_class *class_cache[2U] ;
   char const *name ;
   int cpu ;
   unsigned long ip ;
};

#line 205  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/lockdep.h"
struct held_lock {
   u64 prev_chain_key ;
   unsigned long acquire_ip ;
   struct lockdep_map *instance ;
   struct lockdep_map *nest_lock ;
   u64 waittime_stamp ;
   u64 holdtime_stamp ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(13))) class_idx : 13 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(2))) irq_context : 2 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) trylock : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(2))) read : 2 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(2))) check : 2 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) hardirqs_off : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(11))) references : 11 ;
};

#line 537  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/lockdep.h"
struct raw_spinlock {
   arch_spinlock_t raw_lock ;
   unsigned int magic ;
   unsigned int owner_cpu ;
   void *owner ;
   struct lockdep_map dep_map ;
};

#line 32  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/spinlock_types.h"
typedef struct raw_spinlock raw_spinlock_t;

#line 33  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/spinlock_types.h"
struct __anonstruct_33 {
   u8 __padding[24U] ;
   struct lockdep_map dep_map ;
};

#line 33  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/spinlock_types.h"
union __anonunion_32 {
   struct raw_spinlock rlock ;
   struct __anonstruct_33 __anonCompField___anonunion_32_19 ;
};

#line 33  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/spinlock_types.h"
struct spinlock {
   union __anonunion_32 __anonCompField_spinlock_20 ;
};

#line 76  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/spinlock_types.h"
typedef struct spinlock spinlock_t;

#line 23  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/rwlock_types.h"
struct __anonstruct_rwlock_t_34 {
   arch_rwlock_t raw_lock ;
   unsigned int magic ;
   unsigned int owner_cpu ;
   void *owner ;
   struct lockdep_map dep_map ;
};

#line 23  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/rwlock_types.h"
typedef struct __anonstruct_rwlock_t_34 rwlock_t;

#line 54  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/jump_label.h"
struct jump_entry;

#line 54 
struct static_key_mod;

#line 54  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/jump_label.h"
struct static_key {
   atomic_t enabled ;
   struct jump_entry *entries ;
   struct static_key_mod *next ;
};

#line 36  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/jump_label.h"
typedef u64 jump_label_t;

#line 37  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/jump_label.h"
struct jump_entry {
   jump_label_t code ;
   jump_label_t target ;
   jump_label_t key ;
};

#line 412  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/spinlock.h"
struct seqcount {
   unsigned int sequence ;
   struct lockdep_map dep_map ;
};

#line 51  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/seqlock.h"
typedef struct seqcount seqcount_t;

#line 433  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/seqlock.h"
struct timespec {
   __kernel_time_t tv_sec ;
   long tv_nsec ;
};

#line 83  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/highuid.h"
struct user_namespace;

#line 22  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/uidgid.h"
struct __anonstruct_kuid_t_36 {
   uid_t val ;
};

#line 22  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/uidgid.h"
typedef struct __anonstruct_kuid_t_36 kuid_t;

#line 27  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/uidgid.h"
struct __anonstruct_kgid_t_37 {
   gid_t val ;
};

#line 27  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/uidgid.h"
typedef struct __anonstruct_kgid_t_37 kgid_t;

#line 127  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/uidgid.h"
struct kstat {
   u64 ino ;
   dev_t dev ;
   umode_t mode ;
   unsigned int nlink ;
   kuid_t uid ;
   kgid_t gid ;
   dev_t rdev ;
   loff_t size ;
   struct timespec atime ;
   struct timespec mtime ;
   struct timespec ctime ;
   unsigned long blksize ;
   unsigned long long blocks ;
};

#line 34  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/wait.h"
struct __wait_queue_head {
   spinlock_t lock ;
   struct list_head task_list ;
};

#line 39  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/wait.h"
typedef struct __wait_queue_head wait_queue_head_t;

#line 98  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/nodemask.h"
struct __anonstruct_nodemask_t_38 {
   unsigned long bits[16U] ;
};

#line 98  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/nodemask.h"
typedef struct __anonstruct_nodemask_t_38 nodemask_t;

#line 799  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/mmzone.h"
struct mutex {
   atomic_t count ;
   spinlock_t wait_lock ;
   struct list_head wait_list ;
   struct task_struct *owner ;
   char const *name ;
   void *magic ;
   struct lockdep_map dep_map ;
};

#line 67  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/mutex.h"
struct mutex_waiter {
   struct list_head list ;
   struct task_struct *task ;
   void *magic ;
};

#line 177 
struct rw_semaphore;

#line 178  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/mutex.h"
struct rw_semaphore {
   long count ;
   raw_spinlock_t wait_lock ;
   struct list_head wait_list ;
   struct lockdep_map dep_map ;
};

#line 155  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/rwsem.h"
struct completion {
   unsigned int done ;
   wait_queue_head_t wait ;
};

#line 323  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/jiffies.h"
union ktime {
   s64 tv64 ;
};

#line 59  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/ktime.h"
typedef union ktime ktime_t;

#line 388 
struct tvec_base;

#line 389  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/ktime.h"
struct timer_list {
   struct list_head entry ;
   unsigned long expires ;
   struct tvec_base *base ;
   void (*function)(unsigned long ) ;
   unsigned long data ;
   int slack ;
   int start_pid ;
   void *start_site ;
   char start_comm[16U] ;
   struct lockdep_map lockdep_map ;
};

#line 254  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/timer.h"
struct hrtimer;

#line 255 
enum hrtimer_restart;

#line 266 
struct workqueue_struct;

#line 267 
struct work_struct;

#line 54  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/workqueue.h"
struct work_struct {
   atomic_long_t data ;
   struct list_head entry ;
   void (*func)(struct work_struct *) ;
   struct lockdep_map lockdep_map ;
};

#line 107  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/workqueue.h"
struct delayed_work {
   struct work_struct work ;
   struct timer_list timer ;
   struct workqueue_struct *wq ;
   int cpu ;
};

#line 58  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/pm.h"
struct pm_message {
   int event ;
};

#line 64  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/pm.h"
typedef struct pm_message pm_message_t;

#line 65  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/pm.h"
struct dev_pm_ops {
   int (*prepare)(struct device *) ;
   void (*complete)(struct device *) ;
   int (*suspend)(struct device *) ;
   int (*resume)(struct device *) ;
   int (*freeze)(struct device *) ;
   int (*thaw)(struct device *) ;
   int (*poweroff)(struct device *) ;
   int (*restore)(struct device *) ;
   int (*suspend_late)(struct device *) ;
   int (*resume_early)(struct device *) ;
   int (*freeze_late)(struct device *) ;
   int (*thaw_early)(struct device *) ;
   int (*poweroff_late)(struct device *) ;
   int (*restore_early)(struct device *) ;
   int (*suspend_noirq)(struct device *) ;
   int (*resume_noirq)(struct device *) ;
   int (*freeze_noirq)(struct device *) ;
   int (*thaw_noirq)(struct device *) ;
   int (*poweroff_noirq)(struct device *) ;
   int (*restore_noirq)(struct device *) ;
   int (*runtime_suspend)(struct device *) ;
   int (*runtime_resume)(struct device *) ;
   int (*runtime_idle)(struct device *) ;
};

#line 301 
enum rpm_status {
    RPM_ACTIVE = 0,
    RPM_RESUMING = 1,
    RPM_SUSPENDED = 2,
    RPM_SUSPENDING = 3
};

#line 308 
enum rpm_request {
    RPM_REQ_NONE = 0,
    RPM_REQ_IDLE = 1,
    RPM_REQ_SUSPEND = 2,
    RPM_REQ_AUTOSUSPEND = 3,
    RPM_REQ_RESUME = 4
};

#line 316 
struct wakeup_source;

#line 527  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/pm.h"
struct pm_subsys_data {
   spinlock_t lock ;
   unsigned int refcount ;
   struct list_head clock_list ;
};

#line 534 
struct dev_pm_qos;

#line 534  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/pm.h"
struct dev_pm_info {
   pm_message_t power_state ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) can_wakeup : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) async_suspend : 1 ;
   bool __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) is_prepared : 1 ;
   bool __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) is_suspended : 1 ;
   bool __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) ignore_children : 1 ;
   bool __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) early_init : 1 ;
   spinlock_t lock ;
   struct list_head entry ;
   struct completion completion ;
   struct wakeup_source *wakeup ;
   bool __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) wakeup_path : 1 ;
   bool __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) syscore : 1 ;
   struct timer_list suspend_timer ;
   unsigned long timer_expires ;
   struct work_struct work ;
   wait_queue_head_t wait_queue ;
   atomic_t usage_count ;
   atomic_t child_count ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(3))) disable_depth : 3 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) idle_notification : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) request_pending : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) deferred_resume : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) run_wake : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) runtime_auto : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) no_callbacks : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) irq_safe : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) use_autosuspend : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) timer_autosuspends : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) memalloc_noio : 1 ;
   enum rpm_request request ;
   enum rpm_status runtime_status ;
   int runtime_error ;
   int autosuspend_delay ;
   unsigned long last_busy ;
   unsigned long active_jiffies ;
   unsigned long suspended_jiffies ;
   unsigned long accounting_timestamp ;
   struct pm_subsys_data *subsys_data ;
   struct dev_pm_qos *qos ;
};

#line 591  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/pm.h"
struct dev_pm_domain {
   struct dev_pm_ops ops ;
};

#line 22  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/mmu.h"
struct __anonstruct_mm_context_t_103 {
   void *ldt ;
   int size ;
   unsigned short ia32_compat ;
   struct mutex lock ;
   void *vdso ;
};

#line 22  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/mmu.h"
typedef struct __anonstruct_mm_context_t_103 mm_context_t;

#line 18  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/asm-generic/pci_iomap.h"
struct rb_node {
   unsigned long __rb_parent_color ;
   struct rb_node *rb_right ;
   struct rb_node *rb_left ;
};

#line 40  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/rbtree.h"
struct rb_root {
   struct rb_node *rb_node ;
};

#line 87 
struct vm_area_struct;

#line 341  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/clocksource.h"
struct device_node;

#line 1276  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/mmzone.h"
struct llist_node;

#line 64  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/llist.h"
struct llist_node {
   struct llist_node *next ;
};

#line 835  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/linux/sysctl.h"
struct nsproxy;

#line 37  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/kmod.h"
struct cred;

#line 15  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/linux/elf.h"
typedef __u64 Elf64_Addr;

#line 16  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/linux/elf.h"
typedef __u16 Elf64_Half;

#line 20  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/linux/elf.h"
typedef __u32 Elf64_Word;

#line 21  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/linux/elf.h"
typedef __u64 Elf64_Xword;

#line 190  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/linux/elf.h"
struct elf64_sym {
   Elf64_Word st_name ;
   unsigned char st_info ;
   unsigned char st_other ;
   Elf64_Half st_shndx ;
   Elf64_Addr st_value ;
   Elf64_Xword st_size ;
};

#line 198  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/linux/elf.h"
typedef struct elf64_sym Elf64_Sym;

#line 48  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/elf.h"
struct idr_layer {
   int prefix ;
   unsigned long bitmap[4U] ;
   struct idr_layer *ary[256U] ;
   int count ;
   int layer ;
   struct callback_head callback_head ;
};

#line 38  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/idr.h"
struct idr {
   struct idr_layer *hint ;
   struct idr_layer *top ;
   struct idr_layer *id_free ;
   int layers ;
   int id_free_cnt ;
   int cur ;
   spinlock_t lock ;
};

#line 197  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/idr.h"
struct ida_bitmap {
   long nr_busy ;
   unsigned long bitmap[15U] ;
};

#line 213  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/idr.h"
struct ida {
   struct idr idr ;
   struct ida_bitmap *free_bitmap ;
};

#line 245 
struct dentry;

#line 246 
struct iattr;

#line 247 
struct super_block;

#line 248 
struct file_system_type;

#line 249 
struct kernfs_open_node;

#line 250 
struct kernfs_iattrs;

#line 266 
struct kernfs_root;

#line 266  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/idr.h"
struct kernfs_elem_dir {
   unsigned long subdirs ;
   struct rb_root children ;
   struct kernfs_root *root ;
};

#line 62  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/kernfs.h"
struct kernfs_node;

#line 62  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/kernfs.h"
struct kernfs_elem_symlink {
   struct kernfs_node *target_kn ;
};

#line 66 
struct kernfs_ops;

#line 66  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/kernfs.h"
struct kernfs_elem_attr {
   struct kernfs_ops const *ops ;
   struct kernfs_open_node *open ;
   loff_t size ;
};

#line 72  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/kernfs.h"
union __anonunion_u_137 {
   struct completion *completion ;
   struct kernfs_node *removed_list ;
};

#line 72  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/kernfs.h"
union __anonunion_138 {
   struct kernfs_elem_dir dir ;
   struct kernfs_elem_symlink symlink ;
   struct kernfs_elem_attr attr ;
};

#line 72  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/kernfs.h"
struct kernfs_node {
   atomic_t count ;
   atomic_t active ;
   struct lockdep_map dep_map ;
   struct kernfs_node *parent ;
   char const *name ;
   struct rb_node rb ;
   union __anonunion_u_137 u ;
   void const *ns ;
   unsigned int hash ;
   union __anonunion_138 __anonCompField_kernfs_node_34 ;
   void *priv ;
   unsigned short flags ;
   umode_t mode ;
   unsigned int ino ;
   struct kernfs_iattrs *iattr ;
};

#line 114  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/kernfs.h"
struct kernfs_dir_ops {
   int (*mkdir)(struct kernfs_node *, char const *, umode_t ) ;
   int (*rmdir)(struct kernfs_node *) ;
   int (*rename)(struct kernfs_node *, struct kernfs_node *, char const *) ;
};

#line 127  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/kernfs.h"
struct kernfs_root {
   struct kernfs_node *kn ;
   struct ida ino_ida ;
   struct kernfs_dir_ops *dir_ops ;
};

#line 137 
struct vm_operations_struct;

#line 137  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/kernfs.h"
struct kernfs_open_file {
   struct kernfs_node *kn ;
   struct file *file ;
   struct mutex mutex ;
   int event ;
   struct list_head list ;
   bool mmapped ;
   struct vm_operations_struct const *vm_ops ;
};

#line 151  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/kernfs.h"
struct kernfs_ops {
   int (*seq_show)(struct seq_file *, void *) ;
   void *(*seq_start)(struct seq_file *, loff_t *) ;
   void *(*seq_next)(struct seq_file *, void *, loff_t *) ;
   void (*seq_stop)(struct seq_file *, void *) ;
   ssize_t (*read)(struct kernfs_open_file *, char *, size_t , loff_t ) ;
   ssize_t (*write)(struct kernfs_open_file *, char *, size_t , loff_t ) ;
   int (*mmap)(struct kernfs_open_file *, struct vm_area_struct *) ;
   struct lock_class_key lockdep_key ;
};

#line 376 
struct sock;

#line 377 
struct kobject;

#line 378 
enum kobj_ns_type {
    KOBJ_NS_TYPE_NONE = 0,
    KOBJ_NS_TYPE_NET = 1,
    KOBJ_NS_TYPES = 2
};

#line 384  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/kernfs.h"
struct kobj_ns_type_operations {
   enum kobj_ns_type type ;
   bool (*current_may_mount)(void) ;
   void *(*grab_current_ns)(void) ;
   void const *(*netlink_ns)(struct sock *) ;
   void const *(*initial_ns)(void) ;
   void (*drop_ns)(void *) ;
};

#line 59  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/kobject_ns.h"
struct bin_attribute;

#line 60  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/kobject_ns.h"
struct attribute {
   char const *name ;
   umode_t mode ;
   bool __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) ignore_lockdep : 1 ;
   struct lock_class_key *key ;
   struct lock_class_key skey ;
};

#line 37  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/sysfs.h"
struct attribute_group {
   char const *name ;
   umode_t (*is_visible)(struct kobject *, struct attribute *, int ) ;
   struct attribute **attrs ;
   struct bin_attribute **bin_attrs ;
};

#line 67  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/sysfs.h"
struct bin_attribute {
   struct attribute attr ;
   size_t size ;
   void *private ;
   ssize_t (*read)(struct file *, struct kobject *, struct bin_attribute *, char *, loff_t , size_t ) ;
   ssize_t (*write)(struct file *, struct kobject *, struct bin_attribute *, char *, loff_t , size_t ) ;
   int (*mmap)(struct file *, struct kobject *, struct bin_attribute *, struct vm_area_struct *) ;
};

#line 130  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/sysfs.h"
struct sysfs_ops {
   ssize_t (*show)(struct kobject *, struct attribute *, char *) ;
   ssize_t (*store)(struct kobject *, struct attribute *, char const *, size_t ) ;
};

#line 462  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/sysfs.h"
struct kref {
   atomic_t refcount ;
};

#line 50  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/kobject.h"
struct kset;

#line 50 
struct kobj_type;

#line 50  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/kobject.h"
struct kobject {
   char const *name ;
   struct list_head entry ;
   struct kobject *parent ;
   struct kset *kset ;
   struct kobj_type *ktype ;
   struct kernfs_node *sd ;
   struct kref kref ;
   struct delayed_work release ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) state_initialized : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) state_in_sysfs : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) state_add_uevent_sent : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) state_remove_uevent_sent : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) uevent_suppress : 1 ;
};

#line 112  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/kobject.h"
struct kobj_type {
   void (*release)(struct kobject *) ;
   struct sysfs_ops const *sysfs_ops ;
   struct attribute **default_attrs ;
   struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject *) ;
   void const *(*namespace)(struct kobject *) ;
};

#line 120  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/kobject.h"
struct kobj_uevent_env {
   char *envp[32U] ;
   int envp_idx ;
   char buf[2048U] ;
   int buflen ;
};

#line 127  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/kobject.h"
struct kset_uevent_ops {
   int (* const filter)(struct kset *, struct kobject *) ;
   char const *(* const name)(struct kset *, struct kobject *) ;
   int (* const uevent)(struct kset *, struct kobject *, struct kobj_uevent_env *) ;
};

#line 144  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/kobject.h"
struct kset {
   struct list_head list ;
   spinlock_t list_lock ;
   struct kobject kobj ;
   struct kset_uevent_ops const *uevent_ops ;
};

#line 219 
struct kernel_param;

#line 224  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/kobject.h"
struct kernel_param_ops {
   unsigned int flags ;
   int (*set)(char const *, struct kernel_param const *) ;
   int (*get)(char *, struct kernel_param const *) ;
   void (*free)(void *) ;
};

#line 58  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/moduleparam.h"
struct kparam_string;

#line 58 
struct kparam_array;

#line 58  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/moduleparam.h"
union __anonunion_139 {
   void *arg ;
   struct kparam_string const *str ;
   struct kparam_array const *arr ;
};

#line 58  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/moduleparam.h"
struct kernel_param {
   char const *name ;
   struct kernel_param_ops const *ops ;
   u16 perm ;
   s16 level ;
   union __anonunion_139 __anonCompField_kernel_param_35 ;
};

#line 70  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/moduleparam.h"
struct kparam_string {
   unsigned int maxlen ;
   char *string ;
};

#line 76  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/moduleparam.h"
struct kparam_array {
   unsigned int max ;
   unsigned int elemsize ;
   unsigned int *num ;
   struct kernel_param_ops const *ops ;
   void *elem ;
};

#line 463 
struct tracepoint;

#line 464  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/moduleparam.h"
struct tracepoint_func {
   void *func ;
   void *data ;
};

#line 29  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/tracepoint.h"
struct tracepoint {
   char const *name ;
   struct static_key key ;
   void (*regfunc)(void) ;
   void (*unregfunc)(void) ;
   struct tracepoint_func *funcs ;
};

#line 92  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/tracepoint.h"
struct mod_arch_specific {
   
};

#line 36  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/module.h"
struct module_param_attrs;

#line 36  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/module.h"
struct module_kobject {
   struct kobject kobj ;
   struct module *mod ;
   struct kobject *drivers_dir ;
   struct module_param_attrs *mp ;
   struct completion *kobj_completion ;
};

#line 46  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/module.h"
struct module_attribute {
   struct attribute attr ;
   ssize_t (*show)(struct module_attribute *, struct module_kobject *, char *) ;
   ssize_t (*store)(struct module_attribute *, struct module_kobject *, char const *, size_t ) ;
   void (*setup)(struct module *, char const *) ;
   int (*test)(struct module *) ;
   void (*free)(struct module *) ;
};

#line 72 
struct exception_table_entry;

#line 208 
enum module_state {
    MODULE_STATE_LIVE = 0,
    MODULE_STATE_COMING = 1,
    MODULE_STATE_GOING = 2,
    MODULE_STATE_UNFORMED = 3
};

#line 215  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/module.h"
struct module_ref {
   unsigned long incs ;
   unsigned long decs ;
};

#line 229 
struct module_sect_attrs;

#line 229 
struct module_notes_attrs;

#line 229 
struct ftrace_event_call;

#line 229  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/module.h"
struct module {
   enum module_state state ;
   struct list_head list ;
   char name[56U] ;
   struct module_kobject mkobj ;
   struct module_attribute *modinfo_attrs ;
   char const *version ;
   char const *srcversion ;
   struct kobject *holders_dir ;
   struct kernel_symbol const *syms ;
   unsigned long const *crcs ;
   unsigned int num_syms ;
   struct kernel_param *kp ;
   unsigned int num_kp ;
   unsigned int num_gpl_syms ;
   struct kernel_symbol const *gpl_syms ;
   unsigned long const *gpl_crcs ;
   struct kernel_symbol const *unused_syms ;
   unsigned long const *unused_crcs ;
   unsigned int num_unused_syms ;
   unsigned int num_unused_gpl_syms ;
   struct kernel_symbol const *unused_gpl_syms ;
   unsigned long const *unused_gpl_crcs ;
   bool sig_ok ;
   struct kernel_symbol const *gpl_future_syms ;
   unsigned long const *gpl_future_crcs ;
   unsigned int num_gpl_future_syms ;
   unsigned int num_exentries ;
   struct exception_table_entry *extable ;
   int (*init)(void) ;
   void *module_init ;
   void *module_core ;
   unsigned int init_size ;
   unsigned int core_size ;
   unsigned int init_text_size ;
   unsigned int core_text_size ;
   unsigned int init_ro_size ;
   unsigned int core_ro_size ;
   struct mod_arch_specific arch ;
   unsigned int taints ;
   unsigned int num_bugs ;
   struct list_head bug_list ;
   struct bug_entry *bug_table ;
   Elf64_Sym *symtab ;
   Elf64_Sym *core_symtab ;
   unsigned int num_symtab ;
   unsigned int core_num_syms ;
   char *strtab ;
   char *core_strtab ;
   struct module_sect_attrs *sect_attrs ;
   struct module_notes_attrs *notes_attrs ;
   char *args ;
   void *percpu ;
   unsigned int percpu_size ;
   unsigned int num_tracepoints ;
   struct tracepoint * const *tracepoints_ptrs ;
   struct jump_entry *jump_entries ;
   unsigned int num_jump_entries ;
   unsigned int num_trace_bprintk_fmt ;
   char const **trace_bprintk_fmt_start ;
   struct ftrace_event_call **trace_events ;
   unsigned int num_trace_events ;
   unsigned int num_ftrace_callsites ;
   unsigned long *ftrace_callsites ;
   struct list_head source_list ;
   struct list_head target_list ;
   void (*exit)(void) ;
   struct module_ref *refptr ;
   ctor_fn_t (**ctors)(void) ;
   unsigned int num_ctors ;
};

#line 13  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/mod_devicetable.h"
typedef unsigned long kernel_ulong_t;

#line 39  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/mod_devicetable.h"
struct usb_device_id {
   __u16 match_flags ;
   __u16 idVendor ;
   __u16 idProduct ;
   __u16 bcdDevice_lo ;
   __u16 bcdDevice_hi ;
   __u8 bDeviceClass ;
   __u8 bDeviceSubClass ;
   __u8 bDeviceProtocol ;
   __u8 bInterfaceClass ;
   __u8 bInterfaceSubClass ;
   __u8 bInterfaceProtocol ;
   __u8 bInterfaceNumber ;
   kernel_ulong_t driver_info ;
};

#line 186  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/mod_devicetable.h"
struct acpi_device_id {
   __u8 id[9U] ;
   kernel_ulong_t driver_data ;
};

#line 219  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/mod_devicetable.h"
struct of_device_id {
   char name[32U] ;
   char type[32U] ;
   char compatible[128U] ;
   void const *data ;
};

#line 343  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/linux/usb/ch9.h"
struct usb_interface_descriptor {
   __u8 bLength ;
   __u8 bDescriptorType ;
   __u8 bInterfaceNumber ;
   __u8 bAlternateSetting ;
   __u8 bNumEndpoints ;
   __u8 bInterfaceClass ;
   __u8 bInterfaceSubClass ;
   __u8 bInterfaceProtocol ;
   __u8 iInterface ;
};

#line 363  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/linux/usb/ch9.h"
struct usb_endpoint_descriptor {
   __u8 bLength ;
   __u8 bDescriptorType ;
   __u8 bEndpointAddress ;
   __u8 bmAttributes ;
   __le16 wMaxPacketSize ;
   __u8 bInterval ;
   __u8 bRefresh ;
   __u8 bSynchAddress ;
};

#line 613  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/linux/usb/ch9.h"
struct usb_ss_ep_comp_descriptor {
   __u8 bLength ;
   __u8 bDescriptorType ;
   __u8 bMaxBurst ;
   __u8 bmAttributes ;
   __le16 wBytesPerInterval ;
};

#line 692  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/linux/usb/ch9.h"
struct usb_interface_assoc_descriptor {
   __u8 bLength ;
   __u8 bDescriptorType ;
   __u8 bFirstInterface ;
   __u8 bInterfaceCount ;
   __u8 bFunctionClass ;
   __u8 bFunctionSubClass ;
   __u8 bFunctionProtocol ;
   __u8 iFunction ;
};

#line 62  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/uaccess.h"
struct exception_table_entry {
   int insn ;
   int fixup ;
};

#line 60  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/hardirq.h"
struct timerqueue_node {
   struct rb_node node ;
   ktime_t expires ;
};

#line 12  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/timerqueue.h"
struct timerqueue_head {
   struct rb_root head ;
   struct timerqueue_node *next ;
};

#line 50 
struct hrtimer_clock_base;

#line 51 
struct hrtimer_cpu_base;

#line 60 
enum hrtimer_restart {
    HRTIMER_NORESTART = 0,
    HRTIMER_RESTART = 1
};

#line 65  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/timerqueue.h"
struct hrtimer {
   struct timerqueue_node node ;
   ktime_t _softexpires ;
   enum hrtimer_restart (*function)(struct hrtimer *) ;
   struct hrtimer_clock_base *base ;
   unsigned long state ;
   int start_pid ;
   void *start_site ;
   char start_comm[16U] ;
};

#line 132  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/hrtimer.h"
struct hrtimer_clock_base {
   struct hrtimer_cpu_base *cpu_base ;
   int index ;
   clockid_t clockid ;
   struct timerqueue_head active ;
   ktime_t resolution ;
   ktime_t (*get_time)(void) ;
   ktime_t softirq_time ;
   ktime_t offset ;
};

#line 163  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/hrtimer.h"
struct hrtimer_cpu_base {
   raw_spinlock_t lock ;
   unsigned int active_bases ;
   unsigned int clock_was_set ;
   ktime_t expires_next ;
   int hres_active ;
   int hang_detected ;
   unsigned long nr_events ;
   unsigned long nr_retries ;
   unsigned long nr_hangs ;
   ktime_t max_hang_time ;
   struct hrtimer_clock_base clock_base[4U] ;
};

#line 618  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/interrupt.h"
struct klist_node;

#line 37  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/klist.h"
struct klist_node {
   void *n_klist ;
   struct list_head n_node ;
   struct kref n_ref ;
};

#line 67 
struct path;

#line 68 
struct inode;

#line 69  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/klist.h"
struct seq_file {
   char *buf ;
   size_t size ;
   size_t from ;
   size_t count ;
   size_t pad_until ;
   loff_t index ;
   loff_t read_pos ;
   u64 version ;
   struct mutex lock ;
   struct seq_operations const *op ;
   int poll_event ;
   struct user_namespace *user_ns ;
   void *private ;
};

#line 35  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/seq_file.h"
struct seq_operations {
   void *(*start)(struct seq_file *, loff_t *) ;
   void (*stop)(struct seq_file *, void *) ;
   void *(*next)(struct seq_file *, void *, loff_t *) ;
   int (*show)(struct seq_file *, void *) ;
};

#line 196 
struct pinctrl;

#line 197 
struct pinctrl_state;

#line 194  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/pinctrl/consumer.h"
struct dev_pin_info {
   struct pinctrl *p ;
   struct pinctrl_state *default_state ;
   struct pinctrl_state *sleep_state ;
   struct pinctrl_state *idle_state ;
};

#line 42  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/ratelimit.h"
struct dma_map_ops;

#line 42  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/ratelimit.h"
struct dev_archdata {
   struct dma_map_ops *dma_ops ;
   void *iommu ;
};

#line 15  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/device.h"
struct device_driver;

#line 16 
struct driver_private;

#line 17 
struct class;

#line 18 
struct subsys_private;

#line 19 
struct bus_type;

#line 20 
struct iommu_ops;

#line 21 
struct iommu_group;

#line 60  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/device.h"
struct device_attribute;

#line 60  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/device.h"
struct bus_type {
   char const *name ;
   char const *dev_name ;
   struct device *dev_root ;
   struct device_attribute *dev_attrs ;
   struct attribute_group const **bus_groups ;
   struct attribute_group const **dev_groups ;
   struct attribute_group const **drv_groups ;
   int (*match)(struct device *, struct device_driver *) ;
   int (*uevent)(struct device *, struct kobj_uevent_env *) ;
   int (*probe)(struct device *) ;
   int (*remove)(struct device *) ;
   void (*shutdown)(struct device *) ;
   int (*online)(struct device *) ;
   int (*offline)(struct device *) ;
   int (*suspend)(struct device *, pm_message_t ) ;
   int (*resume)(struct device *) ;
   struct dev_pm_ops const *pm ;
   struct iommu_ops *iommu_ops ;
   struct subsys_private *p ;
   struct lock_class_key lock_key ;
};

#line 138 
struct device_type;

#line 195  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/device.h"
struct device_driver {
   char const *name ;
   struct bus_type *bus ;
   struct module *owner ;
   char const *mod_name ;
   bool suppress_bind_attrs ;
   struct of_device_id const *of_match_table ;
   struct acpi_device_id const *acpi_match_table ;
   int (*probe)(struct device *) ;
   int (*remove)(struct device *) ;
   void (*shutdown)(struct device *) ;
   int (*suspend)(struct device *, pm_message_t ) ;
   int (*resume)(struct device *) ;
   struct attribute_group const **groups ;
   struct dev_pm_ops const *pm ;
   struct driver_private *p ;
};

#line 321 
struct class_attribute;

#line 321  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/device.h"
struct class {
   char const *name ;
   struct module *owner ;
   struct class_attribute *class_attrs ;
   struct attribute_group const **dev_groups ;
   struct kobject *dev_kobj ;
   int (*dev_uevent)(struct device *, struct kobj_uevent_env *) ;
   char *(*devnode)(struct device *, umode_t *) ;
   void (*class_release)(struct class *) ;
   void (*dev_release)(struct device *) ;
   int (*suspend)(struct device *, pm_message_t ) ;
   int (*resume)(struct device *) ;
   struct kobj_ns_type_operations const *ns_type ;
   void const *(*namespace)(struct device *) ;
   struct dev_pm_ops const *pm ;
   struct subsys_private *p ;
};

#line 414  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/device.h"
struct class_attribute {
   struct attribute attr ;
   ssize_t (*show)(struct class *, struct class_attribute *, char *) ;
   ssize_t (*store)(struct class *, struct class_attribute *, char const *, size_t ) ;
};

#line 482  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/device.h"
struct device_type {
   char const *name ;
   struct attribute_group const **groups ;
   int (*uevent)(struct device *, struct kobj_uevent_env *) ;
   char *(*devnode)(struct device *, umode_t *, kuid_t *, kgid_t *) ;
   void (*release)(struct device *) ;
   struct dev_pm_ops const *pm ;
};

#line 510  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/device.h"
struct device_attribute {
   struct attribute attr ;
   ssize_t (*show)(struct device *, struct device_attribute *, char *) ;
   ssize_t (*store)(struct device *, struct device_attribute *, char const *, size_t ) ;
};

#line 637  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/device.h"
struct device_dma_parameters {
   unsigned int max_segment_size ;
   unsigned long segment_boundary_mask ;
};

#line 646 
struct acpi_device;

#line 647  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/device.h"
struct acpi_dev_node {
   struct acpi_device *companion ;
};

#line 653 
struct dma_coherent_mem;

#line 653  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/device.h"
struct device {
   struct device *parent ;
   struct device_private *p ;
   struct kobject kobj ;
   char const *init_name ;
   struct device_type const *type ;
   struct mutex mutex ;
   struct bus_type *bus ;
   struct device_driver *driver ;
   void *platform_data ;
   struct dev_pm_info power ;
   struct dev_pm_domain *pm_domain ;
   struct dev_pin_info *pins ;
   int numa_node ;
   u64 *dma_mask ;
   u64 coherent_dma_mask ;
   struct device_dma_parameters *dma_parms ;
   struct list_head dma_pools ;
   struct dma_coherent_mem *dma_mem ;
   struct dev_archdata archdata ;
   struct device_node *of_node ;
   struct acpi_dev_node acpi_node ;
   dev_t devt ;
   u32 id ;
   spinlock_t devres_lock ;
   struct list_head devres_head ;
   struct klist_node knode_class ;
   struct class *class ;
   struct attribute_group const **groups ;
   void (*release)(struct device *) ;
   struct iommu_group *iommu_group ;
   bool __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) offline_disabled : 1 ;
   bool __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) offline : 1 ;
};

#line 795  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/device.h"
struct wakeup_source {
   char const *name ;
   struct list_head entry ;
   spinlock_t lock ;
   struct timer_list timer ;
   unsigned long timer_expires ;
   ktime_t total_time ;
   ktime_t max_time ;
   ktime_t last_time ;
   ktime_t start_prevent_time ;
   ktime_t prevent_sleep_time ;
   unsigned long event_count ;
   unsigned long active_count ;
   unsigned long relax_count ;
   unsigned long expire_count ;
   unsigned long wakeup_count ;
   bool __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) active : 1 ;
   bool __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) autosleep_enabled : 1 ;
};

#line 93  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/bit_spinlock.h"
struct hlist_bl_node;

#line 93  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/bit_spinlock.h"
struct hlist_bl_head {
   struct hlist_bl_node *first ;
};

#line 36  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/list_bl.h"
struct hlist_bl_node {
   struct hlist_bl_node *next ;
   struct hlist_bl_node **pprev ;
};

#line 114  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/rculist_bl.h"
struct __anonstruct_146 {
   spinlock_t lock ;
   unsigned int count ;
};

#line 114  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/rculist_bl.h"
union __anonunion_145 {
   struct __anonstruct_146 __anonCompField___anonunion_145_37 ;
};

#line 114  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/rculist_bl.h"
struct lockref {
   union __anonunion_145 __anonCompField_lockref_38 ;
};

#line 49  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/lockref.h"
struct nameidata;

#line 50 
struct vfsmount;

#line 51  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/lockref.h"
struct __anonstruct_148 {
   u32 hash ;
   u32 len ;
};

#line 51  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/lockref.h"
union __anonunion_147 {
   struct __anonstruct_148 __anonCompField___anonunion_147_39 ;
   u64 hash_len ;
};

#line 51  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/lockref.h"
struct qstr {
   union __anonunion_147 __anonCompField_qstr_40 ;
   unsigned char const *name ;
};

#line 90  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/dcache.h"
struct dentry_operations;

#line 90  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/dcache.h"
union __anonunion_d_u_149 {
   struct list_head d_child ;
   struct callback_head d_rcu ;
};

#line 90  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/dcache.h"
struct dentry {
   unsigned int d_flags ;
   seqcount_t d_seq ;
   struct hlist_bl_node d_hash ;
   struct dentry *d_parent ;
   struct qstr d_name ;
   struct inode *d_inode ;
   unsigned char d_iname[32U] ;
   struct lockref d_lockref ;
   struct dentry_operations const *d_op ;
   struct super_block *d_sb ;
   unsigned long d_time ;
   void *d_fsdata ;
   struct list_head d_lru ;
   union __anonunion_d_u_149 d_u ;
   struct list_head d_subdirs ;
   struct hlist_node d_alias ;
};

#line 142  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/dcache.h"
struct dentry_operations {
   int (*d_revalidate)(struct dentry *, unsigned int ) ;
   int (*d_weak_revalidate)(struct dentry *, unsigned int ) ;
   int (*d_hash)(struct dentry const *, struct qstr *) ;
   int (*d_compare)(struct dentry const *, struct dentry const *, unsigned int , char const *, struct qstr const *) ;
   int (*d_delete)(struct dentry const *) ;
   void (*d_release)(struct dentry *) ;
   void (*d_prune)(struct dentry *) ;
   void (*d_iput)(struct dentry *, struct inode *) ;
   char *(*d_dname)(struct dentry *, char *, int ) ;
   struct vfsmount *(*d_automount)(struct path *) ;
   int (*d_manage)(struct dentry *, bool ) ;
};

#line 469  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/dcache.h"
struct path {
   struct vfsmount *mnt ;
   struct dentry *dentry ;
};

#line 26  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/path.h"
struct list_lru_node {
   spinlock_t lock ;
   struct list_head list ;
   long nr_items ;
};

#line 28  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/list_lru.h"
struct list_lru {
   struct list_lru_node *node ;
   nodemask_t active_nodes ;
};

#line 58  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/radix-tree.h"
struct radix_tree_node;

#line 58  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/radix-tree.h"
struct radix_tree_root {
   unsigned int height ;
   gfp_t gfp_mask ;
   struct radix_tree_node *rnode ;
};

#line 381 
enum pid_type {
    PIDTYPE_PID = 0,
    PIDTYPE_PGID = 1,
    PIDTYPE_SID = 2,
    PIDTYPE_MAX = 3
};

#line 388 
struct pid_namespace;

#line 388  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/radix-tree.h"
struct upid {
   int nr ;
   struct pid_namespace *ns ;
   struct hlist_node pid_chain ;
};

#line 56  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/pid.h"
struct pid {
   atomic_t count ;
   unsigned int level ;
   struct hlist_head tasks[3U] ;
   struct callback_head rcu ;
   struct upid numbers[1U] ;
};

#line 68  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/pid.h"
struct pid_link {
   struct hlist_node node ;
   struct pid *pid ;
};

#line 22  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/capability.h"
struct kernel_cap_struct {
   __u32 cap[2U] ;
};

#line 25  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/capability.h"
typedef struct kernel_cap_struct kernel_cap_t;

#line 45  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/semaphore.h"
struct fiemap_extent {
   __u64 fe_logical ;
   __u64 fe_physical ;
   __u64 fe_length ;
   __u64 fe_reserved64[2U] ;
   __u32 fe_flags ;
   __u32 fe_reserved[3U] ;
};

#line 38  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/linux/fiemap.h"
struct shrink_control {
   gfp_t gfp_mask ;
   unsigned long nr_to_scan ;
   nodemask_t nodes_to_scan ;
   int nid ;
};

#line 26  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/shrinker.h"
struct shrinker {
   unsigned long (*count_objects)(struct shrinker *, struct shrink_control *) ;
   unsigned long (*scan_objects)(struct shrinker *, struct shrink_control *) ;
   int seeks ;
   long batch ;
   unsigned long flags ;
   struct list_head list ;
   atomic_long_t *nr_deferred ;
};

#line 70 
enum migrate_mode {
    MIGRATE_ASYNC = 0,
    MIGRATE_SYNC_LIGHT = 1,
    MIGRATE_SYNC = 2
};

#line 30  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/percpu-rwsem.h"
struct block_device;

#line 31 
struct io_context;

#line 56  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/linux/fs.h"
struct export_operations;

#line 58 
struct iovec;

#line 59 
struct kiocb;

#line 60 
struct pipe_inode_info;

#line 61 
struct poll_table_struct;

#line 62 
struct kstatfs;

#line 63 
struct swap_info_struct;

#line 68  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/fs.h"
struct iattr {
   unsigned int ia_valid ;
   umode_t ia_mode ;
   kuid_t ia_uid ;
   kgid_t ia_gid ;
   loff_t ia_size ;
   struct timespec ia_atime ;
   struct timespec ia_mtime ;
   struct timespec ia_ctime ;
   struct file *ia_file ;
};

#line 246  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/fs.h"
struct percpu_counter {
   raw_spinlock_t lock ;
   s64 count ;
   struct list_head list ;
   s32 *counters ;
};

#line 176  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/percpu_counter.h"
struct fs_disk_quota {
   __s8 d_version ;
   __s8 d_flags ;
   __u16 d_fieldmask ;
   __u32 d_id ;
   __u64 d_blk_hardlimit ;
   __u64 d_blk_softlimit ;
   __u64 d_ino_hardlimit ;
   __u64 d_ino_softlimit ;
   __u64 d_bcount ;
   __u64 d_icount ;
   __s32 d_itimer ;
   __s32 d_btimer ;
   __u16 d_iwarns ;
   __u16 d_bwarns ;
   __s32 d_padding2 ;
   __u64 d_rtb_hardlimit ;
   __u64 d_rtb_softlimit ;
   __u64 d_rtbcount ;
   __s32 d_rtbtimer ;
   __u16 d_rtbwarns ;
   __s16 d_padding3 ;
   char d_padding4[8U] ;
};

#line 76  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/linux/dqblk_xfs.h"
struct fs_qfilestat {
   __u64 qfs_ino ;
   __u64 qfs_nblks ;
   __u32 qfs_nextents ;
};

#line 151  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/linux/dqblk_xfs.h"
typedef struct fs_qfilestat fs_qfilestat_t;

#line 152  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/linux/dqblk_xfs.h"
struct fs_quota_stat {
   __s8 qs_version ;
   __u16 qs_flags ;
   __s8 qs_pad ;
   fs_qfilestat_t qs_uquota ;
   fs_qfilestat_t qs_gquota ;
   __u32 qs_incoredqs ;
   __s32 qs_btimelimit ;
   __s32 qs_itimelimit ;
   __s32 qs_rtbtimelimit ;
   __u16 qs_bwarnlimit ;
   __u16 qs_iwarnlimit ;
};

#line 166  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/linux/dqblk_xfs.h"
struct fs_qfilestatv {
   __u64 qfs_ino ;
   __u64 qfs_nblks ;
   __u32 qfs_nextents ;
   __u32 qfs_pad ;
};

#line 196  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/linux/dqblk_xfs.h"
struct fs_quota_statv {
   __s8 qs_version ;
   __u8 qs_pad1 ;
   __u16 qs_flags ;
   __u32 qs_incoredqs ;
   struct fs_qfilestatv qs_uquota ;
   struct fs_qfilestatv qs_gquota ;
   struct fs_qfilestatv qs_pquota ;
   __s32 qs_btimelimit ;
   __s32 qs_itimelimit ;
   __s32 qs_rtbtimelimit ;
   __u16 qs_bwarnlimit ;
   __u16 qs_iwarnlimit ;
   __u64 qs_pad2[8U] ;
};

#line 212 
struct dquot;

#line 19  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/projid.h"
typedef __kernel_uid32_t projid_t;

#line 23  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/projid.h"
struct __anonstruct_kprojid_t_151 {
   projid_t val ;
};

#line 23  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/projid.h"
typedef struct __anonstruct_kprojid_t_151 kprojid_t;

#line 119  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/linux/quota.h"
struct if_dqinfo {
   __u64 dqi_bgrace ;
   __u64 dqi_igrace ;
   __u32 dqi_flags ;
   __u32 dqi_valid ;
};

#line 152 
enum quota_type {
    USRQUOTA = 0,
    GRPQUOTA = 1,
    PRJQUOTA = 2
};

#line 60  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/quota.h"
typedef long long qsize_t;

#line 61  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/quota.h"
union __anonunion_152 {
   kuid_t uid ;
   kgid_t gid ;
   kprojid_t projid ;
};

#line 61  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/quota.h"
struct kqid {
   union __anonunion_152 __anonCompField_kqid_41 ;
   enum quota_type type ;
};

#line 178  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/quota.h"
struct mem_dqblk {
   qsize_t dqb_bhardlimit ;
   qsize_t dqb_bsoftlimit ;
   qsize_t dqb_curspace ;
   qsize_t dqb_rsvspace ;
   qsize_t dqb_ihardlimit ;
   qsize_t dqb_isoftlimit ;
   qsize_t dqb_curinodes ;
   time_t dqb_btime ;
   time_t dqb_itime ;
};

#line 200 
struct quota_format_type;

#line 201  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/quota.h"
struct mem_dqinfo {
   struct quota_format_type *dqi_format ;
   int dqi_fmt_id ;
   struct list_head dqi_dirty_list ;
   unsigned long dqi_flags ;
   unsigned int dqi_bgrace ;
   unsigned int dqi_igrace ;
   qsize_t dqi_maxblimit ;
   qsize_t dqi_maxilimit ;
   void *dqi_priv ;
};

#line 264  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/quota.h"
struct dquot {
   struct hlist_node dq_hash ;
   struct list_head dq_inuse ;
   struct list_head dq_free ;
   struct list_head dq_dirty ;
   struct mutex dq_lock ;
   atomic_t dq_count ;
   wait_queue_head_t dq_wait_unused ;
   struct super_block *dq_sb ;
   struct kqid dq_id ;
   loff_t dq_off ;
   unsigned long dq_flags ;
   struct mem_dqblk dq_dqb ;
};

#line 291  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/quota.h"
struct quota_format_ops {
   int (*check_quota_file)(struct super_block *, int ) ;
   int (*read_file_info)(struct super_block *, int ) ;
   int (*write_file_info)(struct super_block *, int ) ;
   int (*free_file_info)(struct super_block *, int ) ;
   int (*read_dqblk)(struct dquot *) ;
   int (*commit_dqblk)(struct dquot *) ;
   int (*release_dqblk)(struct dquot *) ;
};

#line 302  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/quota.h"
struct dquot_operations {
   int (*write_dquot)(struct dquot *) ;
   struct dquot *(*alloc_dquot)(struct super_block *, int ) ;
   void (*destroy_dquot)(struct dquot *) ;
   int (*acquire_dquot)(struct dquot *) ;
   int (*release_dquot)(struct dquot *) ;
   int (*mark_dirty)(struct dquot *) ;
   int (*write_info)(struct super_block *, int ) ;
   qsize_t *(*get_reserved_space)(struct inode *) ;
};

#line 316  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/quota.h"
struct quotactl_ops {
   int (*quota_on)(struct super_block *, int , int , struct path *) ;
   int (*quota_on_meta)(struct super_block *, int , int ) ;
   int (*quota_off)(struct super_block *, int ) ;
   int (*quota_sync)(struct super_block *, int ) ;
   int (*get_info)(struct super_block *, int , struct if_dqinfo *) ;
   int (*set_info)(struct super_block *, int , struct if_dqinfo *) ;
   int (*get_dqblk)(struct super_block *, struct kqid , struct fs_disk_quota *) ;
   int (*set_dqblk)(struct super_block *, struct kqid , struct fs_disk_quota *) ;
   int (*get_xstate)(struct super_block *, struct fs_quota_stat *) ;
   int (*set_xstate)(struct super_block *, unsigned int , int ) ;
   int (*get_xstatev)(struct super_block *, struct fs_quota_statv *) ;
};

#line 333  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/quota.h"
struct quota_format_type {
   int qf_fmt_id ;
   struct quota_format_ops const *qf_ops ;
   struct module *qf_owner ;
   struct quota_format_type *qf_next ;
};

#line 379  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/quota.h"
struct quota_info {
   unsigned int flags ;
   struct mutex dqio_mutex ;
   struct mutex dqonoff_mutex ;
   struct rw_semaphore dqptr_sem ;
   struct inode *files[2U] ;
   struct mem_dqinfo info[2U] ;
   struct quota_format_ops const *ops[2U] ;
};

#line 410 
struct address_space;

#line 411 
struct writeback_control;

#line 345  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/fs.h"
union __anonunion_arg_154 {
   char *buf ;
   void *data ;
};

#line 345  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/fs.h"
struct __anonstruct_read_descriptor_t_153 {
   size_t written ;
   size_t count ;
   union __anonunion_arg_154 arg ;
   int error ;
};

#line 345  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/fs.h"
typedef struct __anonstruct_read_descriptor_t_153 read_descriptor_t;

#line 348  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/fs.h"
struct address_space_operations {
   int (*writepage)(struct page *, struct writeback_control *) ;
   int (*readpage)(struct file *, struct page *) ;
   int (*writepages)(struct address_space *, struct writeback_control *) ;
   int (*set_page_dirty)(struct page *) ;
   int (*readpages)(struct file *, struct address_space *, struct list_head *, unsigned int ) ;
   int (*write_begin)(struct file *, struct address_space *, loff_t , unsigned int , unsigned int , struct page **, void **) ;
   int (*write_end)(struct file *, struct address_space *, loff_t , unsigned int , unsigned int , struct page *, void *) ;
   sector_t (*bmap)(struct address_space *, sector_t ) ;
   void (*invalidatepage)(struct page *, unsigned int , unsigned int ) ;
   int (*releasepage)(struct page *, gfp_t ) ;
   void (*freepage)(struct page *) ;
   ssize_t (*direct_IO)(int , struct kiocb *, struct iovec const *, loff_t , unsigned long ) ;
   int (*get_xip_mem)(struct address_space *, unsigned long , int , void **, unsigned long *) ;
   int (*migratepage)(struct address_space *, struct page *, struct page *, enum migrate_mode ) ;
   int (*launder_page)(struct page *) ;
   int (*is_partially_uptodate)(struct page *, read_descriptor_t *, unsigned long ) ;
   void (*is_dirty_writeback)(struct page *, bool *, bool *) ;
   int (*error_remove_page)(struct address_space *, struct page *) ;
   int (*swap_activate)(struct swap_info_struct *, struct file *, sector_t *) ;
   void (*swap_deactivate)(struct file *) ;
};

#line 408 
struct backing_dev_info;

#line 409  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/fs.h"
struct address_space {
   struct inode *host ;
   struct radix_tree_root page_tree ;
   spinlock_t tree_lock ;
   unsigned int i_mmap_writable ;
   struct rb_root i_mmap ;
   struct list_head i_mmap_nonlinear ;
   struct mutex i_mmap_mutex ;
   unsigned long nrpages ;
   unsigned long writeback_index ;
   struct address_space_operations const *a_ops ;
   unsigned long flags ;
   struct backing_dev_info *backing_dev_info ;
   spinlock_t private_lock ;
   struct list_head private_list ;
   void *private_data ;
};

#line 430 
struct request_queue;

#line 431 
struct hd_struct;

#line 431 
struct gendisk;

#line 431  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/fs.h"
struct block_device {
   dev_t bd_dev ;
   int bd_openers ;
   struct inode *bd_inode ;
   struct super_block *bd_super ;
   struct mutex bd_mutex ;
   struct list_head bd_inodes ;
   void *bd_claiming ;
   void *bd_holder ;
   int bd_holders ;
   bool bd_write_holder ;
   struct list_head bd_holder_disks ;
   struct block_device *bd_contains ;
   unsigned int bd_block_size ;
   struct hd_struct *bd_part ;
   unsigned int bd_part_count ;
   int bd_invalidated ;
   struct gendisk *bd_disk ;
   struct request_queue *bd_queue ;
   struct list_head bd_list ;
   unsigned long bd_private ;
   int bd_fsfreeze_count ;
   struct mutex bd_fsfreeze_mutex ;
};

#line 503 
struct posix_acl;

#line 504 
struct inode_operations;

#line 504  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/fs.h"
union __anonunion_155 {
   unsigned int const i_nlink ;
   unsigned int __i_nlink ;
};

#line 504  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/fs.h"
union __anonunion_156 {
   struct hlist_head i_dentry ;
   struct callback_head i_rcu ;
};

#line 504 
struct file_lock;

#line 504 
struct cdev;

#line 504  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/fs.h"
union __anonunion_157 {
   struct pipe_inode_info *i_pipe ;
   struct block_device *i_bdev ;
   struct cdev *i_cdev ;
};

#line 504  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/fs.h"
struct inode {
   umode_t i_mode ;
   unsigned short i_opflags ;
   kuid_t i_uid ;
   kgid_t i_gid ;
   unsigned int i_flags ;
   struct posix_acl *i_acl ;
   struct posix_acl *i_default_acl ;
   struct inode_operations const *i_op ;
   struct super_block *i_sb ;
   struct address_space *i_mapping ;
   void *i_security ;
   unsigned long i_ino ;
   union __anonunion_155 __anonCompField_inode_42 ;
   dev_t i_rdev ;
   loff_t i_size ;
   struct timespec i_atime ;
   struct timespec i_mtime ;
   struct timespec i_ctime ;
   spinlock_t i_lock ;
   unsigned short i_bytes ;
   unsigned int i_blkbits ;
   blkcnt_t i_blocks ;
   unsigned long i_state ;
   struct mutex i_mutex ;
   unsigned long dirtied_when ;
   struct hlist_node i_hash ;
   struct list_head i_wb_list ;
   struct list_head i_lru ;
   struct list_head i_sb_list ;
   union __anonunion_156 __anonCompField_inode_43 ;
   u64 i_version ;
   atomic_t i_count ;
   atomic_t i_dio_count ;
   atomic_t i_writecount ;
   struct file_operations const *i_fop ;
   struct file_lock *i_flock ;
   struct address_space i_data ;
   struct dquot *i_dquot[2U] ;
   struct list_head i_devices ;
   union __anonunion_157 __anonCompField_inode_44 ;
   __u32 i_generation ;
   __u32 i_fsnotify_mask ;
   struct hlist_head i_fsnotify_marks ;
   atomic_t i_readcount ;
   void *i_private ;
};

#line 740  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/fs.h"
struct fown_struct {
   rwlock_t lock ;
   struct pid *pid ;
   enum pid_type pid_type ;
   kuid_t uid ;
   kuid_t euid ;
   int signum ;
};

#line 748  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/fs.h"
struct file_ra_state {
   unsigned long start ;
   unsigned int size ;
   unsigned int async_size ;
   unsigned int ra_pages ;
   unsigned int mmap_miss ;
   loff_t prev_pos ;
};

#line 771  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/fs.h"
union __anonunion_f_u_158 {
   struct llist_node fu_llist ;
   struct callback_head fu_rcuhead ;
};

#line 771  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/fs.h"
struct file {
   union __anonunion_f_u_158 f_u ;
   struct path f_path ;
   struct inode *f_inode ;
   struct file_operations const *f_op ;
   spinlock_t f_lock ;
   atomic_long_t f_count ;
   unsigned int f_flags ;
   fmode_t f_mode ;
   struct mutex f_pos_lock ;
   loff_t f_pos ;
   struct fown_struct f_owner ;
   struct cred const *f_cred ;
   struct file_ra_state f_ra ;
   u64 f_version ;
   void *f_security ;
   void *private_data ;
   struct list_head f_ep_links ;
   struct list_head f_tfile_llink ;
   struct address_space *f_mapping ;
   unsigned long f_mnt_write_state ;
};

#line 909 
struct files_struct;

#line 909  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/fs.h"
typedef struct files_struct *fl_owner_t;

#line 910  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/fs.h"
struct file_lock_operations {
   void (*fl_copy_lock)(struct file_lock *, struct file_lock *) ;
   void (*fl_release_private)(struct file_lock *) ;
};

#line 915  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/fs.h"
struct lock_manager_operations {
   int (*lm_compare_owner)(struct file_lock *, struct file_lock *) ;
   unsigned long (*lm_owner_key)(struct file_lock *) ;
   void (*lm_notify)(struct file_lock *) ;
   int (*lm_grant)(struct file_lock *, struct file_lock *, int ) ;
   void (*lm_break)(struct file_lock *) ;
   int (*lm_change)(struct file_lock **, int ) ;
};

#line 933 
struct nlm_lockowner;

#line 934  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/fs.h"
struct nfs_lock_info {
   u32 state ;
   struct nlm_lockowner *owner ;
   struct list_head list ;
};

#line 14  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/nfs_fs_i.h"
struct nfs4_lock_state;

#line 15  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/nfs_fs_i.h"
struct nfs4_lock_info {
   struct nfs4_lock_state *owner ;
};

#line 19 
struct fasync_struct;

#line 19  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/nfs_fs_i.h"
struct __anonstruct_afs_160 {
   struct list_head link ;
   int state ;
};

#line 19  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/nfs_fs_i.h"
union __anonunion_fl_u_159 {
   struct nfs_lock_info nfs_fl ;
   struct nfs4_lock_info nfs4_fl ;
   struct __anonstruct_afs_160 afs ;
};

#line 19  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/nfs_fs_i.h"
struct file_lock {
   struct file_lock *fl_next ;
   struct hlist_node fl_link ;
   struct list_head fl_block ;
   fl_owner_t fl_owner ;
   unsigned int fl_flags ;
   unsigned char fl_type ;
   unsigned int fl_pid ;
   int fl_link_cpu ;
   struct pid *fl_nspid ;
   wait_queue_head_t fl_wait ;
   struct file *fl_file ;
   loff_t fl_start ;
   loff_t fl_end ;
   struct fasync_struct *fl_fasync ;
   unsigned long fl_break_time ;
   unsigned long fl_downgrade_time ;
   struct file_lock_operations const *fl_ops ;
   struct lock_manager_operations const *fl_lmops ;
   union __anonunion_fl_u_159 fl_u ;
};

#line 1036  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/fs.h"
struct fasync_struct {
   spinlock_t fa_lock ;
   int magic ;
   int fa_fd ;
   struct fasync_struct *fa_next ;
   struct file *fa_file ;
   struct callback_head fa_rcu ;
};

#line 1228  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/fs.h"
struct sb_writers {
   struct percpu_counter counter[3U] ;
   wait_queue_head_t wait ;
   int frozen ;
   wait_queue_head_t wait_unfrozen ;
   struct lockdep_map lock_map[3U] ;
};

#line 1244 
struct super_operations;

#line 1244 
struct xattr_handler;

#line 1244 
struct mtd_info;

#line 1244  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/fs.h"
struct super_block {
   struct list_head s_list ;
   dev_t s_dev ;
   unsigned char s_blocksize_bits ;
   unsigned long s_blocksize ;
   loff_t s_maxbytes ;
   struct file_system_type *s_type ;
   struct super_operations const *s_op ;
   struct dquot_operations const *dq_op ;
   struct quotactl_ops const *s_qcop ;
   struct export_operations const *s_export_op ;
   unsigned long s_flags ;
   unsigned long s_magic ;
   struct dentry *s_root ;
   struct rw_semaphore s_umount ;
   int s_count ;
   atomic_t s_active ;
   void *s_security ;
   struct xattr_handler const **s_xattr ;
   struct list_head s_inodes ;
   struct hlist_bl_head s_anon ;
   struct list_head s_mounts ;
   struct block_device *s_bdev ;
   struct backing_dev_info *s_bdi ;
   struct mtd_info *s_mtd ;
   struct hlist_node s_instances ;
   struct quota_info s_dquot ;
   struct sb_writers s_writers ;
   char s_id[32U] ;
   u8 s_uuid[16U] ;
   void *s_fs_info ;
   unsigned int s_max_links ;
   fmode_t s_mode ;
   u32 s_time_gran ;
   struct mutex s_vfs_rename_mutex ;
   char *s_subtype ;
   char *s_options ;
   struct dentry_operations const *s_d_op ;
   int cleancache_poolid ;
   struct shrinker s_shrink ;
   atomic_long_t s_remove_count ;
   int s_readonly_remount ;
   struct workqueue_struct *s_dio_done_wq ;
   struct list_lru s_dentry_lru ;
   struct list_lru s_inode_lru ;
   struct callback_head rcu ;
};

#line 1474  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/fs.h"
struct fiemap_extent_info {
   unsigned int fi_flags ;
   unsigned int fi_extents_mapped ;
   unsigned int fi_extents_max ;
   struct fiemap_extent *fi_extents_start ;
};

#line 1512  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/fs.h"
struct dir_context {
   int (*actor)(void *, char const *, int , loff_t , u64 , unsigned int ) ;
   loff_t pos ;
};

#line 1517  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/fs.h"
struct file_operations {
   struct module *owner ;
   loff_t (*llseek)(struct file *, loff_t , int ) ;
   ssize_t (*read)(struct file *, char *, size_t , loff_t *) ;
   ssize_t (*write)(struct file *, char const *, size_t , loff_t *) ;
   ssize_t (*aio_read)(struct kiocb *, struct iovec const *, unsigned long , loff_t ) ;
   ssize_t (*aio_write)(struct kiocb *, struct iovec const *, unsigned long , loff_t ) ;
   int (*iterate)(struct file *, struct dir_context *) ;
   unsigned int (*poll)(struct file *, struct poll_table_struct *) ;
   long (*unlocked_ioctl)(struct file *, unsigned int , unsigned long ) ;
   long (*compat_ioctl)(struct file *, unsigned int , unsigned long ) ;
   int (*mmap)(struct file *, struct vm_area_struct *) ;
   int (*open)(struct inode *, struct file *) ;
   int (*flush)(struct file *, fl_owner_t ) ;
   int (*release)(struct inode *, struct file *) ;
   int (*fsync)(struct file *, loff_t , loff_t , int ) ;
   int (*aio_fsync)(struct kiocb *, int ) ;
   int (*fasync)(int , struct file *, int ) ;
   int (*lock)(struct file *, int , struct file_lock *) ;
   ssize_t (*sendpage)(struct file *, struct page *, int , size_t , loff_t *, int ) ;
   unsigned long (*get_unmapped_area)(struct file *, unsigned long , unsigned long , unsigned long , unsigned long ) ;
   int (*check_flags)(int ) ;
   int (*flock)(struct file *, int , struct file_lock *) ;
   ssize_t (*splice_write)(struct pipe_inode_info *, struct file *, loff_t *, size_t , unsigned int ) ;
   ssize_t (*splice_read)(struct file *, loff_t *, struct pipe_inode_info *, size_t , unsigned int ) ;
   int (*setlease)(struct file *, long , struct file_lock **) ;
   long (*fallocate)(struct file *, int , loff_t , loff_t ) ;
   int (*show_fdinfo)(struct seq_file *, struct file *) ;
};

#line 1555  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/fs.h"
struct inode_operations {
   struct dentry *(*lookup)(struct inode *, struct dentry *, unsigned int ) ;
   void *(*follow_link)(struct dentry *, struct nameidata *) ;
   int (*permission)(struct inode *, int ) ;
   struct posix_acl *(*get_acl)(struct inode *, int ) ;
   int (*readlink)(struct dentry *, char *, int ) ;
   void (*put_link)(struct dentry *, struct nameidata *, void *) ;
   int (*create)(struct inode *, struct dentry *, umode_t , bool ) ;
   int (*link)(struct dentry *, struct inode *, struct dentry *) ;
   int (*unlink)(struct inode *, struct dentry *) ;
   int (*symlink)(struct inode *, struct dentry *, char const *) ;
   int (*mkdir)(struct inode *, struct dentry *, umode_t ) ;
   int (*rmdir)(struct inode *, struct dentry *) ;
   int (*mknod)(struct inode *, struct dentry *, umode_t , dev_t ) ;
   int (*rename)(struct inode *, struct dentry *, struct inode *, struct dentry *) ;
   int (*setattr)(struct dentry *, struct iattr *) ;
   int (*getattr)(struct vfsmount *, struct dentry *, struct kstat *) ;
   int (*setxattr)(struct dentry *, char const *, void const *, size_t , int ) ;
   ssize_t (*getxattr)(struct dentry *, char const *, void *, size_t ) ;
   ssize_t (*listxattr)(struct dentry *, char *, size_t ) ;
   int (*removexattr)(struct dentry *, char const *) ;
   int (*fiemap)(struct inode *, struct fiemap_extent_info *, u64 , u64 ) ;
   int (*update_time)(struct inode *, struct timespec *, int ) ;
   int (*atomic_open)(struct inode *, struct dentry *, struct file *, unsigned int , umode_t , int *) ;
   int (*tmpfile)(struct inode *, struct dentry *, umode_t ) ;
   int (*set_acl)(struct inode *, struct posix_acl *, int ) ;
};

#line 1600  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/fs.h"
struct super_operations {
   struct inode *(*alloc_inode)(struct super_block *) ;
   void (*destroy_inode)(struct inode *) ;
   void (*dirty_inode)(struct inode *, int ) ;
   int (*write_inode)(struct inode *, struct writeback_control *) ;
   int (*drop_inode)(struct inode *) ;
   void (*evict_inode)(struct inode *) ;
   void (*put_super)(struct super_block *) ;
   int (*sync_fs)(struct super_block *, int ) ;
   int (*freeze_fs)(struct super_block *) ;
   int (*unfreeze_fs)(struct super_block *) ;
   int (*statfs)(struct dentry *, struct kstatfs *) ;
   int (*remount_fs)(struct super_block *, int *, char *) ;
   void (*umount_begin)(struct super_block *) ;
   int (*show_options)(struct seq_file *, struct dentry *) ;
   int (*show_devname)(struct seq_file *, struct dentry *) ;
   int (*show_path)(struct seq_file *, struct dentry *) ;
   int (*show_stats)(struct seq_file *, struct dentry *) ;
   ssize_t (*quota_read)(struct super_block *, int , char *, size_t , loff_t ) ;
   ssize_t (*quota_write)(struct super_block *, int , char const *, size_t , loff_t ) ;
   int (*bdev_try_to_free_page)(struct super_block *, struct page *, gfp_t ) ;
   long (*nr_cached_objects)(struct super_block *, int ) ;
   long (*free_cached_objects)(struct super_block *, long , int ) ;
};

#line 1814  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/fs.h"
struct file_system_type {
   char const *name ;
   int fs_flags ;
   struct dentry *(*mount)(struct file_system_type *, int , char const *, void *) ;
   void (*kill_sb)(struct super_block *) ;
   struct module *owner ;
   struct file_system_type *next ;
   struct hlist_head fs_supers ;
   struct lock_class_key s_lock_key ;
   struct lock_class_key s_umount_key ;
   struct lock_class_key s_vfs_rename_key ;
   struct lock_class_key s_writers_key[3U] ;
   struct lock_class_key i_lock_key ;
   struct lock_class_key i_mutex_key ;
   struct lock_class_key i_mutex_dir_key ;
};

#line 84  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/plist.h"
struct plist_node {
   int prio ;
   struct list_head prio_list ;
   struct list_head node_list ;
};

#line 45  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/uprobes.h"
struct arch_uprobe_task {
   unsigned long saved_scratch_register ;
   unsigned int saved_trap_nr ;
   unsigned int saved_tf ;
};

#line 54 
enum uprobe_task_state {
    UTASK_RUNNING = 0,
    UTASK_SSTEP = 1,
    UTASK_SSTEP_ACK = 2,
    UTASK_SSTEP_TRAPPED = 3
};

#line 61  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/uprobes.h"
struct __anonstruct_163 {
   struct arch_uprobe_task autask ;
   unsigned long vaddr ;
};

#line 61  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/uprobes.h"
struct __anonstruct_164 {
   struct callback_head dup_xol_work ;
   unsigned long dup_xol_addr ;
};

#line 61  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/uprobes.h"
union __anonunion_162 {
   struct __anonstruct_163 __anonCompField___anonunion_162_46 ;
   struct __anonstruct_164 __anonCompField___anonunion_162_47 ;
};

#line 61 
struct uprobe;

#line 61 
struct return_instance;

#line 61  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/uprobes.h"
struct uprobe_task {
   enum uprobe_task_state state ;
   union __anonunion_162 __anonCompField_uprobe_task_48 ;
   struct uprobe *active_uprobe ;
   unsigned long xol_vaddr ;
   struct return_instance *return_instances ;
   unsigned int depth ;
};

#line 93  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/uprobes.h"
struct xol_area;

#line 94  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/uprobes.h"
struct uprobes_state {
   struct xol_area *xol_area ;
};

#line 129  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/uprobes.h"
union __anonunion_165 {
   struct address_space *mapping ;
   void *s_mem ;
};

#line 129  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/uprobes.h"
union __anonunion_167 {
   unsigned long index ;
   void *freelist ;
   bool pfmemalloc ;
};

#line 129  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/uprobes.h"
struct __anonstruct_171 {
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(16))) inuse : 16 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(15))) objects : 15 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) frozen : 1 ;
};

#line 129  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/uprobes.h"
union __anonunion_170 {
   atomic_t _mapcount ;
   struct __anonstruct_171 __anonCompField___anonunion_170_51 ;
   int units ;
};

#line 129  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/uprobes.h"
struct __anonstruct_169 {
   union __anonunion_170 __anonCompField___anonstruct_169_52 ;
   atomic_t _count ;
};

#line 129  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/uprobes.h"
union __anonunion_168 {
   unsigned long counters ;
   struct __anonstruct_169 __anonCompField___anonunion_168_53 ;
   unsigned int active ;
};

#line 129  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/uprobes.h"
struct __anonstruct_166 {
   union __anonunion_167 __anonCompField___anonstruct_166_50 ;
   union __anonunion_168 __anonCompField___anonstruct_166_54 ;
};

#line 129  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/uprobes.h"
struct __anonstruct_173 {
   struct page *next ;
   int pages ;
   int pobjects ;
};

#line 129 
struct slab;

#line 129  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/uprobes.h"
union __anonunion_172 {
   struct list_head lru ;
   struct __anonstruct_173 __anonCompField___anonunion_172_56 ;
   struct list_head list ;
   struct slab *slab_page ;
   struct callback_head callback_head ;
   pgtable_t pmd_huge_pte ;
};

#line 129  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/uprobes.h"
union __anonunion_174 {
   unsigned long private ;
   spinlock_t *ptl ;
   struct kmem_cache *slab_cache ;
   struct page *first_page ;
};

#line 129  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/uprobes.h"
struct page {
   unsigned long flags ;
   union __anonunion_165 __anonCompField_page_49 ;
   struct __anonstruct_166 __anonCompField_page_55 ;
   union __anonunion_172 __anonCompField_page_57 ;
   union __anonunion_174 __anonCompField_page_58 ;
   unsigned long debug_flags ;
};

#line 186  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/mm_types.h"
struct page_frag {
   struct page *page ;
   __u32 offset ;
   __u32 size ;
};

#line 238  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/mm_types.h"
struct __anonstruct_linear_176 {
   struct rb_node rb ;
   unsigned long rb_subtree_last ;
};

#line 238  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/mm_types.h"
union __anonunion_shared_175 {
   struct __anonstruct_linear_176 linear ;
   struct list_head nonlinear ;
};

#line 238 
struct anon_vma;

#line 238 
struct mempolicy;

#line 238  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/mm_types.h"
struct vm_area_struct {
   unsigned long vm_start ;
   unsigned long vm_end ;
   struct vm_area_struct *vm_next ;
   struct vm_area_struct *vm_prev ;
   struct rb_node vm_rb ;
   unsigned long rb_subtree_gap ;
   struct mm_struct *vm_mm ;
   pgprot_t vm_page_prot ;
   unsigned long vm_flags ;
   union __anonunion_shared_175 shared ;
   struct list_head anon_vma_chain ;
   struct anon_vma *anon_vma ;
   struct vm_operations_struct const *vm_ops ;
   unsigned long vm_pgoff ;
   struct file *vm_file ;
   void *vm_private_data ;
   struct mempolicy *vm_policy ;
};

#line 310  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/mm_types.h"
struct core_thread {
   struct task_struct *task ;
   struct core_thread *next ;
};

#line 316  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/mm_types.h"
struct core_state {
   atomic_t nr_threads ;
   struct core_thread dumper ;
   struct completion startup ;
};

#line 329  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/mm_types.h"
struct task_rss_stat {
   int events ;
   int count[3U] ;
};

#line 337  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/mm_types.h"
struct mm_rss_stat {
   atomic_long_t count[3U] ;
};

#line 342 
struct kioctx_table;

#line 343 
struct linux_binfmt;

#line 343 
struct mmu_notifier_mm;

#line 343  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/mm_types.h"
struct mm_struct {
   struct vm_area_struct *mmap ;
   struct rb_root mm_rb ;
   struct vm_area_struct *mmap_cache ;
   unsigned long (*get_unmapped_area)(struct file *, unsigned long , unsigned long , unsigned long , unsigned long ) ;
   unsigned long mmap_base ;
   unsigned long mmap_legacy_base ;
   unsigned long task_size ;
   unsigned long highest_vm_end ;
   pgd_t *pgd ;
   atomic_t mm_users ;
   atomic_t mm_count ;
   atomic_long_t nr_ptes ;
   int map_count ;
   spinlock_t page_table_lock ;
   struct rw_semaphore mmap_sem ;
   struct list_head mmlist ;
   unsigned long hiwater_rss ;
   unsigned long hiwater_vm ;
   unsigned long total_vm ;
   unsigned long locked_vm ;
   unsigned long pinned_vm ;
   unsigned long shared_vm ;
   unsigned long exec_vm ;
   unsigned long stack_vm ;
   unsigned long def_flags ;
   unsigned long start_code ;
   unsigned long end_code ;
   unsigned long start_data ;
   unsigned long end_data ;
   unsigned long start_brk ;
   unsigned long brk ;
   unsigned long start_stack ;
   unsigned long arg_start ;
   unsigned long arg_end ;
   unsigned long env_start ;
   unsigned long env_end ;
   unsigned long saved_auxv[46U] ;
   struct mm_rss_stat rss_stat ;
   struct linux_binfmt *binfmt ;
   cpumask_var_t cpu_vm_mask_var ;
   mm_context_t context ;
   unsigned long flags ;
   struct core_state *core_state ;
   spinlock_t ioctx_lock ;
   struct kioctx_table *ioctx_table ;
   struct task_struct *owner ;
   struct file *exe_file ;
   struct mmu_notifier_mm *mmu_notifier_mm ;
   struct cpumask cpumask_allocation ;
   unsigned long numa_next_scan ;
   unsigned long numa_scan_offset ;
   int numa_scan_seq ;
   bool tlb_flush_pending ;
   struct uprobes_state uprobes_state ;
};

#line 4  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/asm-generic/cputime_jiffies.h"
typedef unsigned long cputime_t;

#line 25  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/sem.h"
struct sem_undo_list;

#line 25  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/sem.h"
struct sysv_sem {
   struct sem_undo_list *undo_list ;
};

#line 24  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/signal.h"
struct __anonstruct_sigset_t_177 {
   unsigned long sig[1U] ;
};

#line 24  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/signal.h"
typedef struct __anonstruct_sigset_t_177 sigset_t;

#line 25 
struct siginfo;

#line 17  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/signal-defs.h"
typedef void __signalfn_t(int );

#line 18  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/signal-defs.h"
typedef __signalfn_t *__sighandler_t;

#line 20  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/signal-defs.h"
typedef void __restorefn_t(void);

#line 21  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/signal-defs.h"
typedef __restorefn_t *__sigrestore_t;

#line 34  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/arch/x86/include/asm/signal.h"
union sigval {
   int sival_int ;
   void *sival_ptr ;
};

#line 10  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/siginfo.h"
typedef union sigval sigval_t;

#line 11  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/siginfo.h"
struct __anonstruct__kill_179 {
   __kernel_pid_t _pid ;
   __kernel_uid32_t _uid ;
};

#line 11  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/siginfo.h"
struct __anonstruct__timer_180 {
   __kernel_timer_t _tid ;
   int _overrun ;
   char _pad[0U] ;
   sigval_t _sigval ;
   int _sys_private ;
};

#line 11  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/siginfo.h"
struct __anonstruct__rt_181 {
   __kernel_pid_t _pid ;
   __kernel_uid32_t _uid ;
   sigval_t _sigval ;
};

#line 11  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/siginfo.h"
struct __anonstruct__sigchld_182 {
   __kernel_pid_t _pid ;
   __kernel_uid32_t _uid ;
   int _status ;
   __kernel_clock_t _utime ;
   __kernel_clock_t _stime ;
};

#line 11  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/siginfo.h"
struct __anonstruct__sigfault_183 {
   void *_addr ;
   short _addr_lsb ;
};

#line 11  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/siginfo.h"
struct __anonstruct__sigpoll_184 {
   long _band ;
   int _fd ;
};

#line 11  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/siginfo.h"
struct __anonstruct__sigsys_185 {
   void *_call_addr ;
   int _syscall ;
   unsigned int _arch ;
};

#line 11  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/siginfo.h"
union __anonunion__sifields_178 {
   int _pad[28U] ;
   struct __anonstruct__kill_179 _kill ;
   struct __anonstruct__timer_180 _timer ;
   struct __anonstruct__rt_181 _rt ;
   struct __anonstruct__sigchld_182 _sigchld ;
   struct __anonstruct__sigfault_183 _sigfault ;
   struct __anonstruct__sigpoll_184 _sigpoll ;
   struct __anonstruct__sigsys_185 _sigsys ;
};

#line 11  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/siginfo.h"
struct siginfo {
   int si_signo ;
   int si_errno ;
   int si_code ;
   union __anonunion__sifields_178 _sifields ;
};

#line 109  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/asm-generic/siginfo.h"
typedef struct siginfo siginfo_t;

#line 11  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/signal.h"
struct user_struct;

#line 21  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/signal.h"
struct sigpending {
   struct list_head list ;
   sigset_t signal ;
};

#line 251  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/signal.h"
struct sigaction {
   __sighandler_t sa_handler ;
   unsigned long sa_flags ;
   __sigrestore_t sa_restorer ;
   sigset_t sa_mask ;
};

#line 265  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/signal.h"
struct k_sigaction {
   struct sigaction sa ;
};

#line 46  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/linux/seccomp.h"
struct seccomp_filter;

#line 47  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/linux/seccomp.h"
struct seccomp {
   int mode ;
   struct seccomp_filter *filter ;
};

#line 40  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/rtmutex.h"
struct rt_mutex_waiter;

#line 41  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/linux/resource.h"
struct rlimit {
   __kernel_ulong_t rlim_cur ;
   __kernel_ulong_t rlim_max ;
};

#line 11  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/resource.h"
struct task_io_accounting {
   u64 rchar ;
   u64 wchar ;
   u64 syscr ;
   u64 syscw ;
   u64 read_bytes ;
   u64 write_bytes ;
   u64 cancelled_write_bytes ;
};

#line 45  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/task_io_accounting.h"
struct latency_record {
   unsigned long backtrace[12U] ;
   unsigned int count ;
   unsigned long time ;
   unsigned long max ;
};

#line 39  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/latencytop.h"
struct assoc_array_ptr;

#line 39  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/latencytop.h"
struct assoc_array {
   struct assoc_array_ptr *root ;
   unsigned long nr_leaves_on_tree ;
};

#line 31  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/key.h"
typedef int32_t key_serial_t;

#line 34  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/key.h"
typedef uint32_t key_perm_t;

#line 35 
struct key;

#line 36 
struct signal_struct;

#line 37 
struct key_type;

#line 41  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/key.h"
struct keyring_index_key {
   struct key_type *type ;
   char const *description ;
   size_t desc_len ;
};

#line 123  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/key.h"
union __anonunion_188 {
   struct list_head graveyard_link ;
   struct rb_node serial_node ;
};

#line 123 
struct key_user;

#line 123  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/key.h"
union __anonunion_189 {
   time_t expiry ;
   time_t revoked_at ;
};

#line 123  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/key.h"
struct __anonstruct_191 {
   struct key_type *type ;
   char *description ;
};

#line 123  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/key.h"
union __anonunion_190 {
   struct keyring_index_key index_key ;
   struct __anonstruct_191 __anonCompField___anonunion_190_61 ;
};

#line 123  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/key.h"
union __anonunion_type_data_192 {
   struct list_head link ;
   unsigned long x[2U] ;
   void *p[2U] ;
   int reject_error ;
};

#line 123  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/key.h"
union __anonunion_payload_194 {
   unsigned long value ;
   void *rcudata ;
   void *data ;
   void *data2[2U] ;
};

#line 123  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/key.h"
union __anonunion_193 {
   union __anonunion_payload_194 payload ;
   struct assoc_array keys ;
};

#line 123  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/key.h"
struct key {
   atomic_t usage ;
   key_serial_t serial ;
   union __anonunion_188 __anonCompField_key_59 ;
   struct rw_semaphore sem ;
   struct key_user *user ;
   void *security ;
   union __anonunion_189 __anonCompField_key_60 ;
   time_t last_used_at ;
   kuid_t uid ;
   kgid_t gid ;
   key_perm_t perm ;
   unsigned short quotalen ;
   unsigned short datalen ;
   unsigned long flags ;
   union __anonunion_190 __anonCompField_key_62 ;
   union __anonunion_type_data_192 type_data ;
   union __anonunion_193 __anonCompField_key_63 ;
};

#line 345 
struct audit_context;

#line 27  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/selinux.h"
struct group_info {
   atomic_t usage ;
   int ngroups ;
   int nblocks ;
   kgid_t small_block[32U] ;
   kgid_t *blocks[0U] ;
};

#line 78  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/cred.h"
struct cred {
   atomic_t usage ;
   atomic_t subscribers ;
   void *put_addr ;
   unsigned int magic ;
   kuid_t uid ;
   kgid_t gid ;
   kuid_t suid ;
   kgid_t sgid ;
   kuid_t euid ;
   kgid_t egid ;
   kuid_t fsuid ;
   kgid_t fsgid ;
   unsigned int securebits ;
   kernel_cap_t cap_inheritable ;
   kernel_cap_t cap_permitted ;
   kernel_cap_t cap_effective ;
   kernel_cap_t cap_bset ;
   unsigned char jit_keyring ;
   struct key *session_keyring ;
   struct key *process_keyring ;
   struct key *thread_keyring ;
   struct key *request_key_auth ;
   void *security ;
   struct user_struct *user ;
   struct user_namespace *user_ns ;
   struct group_info *group_info ;
   struct callback_head rcu ;
};

#line 123  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/sched.h"
struct futex_pi_state;

#line 124 
struct robust_list_head;

#line 125 
struct bio_list;

#line 126 
struct fs_struct;

#line 127 
struct perf_event_context;

#line 128 
struct blk_plug;

#line 180 
struct cfs_rq;

#line 181 
struct task_group;

#line 421  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/sched.h"
struct sighand_struct {
   atomic_t count ;
   struct k_sigaction action[64U] ;
   spinlock_t siglock ;
   wait_queue_head_t signalfd_wqh ;
};

#line 460  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/sched.h"
struct pacct_struct {
   int ac_flag ;
   long ac_exitcode ;
   unsigned long ac_mem ;
   cputime_t ac_utime ;
   cputime_t ac_stime ;
   unsigned long ac_minflt ;
   unsigned long ac_majflt ;
};

#line 468  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/sched.h"
struct cpu_itimer {
   cputime_t expires ;
   cputime_t incr ;
   u32 error ;
   u32 incr_error ;
};

#line 475  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/sched.h"
struct cputime {
   cputime_t utime ;
   cputime_t stime ;
};

#line 487  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/sched.h"
struct task_cputime {
   cputime_t utime ;
   cputime_t stime ;
   unsigned long long sum_exec_runtime ;
};

#line 507  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/sched.h"
struct thread_group_cputimer {
   struct task_cputime cputime ;
   int running ;
   raw_spinlock_t lock ;
};

#line 549 
struct autogroup;

#line 550 
struct tty_struct;

#line 550 
struct taskstats;

#line 550 
struct tty_audit_buf;

#line 550  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/sched.h"
struct signal_struct {
   atomic_t sigcnt ;
   atomic_t live ;
   int nr_threads ;
   struct list_head thread_head ;
   wait_queue_head_t wait_chldexit ;
   struct task_struct *curr_target ;
   struct sigpending shared_pending ;
   int group_exit_code ;
   int notify_count ;
   struct task_struct *group_exit_task ;
   int group_stop_count ;
   unsigned int flags ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) is_child_subreaper : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) has_child_subreaper : 1 ;
   int posix_timer_id ;
   struct list_head posix_timers ;
   struct hrtimer real_timer ;
   struct pid *leader_pid ;
   ktime_t it_real_incr ;
   struct cpu_itimer it[2U] ;
   struct thread_group_cputimer cputimer ;
   struct task_cputime cputime_expires ;
   struct list_head cpu_timers[3U] ;
   struct pid *tty_old_pgrp ;
   int leader ;
   struct tty_struct *tty ;
   struct autogroup *autogroup ;
   cputime_t utime ;
   cputime_t stime ;
   cputime_t cutime ;
   cputime_t cstime ;
   cputime_t gtime ;
   cputime_t cgtime ;
   struct cputime prev_cputime ;
   unsigned long nvcsw ;
   unsigned long nivcsw ;
   unsigned long cnvcsw ;
   unsigned long cnivcsw ;
   unsigned long min_flt ;
   unsigned long maj_flt ;
   unsigned long cmin_flt ;
   unsigned long cmaj_flt ;
   unsigned long inblock ;
   unsigned long oublock ;
   unsigned long cinblock ;
   unsigned long coublock ;
   unsigned long maxrss ;
   unsigned long cmaxrss ;
   struct task_io_accounting ioac ;
   unsigned long long sum_sched_runtime ;
   struct rlimit rlim[16U] ;
   struct pacct_struct pacct ;
   struct taskstats *stats ;
   unsigned int audit_tty ;
   unsigned int audit_tty_log_passwd ;
   struct tty_audit_buf *tty_audit_buf ;
   struct rw_semaphore group_rwsem ;
   oom_flags_t oom_flags ;
   short oom_score_adj ;
   short oom_score_adj_min ;
   struct mutex cred_guard_mutex ;
};

#line 730  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/sched.h"
struct user_struct {
   atomic_t __count ;
   atomic_t processes ;
   atomic_t files ;
   atomic_t sigpending ;
   atomic_t inotify_watches ;
   atomic_t inotify_devs ;
   atomic_t fanotify_listeners ;
   atomic_long_t epoll_watches ;
   unsigned long mq_bytes ;
   unsigned long locked_shm ;
   struct key *uid_keyring ;
   struct key *session_keyring ;
   struct hlist_node uidhash_node ;
   kuid_t uid ;
   atomic_long_t locked_vm ;
};

#line 774 
struct reclaim_state;

#line 775  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/sched.h"
struct sched_info {
   unsigned long pcount ;
   unsigned long long run_delay ;
   unsigned long long last_arrival ;
   unsigned long long last_queued ;
};

#line 790  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/sched.h"
struct task_delay_info {
   spinlock_t lock ;
   unsigned int flags ;
   struct timespec blkio_start ;
   struct timespec blkio_end ;
   u64 blkio_delay ;
   u64 swapin_delay ;
   u32 blkio_count ;
   u32 swapin_count ;
   struct timespec freepages_start ;
   struct timespec freepages_end ;
   u64 freepages_delay ;
   u32 freepages_count ;
};

#line 1005  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/sched.h"
struct load_weight {
   unsigned long weight ;
   u32 inv_weight ;
};

#line 1013  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/sched.h"
struct sched_avg {
   u32 runnable_avg_sum ;
   u32 runnable_avg_period ;
   u64 last_runnable_update ;
   s64 decay_count ;
   unsigned long load_avg_contrib ;
};

#line 1025  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/sched.h"
struct sched_statistics {
   u64 wait_start ;
   u64 wait_max ;
   u64 wait_count ;
   u64 wait_sum ;
   u64 iowait_count ;
   u64 iowait_sum ;
   u64 sleep_start ;
   u64 sleep_max ;
   s64 sum_sleep_runtime ;
   u64 block_start ;
   u64 block_max ;
   u64 exec_max ;
   u64 slice_max ;
   u64 nr_migrations_cold ;
   u64 nr_failed_migrations_affine ;
   u64 nr_failed_migrations_running ;
   u64 nr_failed_migrations_hot ;
   u64 nr_forced_migrations ;
   u64 nr_wakeups ;
   u64 nr_wakeups_sync ;
   u64 nr_wakeups_migrate ;
   u64 nr_wakeups_local ;
   u64 nr_wakeups_remote ;
   u64 nr_wakeups_affine ;
   u64 nr_wakeups_affine_attempts ;
   u64 nr_wakeups_passive ;
   u64 nr_wakeups_idle ;
};

#line 1060  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/sched.h"
struct sched_entity {
   struct load_weight load ;
   struct rb_node run_node ;
   struct list_head group_node ;
   unsigned int on_rq ;
   u64 exec_start ;
   u64 sum_exec_runtime ;
   u64 vruntime ;
   u64 prev_sum_exec_runtime ;
   u64 nr_migrations ;
   struct sched_statistics statistics ;
   struct sched_entity *parent ;
   struct cfs_rq *cfs_rq ;
   struct cfs_rq *my_q ;
   struct sched_avg avg ;
};

#line 1091 
struct rt_rq;

#line 1091  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/sched.h"
struct sched_rt_entity {
   struct list_head run_list ;
   unsigned long timeout ;
   unsigned long watchdog_stamp ;
   unsigned int time_slice ;
   struct sched_rt_entity *back ;
   struct sched_rt_entity *parent ;
   struct rt_rq *rt_rq ;
   struct rt_rq *my_q ;
};

#line 1107  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/sched.h"
struct sched_dl_entity {
   struct rb_node rb_node ;
   u64 dl_runtime ;
   u64 dl_deadline ;
   u64 dl_period ;
   u64 dl_bw ;
   s64 runtime ;
   u64 deadline ;
   unsigned int flags ;
   int dl_throttled ;
   int dl_new ;
   int dl_boosted ;
   struct hrtimer dl_timer ;
};

#line 1162 
struct mem_cgroup;

#line 1162  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/sched.h"
struct memcg_batch_info {
   int do_batch ;
   struct mem_cgroup *memcg ;
   unsigned long nr_pages ;
   unsigned long memsw_nr_pages ;
};

#line 1569  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/sched.h"
struct memcg_oom_info {
   struct mem_cgroup *memcg ;
   gfp_t gfp_mask ;
   int order ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) may_oom : 1 ;
};

#line 1576 
struct sched_class;

#line 1576 
struct css_set;

#line 1576 
struct compat_robust_list_head;

#line 1576 
struct numa_group;

#line 1576 
struct ftrace_ret_stack;

#line 1576  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/sched.h"
struct task_struct {
   long volatile state ;
   void *stack ;
   atomic_t usage ;
   unsigned int flags ;
   unsigned int ptrace ;
   struct llist_node wake_entry ;
   int on_cpu ;
   struct task_struct *last_wakee ;
   unsigned long wakee_flips ;
   unsigned long wakee_flip_decay_ts ;
   int wake_cpu ;
   int on_rq ;
   int prio ;
   int static_prio ;
   int normal_prio ;
   unsigned int rt_priority ;
   struct sched_class const *sched_class ;
   struct sched_entity se ;
   struct sched_rt_entity rt ;
   struct task_group *sched_task_group ;
   struct sched_dl_entity dl ;
   struct hlist_head preempt_notifiers ;
   unsigned int btrace_seq ;
   unsigned int policy ;
   int nr_cpus_allowed ;
   cpumask_t cpus_allowed ;
   struct sched_info sched_info ;
   struct list_head tasks ;
   struct plist_node pushable_tasks ;
   struct rb_node pushable_dl_tasks ;
   struct mm_struct *mm ;
   struct mm_struct *active_mm ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) brk_randomized : 1 ;
   struct task_rss_stat rss_stat ;
   int exit_state ;
   int exit_code ;
   int exit_signal ;
   int pdeath_signal ;
   unsigned int jobctl ;
   unsigned int personality ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) in_execve : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) in_iowait : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) no_new_privs : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) sched_reset_on_fork : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) sched_contributes_to_load : 1 ;
   pid_t pid ;
   pid_t tgid ;
   struct task_struct *real_parent ;
   struct task_struct *parent ;
   struct list_head children ;
   struct list_head sibling ;
   struct task_struct *group_leader ;
   struct list_head ptraced ;
   struct list_head ptrace_entry ;
   struct pid_link pids[3U] ;
   struct list_head thread_group ;
   struct list_head thread_node ;
   struct completion *vfork_done ;
   int *set_child_tid ;
   int *clear_child_tid ;
   cputime_t utime ;
   cputime_t stime ;
   cputime_t utimescaled ;
   cputime_t stimescaled ;
   cputime_t gtime ;
   struct cputime prev_cputime ;
   unsigned long nvcsw ;
   unsigned long nivcsw ;
   struct timespec start_time ;
   struct timespec real_start_time ;
   unsigned long min_flt ;
   unsigned long maj_flt ;
   struct task_cputime cputime_expires ;
   struct list_head cpu_timers[3U] ;
   struct cred const *real_cred ;
   struct cred const *cred ;
   char comm[16U] ;
   int link_count ;
   int total_link_count ;
   struct sysv_sem sysvsem ;
   unsigned long last_switch_count ;
   struct thread_struct thread ;
   struct fs_struct *fs ;
   struct files_struct *files ;
   struct nsproxy *nsproxy ;
   struct signal_struct *signal ;
   struct sighand_struct *sighand ;
   sigset_t blocked ;
   sigset_t real_blocked ;
   sigset_t saved_sigmask ;
   struct sigpending pending ;
   unsigned long sas_ss_sp ;
   size_t sas_ss_size ;
   int (*notifier)(void *) ;
   void *notifier_data ;
   sigset_t *notifier_mask ;
   struct callback_head *task_works ;
   struct audit_context *audit_context ;
   kuid_t loginuid ;
   unsigned int sessionid ;
   struct seccomp seccomp ;
   u32 parent_exec_id ;
   u32 self_exec_id ;
   spinlock_t alloc_lock ;
   raw_spinlock_t pi_lock ;
   struct rb_root pi_waiters ;
   struct rb_node *pi_waiters_leftmost ;
   struct rt_mutex_waiter *pi_blocked_on ;
   struct task_struct *pi_top_task ;
   struct mutex_waiter *blocked_on ;
   unsigned int irq_events ;
   unsigned long hardirq_enable_ip ;
   unsigned long hardirq_disable_ip ;
   unsigned int hardirq_enable_event ;
   unsigned int hardirq_disable_event ;
   int hardirqs_enabled ;
   int hardirq_context ;
   unsigned long softirq_disable_ip ;
   unsigned long softirq_enable_ip ;
   unsigned int softirq_disable_event ;
   unsigned int softirq_enable_event ;
   int softirqs_enabled ;
   int softirq_context ;
   u64 curr_chain_key ;
   int lockdep_depth ;
   unsigned int lockdep_recursion ;
   struct held_lock held_locks[48U] ;
   gfp_t lockdep_reclaim_gfp ;
   void *journal_info ;
   struct bio_list *bio_list ;
   struct blk_plug *plug ;
   struct reclaim_state *reclaim_state ;
   struct backing_dev_info *backing_dev_info ;
   struct io_context *io_context ;
   unsigned long ptrace_message ;
   siginfo_t *last_siginfo ;
   struct task_io_accounting ioac ;
   u64 acct_rss_mem1 ;
   u64 acct_vm_mem1 ;
   cputime_t acct_timexpd ;
   nodemask_t mems_allowed ;
   seqcount_t mems_allowed_seq ;
   int cpuset_mem_spread_rotor ;
   int cpuset_slab_spread_rotor ;
   struct css_set *cgroups ;
   struct list_head cg_list ;
   struct robust_list_head *robust_list ;
   struct compat_robust_list_head *compat_robust_list ;
   struct list_head pi_state_list ;
   struct futex_pi_state *pi_state_cache ;
   struct perf_event_context *perf_event_ctxp[2U] ;
   struct mutex perf_event_mutex ;
   struct list_head perf_event_list ;
   struct mempolicy *mempolicy ;
   short il_next ;
   short pref_node_fork ;
   int numa_scan_seq ;
   unsigned int numa_scan_period ;
   unsigned int numa_scan_period_max ;
   int numa_preferred_nid ;
   int numa_migrate_deferred ;
   unsigned long numa_migrate_retry ;
   u64 node_stamp ;
   struct callback_head numa_work ;
   struct list_head numa_entry ;
   struct numa_group *numa_group ;
   unsigned long *numa_faults ;
   unsigned long total_numa_faults ;
   unsigned long *numa_faults_buffer ;
   unsigned long numa_faults_locality[2U] ;
   unsigned long numa_pages_migrated ;
   struct callback_head rcu ;
   struct pipe_inode_info *splice_pipe ;
   struct page_frag task_frag ;
   struct task_delay_info *delays ;
   int make_it_fail ;
   int nr_dirtied ;
   int nr_dirtied_pause ;
   unsigned long dirty_paused_when ;
   int latency_record_count ;
   struct latency_record latency_record[32U] ;
   unsigned long timer_slack_ns ;
   unsigned long default_timer_slack_ns ;
   int curr_ret_stack ;
   struct ftrace_ret_stack *ret_stack ;
   unsigned long long ftrace_timestamp ;
   atomic_t trace_overrun ;
   atomic_t tracing_graph_pause ;
   unsigned long trace ;
   unsigned long trace_recursion ;
   struct memcg_batch_info memcg_batch ;
   unsigned int memcg_kmem_skip_account ;
   struct memcg_oom_info memcg_oom ;
   struct uprobe_task *utask ;
   unsigned int sequential_io ;
   unsigned int sequential_io_avg ;
};

#line 263  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/pm_runtime.h"
struct usb_driver;

#line 265 
struct ep_device;

#line 266  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/pm_runtime.h"
struct usb_host_endpoint {
   struct usb_endpoint_descriptor desc ;
   struct usb_ss_ep_comp_descriptor ss_ep_comp ;
   struct list_head urb_list ;
   void *hcpriv ;
   struct ep_device *ep_dev ;
   unsigned char *extra ;
   int extralen ;
   int enabled ;
};

#line 75  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/usb.h"
struct usb_host_interface {
   struct usb_interface_descriptor desc ;
   int extralen ;
   unsigned char *extra ;
   struct usb_host_endpoint *endpoint ;
   char *string ;
};

#line 90 
enum usb_interface_condition {
    USB_INTERFACE_UNBOUND = 0,
    USB_INTERFACE_BINDING = 1,
    USB_INTERFACE_BOUND = 2,
    USB_INTERFACE_UNBINDING = 3
};

#line 97  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/usb.h"
struct usb_interface {
   struct usb_host_interface *altsetting ;
   struct usb_host_interface *cur_altsetting ;
   unsigned int num_altsetting ;
   struct usb_interface_assoc_descriptor *intf_assoc ;
   int minor ;
   enum usb_interface_condition condition ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) sysfs_files_created : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) ep_devs_created : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) unregistering : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) needs_remote_wakeup : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) needs_altsetting0 : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) needs_binding : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) reset_running : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) resetting_device : 1 ;
   struct device dev ;
   struct device *usb_dev ;
   atomic_t pm_usage_cnt ;
   struct work_struct reset_ws ;
};

#line 785  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/usb.h"
struct usb_dynids {
   spinlock_t lock ;
   struct list_head list ;
};

#line 973  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/usb.h"
struct usbdrv_wrap {
   struct device_driver driver ;
   int for_devices ;
};

#line 983  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/usb.h"
struct usb_driver {
   char const *name ;
   int (*probe)(struct usb_interface *, struct usb_device_id const *) ;
   void (*disconnect)(struct usb_interface *) ;
   int (*unlocked_ioctl)(struct usb_interface *, unsigned int , void *) ;
   int (*suspend)(struct usb_interface *, pm_message_t ) ;
   int (*resume)(struct usb_interface *) ;
   int (*reset_resume)(struct usb_interface *) ;
   int (*pre_reset)(struct usb_interface *) ;
   int (*post_reset)(struct usb_interface *) ;
   struct usb_device_id const *id_table ;
   struct usb_dynids dynids ;
   struct usbdrv_wrap drvwrap ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) no_dynamic_id : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) supports_autosuspend : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) disable_hub_initiated_lpm : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) soft_unbind : 1 ;
};

#line 62  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/memory.h"
struct ldv_list_element {
   void *data ;
   struct ldv_list_element *next ;
};

#line 26  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/memlist.h"
typedef struct ldv_list_element *ldv_list_ptr;

#line 41  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/nondet.h"
struct device_private {
   void *driver_data ;
};

#line 146  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/types.h"
typedef u64 dma_addr_t;

#line 355  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/slab.h"
struct kmem_cache_cpu {
   void **freelist ;
   unsigned long tid ;
   struct page *page ;
   struct page *partial ;
   unsigned int stat[26U] ;
};

#line 48  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/slub_def.h"
struct kmem_cache_order_objects {
   unsigned long x ;
};

#line 58 
struct memcg_cache_params;

#line 58 
struct kmem_cache_node;

#line 58  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/slub_def.h"
struct kmem_cache {
   struct kmem_cache_cpu *cpu_slab ;
   unsigned long flags ;
   unsigned long min_partial ;
   int size ;
   int object_size ;
   int offset ;
   int cpu_partial ;
   struct kmem_cache_order_objects oo ;
   struct kmem_cache_order_objects max ;
   struct kmem_cache_order_objects min ;
   gfp_t allocflags ;
   int refcount ;
   void (*ctor)(void *) ;
   int inuse ;
   int align ;
   int reserved ;
   char const *name ;
   struct list_head list ;
   struct kobject kobj ;
   struct memcg_cache_params *memcg_params ;
   int max_attr_size ;
   int remote_node_defrag_ratio ;
   struct kmem_cache_node *node[1024U] ;
};

#line 497  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/slab.h"
struct __anonstruct_472 {
   struct callback_head callback_head ;
   struct kmem_cache *memcg_caches[0U] ;
};

#line 497  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/slab.h"
struct __anonstruct_473 {
   struct mem_cgroup *memcg ;
   struct list_head list ;
   struct kmem_cache *root_cache ;
   bool dead ;
   atomic_t nr_pages ;
   struct work_struct destroy ;
};

#line 497  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/slab.h"
union __anonunion_471 {
   struct __anonstruct_472 __anonCompField___anonunion_471_33 ;
   struct __anonstruct_473 __anonCompField___anonunion_471_34 ;
};

#line 497  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/slab.h"
struct memcg_cache_params {
   bool is_root_cache ;
   union __anonunion_471 __anonCompField_memcg_cache_params_35 ;
};

#line 54  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/kthread.h"
struct kthread_work;

#line 65  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/kthread.h"
struct kthread_worker {
   spinlock_t lock ;
   struct list_head work_list ;
   struct task_struct *task ;
   struct kthread_work *current_work ;
};

#line 72  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/kthread.h"
struct kthread_work {
   struct list_head node ;
   void (*func)(struct kthread_work *) ;
   wait_queue_head_t done ;
   struct kthread_worker *worker ;
};

#line 33  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/spi/spi.h"
struct spi_master;

#line 33  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/spi/spi.h"
struct spi_device {
   struct device dev ;
   struct spi_master *master ;
   u32 max_speed_hz ;
   u8 chip_select ;
   u8 bits_per_word ;
   u16 mode ;
   int irq ;
   void *controller_state ;
   void *controller_data ;
   char modalias[32U] ;
   int cs_gpio ;
};

#line 152 
struct spi_message;

#line 153 
struct spi_transfer;

#line 210  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/spi/spi.h"
struct spi_master {
   struct device dev ;
   struct list_head list ;
   s16 bus_num ;
   u16 num_chipselect ;
   u16 dma_alignment ;
   u16 mode_bits ;
   u32 bits_per_word_mask ;
   u32 min_speed_hz ;
   u32 max_speed_hz ;
   u16 flags ;
   spinlock_t bus_lock_spinlock ;
   struct mutex bus_lock_mutex ;
   bool bus_lock_flag ;
   int (*setup)(struct spi_device *) ;
   int (*transfer)(struct spi_device *, struct spi_message *) ;
   void (*cleanup)(struct spi_device *) ;
   bool queued ;
   struct kthread_worker kworker ;
   struct task_struct *kworker_task ;
   struct kthread_work pump_messages ;
   spinlock_t queue_lock ;
   struct list_head queue ;
   struct spi_message *cur_msg ;
   bool busy ;
   bool running ;
   bool rt ;
   bool auto_runtime_pm ;
   bool cur_msg_prepared ;
   struct completion xfer_completion ;
   int (*prepare_transfer_hardware)(struct spi_master *) ;
   int (*transfer_one_message)(struct spi_master *, struct spi_message *) ;
   int (*unprepare_transfer_hardware)(struct spi_master *) ;
   int (*prepare_message)(struct spi_master *, struct spi_message *) ;
   int (*unprepare_message)(struct spi_master *, struct spi_message *) ;
   void (*set_cs)(struct spi_device *, bool ) ;
   int (*transfer_one)(struct spi_master *, struct spi_device *, struct spi_transfer *) ;
   int *cs_gpios ;
};

#line 475  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/spi/spi.h"
struct spi_transfer {
   void const *tx_buf ;
   void *rx_buf ;
   unsigned int len ;
   dma_addr_t tx_dma ;
   dma_addr_t rx_dma ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) cs_change : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(3))) tx_nbits : 3 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(3))) rx_nbits : 3 ;
   u8 bits_per_word ;
   u16 delay_usecs ;
   u32 speed_hz ;
   struct list_head transfer_list ;
};

#line 595  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/spi/spi.h"
struct spi_message {
   struct list_head transfers ;
   struct spi_device *spi ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) is_dma_mapped : 1 ;
   void (*complete)(void *) ;
   void *context ;
   unsigned int frame_length ;
   unsigned int actual_length ;
   int status ;
   struct list_head queue ;
   void *state ;
};

#line 34  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/linux/types.h"
typedef __u32 __le32;

#line 253  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/linux/usb/ch9.h"
struct usb_device_descriptor {
   __u8 bLength ;
   __u8 bDescriptorType ;
   __le16 bcdUSB ;
   __u8 bDeviceClass ;
   __u8 bDeviceSubClass ;
   __u8 bDeviceProtocol ;
   __u8 bMaxPacketSize0 ;
   __le16 idVendor ;
   __le16 idProduct ;
   __le16 bcdDevice ;
   __u8 iManufacturer ;
   __u8 iProduct ;
   __u8 iSerialNumber ;
   __u8 bNumConfigurations ;
};

#line 275  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/linux/usb/ch9.h"
struct usb_config_descriptor {
   __u8 bLength ;
   __u8 bDescriptorType ;
   __le16 wTotalLength ;
   __u8 bNumInterfaces ;
   __u8 bConfigurationValue ;
   __u8 iConfiguration ;
   __u8 bmAttributes ;
   __u8 bMaxPower ;
};

#line 751  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/linux/usb/ch9.h"
struct usb_bos_descriptor {
   __u8 bLength ;
   __u8 bDescriptorType ;
   __le16 wTotalLength ;
   __u8 bNumDeviceCaps ;
};

#line 801  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/linux/usb/ch9.h"
struct usb_ext_cap_descriptor {
   __u8 bLength ;
   __u8 bDescriptorType ;
   __u8 bDevCapabilityType ;
   __le32 bmAttributes ;
};

#line 811  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/linux/usb/ch9.h"
struct usb_ss_cap_descriptor {
   __u8 bLength ;
   __u8 bDescriptorType ;
   __u8 bDevCapabilityType ;
   __u8 bmAttributes ;
   __le16 wSpeedSupported ;
   __u8 bFunctionalitySupport ;
   __u8 bU1devExitLat ;
   __le16 bU2DevExitLat ;
};

#line 840  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/uapi/linux/usb/ch9.h"
struct usb_ss_container_id_descriptor {
   __u8 bLength ;
   __u8 bDescriptorType ;
   __u8 bDevCapabilityType ;
   __u8 bReserved ;
   __u8 ContainerID[16U] ;
};

#line 905 
enum usb_device_speed {
    USB_SPEED_UNKNOWN = 0,
    USB_SPEED_LOW = 1,
    USB_SPEED_FULL = 2,
    USB_SPEED_HIGH = 3,
    USB_SPEED_WIRELESS = 4,
    USB_SPEED_SUPER = 5
};

#line 914 
enum usb_device_state {
    USB_STATE_NOTATTACHED = 0,
    USB_STATE_ATTACHED = 1,
    USB_STATE_POWERED = 2,
    USB_STATE_RECONNECTING = 3,
    USB_STATE_UNAUTHENTICATED = 4,
    USB_STATE_DEFAULT = 5,
    USB_STATE_ADDRESS = 6,
    USB_STATE_CONFIGURED = 7,
    USB_STATE_SUSPENDED = 8
};

#line 262  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/pm_runtime.h"
struct usb_device;

#line 264 
struct wusb_dev;

#line 204  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/usb.h"
struct usb_interface_cache {
   unsigned int num_altsetting ;
   struct kref ref ;
   struct usb_host_interface altsetting[0U] ;
};

#line 231  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/usb.h"
struct usb_host_config {
   struct usb_config_descriptor desc ;
   char *string ;
   struct usb_interface_assoc_descriptor *intf_assoc[16U] ;
   struct usb_interface *interface[32U] ;
   struct usb_interface_cache *intf_cache[32U] ;
   unsigned char *extra ;
   int extralen ;
};

#line 295  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/usb.h"
struct usb_host_bos {
   struct usb_bos_descriptor *desc ;
   struct usb_ext_cap_descriptor *ext_cap ;
   struct usb_ss_cap_descriptor *ss_cap ;
   struct usb_ss_container_id_descriptor *ss_id ;
};

#line 307  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/usb.h"
struct usb_devmap {
   unsigned long devicemap[2U] ;
};

#line 319 
struct mon_bus;

#line 319  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/usb.h"
struct usb_bus {
   struct device *controller ;
   int busnum ;
   char const *bus_name ;
   u8 uses_dma ;
   u8 uses_pio_for_control ;
   u8 otg_port ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) is_b_host : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) b_hnp_enable : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) no_stop_on_short : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) no_sg_constraint : 1 ;
   unsigned int sg_tablesize ;
   int devnum_next ;
   struct usb_devmap devmap ;
   struct usb_device *root_hub ;
   struct usb_bus *hs_companion ;
   struct list_head bus_list ;
   int bandwidth_allocated ;
   int bandwidth_int_reqs ;
   int bandwidth_isoc_reqs ;
   unsigned int resuming_ports ;
   struct mon_bus *mon_bus ;
   int monitored ;
};

#line 367 
struct usb_tt;

#line 368 
enum usb_device_removable {
    USB_DEVICE_REMOVABLE_UNKNOWN = 0,
    USB_DEVICE_REMOVABLE = 1,
    USB_DEVICE_FIXED = 2
};

#line 381  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/usb.h"
struct usb2_lpm_parameters {
   unsigned int besl ;
   int timeout ;
};

#line 401  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/usb.h"
struct usb3_lpm_parameters {
   unsigned int mel ;
   unsigned int pel ;
   unsigned int sel ;
   int timeout ;
};

#line 440  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/usb.h"
struct usb_device {
   int devnum ;
   char devpath[16U] ;
   u32 route ;
   enum usb_device_state state ;
   enum usb_device_speed speed ;
   struct usb_tt *tt ;
   int ttport ;
   unsigned int toggle[2U] ;
   struct usb_device *parent ;
   struct usb_bus *bus ;
   struct usb_host_endpoint ep0 ;
   struct device dev ;
   struct usb_device_descriptor descriptor ;
   struct usb_host_bos *bos ;
   struct usb_host_config *config ;
   struct usb_host_config *actconfig ;
   struct usb_host_endpoint *ep_in[16U] ;
   struct usb_host_endpoint *ep_out[16U] ;
   char **rawdescriptors ;
   unsigned short bus_mA ;
   u8 portnum ;
   u8 level ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) can_submit : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) persist_enabled : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) have_langid : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) authorized : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) authenticated : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) wusb : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) lpm_capable : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) usb2_hw_lpm_capable : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) usb2_hw_lpm_besl_capable : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) usb2_hw_lpm_enabled : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) usb2_hw_lpm_allowed : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) usb3_lpm_enabled : 1 ;
   int string_langid ;
   char *product ;
   char *manufacturer ;
   char *serial ;
   struct list_head filelist ;
   int maxchild ;
   u32 quirks ;
   atomic_t urbnum ;
   unsigned long active_duration ;
   unsigned long connect_time ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) do_remote_wakeup : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) reset_resume : 1 ;
   unsigned int __attribute__((__FRAMA_C_BITFIELD_SIZE__(1))) port_is_suspended : 1 ;
   struct wusb_dev *wusb_dev ;
   int slot_id ;
   enum usb_device_removable removable ;
   struct usb2_lpm_parameters l1_params ;
   struct usb3_lpm_parameters u1_params ;
   struct usb3_lpm_parameters u2_params ;
   unsigned int lpm_disable_count ;
};

#line 1847  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/usb.h"
struct ldv_struct_usb_scenario_4 {
   struct usb_driver *arg0 ;
   int signal_pending ;
};

#line 33  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/export.h"
extern struct module __this_module;


#line 1139  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/include/linux/usb.h"
static int ldv_usb_register_driver_17(struct usb_driver *ldv_func_arg1, struct module *ldv_func_arg2, char const *ldv_func_arg3);


#line 1143 
static int ldv_usb_register_driver_18(struct usb_driver *ldv_func_arg1, struct module *ldv_func_arg2, char const *ldv_func_arg3);


#line 1153 
static void ldv_usb_deregister_19(struct usb_driver *ldv_func_arg1);


#line 23  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever/presets/jobs/specifications/verifier/common.h"
void __VERIFIER_assume(int);


#line 22  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/tmp/tmplfnrdhiw/ext-modules/linux/usb/register/register.c"
static int ldv_usb_probe(struct usb_interface *intf, struct usb_device_id const *id)
{
  int __retres;
  struct usb_driver driver;
  int tmp;
  
#line 27 
  tmp = ldv_usb_register_driver_17(& driver,& __this_module,"register");
  
#line 27 
  __VERIFIER_assume(tmp);
  
#line 29 
  __retres = 0;
  
#line 29 
  return __retres;
}


#line 32  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/tmp/tmplfnrdhiw/ext-modules/linux/usb/register/register.c"
static struct usb_driver ldv_usb_driver = {.name = (char const *)0, .probe = & ldv_usb_probe, .disconnect = (void (*)(struct usb_interface *))0, .unlocked_ioctl = (int (*)(struct usb_interface *, unsigned int , void *))0, .suspend = (int (*)(struct usb_interface *, pm_message_t ))0, .resume = (int (*)(struct usb_interface *))0, .reset_resume = (int (*)(struct usb_interface *))0, .pre_reset = (int (*)(struct usb_interface *))0, .post_reset = (int (*)(struct usb_interface *))0, .id_table = (struct usb_device_id const *)0, .dynids = {.lock = {.__anonCompField_spinlock_20 = {.rlock = {.raw_lock = {.__anonCompField_arch_spinlock_7 = {.head_tail = 0U}}, .magic = 0U, .owner_cpu = 0U, .owner = (void *)0, .dep_map = {.key = (struct lock_class_key *)0, .class_cache = {(struct lock_class *)0, (struct lock_class *)0}, .name = (char const *)0, .cpu = 0, .ip = 0UL}}}}, .list = {.next = (struct list_head *)0, .prev = (struct list_head *)0}}, .drvwrap = {.driver = {.name = (char const *)0, .bus = (struct bus_type *)0, .owner = (struct module *)0, .mod_name = (char const *)0, .suppress_bind_attrs = (_Bool)0, .of_match_table = (struct of_device_id const *)0, .acpi_match_table = (struct acpi_device_id const *)0, .probe = (int (*)(struct device *))0, .remove = (int (*)(struct device *))0, .shutdown = (void (*)(struct device *))0, .suspend = (int (*)(struct device *, pm_message_t ))0, .resume = (int (*)(struct device *))0, .groups = (struct attribute_group const **)0, .pm = (struct dev_pm_ops const *)0, .p = (struct driver_private *)0}, .for_devices = 0}, .no_dynamic_id = 0U, .supports_autosuspend = 0U, .disable_hub_initiated_lpm = 0U, .soft_unbind = 0U};

#line 36  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/tmp/tmplfnrdhiw/ext-modules/linux/usb/register/register.c"
static int ldv_init(void)
{
  int __retres;
  int tmp;
  
#line 38 
  tmp = ldv_usb_register_driver_18(& ldv_usb_driver,& __this_module,"register");
  
#line 38 
  __VERIFIER_assume(tmp == 0);
  
#line 39 
  ldv_usb_deregister_19(& ldv_usb_driver);
  
#line 41 
  __retres = 0;
  
#line 41 
  return __retres;
}


#line 29  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/35/vtg/ext-modules/linux/usb/register/register.ko/linux:usb:register/weaver/.tmp_register.c.aux"
struct usb_driver *ldv_emg_alias_ldv_usb_driver_2 = & ldv_usb_driver;

#line 32 
int ldv_emg_usb_register_driver(struct usb_driver *arg0, struct module *arg1, char *arg2);


#line 33 
void ldv_emg_usb_deregister(struct usb_driver *arg0);


#line 37  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/35/vtg/ext-modules/linux/usb/register/register.ko/linux:usb:register/weaver/.tmp_register.c.aux"
int ldv_emg_wrapper_ldv_usb_probe_2(struct usb_interface *arg0, struct usb_device_id *arg1)
{
  int tmp;
  
#line 38 
  tmp = ldv_usb_probe(arg0,(struct usb_device_id const *)arg1);
  
#line 38 
  return tmp;
}


#line 42  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/35/vtg/ext-modules/linux/usb/register/register.ko/linux:usb:register/weaver/.tmp_register.c.aux"
int ldv_emg_ldv_init(void)
{
  int tmp;
  
#line 43 
  tmp = ldv_init();
  
#line 43 
  return tmp;
}


#line 159  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/35/vtg/ext-modules/linux/usb/register/register.ko/linux:usb:register/weaver/.tmp_register.c.aux"
static int ldv_usb_register_driver_17(struct usb_driver *ldv_func_arg1, struct module *ldv_func_arg2, char const *ldv_func_arg3)
{
  int tmp;
  
#line 163 
  tmp = ldv_emg_usb_register_driver(ldv_func_arg1,ldv_func_arg2,(char *)ldv_func_arg3);
  
#line 163 
  return tmp;
}


#line 167  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/35/vtg/ext-modules/linux/usb/register/register.ko/linux:usb:register/weaver/.tmp_register.c.aux"
static int ldv_usb_register_driver_18(struct usb_driver *ldv_func_arg1, struct module *ldv_func_arg2, char const *ldv_func_arg3)
{
  int tmp;
  
#line 171 
  tmp = ldv_emg_usb_register_driver(ldv_func_arg1,ldv_func_arg2,(char *)ldv_func_arg3);
  
#line 171 
  return tmp;
}


#line 175  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/35/vtg/ext-modules/linux/usb/register/register.ko/linux:usb:register/weaver/.tmp_register.c.aux"
static void ldv_usb_deregister_19(struct usb_driver *ldv_func_arg1)
{
  
#line 179 
  ldv_emg_usb_deregister(ldv_func_arg1);
  
#line 180 
  return;
}


#line 21  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/arch/atomic.c"
void ldv_atomic_add(int i, atomic_t *v)
{
  
#line 23 
  v->counter += i;
  
#line 24 
  return;
}


#line 27  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/arch/atomic.c"
void ldv_atomic_sub(int i, atomic_t *v)
{
  
#line 29 
  v->counter -= i;
  
#line 30 
  return;
}


#line 33  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/arch/atomic.c"
int ldv_atomic_sub_and_test(int i, atomic_t *v)
{
  int __retres;
  
#line 35 
  v->counter -= i;
  
#line 36 
  if (v->counter != 0) {
    
#line 37 
    __retres = 0;
    
#line 37 
    goto return_label;
  }
  else ;
  
#line 39 
  __retres = 1;
  return_label: 
#line 39 
                return __retres;
}


#line 43  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/arch/atomic.c"
void ldv_atomic_inc(atomic_t *v)
{
  
#line 45 
  v->counter += 1;
  
#line 46 
  return;
}


#line 49  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/arch/atomic.c"
void ldv_atomic_dec(atomic_t *v)
{
  
#line 51 
  v->counter -= 1;
  
#line 52 
  return;
}


#line 55  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/arch/atomic.c"
int ldv_atomic_dec_and_test(atomic_t *v)
{
  int __retres;
  
#line 57 
  v->counter -= 1;
  
#line 58 
  if (v->counter != 0) {
    
#line 59 
    __retres = 0;
    
#line 59 
    goto return_label;
  }
  else ;
  
#line 61 
  __retres = 1;
  return_label: 
#line 61 
                return __retres;
}


#line 65  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/arch/atomic.c"
int ldv_atomic_inc_and_test(atomic_t *v)
{
  int __retres;
  
#line 67 
  v->counter += 1;
  
#line 68 
  if (v->counter != 0) {
    
#line 69 
    __retres = 0;
    
#line 69 
    goto return_label;
  }
  else ;
  
#line 71 
  __retres = 1;
  return_label: 
#line 71 
                return __retres;
}


#line 75  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/arch/atomic.c"
int ldv_atomic_add_return(int i, atomic_t *v)
{
  int __retres;
  
#line 77 
  v->counter += i;
  
#line 78 
  __retres = v->counter;
  
#line 78 
  return __retres;
}


#line 82  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/arch/atomic.c"
int ldv_atomic_add_negative(int i, atomic_t *v)
{
  int __retres;
  
#line 84 
  v->counter += i;
  
#line 85 
  __retres = v->counter < 0;
  
#line 85 
  return __retres;
}


#line 89  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/arch/atomic.c"
int ldv_atomic_inc_short(short *v)
{
  int __retres;
  
#line 91 
  *v = (short)((unsigned int)*v + 1U);
  
#line 92 
  __retres = (int)*v;
  
#line 92 
  return __retres;
}


#line 23  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/ldv/device.h"
void *ldv_dev_get_drvdata(struct device const *dev);


#line 24 
int ldv_dev_set_drvdata(struct device *dev, void *data);


#line 30  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/memory.h"
void *ldv_xmalloc(size_t size);


#line 31 
void *ldv_xzalloc(size_t size);


#line 28  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/memlist.h"
struct ldv_list_element global_list = {.data = (void *)0, .next = (struct ldv_list_element *)0};

#line 33  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/memlist.h"
__inline static ldv_list_ptr ldv_list_create(void *data)
{
  
#line 35 
  ldv_list_ptr list = (struct ldv_list_element *)0;
  
#line 37 
  list = (ldv_list_ptr)ldv_xmalloc(16UL);
  
#line 39 
  list->data = data;
  
#line 40 
  list->next = (struct ldv_list_element *)0;
  
#line 42 
  return list;
}


#line 45  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/memlist.h"
__inline static void ldv_save_pointer(void *data)
{
  ldv_list_ptr element;
  ldv_list_ptr cached;
  
#line 50 
  if (global_list.data == (void *)0) {
    
#line 51 
    element = & global_list;
    
#line 52 
    element->data = data;
  }
  else {
    
#line 54 
    element = ldv_list_create(data);
    
#line 55 
    cached = global_list.next;
    
#line 56 
    global_list.next = element;
    
#line 57 
    element->next = cached;
  }
  
#line 60 
  return;
}


#line 28  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/drivers/base/dd.c"
void *ldv_dev_get_drvdata(struct device const *dev)
{
  void *__retres;
  
#line 30 
  if (dev != (struct device const *)0 && dev->p != (struct device_private *)0) {
    
#line 31 
    __retres = (dev->p)->driver_data;
    
#line 31 
    goto return_label;
  }
  else ;
  
#line 33 
  __retres = (void *)0;
  return_label: 
#line 33 
                return __retres;
}


#line 42  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/drivers/base/dd.c"
int ldv_dev_set_drvdata(struct device *dev, void *data)
{
  int __retres;
  
#line 44 
  dev->p = (struct device_private *)ldv_xzalloc(8UL);
  
#line 45 
  ldv_save_pointer((void *)dev->p);
  
#line 46 
  (dev->p)->driver_data = data;
  
#line 48 
  __retres = 0;
  
#line 48 
  return __retres;
}


#line 25  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/memory.h"
void *ldv_zalloc(size_t size);


#line 23  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/drivers/spi.c"
struct spi_master *ldv_spi_alloc_master(struct device *host, unsigned int size)
{
  struct spi_master *__retres;
  struct spi_master *master;
  
#line 27 
  master = (struct spi_master *)ldv_zalloc((unsigned long)size + 2200UL);
  
#line 29 
  if (master == (struct spi_master *)0) {
    
#line 30 
    __retres = (struct spi_master *)0;
    
#line 30 
    goto return_label;
  }
  else ;
  
#line 32 
  ldv_dev_set_drvdata(& master->dev,(void *)(master + 1U));
  
#line 34 
  __retres = master;
  return_label: 
#line 34 
                return __retres;
}


#line 27  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/ldv/err.h"
long ldv_is_err(void const *ptr);


#line 28 
long ldv_is_err_or_null(void const *ptr);


#line 29 
void *ldv_err_ptr(long error);


#line 30 
long ldv_ptr_err(void const *ptr);


#line 21  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/err.c"
long ldv_is_err(void const *ptr)
{
  long __retres;
  
#line 23 
  __retres = (long)((unsigned long)ptr > 4294967295UL);
  
#line 23 
  return __retres;
}


#line 26  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/err.c"
void *ldv_err_ptr(long error)
{
  void *__retres;
  
#line 28 
  __VERIFIER_assume(error < 0L);
  
#line 29 
  __retres = (void *)(4294967295L - error);
  
#line 29 
  return __retres;
}


#line 32  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/err.c"
long ldv_ptr_err(void const *ptr)
{
  long __retres;
  
#line 34 
  __VERIFIER_assume((unsigned long)ptr > 4294967295UL);
  
#line 35 
  __retres = (long)(4294967295UL - (unsigned long)ptr);
  
#line 35 
  return __retres;
}


#line 38  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/err.c"
long ldv_is_err_or_null(void const *ptr)
{
  long __retres;
  int tmp_0;
  
#line 40 
  if (ptr == (void const *)0) 
#line 40 
                              tmp_0 = 1;
  else {
    long tmp;
    
#line 40 
    tmp = ldv_is_err(ptr);
    
#line 40 
    if (tmp != 0L) 
#line 40 
                   tmp_0 = 1; else 
#line 40 
                                   tmp_0 = 0;
  }
  
#line 40 
  __retres = (long)tmp_0;
  
#line 40 
  return __retres;
}


#line 21  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/ldv/panic.h"
void ldv_panic(void);


#line 21  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/kernel/panic.c"
void ldv_panic(void)
{
  
#line 23 
  __VERIFIER_assume(0);
  
#line 24 
  return;
}


#line 32  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/ldv/common.h"
void ldv_switch_to_interrupt_context(void);


#line 42 
void ldv_switch_to_process_context(void);


#line 50 
bool ldv_in_interrupt_context(void);


#line 112 
int ldv_post_init(int init_ret_val);


#line 132 
int ldv_post_probe(int probe_ret_val);


#line 133 
void ldv_check_return_value_probe(int retval);


#line 141 
int ldv_filter_err_code(int ret_val);


#line 25  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/ldv/common.c"
static bool __ldv_in_interrupt_context = (_Bool)0;

#line 28  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/ldv/common.c"
void ldv_switch_to_interrupt_context(void)
{
  
#line 30 
  __ldv_in_interrupt_context = (_Bool)1;
  
#line 31 
  return;
}


#line 34  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/ldv/common.c"
void ldv_switch_to_process_context(void)
{
  
#line 36 
  __ldv_in_interrupt_context = (_Bool)0;
  
#line 37 
  return;
}


#line 39  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/ldv/common.c"
bool ldv_in_interrupt_context(void)
{
  
#line 41 
  return __ldv_in_interrupt_context;
}


#line 44  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/ldv/common.c"
static int ldv_filter_positive_int(int val)
{
  
#line 46 
  __VERIFIER_assume(val <= 0);
  
#line 47 
  return val;
}


#line 54  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/ldv/common.c"
int ldv_post_init(int init_ret_val)
{
  int tmp;
  
#line 56 
  tmp = ldv_filter_positive_int(init_ret_val);
  
#line 56 
  return tmp;
}


#line 60  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/ldv/common.c"
int ldv_post_probe(int probe_ret_val)
{
  int tmp;
  
#line 62 
  ldv_check_return_value_probe(probe_ret_val);
  
#line 63 
  tmp = ldv_filter_positive_int(probe_ret_val);
  
#line 63 
  return tmp;
}


#line 67  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/ldv/common.c"
int ldv_filter_err_code(int ret_val)
{
  int tmp;
  
#line 69 
  tmp = ldv_filter_positive_int(ret_val);
  
#line 69 
  return tmp;
}


#line 23  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/ldv/slab.h"
void *ldv_kzalloc(size_t size, gfp_t flags);


#line 24 
void *ldv_kmalloc(size_t size, gfp_t flags);


#line 25 
void *ldv_kcalloc(size_t n, size_t size, gfp_t flags);


#line 26 
void *ldv_kmalloc_array(size_t n, size_t size, gfp_t flags);


#line 28 
void ldv_check_alloc_flags(gfp_t);


#line 29 
void ldv_after_alloc(void *);


#line 23  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/memory.h"
void *ldv_malloc(size_t size);


#line 24 
void *ldv_calloc(size_t nmemb, size_t size);


#line 21  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/mm/slab.c"
void *ldv_kmalloc(size_t size, gfp_t flags)
{
  void *res;
  
#line 25 
  ldv_check_alloc_flags(flags);
  
#line 26 
  res = ldv_malloc(size);
  
#line 27 
  ldv_after_alloc(res);
  
#line 29 
  return res;
}


#line 32  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/mm/slab.c"
void *ldv_kcalloc(size_t n, size_t size, gfp_t flags)
{
  void *res;
  
#line 36 
  ldv_check_alloc_flags(flags);
  
#line 37 
  res = ldv_calloc(n,size);
  
#line 38 
  ldv_after_alloc(res);
  
#line 40 
  return res;
}


#line 43  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/mm/slab.c"
void *ldv_kzalloc(size_t size, gfp_t flags)
{
  void *res;
  
#line 47 
  ldv_check_alloc_flags(flags);
  
#line 48 
  res = ldv_zalloc(size);
  
#line 49 
  ldv_after_alloc(res);
  
#line 51 
  return res;
}


#line 54  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/mm/slab.c"
void *ldv_kmalloc_array(size_t n, size_t size, gfp_t flags)
{
  void *res;
  
#line 58 
  ldv_check_alloc_flags(flags);
  
#line 59 
  res = ldv_malloc(n * size);
  
#line 60 
  ldv_after_alloc(res);
  
#line 62 
  return res;
}


#line 1  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/35/vtg/ext-modules/linux/usb/register/register.ko/linux:usb:register/rsg/models/register.bk.c"
void ldv_assert_linux_usb_register__wrong_return_value(int expr);


#line 87  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/ldv/common.h"
void ldv_failed_usb_register_driver(void);


#line 123 
void ldv_pre_probe(void);


#line 30  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/usb/register.c"
int ldv_probe_state = 0;

#line 33  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/usb/register.c"
void ldv_failed_usb_register_driver(void)
{
  
#line 36 
  ldv_probe_state = 1;
  
#line 37 
  return;
}


#line 40  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/usb/register.c"
void ldv_reset_error_counter(void)
{
  
#line 43 
  ldv_probe_state = 0;
  
#line 44 
  return;
}


#line 47  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/usb/register.c"
void ldv_pre_probe(void)
{
  
#line 49 
  ldv_reset_error_counter();
  
#line 50 
  return;
}


#line 59  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/usb/register.c"
void ldv_check_return_value_probe(int retval)
{
  
#line 61 
  if (ldv_probe_state == 1) 
#line 63 
                            ldv_assert_linux_usb_register__wrong_return_value(retval != 0); else ;
  
#line 66 
  ldv_reset_error_counter();
  
#line 67 
  return;
}


#line 26  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/memory.h"
void ldv_free(void *s);


#line 35 
void *ldv_malloc_unknown_size(void);


#line 36 
void *ldv_calloc_unknown_size(void);


#line 37 
void *ldv_zalloc_unknown_size(void);


#line 40 
void *ldv_reference_malloc(size_t size);


#line 41 
void *ldv_reference_calloc(size_t nmemb, size_t size);


#line 42 
void *ldv_reference_zalloc(size_t size);


#line 43 
void ldv_reference_free(void *s);


#line 47 
void *ldv_reference_xmalloc(size_t size);


#line 48 
void *ldv_reference_xzalloc(size_t size);


#line 52 
void *ldv_reference_malloc_unknown_size(void);


#line 53 
void *ldv_reference_calloc_unknown_size(void);


#line 54 
void *ldv_reference_zalloc_unknown_size(void);


#line 61 
void *ldv_xmalloc_unknown_size(size_t size);


#line 32  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/verifier/memory.c"
void *ldv_reference_xmalloc_unknown_size(size_t size);


#line 34  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/verifier/memory.c"
void *ldv_malloc(size_t size)
{
  void *res;
  
#line 37 
  res = ldv_reference_malloc(size);
  
#line 38 
  if (res != (void *)0) {
    long tmp;
    
#line 39 
    tmp = ldv_is_err((void const *)res);
    
#line 39 
    __VERIFIER_assume(tmp == 0L);
  }
  else ;
  
#line 40 
  return res;
}


#line 43  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/verifier/memory.c"
void *ldv_calloc(size_t nmemb, size_t size)
{
  void *res;
  
#line 46 
  res = ldv_reference_calloc(nmemb,size);
  
#line 47 
  if (res != (void *)0) {
    long tmp;
    
#line 48 
    tmp = ldv_is_err((void const *)res);
    
#line 48 
    __VERIFIER_assume(tmp == 0L);
  }
  else ;
  
#line 49 
  return res;
}


#line 52  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/verifier/memory.c"
void *ldv_zalloc(size_t size)
{
  void *res;
  
#line 55 
  res = ldv_reference_zalloc(size);
  
#line 56 
  if (res != (void *)0) {
    long tmp;
    
#line 57 
    tmp = ldv_is_err((void const *)res);
    
#line 57 
    __VERIFIER_assume(tmp == 0L);
  }
  else ;
  
#line 58 
  return res;
}


#line 61  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/verifier/memory.c"
void ldv_free(void *s)
{
  
#line 63 
  ldv_reference_free(s);
  
#line 64 
  return;
}


#line 66  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/verifier/memory.c"
void *ldv_xmalloc(size_t size)
{
  void *res;
  long tmp;
  
#line 69 
  res = ldv_reference_xmalloc(size);
  
#line 70 
  tmp = ldv_is_err((void const *)res);
  
#line 70 
  __VERIFIER_assume(tmp == 0L);
  
#line 71 
  return res;
}


#line 74  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/verifier/memory.c"
void *ldv_xzalloc(size_t size)
{
  void *res;
  long tmp;
  
#line 77 
  res = ldv_reference_xzalloc(size);
  
#line 78 
  tmp = ldv_is_err((void const *)res);
  
#line 78 
  __VERIFIER_assume(tmp == 0L);
  
#line 79 
  return res;
}


#line 82  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/verifier/memory.c"
void *ldv_malloc_unknown_size(void)
{
  void *res;
  
#line 85 
  res = ldv_reference_malloc_unknown_size();
  
#line 86 
  if (res != (void *)0) {
    long tmp;
    
#line 87 
    tmp = ldv_is_err((void const *)res);
    
#line 87 
    __VERIFIER_assume(tmp == 0L);
  }
  else ;
  
#line 88 
  return res;
}


#line 91  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/verifier/memory.c"
void *ldv_calloc_unknown_size(void)
{
  void *res;
  
#line 94 
  res = ldv_reference_calloc_unknown_size();
  
#line 95 
  if (res != (void *)0) {
    long tmp;
    
#line 96 
    tmp = ldv_is_err((void const *)res);
    
#line 96 
    __VERIFIER_assume(tmp == 0L);
  }
  else ;
  
#line 97 
  return res;
}


#line 100  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/verifier/memory.c"
void *ldv_zalloc_unknown_size(void)
{
  void *res;
  
#line 103 
  res = ldv_reference_zalloc_unknown_size();
  
#line 104 
  if (res != (void *)0) {
    long tmp;
    
#line 105 
    tmp = ldv_is_err((void const *)res);
    
#line 105 
    __VERIFIER_assume(tmp == 0L);
  }
  else ;
  
#line 106 
  return res;
}


#line 109  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/verifier/memory.c"
void *ldv_xmalloc_unknown_size(size_t size)
{
  void *res;
  long tmp;
  
#line 112 
  res = ldv_reference_xmalloc_unknown_size(size);
  
#line 113 
  tmp = ldv_is_err((void const *)res);
  
#line 113 
  __VERIFIER_assume(tmp == 0L);
  
#line 114 
  return res;
}

long __builtin_expect(long exp, long c);


#line 22  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/common.h"
void __VERIFIER_error(void);


#line 24  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/gcc.c"
long __builtin_expect(long exp, long c)
{
  
#line 26 
  return exp;
}


#line 35  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/gcc.c"
void __builtin_trap(void)
{
  
#line 37 
  __VERIFIER_error();
  
#line 38 
  return;
}


#line 23  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/nondet.h"
int ldv_undef_int(void);


#line 24 
int ldv_undef_long(void);


#line 25 
unsigned int ldv_undef_uint(void);


#line 26 
unsigned long ldv_undef_ulong(void);


#line 27 
unsigned long long ldv_undef_ulonglong(void);


#line 28 
void *ldv_undef_ptr(void);


#line 31 
int ldv_undef_int_positive(void);


#line 34 
int ldv_undef_int_negative(void);


#line 37 
int ldv_undef_int_nonpositive(void);


#line 40 
void *ldv_undef_ptr_non_null(void);


#line 29  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/nondet.c"
int __VERIFIER_nondet_int(void);


#line 31 
long __VERIFIER_nondet_long(void);


#line 38 
unsigned int __VERIFIER_nondet_uint(void);


#line 41 
unsigned long __VERIFIER_nondet_ulong(void);


#line 42 
unsigned long long __VERIFIER_nondet_ulonglong(void);


#line 43 
void *__VERIFIER_nondet_pointer(void);


#line 46  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/nondet.c"
int ldv_undef_int(void)
{
  int tmp;
  
#line 48 
  tmp = __VERIFIER_nondet_int();
  
#line 48 
  return tmp;
}


#line 51  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/nondet.c"
int ldv_undef_long(void)
{
  int __retres;
  long tmp;
  
#line 53 
  tmp = __VERIFIER_nondet_long();
  
#line 53 
  __retres = (int)tmp;
  
#line 53 
  return __retres;
}


#line 56  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/nondet.c"
unsigned int ldv_undef_uint(void)
{
  unsigned int tmp;
  
#line 58 
  tmp = __VERIFIER_nondet_uint();
  
#line 58 
  return tmp;
}


#line 61  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/nondet.c"
void *ldv_undef_ptr(void)
{
  void *tmp;
  
#line 63 
  tmp = __VERIFIER_nondet_pointer();
  
#line 63 
  return tmp;
}


#line 66  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/nondet.c"
unsigned long ldv_undef_ulong(void)
{
  unsigned long tmp;
  
#line 68 
  tmp = __VERIFIER_nondet_ulong();
  
#line 68 
  return tmp;
}


#line 71  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/nondet.c"
unsigned long long ldv_undef_ulonglong(void)
{
  unsigned long long tmp;
  
#line 73 
  tmp = __VERIFIER_nondet_ulonglong();
  
#line 73 
  return tmp;
}


#line 76  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/nondet.c"
int ldv_undef_int_positive(void)
{
  
#line 78 
  int ret = ldv_undef_int();
  
#line 80 
  __VERIFIER_assume(ret > 0);
  
#line 82 
  return ret;
}


#line 85  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/nondet.c"
int ldv_undef_int_negative(void)
{
  
#line 87 
  int ret = ldv_undef_int();
  
#line 89 
  __VERIFIER_assume(ret < 0);
  
#line 91 
  return ret;
}


#line 94  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/nondet.c"
int ldv_undef_int_nonpositive(void)
{
  
#line 96 
  int ret = ldv_undef_int();
  
#line 98 
  __VERIFIER_assume(ret <= 0);
  
#line 100 
  return ret;
}


#line 103  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/nondet.c"
void *ldv_undef_ptr_non_null(void)
{
  
#line 105 
  void *ret = ldv_undef_ptr();
  
#line 107 
  __VERIFIER_assume(ret != (void *)0);
  
#line 109 
  return ret;
}


#line 33  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/memory.h"
void *external_allocated_data(void);


#line 45 
void *ldv_reference_realloc(void *ptr, size_t size);


#line 23  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/reference memory.c"
void *malloc(size_t);


#line 24 
void *calloc(size_t, size_t);


#line 25 
void free(void *);


#line 28 
void *memcpy(void *, void const *, size_t);


#line 31 
void *memset(void *, int, size_t);


#line 33  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/reference memory.c"
void *ldv_reference_malloc(size_t size)
{
  void *__retres;
  void *res;
  int tmp;
  
#line 37 
  tmp = ldv_undef_int();
  
#line 37 
  if (tmp != 0) {
    
#line 39 
    res = malloc(size);
    
#line 40 
    __VERIFIER_assume(res != (void *)0);
    
#line 41 
    __retres = res;
    
#line 41 
    goto return_label;
  }
  else {
    
#line 44 
    __retres = (void *)0;
    
#line 44 
    goto return_label;
  }
  return_label: 
#line 37 
                return __retres;
}


#line 47  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/reference memory.c"
void *ldv_reference_calloc(size_t nmemb, size_t size)
{
  void *tmp;
  
#line 49 
  tmp = calloc(nmemb,size);
  
#line 49 
  return tmp;
}


#line 52  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/reference memory.c"
void *ldv_reference_zalloc(size_t size)
{
  void *tmp;
  
#line 54 
  tmp = calloc(1UL,size);
  
#line 54 
  return tmp;
}


#line 57  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/reference memory.c"
void ldv_reference_free(void *s)
{
  
#line 59 
  free(s);
  
#line 60 
  return;
}


#line 62  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/reference memory.c"
void *ldv_reference_realloc(void *ptr, size_t size)
{
  void *__retres;
  void *res;
  int tmp;
  
#line 66 
  if (ptr != (void *)0 && size == 0UL) {
    
#line 67 
    free(ptr);
    
#line 68 
    __retres = (void *)0;
    
#line 68 
    goto return_label;
  }
  else ;
  
#line 71 
  if (ptr == (void *)0) {
    
#line 72 
    res = malloc(size);
    
#line 73 
    __retres = res;
    
#line 73 
    goto return_label;
  }
  else ;
  
#line 76 
  tmp = ldv_undef_int();
  
#line 76 
  if (tmp != 0) {
    
#line 78 
    res = malloc(size);
    
#line 79 
    __VERIFIER_assume(res != (void *)0);
    
#line 81 
    memcpy(res,(void const *)ptr,size);
    
#line 82 
    free(ptr);
    
#line 84 
    __retres = res;
    
#line 84 
    goto return_label;
  }
  else {
    
#line 87 
    __retres = (void *)0;
    
#line 87 
    goto return_label;
  }
  return_label: 
#line 76 
                return __retres;
}


#line 90  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/reference memory.c"
void *ldv_reference_xmalloc(size_t size)
{
  void *res;
  
#line 94 
  res = malloc(size);
  
#line 95 
  __VERIFIER_assume(res != (void *)0);
  
#line 97 
  return res;
}


#line 100  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/reference memory.c"
void *ldv_reference_xzalloc(size_t size)
{
  void *res;
  
#line 104 
  res = calloc(1UL,size);
  
#line 105 
  __VERIFIER_assume(res != (void *)0);
  
#line 107 
  return res;
}


#line 110  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/reference memory.c"
void *ldv_reference_malloc_unknown_size(void)
{
  void *__retres;
  void *res;
  int tmp;
  
#line 114 
  tmp = ldv_undef_int();
  
#line 114 
  if (tmp != 0) {
    
#line 115 
    res = external_allocated_data();
    
#line 116 
    __VERIFIER_assume(res != (void *)0);
    
#line 117 
    __retres = res;
    
#line 117 
    goto return_label;
  }
  else {
    
#line 120 
    __retres = (void *)0;
    
#line 120 
    goto return_label;
  }
  return_label: 
#line 114 
                return __retres;
}


#line 123  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/reference memory.c"
void *ldv_reference_calloc_unknown_size(void)
{
  void *__retres;
  void *res;
  int tmp;
  
#line 127 
  tmp = ldv_undef_int();
  
#line 127 
  if (tmp != 0) {
    
#line 128 
    res = external_allocated_data();
    
#line 129 
    memset(res,0,8UL);
    
#line 130 
    __VERIFIER_assume(res != (void *)0);
    
#line 131 
    __retres = res;
    
#line 131 
    goto return_label;
  }
  else {
    
#line 134 
    __retres = (void *)0;
    
#line 134 
    goto return_label;
  }
  return_label: 
#line 127 
                return __retres;
}


#line 137  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/reference memory.c"
void *ldv_reference_zalloc_unknown_size(void)
{
  void *tmp;
  
#line 139 
  tmp = ldv_reference_calloc_unknown_size();
  
#line 139 
  return tmp;
}


#line 142  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/verifier/reference memory.c"
void *ldv_reference_xmalloc_unknown_size(size_t size)
{
  void *res;
  
#line 146 
  res = external_allocated_data();
  
#line 147 
  __VERIFIER_assume(res != (void *)0);
  
#line 149 
  return res;
}


#line 62  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/job/root/specifications/linux/ldv/common.h"
void ldv_initialize(void);


#line 76 
void ldv_check_final_state(void);


#line 22  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/35/vtg/ext-modules/linux/usb/register/register.ko/linux:usb:register/emg/environment_model.c"
void ldv_dispatch_register_3_3(struct usb_driver *arg0);


#line 23 
int main(void);


#line 25 
void ldv_usb_scenario_4(void *arg0);


#line 27 
void ldv_initialization_1(void *arg0);


#line 31  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/35/vtg/ext-modules/linux/usb/register/register.ko/linux:usb:register/emg/environment_model.c"
void ldv_dispatch_register_3_3(struct usb_driver *arg0)
{
  struct ldv_struct_usb_scenario_4 *cf_arg_4;
  int tmp;
  
#line 33 
  tmp = ldv_undef_int();
  
#line 33 
  switch (tmp) {
    case 0: 
#line 34 
    ;
    
#line 35 
    cf_arg_4 = (struct ldv_struct_usb_scenario_4 *)ldv_xmalloc(16UL);
    
#line 36 
    cf_arg_4->arg0 = arg0;
    
#line 37 
    ldv_usb_scenario_4((void *)cf_arg_4);
    
#line 38 
    goto ldv_25740;
  }
  ldv_25740: 
#line 40 
  ;
  
#line 41 
  return;
}


#line 45  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/35/vtg/ext-modules/linux/usb/register/register.ko/linux:usb:register/emg/environment_model.c"
int main(void)
{
  int __retres;
  
#line 48 
  ldv_initialize();
  
#line 51 
  ldv_initialization_1((void *)0);
  
#line 54 
  ldv_check_final_state();
  
#line 56 
  __retres = 0;
  
#line 56 
  goto return_label;
  
#line 1  "/var/lib/klever/workspace/Branches-and-Tags-Processing/src/build bases/testing/1de383/Storage/home/novikov/work/klever-data/linux-stable/<built-in>"
  __retres = 0;
  return_label: 
#line 1 
                return __retres;
}


#line 61  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/35/vtg/ext-modules/linux/usb/register/register.ko/linux:usb:register/emg/environment_model.c"
int ldv_emg_usb_register_driver(struct usb_driver *arg0, struct module *arg1, char *arg2)
{
  int __retres;
  int tmp_0;
  
#line 64 
  struct usb_driver *ldv_3_usb_driver = ldv_emg_alias_ldv_usb_driver_2;
  
#line 68 
  tmp_0 = ldv_undef_int();
  
#line 68 
  if (tmp_0 != 0) {
    
#line 70 
    ldv_3_usb_driver = arg0;
    
#line 74 
    ldv_dispatch_register_3_3(ldv_3_usb_driver);
    
#line 78 
    __retres = 0;
    
#line 78 
    goto return_label;
  }
  else {
    int tmp;
    
#line 85 
    ldv_failed_usb_register_driver();
    
#line 86 
    tmp = ldv_undef_int_negative();
    
#line 86 
    __retres = tmp;
    
#line 86 
    goto return_label;
  }
  return_label: 
#line 68 
                return __retres;
}


#line 96  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/35/vtg/ext-modules/linux/usb/register/register.ko/linux:usb:register/emg/environment_model.c"
void ldv_usb_scenario_4(void *arg0)
{
  struct usb_interface *ldv_4_resource;
  struct usb_device *ldv_4_usb_device;
  struct usb_device_id *ldv_4_ldv_param_1_3;
  struct pm_message *ldv_4_ldv_param_1_2;
  int tmp_2;
  int tmp_8;
  
#line 102 
  struct usb_driver *ldv_4_container = ldv_emg_alias_ldv_usb_driver_2;
  
#line 104 
  int ldv_4_probe_retval = ldv_undef_int();
  
#line 106 
  struct ldv_struct_usb_scenario_4 *data = (struct ldv_struct_usb_scenario_4 *)arg0;
  
#line 110 
  ldv_4_probe_retval = ldv_undef_int();
  
#line 112 
  __VERIFIER_assume(data->arg0 == ldv_emg_alias_ldv_usb_driver_2);
  
#line 114 
  if (data != (struct ldv_struct_usb_scenario_4 *)0) {
    
#line 115 
    ldv_4_container = data->arg0;
    
#line 116 
    ldv_free((void *)data);
  }
  else ;
  
#line 120 
  tmp_2 = ldv_undef_int();
  
#line 120 
  if (tmp_2 != 0) {
    
#line 122 
    ldv_4_resource = (struct usb_interface *)ldv_xmalloc_unknown_size(0UL);
    
#line 123 
    ldv_4_usb_device = (struct usb_device *)ldv_xmalloc_unknown_size(0UL);
    
#line 124 
    ldv_4_resource->dev.parent = & ldv_4_usb_device->dev;
    
#line 131 
    goto ldv_manage_interface_4;
  }
  else 
#line 139 
       goto return_label;
  
#line 142 
  goto return_label;
  ldv_manage_interface_4: 
#line 145 
  ;
  
#line 148 
  tmp_8 = ldv_undef_int();
  
#line 148 
  if (tmp_8 != 0) {
    int tmp_7;
    
#line 150 
    ldv_4_ldv_param_1_3 = (struct usb_device_id *)ldv_xmalloc_unknown_size(0UL);
    
#line 155 
    ldv_pre_probe();
    
#line 157 
    ldv_4_probe_retval = ldv_emg_wrapper_ldv_usb_probe_2(ldv_4_resource,ldv_4_ldv_param_1_3);
    
#line 159 
    ldv_4_probe_retval = ldv_post_probe(ldv_4_probe_retval);
    
#line 163 
    ldv_free((void *)ldv_4_ldv_param_1_3);
    
#line 166 
    tmp_7 = ldv_undef_int();
    
#line 166 
    if (tmp_7 != 0) {
      
#line 168 
      __VERIFIER_assume(ldv_4_probe_retval != 0);
      
#line 175 
      goto ldv_manage_interface_4;
    }
    else {
      int tmp_4;
      
#line 179 
      __VERIFIER_assume(ldv_4_probe_retval == 0);
      
#line 182 
      tmp_4 = ldv_undef_int();
      
#line 182 
      switch (tmp_4) {
        int tmp_6;
        case 1: 
#line 183 
        ;
        
#line 189 
        if (ldv_4_container->pre_reset != (int (*)(struct usb_interface *))0) 
          
#line 191 
          (*(ldv_4_container->pre_reset))(ldv_4_resource); else ;
        
#line 196 
        if (ldv_4_container->post_reset != (int (*)(struct usb_interface *))0) 
          
#line 198 
          (*(ldv_4_container->post_reset))(ldv_4_resource); else ;
        
#line 202 
        goto ldv_25762;
        case 2: 
#line 204 
        ;
        
#line 206 
        ldv_4_ldv_param_1_2 = (struct pm_message *)ldv_xmalloc_unknown_size(0UL);
        
#line 210 
        if (ldv_4_container->suspend != (int (*)(struct usb_interface *, pm_message_t ))0) 
          
#line 212 
          (*(ldv_4_container->suspend))(ldv_4_resource,*ldv_4_ldv_param_1_2); else ;
        
#line 217 
        ldv_free((void *)ldv_4_ldv_param_1_2);
        
#line 220 
        tmp_6 = ldv_undef_int();
        
#line 220 
        if (tmp_6 != 0) {
          
#line 222 
          if (ldv_4_container->resume != (int (*)(struct usb_interface *))0) 
            
#line 224 
            (*(ldv_4_container->resume))(ldv_4_resource); else ;
        }
        else 
          
#line 231 
          if (ldv_4_container->reset_resume != (int (*)(struct usb_interface *))0) 
            
#line 233 
            (*(ldv_4_container->reset_resume))(ldv_4_resource); else ;
        
#line 238 
        goto ldv_25762;
        case 3: 
#line 240 
        ;
        
#line 245 
        goto ldv_25762;
        case 4: 
#line 247 
        ;
        
#line 251 
        goto ldv_25762;
        default: 
#line 253 
        ;
        
#line 253 
        __VERIFIER_assume(0);
      }
      ldv_25762: 
#line 255 
      ;
    }
    
#line 257 
    if (ldv_4_container->disconnect != (void (*)(struct usb_interface *))0) 
      
#line 259 
      (*(ldv_4_container->disconnect))(ldv_4_resource); else ;
    
#line 267 
    goto ldv_manage_interface_4;
  }
  else {
    
#line 271 
    ldv_free((void *)ldv_4_resource);
    
#line 272 
    ldv_free((void *)ldv_4_usb_device);
    
#line 280 
    goto return_label;
  }
  return_label: 
#line 283 
                return;
}


#line 288  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/35/vtg/ext-modules/linux/usb/register/register.ko/linux:usb:register/emg/environment_model.c"
void ldv_emg_usb_deregister(struct usb_driver *arg0)
{
  
#line 291 
  struct usb_driver *ldv_2_usb_driver = ldv_emg_alias_ldv_usb_driver_2;
  
#line 294 
  ldv_2_usb_driver = arg0;
  
#line 302 
  goto return_label;
  return_label: 
#line 304 
                return;
}


#line 309  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/35/vtg/ext-modules/linux/usb/register/register.ko/linux:usb:register/emg/environment_model.c"
void ldv_initialization_1(void *arg0)
{
  int ldv_1_ret;
  int tmp;
  
#line 316 
  ldv_1_ret = ldv_emg_ldv_init();
  
#line 317 
  ldv_1_ret = ldv_post_init(ldv_1_ret);
  
#line 320 
  tmp = ldv_undef_int();
  
#line 320 
  if (tmp != 0) {
    
#line 322 
    __VERIFIER_assume(ldv_1_ret != 0);
    
#line 326 
    goto return_label;
  }
  else {
    
#line 330 
    __VERIFIER_assume(ldv_1_ret == 0);
    
#line 334 
    goto return_label;
  }
  return_label: 
#line 337 
                return;
}


#line 3  "/var/lib/klever/workspace/Branches-and-Tags-Processing/bin/klever-work/native-scheduler/scheduler/jobs/d347514def4b9b67f5c542deffbacc12/klever-core-work-dir/35/vtg/ext-modules/linux/usb/register/register.ko/linux:usb:register/fvtp/bug kind funcs.c"
void ldv_assert_linux_usb_register__wrong_return_value(int expr)
{
  
#line 4 
  if (! expr) 
#line 5 
              __VERIFIER_error(); else ;
  
#line 6 
  return;
}