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