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