Showing error 1237

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--staging--iio--kfifo_buf.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 2131
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 23 "include/asm-generic/int-ll64.h"
   5typedef unsigned short __u16;
   6#line 26 "include/asm-generic/int-ll64.h"
   7typedef unsigned int __u32;
   8#line 30 "include/asm-generic/int-ll64.h"
   9typedef unsigned long long __u64;
  10#line 43 "include/asm-generic/int-ll64.h"
  11typedef unsigned char u8;
  12#line 45 "include/asm-generic/int-ll64.h"
  13typedef short s16;
  14#line 46 "include/asm-generic/int-ll64.h"
  15typedef unsigned short u16;
  16#line 49 "include/asm-generic/int-ll64.h"
  17typedef unsigned int u32;
  18#line 51 "include/asm-generic/int-ll64.h"
  19typedef long long s64;
  20#line 52 "include/asm-generic/int-ll64.h"
  21typedef unsigned long long u64;
  22#line 14 "include/asm-generic/posix_types.h"
  23typedef long __kernel_long_t;
  24#line 15 "include/asm-generic/posix_types.h"
  25typedef unsigned long __kernel_ulong_t;
  26#line 75 "include/asm-generic/posix_types.h"
  27typedef __kernel_ulong_t __kernel_size_t;
  28#line 76 "include/asm-generic/posix_types.h"
  29typedef __kernel_long_t __kernel_ssize_t;
  30#line 91 "include/asm-generic/posix_types.h"
  31typedef long long __kernel_loff_t;
  32#line 21 "include/linux/types.h"
  33typedef __u32 __kernel_dev_t;
  34#line 24 "include/linux/types.h"
  35typedef __kernel_dev_t dev_t;
  36#line 27 "include/linux/types.h"
  37typedef unsigned short umode_t;
  38#line 38 "include/linux/types.h"
  39typedef _Bool bool;
  40#line 54 "include/linux/types.h"
  41typedef __kernel_loff_t loff_t;
  42#line 63 "include/linux/types.h"
  43typedef __kernel_size_t size_t;
  44#line 68 "include/linux/types.h"
  45typedef __kernel_ssize_t ssize_t;
  46#line 202 "include/linux/types.h"
  47typedef unsigned int gfp_t;
  48#line 221 "include/linux/types.h"
  49struct __anonstruct_atomic_t_6 {
  50   int counter ;
  51};
  52#line 221 "include/linux/types.h"
  53typedef struct __anonstruct_atomic_t_6 atomic_t;
  54#line 226 "include/linux/types.h"
  55struct __anonstruct_atomic64_t_7 {
  56   long counter ;
  57};
  58#line 226 "include/linux/types.h"
  59typedef struct __anonstruct_atomic64_t_7 atomic64_t;
  60#line 227 "include/linux/types.h"
  61struct list_head {
  62   struct list_head *next ;
  63   struct list_head *prev ;
  64};
  65#line 232
  66struct hlist_node;
  67#line 232 "include/linux/types.h"
  68struct hlist_head {
  69   struct hlist_node *first ;
  70};
  71#line 236 "include/linux/types.h"
  72struct hlist_node {
  73   struct hlist_node *next ;
  74   struct hlist_node **pprev ;
  75};
  76#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
  77struct module;
  78#line 55
  79struct module;
  80#line 146 "include/linux/init.h"
  81typedef void (*ctor_fn_t)(void);
  82#line 46 "include/linux/dynamic_debug.h"
  83struct device;
  84#line 46
  85struct device;
  86#line 57
  87struct completion;
  88#line 57
  89struct completion;
  90#line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
  91struct page;
  92#line 58
  93struct page;
  94#line 26 "include/asm-generic/getorder.h"
  95struct task_struct;
  96#line 26
  97struct task_struct;
  98#line 28
  99struct mm_struct;
 100#line 28
 101struct mm_struct;
 102#line 13 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
 103typedef unsigned long pgdval_t;
 104#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
 105typedef unsigned long pgprotval_t;
 106#line 18 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
 107struct pgprot {
 108   pgprotval_t pgprot ;
 109};
 110#line 192 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 111typedef struct pgprot pgprot_t;
 112#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 113struct __anonstruct_pgd_t_16 {
 114   pgdval_t pgd ;
 115};
 116#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 117typedef struct __anonstruct_pgd_t_16 pgd_t;
 118#line 282 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 119typedef struct page *pgtable_t;
 120#line 290
 121struct file;
 122#line 290
 123struct file;
 124#line 339
 125struct cpumask;
 126#line 339
 127struct cpumask;
 128#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
 129struct arch_spinlock;
 130#line 327
 131struct arch_spinlock;
 132#line 306 "include/linux/bitmap.h"
 133struct bug_entry {
 134   int bug_addr_disp ;
 135   int file_disp ;
 136   unsigned short line ;
 137   unsigned short flags ;
 138};
 139#line 89 "include/linux/bug.h"
 140struct cpumask {
 141   unsigned long bits[64U] ;
 142};
 143#line 637 "include/linux/cpumask.h"
 144typedef struct cpumask *cpumask_var_t;
 145#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
 146struct static_key;
 147#line 234
 148struct static_key;
 149#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 150struct kmem_cache;
 151#line 23 "include/asm-generic/atomic-long.h"
 152typedef atomic64_t atomic_long_t;
 153#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 154typedef u16 __ticket_t;
 155#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 156typedef u32 __ticketpair_t;
 157#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 158struct __raw_tickets {
 159   __ticket_t head ;
 160   __ticket_t tail ;
 161};
 162#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 163union __anonunion_ldv_5907_29 {
 164   __ticketpair_t head_tail ;
 165   struct __raw_tickets tickets ;
 166};
 167#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 168struct arch_spinlock {
 169   union __anonunion_ldv_5907_29 ldv_5907 ;
 170};
 171#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 172typedef struct arch_spinlock arch_spinlock_t;
 173#line 34 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 174struct lockdep_map;
 175#line 34
 176struct lockdep_map;
 177#line 55 "include/linux/debug_locks.h"
 178struct stack_trace {
 179   unsigned int nr_entries ;
 180   unsigned int max_entries ;
 181   unsigned long *entries ;
 182   int skip ;
 183};
 184#line 26 "include/linux/stacktrace.h"
 185struct lockdep_subclass_key {
 186   char __one_byte ;
 187};
 188#line 53 "include/linux/lockdep.h"
 189struct lock_class_key {
 190   struct lockdep_subclass_key subkeys[8U] ;
 191};
 192#line 59 "include/linux/lockdep.h"
 193struct lock_class {
 194   struct list_head hash_entry ;
 195   struct list_head lock_entry ;
 196   struct lockdep_subclass_key *key ;
 197   unsigned int subclass ;
 198   unsigned int dep_gen_id ;
 199   unsigned long usage_mask ;
 200   struct stack_trace usage_traces[13U] ;
 201   struct list_head locks_after ;
 202   struct list_head locks_before ;
 203   unsigned int version ;
 204   unsigned long ops ;
 205   char const   *name ;
 206   int name_version ;
 207   unsigned long contention_point[4U] ;
 208   unsigned long contending_point[4U] ;
 209};
 210#line 144 "include/linux/lockdep.h"
 211struct lockdep_map {
 212   struct lock_class_key *key ;
 213   struct lock_class *class_cache[2U] ;
 214   char const   *name ;
 215   int cpu ;
 216   unsigned long ip ;
 217};
 218#line 556 "include/linux/lockdep.h"
 219struct raw_spinlock {
 220   arch_spinlock_t raw_lock ;
 221   unsigned int magic ;
 222   unsigned int owner_cpu ;
 223   void *owner ;
 224   struct lockdep_map dep_map ;
 225};
 226#line 32 "include/linux/spinlock_types.h"
 227typedef struct raw_spinlock raw_spinlock_t;
 228#line 33 "include/linux/spinlock_types.h"
 229struct __anonstruct_ldv_6122_33 {
 230   u8 __padding[24U] ;
 231   struct lockdep_map dep_map ;
 232};
 233#line 33 "include/linux/spinlock_types.h"
 234union __anonunion_ldv_6123_32 {
 235   struct raw_spinlock rlock ;
 236   struct __anonstruct_ldv_6122_33 ldv_6122 ;
 237};
 238#line 33 "include/linux/spinlock_types.h"
 239struct spinlock {
 240   union __anonunion_ldv_6123_32 ldv_6123 ;
 241};
 242#line 76 "include/linux/spinlock_types.h"
 243typedef struct spinlock spinlock_t;
 244#line 48 "include/linux/wait.h"
 245struct __wait_queue_head {
 246   spinlock_t lock ;
 247   struct list_head task_list ;
 248};
 249#line 53 "include/linux/wait.h"
 250typedef struct __wait_queue_head wait_queue_head_t;
 251#line 98 "include/linux/nodemask.h"
 252struct __anonstruct_nodemask_t_36 {
 253   unsigned long bits[16U] ;
 254};
 255#line 98 "include/linux/nodemask.h"
 256typedef struct __anonstruct_nodemask_t_36 nodemask_t;
 257#line 670 "include/linux/mmzone.h"
 258struct mutex {
 259   atomic_t count ;
 260   spinlock_t wait_lock ;
 261   struct list_head wait_list ;
 262   struct task_struct *owner ;
 263   char const   *name ;
 264   void *magic ;
 265   struct lockdep_map dep_map ;
 266};
 267#line 171 "include/linux/mutex.h"
 268struct rw_semaphore;
 269#line 171
 270struct rw_semaphore;
 271#line 172 "include/linux/mutex.h"
 272struct rw_semaphore {
 273   long count ;
 274   raw_spinlock_t wait_lock ;
 275   struct list_head wait_list ;
 276   struct lockdep_map dep_map ;
 277};
 278#line 128 "include/linux/rwsem.h"
 279struct completion {
 280   unsigned int done ;
 281   wait_queue_head_t wait ;
 282};
 283#line 312 "include/linux/jiffies.h"
 284union ktime {
 285   s64 tv64 ;
 286};
 287#line 59 "include/linux/ktime.h"
 288typedef union ktime ktime_t;
 289#line 341
 290struct tvec_base;
 291#line 341
 292struct tvec_base;
 293#line 342 "include/linux/ktime.h"
 294struct timer_list {
 295   struct list_head entry ;
 296   unsigned long expires ;
 297   struct tvec_base *base ;
 298   void (*function)(unsigned long  ) ;
 299   unsigned long data ;
 300   int slack ;
 301   int start_pid ;
 302   void *start_site ;
 303   char start_comm[16U] ;
 304   struct lockdep_map lockdep_map ;
 305};
 306#line 302 "include/linux/timer.h"
 307struct work_struct;
 308#line 302
 309struct work_struct;
 310#line 45 "include/linux/workqueue.h"
 311struct work_struct {
 312   atomic_long_t data ;
 313   struct list_head entry ;
 314   void (*func)(struct work_struct * ) ;
 315   struct lockdep_map lockdep_map ;
 316};
 317#line 46 "include/linux/pm.h"
 318struct pm_message {
 319   int event ;
 320};
 321#line 52 "include/linux/pm.h"
 322typedef struct pm_message pm_message_t;
 323#line 53 "include/linux/pm.h"
 324struct dev_pm_ops {
 325   int (*prepare)(struct device * ) ;
 326   void (*complete)(struct device * ) ;
 327   int (*suspend)(struct device * ) ;
 328   int (*resume)(struct device * ) ;
 329   int (*freeze)(struct device * ) ;
 330   int (*thaw)(struct device * ) ;
 331   int (*poweroff)(struct device * ) ;
 332   int (*restore)(struct device * ) ;
 333   int (*suspend_late)(struct device * ) ;
 334   int (*resume_early)(struct device * ) ;
 335   int (*freeze_late)(struct device * ) ;
 336   int (*thaw_early)(struct device * ) ;
 337   int (*poweroff_late)(struct device * ) ;
 338   int (*restore_early)(struct device * ) ;
 339   int (*suspend_noirq)(struct device * ) ;
 340   int (*resume_noirq)(struct device * ) ;
 341   int (*freeze_noirq)(struct device * ) ;
 342   int (*thaw_noirq)(struct device * ) ;
 343   int (*poweroff_noirq)(struct device * ) ;
 344   int (*restore_noirq)(struct device * ) ;
 345   int (*runtime_suspend)(struct device * ) ;
 346   int (*runtime_resume)(struct device * ) ;
 347   int (*runtime_idle)(struct device * ) ;
 348};
 349#line 289
 350enum rpm_status {
 351    RPM_ACTIVE = 0,
 352    RPM_RESUMING = 1,
 353    RPM_SUSPENDED = 2,
 354    RPM_SUSPENDING = 3
 355} ;
 356#line 296
 357enum rpm_request {
 358    RPM_REQ_NONE = 0,
 359    RPM_REQ_IDLE = 1,
 360    RPM_REQ_SUSPEND = 2,
 361    RPM_REQ_AUTOSUSPEND = 3,
 362    RPM_REQ_RESUME = 4
 363} ;
 364#line 304
 365struct wakeup_source;
 366#line 304
 367struct wakeup_source;
 368#line 494 "include/linux/pm.h"
 369struct pm_subsys_data {
 370   spinlock_t lock ;
 371   unsigned int refcount ;
 372};
 373#line 499
 374struct dev_pm_qos_request;
 375#line 499
 376struct pm_qos_constraints;
 377#line 499 "include/linux/pm.h"
 378struct dev_pm_info {
 379   pm_message_t power_state ;
 380   unsigned char can_wakeup : 1 ;
 381   unsigned char async_suspend : 1 ;
 382   bool is_prepared ;
 383   bool is_suspended ;
 384   bool ignore_children ;
 385   spinlock_t lock ;
 386   struct list_head entry ;
 387   struct completion completion ;
 388   struct wakeup_source *wakeup ;
 389   bool wakeup_path ;
 390   struct timer_list suspend_timer ;
 391   unsigned long timer_expires ;
 392   struct work_struct work ;
 393   wait_queue_head_t wait_queue ;
 394   atomic_t usage_count ;
 395   atomic_t child_count ;
 396   unsigned char disable_depth : 3 ;
 397   unsigned char idle_notification : 1 ;
 398   unsigned char request_pending : 1 ;
 399   unsigned char deferred_resume : 1 ;
 400   unsigned char run_wake : 1 ;
 401   unsigned char runtime_auto : 1 ;
 402   unsigned char no_callbacks : 1 ;
 403   unsigned char irq_safe : 1 ;
 404   unsigned char use_autosuspend : 1 ;
 405   unsigned char timer_autosuspends : 1 ;
 406   enum rpm_request request ;
 407   enum rpm_status runtime_status ;
 408   int runtime_error ;
 409   int autosuspend_delay ;
 410   unsigned long last_busy ;
 411   unsigned long active_jiffies ;
 412   unsigned long suspended_jiffies ;
 413   unsigned long accounting_timestamp ;
 414   ktime_t suspend_time ;
 415   s64 max_time_suspended_ns ;
 416   struct dev_pm_qos_request *pq_req ;
 417   struct pm_subsys_data *subsys_data ;
 418   struct pm_qos_constraints *constraints ;
 419};
 420#line 558 "include/linux/pm.h"
 421struct dev_pm_domain {
 422   struct dev_pm_ops ops ;
 423};
 424#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
 425struct __anonstruct_mm_context_t_101 {
 426   void *ldt ;
 427   int size ;
 428   unsigned short ia32_compat ;
 429   struct mutex lock ;
 430   void *vdso ;
 431};
 432#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
 433typedef struct __anonstruct_mm_context_t_101 mm_context_t;
 434#line 18 "include/asm-generic/pci_iomap.h"
 435struct vm_area_struct;
 436#line 18
 437struct vm_area_struct;
 438#line 835 "include/linux/sysctl.h"
 439struct rb_node {
 440   unsigned long rb_parent_color ;
 441   struct rb_node *rb_right ;
 442   struct rb_node *rb_left ;
 443};
 444#line 108 "include/linux/rbtree.h"
 445struct rb_root {
 446   struct rb_node *rb_node ;
 447};
 448#line 18 "include/linux/elf.h"
 449typedef __u64 Elf64_Addr;
 450#line 19 "include/linux/elf.h"
 451typedef __u16 Elf64_Half;
 452#line 23 "include/linux/elf.h"
 453typedef __u32 Elf64_Word;
 454#line 24 "include/linux/elf.h"
 455typedef __u64 Elf64_Xword;
 456#line 193 "include/linux/elf.h"
 457struct elf64_sym {
 458   Elf64_Word st_name ;
 459   unsigned char st_info ;
 460   unsigned char st_other ;
 461   Elf64_Half st_shndx ;
 462   Elf64_Addr st_value ;
 463   Elf64_Xword st_size ;
 464};
 465#line 201 "include/linux/elf.h"
 466typedef struct elf64_sym Elf64_Sym;
 467#line 445
 468struct sock;
 469#line 445
 470struct sock;
 471#line 446
 472struct kobject;
 473#line 446
 474struct kobject;
 475#line 447
 476enum kobj_ns_type {
 477    KOBJ_NS_TYPE_NONE = 0,
 478    KOBJ_NS_TYPE_NET = 1,
 479    KOBJ_NS_TYPES = 2
 480} ;
 481#line 453 "include/linux/elf.h"
 482struct kobj_ns_type_operations {
 483   enum kobj_ns_type type ;
 484   void *(*grab_current_ns)(void) ;
 485   void const   *(*netlink_ns)(struct sock * ) ;
 486   void const   *(*initial_ns)(void) ;
 487   void (*drop_ns)(void * ) ;
 488};
 489#line 57 "include/linux/kobject_ns.h"
 490struct attribute {
 491   char const   *name ;
 492   umode_t mode ;
 493   struct lock_class_key *key ;
 494   struct lock_class_key skey ;
 495};
 496#line 33 "include/linux/sysfs.h"
 497struct attribute_group {
 498   char const   *name ;
 499   umode_t (*is_visible)(struct kobject * , struct attribute * , int  ) ;
 500   struct attribute **attrs ;
 501};
 502#line 62 "include/linux/sysfs.h"
 503struct bin_attribute {
 504   struct attribute attr ;
 505   size_t size ;
 506   void *private ;
 507   ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 508                   loff_t  , size_t  ) ;
 509   ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 510                    loff_t  , size_t  ) ;
 511   int (*mmap)(struct file * , struct kobject * , struct bin_attribute * , struct vm_area_struct * ) ;
 512};
 513#line 98 "include/linux/sysfs.h"
 514struct sysfs_ops {
 515   ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
 516   ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
 517   void const   *(*namespace)(struct kobject * , struct attribute  const  * ) ;
 518};
 519#line 117
 520struct sysfs_dirent;
 521#line 117
 522struct sysfs_dirent;
 523#line 182 "include/linux/sysfs.h"
 524struct kref {
 525   atomic_t refcount ;
 526};
 527#line 49 "include/linux/kobject.h"
 528struct kset;
 529#line 49
 530struct kobj_type;
 531#line 49 "include/linux/kobject.h"
 532struct kobject {
 533   char const   *name ;
 534   struct list_head entry ;
 535   struct kobject *parent ;
 536   struct kset *kset ;
 537   struct kobj_type *ktype ;
 538   struct sysfs_dirent *sd ;
 539   struct kref kref ;
 540   unsigned char state_initialized : 1 ;
 541   unsigned char state_in_sysfs : 1 ;
 542   unsigned char state_add_uevent_sent : 1 ;
 543   unsigned char state_remove_uevent_sent : 1 ;
 544   unsigned char uevent_suppress : 1 ;
 545};
 546#line 107 "include/linux/kobject.h"
 547struct kobj_type {
 548   void (*release)(struct kobject * ) ;
 549   struct sysfs_ops  const  *sysfs_ops ;
 550   struct attribute **default_attrs ;
 551   struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject * ) ;
 552   void const   *(*namespace)(struct kobject * ) ;
 553};
 554#line 115 "include/linux/kobject.h"
 555struct kobj_uevent_env {
 556   char *envp[32U] ;
 557   int envp_idx ;
 558   char buf[2048U] ;
 559   int buflen ;
 560};
 561#line 122 "include/linux/kobject.h"
 562struct kset_uevent_ops {
 563   int (* const  filter)(struct kset * , struct kobject * ) ;
 564   char const   *(* const  name)(struct kset * , struct kobject * ) ;
 565   int (* const  uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
 566};
 567#line 139 "include/linux/kobject.h"
 568struct kset {
 569   struct list_head list ;
 570   spinlock_t list_lock ;
 571   struct kobject kobj ;
 572   struct kset_uevent_ops  const  *uevent_ops ;
 573};
 574#line 215
 575struct kernel_param;
 576#line 215
 577struct kernel_param;
 578#line 216 "include/linux/kobject.h"
 579struct kernel_param_ops {
 580   int (*set)(char const   * , struct kernel_param  const  * ) ;
 581   int (*get)(char * , struct kernel_param  const  * ) ;
 582   void (*free)(void * ) ;
 583};
 584#line 49 "include/linux/moduleparam.h"
 585struct kparam_string;
 586#line 49
 587struct kparam_array;
 588#line 49 "include/linux/moduleparam.h"
 589union __anonunion_ldv_13363_134 {
 590   void *arg ;
 591   struct kparam_string  const  *str ;
 592   struct kparam_array  const  *arr ;
 593};
 594#line 49 "include/linux/moduleparam.h"
 595struct kernel_param {
 596   char const   *name ;
 597   struct kernel_param_ops  const  *ops ;
 598   u16 perm ;
 599   s16 level ;
 600   union __anonunion_ldv_13363_134 ldv_13363 ;
 601};
 602#line 61 "include/linux/moduleparam.h"
 603struct kparam_string {
 604   unsigned int maxlen ;
 605   char *string ;
 606};
 607#line 67 "include/linux/moduleparam.h"
 608struct kparam_array {
 609   unsigned int max ;
 610   unsigned int elemsize ;
 611   unsigned int *num ;
 612   struct kernel_param_ops  const  *ops ;
 613   void *elem ;
 614};
 615#line 458 "include/linux/moduleparam.h"
 616struct static_key {
 617   atomic_t enabled ;
 618};
 619#line 225 "include/linux/jump_label.h"
 620struct tracepoint;
 621#line 225
 622struct tracepoint;
 623#line 226 "include/linux/jump_label.h"
 624struct tracepoint_func {
 625   void *func ;
 626   void *data ;
 627};
 628#line 29 "include/linux/tracepoint.h"
 629struct tracepoint {
 630   char const   *name ;
 631   struct static_key key ;
 632   void (*regfunc)(void) ;
 633   void (*unregfunc)(void) ;
 634   struct tracepoint_func *funcs ;
 635};
 636#line 86 "include/linux/tracepoint.h"
 637struct kernel_symbol {
 638   unsigned long value ;
 639   char const   *name ;
 640};
 641#line 27 "include/linux/export.h"
 642struct mod_arch_specific {
 643
 644};
 645#line 34 "include/linux/module.h"
 646struct module_param_attrs;
 647#line 34 "include/linux/module.h"
 648struct module_kobject {
 649   struct kobject kobj ;
 650   struct module *mod ;
 651   struct kobject *drivers_dir ;
 652   struct module_param_attrs *mp ;
 653};
 654#line 43 "include/linux/module.h"
 655struct module_attribute {
 656   struct attribute attr ;
 657   ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
 658   ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const   * ,
 659                    size_t  ) ;
 660   void (*setup)(struct module * , char const   * ) ;
 661   int (*test)(struct module * ) ;
 662   void (*free)(struct module * ) ;
 663};
 664#line 69
 665struct exception_table_entry;
 666#line 69
 667struct exception_table_entry;
 668#line 198
 669enum module_state {
 670    MODULE_STATE_LIVE = 0,
 671    MODULE_STATE_COMING = 1,
 672    MODULE_STATE_GOING = 2
 673} ;
 674#line 204 "include/linux/module.h"
 675struct module_ref {
 676   unsigned long incs ;
 677   unsigned long decs ;
 678};
 679#line 219
 680struct module_sect_attrs;
 681#line 219
 682struct module_notes_attrs;
 683#line 219
 684struct ftrace_event_call;
 685#line 219 "include/linux/module.h"
 686struct module {
 687   enum module_state state ;
 688   struct list_head list ;
 689   char name[56U] ;
 690   struct module_kobject mkobj ;
 691   struct module_attribute *modinfo_attrs ;
 692   char const   *version ;
 693   char const   *srcversion ;
 694   struct kobject *holders_dir ;
 695   struct kernel_symbol  const  *syms ;
 696   unsigned long const   *crcs ;
 697   unsigned int num_syms ;
 698   struct kernel_param *kp ;
 699   unsigned int num_kp ;
 700   unsigned int num_gpl_syms ;
 701   struct kernel_symbol  const  *gpl_syms ;
 702   unsigned long const   *gpl_crcs ;
 703   struct kernel_symbol  const  *unused_syms ;
 704   unsigned long const   *unused_crcs ;
 705   unsigned int num_unused_syms ;
 706   unsigned int num_unused_gpl_syms ;
 707   struct kernel_symbol  const  *unused_gpl_syms ;
 708   unsigned long const   *unused_gpl_crcs ;
 709   struct kernel_symbol  const  *gpl_future_syms ;
 710   unsigned long const   *gpl_future_crcs ;
 711   unsigned int num_gpl_future_syms ;
 712   unsigned int num_exentries ;
 713   struct exception_table_entry *extable ;
 714   int (*init)(void) ;
 715   void *module_init ;
 716   void *module_core ;
 717   unsigned int init_size ;
 718   unsigned int core_size ;
 719   unsigned int init_text_size ;
 720   unsigned int core_text_size ;
 721   unsigned int init_ro_size ;
 722   unsigned int core_ro_size ;
 723   struct mod_arch_specific arch ;
 724   unsigned int taints ;
 725   unsigned int num_bugs ;
 726   struct list_head bug_list ;
 727   struct bug_entry *bug_table ;
 728   Elf64_Sym *symtab ;
 729   Elf64_Sym *core_symtab ;
 730   unsigned int num_symtab ;
 731   unsigned int core_num_syms ;
 732   char *strtab ;
 733   char *core_strtab ;
 734   struct module_sect_attrs *sect_attrs ;
 735   struct module_notes_attrs *notes_attrs ;
 736   char *args ;
 737   void *percpu ;
 738   unsigned int percpu_size ;
 739   unsigned int num_tracepoints ;
 740   struct tracepoint * const  *tracepoints_ptrs ;
 741   unsigned int num_trace_bprintk_fmt ;
 742   char const   **trace_bprintk_fmt_start ;
 743   struct ftrace_event_call **trace_events ;
 744   unsigned int num_trace_events ;
 745   struct list_head source_list ;
 746   struct list_head target_list ;
 747   struct task_struct *waiter ;
 748   void (*exit)(void) ;
 749   struct module_ref *refptr ;
 750   ctor_fn_t (**ctors)(void) ;
 751   unsigned int num_ctors ;
 752};
 753#line 88 "include/linux/kmemleak.h"
 754struct kmem_cache_cpu {
 755   void **freelist ;
 756   unsigned long tid ;
 757   struct page *page ;
 758   struct page *partial ;
 759   int node ;
 760   unsigned int stat[26U] ;
 761};
 762#line 55 "include/linux/slub_def.h"
 763struct kmem_cache_node {
 764   spinlock_t list_lock ;
 765   unsigned long nr_partial ;
 766   struct list_head partial ;
 767   atomic_long_t nr_slabs ;
 768   atomic_long_t total_objects ;
 769   struct list_head full ;
 770};
 771#line 66 "include/linux/slub_def.h"
 772struct kmem_cache_order_objects {
 773   unsigned long x ;
 774};
 775#line 76 "include/linux/slub_def.h"
 776struct kmem_cache {
 777   struct kmem_cache_cpu *cpu_slab ;
 778   unsigned long flags ;
 779   unsigned long min_partial ;
 780   int size ;
 781   int objsize ;
 782   int offset ;
 783   int cpu_partial ;
 784   struct kmem_cache_order_objects oo ;
 785   struct kmem_cache_order_objects max ;
 786   struct kmem_cache_order_objects min ;
 787   gfp_t allocflags ;
 788   int refcount ;
 789   void (*ctor)(void * ) ;
 790   int inuse ;
 791   int align ;
 792   int reserved ;
 793   char const   *name ;
 794   struct list_head list ;
 795   struct kobject kobj ;
 796   int remote_node_defrag_ratio ;
 797   struct kmem_cache_node *node[1024U] ;
 798};
 799#line 15 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5494/dscv_tempdir/dscv/ri/43_1a/drivers/staging/iio/kfifo_buf.c.p"
 800struct klist_node;
 801#line 15
 802struct klist_node;
 803#line 37 "include/linux/klist.h"
 804struct klist_node {
 805   void *n_klist ;
 806   struct list_head n_node ;
 807   struct kref n_ref ;
 808};
 809#line 67
 810struct dma_map_ops;
 811#line 67 "include/linux/klist.h"
 812struct dev_archdata {
 813   void *acpi_handle ;
 814   struct dma_map_ops *dma_ops ;
 815   void *iommu ;
 816};
 817#line 17 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 818struct device_private;
 819#line 17
 820struct device_private;
 821#line 18
 822struct device_driver;
 823#line 18
 824struct device_driver;
 825#line 19
 826struct driver_private;
 827#line 19
 828struct driver_private;
 829#line 20
 830struct class;
 831#line 20
 832struct class;
 833#line 21
 834struct subsys_private;
 835#line 21
 836struct subsys_private;
 837#line 22
 838struct bus_type;
 839#line 22
 840struct bus_type;
 841#line 23
 842struct device_node;
 843#line 23
 844struct device_node;
 845#line 24
 846struct iommu_ops;
 847#line 24
 848struct iommu_ops;
 849#line 25 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 850struct bus_attribute {
 851   struct attribute attr ;
 852   ssize_t (*show)(struct bus_type * , char * ) ;
 853   ssize_t (*store)(struct bus_type * , char const   * , size_t  ) ;
 854};
 855#line 51 "include/linux/device.h"
 856struct device_attribute;
 857#line 51
 858struct driver_attribute;
 859#line 51 "include/linux/device.h"
 860struct bus_type {
 861   char const   *name ;
 862   char const   *dev_name ;
 863   struct device *dev_root ;
 864   struct bus_attribute *bus_attrs ;
 865   struct device_attribute *dev_attrs ;
 866   struct driver_attribute *drv_attrs ;
 867   int (*match)(struct device * , struct device_driver * ) ;
 868   int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
 869   int (*probe)(struct device * ) ;
 870   int (*remove)(struct device * ) ;
 871   void (*shutdown)(struct device * ) ;
 872   int (*suspend)(struct device * , pm_message_t  ) ;
 873   int (*resume)(struct device * ) ;
 874   struct dev_pm_ops  const  *pm ;
 875   struct iommu_ops *iommu_ops ;
 876   struct subsys_private *p ;
 877};
 878#line 125
 879struct device_type;
 880#line 182
 881struct of_device_id;
 882#line 182 "include/linux/device.h"
 883struct device_driver {
 884   char const   *name ;
 885   struct bus_type *bus ;
 886   struct module *owner ;
 887   char const   *mod_name ;
 888   bool suppress_bind_attrs ;
 889   struct of_device_id  const  *of_match_table ;
 890   int (*probe)(struct device * ) ;
 891   int (*remove)(struct device * ) ;
 892   void (*shutdown)(struct device * ) ;
 893   int (*suspend)(struct device * , pm_message_t  ) ;
 894   int (*resume)(struct device * ) ;
 895   struct attribute_group  const  **groups ;
 896   struct dev_pm_ops  const  *pm ;
 897   struct driver_private *p ;
 898};
 899#line 245 "include/linux/device.h"
 900struct driver_attribute {
 901   struct attribute attr ;
 902   ssize_t (*show)(struct device_driver * , char * ) ;
 903   ssize_t (*store)(struct device_driver * , char const   * , size_t  ) ;
 904};
 905#line 299
 906struct class_attribute;
 907#line 299 "include/linux/device.h"
 908struct class {
 909   char const   *name ;
 910   struct module *owner ;
 911   struct class_attribute *class_attrs ;
 912   struct device_attribute *dev_attrs ;
 913   struct bin_attribute *dev_bin_attrs ;
 914   struct kobject *dev_kobj ;
 915   int (*dev_uevent)(struct device * , struct kobj_uevent_env * ) ;
 916   char *(*devnode)(struct device * , umode_t * ) ;
 917   void (*class_release)(struct class * ) ;
 918   void (*dev_release)(struct device * ) ;
 919   int (*suspend)(struct device * , pm_message_t  ) ;
 920   int (*resume)(struct device * ) ;
 921   struct kobj_ns_type_operations  const  *ns_type ;
 922   void const   *(*namespace)(struct device * ) ;
 923   struct dev_pm_ops  const  *pm ;
 924   struct subsys_private *p ;
 925};
 926#line 394 "include/linux/device.h"
 927struct class_attribute {
 928   struct attribute attr ;
 929   ssize_t (*show)(struct class * , struct class_attribute * , char * ) ;
 930   ssize_t (*store)(struct class * , struct class_attribute * , char const   * , size_t  ) ;
 931   void const   *(*namespace)(struct class * , struct class_attribute  const  * ) ;
 932};
 933#line 447 "include/linux/device.h"
 934struct device_type {
 935   char const   *name ;
 936   struct attribute_group  const  **groups ;
 937   int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
 938   char *(*devnode)(struct device * , umode_t * ) ;
 939   void (*release)(struct device * ) ;
 940   struct dev_pm_ops  const  *pm ;
 941};
 942#line 474 "include/linux/device.h"
 943struct device_attribute {
 944   struct attribute attr ;
 945   ssize_t (*show)(struct device * , struct device_attribute * , char * ) ;
 946   ssize_t (*store)(struct device * , struct device_attribute * , char const   * ,
 947                    size_t  ) ;
 948};
 949#line 557 "include/linux/device.h"
 950struct device_dma_parameters {
 951   unsigned int max_segment_size ;
 952   unsigned long segment_boundary_mask ;
 953};
 954#line 567
 955struct dma_coherent_mem;
 956#line 567 "include/linux/device.h"
 957struct device {
 958   struct device *parent ;
 959   struct device_private *p ;
 960   struct kobject kobj ;
 961   char const   *init_name ;
 962   struct device_type  const  *type ;
 963   struct mutex mutex ;
 964   struct bus_type *bus ;
 965   struct device_driver *driver ;
 966   void *platform_data ;
 967   struct dev_pm_info power ;
 968   struct dev_pm_domain *pm_domain ;
 969   int numa_node ;
 970   u64 *dma_mask ;
 971   u64 coherent_dma_mask ;
 972   struct device_dma_parameters *dma_parms ;
 973   struct list_head dma_pools ;
 974   struct dma_coherent_mem *dma_mem ;
 975   struct dev_archdata archdata ;
 976   struct device_node *of_node ;
 977   dev_t devt ;
 978   u32 id ;
 979   spinlock_t devres_lock ;
 980   struct list_head devres_head ;
 981   struct klist_node knode_class ;
 982   struct class *class ;
 983   struct attribute_group  const  **groups ;
 984   void (*release)(struct device * ) ;
 985};
 986#line 681 "include/linux/device.h"
 987struct wakeup_source {
 988   char const   *name ;
 989   struct list_head entry ;
 990   spinlock_t lock ;
 991   struct timer_list timer ;
 992   unsigned long timer_expires ;
 993   ktime_t total_time ;
 994   ktime_t max_time ;
 995   ktime_t last_time ;
 996   unsigned long event_count ;
 997   unsigned long active_count ;
 998   unsigned long relax_count ;
 999   unsigned long hit_count ;
1000   unsigned char active : 1 ;
1001};
1002#line 991
1003struct prio_tree_node;
1004#line 991 "include/linux/device.h"
1005struct raw_prio_tree_node {
1006   struct prio_tree_node *left ;
1007   struct prio_tree_node *right ;
1008   struct prio_tree_node *parent ;
1009};
1010#line 19 "include/linux/prio_tree.h"
1011struct prio_tree_node {
1012   struct prio_tree_node *left ;
1013   struct prio_tree_node *right ;
1014   struct prio_tree_node *parent ;
1015   unsigned long start ;
1016   unsigned long last ;
1017};
1018#line 116
1019struct address_space;
1020#line 116
1021struct address_space;
1022#line 117 "include/linux/prio_tree.h"
1023union __anonunion_ldv_14974_136 {
1024   unsigned long index ;
1025   void *freelist ;
1026};
1027#line 117 "include/linux/prio_tree.h"
1028struct __anonstruct_ldv_14984_140 {
1029   unsigned short inuse ;
1030   unsigned short objects : 15 ;
1031   unsigned char frozen : 1 ;
1032};
1033#line 117 "include/linux/prio_tree.h"
1034union __anonunion_ldv_14985_139 {
1035   atomic_t _mapcount ;
1036   struct __anonstruct_ldv_14984_140 ldv_14984 ;
1037};
1038#line 117 "include/linux/prio_tree.h"
1039struct __anonstruct_ldv_14987_138 {
1040   union __anonunion_ldv_14985_139 ldv_14985 ;
1041   atomic_t _count ;
1042};
1043#line 117 "include/linux/prio_tree.h"
1044union __anonunion_ldv_14988_137 {
1045   unsigned long counters ;
1046   struct __anonstruct_ldv_14987_138 ldv_14987 ;
1047};
1048#line 117 "include/linux/prio_tree.h"
1049struct __anonstruct_ldv_14989_135 {
1050   union __anonunion_ldv_14974_136 ldv_14974 ;
1051   union __anonunion_ldv_14988_137 ldv_14988 ;
1052};
1053#line 117 "include/linux/prio_tree.h"
1054struct __anonstruct_ldv_14996_142 {
1055   struct page *next ;
1056   int pages ;
1057   int pobjects ;
1058};
1059#line 117 "include/linux/prio_tree.h"
1060union __anonunion_ldv_14997_141 {
1061   struct list_head lru ;
1062   struct __anonstruct_ldv_14996_142 ldv_14996 ;
1063};
1064#line 117 "include/linux/prio_tree.h"
1065union __anonunion_ldv_15002_143 {
1066   unsigned long private ;
1067   struct kmem_cache *slab ;
1068   struct page *first_page ;
1069};
1070#line 117 "include/linux/prio_tree.h"
1071struct page {
1072   unsigned long flags ;
1073   struct address_space *mapping ;
1074   struct __anonstruct_ldv_14989_135 ldv_14989 ;
1075   union __anonunion_ldv_14997_141 ldv_14997 ;
1076   union __anonunion_ldv_15002_143 ldv_15002 ;
1077   unsigned long debug_flags ;
1078};
1079#line 192 "include/linux/mm_types.h"
1080struct __anonstruct_vm_set_145 {
1081   struct list_head list ;
1082   void *parent ;
1083   struct vm_area_struct *head ;
1084};
1085#line 192 "include/linux/mm_types.h"
1086union __anonunion_shared_144 {
1087   struct __anonstruct_vm_set_145 vm_set ;
1088   struct raw_prio_tree_node prio_tree_node ;
1089};
1090#line 192
1091struct anon_vma;
1092#line 192
1093struct vm_operations_struct;
1094#line 192
1095struct mempolicy;
1096#line 192 "include/linux/mm_types.h"
1097struct vm_area_struct {
1098   struct mm_struct *vm_mm ;
1099   unsigned long vm_start ;
1100   unsigned long vm_end ;
1101   struct vm_area_struct *vm_next ;
1102   struct vm_area_struct *vm_prev ;
1103   pgprot_t vm_page_prot ;
1104   unsigned long vm_flags ;
1105   struct rb_node vm_rb ;
1106   union __anonunion_shared_144 shared ;
1107   struct list_head anon_vma_chain ;
1108   struct anon_vma *anon_vma ;
1109   struct vm_operations_struct  const  *vm_ops ;
1110   unsigned long vm_pgoff ;
1111   struct file *vm_file ;
1112   void *vm_private_data ;
1113   struct mempolicy *vm_policy ;
1114};
1115#line 255 "include/linux/mm_types.h"
1116struct core_thread {
1117   struct task_struct *task ;
1118   struct core_thread *next ;
1119};
1120#line 261 "include/linux/mm_types.h"
1121struct core_state {
1122   atomic_t nr_threads ;
1123   struct core_thread dumper ;
1124   struct completion startup ;
1125};
1126#line 274 "include/linux/mm_types.h"
1127struct mm_rss_stat {
1128   atomic_long_t count[3U] ;
1129};
1130#line 287
1131struct linux_binfmt;
1132#line 287
1133struct mmu_notifier_mm;
1134#line 287 "include/linux/mm_types.h"
1135struct mm_struct {
1136   struct vm_area_struct *mmap ;
1137   struct rb_root mm_rb ;
1138   struct vm_area_struct *mmap_cache ;
1139   unsigned long (*get_unmapped_area)(struct file * , unsigned long  , unsigned long  ,
1140                                      unsigned long  , unsigned long  ) ;
1141   void (*unmap_area)(struct mm_struct * , unsigned long  ) ;
1142   unsigned long mmap_base ;
1143   unsigned long task_size ;
1144   unsigned long cached_hole_size ;
1145   unsigned long free_area_cache ;
1146   pgd_t *pgd ;
1147   atomic_t mm_users ;
1148   atomic_t mm_count ;
1149   int map_count ;
1150   spinlock_t page_table_lock ;
1151   struct rw_semaphore mmap_sem ;
1152   struct list_head mmlist ;
1153   unsigned long hiwater_rss ;
1154   unsigned long hiwater_vm ;
1155   unsigned long total_vm ;
1156   unsigned long locked_vm ;
1157   unsigned long pinned_vm ;
1158   unsigned long shared_vm ;
1159   unsigned long exec_vm ;
1160   unsigned long stack_vm ;
1161   unsigned long reserved_vm ;
1162   unsigned long def_flags ;
1163   unsigned long nr_ptes ;
1164   unsigned long start_code ;
1165   unsigned long end_code ;
1166   unsigned long start_data ;
1167   unsigned long end_data ;
1168   unsigned long start_brk ;
1169   unsigned long brk ;
1170   unsigned long start_stack ;
1171   unsigned long arg_start ;
1172   unsigned long arg_end ;
1173   unsigned long env_start ;
1174   unsigned long env_end ;
1175   unsigned long saved_auxv[44U] ;
1176   struct mm_rss_stat rss_stat ;
1177   struct linux_binfmt *binfmt ;
1178   cpumask_var_t cpu_vm_mask_var ;
1179   mm_context_t context ;
1180   unsigned int faultstamp ;
1181   unsigned int token_priority ;
1182   unsigned int last_interval ;
1183   unsigned long flags ;
1184   struct core_state *core_state ;
1185   spinlock_t ioctx_lock ;
1186   struct hlist_head ioctx_list ;
1187   struct task_struct *owner ;
1188   struct file *exe_file ;
1189   unsigned long num_exe_file_vmas ;
1190   struct mmu_notifier_mm *mmu_notifier_mm ;
1191   pgtable_t pmd_huge_pte ;
1192   struct cpumask cpumask_allocation ;
1193};
1194#line 178 "include/linux/mm.h"
1195struct vm_fault {
1196   unsigned int flags ;
1197   unsigned long pgoff ;
1198   void *virtual_address ;
1199   struct page *page ;
1200};
1201#line 195 "include/linux/mm.h"
1202struct vm_operations_struct {
1203   void (*open)(struct vm_area_struct * ) ;
1204   void (*close)(struct vm_area_struct * ) ;
1205   int (*fault)(struct vm_area_struct * , struct vm_fault * ) ;
1206   int (*page_mkwrite)(struct vm_area_struct * , struct vm_fault * ) ;
1207   int (*access)(struct vm_area_struct * , unsigned long  , void * , int  , int  ) ;
1208   int (*set_policy)(struct vm_area_struct * , struct mempolicy * ) ;
1209   struct mempolicy *(*get_policy)(struct vm_area_struct * , unsigned long  ) ;
1210   int (*migrate)(struct vm_area_struct * , nodemask_t const   * , nodemask_t const   * ,
1211                  unsigned long  ) ;
1212};
1213#line 268 "include/linux/scatterlist.h"
1214struct __kfifo {
1215   unsigned int in ;
1216   unsigned int out ;
1217   unsigned int mask ;
1218   unsigned int esize ;
1219   void *data ;
1220};
1221#line 65 "include/linux/kfifo.h"
1222union __anonunion_ldv_17663_146 {
1223   struct __kfifo kfifo ;
1224   unsigned char *type ;
1225   char (*rectype)[0U] ;
1226   void *ptr ;
1227   void const   *ptr_const ;
1228};
1229#line 65 "include/linux/kfifo.h"
1230struct kfifo {
1231   union __anonunion_ldv_17663_146 ldv_17663 ;
1232   unsigned char buf[0U] ;
1233};
1234#line 89 "include/linux/kdev_t.h"
1235struct file_operations;
1236#line 89
1237struct file_operations;
1238#line 90 "include/linux/kdev_t.h"
1239struct cdev {
1240   struct kobject kobj ;
1241   struct module *owner ;
1242   struct file_operations  const  *ops ;
1243   struct list_head list ;
1244   dev_t dev ;
1245   unsigned int count ;
1246};
1247#line 34 "include/linux/cdev.h"
1248enum iio_chan_type {
1249    IIO_VOLTAGE = 0,
1250    IIO_CURRENT = 1,
1251    IIO_POWER = 2,
1252    IIO_ACCEL = 3,
1253    IIO_ANGL_VEL = 4,
1254    IIO_MAGN = 5,
1255    IIO_LIGHT = 6,
1256    IIO_INTENSITY = 7,
1257    IIO_PROXIMITY = 8,
1258    IIO_TEMP = 9,
1259    IIO_INCLI = 10,
1260    IIO_ROT = 11,
1261    IIO_ANGL = 12,
1262    IIO_TIMESTAMP = 13,
1263    IIO_CAPACITANCE = 14
1264} ;
1265#line 86
1266enum iio_endian {
1267    IIO_CPU = 0,
1268    IIO_BE = 1,
1269    IIO_LE = 2
1270} ;
1271#line 92
1272struct iio_chan_spec;
1273#line 92
1274struct iio_chan_spec;
1275#line 93
1276struct iio_dev;
1277#line 93
1278struct iio_dev;
1279#line 94 "include/linux/cdev.h"
1280struct iio_chan_spec_ext_info {
1281   char const   *name ;
1282   bool shared ;
1283   ssize_t (*read)(struct iio_dev * , struct iio_chan_spec  const  * , char * ) ;
1284   ssize_t (*write)(struct iio_dev * , struct iio_chan_spec  const  * , char const   * ,
1285                    size_t  ) ;
1286};
1287#line 108 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/iio/iio.h"
1288struct __anonstruct_scan_type_149 {
1289   char sign ;
1290   u8 realbits ;
1291   u8 storagebits ;
1292   u8 shift ;
1293   enum iio_endian endianness ;
1294};
1295#line 108 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/iio/iio.h"
1296struct iio_chan_spec {
1297   enum iio_chan_type type ;
1298   int channel ;
1299   int channel2 ;
1300   unsigned long address ;
1301   int scan_index ;
1302   struct __anonstruct_scan_type_149 scan_type ;
1303   long info_mask ;
1304   long event_mask ;
1305   struct iio_chan_spec_ext_info  const  *ext_info ;
1306   char *extend_name ;
1307   char const   *datasheet_name ;
1308   unsigned char processed_val : 1 ;
1309   unsigned char modified : 1 ;
1310   unsigned char indexed : 1 ;
1311   unsigned char output : 1 ;
1312   unsigned char differential : 1 ;
1313};
1314#line 214
1315struct iio_trigger;
1316#line 214
1317struct iio_trigger;
1318#line 215 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/iio/iio.h"
1319struct iio_info {
1320   struct module *driver_module ;
1321   struct attribute_group *event_attrs ;
1322   struct attribute_group  const  *attrs ;
1323   int (*read_raw)(struct iio_dev * , struct iio_chan_spec  const  * , int * , int * ,
1324                   long  ) ;
1325   int (*write_raw)(struct iio_dev * , struct iio_chan_spec  const  * , int  , int  ,
1326                    long  ) ;
1327   int (*write_raw_get_fmt)(struct iio_dev * , struct iio_chan_spec  const  * , long  ) ;
1328   int (*read_event_config)(struct iio_dev * , u64  ) ;
1329   int (*write_event_config)(struct iio_dev * , u64  , int  ) ;
1330   int (*read_event_value)(struct iio_dev * , u64  , int * ) ;
1331   int (*write_event_value)(struct iio_dev * , u64  , int  ) ;
1332   int (*validate_trigger)(struct iio_dev * , struct iio_trigger * ) ;
1333   int (*update_scan_mode)(struct iio_dev * , unsigned long const   * ) ;
1334   int (*debugfs_reg_access)(struct iio_dev * , unsigned int  , unsigned int  , unsigned int * ) ;
1335};
1336#line 291 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/iio/iio.h"
1337struct iio_buffer_setup_ops {
1338   int (*preenable)(struct iio_dev * ) ;
1339   int (*postenable)(struct iio_dev * ) ;
1340   int (*predisable)(struct iio_dev * ) ;
1341   int (*postdisable)(struct iio_dev * ) ;
1342};
1343#line 308
1344struct iio_event_interface;
1345#line 308
1346struct iio_buffer;
1347#line 308
1348struct iio_poll_func;
1349#line 308
1350struct dentry;
1351#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/iio/iio.h"
1352struct iio_dev {
1353   int id ;
1354   int modes ;
1355   int currentmode ;
1356   struct device dev ;
1357   struct iio_event_interface *event_interface ;
1358   struct iio_buffer *buffer ;
1359   struct mutex mlock ;
1360   unsigned long const   *available_scan_masks ;
1361   unsigned int masklength ;
1362   unsigned long const   *active_scan_mask ;
1363   struct iio_trigger *trig ;
1364   struct iio_poll_func *pollfunc ;
1365   struct iio_chan_spec  const  *channels ;
1366   int num_channels ;
1367   struct list_head channel_attr_list ;
1368   struct attribute_group chan_attr_group ;
1369   char const   *name ;
1370   struct iio_info  const  *info ;
1371   struct mutex info_exist_lock ;
1372   struct iio_buffer_setup_ops  const  *setup_ops ;
1373   struct cdev chrdev ;
1374   struct attribute_group  const  *groups[7U] ;
1375   int groupcounter ;
1376   unsigned long flags ;
1377   struct dentry *debugfs_dentry ;
1378   unsigned int cached_reg_addr ;
1379};
1380#line 464 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/iio/iio.h"
1381struct iio_buffer_access_funcs {
1382   int (*store_to)(struct iio_buffer * , u8 * , s64  ) ;
1383   int (*read_first_n)(struct iio_buffer * , size_t  , char * ) ;
1384   int (*request_update)(struct iio_buffer * ) ;
1385   int (*get_bytes_per_datum)(struct iio_buffer * ) ;
1386   int (*set_bytes_per_datum)(struct iio_buffer * , size_t  ) ;
1387   int (*get_length)(struct iio_buffer * ) ;
1388   int (*set_length)(struct iio_buffer * , int  ) ;
1389};
1390#line 51 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/iio/buffer.h"
1391struct iio_buffer {
1392   int length ;
1393   int bytes_per_datum ;
1394   struct attribute_group *scan_el_attrs ;
1395   long *scan_mask ;
1396   bool scan_timestamp ;
1397   unsigned int scan_index_timestamp ;
1398   struct iio_buffer_access_funcs  const  *access ;
1399   struct list_head scan_el_dev_attr_list ;
1400   struct attribute_group scan_el_group ;
1401   wait_queue_head_t pollq ;
1402   bool stufftoread ;
1403   struct attribute_group  const  *attrs ;
1404   struct list_head demux_list ;
1405   unsigned char *demux_bounce ;
1406};
1407#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/iio/kfifo_buf.h"
1408struct iio_kfifo {
1409   struct iio_buffer buffer ;
1410   struct kfifo kf ;
1411   int update_needed ;
1412};
1413#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5494/dscv_tempdir/dscv/ri/43_1a/drivers/staging/iio/kfifo_buf.c.p"
1414void ldv_spin_lock(void) ;
1415#line 3
1416void ldv_spin_unlock(void) ;
1417#line 4
1418int ldv_spin_trylock(void) ;
1419#line 161 "include/linux/slab.h"
1420extern void kfree(void const   * ) ;
1421#line 220 "include/linux/slub_def.h"
1422extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t  ) ;
1423#line 223
1424void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
1425#line 353 "include/linux/slab.h"
1426__inline static void *kzalloc(size_t size , gfp_t flags ) ;
1427#line 10 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5494/dscv_tempdir/dscv/ri/43_1a/drivers/staging/iio/kfifo_buf.c.p"
1428extern void *__VERIFIER_nondet_pointer(void) ;
1429#line 11
1430void ldv_check_alloc_flags(gfp_t flags ) ;
1431#line 12
1432void ldv_check_alloc_nonatomic(void) ;
1433#line 14
1434struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
1435#line 175 "include/linux/kfifo.h"
1436__inline static unsigned int __kfifo_uint_must_check_helper(unsigned int val ) 
1437{ 
1438
1439  {
1440#line 177
1441  return (val);
1442}
1443}
1444#line 181 "include/linux/kfifo.h"
1445__inline static int __kfifo_int_must_check_helper(int val ) 
1446{ 
1447
1448  {
1449#line 183
1450  return (val);
1451}
1452}
1453#line 790
1454extern int __kfifo_alloc(struct __kfifo * , unsigned int  , size_t  , gfp_t  ) ;
1455#line 793
1456extern void __kfifo_free(struct __kfifo * ) ;
1457#line 798
1458extern unsigned int __kfifo_in(struct __kfifo * , void const   * , unsigned int  ) ;
1459#line 807
1460extern int __kfifo_to_user(struct __kfifo * , void * , unsigned long  , unsigned int * ) ;
1461#line 819
1462extern unsigned int __kfifo_in_r(struct __kfifo * , void const   * , unsigned int  ,
1463                                 size_t  ) ;
1464#line 829
1465extern int __kfifo_to_user_r(struct __kfifo * , void * , unsigned long  , unsigned int * ,
1466                             size_t  ) ;
1467#line 92 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/iio/buffer.h"
1468extern void iio_buffer_init(struct iio_buffer * ) ;
1469#line 100 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/iio/buffer.h"
1470__inline static void __iio_update_buffer(struct iio_buffer *buffer , int bytes_per_datum ,
1471                                         int length ) 
1472{ unsigned long __cil_tmp4 ;
1473  unsigned long __cil_tmp5 ;
1474
1475  {
1476#line 103
1477  __cil_tmp4 = (unsigned long )buffer;
1478#line 103
1479  __cil_tmp5 = __cil_tmp4 + 4;
1480#line 103
1481  *((int *)__cil_tmp5) = bytes_per_datum;
1482#line 104
1483  *((int *)buffer) = length;
1484#line 105
1485  return;
1486}
1487}
1488#line 146
1489extern ssize_t iio_buffer_read_length(struct device * , struct device_attribute * ,
1490                                      char * ) ;
1491#line 152
1492extern ssize_t iio_buffer_write_length(struct device * , struct device_attribute * ,
1493                                       char const   * , size_t  ) ;
1494#line 159
1495extern ssize_t iio_buffer_store_enable(struct device * , struct device_attribute * ,
1496                                       char const   * , size_t  ) ;
1497#line 166
1498extern ssize_t iio_buffer_show_enable(struct device * , struct device_attribute * ,
1499                                      char * ) ;
1500#line 6 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/iio/kfifo_buf.h"
1501struct iio_buffer *iio_kfifo_allocate(struct iio_dev *indio_dev ) ;
1502#line 7
1503void iio_kfifo_free(struct iio_buffer *r ) ;
1504#line 34 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5494/dscv_tempdir/dscv/ri/43_1a/drivers/staging/iio/kfifo_buf.c.p"
1505__inline static int __iio_allocate_kfifo(struct iio_kfifo *buf , int bytes_per_datum ,
1506                                         int length ) 
1507{ struct kfifo *__tmp ;
1508  struct __kfifo *__kfifo ;
1509  int tmp ;
1510  int tmp___0 ;
1511  struct iio_buffer *__cil_tmp8 ;
1512  unsigned long __cil_tmp9 ;
1513  unsigned long __cil_tmp10 ;
1514  int __cil_tmp11 ;
1515  unsigned int __cil_tmp12 ;
1516
1517  {
1518#line 37
1519  if (length == 0) {
1520#line 38
1521    return (-22);
1522  } else
1523#line 37
1524  if (bytes_per_datum == 0) {
1525#line 38
1526    return (-22);
1527  } else {
1528
1529  }
1530  {
1531#line 40
1532  __cil_tmp8 = (struct iio_buffer *)buf;
1533#line 40
1534  __iio_update_buffer(__cil_tmp8, bytes_per_datum, length);
1535#line 41
1536  __cil_tmp9 = (unsigned long )buf;
1537#line 41
1538  __cil_tmp10 = __cil_tmp9 + 208;
1539#line 41
1540  __tmp = (struct kfifo *)__cil_tmp10;
1541#line 41
1542  __kfifo = (struct __kfifo *)__tmp;
1543#line 41
1544  __cil_tmp11 = bytes_per_datum * length;
1545#line 41
1546  __cil_tmp12 = (unsigned int )__cil_tmp11;
1547#line 41
1548  tmp = __kfifo_alloc(__kfifo, __cil_tmp12, 1UL, 208U);
1549#line 41
1550  tmp___0 = __kfifo_int_must_check_helper(tmp);
1551  }
1552#line 41
1553  return (tmp___0);
1554}
1555}
1556#line 44 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5494/dscv_tempdir/dscv/ri/43_1a/drivers/staging/iio/kfifo_buf.c.p"
1557static int iio_request_update_kfifo(struct iio_buffer *r ) 
1558{ int ret ;
1559  struct iio_kfifo *buf ;
1560  struct iio_buffer  const  *__mptr ;
1561  struct kfifo *__tmp ;
1562  struct __kfifo *__kfifo ;
1563  unsigned long __cil_tmp7 ;
1564  unsigned long __cil_tmp8 ;
1565  int __cil_tmp9 ;
1566  unsigned long __cil_tmp10 ;
1567  unsigned long __cil_tmp11 ;
1568  unsigned long __cil_tmp12 ;
1569  unsigned long __cil_tmp13 ;
1570  unsigned long __cil_tmp14 ;
1571  int __cil_tmp15 ;
1572  int __cil_tmp16 ;
1573
1574  {
1575#line 46
1576  ret = 0;
1577#line 47
1578  __mptr = (struct iio_buffer  const  *)r;
1579#line 47
1580  buf = (struct iio_kfifo *)__mptr;
1581  {
1582#line 49
1583  __cil_tmp7 = (unsigned long )buf;
1584#line 49
1585  __cil_tmp8 = __cil_tmp7 + 232;
1586#line 49
1587  __cil_tmp9 = *((int *)__cil_tmp8);
1588#line 49
1589  if (__cil_tmp9 == 0) {
1590#line 50
1591    goto error_ret;
1592  } else {
1593
1594  }
1595  }
1596  {
1597#line 51
1598  __cil_tmp10 = (unsigned long )buf;
1599#line 51
1600  __cil_tmp11 = __cil_tmp10 + 208;
1601#line 51
1602  __tmp = (struct kfifo *)__cil_tmp11;
1603#line 51
1604  __kfifo = (struct __kfifo *)__tmp;
1605#line 51
1606  __kfifo_free(__kfifo);
1607#line 52
1608  __cil_tmp12 = 0 + 4;
1609#line 52
1610  __cil_tmp13 = (unsigned long )buf;
1611#line 52
1612  __cil_tmp14 = __cil_tmp13 + __cil_tmp12;
1613#line 52
1614  __cil_tmp15 = *((int *)__cil_tmp14);
1615#line 52
1616  __cil_tmp16 = *((int *)buf);
1617#line 52
1618  ret = __iio_allocate_kfifo(buf, __cil_tmp15, __cil_tmp16);
1619  }
1620  error_ret: ;
1621#line 55
1622  return (ret);
1623}
1624}
1625#line 58 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5494/dscv_tempdir/dscv/ri/43_1a/drivers/staging/iio/kfifo_buf.c.p"
1626static int iio_get_length_kfifo(struct iio_buffer *r ) 
1627{ 
1628
1629  {
1630#line 60
1631  return (*((int *)r));
1632}
1633}
1634#line 63 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5494/dscv_tempdir/dscv/ri/43_1a/drivers/staging/iio/kfifo_buf.c.p"
1635static struct device_attribute dev_attr_enable  =    {{"enable", (umode_t )420U, (struct lock_class_key *)0, {{{(char)0}, {(char)0},
1636                                                             {(char)0}, {(char)0},
1637                                                             {(char)0}, {(char)0},
1638                                                             {(char)0}, {(char)0}}}},
1639    & iio_buffer_show_enable, & iio_buffer_store_enable};
1640#line 64 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5494/dscv_tempdir/dscv/ri/43_1a/drivers/staging/iio/kfifo_buf.c.p"
1641static struct device_attribute dev_attr_length  =    {{"length", (umode_t )420U, (struct lock_class_key *)0, {{{(char)0}, {(char)0},
1642                                                             {(char)0}, {(char)0},
1643                                                             {(char)0}, {(char)0},
1644                                                             {(char)0}, {(char)0}}}},
1645    & iio_buffer_read_length, & iio_buffer_write_length};
1646#line 66 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5494/dscv_tempdir/dscv/ri/43_1a/drivers/staging/iio/kfifo_buf.c.p"
1647static struct attribute *iio_kfifo_attributes[3U]  = {      & dev_attr_length.attr,      & dev_attr_enable.attr,      (struct attribute *)0};
1648#line 72 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5494/dscv_tempdir/dscv/ri/43_1a/drivers/staging/iio/kfifo_buf.c.p"
1649static struct attribute_group iio_kfifo_attribute_group  =    {"buffer", (umode_t (*)(struct kobject * , struct attribute * , int  ))0, (struct attribute **)(& iio_kfifo_attributes)};
1650#line 77 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5494/dscv_tempdir/dscv/ri/43_1a/drivers/staging/iio/kfifo_buf.c.p"
1651static int iio_get_bytes_per_datum_kfifo(struct iio_buffer *r ) 
1652{ unsigned long __cil_tmp2 ;
1653  unsigned long __cil_tmp3 ;
1654
1655  {
1656  {
1657#line 79
1658  __cil_tmp2 = (unsigned long )r;
1659#line 79
1660  __cil_tmp3 = __cil_tmp2 + 4;
1661#line 79
1662  return (*((int *)__cil_tmp3));
1663  }
1664}
1665}
1666#line 82 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5494/dscv_tempdir/dscv/ri/43_1a/drivers/staging/iio/kfifo_buf.c.p"
1667static int iio_mark_update_needed_kfifo(struct iio_buffer *r ) 
1668{ struct iio_kfifo *kf ;
1669  struct iio_buffer  const  *__mptr ;
1670  unsigned long __cil_tmp4 ;
1671  unsigned long __cil_tmp5 ;
1672
1673  {
1674#line 84
1675  __mptr = (struct iio_buffer  const  *)r;
1676#line 84
1677  kf = (struct iio_kfifo *)__mptr;
1678#line 85
1679  __cil_tmp4 = (unsigned long )kf;
1680#line 85
1681  __cil_tmp5 = __cil_tmp4 + 232;
1682#line 85
1683  *((int *)__cil_tmp5) = 1;
1684#line 86
1685  return (0);
1686}
1687}
1688#line 89 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5494/dscv_tempdir/dscv/ri/43_1a/drivers/staging/iio/kfifo_buf.c.p"
1689static int iio_set_bytes_per_datum_kfifo(struct iio_buffer *r , size_t bpd ) 
1690{ unsigned long __cil_tmp3 ;
1691  unsigned long __cil_tmp4 ;
1692  int __cil_tmp5 ;
1693  size_t __cil_tmp6 ;
1694  unsigned long __cil_tmp7 ;
1695  unsigned long __cil_tmp8 ;
1696
1697  {
1698  {
1699#line 91
1700  __cil_tmp3 = (unsigned long )r;
1701#line 91
1702  __cil_tmp4 = __cil_tmp3 + 4;
1703#line 91
1704  __cil_tmp5 = *((int *)__cil_tmp4);
1705#line 91
1706  __cil_tmp6 = (size_t )__cil_tmp5;
1707#line 91
1708  if (__cil_tmp6 != bpd) {
1709    {
1710#line 92
1711    __cil_tmp7 = (unsigned long )r;
1712#line 92
1713    __cil_tmp8 = __cil_tmp7 + 4;
1714#line 92
1715    *((int *)__cil_tmp8) = (int )bpd;
1716#line 93
1717    iio_mark_update_needed_kfifo(r);
1718    }
1719  } else {
1720
1721  }
1722  }
1723#line 95
1724  return (0);
1725}
1726}
1727#line 98 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5494/dscv_tempdir/dscv/ri/43_1a/drivers/staging/iio/kfifo_buf.c.p"
1728static int iio_set_length_kfifo(struct iio_buffer *r , int length ) 
1729{ int __cil_tmp3 ;
1730
1731  {
1732  {
1733#line 100
1734  __cil_tmp3 = *((int *)r);
1735#line 100
1736  if (__cil_tmp3 != length) {
1737    {
1738#line 101
1739    *((int *)r) = length;
1740#line 102
1741    iio_mark_update_needed_kfifo(r);
1742    }
1743  } else {
1744
1745  }
1746  }
1747#line 104
1748  return (0);
1749}
1750}
1751#line 107 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5494/dscv_tempdir/dscv/ri/43_1a/drivers/staging/iio/kfifo_buf.c.p"
1752static int iio_store_to_kfifo(struct iio_buffer *r , u8 *data , s64 timestamp ) 
1753{ int ret ;
1754  struct iio_kfifo *kf ;
1755  struct iio_buffer  const  *__mptr ;
1756  struct kfifo *__tmp ;
1757  u8 *__buf ;
1758  unsigned long __n ;
1759  size_t __recsize ;
1760  struct __kfifo *__kfifo ;
1761  unsigned int tmp ;
1762  unsigned int tmp___0 ;
1763  unsigned int tmp___1 ;
1764  unsigned long __cil_tmp16 ;
1765  unsigned long __cil_tmp17 ;
1766  unsigned long __cil_tmp18 ;
1767  unsigned long __cil_tmp19 ;
1768  int __cil_tmp20 ;
1769  void const   *__cil_tmp21 ;
1770  unsigned int __cil_tmp22 ;
1771  void const   *__cil_tmp23 ;
1772  unsigned int __cil_tmp24 ;
1773  unsigned long __cil_tmp25 ;
1774  unsigned long __cil_tmp26 ;
1775  int __cil_tmp27 ;
1776
1777  {
1778#line 112
1779  __mptr = (struct iio_buffer  const  *)r;
1780#line 112
1781  kf = (struct iio_kfifo *)__mptr;
1782#line 113
1783  __cil_tmp16 = (unsigned long )kf;
1784#line 113
1785  __cil_tmp17 = __cil_tmp16 + 208;
1786#line 113
1787  __tmp = (struct kfifo *)__cil_tmp17;
1788#line 113
1789  __buf = data;
1790#line 113
1791  __cil_tmp18 = (unsigned long )r;
1792#line 113
1793  __cil_tmp19 = __cil_tmp18 + 4;
1794#line 113
1795  __cil_tmp20 = *((int *)__cil_tmp19);
1796#line 113
1797  __n = (unsigned long )__cil_tmp20;
1798#line 113
1799  __recsize = 0UL;
1800#line 113
1801  __kfifo = (struct __kfifo *)__tmp;
1802#line 113
1803  if (__recsize != 0UL) {
1804    {
1805#line 113
1806    __cil_tmp21 = (void const   *)__buf;
1807#line 113
1808    __cil_tmp22 = (unsigned int )__n;
1809#line 113
1810    tmp = __kfifo_in_r(__kfifo, __cil_tmp21, __cil_tmp22, __recsize);
1811#line 113
1812    tmp___1 = tmp;
1813    }
1814  } else {
1815    {
1816#line 113
1817    __cil_tmp23 = (void const   *)__buf;
1818#line 113
1819    __cil_tmp24 = (unsigned int )__n;
1820#line 113
1821    tmp___0 = __kfifo_in(__kfifo, __cil_tmp23, __cil_tmp24);
1822#line 113
1823    tmp___1 = tmp___0;
1824    }
1825  }
1826#line 113
1827  ret = (int )tmp___1;
1828  {
1829#line 114
1830  __cil_tmp25 = (unsigned long )r;
1831#line 114
1832  __cil_tmp26 = __cil_tmp25 + 4;
1833#line 114
1834  __cil_tmp27 = *((int *)__cil_tmp26);
1835#line 114
1836  if (__cil_tmp27 != ret) {
1837#line 115
1838    return (-16);
1839  } else {
1840
1841  }
1842  }
1843#line 116
1844  return (0);
1845}
1846}
1847#line 119 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5494/dscv_tempdir/dscv/ri/43_1a/drivers/staging/iio/kfifo_buf.c.p"
1848static int iio_read_first_n_kfifo(struct iio_buffer *r , size_t n , char *buf ) 
1849{ int ret ;
1850  int copied ;
1851  struct iio_kfifo *kf ;
1852  struct iio_buffer  const  *__mptr ;
1853  size_t __x ;
1854  struct kfifo *__tmp ;
1855  void *__to ;
1856  unsigned int __len ;
1857  unsigned int *__copied ;
1858  size_t __recsize ;
1859  struct __kfifo *__kfifo ;
1860  int tmp ;
1861  int tmp___0 ;
1862  int tmp___1 ;
1863  unsigned int tmp___2 ;
1864  unsigned long __cil_tmp19 ;
1865  unsigned long __cil_tmp20 ;
1866  int __cil_tmp21 ;
1867  size_t __cil_tmp22 ;
1868  unsigned long __cil_tmp23 ;
1869  unsigned long __cil_tmp24 ;
1870  int __cil_tmp25 ;
1871  size_t __cil_tmp26 ;
1872  unsigned long __cil_tmp27 ;
1873  unsigned long __cil_tmp28 ;
1874  unsigned long __cil_tmp29 ;
1875  unsigned long __cil_tmp30 ;
1876  unsigned long __cil_tmp31 ;
1877  unsigned int __cil_tmp32 ;
1878  int *__cil_tmp33 ;
1879
1880  {
1881#line 123
1882  __mptr = (struct iio_buffer  const  *)r;
1883#line 123
1884  kf = (struct iio_kfifo *)__mptr;
1885  {
1886#line 125
1887  __cil_tmp19 = (unsigned long )r;
1888#line 125
1889  __cil_tmp20 = __cil_tmp19 + 4;
1890#line 125
1891  __cil_tmp21 = *((int *)__cil_tmp20);
1892#line 125
1893  __cil_tmp22 = (size_t )__cil_tmp21;
1894#line 125
1895  if (__cil_tmp22 > n) {
1896#line 126
1897    return (-22);
1898  } else {
1899
1900  }
1901  }
1902#line 128
1903  __x = n;
1904#line 128
1905  __cil_tmp23 = (unsigned long )r;
1906#line 128
1907  __cil_tmp24 = __cil_tmp23 + 4;
1908#line 128
1909  __cil_tmp25 = *((int *)__cil_tmp24);
1910#line 128
1911  __cil_tmp26 = (size_t )__cil_tmp25;
1912#line 128
1913  __cil_tmp27 = __x % __cil_tmp26;
1914#line 128
1915  n = __x - __cil_tmp27;
1916#line 129
1917  __cil_tmp28 = (unsigned long )kf;
1918#line 129
1919  __cil_tmp29 = __cil_tmp28 + 208;
1920#line 129
1921  __tmp = (struct kfifo *)__cil_tmp29;
1922#line 129
1923  __to = (void *)buf;
1924#line 129
1925  __len = (unsigned int )n;
1926#line 129
1927  __copied = (unsigned int *)(& copied);
1928#line 129
1929  __recsize = 0UL;
1930#line 129
1931  __kfifo = (struct __kfifo *)__tmp;
1932#line 129
1933  if (__recsize != 0UL) {
1934    {
1935#line 129
1936    __cil_tmp30 = (unsigned long )__len;
1937#line 129
1938    tmp = __kfifo_to_user_r(__kfifo, __to, __cil_tmp30, __copied, __recsize);
1939#line 129
1940    tmp___1 = tmp;
1941    }
1942  } else {
1943    {
1944#line 129
1945    __cil_tmp31 = (unsigned long )__len;
1946#line 129
1947    tmp___0 = __kfifo_to_user(__kfifo, __to, __cil_tmp31, __copied);
1948#line 129
1949    tmp___1 = tmp___0;
1950    }
1951  }
1952  {
1953#line 129
1954  __cil_tmp32 = (unsigned int )tmp___1;
1955#line 129
1956  tmp___2 = __kfifo_uint_must_check_helper(__cil_tmp32);
1957#line 129
1958  ret = (int )tmp___2;
1959  }
1960  {
1961#line 131
1962  __cil_tmp33 = & copied;
1963#line 131
1964  return (*__cil_tmp33);
1965  }
1966}
1967}
1968#line 134 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5494/dscv_tempdir/dscv/ri/43_1a/drivers/staging/iio/kfifo_buf.c.p"
1969static struct iio_buffer_access_funcs  const  kfifo_access_funcs  =    {& iio_store_to_kfifo, & iio_read_first_n_kfifo, & iio_request_update_kfifo, & iio_get_bytes_per_datum_kfifo,
1970    & iio_set_bytes_per_datum_kfifo, & iio_get_length_kfifo, & iio_set_length_kfifo};
1971#line 144 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5494/dscv_tempdir/dscv/ri/43_1a/drivers/staging/iio/kfifo_buf.c.p"
1972struct iio_buffer *iio_kfifo_allocate(struct iio_dev *indio_dev ) 
1973{ struct iio_kfifo *kf ;
1974  void *tmp ;
1975  struct iio_kfifo *__cil_tmp4 ;
1976  unsigned long __cil_tmp5 ;
1977  unsigned long __cil_tmp6 ;
1978  unsigned long __cil_tmp7 ;
1979  unsigned long __cil_tmp8 ;
1980  struct iio_buffer *__cil_tmp9 ;
1981  unsigned long __cil_tmp10 ;
1982  unsigned long __cil_tmp11 ;
1983  unsigned long __cil_tmp12 ;
1984  unsigned long __cil_tmp13 ;
1985  unsigned long __cil_tmp14 ;
1986  unsigned long __cil_tmp15 ;
1987
1988  {
1989  {
1990#line 148
1991  tmp = kzalloc(240UL, 208U);
1992#line 148
1993  kf = (struct iio_kfifo *)tmp;
1994  }
1995  {
1996#line 149
1997  __cil_tmp4 = (struct iio_kfifo *)0;
1998#line 149
1999  __cil_tmp5 = (unsigned long )__cil_tmp4;
2000#line 149
2001  __cil_tmp6 = (unsigned long )kf;
2002#line 149
2003  if (__cil_tmp6 == __cil_tmp5) {
2004#line 150
2005    return ((struct iio_buffer *)0);
2006  } else {
2007
2008  }
2009  }
2010  {
2011#line 151
2012  __cil_tmp7 = (unsigned long )kf;
2013#line 151
2014  __cil_tmp8 = __cil_tmp7 + 232;
2015#line 151
2016  *((int *)__cil_tmp8) = 1;
2017#line 152
2018  __cil_tmp9 = (struct iio_buffer *)kf;
2019#line 152
2020  iio_buffer_init(__cil_tmp9);
2021#line 153
2022  __cil_tmp10 = 0 + 176;
2023#line 153
2024  __cil_tmp11 = (unsigned long )kf;
2025#line 153
2026  __cil_tmp12 = __cil_tmp11 + __cil_tmp10;
2027#line 153
2028  *((struct attribute_group  const  **)__cil_tmp12) = (struct attribute_group  const  *)(& iio_kfifo_attribute_group);
2029#line 154
2030  __cil_tmp13 = 0 + 32;
2031#line 154
2032  __cil_tmp14 = (unsigned long )kf;
2033#line 154
2034  __cil_tmp15 = __cil_tmp14 + __cil_tmp13;
2035#line 154
2036  *((struct iio_buffer_access_funcs  const  **)__cil_tmp15) = & kfifo_access_funcs;
2037  }
2038#line 156
2039  return ((struct iio_buffer *)kf);
2040}
2041}
2042#line 160 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5494/dscv_tempdir/dscv/ri/43_1a/drivers/staging/iio/kfifo_buf.c.p"
2043void iio_kfifo_free(struct iio_buffer *r ) 
2044{ struct iio_buffer  const  *__mptr ;
2045  struct iio_kfifo *__cil_tmp3 ;
2046  void const   *__cil_tmp4 ;
2047
2048  {
2049  {
2050#line 162
2051  __mptr = (struct iio_buffer  const  *)r;
2052#line 162
2053  __cil_tmp3 = (struct iio_kfifo *)__mptr;
2054#line 162
2055  __cil_tmp4 = (void const   *)__cil_tmp3;
2056#line 162
2057  kfree(__cil_tmp4);
2058  }
2059#line 164
2060  return;
2061}
2062}
2063#line 184
2064extern void ldv_check_final_state(void) ;
2065#line 190
2066extern void ldv_initialize(void) ;
2067#line 193
2068extern int __VERIFIER_nondet_int(void) ;
2069#line 196 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5494/dscv_tempdir/dscv/ri/43_1a/drivers/staging/iio/kfifo_buf.c.p"
2070int LDV_IN_INTERRUPT  ;
2071#line 199 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5494/dscv_tempdir/dscv/ri/43_1a/drivers/staging/iio/kfifo_buf.c.p"
2072void main(void) 
2073{ int tmp ;
2074  int tmp___0 ;
2075
2076  {
2077  {
2078#line 211
2079  LDV_IN_INTERRUPT = 1;
2080#line 220
2081  ldv_initialize();
2082  }
2083#line 222
2084  goto ldv_18266;
2085  ldv_18265: 
2086  {
2087#line 225
2088  tmp = __VERIFIER_nondet_int();
2089  }
2090  {
2091#line 227
2092  goto switch_default;
2093#line 225
2094  if (0) {
2095    switch_default: /* CIL Label */ ;
2096#line 227
2097    goto ldv_18264;
2098  } else {
2099    switch_break: /* CIL Label */ ;
2100  }
2101  }
2102  ldv_18264: ;
2103  ldv_18266: 
2104  {
2105#line 222
2106  tmp___0 = __VERIFIER_nondet_int();
2107  }
2108#line 222
2109  if (tmp___0 != 0) {
2110#line 223
2111    goto ldv_18265;
2112  } else {
2113#line 225
2114    goto ldv_18267;
2115  }
2116  ldv_18267: ;
2117
2118  {
2119#line 236
2120  ldv_check_final_state();
2121  }
2122#line 239
2123  return;
2124}
2125}
2126#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5494/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
2127void ldv_blast_assert(void) 
2128{ 
2129
2130  {
2131  ERROR: ;
2132#line 6
2133  goto ERROR;
2134}
2135}
2136#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5494/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
2137extern int __VERIFIER_nondet_int(void) ;
2138#line 260 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5494/dscv_tempdir/dscv/ri/43_1a/drivers/staging/iio/kfifo_buf.c.p"
2139int ldv_spin  =    0;
2140#line 264 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5494/dscv_tempdir/dscv/ri/43_1a/drivers/staging/iio/kfifo_buf.c.p"
2141void ldv_check_alloc_flags(gfp_t flags ) 
2142{ 
2143
2144  {
2145#line 267
2146  if (ldv_spin != 0) {
2147#line 267
2148    if (flags != 32U) {
2149      {
2150#line 267
2151      ldv_blast_assert();
2152      }
2153    } else {
2154
2155    }
2156  } else {
2157
2158  }
2159#line 270
2160  return;
2161}
2162}
2163#line 270
2164extern struct page *ldv_some_page(void) ;
2165#line 273 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5494/dscv_tempdir/dscv/ri/43_1a/drivers/staging/iio/kfifo_buf.c.p"
2166struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) 
2167{ struct page *tmp ;
2168
2169  {
2170#line 276
2171  if (ldv_spin != 0) {
2172#line 276
2173    if (flags != 32U) {
2174      {
2175#line 276
2176      ldv_blast_assert();
2177      }
2178    } else {
2179
2180    }
2181  } else {
2182
2183  }
2184  {
2185#line 278
2186  tmp = ldv_some_page();
2187  }
2188#line 278
2189  return (tmp);
2190}
2191}
2192#line 282 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5494/dscv_tempdir/dscv/ri/43_1a/drivers/staging/iio/kfifo_buf.c.p"
2193void ldv_check_alloc_nonatomic(void) 
2194{ 
2195
2196  {
2197#line 285
2198  if (ldv_spin != 0) {
2199    {
2200#line 285
2201    ldv_blast_assert();
2202    }
2203  } else {
2204
2205  }
2206#line 288
2207  return;
2208}
2209}
2210#line 289 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5494/dscv_tempdir/dscv/ri/43_1a/drivers/staging/iio/kfifo_buf.c.p"
2211void ldv_spin_lock(void) 
2212{ 
2213
2214  {
2215#line 292
2216  ldv_spin = 1;
2217#line 293
2218  return;
2219}
2220}
2221#line 296 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5494/dscv_tempdir/dscv/ri/43_1a/drivers/staging/iio/kfifo_buf.c.p"
2222void ldv_spin_unlock(void) 
2223{ 
2224
2225  {
2226#line 299
2227  ldv_spin = 0;
2228#line 300
2229  return;
2230}
2231}
2232#line 303 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5494/dscv_tempdir/dscv/ri/43_1a/drivers/staging/iio/kfifo_buf.c.p"
2233int ldv_spin_trylock(void) 
2234{ int is_lock ;
2235
2236  {
2237  {
2238#line 308
2239  is_lock = __VERIFIER_nondet_int();
2240  }
2241#line 310
2242  if (is_lock != 0) {
2243#line 313
2244    return (0);
2245  } else {
2246#line 318
2247    ldv_spin = 1;
2248#line 320
2249    return (1);
2250  }
2251}
2252}
2253#line 487 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5494/dscv_tempdir/dscv/ri/43_1a/drivers/staging/iio/kfifo_buf.c.p"
2254void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) 
2255{ 
2256
2257  {
2258  {
2259#line 493
2260  ldv_check_alloc_flags(ldv_func_arg2);
2261#line 495
2262  kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
2263  }
2264#line 496
2265  return ((void *)0);
2266}
2267}
2268#line 498 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5494/dscv_tempdir/dscv/ri/43_1a/drivers/staging/iio/kfifo_buf.c.p"
2269__inline static void *kzalloc(size_t size , gfp_t flags ) 
2270{ void *tmp ;
2271
2272  {
2273  {
2274#line 504
2275  ldv_check_alloc_flags(flags);
2276#line 505
2277  tmp = __VERIFIER_nondet_pointer();
2278  }
2279#line 505
2280  return (tmp);
2281}
2282}