32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--char--hw_random--virtio-rng.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c

extern void __VERIFIER_error() __attribute__ ((__noreturn__));

/* Generated by CIL v. 1.3.7 */
/* print_CIL_Input is true */

typedef unsigned short __u16;
typedef unsigned int __u32;
typedef unsigned long long __u64;
typedef unsigned char u8;
typedef short s16;
typedef unsigned short u16;
typedef unsigned int u32;
typedef long long s64;
typedef unsigned long long u64;
typedef long __kernel_long_t;
typedef unsigned long __kernel_ulong_t;
typedef __kernel_ulong_t __kernel_size_t;
typedef __kernel_long_t __kernel_ssize_t;
typedef long long __kernel_loff_t;
typedef __u32 __kernel_dev_t;
typedef __kernel_dev_t dev_t;
typedef unsigned short umode_t;
typedef _Bool bool;
typedef __kernel_loff_t loff_t;
typedef __kernel_size_t size_t;
typedef __kernel_ssize_t ssize_t;
typedef u64 dma_addr_t;
typedef unsigned int gfp_t;
struct __anonstruct_atomic_t_7 {
   int counter ;
};
typedef struct __anonstruct_atomic_t_7 atomic_t;
struct __anonstruct_atomic64_t_8 {
   long counter ;
};
typedef struct __anonstruct_atomic64_t_8 atomic64_t;
struct list_head {
   struct list_head *next ;
   struct list_head *prev ;
};
struct hlist_node;
struct hlist_head {
   struct hlist_node *first ;
};
struct hlist_node {
   struct hlist_node *next ;
   struct hlist_node **pprev ;
};
struct hwrng {
   char const   *name ;
   int (*init)(struct hwrng *rng ) ;
   void (*cleanup)(struct hwrng *rng ) ;
   int (*data_present)(struct hwrng *rng , int wait ) ;
   int (*data_read)(struct hwrng *rng , u32 *data ) ;
   int (*read)(struct hwrng *rng , void *data , size_t max , bool wait ) ;
   unsigned long priv ;
   struct list_head list ;
};
struct bug_entry {
   int bug_addr_disp ;
   int file_disp ;
   unsigned short line ;
   unsigned short flags ;
};
struct module;
struct module;
struct page;
struct page;
struct task_struct;
struct task_struct;
struct task_struct;
struct mm_struct;
struct mm_struct;
typedef void (*ctor_fn_t)(void);
typedef unsigned long pgdval_t;
typedef unsigned long pgprotval_t;
struct pgprot {
   pgprotval_t pgprot ;
};
typedef struct pgprot pgprot_t;
struct __anonstruct_pgd_t_19 {
   pgdval_t pgd ;
};
typedef struct __anonstruct_pgd_t_19 pgd_t;
typedef struct page *pgtable_t;
struct file;
struct file;
struct page;
struct mm_struct;
struct task_struct;
struct cpumask;
struct cpumask;
struct arch_spinlock;
struct arch_spinlock;
struct task_struct;
struct device;
struct device;
struct completion;
struct completion;
struct task_struct;
struct cpumask {
   unsigned long bits[((4096UL + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
};
typedef struct cpumask *cpumask_var_t;
struct static_key;
struct static_key;
struct kmem_cache;
typedef atomic64_t atomic_long_t;
typedef u16 __ticket_t;
typedef u32 __ticketpair_t;
struct __raw_tickets {
   __ticket_t head ;
   __ticket_t tail ;
};
union __anonunion____missing_field_name_36 {
   __ticketpair_t head_tail ;
   struct __raw_tickets tickets ;
};
struct arch_spinlock {
   union __anonunion____missing_field_name_36 __annonCompField17 ;
};
typedef struct arch_spinlock arch_spinlock_t;
struct task_struct;
struct lock_class_key {

};
struct raw_spinlock {
   arch_spinlock_t raw_lock ;
   unsigned int magic ;
   unsigned int owner_cpu ;
   void *owner ;
};
typedef struct raw_spinlock raw_spinlock_t;
union __anonunion____missing_field_name_39 {
   struct raw_spinlock rlock ;
};
struct spinlock {
   union __anonunion____missing_field_name_39 __annonCompField19 ;
};
typedef struct spinlock spinlock_t;
struct __wait_queue_head {
   spinlock_t lock ;
   struct list_head task_list ;
};
typedef struct __wait_queue_head wait_queue_head_t;
struct task_struct;
struct __anonstruct_nodemask_t_42 {
   unsigned long bits[(((unsigned long )(1 << 10) + 8UL * sizeof(long )) - 1UL) / (8UL * sizeof(long ))] ;
};
typedef struct __anonstruct_nodemask_t_42 nodemask_t;
struct page;
struct mutex {
   atomic_t count ;
   spinlock_t wait_lock ;
   struct list_head wait_list ;
   struct task_struct *owner ;
   char const   *name ;
   void *magic ;
};
struct rw_semaphore;
struct rw_semaphore;
struct rw_semaphore {
   long count ;
   raw_spinlock_t wait_lock ;
   struct list_head wait_list ;
};
struct completion {
   unsigned int done ;
   wait_queue_head_t wait ;
};
struct page;
struct device;
struct device;
union ktime {
   s64 tv64 ;
};
typedef union ktime ktime_t;
struct tvec_base;
struct tvec_base;
struct timer_list {
   struct list_head entry ;
   unsigned long expires ;
   struct tvec_base *base ;
   void (*function)(unsigned long  ) ;
   unsigned long data ;
   int slack ;
   int start_pid ;
   void *start_site ;
   char start_comm[16] ;
};
struct work_struct;
struct work_struct;
struct work_struct {
   atomic_long_t data ;
   struct list_head entry ;
   void (*func)(struct work_struct *work ) ;
};
struct device;
struct pm_message {
   int event ;
};
typedef struct pm_message pm_message_t;
struct dev_pm_ops {
   int (*prepare)(struct device *dev ) ;
   void (*complete)(struct device *dev ) ;
   int (*suspend)(struct device *dev ) ;
   int (*resume)(struct device *dev ) ;
   int (*freeze)(struct device *dev ) ;
   int (*thaw)(struct device *dev ) ;
   int (*poweroff)(struct device *dev ) ;
   int (*restore)(struct device *dev ) ;
   int (*suspend_late)(struct device *dev ) ;
   int (*resume_early)(struct device *dev ) ;
   int (*freeze_late)(struct device *dev ) ;
   int (*thaw_early)(struct device *dev ) ;
   int (*poweroff_late)(struct device *dev ) ;
   int (*restore_early)(struct device *dev ) ;
   int (*suspend_noirq)(struct device *dev ) ;
   int (*resume_noirq)(struct device *dev ) ;
   int (*freeze_noirq)(struct device *dev ) ;
   int (*thaw_noirq)(struct device *dev ) ;
   int (*poweroff_noirq)(struct device *dev ) ;
   int (*restore_noirq)(struct device *dev ) ;
   int (*runtime_suspend)(struct device *dev ) ;
   int (*runtime_resume)(struct device *dev ) ;
   int (*runtime_idle)(struct device *dev ) ;
};
enum rpm_status {
    RPM_ACTIVE = 0,
    RPM_RESUMING = 1,
    RPM_SUSPENDED = 2,
    RPM_SUSPENDING = 3
} ;
enum rpm_request {
    RPM_REQ_NONE = 0,
    RPM_REQ_IDLE = 1,
    RPM_REQ_SUSPEND = 2,
    RPM_REQ_AUTOSUSPEND = 3,
    RPM_REQ_RESUME = 4
} ;
struct wakeup_source;
struct wakeup_source;
struct pm_subsys_data {
   spinlock_t lock ;
   unsigned int refcount ;
};
struct dev_pm_qos_request;
struct pm_qos_constraints;
struct dev_pm_info {
   pm_message_t power_state ;
   unsigned int can_wakeup : 1 ;
   unsigned int async_suspend : 1 ;
   bool is_prepared : 1 ;
   bool is_suspended : 1 ;
   bool ignore_children : 1 ;
   spinlock_t lock ;
   struct list_head entry ;
   struct completion completion ;
   struct wakeup_source *wakeup ;
   bool wakeup_path : 1 ;
   struct timer_list suspend_timer ;
   unsigned long timer_expires ;
   struct work_struct work ;
   wait_queue_head_t wait_queue ;
   atomic_t usage_count ;
   atomic_t child_count ;
   unsigned int disable_depth : 3 ;
   unsigned int idle_notification : 1 ;
   unsigned int request_pending : 1 ;
   unsigned int deferred_resume : 1 ;
   unsigned int run_wake : 1 ;
   unsigned int runtime_auto : 1 ;
   unsigned int no_callbacks : 1 ;
   unsigned int irq_safe : 1 ;
   unsigned int use_autosuspend : 1 ;
   unsigned int timer_autosuspends : 1 ;
   enum rpm_request request ;
   enum rpm_status runtime_status ;
   int runtime_error ;
   int autosuspend_delay ;
   unsigned long last_busy ;
   unsigned long active_jiffies ;
   unsigned long suspended_jiffies ;
   unsigned long accounting_timestamp ;
   ktime_t suspend_time ;
   s64 max_time_suspended_ns ;
   struct dev_pm_qos_request *pq_req ;
   struct pm_subsys_data *subsys_data ;
   struct pm_qos_constraints *constraints ;
};
struct dev_pm_domain {
   struct dev_pm_ops ops ;
};
struct __anonstruct_mm_context_t_112 {
   void *ldt ;
   int size ;
   unsigned short ia32_compat ;
   struct mutex lock ;
   void *vdso ;
};
typedef struct __anonstruct_mm_context_t_112 mm_context_t;
struct vm_area_struct;
struct vm_area_struct;
struct page;
struct vm_area_struct;
struct rb_node {
   unsigned long rb_parent_color ;
   struct rb_node *rb_right ;
   struct rb_node *rb_left ;
} __attribute__((__aligned__(sizeof(long )))) ;
struct rb_root {
   struct rb_node *rb_node ;
};
struct prio_tree_node;
struct raw_prio_tree_node {
   struct prio_tree_node *left ;
   struct prio_tree_node *right ;
   struct prio_tree_node *parent ;
};
struct prio_tree_node {
   struct prio_tree_node *left ;
   struct prio_tree_node *right ;
   struct prio_tree_node *parent ;
   unsigned long start ;
   unsigned long last ;
};
struct task_struct;
struct task_struct;
struct address_space;
struct address_space;
union __anonunion____missing_field_name_140 {
   unsigned long index ;
   void *freelist ;
};
struct __anonstruct____missing_field_name_144 {
   unsigned int inuse : 16 ;
   unsigned int objects : 15 ;
   unsigned int frozen : 1 ;
};
union __anonunion____missing_field_name_143 {
   atomic_t _mapcount ;
   struct __anonstruct____missing_field_name_144 __annonCompField31 ;
};
struct __anonstruct____missing_field_name_142 {
   union __anonunion____missing_field_name_143 __annonCompField32 ;
   atomic_t _count ;
};
union __anonunion____missing_field_name_141 {
   unsigned long counters ;
   struct __anonstruct____missing_field_name_142 __annonCompField33 ;
};
struct __anonstruct____missing_field_name_139 {
   union __anonunion____missing_field_name_140 __annonCompField30 ;
   union __anonunion____missing_field_name_141 __annonCompField34 ;
};
struct __anonstruct____missing_field_name_146 {
   struct page *next ;
   int pages ;
   int pobjects ;
};
union __anonunion____missing_field_name_145 {
   struct list_head lru ;
   struct __anonstruct____missing_field_name_146 __annonCompField36 ;
};
union __anonunion____missing_field_name_147 {
   unsigned long private ;
   struct kmem_cache *slab ;
   struct page *first_page ;
};
struct page {
   unsigned long flags ;
   struct address_space *mapping ;
   struct __anonstruct____missing_field_name_139 __annonCompField35 ;
   union __anonunion____missing_field_name_145 __annonCompField37 ;
   union __anonunion____missing_field_name_147 __annonCompField38 ;
   unsigned long debug_flags ;
} __attribute__((__aligned__((2) *  (sizeof(unsigned long )) ))) ;
struct __anonstruct_vm_set_149 {
   struct list_head list ;
   void *parent ;
   struct vm_area_struct *head ;
};
union __anonunion_shared_148 {
   struct __anonstruct_vm_set_149 vm_set ;
   struct raw_prio_tree_node prio_tree_node ;
};
struct anon_vma;
struct vm_operations_struct;
struct mempolicy;
struct vm_area_struct {
   struct mm_struct *vm_mm ;
   unsigned long vm_start ;
   unsigned long vm_end ;
   struct vm_area_struct *vm_next ;
   struct vm_area_struct *vm_prev ;
   pgprot_t vm_page_prot ;
   unsigned long vm_flags ;
   struct rb_node vm_rb ;
   union __anonunion_shared_148 shared ;
   struct list_head anon_vma_chain ;
   struct anon_vma *anon_vma ;
   struct vm_operations_struct  const  *vm_ops ;
   unsigned long vm_pgoff ;
   struct file *vm_file ;
   void *vm_private_data ;
   struct mempolicy *vm_policy ;
};
struct core_thread {
   struct task_struct *task ;
   struct core_thread *next ;
};
struct core_state {
   atomic_t nr_threads ;
   struct core_thread dumper ;
   struct completion startup ;
};
struct mm_rss_stat {
   atomic_long_t count[3] ;
};
struct linux_binfmt;
struct mmu_notifier_mm;
struct mm_struct {
   struct vm_area_struct *mmap ;
   struct rb_root mm_rb ;
   struct vm_area_struct *mmap_cache ;
   unsigned long (*get_unmapped_area)(struct file *filp , unsigned long addr , unsigned long len ,
                                      unsigned long pgoff , unsigned long flags ) ;
   void (*unmap_area)(struct mm_struct *mm , unsigned long addr ) ;
   unsigned long mmap_base ;
   unsigned long task_size ;
   unsigned long cached_hole_size ;
   unsigned long free_area_cache ;
   pgd_t *pgd ;
   atomic_t mm_users ;
   atomic_t mm_count ;
   int map_count ;
   spinlock_t page_table_lock ;
   struct rw_semaphore mmap_sem ;
   struct list_head mmlist ;
   unsigned long hiwater_rss ;
   unsigned long hiwater_vm ;
   unsigned long total_vm ;
   unsigned long locked_vm ;
   unsigned long pinned_vm ;
   unsigned long shared_vm ;
   unsigned long exec_vm ;
   unsigned long stack_vm ;
   unsigned long reserved_vm ;
   unsigned long def_flags ;
   unsigned long nr_ptes ;
   unsigned long start_code ;
   unsigned long end_code ;
   unsigned long start_data ;
   unsigned long end_data ;
   unsigned long start_brk ;
   unsigned long brk ;
   unsigned long start_stack ;
   unsigned long arg_start ;
   unsigned long arg_end ;
   unsigned long env_start ;
   unsigned long env_end ;
   unsigned long saved_auxv[44] ;
   struct mm_rss_stat rss_stat ;
   struct linux_binfmt *binfmt ;
   cpumask_var_t cpu_vm_mask_var ;
   mm_context_t context ;
   unsigned int faultstamp ;
   unsigned int token_priority ;
   unsigned int last_interval ;
   unsigned long flags ;
   struct core_state *core_state ;
   spinlock_t ioctx_lock ;
   struct hlist_head ioctx_list ;
   struct task_struct *owner ;
   struct file *exe_file ;
   unsigned long num_exe_file_vmas ;
   struct mmu_notifier_mm *mmu_notifier_mm ;
   pgtable_t pmd_huge_pte ;
   struct cpumask cpumask_allocation ;
};
struct mempolicy;
struct anon_vma;
struct mm_struct;
struct vm_area_struct;
struct vm_fault {
   unsigned int flags ;
   unsigned long pgoff ;
   void *virtual_address ;
   struct page *page ;
};
struct vm_operations_struct {
   void (*open)(struct vm_area_struct *area ) ;
   void (*close)(struct vm_area_struct *area ) ;
   int (*fault)(struct vm_area_struct *vma , struct vm_fault *vmf ) ;
   int (*page_mkwrite)(struct vm_area_struct *vma , struct vm_fault *vmf ) ;
   int (*access)(struct vm_area_struct *vma , unsigned long addr , void *buf , int len ,
                 int write ) ;
   int (*set_policy)(struct vm_area_struct *vma , struct mempolicy *new ) ;
   struct mempolicy *(*get_policy)(struct vm_area_struct *vma , unsigned long addr ) ;
   int (*migrate)(struct vm_area_struct *vma , nodemask_t const   *from , nodemask_t const   *to ,
                  unsigned long flags ) ;
};
struct page;
struct scatterlist {
   unsigned long sg_magic ;
   unsigned long page_link ;
   unsigned int offset ;
   unsigned int length ;
   dma_addr_t dma_address ;
   unsigned int dma_length ;
};
struct sock;
struct sock;
struct kobject;
struct kobject;
enum kobj_ns_type {
    KOBJ_NS_TYPE_NONE = 0,
    KOBJ_NS_TYPE_NET = 1,
    KOBJ_NS_TYPES = 2
} ;
struct kobj_ns_type_operations {
   enum kobj_ns_type type ;
   void *(*grab_current_ns)(void) ;
   void const   *(*netlink_ns)(struct sock *sk ) ;
   void const   *(*initial_ns)(void) ;
   void (*drop_ns)(void * ) ;
};
struct kobject;
struct module;
enum kobj_ns_type;
struct attribute {
   char const   *name ;
   umode_t mode ;
};
struct attribute_group {
   char const   *name ;
   umode_t (*is_visible)(struct kobject * , struct attribute * , int  ) ;
   struct attribute **attrs ;
};
struct file;
struct vm_area_struct;
struct bin_attribute {
   struct attribute attr ;
   size_t size ;
   void *private ;
   ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
                   loff_t  , size_t  ) ;
   ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
                    loff_t  , size_t  ) ;
   int (*mmap)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ) ;
};
struct sysfs_ops {
   ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
   ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
   void const   *(*namespace)(struct kobject * , struct attribute  const  * ) ;
};
struct sysfs_dirent;
struct sysfs_dirent;
struct kref {
   atomic_t refcount ;
};
struct kset;
struct kobj_type;
struct kobject {
   char const   *name ;
   struct list_head entry ;
   struct kobject *parent ;
   struct kset *kset ;
   struct kobj_type *ktype ;
   struct sysfs_dirent *sd ;
   struct kref kref ;
   unsigned int state_initialized : 1 ;
   unsigned int state_in_sysfs : 1 ;
   unsigned int state_add_uevent_sent : 1 ;
   unsigned int state_remove_uevent_sent : 1 ;
   unsigned int uevent_suppress : 1 ;
};
struct kobj_type {
   void (*release)(struct kobject *kobj ) ;
   struct sysfs_ops  const  *sysfs_ops ;
   struct attribute **default_attrs ;
   struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject *kobj ) ;
   void const   *(*namespace)(struct kobject *kobj ) ;
};
struct kobj_uevent_env {
   char *envp[32] ;
   int envp_idx ;
   char buf[2048] ;
   int buflen ;
};
struct kset_uevent_ops {
   int (* const  filter)(struct kset *kset , struct kobject *kobj ) ;
   char const   *(* const  name)(struct kset *kset , struct kobject *kobj ) ;
   int (* const  uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
};
struct sock;
struct kset {
   struct list_head list ;
   spinlock_t list_lock ;
   struct kobject kobj ;
   struct kset_uevent_ops  const  *uevent_ops ;
};
struct klist_node;
struct klist_node;
struct klist_node {
   void *n_klist ;
   struct list_head n_node ;
   struct kref n_ref ;
};
struct dma_map_ops;
struct dev_archdata {
   void *acpi_handle ;
   struct dma_map_ops *dma_ops ;
   void *iommu ;
};
struct device;
struct device_private;
struct device_private;
struct device_driver;
struct device_driver;
struct driver_private;
struct driver_private;
struct module;
struct class;
struct class;
struct subsys_private;
struct subsys_private;
struct bus_type;
struct bus_type;
struct device_node;
struct device_node;
struct iommu_ops;
struct iommu_ops;
struct bus_attribute {
   struct attribute attr ;
   ssize_t (*show)(struct bus_type *bus , char *buf ) ;
   ssize_t (*store)(struct bus_type *bus , char const   *buf , size_t count ) ;
};
struct device_attribute;
struct driver_attribute;
struct bus_type {
   char const   *name ;
   char const   *dev_name ;
   struct device *dev_root ;
   struct bus_attribute *bus_attrs ;
   struct device_attribute *dev_attrs ;
   struct driver_attribute *drv_attrs ;
   int (*match)(struct device *dev , struct device_driver *drv ) ;
   int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
   int (*probe)(struct device *dev ) ;
   int (*remove)(struct device *dev ) ;
   void (*shutdown)(struct device *dev ) ;
   int (*suspend)(struct device *dev , pm_message_t state ) ;
   int (*resume)(struct device *dev ) ;
   struct dev_pm_ops  const  *pm ;
   struct iommu_ops *iommu_ops ;
   struct subsys_private *p ;
};
struct device_type;
struct of_device_id;
struct device_driver {
   char const   *name ;
   struct bus_type *bus ;
   struct module *owner ;
   char const   *mod_name ;
   bool suppress_bind_attrs ;
   struct of_device_id  const  *of_match_table ;
   int (*probe)(struct device *dev ) ;
   int (*remove)(struct device *dev ) ;
   void (*shutdown)(struct device *dev ) ;
   int (*suspend)(struct device *dev , pm_message_t state ) ;
   int (*resume)(struct device *dev ) ;
   struct attribute_group  const  **groups ;
   struct dev_pm_ops  const  *pm ;
   struct driver_private *p ;
};
struct driver_attribute {
   struct attribute attr ;
   ssize_t (*show)(struct device_driver *driver , char *buf ) ;
   ssize_t (*store)(struct device_driver *driver , char const   *buf , size_t count ) ;
};
struct class_attribute;
struct class {
   char const   *name ;
   struct module *owner ;
   struct class_attribute *class_attrs ;
   struct device_attribute *dev_attrs ;
   struct bin_attribute *dev_bin_attrs ;
   struct kobject *dev_kobj ;
   int (*dev_uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
   char *(*devnode)(struct device *dev , umode_t *mode ) ;
   void (*class_release)(struct class *class ) ;
   void (*dev_release)(struct device *dev ) ;
   int (*suspend)(struct device *dev , pm_message_t state ) ;
   int (*resume)(struct device *dev ) ;
   struct kobj_ns_type_operations  const  *ns_type ;
   void const   *(*namespace)(struct device *dev ) ;
   struct dev_pm_ops  const  *pm ;
   struct subsys_private *p ;
};
struct class_attribute {
   struct attribute attr ;
   ssize_t (*show)(struct class *class , struct class_attribute *attr , char *buf ) ;
   ssize_t (*store)(struct class *class , struct class_attribute *attr , char const   *buf ,
                    size_t count ) ;
   void const   *(*namespace)(struct class *class , struct class_attribute  const  *attr ) ;
};
struct device_type {
   char const   *name ;
   struct attribute_group  const  **groups ;
   int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
   char *(*devnode)(struct device *dev , umode_t *mode ) ;
   void (*release)(struct device *dev ) ;
   struct dev_pm_ops  const  *pm ;
};
struct device_attribute {
   struct attribute attr ;
   ssize_t (*show)(struct device *dev , struct device_attribute *attr , char *buf ) ;
   ssize_t (*store)(struct device *dev , struct device_attribute *attr , char const   *buf ,
                    size_t count ) ;
};
struct device_dma_parameters {
   unsigned int max_segment_size ;
   unsigned long segment_boundary_mask ;
};
struct dma_coherent_mem;
struct device {
   struct device *parent ;
   struct device_private *p ;
   struct kobject kobj ;
   char const   *init_name ;
   struct device_type  const  *type ;
   struct mutex mutex ;
   struct bus_type *bus ;
   struct device_driver *driver ;
   void *platform_data ;
   struct dev_pm_info power ;
   struct dev_pm_domain *pm_domain ;
   int numa_node ;
   u64 *dma_mask ;
   u64 coherent_dma_mask ;
   struct device_dma_parameters *dma_parms ;
   struct list_head dma_pools ;
   struct dma_coherent_mem *dma_mem ;
   struct dev_archdata archdata ;
   struct device_node *of_node ;
   dev_t devt ;
   u32 id ;
   spinlock_t devres_lock ;
   struct list_head devres_head ;
   struct klist_node knode_class ;
   struct class *class ;
   struct attribute_group  const  **groups ;
   void (*release)(struct device *dev ) ;
};
struct wakeup_source {
   char const   *name ;
   struct list_head entry ;
   spinlock_t lock ;
   struct timer_list timer ;
   unsigned long timer_expires ;
   ktime_t total_time ;
   ktime_t max_time ;
   ktime_t last_time ;
   unsigned long event_count ;
   unsigned long active_count ;
   unsigned long relax_count ;
   unsigned long hit_count ;
   unsigned int active : 1 ;
};
struct of_device_id {
   char name[32] ;
   char type[32] ;
   char compatible[128] ;
   void *data ;
};
struct virtio_device_id {
   __u32 device ;
   __u32 vendor ;
};
struct virtio_device;
struct virtqueue {
   struct list_head list ;
   void (*callback)(struct virtqueue *vq ) ;
   char const   *name ;
   struct virtio_device *vdev ;
   void *priv ;
};
struct virtio_config_ops;
struct virtio_device {
   int index ;
   struct device dev ;
   struct virtio_device_id id ;
   struct virtio_config_ops *config ;
   struct list_head vqs ;
   unsigned long features[1] ;
   void *priv ;
};
struct virtio_driver {
   struct device_driver driver ;
   struct virtio_device_id  const  *id_table ;
   unsigned int const   *feature_table ;
   unsigned int feature_table_size ;
   int (*probe)(struct virtio_device *dev ) ;
   void (*remove)(struct virtio_device *dev ) ;
   void (*config_changed)(struct virtio_device *dev ) ;
   int (*freeze)(struct virtio_device *dev ) ;
   int (*restore)(struct virtio_device *dev ) ;
};
typedef void vq_callback_t(struct virtqueue * );
struct virtio_config_ops {
   void (*get)(struct virtio_device *vdev , unsigned int offset , void *buf , unsigned int len ) ;
   void (*set)(struct virtio_device *vdev , unsigned int offset , void const   *buf ,
               unsigned int len ) ;
   u8 (*get_status)(struct virtio_device *vdev ) ;
   void (*set_status)(struct virtio_device *vdev , u8 status ) ;
   void (*reset)(struct virtio_device *vdev ) ;
   int (*find_vqs)(struct virtio_device * , unsigned int nvqs , struct virtqueue **vqs ,
                   vq_callback_t **callbacks , char const   **names ) ;
   void (*del_vqs)(struct virtio_device * ) ;
   u32 (*get_features)(struct virtio_device *vdev ) ;
   void (*finalize_features)(struct virtio_device *vdev ) ;
   char const   *(*bus_name)(struct virtio_device *vdev ) ;
};
struct completion;
struct file;
struct task_struct;
typedef __u64 Elf64_Addr;
typedef __u16 Elf64_Half;
typedef __u32 Elf64_Word;
typedef __u64 Elf64_Xword;
struct elf64_sym {
   Elf64_Word st_name ;
   unsigned char st_info ;
   unsigned char st_other ;
   Elf64_Half st_shndx ;
   Elf64_Addr st_value ;
   Elf64_Xword st_size ;
};
typedef struct elf64_sym Elf64_Sym;
struct file;
struct kernel_param;
struct kernel_param;
struct kernel_param_ops {
   int (*set)(char const   *val , struct kernel_param  const  *kp ) ;
   int (*get)(char *buffer , struct kernel_param  const  *kp ) ;
   void (*free)(void *arg ) ;
};
struct kparam_string;
struct kparam_array;
union __anonunion____missing_field_name_212 {
   void *arg ;
   struct kparam_string  const  *str ;
   struct kparam_array  const  *arr ;
};
struct kernel_param {
   char const   *name ;
   struct kernel_param_ops  const  *ops ;
   u16 perm ;
   s16 level ;
   union __anonunion____missing_field_name_212 __annonCompField41 ;
};
struct kparam_string {
   unsigned int maxlen ;
   char *string ;
};
struct kparam_array {
   unsigned int max ;
   unsigned int elemsize ;
   unsigned int *num ;
   struct kernel_param_ops  const  *ops ;
   void *elem ;
};
struct module;
struct module;
struct static_key {
   atomic_t enabled ;
};
struct module;
struct tracepoint;
struct tracepoint;
struct tracepoint_func {
   void *func ;
   void *data ;
};
struct tracepoint {
   char const   *name ;
   struct static_key key ;
   void (*regfunc)(void) ;
   void (*unregfunc)(void) ;
   struct tracepoint_func *funcs ;
};
struct kernel_symbol {
   unsigned long value ;
   char const   *name ;
};
struct mod_arch_specific {

};
struct module;
struct module_param_attrs;
struct module_kobject {
   struct kobject kobj ;
   struct module *mod ;
   struct kobject *drivers_dir ;
   struct module_param_attrs *mp ;
};
struct module_attribute {
   struct attribute attr ;
   ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
   ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const   * ,
                    size_t count ) ;
   void (*setup)(struct module * , char const   * ) ;
   int (*test)(struct module * ) ;
   void (*free)(struct module * ) ;
};
struct exception_table_entry;
struct exception_table_entry;
enum module_state {
    MODULE_STATE_LIVE = 0,
    MODULE_STATE_COMING = 1,
    MODULE_STATE_GOING = 2
} ;
struct module_ref {
   unsigned long incs ;
   unsigned long decs ;
} __attribute__((__aligned__((2) *  (sizeof(unsigned long )) ))) ;
struct module_sect_attrs;
struct module_notes_attrs;
struct ftrace_event_call;
struct module {
   enum module_state state ;
   struct list_head list ;
   char name[64UL - sizeof(unsigned long )] ;
   struct module_kobject mkobj ;
   struct module_attribute *modinfo_attrs ;
   char const   *version ;
   char const   *srcversion ;
   struct kobject *holders_dir ;
   struct kernel_symbol  const  *syms ;
   unsigned long const   *crcs ;
   unsigned int num_syms ;
   struct kernel_param *kp ;
   unsigned int num_kp ;
   unsigned int num_gpl_syms ;
   struct kernel_symbol  const  *gpl_syms ;
   unsigned long const   *gpl_crcs ;
   struct kernel_symbol  const  *unused_syms ;
   unsigned long const   *unused_crcs ;
   unsigned int num_unused_syms ;
   unsigned int num_unused_gpl_syms ;
   struct kernel_symbol  const  *unused_gpl_syms ;
   unsigned long const   *unused_gpl_crcs ;
   struct kernel_symbol  const  *gpl_future_syms ;
   unsigned long const   *gpl_future_crcs ;
   unsigned int num_gpl_future_syms ;
   unsigned int num_exentries ;
   struct exception_table_entry *extable ;
   int (*init)(void) ;
   void *module_init ;
   void *module_core ;
   unsigned int init_size ;
   unsigned int core_size ;
   unsigned int init_text_size ;
   unsigned int core_text_size ;
   unsigned int init_ro_size ;
   unsigned int core_ro_size ;
   struct mod_arch_specific arch ;
   unsigned int taints ;
   unsigned int num_bugs ;
   struct list_head bug_list ;
   struct bug_entry *bug_table ;
   Elf64_Sym *symtab ;
   Elf64_Sym *core_symtab ;
   unsigned int num_symtab ;
   unsigned int core_num_syms ;
   char *strtab ;
   char *core_strtab ;
   struct module_sect_attrs *sect_attrs ;
   struct module_notes_attrs *notes_attrs ;
   char *args ;
   void *percpu ;
   unsigned int percpu_size ;
   unsigned int num_tracepoints ;
   struct tracepoint * const  *tracepoints_ptrs ;
   unsigned int num_trace_bprintk_fmt ;
   char const   **trace_bprintk_fmt_start ;
   struct ftrace_event_call **trace_events ;
   unsigned int num_trace_events ;
   struct list_head source_list ;
   struct list_head target_list ;
   struct task_struct *waiter ;
   void (*exit)(void) ;
   struct module_ref *refptr ;
   ctor_fn_t *ctors ;
   unsigned int num_ctors ;
};
long ldv__builtin_expect(long val , long res ) ;
__inline static void * __attribute__((__warn_unused_result__)) ERR_PTR(long error )  __attribute__((__no_instrument_function__)) ;
__inline static void * __attribute__((__warn_unused_result__)) ERR_PTR(long error ) 
{ 

  {
  return ((void *)error);
}
}
__inline static long __attribute__((__warn_unused_result__))  PTR_ERR(void const   *ptr )  __attribute__((__no_instrument_function__)) ;
__inline static long __attribute__((__warn_unused_result__))  PTR_ERR(void const   *ptr ) 
{ 

  {
  return ((long )ptr);
}
}
__inline static long __attribute__((__warn_unused_result__))  IS_ERR(void const   *ptr )  __attribute__((__no_instrument_function__)) ;
__inline static long __attribute__((__warn_unused_result__))  IS_ERR(void const   *ptr ) 
{ long tmp ;
  unsigned long __cil_tmp3 ;
  int __cil_tmp4 ;
  int __cil_tmp5 ;
  int __cil_tmp6 ;
  long __cil_tmp7 ;

  {
  {
  __cil_tmp3 = (unsigned long )ptr;
  __cil_tmp4 = __cil_tmp3 >= 0xfffffffffffff001UL;
  __cil_tmp5 = ! __cil_tmp4;
  __cil_tmp6 = ! __cil_tmp5;
  __cil_tmp7 = (long )__cil_tmp6;
  tmp = ldv__builtin_expect(__cil_tmp7, 0L);
  }
  return (tmp);
}
}
extern int hwrng_register(struct hwrng *rng ) ;
extern void hwrng_unregister(struct hwrng *rng ) ;
extern void __init_waitqueue_head(wait_queue_head_t *q , char const   *name , struct lock_class_key * ) ;
void mutex_lock(struct mutex *lock ) ;
int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) ;
int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) ;
int mutex_trylock(struct mutex *lock ) ;
void mutex_unlock(struct mutex *lock ) ;
int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
static struct lock_class_key __key  ;
__inline static void init_completion(struct completion *x )  __attribute__((__no_instrument_function__)) ;
__inline static void init_completion(struct completion *x ) 
{ unsigned long __cil_tmp2 ;
  unsigned long __cil_tmp3 ;
  wait_queue_head_t *__cil_tmp4 ;

  {
  *((unsigned int *)x) = 0U;
  {
  while (1) {
    while_continue: /* CIL Label */ ;
    {
    __cil_tmp2 = (unsigned long )x;
    __cil_tmp3 = __cil_tmp2 + 8;
    __cil_tmp4 = (wait_queue_head_t *)__cil_tmp3;
    __init_waitqueue_head(__cil_tmp4, "&x->wait", & __key);
    }
    goto while_break;
  }
  while_break: /* CIL Label */ ;
  }
  return;
}
}
extern void wait_for_completion(struct completion * ) ;
extern void complete(struct completion * ) ;
extern void sg_init_one(struct scatterlist * , void const   * , unsigned int  ) ;
extern int virtqueue_add_buf(struct virtqueue *vq , struct scatterlist *sg , unsigned int out_num ,
                             unsigned int in_num , void *data , gfp_t gfp ) ;
extern void virtqueue_kick(struct virtqueue *vq ) ;
extern void *virtqueue_get_buf(struct virtqueue *vq , unsigned int *len ) ;
extern int register_virtio_driver(struct virtio_driver *drv ) ;
extern void unregister_virtio_driver(struct virtio_driver *drv ) ;
__inline static struct virtqueue *virtio_find_single_vq(struct virtio_device *vdev ,
                                                        vq_callback_t *c , char const   *n )  __attribute__((__no_instrument_function__)) ;
__inline static struct virtqueue *virtio_find_single_vq(struct virtio_device *vdev ,
                                                        vq_callback_t *c , char const   *n ) 
{ vq_callback_t *callbacks[1] ;
  char const   *names[1] ;
  struct virtqueue *vq ;
  int err ;
  int tmp ;
  void *tmp___0 ;
  unsigned long __cil_tmp10 ;
  unsigned long __cil_tmp11 ;
  unsigned long __cil_tmp12 ;
  unsigned long __cil_tmp13 ;
  unsigned long __cil_tmp14 ;
  unsigned long __cil_tmp15 ;
  struct virtio_config_ops *__cil_tmp16 ;
  unsigned long __cil_tmp17 ;
  unsigned long __cil_tmp18 ;
  int (*__cil_tmp19)(struct virtio_device * , unsigned int nvqs , struct virtqueue **vqs ,
                     vq_callback_t **callbacks , char const   **names ) ;
  unsigned long __cil_tmp20 ;
  unsigned long __cil_tmp21 ;
  vq_callback_t **__cil_tmp22 ;
  unsigned long __cil_tmp23 ;
  unsigned long __cil_tmp24 ;
  char const   **__cil_tmp25 ;
  long __cil_tmp26 ;
  struct virtqueue **__cil_tmp27 ;

  {
  {
  __cil_tmp10 = 0 * 8UL;
  __cil_tmp11 = (unsigned long )(callbacks) + __cil_tmp10;
  *((vq_callback_t **)__cil_tmp11) = c;
  __cil_tmp12 = 0 * 8UL;
  __cil_tmp13 = (unsigned long )(names) + __cil_tmp12;
  *((char const   **)__cil_tmp13) = n;
  __cil_tmp14 = (unsigned long )vdev;
  __cil_tmp15 = __cil_tmp14 + 784;
  __cil_tmp16 = *((struct virtio_config_ops **)__cil_tmp15);
  __cil_tmp17 = (unsigned long )__cil_tmp16;
  __cil_tmp18 = __cil_tmp17 + 40;
  __cil_tmp19 = *((int (**)(struct virtio_device * , unsigned int nvqs , struct virtqueue **vqs ,
                            vq_callback_t **callbacks , char const   **names ))__cil_tmp18);
  __cil_tmp20 = 0 * 8UL;
  __cil_tmp21 = (unsigned long )(callbacks) + __cil_tmp20;
  __cil_tmp22 = (vq_callback_t **)__cil_tmp21;
  __cil_tmp23 = 0 * 8UL;
  __cil_tmp24 = (unsigned long )(names) + __cil_tmp23;
  __cil_tmp25 = (char const   **)__cil_tmp24;
  tmp = (*__cil_tmp19)(vdev, 1U, & vq, __cil_tmp22, __cil_tmp25);
  err = tmp;
  }
  if (err < 0) {
    {
    __cil_tmp26 = (long )err;
    tmp___0 = (void *)ERR_PTR(__cil_tmp26);
    }
    return ((struct virtqueue *)tmp___0);
  } else {

  }
  {
  __cil_tmp27 = & vq;
  return (*__cil_tmp27);
  }
}
}
extern struct module __this_module ;
int init_module(void) ;
void cleanup_module(void) ;
static struct virtqueue *vq  ;
static unsigned int data_avail  ;
static struct completion have_data  =    {0U, {{{{{{(__ticketpair_t )0}}, 3735899821U, 4294967295U, (void *)-1L}}}, {& have_data.wait.task_list,
                                                                               & have_data.wait.task_list}}};
static bool busy  ;
static void random_recv_done(struct virtqueue *vq___0 ) 
{ void *tmp ;

  {
  {
  tmp = virtqueue_get_buf(vq___0, & data_avail);
  }
  if (tmp) {

  } else {
    return;
  }
  {
  complete(& have_data);
  }
  return;
}
}
static void register_buffer(u8 *buf , size_t size ) 
{ struct scatterlist sg ;
  int tmp ;
  void const   *__cil_tmp5 ;
  unsigned int __cil_tmp6 ;
  void *__cil_tmp7 ;

  {
  {
  __cil_tmp5 = (void const   *)buf;
  __cil_tmp6 = (unsigned int )size;
  sg_init_one(& sg, __cil_tmp5, __cil_tmp6);
  __cil_tmp7 = (void *)buf;
  tmp = virtqueue_add_buf(vq, & sg, 0U, 1U, __cil_tmp7, 208U);
  }
  if (tmp < 0) {
    {
    while (1) {
      while_continue: /* CIL Label */ ;
      __asm__  volatile   ("1:\tud2\n"
                           ".pushsection __bug_table,\"a\"\n"
                           "2:\t.long 1b - 2b, %c0 - 2b\n"
                           "\t.word %c1, 0\n"
                           "\t.org 2b+%c2\n"
                           ".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"),
                           "i" (52), "i" (12UL));
      {
      while (1) {
        while_continue___0: /* CIL Label */ ;
      }
      while_break___0: /* CIL Label */ ;
      }
      goto while_break;
    }
    while_break: /* CIL Label */ ;
    }
  } else {

  }
  {
  virtqueue_kick(vq);
  }
  return;
}
}
static int virtio_read(struct hwrng *rng , void *buf , size_t size , bool wait ) 
{ u8 *__cil_tmp5 ;
  unsigned int *__cil_tmp6 ;
  unsigned int __cil_tmp7 ;

  {
  if (! busy) {
    {
    busy = (bool )1;
    init_completion(& have_data);
    __cil_tmp5 = (u8 *)buf;
    register_buffer(__cil_tmp5, size);
    }
  } else {

  }
  if (! wait) {
    return (0);
  } else {

  }
  {
  wait_for_completion(& have_data);
  busy = (bool )0;
  }
  {
  __cil_tmp6 = & data_avail;
  __cil_tmp7 = *__cil_tmp6;
  return ((int )__cil_tmp7);
  }
}
}
static void virtio_cleanup(struct hwrng *rng ) 
{ 

  {
  if (busy) {
    {
    wait_for_completion(& have_data);
    }
  } else {

  }
  return;
}
}
static struct hwrng virtio_hwrng  = 
     {"virtio", (int (*)(struct hwrng *rng ))0, & virtio_cleanup, (int (*)(struct hwrng *rng ,
                                                                         int wait ))0,
    (int (*)(struct hwrng *rng , u32 *data ))0, & virtio_read, 0UL, {(struct list_head *)0,
                                                                     (struct list_head *)0}};
static int virtrng_probe(struct virtio_device *vdev ) 
{ int err ;
  long tmp ;
  long tmp___0 ;
  void const   *__cil_tmp5 ;
  void const   *__cil_tmp6 ;
  unsigned long __cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  struct virtio_config_ops *__cil_tmp9 ;
  unsigned long __cil_tmp10 ;
  unsigned long __cil_tmp11 ;
  void (*__cil_tmp12)(struct virtio_device * ) ;

  {
  {
  vq = virtio_find_single_vq(vdev, & random_recv_done, "input");
  __cil_tmp5 = (void const   *)vq;
  tmp___0 = (long )IS_ERR(__cil_tmp5);
  }
  if (tmp___0) {
    {
    __cil_tmp6 = (void const   *)vq;
    tmp = (long )PTR_ERR(__cil_tmp6);
    }
    return ((int )tmp);
  } else {

  }
  {
  err = hwrng_register(& virtio_hwrng);
  }
  if (err) {
    {
    __cil_tmp7 = (unsigned long )vdev;
    __cil_tmp8 = __cil_tmp7 + 784;
    __cil_tmp9 = *((struct virtio_config_ops **)__cil_tmp8);
    __cil_tmp10 = (unsigned long )__cil_tmp9;
    __cil_tmp11 = __cil_tmp10 + 48;
    __cil_tmp12 = *((void (**)(struct virtio_device * ))__cil_tmp11);
    (*__cil_tmp12)(vdev);
    }
    return (err);
  } else {

  }
  return (0);
}
}
static void virtrng_remove(struct virtio_device *vdev )  __attribute__((__section__(".devexit.text"),
__no_instrument_function__)) ;
static void virtrng_remove(struct virtio_device *vdev ) 
{ unsigned long __cil_tmp2 ;
  unsigned long __cil_tmp3 ;
  struct virtio_config_ops *__cil_tmp4 ;
  unsigned long __cil_tmp5 ;
  unsigned long __cil_tmp6 ;
  void (*__cil_tmp7)(struct virtio_device *vdev ) ;
  unsigned long __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  struct virtio_config_ops *__cil_tmp10 ;
  unsigned long __cil_tmp11 ;
  unsigned long __cil_tmp12 ;
  void (*__cil_tmp13)(struct virtio_device * ) ;

  {
  {
  __cil_tmp2 = (unsigned long )vdev;
  __cil_tmp3 = __cil_tmp2 + 784;
  __cil_tmp4 = *((struct virtio_config_ops **)__cil_tmp3);
  __cil_tmp5 = (unsigned long )__cil_tmp4;
  __cil_tmp6 = __cil_tmp5 + 32;
  __cil_tmp7 = *((void (**)(struct virtio_device *vdev ))__cil_tmp6);
  (*__cil_tmp7)(vdev);
  hwrng_unregister(& virtio_hwrng);
  __cil_tmp8 = (unsigned long )vdev;
  __cil_tmp9 = __cil_tmp8 + 784;
  __cil_tmp10 = *((struct virtio_config_ops **)__cil_tmp9);
  __cil_tmp11 = (unsigned long )__cil_tmp10;
  __cil_tmp12 = __cil_tmp11 + 48;
  __cil_tmp13 = *((void (**)(struct virtio_device * ))__cil_tmp12);
  (*__cil_tmp13)(vdev);
  }
  return;
}
}
static struct virtio_device_id id_table[2]  = {      {(__u32 )4, 4294967295U}, 
        {(__u32 )0, 0U}};
static struct virtio_driver virtio_rng_driver  = 
     {{"virtio_rng", (struct bus_type *)0, & __this_module, (char const   *)0, (_Bool)0,
     (struct of_device_id  const  *)0, (int (*)(struct device *dev ))0, (int (*)(struct device *dev ))0,
     (void (*)(struct device *dev ))0, (int (*)(struct device *dev , pm_message_t state ))0,
     (int (*)(struct device *dev ))0, (struct attribute_group  const  **)0, (struct dev_pm_ops  const  *)0,
     (struct driver_private *)0}, (struct virtio_device_id  const  *)(id_table), (unsigned int const   *)0,
    0U, & virtrng_probe, & virtrng_remove, (void (*)(struct virtio_device *dev ))0,
    (int (*)(struct virtio_device *dev ))0, (int (*)(struct virtio_device *dev ))0};
static int init(void)  __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
static int init(void) 
{ int tmp ;

  {
  {
  tmp = register_virtio_driver(& virtio_rng_driver);
  }
  return (tmp);
}
}
static void fini(void)  __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
static void fini(void) 
{ 

  {
  {
  unregister_virtio_driver(& virtio_rng_driver);
  }
  return;
}
}
int init_module(void) 
{ int tmp ;

  {
  {
  tmp = init();
  }
  return (tmp);
}
}
void cleanup_module(void) 
{ 

  {
  {
  fini();
  }
  return;
}
}
extern struct virtio_device_id  const  __mod_virtio_device_table  __attribute__((__unused__,
__alias__("id_table"))) ;
static char const   __mod_description140[40]  __attribute__((__used__, __unused__,
__section__(".modinfo"), __aligned__(1)))  = 
  {      (char const   )'d',      (char const   )'e',      (char const   )'s',      (char const   )'c', 
        (char const   )'r',      (char const   )'i',      (char const   )'p',      (char const   )'t', 
        (char const   )'i',      (char const   )'o',      (char const   )'n',      (char const   )'=', 
        (char const   )'V',      (char const   )'i',      (char const   )'r',      (char const   )'t', 
        (char const   )'i',      (char const   )'o',      (char const   )' ',      (char const   )'r', 
        (char const   )'a',      (char const   )'n',      (char const   )'d',      (char const   )'o', 
        (char const   )'m',      (char const   )' ',      (char const   )'n',      (char const   )'u', 
        (char const   )'m',      (char const   )'b',      (char const   )'e',      (char const   )'r', 
        (char const   )' ',      (char const   )'d',      (char const   )'r',      (char const   )'i', 
        (char const   )'v',      (char const   )'e',      (char const   )'r',      (char const   )'\000'};
static char const   __mod_license141[12]  __attribute__((__used__, __unused__, __section__(".modinfo"),
__aligned__(1)))  = 
  {      (char const   )'l',      (char const   )'i',      (char const   )'c',      (char const   )'e', 
        (char const   )'n',      (char const   )'s',      (char const   )'e',      (char const   )'=', 
        (char const   )'G',      (char const   )'P',      (char const   )'L',      (char const   )'\000'};
void ldv_check_final_state(void) ;
extern void ldv_check_return_value(int res ) ;
extern void ldv_initialize(void) ;
extern int __VERIFIER_nondet_int(void) ;
int LDV_IN_INTERRUPT  ;
static int res_virtrng_probe_4  ;
void main(void) 
{ struct hwrng *var_group1 ;
  void *var_virtio_read_2_p1 ;
  size_t var_virtio_read_2_p2 ;
  bool var_virtio_read_2_p3 ;
  struct virtio_device *var_group2 ;
  int tmp ;
  int ldv_s_virtio_rng_driver_virtio_driver ;
  int tmp___0 ;
  int tmp___1 ;
  int __cil_tmp10 ;

  {
  {
  LDV_IN_INTERRUPT = 1;
  ldv_initialize();
  tmp = init();
  }
  if (tmp) {
    goto ldv_final;
  } else {

  }
  ldv_s_virtio_rng_driver_virtio_driver = 0;
  {
  while (1) {
    while_continue: /* CIL Label */ ;
    {
    tmp___1 = __VERIFIER_nondet_int();
    }
    if (tmp___1) {

    } else {
      {
      __cil_tmp10 = ldv_s_virtio_rng_driver_virtio_driver == 0;
      if (! __cil_tmp10) {

      } else {
        goto while_break;
      }
      }
    }
    {
    tmp___0 = __VERIFIER_nondet_int();
    }
    if (tmp___0 == 0) {
      goto case_0;
    } else
    if (tmp___0 == 1) {
      goto case_1;
    } else
    if (tmp___0 == 2) {
      goto case_2;
    } else {
      {
      goto switch_default;
      if (0) {
        case_0: /* CIL Label */ 
        {
        virtio_cleanup(var_group1);
        }
        goto switch_break;
        case_1: /* CIL Label */ 
        {
        virtio_read(var_group1, var_virtio_read_2_p1, var_virtio_read_2_p2, var_virtio_read_2_p3);
        }
        goto switch_break;
        case_2: /* CIL Label */ 
        if (ldv_s_virtio_rng_driver_virtio_driver == 0) {
          {
          res_virtrng_probe_4 = virtrng_probe(var_group2);
          ldv_check_return_value(res_virtrng_probe_4);
          }
          if (res_virtrng_probe_4) {
            goto ldv_module_exit;
          } else {

          }
          ldv_s_virtio_rng_driver_virtio_driver = 0;
        } else {

        }
        goto switch_break;
        switch_default: /* CIL Label */ 
        goto switch_break;
      } else {
        switch_break: /* CIL Label */ ;
      }
      }
    }
  }
  while_break: /* CIL Label */ ;
  }
  ldv_module_exit: 
  {
  fini();
  }
  ldv_final: 
  {
  ldv_check_final_state();
  }
  return;
}
}
void ldv_blast_assert(void) 
{ 

  {
  ERROR: __VERIFIER_error();
}
}
extern int __VERIFIER_nondet_int(void) ;
int ldv_mutex  =    1;
int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) 
{ int nondetermined ;

  {
  if (ldv_mutex == 1) {

  } else {
    {
    ldv_blast_assert();
    }
  }
  {
  nondetermined = __VERIFIER_nondet_int();
  }
  if (nondetermined) {
    ldv_mutex = 2;
    return (0);
  } else {
    return (-4);
  }
}
}
int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) 
{ int nondetermined ;

  {
  if (ldv_mutex == 1) {

  } else {
    {
    ldv_blast_assert();
    }
  }
  {
  nondetermined = __VERIFIER_nondet_int();
  }
  if (nondetermined) {
    ldv_mutex = 2;
    return (0);
  } else {
    return (-4);
  }
}
}
int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) 
{ int atomic_value_after_dec ;

  {
  if (ldv_mutex == 1) {

  } else {
    {
    ldv_blast_assert();
    }
  }
  {
  atomic_value_after_dec = __VERIFIER_nondet_int();
  }
  if (atomic_value_after_dec == 0) {
    ldv_mutex = 2;
    return (1);
  } else {

  }
  return (0);
}
}
void mutex_lock(struct mutex *lock ) 
{ 

  {
  if (ldv_mutex == 1) {

  } else {
    {
    ldv_blast_assert();
    }
  }
  ldv_mutex = 2;
  return;
}
}
int mutex_trylock(struct mutex *lock ) 
{ int nondetermined ;

  {
  if (ldv_mutex == 1) {

  } else {
    {
    ldv_blast_assert();
    }
  }
  {
  nondetermined = __VERIFIER_nondet_int();
  }
  if (nondetermined) {
    ldv_mutex = 2;
    return (1);
  } else {
    return (0);
  }
}
}
void mutex_unlock(struct mutex *lock ) 
{ 

  {
  if (ldv_mutex == 2) {

  } else {
    {
    ldv_blast_assert();
    }
  }
  ldv_mutex = 1;
  return;
}
}
void ldv_check_final_state(void) 
{ 

  {
  if (ldv_mutex == 1) {

  } else {
    {
    ldv_blast_assert();
    }
  }
  return;
}
}
long ldv__builtin_expect(long val , long res ) 
{ 

  {
  return (val);
}
}
#include "model/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--char--hw_random--virtio-rng.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.env.c"
#include "model/common.env.c"