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