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