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/4912/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2760.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/4912/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2760.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 101 "include/linux/printk.h"
1086extern int printk(char const * , ...) ;
1087#line 134 "include/linux/mutex.h"
1088extern void mutex_lock_nested(struct mutex * , unsigned int ) ;
1089#line 169
1090extern void mutex_unlock(struct mutex * ) ;
1091#line 140 "include/linux/sysfs.h"
1092extern int sysfs_create_bin_file(struct kobject * , struct bin_attribute const * ) ;
1093#line 142
1094extern void sysfs_remove_bin_file(struct kobject * , struct bin_attribute const * ) ;
1095#line 220 "include/linux/slub_def.h"
1096extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t ) ;
1097#line 223
1098void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
1099#line 11 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4912/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2760.c.p"
1100void ldv_check_alloc_flags(gfp_t flags ) ;
1101#line 12
1102void ldv_check_alloc_nonatomic(void) ;
1103#line 14
1104struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
1105#line 792 "include/linux/device.h"
1106extern void *dev_get_drvdata(struct device const * ) ;
1107#line 793
1108extern int dev_set_drvdata(struct device * , void * ) ;
1109#line 40 "include/linux/platform_device.h"
1110extern void platform_device_unregister(struct platform_device * ) ;
1111#line 155
1112extern struct platform_device *platform_device_alloc(char const * , int ) ;
1113#line 160
1114extern int platform_device_add(struct platform_device * ) ;
1115#line 146 "include/linux/idr.h"
1116extern void ida_destroy(struct ida * ) ;
1117#line 147
1118extern void ida_init(struct ida * ) ;
1119#line 149
1120extern int ida_simple_get(struct ida * , unsigned int , unsigned int , gfp_t ) ;
1121#line 151
1122extern void ida_simple_remove(struct ida * , unsigned int ) ;
1123#line 69 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1_family.h"
1124extern void w1_unregister_family(struct w1_family * ) ;
1125#line 70
1126extern int w1_register_family(struct w1_family * ) ;
1127#line 211 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1.h"
1128extern void w1_write_8(struct w1_master * , u8 ) ;
1129#line 215
1130extern void w1_write_block(struct w1_master * , u8 const * , int ) ;
1131#line 217
1132extern u8 w1_read_block(struct w1_master * , u8 * , int ) ;
1133#line 218
1134extern int w1_reset_select_slave(struct w1_slave * ) ;
1135#line 50 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/w1_ds2760.h"
1136int w1_ds2760_read(struct device *dev , char *buf , int addr , size_t count ) ;
1137#line 52
1138int w1_ds2760_write(struct device *dev , char *buf , int addr , size_t count ) ;
1139#line 54
1140int w1_ds2760_store_eeprom(struct device *dev , int addr ) ;
1141#line 55
1142int w1_ds2760_recall_eeprom(struct device *dev , int addr ) ;
1143#line 41 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4912/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2760.c.p"
1144static int w1_ds2760_io(struct device *dev , char *buf , int addr , size_t count ,
1145 int io )
1146{ struct w1_slave *sl ;
1147 struct device const *__mptr ;
1148 u8 tmp ;
1149 int tmp___0 ;
1150 struct w1_slave *__cil_tmp10 ;
1151 struct device *__cil_tmp11 ;
1152 unsigned long __cil_tmp12 ;
1153 unsigned long __cil_tmp13 ;
1154 unsigned long __cil_tmp14 ;
1155 unsigned long __cil_tmp15 ;
1156 struct w1_master *__cil_tmp16 ;
1157 unsigned long __cil_tmp17 ;
1158 unsigned long __cil_tmp18 ;
1159 struct mutex *__cil_tmp19 ;
1160 size_t __cil_tmp20 ;
1161 size_t __cil_tmp21 ;
1162 int __cil_tmp22 ;
1163 unsigned long __cil_tmp23 ;
1164 unsigned long __cil_tmp24 ;
1165 struct w1_master *__cil_tmp25 ;
1166 u8 __cil_tmp26 ;
1167 unsigned long __cil_tmp27 ;
1168 unsigned long __cil_tmp28 ;
1169 struct w1_master *__cil_tmp29 ;
1170 u8 __cil_tmp30 ;
1171 int __cil_tmp31 ;
1172 u8 __cil_tmp32 ;
1173 unsigned long __cil_tmp33 ;
1174 unsigned long __cil_tmp34 ;
1175 struct w1_master *__cil_tmp35 ;
1176 u8 *__cil_tmp36 ;
1177 int __cil_tmp37 ;
1178 unsigned long __cil_tmp38 ;
1179 unsigned long __cil_tmp39 ;
1180 struct w1_master *__cil_tmp40 ;
1181 u8 __cil_tmp41 ;
1182 unsigned long __cil_tmp42 ;
1183 unsigned long __cil_tmp43 ;
1184 struct w1_master *__cil_tmp44 ;
1185 u8 __cil_tmp45 ;
1186 int __cil_tmp46 ;
1187 u8 __cil_tmp47 ;
1188 unsigned long __cil_tmp48 ;
1189 unsigned long __cil_tmp49 ;
1190 struct w1_master *__cil_tmp50 ;
1191 u8 const *__cil_tmp51 ;
1192 int __cil_tmp52 ;
1193 unsigned long __cil_tmp53 ;
1194 unsigned long __cil_tmp54 ;
1195 struct w1_master *__cil_tmp55 ;
1196 unsigned long __cil_tmp56 ;
1197 unsigned long __cil_tmp57 ;
1198 struct mutex *__cil_tmp58 ;
1199
1200 {
1201#line 44
1202 __mptr = (struct device const *)dev;
1203#line 44
1204 __cil_tmp10 = (struct w1_slave *)__mptr;
1205#line 44
1206 sl = __cil_tmp10 + 0xffffffffffffff90UL;
1207 {
1208#line 46
1209 __cil_tmp11 = (struct device *)0;
1210#line 46
1211 __cil_tmp12 = (unsigned long )__cil_tmp11;
1212#line 46
1213 __cil_tmp13 = (unsigned long )dev;
1214#line 46
1215 if (__cil_tmp13 == __cil_tmp12) {
1216#line 47
1217 return (0);
1218 } else {
1219
1220 }
1221 }
1222 {
1223#line 49
1224 __cil_tmp14 = (unsigned long )sl;
1225#line 49
1226 __cil_tmp15 = __cil_tmp14 + 88;
1227#line 49
1228 __cil_tmp16 = *((struct w1_master **)__cil_tmp15);
1229#line 49
1230 __cil_tmp17 = (unsigned long )__cil_tmp16;
1231#line 49
1232 __cil_tmp18 = __cil_tmp17 + 144;
1233#line 49
1234 __cil_tmp19 = (struct mutex *)__cil_tmp18;
1235#line 49
1236 mutex_lock_nested(__cil_tmp19, 0U);
1237 }
1238#line 51
1239 if (addr > 64) {
1240#line 52
1241 count = 0UL;
1242#line 53
1243 goto out;
1244 } else
1245#line 51
1246 if (addr < 0) {
1247#line 52
1248 count = 0UL;
1249#line 53
1250 goto out;
1251 } else {
1252
1253 }
1254 {
1255#line 55
1256 __cil_tmp20 = (size_t )addr;
1257#line 55
1258 __cil_tmp21 = __cil_tmp20 + count;
1259#line 55
1260 if (__cil_tmp21 > 64UL) {
1261#line 56
1262 __cil_tmp22 = 64 - addr;
1263#line 56
1264 count = (size_t )__cil_tmp22;
1265 } else {
1266
1267 }
1268 }
1269 {
1270#line 58
1271 tmp___0 = w1_reset_select_slave(sl);
1272 }
1273#line 58
1274 if (tmp___0 == 0) {
1275#line 59
1276 if (io == 0) {
1277 {
1278#line 60
1279 __cil_tmp23 = (unsigned long )sl;
1280#line 60
1281 __cil_tmp24 = __cil_tmp23 + 88;
1282#line 60
1283 __cil_tmp25 = *((struct w1_master **)__cil_tmp24);
1284#line 60
1285 __cil_tmp26 = (u8 )105;
1286#line 60
1287 w1_write_8(__cil_tmp25, __cil_tmp26);
1288#line 61
1289 __cil_tmp27 = (unsigned long )sl;
1290#line 61
1291 __cil_tmp28 = __cil_tmp27 + 88;
1292#line 61
1293 __cil_tmp29 = *((struct w1_master **)__cil_tmp28);
1294#line 61
1295 __cil_tmp30 = (u8 )addr;
1296#line 61
1297 __cil_tmp31 = (int )__cil_tmp30;
1298#line 61
1299 __cil_tmp32 = (u8 )__cil_tmp31;
1300#line 61
1301 w1_write_8(__cil_tmp29, __cil_tmp32);
1302#line 62
1303 __cil_tmp33 = (unsigned long )sl;
1304#line 62
1305 __cil_tmp34 = __cil_tmp33 + 88;
1306#line 62
1307 __cil_tmp35 = *((struct w1_master **)__cil_tmp34);
1308#line 62
1309 __cil_tmp36 = (u8 *)buf;
1310#line 62
1311 __cil_tmp37 = (int )count;
1312#line 62
1313 tmp = w1_read_block(__cil_tmp35, __cil_tmp36, __cil_tmp37);
1314#line 62
1315 count = (size_t )tmp;
1316 }
1317 } else {
1318 {
1319#line 64
1320 __cil_tmp38 = (unsigned long )sl;
1321#line 64
1322 __cil_tmp39 = __cil_tmp38 + 88;
1323#line 64
1324 __cil_tmp40 = *((struct w1_master **)__cil_tmp39);
1325#line 64
1326 __cil_tmp41 = (u8 )108;
1327#line 64
1328 w1_write_8(__cil_tmp40, __cil_tmp41);
1329#line 65
1330 __cil_tmp42 = (unsigned long )sl;
1331#line 65
1332 __cil_tmp43 = __cil_tmp42 + 88;
1333#line 65
1334 __cil_tmp44 = *((struct w1_master **)__cil_tmp43);
1335#line 65
1336 __cil_tmp45 = (u8 )addr;
1337#line 65
1338 __cil_tmp46 = (int )__cil_tmp45;
1339#line 65
1340 __cil_tmp47 = (u8 )__cil_tmp46;
1341#line 65
1342 w1_write_8(__cil_tmp44, __cil_tmp47);
1343#line 66
1344 __cil_tmp48 = (unsigned long )sl;
1345#line 66
1346 __cil_tmp49 = __cil_tmp48 + 88;
1347#line 66
1348 __cil_tmp50 = *((struct w1_master **)__cil_tmp49);
1349#line 66
1350 __cil_tmp51 = (u8 const *)buf;
1351#line 66
1352 __cil_tmp52 = (int )count;
1353#line 66
1354 w1_write_block(__cil_tmp50, __cil_tmp51, __cil_tmp52);
1355 }
1356 }
1357 } else {
1358
1359 }
1360 out:
1361 {
1362#line 72
1363 __cil_tmp53 = (unsigned long )sl;
1364#line 72
1365 __cil_tmp54 = __cil_tmp53 + 88;
1366#line 72
1367 __cil_tmp55 = *((struct w1_master **)__cil_tmp54);
1368#line 72
1369 __cil_tmp56 = (unsigned long )__cil_tmp55;
1370#line 72
1371 __cil_tmp57 = __cil_tmp56 + 144;
1372#line 72
1373 __cil_tmp58 = (struct mutex *)__cil_tmp57;
1374#line 72
1375 mutex_unlock(__cil_tmp58);
1376 }
1377#line 74
1378 return ((int )count);
1379}
1380}
1381#line 77 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4912/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2760.c.p"
1382int w1_ds2760_read(struct device *dev , char *buf , int addr , size_t count )
1383{ int tmp ;
1384
1385 {
1386 {
1387#line 79
1388 tmp = w1_ds2760_io(dev, buf, addr, count, 0);
1389 }
1390#line 79
1391 return (tmp);
1392}
1393}
1394#line 82 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4912/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2760.c.p"
1395int w1_ds2760_write(struct device *dev , char *buf , int addr , size_t count )
1396{ int tmp ;
1397
1398 {
1399 {
1400#line 84
1401 tmp = w1_ds2760_io(dev, buf, addr, count, 1);
1402 }
1403#line 84
1404 return (tmp);
1405}
1406}
1407#line 87 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4912/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2760.c.p"
1408static int w1_ds2760_eeprom_cmd(struct device *dev , int addr , int cmd )
1409{ struct w1_slave *sl ;
1410 struct device const *__mptr ;
1411 int tmp ;
1412 struct w1_slave *__cil_tmp7 ;
1413 struct device *__cil_tmp8 ;
1414 unsigned long __cil_tmp9 ;
1415 unsigned long __cil_tmp10 ;
1416 unsigned long __cil_tmp11 ;
1417 unsigned long __cil_tmp12 ;
1418 struct w1_master *__cil_tmp13 ;
1419 unsigned long __cil_tmp14 ;
1420 unsigned long __cil_tmp15 ;
1421 struct mutex *__cil_tmp16 ;
1422 unsigned long __cil_tmp17 ;
1423 unsigned long __cil_tmp18 ;
1424 struct w1_master *__cil_tmp19 ;
1425 u8 __cil_tmp20 ;
1426 int __cil_tmp21 ;
1427 u8 __cil_tmp22 ;
1428 unsigned long __cil_tmp23 ;
1429 unsigned long __cil_tmp24 ;
1430 struct w1_master *__cil_tmp25 ;
1431 u8 __cil_tmp26 ;
1432 int __cil_tmp27 ;
1433 u8 __cil_tmp28 ;
1434 unsigned long __cil_tmp29 ;
1435 unsigned long __cil_tmp30 ;
1436 struct w1_master *__cil_tmp31 ;
1437 unsigned long __cil_tmp32 ;
1438 unsigned long __cil_tmp33 ;
1439 struct mutex *__cil_tmp34 ;
1440
1441 {
1442#line 89
1443 __mptr = (struct device const *)dev;
1444#line 89
1445 __cil_tmp7 = (struct w1_slave *)__mptr;
1446#line 89
1447 sl = __cil_tmp7 + 0xffffffffffffff90UL;
1448 {
1449#line 91
1450 __cil_tmp8 = (struct device *)0;
1451#line 91
1452 __cil_tmp9 = (unsigned long )__cil_tmp8;
1453#line 91
1454 __cil_tmp10 = (unsigned long )dev;
1455#line 91
1456 if (__cil_tmp10 == __cil_tmp9) {
1457#line 92
1458 return (-22);
1459 } else {
1460
1461 }
1462 }
1463 {
1464#line 94
1465 __cil_tmp11 = (unsigned long )sl;
1466#line 94
1467 __cil_tmp12 = __cil_tmp11 + 88;
1468#line 94
1469 __cil_tmp13 = *((struct w1_master **)__cil_tmp12);
1470#line 94
1471 __cil_tmp14 = (unsigned long )__cil_tmp13;
1472#line 94
1473 __cil_tmp15 = __cil_tmp14 + 144;
1474#line 94
1475 __cil_tmp16 = (struct mutex *)__cil_tmp15;
1476#line 94
1477 mutex_lock_nested(__cil_tmp16, 0U);
1478#line 96
1479 tmp = w1_reset_select_slave(sl);
1480 }
1481#line 96
1482 if (tmp == 0) {
1483 {
1484#line 97
1485 __cil_tmp17 = (unsigned long )sl;
1486#line 97
1487 __cil_tmp18 = __cil_tmp17 + 88;
1488#line 97
1489 __cil_tmp19 = *((struct w1_master **)__cil_tmp18);
1490#line 97
1491 __cil_tmp20 = (u8 )cmd;
1492#line 97
1493 __cil_tmp21 = (int )__cil_tmp20;
1494#line 97
1495 __cil_tmp22 = (u8 )__cil_tmp21;
1496#line 97
1497 w1_write_8(__cil_tmp19, __cil_tmp22);
1498#line 98
1499 __cil_tmp23 = (unsigned long )sl;
1500#line 98
1501 __cil_tmp24 = __cil_tmp23 + 88;
1502#line 98
1503 __cil_tmp25 = *((struct w1_master **)__cil_tmp24);
1504#line 98
1505 __cil_tmp26 = (u8 )addr;
1506#line 98
1507 __cil_tmp27 = (int )__cil_tmp26;
1508#line 98
1509 __cil_tmp28 = (u8 )__cil_tmp27;
1510#line 98
1511 w1_write_8(__cil_tmp25, __cil_tmp28);
1512 }
1513 } else {
1514
1515 }
1516 {
1517#line 101
1518 __cil_tmp29 = (unsigned long )sl;
1519#line 101
1520 __cil_tmp30 = __cil_tmp29 + 88;
1521#line 101
1522 __cil_tmp31 = *((struct w1_master **)__cil_tmp30);
1523#line 101
1524 __cil_tmp32 = (unsigned long )__cil_tmp31;
1525#line 101
1526 __cil_tmp33 = __cil_tmp32 + 144;
1527#line 101
1528 __cil_tmp34 = (struct mutex *)__cil_tmp33;
1529#line 101
1530 mutex_unlock(__cil_tmp34);
1531 }
1532#line 102
1533 return (0);
1534}
1535}
1536#line 105 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4912/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2760.c.p"
1537int w1_ds2760_store_eeprom(struct device *dev , int addr )
1538{ int tmp ;
1539
1540 {
1541 {
1542#line 107
1543 tmp = w1_ds2760_eeprom_cmd(dev, addr, 72);
1544 }
1545#line 107
1546 return (tmp);
1547}
1548}
1549#line 110 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4912/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2760.c.p"
1550int w1_ds2760_recall_eeprom(struct device *dev , int addr )
1551{ int tmp ;
1552
1553 {
1554 {
1555#line 112
1556 tmp = w1_ds2760_eeprom_cmd(dev, addr, 184);
1557 }
1558#line 112
1559 return (tmp);
1560}
1561}
1562#line 115 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4912/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2760.c.p"
1563static ssize_t w1_ds2760_read_bin(struct file *filp , struct kobject *kobj , struct bin_attribute *bin_attr ,
1564 char *buf , loff_t off , size_t count )
1565{ struct device *dev ;
1566 struct kobject const *__mptr ;
1567 int tmp ;
1568 struct device *__cil_tmp10 ;
1569 int __cil_tmp11 ;
1570
1571 {
1572 {
1573#line 119
1574 __mptr = (struct kobject const *)kobj;
1575#line 119
1576 __cil_tmp10 = (struct device *)__mptr;
1577#line 119
1578 dev = __cil_tmp10 + 0xfffffffffffffff0UL;
1579#line 120
1580 __cil_tmp11 = (int )off;
1581#line 120
1582 tmp = w1_ds2760_read(dev, buf, __cil_tmp11, count);
1583 }
1584#line 120
1585 return ((ssize_t )tmp);
1586}
1587}
1588#line 123 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4912/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2760.c.p"
1589static struct bin_attribute w1_ds2760_bin_attr = {{"w1_slave", (umode_t )292U, (struct lock_class_key *)0, {{{(char)0}, {(char)0},
1590 {(char)0}, {(char)0},
1591 {(char)0}, {(char)0},
1592 {(char)0}, {(char)0}}}},
1593 64UL, (void *)0, & w1_ds2760_read_bin, (ssize_t (*)(struct file * , struct kobject * ,
1594 struct bin_attribute * , char * ,
1595 loff_t , size_t ))0, (int (*)(struct file * ,
1596 struct kobject * ,
1597 struct bin_attribute * ,
1598 struct vm_area_struct * ))0};
1599#line 132 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4912/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2760.c.p"
1600static struct ida bat_ida = {{(struct idr_layer *)0, (struct idr_layer *)0, 0, 0, {{{{{0U}}, 3735899821U, 4294967295U,
1601 (void *)0xffffffffffffffffUL,
1602 {(struct lock_class_key *)0,
1603 {(struct lock_class *)0,
1604 (struct lock_class *)0},
1605 "bat_ida.lock", 0, 0UL}}}}},
1606 (struct ida_bitmap *)0};
1607#line 134 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4912/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2760.c.p"
1608static int w1_ds2760_add_slave(struct w1_slave *sl )
1609{ int ret ;
1610 int id ;
1611 struct platform_device *pdev ;
1612 struct platform_device *__cil_tmp5 ;
1613 unsigned long __cil_tmp6 ;
1614 unsigned long __cil_tmp7 ;
1615 unsigned long __cil_tmp8 ;
1616 unsigned long __cil_tmp9 ;
1617 unsigned long __cil_tmp10 ;
1618 unsigned long __cil_tmp11 ;
1619 unsigned long __cil_tmp12 ;
1620 unsigned long __cil_tmp13 ;
1621 unsigned long __cil_tmp14 ;
1622 struct kobject *__cil_tmp15 ;
1623 struct bin_attribute const *__cil_tmp16 ;
1624 unsigned long __cil_tmp17 ;
1625 unsigned long __cil_tmp18 ;
1626 struct device *__cil_tmp19 ;
1627 void *__cil_tmp20 ;
1628 unsigned int __cil_tmp21 ;
1629
1630 {
1631 {
1632#line 140
1633 id = ida_simple_get(& bat_ida, 0U, 0U, 208U);
1634 }
1635#line 141
1636 if (id < 0) {
1637#line 142
1638 ret = id;
1639#line 143
1640 goto noid;
1641 } else {
1642
1643 }
1644 {
1645#line 146
1646 pdev = platform_device_alloc("ds2760-battery", id);
1647 }
1648 {
1649#line 147
1650 __cil_tmp5 = (struct platform_device *)0;
1651#line 147
1652 __cil_tmp6 = (unsigned long )__cil_tmp5;
1653#line 147
1654 __cil_tmp7 = (unsigned long )pdev;
1655#line 147
1656 if (__cil_tmp7 == __cil_tmp6) {
1657#line 148
1658 ret = -12;
1659#line 149
1660 goto pdev_alloc_failed;
1661 } else {
1662
1663 }
1664 }
1665 {
1666#line 151
1667 __cil_tmp8 = (unsigned long )pdev;
1668#line 151
1669 __cil_tmp9 = __cil_tmp8 + 16;
1670#line 151
1671 __cil_tmp10 = (unsigned long )sl;
1672#line 151
1673 __cil_tmp11 = __cil_tmp10 + 112;
1674#line 151
1675 *((struct device **)__cil_tmp9) = (struct device *)__cil_tmp11;
1676#line 153
1677 ret = platform_device_add(pdev);
1678 }
1679#line 154
1680 if (ret != 0) {
1681#line 155
1682 goto pdev_add_failed;
1683 } else {
1684
1685 }
1686 {
1687#line 157
1688 __cil_tmp12 = 112 + 16;
1689#line 157
1690 __cil_tmp13 = (unsigned long )sl;
1691#line 157
1692 __cil_tmp14 = __cil_tmp13 + __cil_tmp12;
1693#line 157
1694 __cil_tmp15 = (struct kobject *)__cil_tmp14;
1695#line 157
1696 __cil_tmp16 = (struct bin_attribute const *)(& w1_ds2760_bin_attr);
1697#line 157
1698 ret = sysfs_create_bin_file(__cil_tmp15, __cil_tmp16);
1699 }
1700#line 158
1701 if (ret != 0) {
1702#line 159
1703 goto bin_attr_failed;
1704 } else {
1705
1706 }
1707 {
1708#line 161
1709 __cil_tmp17 = (unsigned long )sl;
1710#line 161
1711 __cil_tmp18 = __cil_tmp17 + 112;
1712#line 161
1713 __cil_tmp19 = (struct device *)__cil_tmp18;
1714#line 161
1715 __cil_tmp20 = (void *)pdev;
1716#line 161
1717 dev_set_drvdata(__cil_tmp19, __cil_tmp20);
1718 }
1719#line 163
1720 goto success;
1721 bin_attr_failed: ;
1722 pdev_add_failed:
1723 {
1724#line 167
1725 platform_device_unregister(pdev);
1726 }
1727 pdev_alloc_failed:
1728 {
1729#line 169
1730 __cil_tmp21 = (unsigned int )id;
1731#line 169
1732 ida_simple_remove(& bat_ida, __cil_tmp21);
1733 }
1734 noid: ;
1735 success: ;
1736#line 172
1737 return (ret);
1738}
1739}
1740#line 175 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4912/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2760.c.p"
1741static void w1_ds2760_remove_slave(struct w1_slave *sl )
1742{ struct platform_device *pdev ;
1743 void *tmp ;
1744 int id ;
1745 unsigned long __cil_tmp5 ;
1746 unsigned long __cil_tmp6 ;
1747 struct device *__cil_tmp7 ;
1748 struct device const *__cil_tmp8 ;
1749 unsigned long __cil_tmp9 ;
1750 unsigned long __cil_tmp10 ;
1751 unsigned int __cil_tmp11 ;
1752 unsigned long __cil_tmp12 ;
1753 unsigned long __cil_tmp13 ;
1754 unsigned long __cil_tmp14 ;
1755 struct kobject *__cil_tmp15 ;
1756 struct bin_attribute const *__cil_tmp16 ;
1757
1758 {
1759 {
1760#line 177
1761 __cil_tmp5 = (unsigned long )sl;
1762#line 177
1763 __cil_tmp6 = __cil_tmp5 + 112;
1764#line 177
1765 __cil_tmp7 = (struct device *)__cil_tmp6;
1766#line 177
1767 __cil_tmp8 = (struct device const *)__cil_tmp7;
1768#line 177
1769 tmp = dev_get_drvdata(__cil_tmp8);
1770#line 177
1771 pdev = (struct platform_device *)tmp;
1772#line 178
1773 __cil_tmp9 = (unsigned long )pdev;
1774#line 178
1775 __cil_tmp10 = __cil_tmp9 + 8;
1776#line 178
1777 id = *((int *)__cil_tmp10);
1778#line 180
1779 platform_device_unregister(pdev);
1780#line 181
1781 __cil_tmp11 = (unsigned int )id;
1782#line 181
1783 ida_simple_remove(& bat_ida, __cil_tmp11);
1784#line 182
1785 __cil_tmp12 = 112 + 16;
1786#line 182
1787 __cil_tmp13 = (unsigned long )sl;
1788#line 182
1789 __cil_tmp14 = __cil_tmp13 + __cil_tmp12;
1790#line 182
1791 __cil_tmp15 = (struct kobject *)__cil_tmp14;
1792#line 182
1793 __cil_tmp16 = (struct bin_attribute const *)(& w1_ds2760_bin_attr);
1794#line 182
1795 sysfs_remove_bin_file(__cil_tmp15, __cil_tmp16);
1796 }
1797#line 183
1798 return;
1799}
1800}
1801#line 185 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4912/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2760.c.p"
1802static struct w1_family_ops w1_ds2760_fops = {& w1_ds2760_add_slave, & w1_ds2760_remove_slave};
1803#line 190 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4912/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2760.c.p"
1804static struct w1_family w1_ds2760_family = {{(struct list_head *)0, (struct list_head *)0}, (u8 )48U, & w1_ds2760_fops, {0}};
1805#line 195 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4912/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2760.c.p"
1806static int w1_ds2760_init(void)
1807{ int tmp ;
1808
1809 {
1810 {
1811#line 197
1812 printk("<6>1-Wire driver for the DS2760 battery monitor chip - (c) 2004-2005, Szabolcs Gyurko\n");
1813#line 199
1814 ida_init(& bat_ida);
1815#line 200
1816 tmp = w1_register_family(& w1_ds2760_family);
1817 }
1818#line 200
1819 return (tmp);
1820}
1821}
1822#line 203 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4912/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2760.c.p"
1823static void w1_ds2760_exit(void)
1824{
1825
1826 {
1827 {
1828#line 205
1829 w1_unregister_family(& w1_ds2760_family);
1830#line 206
1831 ida_destroy(& bat_ida);
1832 }
1833#line 207
1834 return;
1835}
1836}
1837#line 237
1838extern void ldv_check_final_state(void) ;
1839#line 243
1840extern void ldv_initialize(void) ;
1841#line 246
1842extern int __VERIFIER_nondet_int(void) ;
1843#line 249 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4912/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2760.c.p"
1844int LDV_IN_INTERRUPT ;
1845#line 252 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4912/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2760.c.p"
1846void main(void)
1847{ struct file *var_group1 ;
1848 struct kobject *var_group2 ;
1849 struct bin_attribute *var_w1_ds2760_read_bin_6_p2 ;
1850 char *var_w1_ds2760_read_bin_6_p3 ;
1851 loff_t var_w1_ds2760_read_bin_6_p4 ;
1852 size_t var_w1_ds2760_read_bin_6_p5 ;
1853 struct w1_slave *var_group3 ;
1854 int tmp ;
1855 int tmp___0 ;
1856 int tmp___1 ;
1857
1858 {
1859 {
1860#line 288
1861 LDV_IN_INTERRUPT = 1;
1862#line 297
1863 ldv_initialize();
1864#line 303
1865 tmp = w1_ds2760_init();
1866 }
1867#line 303
1868 if (tmp != 0) {
1869#line 304
1870 goto ldv_final;
1871 } else {
1872
1873 }
1874#line 310
1875 goto ldv_15704;
1876 ldv_15703:
1877 {
1878#line 313
1879 tmp___0 = __VERIFIER_nondet_int();
1880 }
1881#line 315
1882 if (tmp___0 == 0) {
1883#line 315
1884 goto case_0;
1885 } else
1886#line 331
1887 if (tmp___0 == 1) {
1888#line 331
1889 goto case_1;
1890 } else
1891#line 347
1892 if (tmp___0 == 2) {
1893#line 347
1894 goto case_2;
1895 } else {
1896 {
1897#line 363
1898 goto switch_default;
1899#line 313
1900 if (0) {
1901 case_0:
1902 {
1903#line 323
1904 w1_ds2760_read_bin(var_group1, var_group2, var_w1_ds2760_read_bin_6_p2, var_w1_ds2760_read_bin_6_p3,
1905 var_w1_ds2760_read_bin_6_p4, var_w1_ds2760_read_bin_6_p5);
1906 }
1907#line 330
1908 goto ldv_15699;
1909 case_1:
1910 {
1911#line 339
1912 w1_ds2760_add_slave(var_group3);
1913 }
1914#line 346
1915 goto ldv_15699;
1916 case_2:
1917 {
1918#line 355
1919 w1_ds2760_remove_slave(var_group3);
1920 }
1921#line 362
1922 goto ldv_15699;
1923 switch_default: ;
1924#line 363
1925 goto ldv_15699;
1926 } else {
1927 switch_break: ;
1928 }
1929 }
1930 }
1931 ldv_15699: ;
1932 ldv_15704:
1933 {
1934#line 310
1935 tmp___1 = __VERIFIER_nondet_int();
1936 }
1937#line 310
1938 if (tmp___1 != 0) {
1939#line 311
1940 goto ldv_15703;
1941 } else {
1942#line 313
1943 goto ldv_15705;
1944 }
1945 ldv_15705: ;
1946 {
1947#line 375
1948 w1_ds2760_exit();
1949 }
1950 ldv_final:
1951 {
1952#line 378
1953 ldv_check_final_state();
1954 }
1955#line 381
1956 return;
1957}
1958}
1959#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4912/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
1960void ldv_blast_assert(void)
1961{
1962
1963 {
1964 ERROR: ;
1965#line 6
1966 goto ERROR;
1967}
1968}
1969#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4912/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
1970extern int __VERIFIER_nondet_int(void) ;
1971#line 402 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4912/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2760.c.p"
1972int ldv_spin = 0;
1973#line 406 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4912/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2760.c.p"
1974void ldv_check_alloc_flags(gfp_t flags )
1975{
1976
1977 {
1978#line 409
1979 if (ldv_spin != 0) {
1980#line 409
1981 if (flags != 32U) {
1982 {
1983#line 409
1984 ldv_blast_assert();
1985 }
1986 } else {
1987
1988 }
1989 } else {
1990
1991 }
1992#line 412
1993 return;
1994}
1995}
1996#line 412
1997extern struct page *ldv_some_page(void) ;
1998#line 415 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4912/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2760.c.p"
1999struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags )
2000{ struct page *tmp ;
2001
2002 {
2003#line 418
2004 if (ldv_spin != 0) {
2005#line 418
2006 if (flags != 32U) {
2007 {
2008#line 418
2009 ldv_blast_assert();
2010 }
2011 } else {
2012
2013 }
2014 } else {
2015
2016 }
2017 {
2018#line 420
2019 tmp = ldv_some_page();
2020 }
2021#line 420
2022 return (tmp);
2023}
2024}
2025#line 424 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4912/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2760.c.p"
2026void ldv_check_alloc_nonatomic(void)
2027{
2028
2029 {
2030#line 427
2031 if (ldv_spin != 0) {
2032 {
2033#line 427
2034 ldv_blast_assert();
2035 }
2036 } else {
2037
2038 }
2039#line 430
2040 return;
2041}
2042}
2043#line 431 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4912/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2760.c.p"
2044void ldv_spin_lock(void)
2045{
2046
2047 {
2048#line 434
2049 ldv_spin = 1;
2050#line 435
2051 return;
2052}
2053}
2054#line 438 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4912/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2760.c.p"
2055void ldv_spin_unlock(void)
2056{
2057
2058 {
2059#line 441
2060 ldv_spin = 0;
2061#line 442
2062 return;
2063}
2064}
2065#line 445 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4912/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2760.c.p"
2066int ldv_spin_trylock(void)
2067{ int is_lock ;
2068
2069 {
2070 {
2071#line 450
2072 is_lock = __VERIFIER_nondet_int();
2073 }
2074#line 452
2075 if (is_lock != 0) {
2076#line 455
2077 return (0);
2078 } else {
2079#line 460
2080 ldv_spin = 1;
2081#line 462
2082 return (1);
2083 }
2084}
2085}
2086#line 629 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4912/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2760.c.p"
2087void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 )
2088{
2089
2090 {
2091 {
2092#line 635
2093 ldv_check_alloc_flags(ldv_func_arg2);
2094#line 637
2095 kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
2096 }
2097#line 638
2098 return ((void *)0);
2099}
2100}