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