Showing error 1011

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


Source:

   1/* Generated by CIL v. 1.3.7 */
   2/* print_CIL_Input is true */
   3
   4#line 19 "include/asm-generic/int-ll64.h"
   5typedef signed char __s8;
   6#line 22 "include/asm-generic/int-ll64.h"
   7typedef short __s16;
   8#line 23 "include/asm-generic/int-ll64.h"
   9typedef unsigned short __u16;
  10#line 25 "include/asm-generic/int-ll64.h"
  11typedef int __s32;
  12#line 26 "include/asm-generic/int-ll64.h"
  13typedef unsigned int __u32;
  14#line 30 "include/asm-generic/int-ll64.h"
  15typedef unsigned long long __u64;
  16#line 43 "include/asm-generic/int-ll64.h"
  17typedef unsigned char u8;
  18#line 45 "include/asm-generic/int-ll64.h"
  19typedef short s16;
  20#line 46 "include/asm-generic/int-ll64.h"
  21typedef unsigned short u16;
  22#line 48 "include/asm-generic/int-ll64.h"
  23typedef int s32;
  24#line 49 "include/asm-generic/int-ll64.h"
  25typedef unsigned int u32;
  26#line 51 "include/asm-generic/int-ll64.h"
  27typedef long long s64;
  28#line 52 "include/asm-generic/int-ll64.h"
  29typedef unsigned long long u64;
  30#line 14 "include/asm-generic/posix_types.h"
  31typedef long __kernel_long_t;
  32#line 15 "include/asm-generic/posix_types.h"
  33typedef unsigned long __kernel_ulong_t;
  34#line 52 "include/asm-generic/posix_types.h"
  35typedef unsigned int __kernel_uid32_t;
  36#line 53 "include/asm-generic/posix_types.h"
  37typedef unsigned int __kernel_gid32_t;
  38#line 75 "include/asm-generic/posix_types.h"
  39typedef __kernel_ulong_t __kernel_size_t;
  40#line 76 "include/asm-generic/posix_types.h"
  41typedef __kernel_long_t __kernel_ssize_t;
  42#line 91 "include/asm-generic/posix_types.h"
  43typedef long long __kernel_loff_t;
  44#line 92 "include/asm-generic/posix_types.h"
  45typedef __kernel_long_t __kernel_time_t;
  46#line 21 "include/linux/types.h"
  47typedef __u32 __kernel_dev_t;
  48#line 24 "include/linux/types.h"
  49typedef __kernel_dev_t dev_t;
  50#line 27 "include/linux/types.h"
  51typedef unsigned short umode_t;
  52#line 38 "include/linux/types.h"
  53typedef _Bool bool;
  54#line 40 "include/linux/types.h"
  55typedef __kernel_uid32_t uid_t;
  56#line 41 "include/linux/types.h"
  57typedef __kernel_gid32_t gid_t;
  58#line 54 "include/linux/types.h"
  59typedef __kernel_loff_t loff_t;
  60#line 63 "include/linux/types.h"
  61typedef __kernel_size_t size_t;
  62#line 68 "include/linux/types.h"
  63typedef __kernel_ssize_t ssize_t;
  64#line 78 "include/linux/types.h"
  65typedef __kernel_time_t time_t;
  66#line 142 "include/linux/types.h"
  67typedef unsigned long sector_t;
  68#line 143 "include/linux/types.h"
  69typedef unsigned long blkcnt_t;
  70#line 202 "include/linux/types.h"
  71typedef unsigned int gfp_t;
  72#line 203 "include/linux/types.h"
  73typedef unsigned int fmode_t;
  74#line 221 "include/linux/types.h"
  75struct __anonstruct_atomic_t_6 {
  76   int counter ;
  77};
  78#line 221 "include/linux/types.h"
  79typedef struct __anonstruct_atomic_t_6 atomic_t;
  80#line 226 "include/linux/types.h"
  81struct __anonstruct_atomic64_t_7 {
  82   long counter ;
  83};
  84#line 226 "include/linux/types.h"
  85typedef struct __anonstruct_atomic64_t_7 atomic64_t;
  86#line 227 "include/linux/types.h"
  87struct list_head {
  88   struct list_head *next ;
  89   struct list_head *prev ;
  90};
  91#line 232
  92struct hlist_node;
  93#line 232 "include/linux/types.h"
  94struct hlist_head {
  95   struct hlist_node *first ;
  96};
  97#line 236 "include/linux/types.h"
  98struct hlist_node {
  99   struct hlist_node *next ;
 100   struct hlist_node **pprev ;
 101};
 102#line 247 "include/linux/types.h"
 103struct rcu_head {
 104   struct rcu_head *next ;
 105   void (*func)(struct rcu_head * ) ;
 106};
 107#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
 108struct module;
 109#line 55
 110struct module;
 111#line 146 "include/linux/init.h"
 112typedef void (*ctor_fn_t)(void);
 113#line 57 "include/linux/dynamic_debug.h"
 114struct completion;
 115#line 57
 116struct completion;
 117#line 348 "include/linux/kernel.h"
 118struct pid;
 119#line 348
 120struct pid;
 121#line 112 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/stat.h"
 122struct timespec;
 123#line 112
 124struct timespec;
 125#line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
 126struct page;
 127#line 58
 128struct page;
 129#line 26 "include/asm-generic/getorder.h"
 130struct task_struct;
 131#line 26
 132struct task_struct;
 133#line 28
 134struct mm_struct;
 135#line 28
 136struct mm_struct;
 137#line 13 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
 138typedef unsigned long pgdval_t;
 139#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
 140typedef unsigned long pgprotval_t;
 141#line 18 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
 142struct pgprot {
 143   pgprotval_t pgprot ;
 144};
 145#line 192 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 146typedef struct pgprot pgprot_t;
 147#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 148struct __anonstruct_pgd_t_16 {
 149   pgdval_t pgd ;
 150};
 151#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 152typedef struct __anonstruct_pgd_t_16 pgd_t;
 153#line 282 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 154typedef struct page *pgtable_t;
 155#line 290
 156struct file;
 157#line 290
 158struct file;
 159#line 305
 160struct seq_file;
 161#line 305
 162struct seq_file;
 163#line 339
 164struct cpumask;
 165#line 339
 166struct cpumask;
 167#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
 168struct arch_spinlock;
 169#line 327
 170struct arch_spinlock;
 171#line 306 "include/linux/bitmap.h"
 172struct bug_entry {
 173   int bug_addr_disp ;
 174   int file_disp ;
 175   unsigned short line ;
 176   unsigned short flags ;
 177};
 178#line 89 "include/linux/bug.h"
 179struct cpumask {
 180   unsigned long bits[64U] ;
 181};
 182#line 637 "include/linux/cpumask.h"
 183typedef struct cpumask *cpumask_var_t;
 184#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
 185struct static_key;
 186#line 234
 187struct static_key;
 188#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 189struct kmem_cache;
 190#line 23 "include/asm-generic/atomic-long.h"
 191typedef atomic64_t atomic_long_t;
 192#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 193typedef u16 __ticket_t;
 194#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 195typedef u32 __ticketpair_t;
 196#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 197struct __raw_tickets {
 198   __ticket_t head ;
 199   __ticket_t tail ;
 200};
 201#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 202union __anonunion_ldv_5907_29 {
 203   __ticketpair_t head_tail ;
 204   struct __raw_tickets tickets ;
 205};
 206#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 207struct arch_spinlock {
 208   union __anonunion_ldv_5907_29 ldv_5907 ;
 209};
 210#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 211typedef struct arch_spinlock arch_spinlock_t;
 212#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 213struct __anonstruct_ldv_5914_31 {
 214   u32 read ;
 215   s32 write ;
 216};
 217#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 218union __anonunion_arch_rwlock_t_30 {
 219   s64 lock ;
 220   struct __anonstruct_ldv_5914_31 ldv_5914 ;
 221};
 222#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 223typedef union __anonunion_arch_rwlock_t_30 arch_rwlock_t;
 224#line 34
 225struct lockdep_map;
 226#line 34
 227struct lockdep_map;
 228#line 55 "include/linux/debug_locks.h"
 229struct stack_trace {
 230   unsigned int nr_entries ;
 231   unsigned int max_entries ;
 232   unsigned long *entries ;
 233   int skip ;
 234};
 235#line 26 "include/linux/stacktrace.h"
 236struct lockdep_subclass_key {
 237   char __one_byte ;
 238};
 239#line 53 "include/linux/lockdep.h"
 240struct lock_class_key {
 241   struct lockdep_subclass_key subkeys[8U] ;
 242};
 243#line 59 "include/linux/lockdep.h"
 244struct lock_class {
 245   struct list_head hash_entry ;
 246   struct list_head lock_entry ;
 247   struct lockdep_subclass_key *key ;
 248   unsigned int subclass ;
 249   unsigned int dep_gen_id ;
 250   unsigned long usage_mask ;
 251   struct stack_trace usage_traces[13U] ;
 252   struct list_head locks_after ;
 253   struct list_head locks_before ;
 254   unsigned int version ;
 255   unsigned long ops ;
 256   char const   *name ;
 257   int name_version ;
 258   unsigned long contention_point[4U] ;
 259   unsigned long contending_point[4U] ;
 260};
 261#line 144 "include/linux/lockdep.h"
 262struct lockdep_map {
 263   struct lock_class_key *key ;
 264   struct lock_class *class_cache[2U] ;
 265   char const   *name ;
 266   int cpu ;
 267   unsigned long ip ;
 268};
 269#line 556 "include/linux/lockdep.h"
 270struct raw_spinlock {
 271   arch_spinlock_t raw_lock ;
 272   unsigned int magic ;
 273   unsigned int owner_cpu ;
 274   void *owner ;
 275   struct lockdep_map dep_map ;
 276};
 277#line 32 "include/linux/spinlock_types.h"
 278typedef struct raw_spinlock raw_spinlock_t;
 279#line 33 "include/linux/spinlock_types.h"
 280struct __anonstruct_ldv_6122_33 {
 281   u8 __padding[24U] ;
 282   struct lockdep_map dep_map ;
 283};
 284#line 33 "include/linux/spinlock_types.h"
 285union __anonunion_ldv_6123_32 {
 286   struct raw_spinlock rlock ;
 287   struct __anonstruct_ldv_6122_33 ldv_6122 ;
 288};
 289#line 33 "include/linux/spinlock_types.h"
 290struct spinlock {
 291   union __anonunion_ldv_6123_32 ldv_6123 ;
 292};
 293#line 76 "include/linux/spinlock_types.h"
 294typedef struct spinlock spinlock_t;
 295#line 23 "include/linux/rwlock_types.h"
 296struct __anonstruct_rwlock_t_34 {
 297   arch_rwlock_t raw_lock ;
 298   unsigned int magic ;
 299   unsigned int owner_cpu ;
 300   void *owner ;
 301   struct lockdep_map dep_map ;
 302};
 303#line 23 "include/linux/rwlock_types.h"
 304typedef struct __anonstruct_rwlock_t_34 rwlock_t;
 305#line 110 "include/linux/seqlock.h"
 306struct seqcount {
 307   unsigned int sequence ;
 308};
 309#line 121 "include/linux/seqlock.h"
 310typedef struct seqcount seqcount_t;
 311#line 254 "include/linux/seqlock.h"
 312struct timespec {
 313   __kernel_time_t tv_sec ;
 314   long tv_nsec ;
 315};
 316#line 286 "include/linux/time.h"
 317struct kstat {
 318   u64 ino ;
 319   dev_t dev ;
 320   umode_t mode ;
 321   unsigned int nlink ;
 322   uid_t uid ;
 323   gid_t gid ;
 324   dev_t rdev ;
 325   loff_t size ;
 326   struct timespec atime ;
 327   struct timespec mtime ;
 328   struct timespec ctime ;
 329   unsigned long blksize ;
 330   unsigned long long blocks ;
 331};
 332#line 48 "include/linux/wait.h"
 333struct __wait_queue_head {
 334   spinlock_t lock ;
 335   struct list_head task_list ;
 336};
 337#line 53 "include/linux/wait.h"
 338typedef struct __wait_queue_head wait_queue_head_t;
 339#line 98 "include/linux/nodemask.h"
 340struct __anonstruct_nodemask_t_36 {
 341   unsigned long bits[16U] ;
 342};
 343#line 98 "include/linux/nodemask.h"
 344typedef struct __anonstruct_nodemask_t_36 nodemask_t;
 345#line 670 "include/linux/mmzone.h"
 346struct mutex {
 347   atomic_t count ;
 348   spinlock_t wait_lock ;
 349   struct list_head wait_list ;
 350   struct task_struct *owner ;
 351   char const   *name ;
 352   void *magic ;
 353   struct lockdep_map dep_map ;
 354};
 355#line 171 "include/linux/mutex.h"
 356struct rw_semaphore;
 357#line 171
 358struct rw_semaphore;
 359#line 172 "include/linux/mutex.h"
 360struct rw_semaphore {
 361   long count ;
 362   raw_spinlock_t wait_lock ;
 363   struct list_head wait_list ;
 364   struct lockdep_map dep_map ;
 365};
 366#line 128 "include/linux/rwsem.h"
 367struct completion {
 368   unsigned int done ;
 369   wait_queue_head_t wait ;
 370};
 371#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
 372struct __anonstruct_mm_context_t_101 {
 373   void *ldt ;
 374   int size ;
 375   unsigned short ia32_compat ;
 376   struct mutex lock ;
 377   void *vdso ;
 378};
 379#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
 380typedef struct __anonstruct_mm_context_t_101 mm_context_t;
 381#line 18 "include/asm-generic/pci_iomap.h"
 382struct vm_area_struct;
 383#line 18
 384struct vm_area_struct;
 385#line 835 "include/linux/sysctl.h"
 386struct rb_node {
 387   unsigned long rb_parent_color ;
 388   struct rb_node *rb_right ;
 389   struct rb_node *rb_left ;
 390};
 391#line 108 "include/linux/rbtree.h"
 392struct rb_root {
 393   struct rb_node *rb_node ;
 394};
 395#line 37 "include/linux/kmod.h"
 396struct cred;
 397#line 37
 398struct cred;
 399#line 18 "include/linux/elf.h"
 400typedef __u64 Elf64_Addr;
 401#line 19 "include/linux/elf.h"
 402typedef __u16 Elf64_Half;
 403#line 23 "include/linux/elf.h"
 404typedef __u32 Elf64_Word;
 405#line 24 "include/linux/elf.h"
 406typedef __u64 Elf64_Xword;
 407#line 193 "include/linux/elf.h"
 408struct elf64_sym {
 409   Elf64_Word st_name ;
 410   unsigned char st_info ;
 411   unsigned char st_other ;
 412   Elf64_Half st_shndx ;
 413   Elf64_Addr st_value ;
 414   Elf64_Xword st_size ;
 415};
 416#line 201 "include/linux/elf.h"
 417typedef struct elf64_sym Elf64_Sym;
 418#line 445
 419struct sock;
 420#line 445
 421struct sock;
 422#line 446
 423struct kobject;
 424#line 446
 425struct kobject;
 426#line 447
 427enum kobj_ns_type {
 428    KOBJ_NS_TYPE_NONE = 0,
 429    KOBJ_NS_TYPE_NET = 1,
 430    KOBJ_NS_TYPES = 2
 431} ;
 432#line 453 "include/linux/elf.h"
 433struct kobj_ns_type_operations {
 434   enum kobj_ns_type type ;
 435   void *(*grab_current_ns)(void) ;
 436   void const   *(*netlink_ns)(struct sock * ) ;
 437   void const   *(*initial_ns)(void) ;
 438   void (*drop_ns)(void * ) ;
 439};
 440#line 57 "include/linux/kobject_ns.h"
 441struct attribute {
 442   char const   *name ;
 443   umode_t mode ;
 444   struct lock_class_key *key ;
 445   struct lock_class_key skey ;
 446};
 447#line 98 "include/linux/sysfs.h"
 448struct sysfs_ops {
 449   ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
 450   ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
 451   void const   *(*namespace)(struct kobject * , struct attribute  const  * ) ;
 452};
 453#line 117
 454struct sysfs_dirent;
 455#line 117
 456struct sysfs_dirent;
 457#line 182 "include/linux/sysfs.h"
 458struct kref {
 459   atomic_t refcount ;
 460};
 461#line 49 "include/linux/kobject.h"
 462struct kset;
 463#line 49
 464struct kobj_type;
 465#line 49 "include/linux/kobject.h"
 466struct kobject {
 467   char const   *name ;
 468   struct list_head entry ;
 469   struct kobject *parent ;
 470   struct kset *kset ;
 471   struct kobj_type *ktype ;
 472   struct sysfs_dirent *sd ;
 473   struct kref kref ;
 474   unsigned char state_initialized : 1 ;
 475   unsigned char state_in_sysfs : 1 ;
 476   unsigned char state_add_uevent_sent : 1 ;
 477   unsigned char state_remove_uevent_sent : 1 ;
 478   unsigned char uevent_suppress : 1 ;
 479};
 480#line 107 "include/linux/kobject.h"
 481struct kobj_type {
 482   void (*release)(struct kobject * ) ;
 483   struct sysfs_ops  const  *sysfs_ops ;
 484   struct attribute **default_attrs ;
 485   struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject * ) ;
 486   void const   *(*namespace)(struct kobject * ) ;
 487};
 488#line 115 "include/linux/kobject.h"
 489struct kobj_uevent_env {
 490   char *envp[32U] ;
 491   int envp_idx ;
 492   char buf[2048U] ;
 493   int buflen ;
 494};
 495#line 122 "include/linux/kobject.h"
 496struct kset_uevent_ops {
 497   int (* const  filter)(struct kset * , struct kobject * ) ;
 498   char const   *(* const  name)(struct kset * , struct kobject * ) ;
 499   int (* const  uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
 500};
 501#line 139 "include/linux/kobject.h"
 502struct kset {
 503   struct list_head list ;
 504   spinlock_t list_lock ;
 505   struct kobject kobj ;
 506   struct kset_uevent_ops  const  *uevent_ops ;
 507};
 508#line 215
 509struct kernel_param;
 510#line 215
 511struct kernel_param;
 512#line 216 "include/linux/kobject.h"
 513struct kernel_param_ops {
 514   int (*set)(char const   * , struct kernel_param  const  * ) ;
 515   int (*get)(char * , struct kernel_param  const  * ) ;
 516   void (*free)(void * ) ;
 517};
 518#line 49 "include/linux/moduleparam.h"
 519struct kparam_string;
 520#line 49
 521struct kparam_array;
 522#line 49 "include/linux/moduleparam.h"
 523union __anonunion_ldv_13363_134 {
 524   void *arg ;
 525   struct kparam_string  const  *str ;
 526   struct kparam_array  const  *arr ;
 527};
 528#line 49 "include/linux/moduleparam.h"
 529struct kernel_param {
 530   char const   *name ;
 531   struct kernel_param_ops  const  *ops ;
 532   u16 perm ;
 533   s16 level ;
 534   union __anonunion_ldv_13363_134 ldv_13363 ;
 535};
 536#line 61 "include/linux/moduleparam.h"
 537struct kparam_string {
 538   unsigned int maxlen ;
 539   char *string ;
 540};
 541#line 67 "include/linux/moduleparam.h"
 542struct kparam_array {
 543   unsigned int max ;
 544   unsigned int elemsize ;
 545   unsigned int *num ;
 546   struct kernel_param_ops  const  *ops ;
 547   void *elem ;
 548};
 549#line 458 "include/linux/moduleparam.h"
 550struct static_key {
 551   atomic_t enabled ;
 552};
 553#line 225 "include/linux/jump_label.h"
 554struct tracepoint;
 555#line 225
 556struct tracepoint;
 557#line 226 "include/linux/jump_label.h"
 558struct tracepoint_func {
 559   void *func ;
 560   void *data ;
 561};
 562#line 29 "include/linux/tracepoint.h"
 563struct tracepoint {
 564   char const   *name ;
 565   struct static_key key ;
 566   void (*regfunc)(void) ;
 567   void (*unregfunc)(void) ;
 568   struct tracepoint_func *funcs ;
 569};
 570#line 86 "include/linux/tracepoint.h"
 571struct kernel_symbol {
 572   unsigned long value ;
 573   char const   *name ;
 574};
 575#line 27 "include/linux/export.h"
 576struct mod_arch_specific {
 577
 578};
 579#line 34 "include/linux/module.h"
 580struct module_param_attrs;
 581#line 34 "include/linux/module.h"
 582struct module_kobject {
 583   struct kobject kobj ;
 584   struct module *mod ;
 585   struct kobject *drivers_dir ;
 586   struct module_param_attrs *mp ;
 587};
 588#line 43 "include/linux/module.h"
 589struct module_attribute {
 590   struct attribute attr ;
 591   ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
 592   ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const   * ,
 593                    size_t  ) ;
 594   void (*setup)(struct module * , char const   * ) ;
 595   int (*test)(struct module * ) ;
 596   void (*free)(struct module * ) ;
 597};
 598#line 69
 599struct exception_table_entry;
 600#line 69
 601struct exception_table_entry;
 602#line 198
 603enum module_state {
 604    MODULE_STATE_LIVE = 0,
 605    MODULE_STATE_COMING = 1,
 606    MODULE_STATE_GOING = 2
 607} ;
 608#line 204 "include/linux/module.h"
 609struct module_ref {
 610   unsigned long incs ;
 611   unsigned long decs ;
 612};
 613#line 219
 614struct module_sect_attrs;
 615#line 219
 616struct module_notes_attrs;
 617#line 219
 618struct ftrace_event_call;
 619#line 219 "include/linux/module.h"
 620struct module {
 621   enum module_state state ;
 622   struct list_head list ;
 623   char name[56U] ;
 624   struct module_kobject mkobj ;
 625   struct module_attribute *modinfo_attrs ;
 626   char const   *version ;
 627   char const   *srcversion ;
 628   struct kobject *holders_dir ;
 629   struct kernel_symbol  const  *syms ;
 630   unsigned long const   *crcs ;
 631   unsigned int num_syms ;
 632   struct kernel_param *kp ;
 633   unsigned int num_kp ;
 634   unsigned int num_gpl_syms ;
 635   struct kernel_symbol  const  *gpl_syms ;
 636   unsigned long const   *gpl_crcs ;
 637   struct kernel_symbol  const  *unused_syms ;
 638   unsigned long const   *unused_crcs ;
 639   unsigned int num_unused_syms ;
 640   unsigned int num_unused_gpl_syms ;
 641   struct kernel_symbol  const  *unused_gpl_syms ;
 642   unsigned long const   *unused_gpl_crcs ;
 643   struct kernel_symbol  const  *gpl_future_syms ;
 644   unsigned long const   *gpl_future_crcs ;
 645   unsigned int num_gpl_future_syms ;
 646   unsigned int num_exentries ;
 647   struct exception_table_entry *extable ;
 648   int (*init)(void) ;
 649   void *module_init ;
 650   void *module_core ;
 651   unsigned int init_size ;
 652   unsigned int core_size ;
 653   unsigned int init_text_size ;
 654   unsigned int core_text_size ;
 655   unsigned int init_ro_size ;
 656   unsigned int core_ro_size ;
 657   struct mod_arch_specific arch ;
 658   unsigned int taints ;
 659   unsigned int num_bugs ;
 660   struct list_head bug_list ;
 661   struct bug_entry *bug_table ;
 662   Elf64_Sym *symtab ;
 663   Elf64_Sym *core_symtab ;
 664   unsigned int num_symtab ;
 665   unsigned int core_num_syms ;
 666   char *strtab ;
 667   char *core_strtab ;
 668   struct module_sect_attrs *sect_attrs ;
 669   struct module_notes_attrs *notes_attrs ;
 670   char *args ;
 671   void *percpu ;
 672   unsigned int percpu_size ;
 673   unsigned int num_tracepoints ;
 674   struct tracepoint * const  *tracepoints_ptrs ;
 675   unsigned int num_trace_bprintk_fmt ;
 676   char const   **trace_bprintk_fmt_start ;
 677   struct ftrace_event_call **trace_events ;
 678   unsigned int num_trace_events ;
 679   struct list_head source_list ;
 680   struct list_head target_list ;
 681   struct task_struct *waiter ;
 682   void (*exit)(void) ;
 683   struct module_ref *refptr ;
 684   ctor_fn_t (**ctors)(void) ;
 685   unsigned int num_ctors ;
 686};
 687#line 88 "include/linux/kmemleak.h"
 688struct kmem_cache_cpu {
 689   void **freelist ;
 690   unsigned long tid ;
 691   struct page *page ;
 692   struct page *partial ;
 693   int node ;
 694   unsigned int stat[26U] ;
 695};
 696#line 55 "include/linux/slub_def.h"
 697struct kmem_cache_node {
 698   spinlock_t list_lock ;
 699   unsigned long nr_partial ;
 700   struct list_head partial ;
 701   atomic_long_t nr_slabs ;
 702   atomic_long_t total_objects ;
 703   struct list_head full ;
 704};
 705#line 66 "include/linux/slub_def.h"
 706struct kmem_cache_order_objects {
 707   unsigned long x ;
 708};
 709#line 76 "include/linux/slub_def.h"
 710struct kmem_cache {
 711   struct kmem_cache_cpu *cpu_slab ;
 712   unsigned long flags ;
 713   unsigned long min_partial ;
 714   int size ;
 715   int objsize ;
 716   int offset ;
 717   int cpu_partial ;
 718   struct kmem_cache_order_objects oo ;
 719   struct kmem_cache_order_objects max ;
 720   struct kmem_cache_order_objects min ;
 721   gfp_t allocflags ;
 722   int refcount ;
 723   void (*ctor)(void * ) ;
 724   int inuse ;
 725   int align ;
 726   int reserved ;
 727   char const   *name ;
 728   struct list_head list ;
 729   struct kobject kobj ;
 730   int remote_node_defrag_ratio ;
 731   struct kmem_cache_node *node[1024U] ;
 732};
 733#line 15 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9168/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-lirc.c.p"
 734struct prio_tree_node;
 735#line 15 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9168/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-lirc.c.p"
 736struct raw_prio_tree_node {
 737   struct prio_tree_node *left ;
 738   struct prio_tree_node *right ;
 739   struct prio_tree_node *parent ;
 740};
 741#line 19 "include/linux/prio_tree.h"
 742struct prio_tree_node {
 743   struct prio_tree_node *left ;
 744   struct prio_tree_node *right ;
 745   struct prio_tree_node *parent ;
 746   unsigned long start ;
 747   unsigned long last ;
 748};
 749#line 27 "include/linux/prio_tree.h"
 750struct prio_tree_root {
 751   struct prio_tree_node *prio_tree_node ;
 752   unsigned short index_bits ;
 753   unsigned short raw ;
 754};
 755#line 116
 756struct address_space;
 757#line 116
 758struct address_space;
 759#line 117 "include/linux/prio_tree.h"
 760union __anonunion_ldv_14216_136 {
 761   unsigned long index ;
 762   void *freelist ;
 763};
 764#line 117 "include/linux/prio_tree.h"
 765struct __anonstruct_ldv_14226_140 {
 766   unsigned short inuse ;
 767   unsigned short objects : 15 ;
 768   unsigned char frozen : 1 ;
 769};
 770#line 117 "include/linux/prio_tree.h"
 771union __anonunion_ldv_14227_139 {
 772   atomic_t _mapcount ;
 773   struct __anonstruct_ldv_14226_140 ldv_14226 ;
 774};
 775#line 117 "include/linux/prio_tree.h"
 776struct __anonstruct_ldv_14229_138 {
 777   union __anonunion_ldv_14227_139 ldv_14227 ;
 778   atomic_t _count ;
 779};
 780#line 117 "include/linux/prio_tree.h"
 781union __anonunion_ldv_14230_137 {
 782   unsigned long counters ;
 783   struct __anonstruct_ldv_14229_138 ldv_14229 ;
 784};
 785#line 117 "include/linux/prio_tree.h"
 786struct __anonstruct_ldv_14231_135 {
 787   union __anonunion_ldv_14216_136 ldv_14216 ;
 788   union __anonunion_ldv_14230_137 ldv_14230 ;
 789};
 790#line 117 "include/linux/prio_tree.h"
 791struct __anonstruct_ldv_14238_142 {
 792   struct page *next ;
 793   int pages ;
 794   int pobjects ;
 795};
 796#line 117 "include/linux/prio_tree.h"
 797union __anonunion_ldv_14239_141 {
 798   struct list_head lru ;
 799   struct __anonstruct_ldv_14238_142 ldv_14238 ;
 800};
 801#line 117 "include/linux/prio_tree.h"
 802union __anonunion_ldv_14244_143 {
 803   unsigned long private ;
 804   struct kmem_cache *slab ;
 805   struct page *first_page ;
 806};
 807#line 117 "include/linux/prio_tree.h"
 808struct page {
 809   unsigned long flags ;
 810   struct address_space *mapping ;
 811   struct __anonstruct_ldv_14231_135 ldv_14231 ;
 812   union __anonunion_ldv_14239_141 ldv_14239 ;
 813   union __anonunion_ldv_14244_143 ldv_14244 ;
 814   unsigned long debug_flags ;
 815};
 816#line 192 "include/linux/mm_types.h"
 817struct __anonstruct_vm_set_145 {
 818   struct list_head list ;
 819   void *parent ;
 820   struct vm_area_struct *head ;
 821};
 822#line 192 "include/linux/mm_types.h"
 823union __anonunion_shared_144 {
 824   struct __anonstruct_vm_set_145 vm_set ;
 825   struct raw_prio_tree_node prio_tree_node ;
 826};
 827#line 192
 828struct anon_vma;
 829#line 192
 830struct vm_operations_struct;
 831#line 192
 832struct mempolicy;
 833#line 192 "include/linux/mm_types.h"
 834struct vm_area_struct {
 835   struct mm_struct *vm_mm ;
 836   unsigned long vm_start ;
 837   unsigned long vm_end ;
 838   struct vm_area_struct *vm_next ;
 839   struct vm_area_struct *vm_prev ;
 840   pgprot_t vm_page_prot ;
 841   unsigned long vm_flags ;
 842   struct rb_node vm_rb ;
 843   union __anonunion_shared_144 shared ;
 844   struct list_head anon_vma_chain ;
 845   struct anon_vma *anon_vma ;
 846   struct vm_operations_struct  const  *vm_ops ;
 847   unsigned long vm_pgoff ;
 848   struct file *vm_file ;
 849   void *vm_private_data ;
 850   struct mempolicy *vm_policy ;
 851};
 852#line 255 "include/linux/mm_types.h"
 853struct core_thread {
 854   struct task_struct *task ;
 855   struct core_thread *next ;
 856};
 857#line 261 "include/linux/mm_types.h"
 858struct core_state {
 859   atomic_t nr_threads ;
 860   struct core_thread dumper ;
 861   struct completion startup ;
 862};
 863#line 274 "include/linux/mm_types.h"
 864struct mm_rss_stat {
 865   atomic_long_t count[3U] ;
 866};
 867#line 287
 868struct linux_binfmt;
 869#line 287
 870struct mmu_notifier_mm;
 871#line 287 "include/linux/mm_types.h"
 872struct mm_struct {
 873   struct vm_area_struct *mmap ;
 874   struct rb_root mm_rb ;
 875   struct vm_area_struct *mmap_cache ;
 876   unsigned long (*get_unmapped_area)(struct file * , unsigned long  , unsigned long  ,
 877                                      unsigned long  , unsigned long  ) ;
 878   void (*unmap_area)(struct mm_struct * , unsigned long  ) ;
 879   unsigned long mmap_base ;
 880   unsigned long task_size ;
 881   unsigned long cached_hole_size ;
 882   unsigned long free_area_cache ;
 883   pgd_t *pgd ;
 884   atomic_t mm_users ;
 885   atomic_t mm_count ;
 886   int map_count ;
 887   spinlock_t page_table_lock ;
 888   struct rw_semaphore mmap_sem ;
 889   struct list_head mmlist ;
 890   unsigned long hiwater_rss ;
 891   unsigned long hiwater_vm ;
 892   unsigned long total_vm ;
 893   unsigned long locked_vm ;
 894   unsigned long pinned_vm ;
 895   unsigned long shared_vm ;
 896   unsigned long exec_vm ;
 897   unsigned long stack_vm ;
 898   unsigned long reserved_vm ;
 899   unsigned long def_flags ;
 900   unsigned long nr_ptes ;
 901   unsigned long start_code ;
 902   unsigned long end_code ;
 903   unsigned long start_data ;
 904   unsigned long end_data ;
 905   unsigned long start_brk ;
 906   unsigned long brk ;
 907   unsigned long start_stack ;
 908   unsigned long arg_start ;
 909   unsigned long arg_end ;
 910   unsigned long env_start ;
 911   unsigned long env_end ;
 912   unsigned long saved_auxv[44U] ;
 913   struct mm_rss_stat rss_stat ;
 914   struct linux_binfmt *binfmt ;
 915   cpumask_var_t cpu_vm_mask_var ;
 916   mm_context_t context ;
 917   unsigned int faultstamp ;
 918   unsigned int token_priority ;
 919   unsigned int last_interval ;
 920   unsigned long flags ;
 921   struct core_state *core_state ;
 922   spinlock_t ioctx_lock ;
 923   struct hlist_head ioctx_list ;
 924   struct task_struct *owner ;
 925   struct file *exe_file ;
 926   unsigned long num_exe_file_vmas ;
 927   struct mmu_notifier_mm *mmu_notifier_mm ;
 928   pgtable_t pmd_huge_pte ;
 929   struct cpumask cpumask_allocation ;
 930};
 931#line 93 "include/linux/bit_spinlock.h"
 932struct shrink_control {
 933   gfp_t gfp_mask ;
 934   unsigned long nr_to_scan ;
 935};
 936#line 14 "include/linux/shrinker.h"
 937struct shrinker {
 938   int (*shrink)(struct shrinker * , struct shrink_control * ) ;
 939   int seeks ;
 940   long batch ;
 941   struct list_head list ;
 942   atomic_long_t nr_in_batch ;
 943};
 944#line 43
 945struct file_ra_state;
 946#line 43
 947struct file_ra_state;
 948#line 45
 949struct writeback_control;
 950#line 45
 951struct writeback_control;
 952#line 178 "include/linux/mm.h"
 953struct vm_fault {
 954   unsigned int flags ;
 955   unsigned long pgoff ;
 956   void *virtual_address ;
 957   struct page *page ;
 958};
 959#line 195 "include/linux/mm.h"
 960struct vm_operations_struct {
 961   void (*open)(struct vm_area_struct * ) ;
 962   void (*close)(struct vm_area_struct * ) ;
 963   int (*fault)(struct vm_area_struct * , struct vm_fault * ) ;
 964   int (*page_mkwrite)(struct vm_area_struct * , struct vm_fault * ) ;
 965   int (*access)(struct vm_area_struct * , unsigned long  , void * , int  , int  ) ;
 966   int (*set_policy)(struct vm_area_struct * , struct mempolicy * ) ;
 967   struct mempolicy *(*get_policy)(struct vm_area_struct * , unsigned long  ) ;
 968   int (*migrate)(struct vm_area_struct * , nodemask_t const   * , nodemask_t const   * ,
 969                  unsigned long  ) ;
 970};
 971#line 244
 972struct inode;
 973#line 244
 974struct inode;
 975#line 994 "include/linux/device.h"
 976struct block_device;
 977#line 994
 978struct block_device;
 979#line 427 "include/linux/rculist.h"
 980struct hlist_bl_node;
 981#line 427 "include/linux/rculist.h"
 982struct hlist_bl_head {
 983   struct hlist_bl_node *first ;
 984};
 985#line 36 "include/linux/list_bl.h"
 986struct hlist_bl_node {
 987   struct hlist_bl_node *next ;
 988   struct hlist_bl_node **pprev ;
 989};
 990#line 114 "include/linux/rculist_bl.h"
 991struct nameidata;
 992#line 114
 993struct nameidata;
 994#line 115
 995struct path;
 996#line 115
 997struct path;
 998#line 116
 999struct vfsmount;
1000#line 116
1001struct vfsmount;
1002#line 117 "include/linux/rculist_bl.h"
1003struct qstr {
1004   unsigned int hash ;
1005   unsigned int len ;
1006   unsigned char const   *name ;
1007};
1008#line 72 "include/linux/dcache.h"
1009struct dentry_operations;
1010#line 72
1011struct super_block;
1012#line 72 "include/linux/dcache.h"
1013union __anonunion_d_u_150 {
1014   struct list_head d_child ;
1015   struct rcu_head d_rcu ;
1016};
1017#line 72 "include/linux/dcache.h"
1018struct dentry {
1019   unsigned int d_flags ;
1020   seqcount_t d_seq ;
1021   struct hlist_bl_node d_hash ;
1022   struct dentry *d_parent ;
1023   struct qstr d_name ;
1024   struct inode *d_inode ;
1025   unsigned char d_iname[32U] ;
1026   unsigned int d_count ;
1027   spinlock_t d_lock ;
1028   struct dentry_operations  const  *d_op ;
1029   struct super_block *d_sb ;
1030   unsigned long d_time ;
1031   void *d_fsdata ;
1032   struct list_head d_lru ;
1033   union __anonunion_d_u_150 d_u ;
1034   struct list_head d_subdirs ;
1035   struct list_head d_alias ;
1036};
1037#line 123 "include/linux/dcache.h"
1038struct dentry_operations {
1039   int (*d_revalidate)(struct dentry * , struct nameidata * ) ;
1040   int (*d_hash)(struct dentry  const  * , struct inode  const  * , struct qstr * ) ;
1041   int (*d_compare)(struct dentry  const  * , struct inode  const  * , struct dentry  const  * ,
1042                    struct inode  const  * , unsigned int  , char const   * , struct qstr  const  * ) ;
1043   int (*d_delete)(struct dentry  const  * ) ;
1044   void (*d_release)(struct dentry * ) ;
1045   void (*d_prune)(struct dentry * ) ;
1046   void (*d_iput)(struct dentry * , struct inode * ) ;
1047   char *(*d_dname)(struct dentry * , char * , int  ) ;
1048   struct vfsmount *(*d_automount)(struct path * ) ;
1049   int (*d_manage)(struct dentry * , bool  ) ;
1050};
1051#line 402 "include/linux/dcache.h"
1052struct path {
1053   struct vfsmount *mnt ;
1054   struct dentry *dentry ;
1055};
1056#line 58 "include/linux/radix-tree.h"
1057struct radix_tree_node;
1058#line 58 "include/linux/radix-tree.h"
1059struct radix_tree_root {
1060   unsigned int height ;
1061   gfp_t gfp_mask ;
1062   struct radix_tree_node *rnode ;
1063};
1064#line 377
1065enum pid_type {
1066    PIDTYPE_PID = 0,
1067    PIDTYPE_PGID = 1,
1068    PIDTYPE_SID = 2,
1069    PIDTYPE_MAX = 3
1070} ;
1071#line 384
1072struct pid_namespace;
1073#line 384 "include/linux/radix-tree.h"
1074struct upid {
1075   int nr ;
1076   struct pid_namespace *ns ;
1077   struct hlist_node pid_chain ;
1078};
1079#line 56 "include/linux/pid.h"
1080struct pid {
1081   atomic_t count ;
1082   unsigned int level ;
1083   struct hlist_head tasks[3U] ;
1084   struct rcu_head rcu ;
1085   struct upid numbers[1U] ;
1086};
1087#line 45 "include/linux/semaphore.h"
1088struct fiemap_extent {
1089   __u64 fe_logical ;
1090   __u64 fe_physical ;
1091   __u64 fe_length ;
1092   __u64 fe_reserved64[2U] ;
1093   __u32 fe_flags ;
1094   __u32 fe_reserved[3U] ;
1095};
1096#line 38 "include/linux/fiemap.h"
1097enum migrate_mode {
1098    MIGRATE_ASYNC = 0,
1099    MIGRATE_SYNC_LIGHT = 1,
1100    MIGRATE_SYNC = 2
1101} ;
1102#line 44
1103struct export_operations;
1104#line 44
1105struct export_operations;
1106#line 46
1107struct iovec;
1108#line 46
1109struct iovec;
1110#line 47
1111struct kiocb;
1112#line 47
1113struct kiocb;
1114#line 48
1115struct pipe_inode_info;
1116#line 48
1117struct pipe_inode_info;
1118#line 49
1119struct poll_table_struct;
1120#line 49
1121struct poll_table_struct;
1122#line 50
1123struct kstatfs;
1124#line 50
1125struct kstatfs;
1126#line 435 "include/linux/fs.h"
1127struct iattr {
1128   unsigned int ia_valid ;
1129   umode_t ia_mode ;
1130   uid_t ia_uid ;
1131   gid_t ia_gid ;
1132   loff_t ia_size ;
1133   struct timespec ia_atime ;
1134   struct timespec ia_mtime ;
1135   struct timespec ia_ctime ;
1136   struct file *ia_file ;
1137};
1138#line 119 "include/linux/quota.h"
1139struct if_dqinfo {
1140   __u64 dqi_bgrace ;
1141   __u64 dqi_igrace ;
1142   __u32 dqi_flags ;
1143   __u32 dqi_valid ;
1144};
1145#line 176 "include/linux/percpu_counter.h"
1146struct fs_disk_quota {
1147   __s8 d_version ;
1148   __s8 d_flags ;
1149   __u16 d_fieldmask ;
1150   __u32 d_id ;
1151   __u64 d_blk_hardlimit ;
1152   __u64 d_blk_softlimit ;
1153   __u64 d_ino_hardlimit ;
1154   __u64 d_ino_softlimit ;
1155   __u64 d_bcount ;
1156   __u64 d_icount ;
1157   __s32 d_itimer ;
1158   __s32 d_btimer ;
1159   __u16 d_iwarns ;
1160   __u16 d_bwarns ;
1161   __s32 d_padding2 ;
1162   __u64 d_rtb_hardlimit ;
1163   __u64 d_rtb_softlimit ;
1164   __u64 d_rtbcount ;
1165   __s32 d_rtbtimer ;
1166   __u16 d_rtbwarns ;
1167   __s16 d_padding3 ;
1168   char d_padding4[8U] ;
1169};
1170#line 75 "include/linux/dqblk_xfs.h"
1171struct fs_qfilestat {
1172   __u64 qfs_ino ;
1173   __u64 qfs_nblks ;
1174   __u32 qfs_nextents ;
1175};
1176#line 150 "include/linux/dqblk_xfs.h"
1177typedef struct fs_qfilestat fs_qfilestat_t;
1178#line 151 "include/linux/dqblk_xfs.h"
1179struct fs_quota_stat {
1180   __s8 qs_version ;
1181   __u16 qs_flags ;
1182   __s8 qs_pad ;
1183   fs_qfilestat_t qs_uquota ;
1184   fs_qfilestat_t qs_gquota ;
1185   __u32 qs_incoredqs ;
1186   __s32 qs_btimelimit ;
1187   __s32 qs_itimelimit ;
1188   __s32 qs_rtbtimelimit ;
1189   __u16 qs_bwarnlimit ;
1190   __u16 qs_iwarnlimit ;
1191};
1192#line 165
1193struct dquot;
1194#line 165
1195struct dquot;
1196#line 185 "include/linux/quota.h"
1197typedef __kernel_uid32_t qid_t;
1198#line 186 "include/linux/quota.h"
1199typedef long long qsize_t;
1200#line 189 "include/linux/quota.h"
1201struct mem_dqblk {
1202   qsize_t dqb_bhardlimit ;
1203   qsize_t dqb_bsoftlimit ;
1204   qsize_t dqb_curspace ;
1205   qsize_t dqb_rsvspace ;
1206   qsize_t dqb_ihardlimit ;
1207   qsize_t dqb_isoftlimit ;
1208   qsize_t dqb_curinodes ;
1209   time_t dqb_btime ;
1210   time_t dqb_itime ;
1211};
1212#line 211
1213struct quota_format_type;
1214#line 211
1215struct quota_format_type;
1216#line 212 "include/linux/quota.h"
1217struct mem_dqinfo {
1218   struct quota_format_type *dqi_format ;
1219   int dqi_fmt_id ;
1220   struct list_head dqi_dirty_list ;
1221   unsigned long dqi_flags ;
1222   unsigned int dqi_bgrace ;
1223   unsigned int dqi_igrace ;
1224   qsize_t dqi_maxblimit ;
1225   qsize_t dqi_maxilimit ;
1226   void *dqi_priv ;
1227};
1228#line 275 "include/linux/quota.h"
1229struct dquot {
1230   struct hlist_node dq_hash ;
1231   struct list_head dq_inuse ;
1232   struct list_head dq_free ;
1233   struct list_head dq_dirty ;
1234   struct mutex dq_lock ;
1235   atomic_t dq_count ;
1236   wait_queue_head_t dq_wait_unused ;
1237   struct super_block *dq_sb ;
1238   unsigned int dq_id ;
1239   loff_t dq_off ;
1240   unsigned long dq_flags ;
1241   short dq_type ;
1242   struct mem_dqblk dq_dqb ;
1243};
1244#line 303 "include/linux/quota.h"
1245struct quota_format_ops {
1246   int (*check_quota_file)(struct super_block * , int  ) ;
1247   int (*read_file_info)(struct super_block * , int  ) ;
1248   int (*write_file_info)(struct super_block * , int  ) ;
1249   int (*free_file_info)(struct super_block * , int  ) ;
1250   int (*read_dqblk)(struct dquot * ) ;
1251   int (*commit_dqblk)(struct dquot * ) ;
1252   int (*release_dqblk)(struct dquot * ) ;
1253};
1254#line 314 "include/linux/quota.h"
1255struct dquot_operations {
1256   int (*write_dquot)(struct dquot * ) ;
1257   struct dquot *(*alloc_dquot)(struct super_block * , int  ) ;
1258   void (*destroy_dquot)(struct dquot * ) ;
1259   int (*acquire_dquot)(struct dquot * ) ;
1260   int (*release_dquot)(struct dquot * ) ;
1261   int (*mark_dirty)(struct dquot * ) ;
1262   int (*write_info)(struct super_block * , int  ) ;
1263   qsize_t *(*get_reserved_space)(struct inode * ) ;
1264};
1265#line 328 "include/linux/quota.h"
1266struct quotactl_ops {
1267   int (*quota_on)(struct super_block * , int  , int  , struct path * ) ;
1268   int (*quota_on_meta)(struct super_block * , int  , int  ) ;
1269   int (*quota_off)(struct super_block * , int  ) ;
1270   int (*quota_sync)(struct super_block * , int  , int  ) ;
1271   int (*get_info)(struct super_block * , int  , struct if_dqinfo * ) ;
1272   int (*set_info)(struct super_block * , int  , struct if_dqinfo * ) ;
1273   int (*get_dqblk)(struct super_block * , int  , qid_t  , struct fs_disk_quota * ) ;
1274   int (*set_dqblk)(struct super_block * , int  , qid_t  , struct fs_disk_quota * ) ;
1275   int (*get_xstate)(struct super_block * , struct fs_quota_stat * ) ;
1276   int (*set_xstate)(struct super_block * , unsigned int  , int  ) ;
1277};
1278#line 344 "include/linux/quota.h"
1279struct quota_format_type {
1280   int qf_fmt_id ;
1281   struct quota_format_ops  const  *qf_ops ;
1282   struct module *qf_owner ;
1283   struct quota_format_type *qf_next ;
1284};
1285#line 390 "include/linux/quota.h"
1286struct quota_info {
1287   unsigned int flags ;
1288   struct mutex dqio_mutex ;
1289   struct mutex dqonoff_mutex ;
1290   struct rw_semaphore dqptr_sem ;
1291   struct inode *files[2U] ;
1292   struct mem_dqinfo info[2U] ;
1293   struct quota_format_ops  const  *ops[2U] ;
1294};
1295#line 585 "include/linux/fs.h"
1296union __anonunion_arg_153 {
1297   char *buf ;
1298   void *data ;
1299};
1300#line 585 "include/linux/fs.h"
1301struct __anonstruct_read_descriptor_t_152 {
1302   size_t written ;
1303   size_t count ;
1304   union __anonunion_arg_153 arg ;
1305   int error ;
1306};
1307#line 585 "include/linux/fs.h"
1308typedef struct __anonstruct_read_descriptor_t_152 read_descriptor_t;
1309#line 588 "include/linux/fs.h"
1310struct address_space_operations {
1311   int (*writepage)(struct page * , struct writeback_control * ) ;
1312   int (*readpage)(struct file * , struct page * ) ;
1313   int (*writepages)(struct address_space * , struct writeback_control * ) ;
1314   int (*set_page_dirty)(struct page * ) ;
1315   int (*readpages)(struct file * , struct address_space * , struct list_head * ,
1316                    unsigned int  ) ;
1317   int (*write_begin)(struct file * , struct address_space * , loff_t  , unsigned int  ,
1318                      unsigned int  , struct page ** , void ** ) ;
1319   int (*write_end)(struct file * , struct address_space * , loff_t  , unsigned int  ,
1320                    unsigned int  , struct page * , void * ) ;
1321   sector_t (*bmap)(struct address_space * , sector_t  ) ;
1322   void (*invalidatepage)(struct page * , unsigned long  ) ;
1323   int (*releasepage)(struct page * , gfp_t  ) ;
1324   void (*freepage)(struct page * ) ;
1325   ssize_t (*direct_IO)(int  , struct kiocb * , struct iovec  const  * , loff_t  ,
1326                        unsigned long  ) ;
1327   int (*get_xip_mem)(struct address_space * , unsigned long  , int  , void ** , unsigned long * ) ;
1328   int (*migratepage)(struct address_space * , struct page * , struct page * , enum migrate_mode  ) ;
1329   int (*launder_page)(struct page * ) ;
1330   int (*is_partially_uptodate)(struct page * , read_descriptor_t * , unsigned long  ) ;
1331   int (*error_remove_page)(struct address_space * , struct page * ) ;
1332};
1333#line 642
1334struct backing_dev_info;
1335#line 642
1336struct backing_dev_info;
1337#line 643 "include/linux/fs.h"
1338struct address_space {
1339   struct inode *host ;
1340   struct radix_tree_root page_tree ;
1341   spinlock_t tree_lock ;
1342   unsigned int i_mmap_writable ;
1343   struct prio_tree_root i_mmap ;
1344   struct list_head i_mmap_nonlinear ;
1345   struct mutex i_mmap_mutex ;
1346   unsigned long nrpages ;
1347   unsigned long writeback_index ;
1348   struct address_space_operations  const  *a_ops ;
1349   unsigned long flags ;
1350   struct backing_dev_info *backing_dev_info ;
1351   spinlock_t private_lock ;
1352   struct list_head private_list ;
1353   struct address_space *assoc_mapping ;
1354};
1355#line 664
1356struct request_queue;
1357#line 664
1358struct request_queue;
1359#line 665
1360struct hd_struct;
1361#line 665
1362struct gendisk;
1363#line 665 "include/linux/fs.h"
1364struct block_device {
1365   dev_t bd_dev ;
1366   int bd_openers ;
1367   struct inode *bd_inode ;
1368   struct super_block *bd_super ;
1369   struct mutex bd_mutex ;
1370   struct list_head bd_inodes ;
1371   void *bd_claiming ;
1372   void *bd_holder ;
1373   int bd_holders ;
1374   bool bd_write_holder ;
1375   struct list_head bd_holder_disks ;
1376   struct block_device *bd_contains ;
1377   unsigned int bd_block_size ;
1378   struct hd_struct *bd_part ;
1379   unsigned int bd_part_count ;
1380   int bd_invalidated ;
1381   struct gendisk *bd_disk ;
1382   struct request_queue *bd_queue ;
1383   struct list_head bd_list ;
1384   unsigned long bd_private ;
1385   int bd_fsfreeze_count ;
1386   struct mutex bd_fsfreeze_mutex ;
1387};
1388#line 737
1389struct posix_acl;
1390#line 737
1391struct posix_acl;
1392#line 738
1393struct inode_operations;
1394#line 738 "include/linux/fs.h"
1395union __anonunion_ldv_19358_154 {
1396   unsigned int const   i_nlink ;
1397   unsigned int __i_nlink ;
1398};
1399#line 738 "include/linux/fs.h"
1400union __anonunion_ldv_19377_155 {
1401   struct list_head i_dentry ;
1402   struct rcu_head i_rcu ;
1403};
1404#line 738
1405struct file_operations;
1406#line 738
1407struct file_lock;
1408#line 738
1409struct cdev;
1410#line 738 "include/linux/fs.h"
1411union __anonunion_ldv_19395_156 {
1412   struct pipe_inode_info *i_pipe ;
1413   struct block_device *i_bdev ;
1414   struct cdev *i_cdev ;
1415};
1416#line 738 "include/linux/fs.h"
1417struct inode {
1418   umode_t i_mode ;
1419   unsigned short i_opflags ;
1420   uid_t i_uid ;
1421   gid_t i_gid ;
1422   unsigned int i_flags ;
1423   struct posix_acl *i_acl ;
1424   struct posix_acl *i_default_acl ;
1425   struct inode_operations  const  *i_op ;
1426   struct super_block *i_sb ;
1427   struct address_space *i_mapping ;
1428   void *i_security ;
1429   unsigned long i_ino ;
1430   union __anonunion_ldv_19358_154 ldv_19358 ;
1431   dev_t i_rdev ;
1432   struct timespec i_atime ;
1433   struct timespec i_mtime ;
1434   struct timespec i_ctime ;
1435   spinlock_t i_lock ;
1436   unsigned short i_bytes ;
1437   blkcnt_t i_blocks ;
1438   loff_t i_size ;
1439   unsigned long i_state ;
1440   struct mutex i_mutex ;
1441   unsigned long dirtied_when ;
1442   struct hlist_node i_hash ;
1443   struct list_head i_wb_list ;
1444   struct list_head i_lru ;
1445   struct list_head i_sb_list ;
1446   union __anonunion_ldv_19377_155 ldv_19377 ;
1447   atomic_t i_count ;
1448   unsigned int i_blkbits ;
1449   u64 i_version ;
1450   atomic_t i_dio_count ;
1451   atomic_t i_writecount ;
1452   struct file_operations  const  *i_fop ;
1453   struct file_lock *i_flock ;
1454   struct address_space i_data ;
1455   struct dquot *i_dquot[2U] ;
1456   struct list_head i_devices ;
1457   union __anonunion_ldv_19395_156 ldv_19395 ;
1458   __u32 i_generation ;
1459   __u32 i_fsnotify_mask ;
1460   struct hlist_head i_fsnotify_marks ;
1461   atomic_t i_readcount ;
1462   void *i_private ;
1463};
1464#line 941 "include/linux/fs.h"
1465struct fown_struct {
1466   rwlock_t lock ;
1467   struct pid *pid ;
1468   enum pid_type pid_type ;
1469   uid_t uid ;
1470   uid_t euid ;
1471   int signum ;
1472};
1473#line 949 "include/linux/fs.h"
1474struct file_ra_state {
1475   unsigned long start ;
1476   unsigned int size ;
1477   unsigned int async_size ;
1478   unsigned int ra_pages ;
1479   unsigned int mmap_miss ;
1480   loff_t prev_pos ;
1481};
1482#line 972 "include/linux/fs.h"
1483union __anonunion_f_u_157 {
1484   struct list_head fu_list ;
1485   struct rcu_head fu_rcuhead ;
1486};
1487#line 972 "include/linux/fs.h"
1488struct file {
1489   union __anonunion_f_u_157 f_u ;
1490   struct path f_path ;
1491   struct file_operations  const  *f_op ;
1492   spinlock_t f_lock ;
1493   int f_sb_list_cpu ;
1494   atomic_long_t f_count ;
1495   unsigned int f_flags ;
1496   fmode_t f_mode ;
1497   loff_t f_pos ;
1498   struct fown_struct f_owner ;
1499   struct cred  const  *f_cred ;
1500   struct file_ra_state f_ra ;
1501   u64 f_version ;
1502   void *f_security ;
1503   void *private_data ;
1504   struct list_head f_ep_links ;
1505   struct list_head f_tfile_llink ;
1506   struct address_space *f_mapping ;
1507   unsigned long f_mnt_write_state ;
1508};
1509#line 1111
1510struct files_struct;
1511#line 1111 "include/linux/fs.h"
1512typedef struct files_struct *fl_owner_t;
1513#line 1112 "include/linux/fs.h"
1514struct file_lock_operations {
1515   void (*fl_copy_lock)(struct file_lock * , struct file_lock * ) ;
1516   void (*fl_release_private)(struct file_lock * ) ;
1517};
1518#line 1117 "include/linux/fs.h"
1519struct lock_manager_operations {
1520   int (*lm_compare_owner)(struct file_lock * , struct file_lock * ) ;
1521   void (*lm_notify)(struct file_lock * ) ;
1522   int (*lm_grant)(struct file_lock * , struct file_lock * , int  ) ;
1523   void (*lm_release_private)(struct file_lock * ) ;
1524   void (*lm_break)(struct file_lock * ) ;
1525   int (*lm_change)(struct file_lock ** , int  ) ;
1526};
1527#line 1134
1528struct nlm_lockowner;
1529#line 1134
1530struct nlm_lockowner;
1531#line 1135 "include/linux/fs.h"
1532struct nfs_lock_info {
1533   u32 state ;
1534   struct nlm_lockowner *owner ;
1535   struct list_head list ;
1536};
1537#line 14 "include/linux/nfs_fs_i.h"
1538struct nfs4_lock_state;
1539#line 14
1540struct nfs4_lock_state;
1541#line 15 "include/linux/nfs_fs_i.h"
1542struct nfs4_lock_info {
1543   struct nfs4_lock_state *owner ;
1544};
1545#line 19
1546struct fasync_struct;
1547#line 19 "include/linux/nfs_fs_i.h"
1548struct __anonstruct_afs_159 {
1549   struct list_head link ;
1550   int state ;
1551};
1552#line 19 "include/linux/nfs_fs_i.h"
1553union __anonunion_fl_u_158 {
1554   struct nfs_lock_info nfs_fl ;
1555   struct nfs4_lock_info nfs4_fl ;
1556   struct __anonstruct_afs_159 afs ;
1557};
1558#line 19 "include/linux/nfs_fs_i.h"
1559struct file_lock {
1560   struct file_lock *fl_next ;
1561   struct list_head fl_link ;
1562   struct list_head fl_block ;
1563   fl_owner_t fl_owner ;
1564   unsigned int fl_flags ;
1565   unsigned char fl_type ;
1566   unsigned int fl_pid ;
1567   struct pid *fl_nspid ;
1568   wait_queue_head_t fl_wait ;
1569   struct file *fl_file ;
1570   loff_t fl_start ;
1571   loff_t fl_end ;
1572   struct fasync_struct *fl_fasync ;
1573   unsigned long fl_break_time ;
1574   unsigned long fl_downgrade_time ;
1575   struct file_lock_operations  const  *fl_ops ;
1576   struct lock_manager_operations  const  *fl_lmops ;
1577   union __anonunion_fl_u_158 fl_u ;
1578};
1579#line 1221 "include/linux/fs.h"
1580struct fasync_struct {
1581   spinlock_t fa_lock ;
1582   int magic ;
1583   int fa_fd ;
1584   struct fasync_struct *fa_next ;
1585   struct file *fa_file ;
1586   struct rcu_head fa_rcu ;
1587};
1588#line 1417
1589struct file_system_type;
1590#line 1417
1591struct super_operations;
1592#line 1417
1593struct xattr_handler;
1594#line 1417
1595struct mtd_info;
1596#line 1417 "include/linux/fs.h"
1597struct super_block {
1598   struct list_head s_list ;
1599   dev_t s_dev ;
1600   unsigned char s_dirt ;
1601   unsigned char s_blocksize_bits ;
1602   unsigned long s_blocksize ;
1603   loff_t s_maxbytes ;
1604   struct file_system_type *s_type ;
1605   struct super_operations  const  *s_op ;
1606   struct dquot_operations  const  *dq_op ;
1607   struct quotactl_ops  const  *s_qcop ;
1608   struct export_operations  const  *s_export_op ;
1609   unsigned long s_flags ;
1610   unsigned long s_magic ;
1611   struct dentry *s_root ;
1612   struct rw_semaphore s_umount ;
1613   struct mutex s_lock ;
1614   int s_count ;
1615   atomic_t s_active ;
1616   void *s_security ;
1617   struct xattr_handler  const  **s_xattr ;
1618   struct list_head s_inodes ;
1619   struct hlist_bl_head s_anon ;
1620   struct list_head *s_files ;
1621   struct list_head s_mounts ;
1622   struct list_head s_dentry_lru ;
1623   int s_nr_dentry_unused ;
1624   spinlock_t s_inode_lru_lock ;
1625   struct list_head s_inode_lru ;
1626   int s_nr_inodes_unused ;
1627   struct block_device *s_bdev ;
1628   struct backing_dev_info *s_bdi ;
1629   struct mtd_info *s_mtd ;
1630   struct hlist_node s_instances ;
1631   struct quota_info s_dquot ;
1632   int s_frozen ;
1633   wait_queue_head_t s_wait_unfrozen ;
1634   char s_id[32U] ;
1635   u8 s_uuid[16U] ;
1636   void *s_fs_info ;
1637   unsigned int s_max_links ;
1638   fmode_t s_mode ;
1639   u32 s_time_gran ;
1640   struct mutex s_vfs_rename_mutex ;
1641   char *s_subtype ;
1642   char *s_options ;
1643   struct dentry_operations  const  *s_d_op ;
1644   int cleancache_poolid ;
1645   struct shrinker s_shrink ;
1646   atomic_long_t s_remove_count ;
1647   int s_readonly_remount ;
1648};
1649#line 1563 "include/linux/fs.h"
1650struct fiemap_extent_info {
1651   unsigned int fi_flags ;
1652   unsigned int fi_extents_mapped ;
1653   unsigned int fi_extents_max ;
1654   struct fiemap_extent *fi_extents_start ;
1655};
1656#line 1602 "include/linux/fs.h"
1657struct file_operations {
1658   struct module *owner ;
1659   loff_t (*llseek)(struct file * , loff_t  , int  ) ;
1660   ssize_t (*read)(struct file * , char * , size_t  , loff_t * ) ;
1661   ssize_t (*write)(struct file * , char const   * , size_t  , loff_t * ) ;
1662   ssize_t (*aio_read)(struct kiocb * , struct iovec  const  * , unsigned long  ,
1663                       loff_t  ) ;
1664   ssize_t (*aio_write)(struct kiocb * , struct iovec  const  * , unsigned long  ,
1665                        loff_t  ) ;
1666   int (*readdir)(struct file * , void * , int (*)(void * , char const   * , int  ,
1667                                                   loff_t  , u64  , unsigned int  ) ) ;
1668   unsigned int (*poll)(struct file * , struct poll_table_struct * ) ;
1669   long (*unlocked_ioctl)(struct file * , unsigned int  , unsigned long  ) ;
1670   long (*compat_ioctl)(struct file * , unsigned int  , unsigned long  ) ;
1671   int (*mmap)(struct file * , struct vm_area_struct * ) ;
1672   int (*open)(struct inode * , struct file * ) ;
1673   int (*flush)(struct file * , fl_owner_t  ) ;
1674   int (*release)(struct inode * , struct file * ) ;
1675   int (*fsync)(struct file * , loff_t  , loff_t  , int  ) ;
1676   int (*aio_fsync)(struct kiocb * , int  ) ;
1677   int (*fasync)(int  , struct file * , int  ) ;
1678   int (*lock)(struct file * , int  , struct file_lock * ) ;
1679   ssize_t (*sendpage)(struct file * , struct page * , int  , size_t  , loff_t * ,
1680                       int  ) ;
1681   unsigned long (*get_unmapped_area)(struct file * , unsigned long  , unsigned long  ,
1682                                      unsigned long  , unsigned long  ) ;
1683   int (*check_flags)(int  ) ;
1684   int (*flock)(struct file * , int  , struct file_lock * ) ;
1685   ssize_t (*splice_write)(struct pipe_inode_info * , struct file * , loff_t * , size_t  ,
1686                           unsigned int  ) ;
1687   ssize_t (*splice_read)(struct file * , loff_t * , struct pipe_inode_info * , size_t  ,
1688                          unsigned int  ) ;
1689   int (*setlease)(struct file * , long  , struct file_lock ** ) ;
1690   long (*fallocate)(struct file * , int  , loff_t  , loff_t  ) ;
1691};
1692#line 1637 "include/linux/fs.h"
1693struct inode_operations {
1694   struct dentry *(*lookup)(struct inode * , struct dentry * , struct nameidata * ) ;
1695   void *(*follow_link)(struct dentry * , struct nameidata * ) ;
1696   int (*permission)(struct inode * , int  ) ;
1697   struct posix_acl *(*get_acl)(struct inode * , int  ) ;
1698   int (*readlink)(struct dentry * , char * , int  ) ;
1699   void (*put_link)(struct dentry * , struct nameidata * , void * ) ;
1700   int (*create)(struct inode * , struct dentry * , umode_t  , struct nameidata * ) ;
1701   int (*link)(struct dentry * , struct inode * , struct dentry * ) ;
1702   int (*unlink)(struct inode * , struct dentry * ) ;
1703   int (*symlink)(struct inode * , struct dentry * , char const   * ) ;
1704   int (*mkdir)(struct inode * , struct dentry * , umode_t  ) ;
1705   int (*rmdir)(struct inode * , struct dentry * ) ;
1706   int (*mknod)(struct inode * , struct dentry * , umode_t  , dev_t  ) ;
1707   int (*rename)(struct inode * , struct dentry * , struct inode * , struct dentry * ) ;
1708   void (*truncate)(struct inode * ) ;
1709   int (*setattr)(struct dentry * , struct iattr * ) ;
1710   int (*getattr)(struct vfsmount * , struct dentry * , struct kstat * ) ;
1711   int (*setxattr)(struct dentry * , char const   * , void const   * , size_t  , int  ) ;
1712   ssize_t (*getxattr)(struct dentry * , char const   * , void * , size_t  ) ;
1713   ssize_t (*listxattr)(struct dentry * , char * , size_t  ) ;
1714   int (*removexattr)(struct dentry * , char const   * ) ;
1715   void (*truncate_range)(struct inode * , loff_t  , loff_t  ) ;
1716   int (*fiemap)(struct inode * , struct fiemap_extent_info * , u64  , u64  ) ;
1717};
1718#line 1682 "include/linux/fs.h"
1719struct super_operations {
1720   struct inode *(*alloc_inode)(struct super_block * ) ;
1721   void (*destroy_inode)(struct inode * ) ;
1722   void (*dirty_inode)(struct inode * , int  ) ;
1723   int (*write_inode)(struct inode * , struct writeback_control * ) ;
1724   int (*drop_inode)(struct inode * ) ;
1725   void (*evict_inode)(struct inode * ) ;
1726   void (*put_super)(struct super_block * ) ;
1727   void (*write_super)(struct super_block * ) ;
1728   int (*sync_fs)(struct super_block * , int  ) ;
1729   int (*freeze_fs)(struct super_block * ) ;
1730   int (*unfreeze_fs)(struct super_block * ) ;
1731   int (*statfs)(struct dentry * , struct kstatfs * ) ;
1732   int (*remount_fs)(struct super_block * , int * , char * ) ;
1733   void (*umount_begin)(struct super_block * ) ;
1734   int (*show_options)(struct seq_file * , struct dentry * ) ;
1735   int (*show_devname)(struct seq_file * , struct dentry * ) ;
1736   int (*show_path)(struct seq_file * , struct dentry * ) ;
1737   int (*show_stats)(struct seq_file * , struct dentry * ) ;
1738   ssize_t (*quota_read)(struct super_block * , int  , char * , size_t  , loff_t  ) ;
1739   ssize_t (*quota_write)(struct super_block * , int  , char const   * , size_t  ,
1740                          loff_t  ) ;
1741   int (*bdev_try_to_free_page)(struct super_block * , struct page * , gfp_t  ) ;
1742   int (*nr_cached_objects)(struct super_block * ) ;
1743   void (*free_cached_objects)(struct super_block * , int  ) ;
1744};
1745#line 1834 "include/linux/fs.h"
1746struct file_system_type {
1747   char const   *name ;
1748   int fs_flags ;
1749   struct dentry *(*mount)(struct file_system_type * , int  , char const   * , void * ) ;
1750   void (*kill_sb)(struct super_block * ) ;
1751   struct module *owner ;
1752   struct file_system_type *next ;
1753   struct hlist_head fs_supers ;
1754   struct lock_class_key s_lock_key ;
1755   struct lock_class_key s_umount_key ;
1756   struct lock_class_key s_vfs_rename_key ;
1757   struct lock_class_key i_lock_key ;
1758   struct lock_class_key i_mutex_key ;
1759   struct lock_class_key i_mutex_dir_key ;
1760};
1761#line 1650 "include/linux/input.h"
1762struct rc_map_table {
1763   u32 scancode ;
1764   u32 keycode ;
1765};
1766#line 35 "include/media/rc-map.h"
1767struct rc_map {
1768   struct rc_map_table *scan ;
1769   unsigned int size ;
1770   unsigned int len ;
1771   unsigned int alloc ;
1772   u64 rc_type ;
1773   char const   *name ;
1774   spinlock_t lock ;
1775};
1776#line 45 "include/media/rc-map.h"
1777struct rc_map_list {
1778   struct list_head list ;
1779   struct rc_map map ;
1780};
1781#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9168/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-lirc.c.p"
1782void ldv_spin_lock(void) ;
1783#line 3
1784void ldv_spin_unlock(void) ;
1785#line 4
1786int ldv_spin_trylock(void) ;
1787#line 220 "include/linux/slub_def.h"
1788extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t  ) ;
1789#line 223
1790void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
1791#line 11 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9168/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-lirc.c.p"
1792void ldv_check_alloc_flags(gfp_t flags ) ;
1793#line 12
1794void ldv_check_alloc_nonatomic(void) ;
1795#line 14
1796struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
1797#line 53 "include/media/rc-map.h"
1798extern int rc_map_register(struct rc_map_list * ) ;
1799#line 54
1800extern void rc_map_unregister(struct rc_map_list * ) ;
1801#line 30 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9168/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-lirc.c.p"
1802static struct rc_map_table lirc[1U]  = {      {0U, 0U}};
1803#line 34 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9168/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-lirc.c.p"
1804static struct rc_map_list lirc_map  =    {{(struct list_head *)0, (struct list_head *)0}, {(struct rc_map_table *)(& lirc),
1805                                                     1U, 0U, 0U, 1073741824ULL, "rc-lirc",
1806                                                     {{{{{0U}}, 0U, 0U, (void *)0,
1807                                                        {(struct lock_class_key *)0,
1808                                                         {(struct lock_class *)0,
1809                                                          (struct lock_class *)0},
1810                                                         (char const   *)0, 0, 0UL}}}}}};
1811#line 43 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9168/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-lirc.c.p"
1812static int init_rc_map_lirc(void) 
1813{ int tmp ;
1814
1815  {
1816  {
1817#line 45
1818  tmp = rc_map_register(& lirc_map);
1819  }
1820#line 45
1821  return (tmp);
1822}
1823}
1824#line 48 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9168/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-lirc.c.p"
1825static void exit_rc_map_lirc(void) 
1826{ 
1827
1828  {
1829  {
1830#line 50
1831  rc_map_unregister(& lirc_map);
1832  }
1833#line 51
1834  return;
1835}
1836}
1837#line 75
1838extern void ldv_check_final_state(void) ;
1839#line 81
1840extern void ldv_initialize(void) ;
1841#line 84
1842extern int __VERIFIER_nondet_int(void) ;
1843#line 87 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9168/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-lirc.c.p"
1844int LDV_IN_INTERRUPT  ;
1845#line 90 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9168/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-lirc.c.p"
1846void main(void) 
1847{ int tmp ;
1848  int tmp___0 ;
1849  int tmp___1 ;
1850
1851  {
1852  {
1853#line 102
1854  LDV_IN_INTERRUPT = 1;
1855#line 111
1856  ldv_initialize();
1857#line 117
1858  tmp = init_rc_map_lirc();
1859  }
1860#line 117
1861  if (tmp != 0) {
1862#line 118
1863    goto ldv_final;
1864  } else {
1865
1866  }
1867#line 120
1868  goto ldv_21995;
1869  ldv_21994: 
1870  {
1871#line 123
1872  tmp___0 = __VERIFIER_nondet_int();
1873  }
1874  {
1875#line 125
1876  goto switch_default;
1877#line 123
1878  if (0) {
1879    switch_default: /* CIL Label */ ;
1880#line 125
1881    goto ldv_21993;
1882  } else {
1883    switch_break: /* CIL Label */ ;
1884  }
1885  }
1886  ldv_21993: ;
1887  ldv_21995: 
1888  {
1889#line 120
1890  tmp___1 = __VERIFIER_nondet_int();
1891  }
1892#line 120
1893  if (tmp___1 != 0) {
1894#line 121
1895    goto ldv_21994;
1896  } else {
1897#line 123
1898    goto ldv_21996;
1899  }
1900  ldv_21996: ;
1901  {
1902#line 137
1903  exit_rc_map_lirc();
1904  }
1905  ldv_final: 
1906  {
1907#line 140
1908  ldv_check_final_state();
1909  }
1910#line 143
1911  return;
1912}
1913}
1914#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9168/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
1915void ldv_blast_assert(void) 
1916{ 
1917
1918  {
1919  ERROR: ;
1920#line 6
1921  goto ERROR;
1922}
1923}
1924#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9168/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
1925extern int __VERIFIER_nondet_int(void) ;
1926#line 164 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9168/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-lirc.c.p"
1927int ldv_spin  =    0;
1928#line 168 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9168/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-lirc.c.p"
1929void ldv_check_alloc_flags(gfp_t flags ) 
1930{ 
1931
1932  {
1933#line 171
1934  if (ldv_spin != 0) {
1935#line 171
1936    if (flags != 32U) {
1937      {
1938#line 171
1939      ldv_blast_assert();
1940      }
1941    } else {
1942
1943    }
1944  } else {
1945
1946  }
1947#line 174
1948  return;
1949}
1950}
1951#line 174
1952extern struct page *ldv_some_page(void) ;
1953#line 177 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9168/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-lirc.c.p"
1954struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) 
1955{ struct page *tmp ;
1956
1957  {
1958#line 180
1959  if (ldv_spin != 0) {
1960#line 180
1961    if (flags != 32U) {
1962      {
1963#line 180
1964      ldv_blast_assert();
1965      }
1966    } else {
1967
1968    }
1969  } else {
1970
1971  }
1972  {
1973#line 182
1974  tmp = ldv_some_page();
1975  }
1976#line 182
1977  return (tmp);
1978}
1979}
1980#line 186 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9168/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-lirc.c.p"
1981void ldv_check_alloc_nonatomic(void) 
1982{ 
1983
1984  {
1985#line 189
1986  if (ldv_spin != 0) {
1987    {
1988#line 189
1989    ldv_blast_assert();
1990    }
1991  } else {
1992
1993  }
1994#line 192
1995  return;
1996}
1997}
1998#line 193 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9168/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-lirc.c.p"
1999void ldv_spin_lock(void) 
2000{ 
2001
2002  {
2003#line 196
2004  ldv_spin = 1;
2005#line 197
2006  return;
2007}
2008}
2009#line 200 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9168/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-lirc.c.p"
2010void ldv_spin_unlock(void) 
2011{ 
2012
2013  {
2014#line 203
2015  ldv_spin = 0;
2016#line 204
2017  return;
2018}
2019}
2020#line 207 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9168/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-lirc.c.p"
2021int ldv_spin_trylock(void) 
2022{ int is_lock ;
2023
2024  {
2025  {
2026#line 212
2027  is_lock = __VERIFIER_nondet_int();
2028  }
2029#line 214
2030  if (is_lock != 0) {
2031#line 217
2032    return (0);
2033  } else {
2034#line 222
2035    ldv_spin = 1;
2036#line 224
2037    return (1);
2038  }
2039}
2040}
2041#line 391 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9168/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-lirc.c.p"
2042void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) 
2043{ 
2044
2045  {
2046  {
2047#line 397
2048  ldv_check_alloc_flags(ldv_func_arg2);
2049#line 399
2050  kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
2051  }
2052#line 400
2053  return ((void *)0);
2054}
2055}