Showing error 237

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