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