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