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