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 phram_mtd_list {
1081 struct mtd_info mtd ;
1082 struct list_head list ;
1083};
1084#line 1 "<compiler builtins>"
1085
1086#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11720/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/phram.c.p"
1087void ldv_spin_lock(void) ;
1088#line 3
1089void ldv_spin_unlock(void) ;
1090#line 4
1091int ldv_spin_trylock(void) ;
1092#line 101 "include/linux/printk.h"
1093extern int printk(char const * , ...) ;
1094#line 307 "include/linux/kernel.h"
1095extern unsigned long simple_strtoul(char const * , char ** , unsigned int ) ;
1096#line 47 "include/linux/list.h"
1097extern void __list_add(struct list_head * , struct list_head * , struct list_head * ) ;
1098#line 74 "include/linux/list.h"
1099__inline static void list_add_tail(struct list_head *new , struct list_head *head )
1100{ unsigned long __cil_tmp3 ;
1101 unsigned long __cil_tmp4 ;
1102 struct list_head *__cil_tmp5 ;
1103
1104 {
1105 {
1106#line 76
1107 __cil_tmp3 = (unsigned long )head;
1108#line 76
1109 __cil_tmp4 = __cil_tmp3 + 8;
1110#line 76
1111 __cil_tmp5 = *((struct list_head **)__cil_tmp4);
1112#line 76
1113 __list_add(new, __cil_tmp5, head);
1114 }
1115#line 77
1116 return;
1117}
1118}
1119#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/string_64.h"
1120extern void *memset(void * , int , size_t ) ;
1121#line 61
1122extern size_t strlen(char const * ) ;
1123#line 62
1124extern char *strcpy(char * , char const * ) ;
1125#line 63 "include/linux/string.h"
1126extern char *strrchr(char const * , int ) ;
1127#line 84
1128extern __kernel_size_t strnlen(char const * , __kernel_size_t ) ;
1129#line 90
1130extern char *strsep(char ** , char const * ) ;
1131#line 174 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
1132extern void *ioremap_nocache(resource_size_t , unsigned long ) ;
1133#line 182 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
1134__inline static void *ioremap(resource_size_t offset , unsigned long size )
1135{ void *tmp ;
1136
1137 {
1138 {
1139#line 184
1140 tmp = ioremap_nocache(offset, size);
1141 }
1142#line 184
1143 return (tmp);
1144}
1145}
1146#line 187
1147extern void iounmap(void volatile * ) ;
1148#line 26 "include/linux/export.h"
1149extern struct module __this_module ;
1150#line 161 "include/linux/slab.h"
1151extern void kfree(void const * ) ;
1152#line 220 "include/linux/slub_def.h"
1153extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t ) ;
1154#line 223
1155void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
1156#line 225
1157extern void *__kmalloc(size_t , gfp_t ) ;
1158#line 268 "include/linux/slub_def.h"
1159__inline static void *ldv_kmalloc_12(size_t size , gfp_t flags )
1160{ void *tmp___2 ;
1161
1162 {
1163 {
1164#line 283
1165 tmp___2 = __kmalloc(size, flags);
1166 }
1167#line 283
1168 return (tmp___2);
1169}
1170}
1171#line 268
1172__inline static void *kmalloc(size_t size , gfp_t flags ) ;
1173#line 353 "include/linux/slab.h"
1174__inline static void *kzalloc(size_t size , gfp_t flags ) ;
1175#line 10 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11720/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/phram.c.p"
1176extern void *__VERIFIER_nondet_pointer(void) ;
1177#line 11
1178void ldv_check_alloc_flags(gfp_t flags ) ;
1179#line 12
1180void ldv_check_alloc_nonatomic(void) ;
1181#line 14
1182struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
1183#line 362 "include/linux/mtd/mtd.h"
1184extern int mtd_device_parse_register(struct mtd_info * , char const ** , struct mtd_part_parser_data * ,
1185 struct mtd_partition const * , int ) ;
1186#line 369
1187extern int mtd_device_unregister(struct mtd_info * ) ;
1188#line 388
1189extern void mtd_erase_callback(struct erase_info * ) ;
1190#line 49 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11720/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/phram.c.p"
1191static struct list_head phram_list = {& phram_list, & phram_list};
1192#line 51 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11720/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/phram.c.p"
1193static int phram_erase(struct mtd_info *mtd , struct erase_info *instr )
1194{ u_char *start ;
1195 unsigned long __cil_tmp4 ;
1196 unsigned long __cil_tmp5 ;
1197 void *__cil_tmp6 ;
1198 unsigned long __cil_tmp7 ;
1199 unsigned long __cil_tmp8 ;
1200 uint64_t __cil_tmp9 ;
1201 u_char *__cil_tmp10 ;
1202 void *__cil_tmp11 ;
1203 unsigned long __cil_tmp12 ;
1204 unsigned long __cil_tmp13 ;
1205 uint64_t __cil_tmp14 ;
1206 size_t __cil_tmp15 ;
1207 unsigned long __cil_tmp16 ;
1208 unsigned long __cil_tmp17 ;
1209
1210 {
1211 {
1212#line 53
1213 __cil_tmp4 = (unsigned long )mtd;
1214#line 53
1215 __cil_tmp5 = __cil_tmp4 + 360;
1216#line 53
1217 __cil_tmp6 = *((void **)__cil_tmp5);
1218#line 53
1219 start = (u_char *)__cil_tmp6;
1220#line 55
1221 __cil_tmp7 = (unsigned long )instr;
1222#line 55
1223 __cil_tmp8 = __cil_tmp7 + 8;
1224#line 55
1225 __cil_tmp9 = *((uint64_t *)__cil_tmp8);
1226#line 55
1227 __cil_tmp10 = start + __cil_tmp9;
1228#line 55
1229 __cil_tmp11 = (void *)__cil_tmp10;
1230#line 55
1231 __cil_tmp12 = (unsigned long )instr;
1232#line 55
1233 __cil_tmp13 = __cil_tmp12 + 16;
1234#line 55
1235 __cil_tmp14 = *((uint64_t *)__cil_tmp13);
1236#line 55
1237 __cil_tmp15 = (size_t )__cil_tmp14;
1238#line 55
1239 memset(__cil_tmp11, 255, __cil_tmp15);
1240#line 62
1241 __cil_tmp16 = (unsigned long )instr;
1242#line 62
1243 __cil_tmp17 = __cil_tmp16 + 72;
1244#line 62
1245 *((u_char *)__cil_tmp17) = (u_char )8U;
1246#line 63
1247 mtd_erase_callback(instr);
1248 }
1249#line 64
1250 return (0);
1251}
1252}
1253#line 67 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11720/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/phram.c.p"
1254static int phram_point(struct mtd_info *mtd , loff_t from , size_t len , size_t *retlen ,
1255 void **virt , resource_size_t *phys )
1256{ unsigned long __cil_tmp7 ;
1257 unsigned long __cil_tmp8 ;
1258 unsigned long __cil_tmp9 ;
1259 void *__cil_tmp10 ;
1260
1261 {
1262#line 70
1263 __cil_tmp7 = (unsigned long )from;
1264#line 70
1265 __cil_tmp8 = (unsigned long )mtd;
1266#line 70
1267 __cil_tmp9 = __cil_tmp8 + 360;
1268#line 70
1269 __cil_tmp10 = *((void **)__cil_tmp9);
1270#line 70
1271 *virt = __cil_tmp10 + __cil_tmp7;
1272#line 71
1273 *retlen = len;
1274#line 72
1275 return (0);
1276}
1277}
1278#line 75 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11720/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/phram.c.p"
1279static int phram_unpoint(struct mtd_info *mtd , loff_t from , size_t len )
1280{
1281
1282 {
1283#line 77
1284 return (0);
1285}
1286}
1287#line 80 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11720/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/phram.c.p"
1288static int phram_read(struct mtd_info *mtd , loff_t from , size_t len , size_t *retlen ,
1289 u_char *buf )
1290{ u_char *start ;
1291 size_t __len ;
1292 void *__ret ;
1293 unsigned long __cil_tmp9 ;
1294 unsigned long __cil_tmp10 ;
1295 void *__cil_tmp11 ;
1296 void *__cil_tmp12 ;
1297 unsigned long __cil_tmp13 ;
1298 void const *__cil_tmp14 ;
1299 void const *__cil_tmp15 ;
1300
1301 {
1302 {
1303#line 83
1304 __cil_tmp9 = (unsigned long )mtd;
1305#line 83
1306 __cil_tmp10 = __cil_tmp9 + 360;
1307#line 83
1308 __cil_tmp11 = *((void **)__cil_tmp10);
1309#line 83
1310 start = (u_char *)__cil_tmp11;
1311#line 85
1312 __len = len;
1313#line 85
1314 __cil_tmp12 = (void *)buf;
1315#line 85
1316 __cil_tmp13 = (unsigned long )from;
1317#line 85
1318 __cil_tmp14 = (void const *)start;
1319#line 85
1320 __cil_tmp15 = __cil_tmp14 + __cil_tmp13;
1321#line 85
1322 __ret = __builtin_memcpy(__cil_tmp12, __cil_tmp15, __len);
1323#line 86
1324 *retlen = len;
1325 }
1326#line 87
1327 return (0);
1328}
1329}
1330#line 90 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11720/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/phram.c.p"
1331static int phram_write(struct mtd_info *mtd , loff_t to , size_t len , size_t *retlen ,
1332 u_char const *buf )
1333{ u_char *start ;
1334 size_t __len ;
1335 void *__ret ;
1336 unsigned long __cil_tmp9 ;
1337 unsigned long __cil_tmp10 ;
1338 void *__cil_tmp11 ;
1339 unsigned long __cil_tmp12 ;
1340 void *__cil_tmp13 ;
1341 void *__cil_tmp14 ;
1342 void const *__cil_tmp15 ;
1343
1344 {
1345 {
1346#line 93
1347 __cil_tmp9 = (unsigned long )mtd;
1348#line 93
1349 __cil_tmp10 = __cil_tmp9 + 360;
1350#line 93
1351 __cil_tmp11 = *((void **)__cil_tmp10);
1352#line 93
1353 start = (u_char *)__cil_tmp11;
1354#line 95
1355 __len = len;
1356#line 95
1357 __cil_tmp12 = (unsigned long )to;
1358#line 95
1359 __cil_tmp13 = (void *)start;
1360#line 95
1361 __cil_tmp14 = __cil_tmp13 + __cil_tmp12;
1362#line 95
1363 __cil_tmp15 = (void const *)buf;
1364#line 95
1365 __ret = __builtin_memcpy(__cil_tmp14, __cil_tmp15, __len);
1366#line 96
1367 *retlen = len;
1368 }
1369#line 97
1370 return (0);
1371}
1372}
1373#line 100 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11720/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/phram.c.p"
1374static void unregister_devices(void)
1375{ struct phram_mtd_list *this ;
1376 struct phram_mtd_list *safe ;
1377 struct list_head const *__mptr ;
1378 struct list_head const *__mptr___0 ;
1379 struct list_head const *__mptr___1 ;
1380 struct list_head *__cil_tmp6 ;
1381 struct list_head *__cil_tmp7 ;
1382 struct phram_mtd_list *__cil_tmp8 ;
1383 unsigned long __cil_tmp9 ;
1384 unsigned long __cil_tmp10 ;
1385 struct list_head *__cil_tmp11 ;
1386 struct phram_mtd_list *__cil_tmp12 ;
1387 struct mtd_info *__cil_tmp13 ;
1388 unsigned long __cil_tmp14 ;
1389 unsigned long __cil_tmp15 ;
1390 unsigned long __cil_tmp16 ;
1391 void *__cil_tmp17 ;
1392 void volatile *__cil_tmp18 ;
1393 unsigned long __cil_tmp19 ;
1394 unsigned long __cil_tmp20 ;
1395 unsigned long __cil_tmp21 ;
1396 char const *__cil_tmp22 ;
1397 void const *__cil_tmp23 ;
1398 void const *__cil_tmp24 ;
1399 unsigned long __cil_tmp25 ;
1400 unsigned long __cil_tmp26 ;
1401 struct list_head *__cil_tmp27 ;
1402 struct phram_mtd_list *__cil_tmp28 ;
1403 unsigned long __cil_tmp29 ;
1404 unsigned long __cil_tmp30 ;
1405 unsigned long __cil_tmp31 ;
1406 struct list_head *__cil_tmp32 ;
1407 unsigned long __cil_tmp33 ;
1408
1409 {
1410#line 104
1411 __cil_tmp6 = & phram_list;
1412#line 104
1413 __cil_tmp7 = *((struct list_head **)__cil_tmp6);
1414#line 104
1415 __mptr = (struct list_head const *)__cil_tmp7;
1416#line 104
1417 __cil_tmp8 = (struct phram_mtd_list *)__mptr;
1418#line 104
1419 this = __cil_tmp8 + 0xfffffffffffffa00UL;
1420#line 104
1421 __cil_tmp9 = (unsigned long )this;
1422#line 104
1423 __cil_tmp10 = __cil_tmp9 + 1536;
1424#line 104
1425 __cil_tmp11 = *((struct list_head **)__cil_tmp10);
1426#line 104
1427 __mptr___0 = (struct list_head const *)__cil_tmp11;
1428#line 104
1429 __cil_tmp12 = (struct phram_mtd_list *)__mptr___0;
1430#line 104
1431 safe = __cil_tmp12 + 0xfffffffffffffa00UL;
1432#line 104
1433 goto ldv_15413;
1434 ldv_15412:
1435 {
1436#line 105
1437 __cil_tmp13 = (struct mtd_info *)this;
1438#line 105
1439 mtd_device_unregister(__cil_tmp13);
1440#line 106
1441 __cil_tmp14 = 0 + 360;
1442#line 106
1443 __cil_tmp15 = (unsigned long )this;
1444#line 106
1445 __cil_tmp16 = __cil_tmp15 + __cil_tmp14;
1446#line 106
1447 __cil_tmp17 = *((void **)__cil_tmp16);
1448#line 106
1449 __cil_tmp18 = (void volatile *)__cil_tmp17;
1450#line 106
1451 iounmap(__cil_tmp18);
1452#line 107
1453 __cil_tmp19 = 0 + 56;
1454#line 107
1455 __cil_tmp20 = (unsigned long )this;
1456#line 107
1457 __cil_tmp21 = __cil_tmp20 + __cil_tmp19;
1458#line 107
1459 __cil_tmp22 = *((char const **)__cil_tmp21);
1460#line 107
1461 __cil_tmp23 = (void const *)__cil_tmp22;
1462#line 107
1463 kfree(__cil_tmp23);
1464#line 108
1465 __cil_tmp24 = (void const *)this;
1466#line 108
1467 kfree(__cil_tmp24);
1468#line 104
1469 this = safe;
1470#line 104
1471 __cil_tmp25 = (unsigned long )safe;
1472#line 104
1473 __cil_tmp26 = __cil_tmp25 + 1536;
1474#line 104
1475 __cil_tmp27 = *((struct list_head **)__cil_tmp26);
1476#line 104
1477 __mptr___1 = (struct list_head const *)__cil_tmp27;
1478#line 104
1479 __cil_tmp28 = (struct phram_mtd_list *)__mptr___1;
1480#line 104
1481 safe = __cil_tmp28 + 0xfffffffffffffa00UL;
1482 }
1483 ldv_15413: ;
1484 {
1485#line 104
1486 __cil_tmp29 = (unsigned long )(& phram_list);
1487#line 104
1488 __cil_tmp30 = (unsigned long )this;
1489#line 104
1490 __cil_tmp31 = __cil_tmp30 + 1536;
1491#line 104
1492 __cil_tmp32 = (struct list_head *)__cil_tmp31;
1493#line 104
1494 __cil_tmp33 = (unsigned long )__cil_tmp32;
1495#line 104
1496 if (__cil_tmp33 != __cil_tmp29) {
1497#line 105
1498 goto ldv_15412;
1499 } else {
1500#line 107
1501 goto ldv_15414;
1502 }
1503 }
1504 ldv_15414: ;
1505#line 109
1506 return;
1507}
1508}
1509#line 112 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11720/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/phram.c.p"
1510static int register_device(char *name , unsigned long start , unsigned long len )
1511{ struct phram_mtd_list *new ;
1512 int ret ;
1513 void *tmp ;
1514 int tmp___0 ;
1515 struct phram_mtd_list *__cil_tmp8 ;
1516 unsigned long __cil_tmp9 ;
1517 unsigned long __cil_tmp10 ;
1518 unsigned long __cil_tmp11 ;
1519 unsigned long __cil_tmp12 ;
1520 unsigned long __cil_tmp13 ;
1521 resource_size_t __cil_tmp14 ;
1522 void *__cil_tmp15 ;
1523 unsigned long __cil_tmp16 ;
1524 unsigned long __cil_tmp17 ;
1525 unsigned long __cil_tmp18 ;
1526 unsigned long __cil_tmp19 ;
1527 void *__cil_tmp20 ;
1528 unsigned long __cil_tmp21 ;
1529 unsigned long __cil_tmp22 ;
1530 unsigned long __cil_tmp23 ;
1531 unsigned long __cil_tmp24 ;
1532 unsigned long __cil_tmp25 ;
1533 unsigned long __cil_tmp26 ;
1534 unsigned long __cil_tmp27 ;
1535 unsigned long __cil_tmp28 ;
1536 unsigned long __cil_tmp29 ;
1537 unsigned long __cil_tmp30 ;
1538 unsigned long __cil_tmp31 ;
1539 unsigned long __cil_tmp32 ;
1540 unsigned long __cil_tmp33 ;
1541 unsigned long __cil_tmp34 ;
1542 unsigned long __cil_tmp35 ;
1543 unsigned long __cil_tmp36 ;
1544 unsigned long __cil_tmp37 ;
1545 unsigned long __cil_tmp38 ;
1546 unsigned long __cil_tmp39 ;
1547 unsigned long __cil_tmp40 ;
1548 unsigned long __cil_tmp41 ;
1549 unsigned long __cil_tmp42 ;
1550 unsigned long __cil_tmp43 ;
1551 unsigned long __cil_tmp44 ;
1552 unsigned long __cil_tmp45 ;
1553 unsigned long __cil_tmp46 ;
1554 unsigned long __cil_tmp47 ;
1555 unsigned long __cil_tmp48 ;
1556 unsigned long __cil_tmp49 ;
1557 unsigned long __cil_tmp50 ;
1558 unsigned long __cil_tmp51 ;
1559 unsigned long __cil_tmp52 ;
1560 unsigned long __cil_tmp53 ;
1561 unsigned long __cil_tmp54 ;
1562 struct mtd_info *__cil_tmp55 ;
1563 char const **__cil_tmp56 ;
1564 struct mtd_part_parser_data *__cil_tmp57 ;
1565 struct mtd_partition const *__cil_tmp58 ;
1566 unsigned long __cil_tmp59 ;
1567 unsigned long __cil_tmp60 ;
1568 struct list_head *__cil_tmp61 ;
1569 unsigned long __cil_tmp62 ;
1570 unsigned long __cil_tmp63 ;
1571 unsigned long __cil_tmp64 ;
1572 void *__cil_tmp65 ;
1573 void volatile *__cil_tmp66 ;
1574 void const *__cil_tmp67 ;
1575
1576 {
1577 {
1578#line 115
1579 ret = -12;
1580#line 117
1581 tmp = kzalloc(1552UL, 208U);
1582#line 117
1583 new = (struct phram_mtd_list *)tmp;
1584 }
1585 {
1586#line 118
1587 __cil_tmp8 = (struct phram_mtd_list *)0;
1588#line 118
1589 __cil_tmp9 = (unsigned long )__cil_tmp8;
1590#line 118
1591 __cil_tmp10 = (unsigned long )new;
1592#line 118
1593 if (__cil_tmp10 == __cil_tmp9) {
1594#line 119
1595 goto out0;
1596 } else {
1597
1598 }
1599 }
1600 {
1601#line 121
1602 ret = -5;
1603#line 122
1604 __cil_tmp11 = 0 + 360;
1605#line 122
1606 __cil_tmp12 = (unsigned long )new;
1607#line 122
1608 __cil_tmp13 = __cil_tmp12 + __cil_tmp11;
1609#line 122
1610 __cil_tmp14 = (resource_size_t )start;
1611#line 122
1612 *((void **)__cil_tmp13) = ioremap(__cil_tmp14, len);
1613 }
1614 {
1615#line 123
1616 __cil_tmp15 = (void *)0;
1617#line 123
1618 __cil_tmp16 = (unsigned long )__cil_tmp15;
1619#line 123
1620 __cil_tmp17 = 0 + 360;
1621#line 123
1622 __cil_tmp18 = (unsigned long )new;
1623#line 123
1624 __cil_tmp19 = __cil_tmp18 + __cil_tmp17;
1625#line 123
1626 __cil_tmp20 = *((void **)__cil_tmp19);
1627#line 123
1628 __cil_tmp21 = (unsigned long )__cil_tmp20;
1629#line 123
1630 if (__cil_tmp21 == __cil_tmp16) {
1631 {
1632#line 124
1633 printk("<3>phram: ioremap failed\n");
1634 }
1635#line 125
1636 goto out1;
1637 } else {
1638
1639 }
1640 }
1641 {
1642#line 129
1643 __cil_tmp22 = 0 + 56;
1644#line 129
1645 __cil_tmp23 = (unsigned long )new;
1646#line 129
1647 __cil_tmp24 = __cil_tmp23 + __cil_tmp22;
1648#line 129
1649 *((char const **)__cil_tmp24) = (char const *)name;
1650#line 130
1651 __cil_tmp25 = 0 + 8;
1652#line 130
1653 __cil_tmp26 = (unsigned long )new;
1654#line 130
1655 __cil_tmp27 = __cil_tmp26 + __cil_tmp25;
1656#line 130
1657 *((uint64_t *)__cil_tmp27) = (uint64_t )len;
1658#line 131
1659 __cil_tmp28 = 0 + 4;
1660#line 131
1661 __cil_tmp29 = (unsigned long )new;
1662#line 131
1663 __cil_tmp30 = __cil_tmp29 + __cil_tmp28;
1664#line 131
1665 *((uint32_t *)__cil_tmp30) = 7168U;
1666#line 132
1667 __cil_tmp31 = 0 + 96;
1668#line 132
1669 __cil_tmp32 = (unsigned long )new;
1670#line 132
1671 __cil_tmp33 = __cil_tmp32 + __cil_tmp31;
1672#line 132
1673 *((int (**)(struct mtd_info * , struct erase_info * ))__cil_tmp33) = & phram_erase;
1674#line 133
1675 __cil_tmp34 = 0 + 104;
1676#line 133
1677 __cil_tmp35 = (unsigned long )new;
1678#line 133
1679 __cil_tmp36 = __cil_tmp35 + __cil_tmp34;
1680#line 133
1681 *((int (**)(struct mtd_info * , loff_t , size_t , size_t * , void ** , resource_size_t * ))__cil_tmp36) = & phram_point;
1682#line 134
1683 __cil_tmp37 = 0 + 112;
1684#line 134
1685 __cil_tmp38 = (unsigned long )new;
1686#line 134
1687 __cil_tmp39 = __cil_tmp38 + __cil_tmp37;
1688#line 134
1689 *((int (**)(struct mtd_info * , loff_t , size_t ))__cil_tmp39) = & phram_unpoint;
1690#line 135
1691 __cil_tmp40 = 0 + 128;
1692#line 135
1693 __cil_tmp41 = (unsigned long )new;
1694#line 135
1695 __cil_tmp42 = __cil_tmp41 + __cil_tmp40;
1696#line 135
1697 *((int (**)(struct mtd_info * , loff_t , size_t , size_t * , u_char * ))__cil_tmp42) = & phram_read;
1698#line 136
1699 __cil_tmp43 = 0 + 136;
1700#line 136
1701 __cil_tmp44 = (unsigned long )new;
1702#line 136
1703 __cil_tmp45 = __cil_tmp44 + __cil_tmp43;
1704#line 136
1705 *((int (**)(struct mtd_info * , loff_t , size_t , size_t * , u_char const * ))__cil_tmp45) = & phram_write;
1706#line 137
1707 __cil_tmp46 = 0 + 368;
1708#line 137
1709 __cil_tmp47 = (unsigned long )new;
1710#line 137
1711 __cil_tmp48 = __cil_tmp47 + __cil_tmp46;
1712#line 137
1713 *((struct module **)__cil_tmp48) = & __this_module;
1714#line 138
1715 *((u_char *)new) = (u_char )1U;
1716#line 139
1717 __cil_tmp49 = 0 + 16;
1718#line 139
1719 __cil_tmp50 = (unsigned long )new;
1720#line 139
1721 __cil_tmp51 = __cil_tmp50 + __cil_tmp49;
1722#line 139
1723 *((uint32_t *)__cil_tmp51) = 4096U;
1724#line 140
1725 __cil_tmp52 = 0 + 20;
1726#line 140
1727 __cil_tmp53 = (unsigned long )new;
1728#line 140
1729 __cil_tmp54 = __cil_tmp53 + __cil_tmp52;
1730#line 140
1731 *((uint32_t *)__cil_tmp54) = 1U;
1732#line 142
1733 ret = -11;
1734#line 143
1735 __cil_tmp55 = (struct mtd_info *)new;
1736#line 143
1737 __cil_tmp56 = (char const **)0;
1738#line 143
1739 __cil_tmp57 = (struct mtd_part_parser_data *)0;
1740#line 143
1741 __cil_tmp58 = (struct mtd_partition const *)0;
1742#line 143
1743 tmp___0 = mtd_device_parse_register(__cil_tmp55, __cil_tmp56, __cil_tmp57, __cil_tmp58,
1744 0);
1745 }
1746#line 143
1747 if (tmp___0 != 0) {
1748 {
1749#line 144
1750 printk("<3>phram: Failed to register new device\n");
1751 }
1752#line 145
1753 goto out2;
1754 } else {
1755
1756 }
1757 {
1758#line 148
1759 __cil_tmp59 = (unsigned long )new;
1760#line 148
1761 __cil_tmp60 = __cil_tmp59 + 1536;
1762#line 148
1763 __cil_tmp61 = (struct list_head *)__cil_tmp60;
1764#line 148
1765 list_add_tail(__cil_tmp61, & phram_list);
1766 }
1767#line 149
1768 return (0);
1769 out2:
1770 {
1771#line 152
1772 __cil_tmp62 = 0 + 360;
1773#line 152
1774 __cil_tmp63 = (unsigned long )new;
1775#line 152
1776 __cil_tmp64 = __cil_tmp63 + __cil_tmp62;
1777#line 152
1778 __cil_tmp65 = *((void **)__cil_tmp64);
1779#line 152
1780 __cil_tmp66 = (void volatile *)__cil_tmp65;
1781#line 152
1782 iounmap(__cil_tmp66);
1783 }
1784 out1:
1785 {
1786#line 154
1787 __cil_tmp67 = (void const *)new;
1788#line 154
1789 kfree(__cil_tmp67);
1790 }
1791 out0: ;
1792#line 156
1793 return (ret);
1794}
1795}
1796#line 159 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11720/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/phram.c.p"
1797static int ustrtoul(char const *cp , char **endp , unsigned int base )
1798{ unsigned long result ;
1799 unsigned long tmp ;
1800 char *__cil_tmp6 ;
1801 char __cil_tmp7 ;
1802 char *__cil_tmp8 ;
1803 char *__cil_tmp9 ;
1804 char __cil_tmp10 ;
1805 signed char __cil_tmp11 ;
1806 int __cil_tmp12 ;
1807 char *__cil_tmp13 ;
1808
1809 {
1810 {
1811#line 161
1812 tmp = simple_strtoul(cp, endp, base);
1813#line 161
1814 result = tmp;
1815 }
1816 {
1817#line 163
1818 __cil_tmp6 = *endp;
1819#line 163
1820 __cil_tmp7 = *__cil_tmp6;
1821#line 164
1822 if ((int )__cil_tmp7 == 71) {
1823#line 164
1824 goto case_71;
1825 } else
1826#line 166
1827 if ((int )__cil_tmp7 == 77) {
1828#line 166
1829 goto case_77;
1830 } else
1831#line 168
1832 if ((int )__cil_tmp7 == 107) {
1833#line 168
1834 goto case_107;
1835 } else
1836#line 163
1837 if (0) {
1838 case_71:
1839#line 165
1840 result = result * 1024UL;
1841 case_77:
1842#line 167
1843 result = result * 1024UL;
1844 case_107:
1845#line 169
1846 result = result * 1024UL;
1847 {
1848#line 171
1849 __cil_tmp8 = *endp;
1850#line 171
1851 __cil_tmp9 = __cil_tmp8 + 1UL;
1852#line 171
1853 __cil_tmp10 = *__cil_tmp9;
1854#line 171
1855 __cil_tmp11 = (signed char )__cil_tmp10;
1856#line 171
1857 __cil_tmp12 = (int )__cil_tmp11;
1858#line 171
1859 if (__cil_tmp12 == 105) {
1860#line 172
1861 __cil_tmp13 = *endp;
1862#line 172
1863 *endp = __cil_tmp13 + 2UL;
1864 } else {
1865
1866 }
1867 }
1868 } else {
1869 switch_break: ;
1870 }
1871 }
1872#line 174
1873 return ((int )result);
1874}
1875}
1876#line 177 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11720/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/phram.c.p"
1877static int parse_num32(uint32_t *num32 , char const *token )
1878{ char *endp ;
1879 unsigned long n ;
1880 int tmp ;
1881 char **__cil_tmp6 ;
1882 char *__cil_tmp7 ;
1883 char __cil_tmp8 ;
1884 signed char __cil_tmp9 ;
1885 int __cil_tmp10 ;
1886
1887 {
1888 {
1889#line 182
1890 tmp = ustrtoul(token, & endp, 0U);
1891#line 182
1892 n = (unsigned long )tmp;
1893 }
1894 {
1895#line 183
1896 __cil_tmp6 = & endp;
1897#line 183
1898 __cil_tmp7 = *__cil_tmp6;
1899#line 183
1900 __cil_tmp8 = *__cil_tmp7;
1901#line 183
1902 __cil_tmp9 = (signed char )__cil_tmp8;
1903#line 183
1904 __cil_tmp10 = (int )__cil_tmp9;
1905#line 183
1906 if (__cil_tmp10 != 0) {
1907#line 184
1908 return (-22);
1909 } else {
1910
1911 }
1912 }
1913#line 186
1914 *num32 = (uint32_t )n;
1915#line 187
1916 return (0);
1917}
1918}
1919#line 190 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11720/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/phram.c.p"
1920static int parse_name(char **pname , char const *token )
1921{ size_t len ;
1922 char *name ;
1923 size_t tmp ;
1924 void *tmp___0 ;
1925 char *__cil_tmp7 ;
1926 unsigned long __cil_tmp8 ;
1927 unsigned long __cil_tmp9 ;
1928
1929 {
1930 {
1931#line 195
1932 tmp = strlen(token);
1933#line 195
1934 len = tmp + 1UL;
1935 }
1936#line 196
1937 if (len > 64UL) {
1938#line 197
1939 return (-28);
1940 } else {
1941
1942 }
1943 {
1944#line 199
1945 tmp___0 = kmalloc(len, 208U);
1946#line 199
1947 name = (char *)tmp___0;
1948 }
1949 {
1950#line 200
1951 __cil_tmp7 = (char *)0;
1952#line 200
1953 __cil_tmp8 = (unsigned long )__cil_tmp7;
1954#line 200
1955 __cil_tmp9 = (unsigned long )name;
1956#line 200
1957 if (__cil_tmp9 == __cil_tmp8) {
1958#line 201
1959 return (-12);
1960 } else {
1961
1962 }
1963 }
1964 {
1965#line 203
1966 strcpy(name, token);
1967#line 205
1968 *pname = name;
1969 }
1970#line 206
1971 return (0);
1972}
1973}
1974#line 210 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11720/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/phram.c.p"
1975__inline static void kill_final_newline(char *str )
1976{ char *newline ;
1977 char *tmp ;
1978 char const *__cil_tmp4 ;
1979 char *__cil_tmp5 ;
1980 unsigned long __cil_tmp6 ;
1981 unsigned long __cil_tmp7 ;
1982 char *__cil_tmp8 ;
1983 char __cil_tmp9 ;
1984 signed char __cil_tmp10 ;
1985 int __cil_tmp11 ;
1986
1987 {
1988 {
1989#line 212
1990 __cil_tmp4 = (char const *)str;
1991#line 212
1992 tmp = strrchr(__cil_tmp4, 10);
1993#line 212
1994 newline = tmp;
1995 }
1996 {
1997#line 213
1998 __cil_tmp5 = (char *)0;
1999#line 213
2000 __cil_tmp6 = (unsigned long )__cil_tmp5;
2001#line 213
2002 __cil_tmp7 = (unsigned long )newline;
2003#line 213
2004 if (__cil_tmp7 != __cil_tmp6) {
2005 {
2006#line 213
2007 __cil_tmp8 = newline + 1UL;
2008#line 213
2009 __cil_tmp9 = *__cil_tmp8;
2010#line 213
2011 __cil_tmp10 = (signed char )__cil_tmp9;
2012#line 213
2013 __cil_tmp11 = (int )__cil_tmp10;
2014#line 213
2015 if (__cil_tmp11 == 0) {
2016#line 214
2017 *newline = (char)0;
2018 } else {
2019
2020 }
2021 }
2022 } else {
2023
2024 }
2025 }
2026#line 215
2027 return;
2028}
2029}
2030#line 231 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11720/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/phram.c.p"
2031static char phram_paramline[88U] ;
2032#line 233 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11720/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/phram.c.p"
2033static int phram_setup(char const *val )
2034{ char buf[88U] ;
2035 char *str ;
2036 char *token[3U] ;
2037 char *name ;
2038 uint32_t start ;
2039 uint32_t len ;
2040 int i ;
2041 int ret ;
2042 __kernel_size_t tmp ;
2043 char **__cil_tmp11 ;
2044 char **__cil_tmp12 ;
2045 char *__cil_tmp13 ;
2046 char **__cil_tmp14 ;
2047 char *__cil_tmp15 ;
2048 unsigned long __cil_tmp16 ;
2049 unsigned long __cil_tmp17 ;
2050 char *__cil_tmp18 ;
2051 unsigned long __cil_tmp19 ;
2052 char **__cil_tmp20 ;
2053 char *__cil_tmp21 ;
2054 unsigned long __cil_tmp22 ;
2055 char *__cil_tmp23 ;
2056 unsigned long __cil_tmp24 ;
2057 unsigned long __cil_tmp25 ;
2058 unsigned long __cil_tmp26 ;
2059 char *__cil_tmp27 ;
2060 unsigned long __cil_tmp28 ;
2061 unsigned long __cil_tmp29 ;
2062 unsigned long __cil_tmp30 ;
2063 char *__cil_tmp31 ;
2064 char const *__cil_tmp32 ;
2065 unsigned long __cil_tmp33 ;
2066 unsigned long __cil_tmp34 ;
2067 char *__cil_tmp35 ;
2068 char const *__cil_tmp36 ;
2069 char **__cil_tmp37 ;
2070 char *__cil_tmp38 ;
2071 void const *__cil_tmp39 ;
2072 unsigned long __cil_tmp40 ;
2073 unsigned long __cil_tmp41 ;
2074 char *__cil_tmp42 ;
2075 char const *__cil_tmp43 ;
2076 char **__cil_tmp44 ;
2077 char *__cil_tmp45 ;
2078 void const *__cil_tmp46 ;
2079 char **__cil_tmp47 ;
2080 char *__cil_tmp48 ;
2081 uint32_t *__cil_tmp49 ;
2082 uint32_t __cil_tmp50 ;
2083 unsigned long __cil_tmp51 ;
2084 uint32_t *__cil_tmp52 ;
2085 uint32_t __cil_tmp53 ;
2086 unsigned long __cil_tmp54 ;
2087 char **__cil_tmp55 ;
2088 char *__cil_tmp56 ;
2089 uint32_t *__cil_tmp57 ;
2090 uint32_t __cil_tmp58 ;
2091 uint32_t *__cil_tmp59 ;
2092 uint32_t __cil_tmp60 ;
2093 char **__cil_tmp61 ;
2094 char *__cil_tmp62 ;
2095 void const *__cil_tmp63 ;
2096
2097 {
2098 {
2099#line 235
2100 __cil_tmp11 = & str;
2101#line 235
2102 *__cil_tmp11 = (char *)(& buf);
2103#line 242
2104 tmp = strnlen(val, 88UL);
2105 }
2106#line 242
2107 if (tmp > 87UL) {
2108 {
2109#line 243
2110 printk("<3>phram: parameter too long\n");
2111 }
2112#line 243
2113 return (1);
2114 } else {
2115
2116 }
2117 {
2118#line 245
2119 __cil_tmp12 = & str;
2120#line 245
2121 __cil_tmp13 = *__cil_tmp12;
2122#line 245
2123 strcpy(__cil_tmp13, val);
2124#line 246
2125 __cil_tmp14 = & str;
2126#line 246
2127 __cil_tmp15 = *__cil_tmp14;
2128#line 246
2129 kill_final_newline(__cil_tmp15);
2130#line 248
2131 i = 0;
2132 }
2133#line 248
2134 goto ldv_15463;
2135 ldv_15462:
2136 {
2137#line 249
2138 __cil_tmp16 = i * 8UL;
2139#line 249
2140 __cil_tmp17 = (unsigned long )(token) + __cil_tmp16;
2141#line 249
2142 *((char **)__cil_tmp17) = strsep(& str, ",");
2143#line 248
2144 i = i + 1;
2145 }
2146 ldv_15463: ;
2147#line 248
2148 if (i <= 2) {
2149#line 249
2150 goto ldv_15462;
2151 } else {
2152#line 251
2153 goto ldv_15464;
2154 }
2155 ldv_15464: ;
2156 {
2157#line 251
2158 __cil_tmp18 = (char *)0;
2159#line 251
2160 __cil_tmp19 = (unsigned long )__cil_tmp18;
2161#line 251
2162 __cil_tmp20 = & str;
2163#line 251
2164 __cil_tmp21 = *__cil_tmp20;
2165#line 251
2166 __cil_tmp22 = (unsigned long )__cil_tmp21;
2167#line 251
2168 if (__cil_tmp22 != __cil_tmp19) {
2169 {
2170#line 252
2171 printk("<3>phram: too many arguments\n");
2172 }
2173#line 252
2174 return (1);
2175 } else {
2176
2177 }
2178 }
2179 {
2180#line 254
2181 __cil_tmp23 = (char *)0;
2182#line 254
2183 __cil_tmp24 = (unsigned long )__cil_tmp23;
2184#line 254
2185 __cil_tmp25 = 2 * 8UL;
2186#line 254
2187 __cil_tmp26 = (unsigned long )(token) + __cil_tmp25;
2188#line 254
2189 __cil_tmp27 = *((char **)__cil_tmp26);
2190#line 254
2191 __cil_tmp28 = (unsigned long )__cil_tmp27;
2192#line 254
2193 if (__cil_tmp28 == __cil_tmp24) {
2194 {
2195#line 255
2196 printk("<3>phram: not enough arguments\n");
2197 }
2198#line 255
2199 return (1);
2200 } else {
2201
2202 }
2203 }
2204 {
2205#line 257
2206 __cil_tmp29 = 0 * 8UL;
2207#line 257
2208 __cil_tmp30 = (unsigned long )(token) + __cil_tmp29;
2209#line 257
2210 __cil_tmp31 = *((char **)__cil_tmp30);
2211#line 257
2212 __cil_tmp32 = (char const *)__cil_tmp31;
2213#line 257
2214 ret = parse_name(& name, __cil_tmp32);
2215 }
2216#line 258
2217 if (ret != 0) {
2218#line 259
2219 return (ret);
2220 } else {
2221
2222 }
2223 {
2224#line 261
2225 __cil_tmp33 = 1 * 8UL;
2226#line 261
2227 __cil_tmp34 = (unsigned long )(token) + __cil_tmp33;
2228#line 261
2229 __cil_tmp35 = *((char **)__cil_tmp34);
2230#line 261
2231 __cil_tmp36 = (char const *)__cil_tmp35;
2232#line 261
2233 ret = parse_num32(& start, __cil_tmp36);
2234 }
2235#line 262
2236 if (ret != 0) {
2237 {
2238#line 263
2239 __cil_tmp37 = & name;
2240#line 263
2241 __cil_tmp38 = *__cil_tmp37;
2242#line 263
2243 __cil_tmp39 = (void const *)__cil_tmp38;
2244#line 263
2245 kfree(__cil_tmp39);
2246#line 264
2247 printk("<3>phram: illegal start address\n");
2248 }
2249#line 264
2250 return (1);
2251 } else {
2252
2253 }
2254 {
2255#line 267
2256 __cil_tmp40 = 2 * 8UL;
2257#line 267
2258 __cil_tmp41 = (unsigned long )(token) + __cil_tmp40;
2259#line 267
2260 __cil_tmp42 = *((char **)__cil_tmp41);
2261#line 267
2262 __cil_tmp43 = (char const *)__cil_tmp42;
2263#line 267
2264 ret = parse_num32(& len, __cil_tmp43);
2265 }
2266#line 268
2267 if (ret != 0) {
2268 {
2269#line 269
2270 __cil_tmp44 = & name;
2271#line 269
2272 __cil_tmp45 = *__cil_tmp44;
2273#line 269
2274 __cil_tmp46 = (void const *)__cil_tmp45;
2275#line 269
2276 kfree(__cil_tmp46);
2277#line 270
2278 printk("<3>phram: illegal device length\n");
2279 }
2280#line 270
2281 return (1);
2282 } else {
2283
2284 }
2285 {
2286#line 273
2287 __cil_tmp47 = & name;
2288#line 273
2289 __cil_tmp48 = *__cil_tmp47;
2290#line 273
2291 __cil_tmp49 = & start;
2292#line 273
2293 __cil_tmp50 = *__cil_tmp49;
2294#line 273
2295 __cil_tmp51 = (unsigned long )__cil_tmp50;
2296#line 273
2297 __cil_tmp52 = & len;
2298#line 273
2299 __cil_tmp53 = *__cil_tmp52;
2300#line 273
2301 __cil_tmp54 = (unsigned long )__cil_tmp53;
2302#line 273
2303 ret = register_device(__cil_tmp48, __cil_tmp51, __cil_tmp54);
2304 }
2305#line 274
2306 if (ret == 0) {
2307 {
2308#line 275
2309 __cil_tmp55 = & name;
2310#line 275
2311 __cil_tmp56 = *__cil_tmp55;
2312#line 275
2313 __cil_tmp57 = & len;
2314#line 275
2315 __cil_tmp58 = *__cil_tmp57;
2316#line 275
2317 __cil_tmp59 = & start;
2318#line 275
2319 __cil_tmp60 = *__cil_tmp59;
2320#line 275
2321 printk("<6>phram: %s device: %#x at %#x\n", __cil_tmp56, __cil_tmp58, __cil_tmp60);
2322 }
2323 } else {
2324 {
2325#line 277
2326 __cil_tmp61 = & name;
2327#line 277
2328 __cil_tmp62 = *__cil_tmp61;
2329#line 277
2330 __cil_tmp63 = (void const *)__cil_tmp62;
2331#line 277
2332 kfree(__cil_tmp63);
2333 }
2334 }
2335#line 279
2336 return (ret);
2337}
2338}
2339#line 299 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11720/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/phram.c.p"
2340static int init_phram(void)
2341{ int tmp ;
2342 unsigned long __cil_tmp2 ;
2343 unsigned long __cil_tmp3 ;
2344 char __cil_tmp4 ;
2345 signed char __cil_tmp5 ;
2346 int __cil_tmp6 ;
2347 char const *__cil_tmp7 ;
2348
2349 {
2350 {
2351#line 301
2352 __cil_tmp2 = 0 * 1UL;
2353#line 301
2354 __cil_tmp3 = (unsigned long )(phram_paramline) + __cil_tmp2;
2355#line 301
2356 __cil_tmp4 = *((char *)__cil_tmp3);
2357#line 301
2358 __cil_tmp5 = (signed char )__cil_tmp4;
2359#line 301
2360 __cil_tmp6 = (int )__cil_tmp5;
2361#line 301
2362 if (__cil_tmp6 != 0) {
2363 {
2364#line 302
2365 __cil_tmp7 = (char const *)(& phram_paramline);
2366#line 302
2367 tmp = phram_setup(__cil_tmp7);
2368 }
2369#line 302
2370 return (tmp);
2371 } else {
2372
2373 }
2374 }
2375#line 304
2376 return (0);
2377}
2378}
2379#line 307 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11720/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/phram.c.p"
2380static void cleanup_phram(void)
2381{
2382
2383 {
2384 {
2385#line 309
2386 unregister_devices();
2387 }
2388#line 310
2389 return;
2390}
2391}
2392#line 335
2393extern void ldv_check_final_state(void) ;
2394#line 341
2395extern void ldv_initialize(void) ;
2396#line 344
2397extern int __VERIFIER_nondet_int(void) ;
2398#line 347 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11720/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/phram.c.p"
2399int LDV_IN_INTERRUPT ;
2400#line 350 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11720/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/phram.c.p"
2401void main(void)
2402{ int tmp ;
2403 int tmp___0 ;
2404 int tmp___1 ;
2405
2406 {
2407 {
2408#line 362
2409 LDV_IN_INTERRUPT = 1;
2410#line 371
2411 ldv_initialize();
2412#line 383
2413 tmp = init_phram();
2414 }
2415#line 383
2416 if (tmp != 0) {
2417#line 384
2418 goto ldv_final;
2419 } else {
2420
2421 }
2422#line 386
2423 goto ldv_15513;
2424 ldv_15512:
2425 {
2426#line 389
2427 tmp___0 = __VERIFIER_nondet_int();
2428 }
2429 {
2430#line 391
2431 goto switch_default;
2432#line 389
2433 if (0) {
2434 switch_default: ;
2435#line 391
2436 goto ldv_15511;
2437 } else {
2438 switch_break: ;
2439 }
2440 }
2441 ldv_15511: ;
2442 ldv_15513:
2443 {
2444#line 386
2445 tmp___1 = __VERIFIER_nondet_int();
2446 }
2447#line 386
2448 if (tmp___1 != 0) {
2449#line 387
2450 goto ldv_15512;
2451 } else {
2452#line 389
2453 goto ldv_15514;
2454 }
2455 ldv_15514: ;
2456 {
2457#line 409
2458 cleanup_phram();
2459 }
2460 ldv_final:
2461 {
2462#line 412
2463 ldv_check_final_state();
2464 }
2465#line 415
2466 return;
2467}
2468}
2469#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11720/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
2470void ldv_blast_assert(void)
2471{
2472
2473 {
2474 ERROR: ;
2475#line 6
2476 goto ERROR;
2477}
2478}
2479#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11720/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
2480extern int __VERIFIER_nondet_int(void) ;
2481#line 436 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11720/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/phram.c.p"
2482int ldv_spin = 0;
2483#line 440 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11720/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/phram.c.p"
2484void ldv_check_alloc_flags(gfp_t flags )
2485{
2486
2487 {
2488#line 443
2489 if (ldv_spin != 0) {
2490#line 443
2491 if (flags != 32U) {
2492 {
2493#line 443
2494 ldv_blast_assert();
2495 }
2496 } else {
2497
2498 }
2499 } else {
2500
2501 }
2502#line 446
2503 return;
2504}
2505}
2506#line 446
2507extern struct page *ldv_some_page(void) ;
2508#line 449 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11720/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/phram.c.p"
2509struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags )
2510{ struct page *tmp ;
2511
2512 {
2513#line 452
2514 if (ldv_spin != 0) {
2515#line 452
2516 if (flags != 32U) {
2517 {
2518#line 452
2519 ldv_blast_assert();
2520 }
2521 } else {
2522
2523 }
2524 } else {
2525
2526 }
2527 {
2528#line 454
2529 tmp = ldv_some_page();
2530 }
2531#line 454
2532 return (tmp);
2533}
2534}
2535#line 458 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11720/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/phram.c.p"
2536void ldv_check_alloc_nonatomic(void)
2537{
2538
2539 {
2540#line 461
2541 if (ldv_spin != 0) {
2542 {
2543#line 461
2544 ldv_blast_assert();
2545 }
2546 } else {
2547
2548 }
2549#line 464
2550 return;
2551}
2552}
2553#line 465 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11720/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/phram.c.p"
2554void ldv_spin_lock(void)
2555{
2556
2557 {
2558#line 468
2559 ldv_spin = 1;
2560#line 469
2561 return;
2562}
2563}
2564#line 472 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11720/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/phram.c.p"
2565void ldv_spin_unlock(void)
2566{
2567
2568 {
2569#line 475
2570 ldv_spin = 0;
2571#line 476
2572 return;
2573}
2574}
2575#line 479 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11720/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/phram.c.p"
2576int ldv_spin_trylock(void)
2577{ int is_lock ;
2578
2579 {
2580 {
2581#line 484
2582 is_lock = __VERIFIER_nondet_int();
2583 }
2584#line 486
2585 if (is_lock != 0) {
2586#line 489
2587 return (0);
2588 } else {
2589#line 494
2590 ldv_spin = 1;
2591#line 496
2592 return (1);
2593 }
2594}
2595}
2596#line 618 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11720/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/phram.c.p"
2597__inline static void *kmalloc(size_t size , gfp_t flags )
2598{
2599
2600 {
2601 {
2602#line 624
2603 ldv_check_alloc_flags(flags);
2604#line 626
2605 ldv_kmalloc_12(size, flags);
2606 }
2607#line 627
2608 return ((void *)0);
2609}
2610}
2611#line 663 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11720/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/phram.c.p"
2612void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 )
2613{
2614
2615 {
2616 {
2617#line 669
2618 ldv_check_alloc_flags(ldv_func_arg2);
2619#line 671
2620 kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
2621 }
2622#line 672
2623 return ((void *)0);
2624}
2625}
2626#line 674 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11720/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/phram.c.p"
2627__inline static void *kzalloc(size_t size , gfp_t flags )
2628{ void *tmp ;
2629
2630 {
2631 {
2632#line 680
2633 ldv_check_alloc_flags(flags);
2634#line 681
2635 tmp = __VERIFIER_nondet_pointer();
2636 }
2637#line 681
2638 return (tmp);
2639}
2640}