1
2
3
4#line 20 "include/asm-generic/int-ll64.h"
5typedef unsigned char __u8;
6#line 23 "include/asm-generic/int-ll64.h"
7typedef unsigned short __u16;
8#line 26 "include/asm-generic/int-ll64.h"
9typedef unsigned int __u32;
10#line 30 "include/asm-generic/int-ll64.h"
11typedef unsigned long long __u64;
12#line 43 "include/asm-generic/int-ll64.h"
13typedef unsigned char u8;
14#line 45 "include/asm-generic/int-ll64.h"
15typedef short s16;
16#line 46 "include/asm-generic/int-ll64.h"
17typedef unsigned short u16;
18#line 49 "include/asm-generic/int-ll64.h"
19typedef unsigned int u32;
20#line 51 "include/asm-generic/int-ll64.h"
21typedef long long s64;
22#line 52 "include/asm-generic/int-ll64.h"
23typedef unsigned long long u64;
24#line 14 "include/asm-generic/posix_types.h"
25typedef long __kernel_long_t;
26#line 15 "include/asm-generic/posix_types.h"
27typedef unsigned long __kernel_ulong_t;
28#line 75 "include/asm-generic/posix_types.h"
29typedef __kernel_ulong_t __kernel_size_t;
30#line 76 "include/asm-generic/posix_types.h"
31typedef __kernel_long_t __kernel_ssize_t;
32#line 91 "include/asm-generic/posix_types.h"
33typedef long long __kernel_loff_t;
34#line 21 "include/linux/types.h"
35typedef __u32 __kernel_dev_t;
36#line 24 "include/linux/types.h"
37typedef __kernel_dev_t dev_t;
38#line 27 "include/linux/types.h"
39typedef unsigned short umode_t;
40#line 38 "include/linux/types.h"
41typedef _Bool bool;
42#line 54 "include/linux/types.h"
43typedef __kernel_loff_t loff_t;
44#line 63 "include/linux/types.h"
45typedef __kernel_size_t size_t;
46#line 68 "include/linux/types.h"
47typedef __kernel_ssize_t ssize_t;
48#line 92 "include/linux/types.h"
49typedef unsigned char u_char;
50#line 95 "include/linux/types.h"
51typedef unsigned long u_long;
52#line 115 "include/linux/types.h"
53typedef __u8 uint8_t;
54#line 117 "include/linux/types.h"
55typedef __u32 uint32_t;
56#line 120 "include/linux/types.h"
57typedef __u64 uint64_t;
58#line 202 "include/linux/types.h"
59typedef unsigned int gfp_t;
60#line 203 "include/linux/types.h"
61typedef unsigned int fmode_t;
62#line 206 "include/linux/types.h"
63typedef u64 phys_addr_t;
64#line 211 "include/linux/types.h"
65typedef phys_addr_t resource_size_t;
66#line 221 "include/linux/types.h"
67struct __anonstruct_atomic_t_6 {
68 int counter ;
69};
70#line 221 "include/linux/types.h"
71typedef struct __anonstruct_atomic_t_6 atomic_t;
72#line 226 "include/linux/types.h"
73struct __anonstruct_atomic64_t_7 {
74 long counter ;
75};
76#line 226 "include/linux/types.h"
77typedef struct __anonstruct_atomic64_t_7 atomic64_t;
78#line 227 "include/linux/types.h"
79struct list_head {
80 struct list_head *next ;
81 struct list_head *prev ;
82};
83#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
84struct module;
85#line 55
86struct module;
87#line 146 "include/linux/init.h"
88typedef void (*ctor_fn_t)(void);
89#line 46 "include/linux/dynamic_debug.h"
90struct device;
91#line 46
92struct device;
93#line 57
94struct completion;
95#line 57
96struct completion;
97#line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
98struct page;
99#line 58
100struct page;
101#line 26 "include/asm-generic/getorder.h"
102struct task_struct;
103#line 26
104struct task_struct;
105#line 290 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
106struct file;
107#line 290
108struct file;
109#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
110struct arch_spinlock;
111#line 327
112struct arch_spinlock;
113#line 306 "include/linux/bitmap.h"
114struct bug_entry {
115 int bug_addr_disp ;
116 int file_disp ;
117 unsigned short line ;
118 unsigned short flags ;
119};
120#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
121struct static_key;
122#line 234
123struct static_key;
124#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
125struct kmem_cache;
126#line 23 "include/asm-generic/atomic-long.h"
127typedef atomic64_t atomic_long_t;
128#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
129typedef u16 __ticket_t;
130#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
131typedef u32 __ticketpair_t;
132#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
133struct __raw_tickets {
134 __ticket_t head ;
135 __ticket_t tail ;
136};
137#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
138union __anonunion_ldv_5907_29 {
139 __ticketpair_t head_tail ;
140 struct __raw_tickets tickets ;
141};
142#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
143struct arch_spinlock {
144 union __anonunion_ldv_5907_29 ldv_5907 ;
145};
146#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
147typedef struct arch_spinlock arch_spinlock_t;
148#line 34 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
149struct lockdep_map;
150#line 34
151struct lockdep_map;
152#line 55 "include/linux/debug_locks.h"
153struct stack_trace {
154 unsigned int nr_entries ;
155 unsigned int max_entries ;
156 unsigned long *entries ;
157 int skip ;
158};
159#line 26 "include/linux/stacktrace.h"
160struct lockdep_subclass_key {
161 char __one_byte ;
162};
163#line 53 "include/linux/lockdep.h"
164struct lock_class_key {
165 struct lockdep_subclass_key subkeys[8U] ;
166};
167#line 59 "include/linux/lockdep.h"
168struct lock_class {
169 struct list_head hash_entry ;
170 struct list_head lock_entry ;
171 struct lockdep_subclass_key *key ;
172 unsigned int subclass ;
173 unsigned int dep_gen_id ;
174 unsigned long usage_mask ;
175 struct stack_trace usage_traces[13U] ;
176 struct list_head locks_after ;
177 struct list_head locks_before ;
178 unsigned int version ;
179 unsigned long ops ;
180 char const *name ;
181 int name_version ;
182 unsigned long contention_point[4U] ;
183 unsigned long contending_point[4U] ;
184};
185#line 144 "include/linux/lockdep.h"
186struct lockdep_map {
187 struct lock_class_key *key ;
188 struct lock_class *class_cache[2U] ;
189 char const *name ;
190 int cpu ;
191 unsigned long ip ;
192};
193#line 556 "include/linux/lockdep.h"
194struct raw_spinlock {
195 arch_spinlock_t raw_lock ;
196 unsigned int magic ;
197 unsigned int owner_cpu ;
198 void *owner ;
199 struct lockdep_map dep_map ;
200};
201#line 33 "include/linux/spinlock_types.h"
202struct __anonstruct_ldv_6122_33 {
203 u8 __padding[24U] ;
204 struct lockdep_map dep_map ;
205};
206#line 33 "include/linux/spinlock_types.h"
207union __anonunion_ldv_6123_32 {
208 struct raw_spinlock rlock ;
209 struct __anonstruct_ldv_6122_33 ldv_6122 ;
210};
211#line 33 "include/linux/spinlock_types.h"
212struct spinlock {
213 union __anonunion_ldv_6123_32 ldv_6123 ;
214};
215#line 76 "include/linux/spinlock_types.h"
216typedef struct spinlock spinlock_t;
217#line 48 "include/linux/wait.h"
218struct __wait_queue_head {
219 spinlock_t lock ;
220 struct list_head task_list ;
221};
222#line 53 "include/linux/wait.h"
223typedef struct __wait_queue_head wait_queue_head_t;
224#line 670 "include/linux/mmzone.h"
225struct mutex {
226 atomic_t count ;
227 spinlock_t wait_lock ;
228 struct list_head wait_list ;
229 struct task_struct *owner ;
230 char const *name ;
231 void *magic ;
232 struct lockdep_map dep_map ;
233};
234#line 128 "include/linux/rwsem.h"
235struct completion {
236 unsigned int done ;
237 wait_queue_head_t wait ;
238};
239#line 188 "include/linux/rcupdate.h"
240struct notifier_block;
241#line 188
242struct notifier_block;
243#line 239 "include/linux/srcu.h"
244struct notifier_block {
245 int (*notifier_call)(struct notifier_block * , unsigned long , void * ) ;
246 struct notifier_block *next ;
247 int priority ;
248};
249#line 312 "include/linux/jiffies.h"
250union ktime {
251 s64 tv64 ;
252};
253#line 59 "include/linux/ktime.h"
254typedef union ktime ktime_t;
255#line 341
256struct tvec_base;
257#line 341
258struct tvec_base;
259#line 342 "include/linux/ktime.h"
260struct timer_list {
261 struct list_head entry ;
262 unsigned long expires ;
263 struct tvec_base *base ;
264 void (*function)(unsigned long ) ;
265 unsigned long data ;
266 int slack ;
267 int start_pid ;
268 void *start_site ;
269 char start_comm[16U] ;
270 struct lockdep_map lockdep_map ;
271};
272#line 302 "include/linux/timer.h"
273struct work_struct;
274#line 302
275struct work_struct;
276#line 45 "include/linux/workqueue.h"
277struct work_struct {
278 atomic_long_t data ;
279 struct list_head entry ;
280 void (*func)(struct work_struct * ) ;
281 struct lockdep_map lockdep_map ;
282};
283#line 46 "include/linux/pm.h"
284struct pm_message {
285 int event ;
286};
287#line 52 "include/linux/pm.h"
288typedef struct pm_message pm_message_t;
289#line 53 "include/linux/pm.h"
290struct dev_pm_ops {
291 int (*prepare)(struct device * ) ;
292 void (*complete)(struct device * ) ;
293 int (*suspend)(struct device * ) ;
294 int (*resume)(struct device * ) ;
295 int (*freeze)(struct device * ) ;
296 int (*thaw)(struct device * ) ;
297 int (*poweroff)(struct device * ) ;
298 int (*restore)(struct device * ) ;
299 int (*suspend_late)(struct device * ) ;
300 int (*resume_early)(struct device * ) ;
301 int (*freeze_late)(struct device * ) ;
302 int (*thaw_early)(struct device * ) ;
303 int (*poweroff_late)(struct device * ) ;
304 int (*restore_early)(struct device * ) ;
305 int (*suspend_noirq)(struct device * ) ;
306 int (*resume_noirq)(struct device * ) ;
307 int (*freeze_noirq)(struct device * ) ;
308 int (*thaw_noirq)(struct device * ) ;
309 int (*poweroff_noirq)(struct device * ) ;
310 int (*restore_noirq)(struct device * ) ;
311 int (*runtime_suspend)(struct device * ) ;
312 int (*runtime_resume)(struct device * ) ;
313 int (*runtime_idle)(struct device * ) ;
314};
315#line 289
316enum rpm_status {
317 RPM_ACTIVE = 0,
318 RPM_RESUMING = 1,
319 RPM_SUSPENDED = 2,
320 RPM_SUSPENDING = 3
321} ;
322#line 296
323enum rpm_request {
324 RPM_REQ_NONE = 0,
325 RPM_REQ_IDLE = 1,
326 RPM_REQ_SUSPEND = 2,
327 RPM_REQ_AUTOSUSPEND = 3,
328 RPM_REQ_RESUME = 4
329} ;
330#line 304
331struct wakeup_source;
332#line 304
333struct wakeup_source;
334#line 494 "include/linux/pm.h"
335struct pm_subsys_data {
336 spinlock_t lock ;
337 unsigned int refcount ;
338};
339#line 499
340struct dev_pm_qos_request;
341#line 499
342struct pm_qos_constraints;
343#line 499 "include/linux/pm.h"
344struct dev_pm_info {
345 pm_message_t power_state ;
346 unsigned char can_wakeup : 1 ;
347 unsigned char async_suspend : 1 ;
348 bool is_prepared ;
349 bool is_suspended ;
350 bool ignore_children ;
351 spinlock_t lock ;
352 struct list_head entry ;
353 struct completion completion ;
354 struct wakeup_source *wakeup ;
355 bool wakeup_path ;
356 struct timer_list suspend_timer ;
357 unsigned long timer_expires ;
358 struct work_struct work ;
359 wait_queue_head_t wait_queue ;
360 atomic_t usage_count ;
361 atomic_t child_count ;
362 unsigned char disable_depth : 3 ;
363 unsigned char idle_notification : 1 ;
364 unsigned char request_pending : 1 ;
365 unsigned char deferred_resume : 1 ;
366 unsigned char run_wake : 1 ;
367 unsigned char runtime_auto : 1 ;
368 unsigned char no_callbacks : 1 ;
369 unsigned char irq_safe : 1 ;
370 unsigned char use_autosuspend : 1 ;
371 unsigned char timer_autosuspends : 1 ;
372 enum rpm_request request ;
373 enum rpm_status runtime_status ;
374 int runtime_error ;
375 int autosuspend_delay ;
376 unsigned long last_busy ;
377 unsigned long active_jiffies ;
378 unsigned long suspended_jiffies ;
379 unsigned long accounting_timestamp ;
380 ktime_t suspend_time ;
381 s64 max_time_suspended_ns ;
382 struct dev_pm_qos_request *pq_req ;
383 struct pm_subsys_data *subsys_data ;
384 struct pm_qos_constraints *constraints ;
385};
386#line 558 "include/linux/pm.h"
387struct dev_pm_domain {
388 struct dev_pm_ops ops ;
389};
390#line 18 "include/asm-generic/pci_iomap.h"
391struct vm_area_struct;
392#line 18
393struct vm_area_struct;
394#line 18 "include/linux/elf.h"
395typedef __u64 Elf64_Addr;
396#line 19 "include/linux/elf.h"
397typedef __u16 Elf64_Half;
398#line 23 "include/linux/elf.h"
399typedef __u32 Elf64_Word;
400#line 24 "include/linux/elf.h"
401typedef __u64 Elf64_Xword;
402#line 193 "include/linux/elf.h"
403struct elf64_sym {
404 Elf64_Word st_name ;
405 unsigned char st_info ;
406 unsigned char st_other ;
407 Elf64_Half st_shndx ;
408 Elf64_Addr st_value ;
409 Elf64_Xword st_size ;
410};
411#line 201 "include/linux/elf.h"
412typedef struct elf64_sym Elf64_Sym;
413#line 445
414struct sock;
415#line 445
416struct sock;
417#line 446
418struct kobject;
419#line 446
420struct kobject;
421#line 447
422enum kobj_ns_type {
423 KOBJ_NS_TYPE_NONE = 0,
424 KOBJ_NS_TYPE_NET = 1,
425 KOBJ_NS_TYPES = 2
426} ;
427#line 453 "include/linux/elf.h"
428struct kobj_ns_type_operations {
429 enum kobj_ns_type type ;
430 void *(*grab_current_ns)(void) ;
431 void const *(*netlink_ns)(struct sock * ) ;
432 void const *(*initial_ns)(void) ;
433 void (*drop_ns)(void * ) ;
434};
435#line 57 "include/linux/kobject_ns.h"
436struct attribute {
437 char const *name ;
438 umode_t mode ;
439 struct lock_class_key *key ;
440 struct lock_class_key skey ;
441};
442#line 33 "include/linux/sysfs.h"
443struct attribute_group {
444 char const *name ;
445 umode_t (*is_visible)(struct kobject * , struct attribute * , int ) ;
446 struct attribute **attrs ;
447};
448#line 62 "include/linux/sysfs.h"
449struct bin_attribute {
450 struct attribute attr ;
451 size_t size ;
452 void *private ;
453 ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
454 loff_t , size_t ) ;
455 ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
456 loff_t , size_t ) ;
457 int (*mmap)(struct file * , struct kobject * , struct bin_attribute * , struct vm_area_struct * ) ;
458};
459#line 98 "include/linux/sysfs.h"
460struct sysfs_ops {
461 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
462 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
463 void const *(*namespace)(struct kobject * , struct attribute const * ) ;
464};
465#line 117
466struct sysfs_dirent;
467#line 117
468struct sysfs_dirent;
469#line 182 "include/linux/sysfs.h"
470struct kref {
471 atomic_t refcount ;
472};
473#line 49 "include/linux/kobject.h"
474struct kset;
475#line 49
476struct kobj_type;
477#line 49 "include/linux/kobject.h"
478struct kobject {
479 char const *name ;
480 struct list_head entry ;
481 struct kobject *parent ;
482 struct kset *kset ;
483 struct kobj_type *ktype ;
484 struct sysfs_dirent *sd ;
485 struct kref kref ;
486 unsigned char state_initialized : 1 ;
487 unsigned char state_in_sysfs : 1 ;
488 unsigned char state_add_uevent_sent : 1 ;
489 unsigned char state_remove_uevent_sent : 1 ;
490 unsigned char uevent_suppress : 1 ;
491};
492#line 107 "include/linux/kobject.h"
493struct kobj_type {
494 void (*release)(struct kobject * ) ;
495 struct sysfs_ops const *sysfs_ops ;
496 struct attribute **default_attrs ;
497 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject * ) ;
498 void const *(*namespace)(struct kobject * ) ;
499};
500#line 115 "include/linux/kobject.h"
501struct kobj_uevent_env {
502 char *envp[32U] ;
503 int envp_idx ;
504 char buf[2048U] ;
505 int buflen ;
506};
507#line 122 "include/linux/kobject.h"
508struct kset_uevent_ops {
509 int (* const filter)(struct kset * , struct kobject * ) ;
510 char const *(* const name)(struct kset * , struct kobject * ) ;
511 int (* const uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
512};
513#line 139 "include/linux/kobject.h"
514struct kset {
515 struct list_head list ;
516 spinlock_t list_lock ;
517 struct kobject kobj ;
518 struct kset_uevent_ops const *uevent_ops ;
519};
520#line 215
521struct kernel_param;
522#line 215
523struct kernel_param;
524#line 216 "include/linux/kobject.h"
525struct kernel_param_ops {
526 int (*set)(char const * , struct kernel_param const * ) ;
527 int (*get)(char * , struct kernel_param const * ) ;
528 void (*free)(void * ) ;
529};
530#line 49 "include/linux/moduleparam.h"
531struct kparam_string;
532#line 49
533struct kparam_array;
534#line 49 "include/linux/moduleparam.h"
535union __anonunion_ldv_13363_134 {
536 void *arg ;
537 struct kparam_string const *str ;
538 struct kparam_array const *arr ;
539};
540#line 49 "include/linux/moduleparam.h"
541struct kernel_param {
542 char const *name ;
543 struct kernel_param_ops const *ops ;
544 u16 perm ;
545 s16 level ;
546 union __anonunion_ldv_13363_134 ldv_13363 ;
547};
548#line 61 "include/linux/moduleparam.h"
549struct kparam_string {
550 unsigned int maxlen ;
551 char *string ;
552};
553#line 67 "include/linux/moduleparam.h"
554struct kparam_array {
555 unsigned int max ;
556 unsigned int elemsize ;
557 unsigned int *num ;
558 struct kernel_param_ops const *ops ;
559 void *elem ;
560};
561#line 458 "include/linux/moduleparam.h"
562struct static_key {
563 atomic_t enabled ;
564};
565#line 225 "include/linux/jump_label.h"
566struct tracepoint;
567#line 225
568struct tracepoint;
569#line 226 "include/linux/jump_label.h"
570struct tracepoint_func {
571 void *func ;
572 void *data ;
573};
574#line 29 "include/linux/tracepoint.h"
575struct tracepoint {
576 char const *name ;
577 struct static_key key ;
578 void (*regfunc)(void) ;
579 void (*unregfunc)(void) ;
580 struct tracepoint_func *funcs ;
581};
582#line 86 "include/linux/tracepoint.h"
583struct kernel_symbol {
584 unsigned long value ;
585 char const *name ;
586};
587#line 27 "include/linux/export.h"
588struct mod_arch_specific {
589
590};
591#line 34 "include/linux/module.h"
592struct module_param_attrs;
593#line 34 "include/linux/module.h"
594struct module_kobject {
595 struct kobject kobj ;
596 struct module *mod ;
597 struct kobject *drivers_dir ;
598 struct module_param_attrs *mp ;
599};
600#line 43 "include/linux/module.h"
601struct module_attribute {
602 struct attribute attr ;
603 ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
604 ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const * ,
605 size_t ) ;
606 void (*setup)(struct module * , char const * ) ;
607 int (*test)(struct module * ) ;
608 void (*free)(struct module * ) ;
609};
610#line 69
611struct exception_table_entry;
612#line 69
613struct exception_table_entry;
614#line 198
615enum module_state {
616 MODULE_STATE_LIVE = 0,
617 MODULE_STATE_COMING = 1,
618 MODULE_STATE_GOING = 2
619} ;
620#line 204 "include/linux/module.h"
621struct module_ref {
622 unsigned long incs ;
623 unsigned long decs ;
624};
625#line 219
626struct module_sect_attrs;
627#line 219
628struct module_notes_attrs;
629#line 219
630struct ftrace_event_call;
631#line 219 "include/linux/module.h"
632struct module {
633 enum module_state state ;
634 struct list_head list ;
635 char name[56U] ;
636 struct module_kobject mkobj ;
637 struct module_attribute *modinfo_attrs ;
638 char const *version ;
639 char const *srcversion ;
640 struct kobject *holders_dir ;
641 struct kernel_symbol const *syms ;
642 unsigned long const *crcs ;
643 unsigned int num_syms ;
644 struct kernel_param *kp ;
645 unsigned int num_kp ;
646 unsigned int num_gpl_syms ;
647 struct kernel_symbol const *gpl_syms ;
648 unsigned long const *gpl_crcs ;
649 struct kernel_symbol const *unused_syms ;
650 unsigned long const *unused_crcs ;
651 unsigned int num_unused_syms ;
652 unsigned int num_unused_gpl_syms ;
653 struct kernel_symbol const *unused_gpl_syms ;
654 unsigned long const *unused_gpl_crcs ;
655 struct kernel_symbol const *gpl_future_syms ;
656 unsigned long const *gpl_future_crcs ;
657 unsigned int num_gpl_future_syms ;
658 unsigned int num_exentries ;
659 struct exception_table_entry *extable ;
660 int (*init)(void) ;
661 void *module_init ;
662 void *module_core ;
663 unsigned int init_size ;
664 unsigned int core_size ;
665 unsigned int init_text_size ;
666 unsigned int core_text_size ;
667 unsigned int init_ro_size ;
668 unsigned int core_ro_size ;
669 struct mod_arch_specific arch ;
670 unsigned int taints ;
671 unsigned int num_bugs ;
672 struct list_head bug_list ;
673 struct bug_entry *bug_table ;
674 Elf64_Sym *symtab ;
675 Elf64_Sym *core_symtab ;
676 unsigned int num_symtab ;
677 unsigned int core_num_syms ;
678 char *strtab ;
679 char *core_strtab ;
680 struct module_sect_attrs *sect_attrs ;
681 struct module_notes_attrs *notes_attrs ;
682 char *args ;
683 void *percpu ;
684 unsigned int percpu_size ;
685 unsigned int num_tracepoints ;
686 struct tracepoint * const *tracepoints_ptrs ;
687 unsigned int num_trace_bprintk_fmt ;
688 char const **trace_bprintk_fmt_start ;
689 struct ftrace_event_call **trace_events ;
690 unsigned int num_trace_events ;
691 struct list_head source_list ;
692 struct list_head target_list ;
693 struct task_struct *waiter ;
694 void (*exit)(void) ;
695 struct module_ref *refptr ;
696 ctor_fn_t (**ctors)(void) ;
697 unsigned int num_ctors ;
698};
699#line 88 "include/linux/kmemleak.h"
700struct kmem_cache_cpu {
701 void **freelist ;
702 unsigned long tid ;
703 struct page *page ;
704 struct page *partial ;
705 int node ;
706 unsigned int stat[26U] ;
707};
708#line 55 "include/linux/slub_def.h"
709struct kmem_cache_node {
710 spinlock_t list_lock ;
711 unsigned long nr_partial ;
712 struct list_head partial ;
713 atomic_long_t nr_slabs ;
714 atomic_long_t total_objects ;
715 struct list_head full ;
716};
717#line 66 "include/linux/slub_def.h"
718struct kmem_cache_order_objects {
719 unsigned long x ;
720};
721#line 76 "include/linux/slub_def.h"
722struct kmem_cache {
723 struct kmem_cache_cpu *cpu_slab ;
724 unsigned long flags ;
725 unsigned long min_partial ;
726 int size ;
727 int objsize ;
728 int offset ;
729 int cpu_partial ;
730 struct kmem_cache_order_objects oo ;
731 struct kmem_cache_order_objects max ;
732 struct kmem_cache_order_objects min ;
733 gfp_t allocflags ;
734 int refcount ;
735 void (*ctor)(void * ) ;
736 int inuse ;
737 int align ;
738 int reserved ;
739 char const *name ;
740 struct list_head list ;
741 struct kobject kobj ;
742 int remote_node_defrag_ratio ;
743 struct kmem_cache_node *node[1024U] ;
744};
745#line 21 "include/linux/uio.h"
746struct kvec {
747 void *iov_base ;
748 size_t iov_len ;
749};
750#line 54
751struct klist_node;
752#line 54
753struct klist_node;
754#line 37 "include/linux/klist.h"
755struct klist_node {
756 void *n_klist ;
757 struct list_head n_node ;
758 struct kref n_ref ;
759};
760#line 67
761struct dma_map_ops;
762#line 67 "include/linux/klist.h"
763struct dev_archdata {
764 void *acpi_handle ;
765 struct dma_map_ops *dma_ops ;
766 void *iommu ;
767};
768#line 17 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
769struct device_private;
770#line 17
771struct device_private;
772#line 18
773struct device_driver;
774#line 18
775struct device_driver;
776#line 19
777struct driver_private;
778#line 19
779struct driver_private;
780#line 20
781struct class;
782#line 20
783struct class;
784#line 21
785struct subsys_private;
786#line 21
787struct subsys_private;
788#line 22
789struct bus_type;
790#line 22
791struct bus_type;
792#line 23
793struct device_node;
794#line 23
795struct device_node;
796#line 24
797struct iommu_ops;
798#line 24
799struct iommu_ops;
800#line 25 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
801struct bus_attribute {
802 struct attribute attr ;
803 ssize_t (*show)(struct bus_type * , char * ) ;
804 ssize_t (*store)(struct bus_type * , char const * , size_t ) ;
805};
806#line 51 "include/linux/device.h"
807struct device_attribute;
808#line 51
809struct driver_attribute;
810#line 51 "include/linux/device.h"
811struct bus_type {
812 char const *name ;
813 char const *dev_name ;
814 struct device *dev_root ;
815 struct bus_attribute *bus_attrs ;
816 struct device_attribute *dev_attrs ;
817 struct driver_attribute *drv_attrs ;
818 int (*match)(struct device * , struct device_driver * ) ;
819 int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
820 int (*probe)(struct device * ) ;
821 int (*remove)(struct device * ) ;
822 void (*shutdown)(struct device * ) ;
823 int (*suspend)(struct device * , pm_message_t ) ;
824 int (*resume)(struct device * ) ;
825 struct dev_pm_ops const *pm ;
826 struct iommu_ops *iommu_ops ;
827 struct subsys_private *p ;
828};
829#line 125
830struct device_type;
831#line 182
832struct of_device_id;
833#line 182 "include/linux/device.h"
834struct device_driver {
835 char const *name ;
836 struct bus_type *bus ;
837 struct module *owner ;
838 char const *mod_name ;
839 bool suppress_bind_attrs ;
840 struct of_device_id const *of_match_table ;
841 int (*probe)(struct device * ) ;
842 int (*remove)(struct device * ) ;
843 void (*shutdown)(struct device * ) ;
844 int (*suspend)(struct device * , pm_message_t ) ;
845 int (*resume)(struct device * ) ;
846 struct attribute_group const **groups ;
847 struct dev_pm_ops const *pm ;
848 struct driver_private *p ;
849};
850#line 245 "include/linux/device.h"
851struct driver_attribute {
852 struct attribute attr ;
853 ssize_t (*show)(struct device_driver * , char * ) ;
854 ssize_t (*store)(struct device_driver * , char const * , size_t ) ;
855};
856#line 299
857struct class_attribute;
858#line 299 "include/linux/device.h"
859struct class {
860 char const *name ;
861 struct module *owner ;
862 struct class_attribute *class_attrs ;
863 struct device_attribute *dev_attrs ;
864 struct bin_attribute *dev_bin_attrs ;
865 struct kobject *dev_kobj ;
866 int (*dev_uevent)(struct device * , struct kobj_uevent_env * ) ;
867 char *(*devnode)(struct device * , umode_t * ) ;
868 void (*class_release)(struct class * ) ;
869 void (*dev_release)(struct device * ) ;
870 int (*suspend)(struct device * , pm_message_t ) ;
871 int (*resume)(struct device * ) ;
872 struct kobj_ns_type_operations const *ns_type ;
873 void const *(*namespace)(struct device * ) ;
874 struct dev_pm_ops const *pm ;
875 struct subsys_private *p ;
876};
877#line 394 "include/linux/device.h"
878struct class_attribute {
879 struct attribute attr ;
880 ssize_t (*show)(struct class * , struct class_attribute * , char * ) ;
881 ssize_t (*store)(struct class * , struct class_attribute * , char const * , size_t ) ;
882 void const *(*namespace)(struct class * , struct class_attribute const * ) ;
883};
884#line 447 "include/linux/device.h"
885struct device_type {
886 char const *name ;
887 struct attribute_group const **groups ;
888 int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
889 char *(*devnode)(struct device * , umode_t * ) ;
890 void (*release)(struct device * ) ;
891 struct dev_pm_ops const *pm ;
892};
893#line 474 "include/linux/device.h"
894struct device_attribute {
895 struct attribute attr ;
896 ssize_t (*show)(struct device * , struct device_attribute * , char * ) ;
897 ssize_t (*store)(struct device * , struct device_attribute * , char const * ,
898 size_t ) ;
899};
900#line 557 "include/linux/device.h"
901struct device_dma_parameters {
902 unsigned int max_segment_size ;
903 unsigned long segment_boundary_mask ;
904};
905#line 567
906struct dma_coherent_mem;
907#line 567 "include/linux/device.h"
908struct device {
909 struct device *parent ;
910 struct device_private *p ;
911 struct kobject kobj ;
912 char const *init_name ;
913 struct device_type const *type ;
914 struct mutex mutex ;
915 struct bus_type *bus ;
916 struct device_driver *driver ;
917 void *platform_data ;
918 struct dev_pm_info power ;
919 struct dev_pm_domain *pm_domain ;
920 int numa_node ;
921 u64 *dma_mask ;
922 u64 coherent_dma_mask ;
923 struct device_dma_parameters *dma_parms ;
924 struct list_head dma_pools ;
925 struct dma_coherent_mem *dma_mem ;
926 struct dev_archdata archdata ;
927 struct device_node *of_node ;
928 dev_t devt ;
929 u32 id ;
930 spinlock_t devres_lock ;
931 struct list_head devres_head ;
932 struct klist_node knode_class ;
933 struct class *class ;
934 struct attribute_group const **groups ;
935 void (*release)(struct device * ) ;
936};
937#line 681 "include/linux/device.h"
938struct wakeup_source {
939 char const *name ;
940 struct list_head entry ;
941 spinlock_t lock ;
942 struct timer_list timer ;
943 unsigned long timer_expires ;
944 ktime_t total_time ;
945 ktime_t max_time ;
946 ktime_t last_time ;
947 unsigned long event_count ;
948 unsigned long active_count ;
949 unsigned long relax_count ;
950 unsigned long hit_count ;
951 unsigned char active : 1 ;
952};
953#line 142 "include/mtd/mtd-abi.h"
954struct otp_info {
955 __u32 start ;
956 __u32 length ;
957 __u32 locked ;
958};
959#line 216 "include/mtd/mtd-abi.h"
960struct nand_oobfree {
961 __u32 offset ;
962 __u32 length ;
963};
964#line 238 "include/mtd/mtd-abi.h"
965struct mtd_ecc_stats {
966 __u32 corrected ;
967 __u32 failed ;
968 __u32 badblocks ;
969 __u32 bbtblocks ;
970};
971#line 260
972struct mtd_info;
973#line 260 "include/mtd/mtd-abi.h"
974struct erase_info {
975 struct mtd_info *mtd ;
976 uint64_t addr ;
977 uint64_t len ;
978 uint64_t fail_addr ;
979 u_long time ;
980 u_long retries ;
981 unsigned int dev ;
982 unsigned int cell ;
983 void (*callback)(struct erase_info * ) ;
984 u_long priv ;
985 u_char state ;
986 struct erase_info *next ;
987};
988#line 62 "include/linux/mtd/mtd.h"
989struct mtd_erase_region_info {
990 uint64_t offset ;
991 uint32_t erasesize ;
992 uint32_t numblocks ;
993 unsigned long *lockmap ;
994};
995#line 69 "include/linux/mtd/mtd.h"
996struct mtd_oob_ops {
997 unsigned int mode ;
998 size_t len ;
999 size_t retlen ;
1000 size_t ooblen ;
1001 size_t oobretlen ;
1002 uint32_t ooboffs ;
1003 uint8_t *datbuf ;
1004 uint8_t *oobbuf ;
1005};
1006#line 99 "include/linux/mtd/mtd.h"
1007struct nand_ecclayout {
1008 __u32 eccbytes ;
1009 __u32 eccpos[448U] ;
1010 __u32 oobavail ;
1011 struct nand_oobfree oobfree[32U] ;
1012};
1013#line 114
1014struct backing_dev_info;
1015#line 114 "include/linux/mtd/mtd.h"
1016struct mtd_info {
1017 u_char type ;
1018 uint32_t flags ;
1019 uint64_t size ;
1020 uint32_t erasesize ;
1021 uint32_t writesize ;
1022 uint32_t writebufsize ;
1023 uint32_t oobsize ;
1024 uint32_t oobavail ;
1025 unsigned int erasesize_shift ;
1026 unsigned int writesize_shift ;
1027 unsigned int erasesize_mask ;
1028 unsigned int writesize_mask ;
1029 char const *name ;
1030 int index ;
1031 struct nand_ecclayout *ecclayout ;
1032 unsigned int ecc_strength ;
1033 int numeraseregions ;
1034 struct mtd_erase_region_info *eraseregions ;
1035 int (*_erase)(struct mtd_info * , struct erase_info * ) ;
1036 int (*_point)(struct mtd_info * , loff_t , size_t , size_t * , void ** , resource_size_t * ) ;
1037 int (*_unpoint)(struct mtd_info * , loff_t , size_t ) ;
1038 unsigned long (*_get_unmapped_area)(struct mtd_info * , unsigned long , unsigned long ,
1039 unsigned long ) ;
1040 int (*_read)(struct mtd_info * , loff_t , size_t , size_t * , u_char * ) ;
1041 int (*_write)(struct mtd_info * , loff_t , size_t , size_t * , u_char const * ) ;
1042 int (*_panic_write)(struct mtd_info * , loff_t , size_t , size_t * , u_char const * ) ;
1043 int (*_read_oob)(struct mtd_info * , loff_t , struct mtd_oob_ops * ) ;
1044 int (*_write_oob)(struct mtd_info * , loff_t , struct mtd_oob_ops * ) ;
1045 int (*_get_fact_prot_info)(struct mtd_info * , struct otp_info * , size_t ) ;
1046 int (*_read_fact_prot_reg)(struct mtd_info * , loff_t , size_t , size_t * , u_char * ) ;
1047 int (*_get_user_prot_info)(struct mtd_info * , struct otp_info * , size_t ) ;
1048 int (*_read_user_prot_reg)(struct mtd_info * , loff_t , size_t , size_t * , u_char * ) ;
1049 int (*_write_user_prot_reg)(struct mtd_info * , loff_t , size_t , size_t * ,
1050 u_char * ) ;
1051 int (*_lock_user_prot_reg)(struct mtd_info * , loff_t , size_t ) ;
1052 int (*_writev)(struct mtd_info * , struct kvec const * , unsigned long , loff_t ,
1053 size_t * ) ;
1054 void (*_sync)(struct mtd_info * ) ;
1055 int (*_lock)(struct mtd_info * , loff_t , uint64_t ) ;
1056 int (*_unlock)(struct mtd_info * , loff_t , uint64_t ) ;
1057 int (*_is_locked)(struct mtd_info * , loff_t , uint64_t ) ;
1058 int (*_block_isbad)(struct mtd_info * , loff_t ) ;
1059 int (*_block_markbad)(struct mtd_info * , loff_t ) ;
1060 int (*_suspend)(struct mtd_info * ) ;
1061 void (*_resume)(struct mtd_info * ) ;
1062 int (*_get_device)(struct mtd_info * ) ;
1063 void (*_put_device)(struct mtd_info * ) ;
1064 struct backing_dev_info *backing_dev_info ;
1065 struct notifier_block reboot_notifier ;
1066 struct mtd_ecc_stats ecc_stats ;
1067 int subpage_sft ;
1068 void *priv ;
1069 struct module *owner ;
1070 struct device dev ;
1071 int usecount ;
1072};
1073#line 401
1074struct hd_geometry;
1075#line 401
1076struct hd_geometry;
1077#line 402
1078struct mtd_blktrans_ops;
1079#line 402
1080struct mtd_blktrans_ops;
1081#line 404
1082struct gendisk;
1083#line 404
1084struct request_queue;
1085#line 404 "include/linux/mtd/mtd.h"
1086struct mtd_blktrans_dev {
1087 struct mtd_blktrans_ops *tr ;
1088 struct list_head list ;
1089 struct mtd_info *mtd ;
1090 struct mutex lock ;
1091 int devnum ;
1092 bool bg_stop ;
1093 unsigned long size ;
1094 int readonly ;
1095 int open ;
1096 struct kref ref ;
1097 struct gendisk *disk ;
1098 struct attribute_group *disk_attributes ;
1099 struct task_struct *thread ;
1100 struct request_queue *rq ;
1101 spinlock_t queue_lock ;
1102 void *priv ;
1103 fmode_t file_mode ;
1104};
1105#line 52 "include/linux/mtd/blktrans.h"
1106struct mtd_blktrans_ops {
1107 char *name ;
1108 int major ;
1109 int part_bits ;
1110 int blksize ;
1111 int blkshift ;
1112 int (*readsect)(struct mtd_blktrans_dev * , unsigned long , char * ) ;
1113 int (*writesect)(struct mtd_blktrans_dev * , unsigned long , char * ) ;
1114 int (*discard)(struct mtd_blktrans_dev * , unsigned long , unsigned int ) ;
1115 void (*background)(struct mtd_blktrans_dev * ) ;
1116 int (*getgeo)(struct mtd_blktrans_dev * , struct hd_geometry * ) ;
1117 int (*flush)(struct mtd_blktrans_dev * ) ;
1118 int (*open)(struct mtd_blktrans_dev * ) ;
1119 int (*release)(struct mtd_blktrans_dev * ) ;
1120 void (*add_mtd)(struct mtd_blktrans_ops * , struct mtd_info * ) ;
1121 void (*remove_dev)(struct mtd_blktrans_dev * ) ;
1122 struct list_head devs ;
1123 struct list_head list ;
1124 struct module *owner ;
1125};
1126#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11885/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdblock_ro.c.p"
1127void ldv_spin_lock(void) ;
1128#line 3
1129void ldv_spin_unlock(void) ;
1130#line 4
1131int ldv_spin_trylock(void) ;
1132#line 26 "include/linux/export.h"
1133extern struct module __this_module ;
1134#line 161 "include/linux/slab.h"
1135extern void kfree(void const * ) ;
1136#line 220 "include/linux/slub_def.h"
1137extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t ) ;
1138#line 223
1139void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
1140#line 353 "include/linux/slab.h"
1141__inline static void *kzalloc(size_t size , gfp_t flags ) ;
1142#line 10 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11885/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdblock_ro.c.p"
1143extern void *__VERIFIER_nondet_pointer(void) ;
1144#line 11
1145void ldv_check_alloc_flags(gfp_t flags ) ;
1146#line 12
1147void ldv_check_alloc_nonatomic(void) ;
1148#line 14
1149struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
1150#line 252 "include/linux/mtd/mtd.h"
1151extern int mtd_read(struct mtd_info * , loff_t , size_t , size_t * , u_char * ) ;
1152#line 254
1153extern int mtd_write(struct mtd_info * , loff_t , size_t , size_t * , u_char const * ) ;
1154#line 87 "include/linux/mtd/blktrans.h"
1155extern int register_mtd_blktrans(struct mtd_blktrans_ops * ) ;
1156#line 88
1157extern int deregister_mtd_blktrans(struct mtd_blktrans_ops * ) ;
1158#line 89
1159extern int add_mtd_blktrans_dev(struct mtd_blktrans_dev * ) ;
1160#line 90
1161extern int del_mtd_blktrans_dev(struct mtd_blktrans_dev * ) ;
1162#line 43 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11885/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdblock_ro.c.p"
1163static int mtdblock_readsect(struct mtd_blktrans_dev *dev , unsigned long block ,
1164 char *buf )
1165{ size_t retlen ;
1166 int tmp ;
1167 unsigned long __cil_tmp6 ;
1168 unsigned long __cil_tmp7 ;
1169 struct mtd_info *__cil_tmp8 ;
1170 unsigned long __cil_tmp9 ;
1171 loff_t __cil_tmp10 ;
1172 u_char *__cil_tmp11 ;
1173
1174 {
1175 {
1176#line 48
1177 __cil_tmp6 = (unsigned long )dev;
1178#line 48
1179 __cil_tmp7 = __cil_tmp6 + 24;
1180#line 48
1181 __cil_tmp8 = *((struct mtd_info **)__cil_tmp7);
1182#line 48
1183 __cil_tmp9 = block * 512UL;
1184#line 48
1185 __cil_tmp10 = (loff_t )__cil_tmp9;
1186#line 48
1187 __cil_tmp11 = (u_char *)buf;
1188#line 48
1189 tmp = mtd_read(__cil_tmp8, __cil_tmp10, 512UL, & retlen, __cil_tmp11);
1190 }
1191#line 48
1192 if (tmp != 0) {
1193#line 49
1194 return (1);
1195 } else {
1196
1197 }
1198#line 50
1199 return (0);
1200}
1201}
1202#line 53 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11885/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdblock_ro.c.p"
1203static int mtdblock_writesect(struct mtd_blktrans_dev *dev , unsigned long block ,
1204 char *buf )
1205{ size_t retlen ;
1206 int tmp ;
1207 unsigned long __cil_tmp6 ;
1208 unsigned long __cil_tmp7 ;
1209 struct mtd_info *__cil_tmp8 ;
1210 unsigned long __cil_tmp9 ;
1211 loff_t __cil_tmp10 ;
1212 u_char const *__cil_tmp11 ;
1213
1214 {
1215 {
1216#line 58
1217 __cil_tmp6 = (unsigned long )dev;
1218#line 58
1219 __cil_tmp7 = __cil_tmp6 + 24;
1220#line 58
1221 __cil_tmp8 = *((struct mtd_info **)__cil_tmp7);
1222#line 58
1223 __cil_tmp9 = block * 512UL;
1224#line 58
1225 __cil_tmp10 = (loff_t )__cil_tmp9;
1226#line 58
1227 __cil_tmp11 = (u_char const *)buf;
1228#line 58
1229 tmp = mtd_write(__cil_tmp8, __cil_tmp10, 512UL, & retlen, __cil_tmp11);
1230 }
1231#line 58
1232 if (tmp != 0) {
1233#line 59
1234 return (1);
1235 } else {
1236
1237 }
1238#line 60
1239 return (0);
1240}
1241}
1242#line 63 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11885/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdblock_ro.c.p"
1243static void mtdblock_add_mtd(struct mtd_blktrans_ops *tr , struct mtd_info *mtd )
1244{ struct mtd_blktrans_dev *dev ;
1245 void *tmp ;
1246 int tmp___0 ;
1247 struct mtd_blktrans_dev *__cil_tmp6 ;
1248 unsigned long __cil_tmp7 ;
1249 unsigned long __cil_tmp8 ;
1250 unsigned long __cil_tmp9 ;
1251 unsigned long __cil_tmp10 ;
1252 unsigned long __cil_tmp11 ;
1253 unsigned long __cil_tmp12 ;
1254 unsigned long __cil_tmp13 ;
1255 unsigned long __cil_tmp14 ;
1256 unsigned long __cil_tmp15 ;
1257 unsigned long __cil_tmp16 ;
1258 unsigned long __cil_tmp17 ;
1259 unsigned long __cil_tmp18 ;
1260 uint64_t __cil_tmp19 ;
1261 uint64_t __cil_tmp20 ;
1262 unsigned long __cil_tmp21 ;
1263 unsigned long __cil_tmp22 ;
1264 void const *__cil_tmp23 ;
1265
1266 {
1267 {
1268#line 65
1269 tmp = kzalloc(352UL, 208U);
1270#line 65
1271 dev = (struct mtd_blktrans_dev *)tmp;
1272 }
1273 {
1274#line 67
1275 __cil_tmp6 = (struct mtd_blktrans_dev *)0;
1276#line 67
1277 __cil_tmp7 = (unsigned long )__cil_tmp6;
1278#line 67
1279 __cil_tmp8 = (unsigned long )dev;
1280#line 67
1281 if (__cil_tmp8 == __cil_tmp7) {
1282#line 68
1283 return;
1284 } else {
1285
1286 }
1287 }
1288 {
1289#line 70
1290 __cil_tmp9 = (unsigned long )dev;
1291#line 70
1292 __cil_tmp10 = __cil_tmp9 + 24;
1293#line 70
1294 *((struct mtd_info **)__cil_tmp10) = mtd;
1295#line 71
1296 __cil_tmp11 = (unsigned long )dev;
1297#line 71
1298 __cil_tmp12 = __cil_tmp11 + 200;
1299#line 71
1300 __cil_tmp13 = (unsigned long )mtd;
1301#line 71
1302 __cil_tmp14 = __cil_tmp13 + 64;
1303#line 71
1304 *((int *)__cil_tmp12) = *((int *)__cil_tmp14);
1305#line 73
1306 __cil_tmp15 = (unsigned long )dev;
1307#line 73
1308 __cil_tmp16 = __cil_tmp15 + 208;
1309#line 73
1310 __cil_tmp17 = (unsigned long )mtd;
1311#line 73
1312 __cil_tmp18 = __cil_tmp17 + 8;
1313#line 73
1314 __cil_tmp19 = *((uint64_t *)__cil_tmp18);
1315#line 73
1316 __cil_tmp20 = __cil_tmp19 >> 9;
1317#line 73
1318 *((unsigned long *)__cil_tmp16) = (unsigned long )__cil_tmp20;
1319#line 74
1320 *((struct mtd_blktrans_ops **)dev) = tr;
1321#line 75
1322 __cil_tmp21 = (unsigned long )dev;
1323#line 75
1324 __cil_tmp22 = __cil_tmp21 + 216;
1325#line 75
1326 *((int *)__cil_tmp22) = 1;
1327#line 77
1328 tmp___0 = add_mtd_blktrans_dev(dev);
1329 }
1330#line 77
1331 if (tmp___0 != 0) {
1332 {
1333#line 78
1334 __cil_tmp23 = (void const *)dev;
1335#line 78
1336 kfree(__cil_tmp23);
1337 }
1338 } else {
1339
1340 }
1341#line 79
1342 return;
1343}
1344}
1345#line 81 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11885/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdblock_ro.c.p"
1346static void mtdblock_remove_dev(struct mtd_blktrans_dev *dev )
1347{
1348
1349 {
1350 {
1351#line 83
1352 del_mtd_blktrans_dev(dev);
1353 }
1354#line 84
1355 return;
1356}
1357}
1358#line 86 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11885/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdblock_ro.c.p"
1359static struct mtd_blktrans_ops mtdblock_tr =
1360#line 86
1361 {(char *)"mtdblock", 31, 0, 512, 0, & mtdblock_readsect, & mtdblock_writesect,
1362 (int (*)(struct mtd_blktrans_dev * , unsigned long , unsigned int ))0, (void (*)(struct mtd_blktrans_dev * ))0,
1363 (int (*)(struct mtd_blktrans_dev * , struct hd_geometry * ))0, (int (*)(struct mtd_blktrans_dev * ))0,
1364 (int (*)(struct mtd_blktrans_dev * ))0, (int (*)(struct mtd_blktrans_dev * ))0,
1365 & mtdblock_add_mtd, & mtdblock_remove_dev, {(struct list_head *)0, (struct list_head *)0},
1366 {(struct list_head *)0, (struct list_head *)0}, & __this_module};
1367#line 98 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11885/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdblock_ro.c.p"
1368static int mtdblock_init(void)
1369{ int tmp ;
1370
1371 {
1372 {
1373#line 100
1374 tmp = register_mtd_blktrans(& mtdblock_tr);
1375 }
1376#line 100
1377 return (tmp);
1378}
1379}
1380#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11885/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdblock_ro.c.p"
1381static void mtdblock_exit(void)
1382{
1383
1384 {
1385 {
1386#line 105
1387 deregister_mtd_blktrans(& mtdblock_tr);
1388 }
1389#line 106
1390 return;
1391}
1392}
1393#line 131
1394extern void ldv_check_final_state(void) ;
1395#line 137
1396extern void ldv_initialize(void) ;
1397#line 140
1398extern int __VERIFIER_nondet_int(void) ;
1399#line 143 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11885/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdblock_ro.c.p"
1400int LDV_IN_INTERRUPT ;
1401#line 146 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11885/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdblock_ro.c.p"
1402void main(void)
1403{ struct mtd_blktrans_dev *var_group1 ;
1404 unsigned long var_mtdblock_readsect_0_p1 ;
1405 char *var_mtdblock_readsect_0_p2 ;
1406 unsigned long var_mtdblock_writesect_1_p1 ;
1407 char *var_mtdblock_writesect_1_p2 ;
1408 struct mtd_blktrans_ops *var_group2 ;
1409 struct mtd_info *var_group3 ;
1410 int tmp ;
1411 int tmp___0 ;
1412 int tmp___1 ;
1413
1414 {
1415 {
1416#line 182
1417 LDV_IN_INTERRUPT = 1;
1418#line 191
1419 ldv_initialize();
1420#line 197
1421 tmp = mtdblock_init();
1422 }
1423#line 197
1424 if (tmp != 0) {
1425#line 198
1426 goto ldv_final;
1427 } else {
1428
1429 }
1430#line 202
1431 goto ldv_15493;
1432 ldv_15492:
1433 {
1434#line 205
1435 tmp___0 = __VERIFIER_nondet_int();
1436 }
1437#line 207
1438 if (tmp___0 == 0) {
1439#line 207
1440 goto case_0;
1441 } else
1442#line 223
1443 if (tmp___0 == 1) {
1444#line 223
1445 goto case_1;
1446 } else
1447#line 239
1448 if (tmp___0 == 2) {
1449#line 239
1450 goto case_2;
1451 } else
1452#line 255
1453 if (tmp___0 == 3) {
1454#line 255
1455 goto case_3;
1456 } else {
1457 {
1458#line 271
1459 goto switch_default;
1460#line 205
1461 if (0) {
1462 case_0:
1463 {
1464#line 215
1465 mtdblock_readsect(var_group1, var_mtdblock_readsect_0_p1, var_mtdblock_readsect_0_p2);
1466 }
1467#line 222
1468 goto ldv_15487;
1469 case_1:
1470 {
1471#line 231
1472 mtdblock_writesect(var_group1, var_mtdblock_writesect_1_p1, var_mtdblock_writesect_1_p2);
1473 }
1474#line 238
1475 goto ldv_15487;
1476 case_2:
1477 {
1478#line 247
1479 mtdblock_add_mtd(var_group2, var_group3);
1480 }
1481#line 254
1482 goto ldv_15487;
1483 case_3:
1484 {
1485#line 263
1486 mtdblock_remove_dev(var_group1);
1487 }
1488#line 270
1489 goto ldv_15487;
1490 switch_default: ;
1491#line 271
1492 goto ldv_15487;
1493 } else {
1494 switch_break: ;
1495 }
1496 }
1497 }
1498 ldv_15487: ;
1499 ldv_15493:
1500 {
1501#line 202
1502 tmp___1 = __VERIFIER_nondet_int();
1503 }
1504#line 202
1505 if (tmp___1 != 0) {
1506#line 203
1507 goto ldv_15492;
1508 } else {
1509#line 205
1510 goto ldv_15494;
1511 }
1512 ldv_15494: ;
1513 {
1514#line 283
1515 mtdblock_exit();
1516 }
1517 ldv_final:
1518 {
1519#line 286
1520 ldv_check_final_state();
1521 }
1522#line 289
1523 return;
1524}
1525}
1526#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11885/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
1527void ldv_blast_assert(void)
1528{
1529
1530 {
1531 ERROR: ;
1532#line 6
1533 goto ERROR;
1534}
1535}
1536#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11885/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
1537extern int __VERIFIER_nondet_int(void) ;
1538#line 310 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11885/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdblock_ro.c.p"
1539int ldv_spin = 0;
1540#line 314 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11885/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdblock_ro.c.p"
1541void ldv_check_alloc_flags(gfp_t flags )
1542{
1543
1544 {
1545#line 317
1546 if (ldv_spin != 0) {
1547#line 317
1548 if (flags != 32U) {
1549 {
1550#line 317
1551 ldv_blast_assert();
1552 }
1553 } else {
1554
1555 }
1556 } else {
1557
1558 }
1559#line 320
1560 return;
1561}
1562}
1563#line 320
1564extern struct page *ldv_some_page(void) ;
1565#line 323 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11885/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdblock_ro.c.p"
1566struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags )
1567{ struct page *tmp ;
1568
1569 {
1570#line 326
1571 if (ldv_spin != 0) {
1572#line 326
1573 if (flags != 32U) {
1574 {
1575#line 326
1576 ldv_blast_assert();
1577 }
1578 } else {
1579
1580 }
1581 } else {
1582
1583 }
1584 {
1585#line 328
1586 tmp = ldv_some_page();
1587 }
1588#line 328
1589 return (tmp);
1590}
1591}
1592#line 332 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11885/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdblock_ro.c.p"
1593void ldv_check_alloc_nonatomic(void)
1594{
1595
1596 {
1597#line 335
1598 if (ldv_spin != 0) {
1599 {
1600#line 335
1601 ldv_blast_assert();
1602 }
1603 } else {
1604
1605 }
1606#line 338
1607 return;
1608}
1609}
1610#line 339 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11885/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdblock_ro.c.p"
1611void ldv_spin_lock(void)
1612{
1613
1614 {
1615#line 342
1616 ldv_spin = 1;
1617#line 343
1618 return;
1619}
1620}
1621#line 346 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11885/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdblock_ro.c.p"
1622void ldv_spin_unlock(void)
1623{
1624
1625 {
1626#line 349
1627 ldv_spin = 0;
1628#line 350
1629 return;
1630}
1631}
1632#line 353 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11885/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdblock_ro.c.p"
1633int ldv_spin_trylock(void)
1634{ int is_lock ;
1635
1636 {
1637 {
1638#line 358
1639 is_lock = __VERIFIER_nondet_int();
1640 }
1641#line 360
1642 if (is_lock != 0) {
1643#line 363
1644 return (0);
1645 } else {
1646#line 368
1647 ldv_spin = 1;
1648#line 370
1649 return (1);
1650 }
1651}
1652}
1653#line 537 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11885/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdblock_ro.c.p"
1654void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 )
1655{
1656
1657 {
1658 {
1659#line 543
1660 ldv_check_alloc_flags(ldv_func_arg2);
1661#line 545
1662 kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
1663 }
1664#line 546
1665 return ((void *)0);
1666}
1667}
1668#line 548 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11885/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdblock_ro.c.p"
1669__inline static void *kzalloc(size_t size , gfp_t flags )
1670{ void *tmp ;
1671
1672 {
1673 {
1674#line 554
1675 ldv_check_alloc_flags(flags);
1676#line 555
1677 tmp = __VERIFIER_nondet_pointer();
1678 }
1679#line 555
1680 return (tmp);
1681}
1682}