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 152 "include/linux/mutex.h"
946void mutex_lock(struct mutex *lock ) ;
947#line 153
948int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock ) ;
949#line 154
950int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock ) ;
951#line 168
952int mutex_trylock(struct mutex *lock ) ;
953#line 169
954void mutex_unlock(struct mutex *lock ) ;
955#line 170
956int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
957#line 67 "include/linux/module.h"
958int init_module(void) ;
959#line 68
960void cleanup_module(void) ;
961#line 69 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1_family.h"
962extern void w1_unregister_family(struct w1_family * ) ;
963#line 70
964extern int w1_register_family(struct w1_family * ) ;
965#line 35 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12361/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_smem.c.common.c"
966static char const __mod_license35[12] __attribute__((__used__, __unused__, __section__(".modinfo"),
967__aligned__(1))) =
968#line 35 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12361/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_smem.c.common.c"
969 { (char const )'l', (char const )'i', (char const )'c', (char const )'e',
970 (char const )'n', (char const )'s', (char const )'e', (char const )'=',
971 (char const )'G', (char const )'P', (char const )'L', (char const )'\000'};
972#line 36 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12361/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_smem.c.common.c"
973static char const __mod_author36[42] __attribute__((__used__, __unused__, __section__(".modinfo"),
974__aligned__(1))) =
975#line 36
976 { (char const )'a', (char const )'u', (char const )'t', (char const )'h',
977 (char const )'o', (char const )'r', (char const )'=', (char const )'E',
978 (char const )'v', (char const )'g', (char const )'e', (char const )'n',
979 (char const )'i', (char const )'y', (char const )' ', (char const )'P',
980 (char const )'o', (char const )'l', (char const )'y', (char const )'a',
981 (char const )'k', (char const )'o', (char const )'v', (char const )' ',
982 (char const )'<', (char const )'z', (char const )'b', (char const )'r',
983 (char const )'@', (char const )'i', (char const )'o', (char const )'r',
984 (char const )'e', (char const )'m', (char const )'a', (char const )'p',
985 (char const )'.', (char const )'n', (char const )'e', (char const )'t',
986 (char const )'>', (char const )'\000'};
987#line 37 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12361/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_smem.c.common.c"
988static char const __mod_description37[76] __attribute__((__used__, __unused__,
989__section__(".modinfo"), __aligned__(1))) =
990#line 37
991 { (char const )'d', (char const )'e', (char const )'s', (char const )'c',
992 (char const )'r', (char const )'i', (char const )'p', (char const )'t',
993 (char const )'i', (char const )'o', (char const )'n', (char const )'=',
994 (char const )'D', (char const )'r', (char const )'i', (char const )'v',
995 (char const )'e', (char const )'r', (char const )' ', (char const )'f',
996 (char const )'o', (char const )'r', (char const )' ', (char const )'1',
997 (char const )'-', (char const )'w', (char const )'i', (char const )'r',
998 (char const )'e', (char const )' ', (char const )'D', (char const )'a',
999 (char const )'l', (char const )'l', (char const )'a', (char const )'s',
1000 (char const )' ', (char const )'n', (char const )'e', (char const )'t',
1001 (char const )'w', (char const )'o', (char const )'r', (char const )'k',
1002 (char const )' ', (char const )'p', (char const )'r', (char const )'o',
1003 (char const )'t', (char const )'o', (char const )'c', (char const )'o',
1004 (char const )'l', (char const )',', (char const )' ', (char const )'6',
1005 (char const )'4', (char const )'b', (char const )'i', (char const )'t',
1006 (char const )' ', (char const )'m', (char const )'e', (char const )'m',
1007 (char const )'o', (char const )'r', (char const )'y', (char const )' ',
1008 (char const )'f', (char const )'a', (char const )'m', (char const )'i',
1009 (char const )'l', (char const )'y', (char const )'.', (char const )'\000'};
1010#line 39 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12361/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_smem.c.common.c"
1011static struct w1_family w1_smem_family_01 = {{(struct list_head *)0, (struct list_head *)0}, (u8 )1, (struct w1_family_ops *)0,
1012 {0}};
1013#line 43 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12361/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_smem.c.common.c"
1014static struct w1_family w1_smem_family_81 = {{(struct list_head *)0, (struct list_head *)0}, (u8 )129, (struct w1_family_ops *)0,
1015 {0}};
1016#line 47
1017static int w1_smem_init(void) __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
1018#line 47 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12361/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_smem.c.common.c"
1019static int w1_smem_init(void)
1020{ int err ;
1021
1022 {
1023 {
1024#line 51
1025 err = w1_register_family(& w1_smem_family_01);
1026 }
1027#line 52
1028 if (err) {
1029#line 53
1030 return (err);
1031 } else {
1032
1033 }
1034 {
1035#line 55
1036 err = w1_register_family(& w1_smem_family_81);
1037 }
1038#line 56
1039 if (err) {
1040 {
1041#line 57
1042 w1_unregister_family(& w1_smem_family_01);
1043 }
1044#line 58
1045 return (err);
1046 } else {
1047
1048 }
1049#line 61
1050 return (0);
1051}
1052}
1053#line 64
1054static void w1_smem_fini(void) __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
1055#line 64 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12361/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_smem.c.common.c"
1056static void w1_smem_fini(void)
1057{
1058
1059 {
1060 {
1061#line 66
1062 w1_unregister_family(& w1_smem_family_01);
1063#line 67
1064 w1_unregister_family(& w1_smem_family_81);
1065 }
1066#line 68
1067 return;
1068}
1069}
1070#line 70 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12361/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_smem.c.common.c"
1071int init_module(void)
1072{ int tmp ;
1073
1074 {
1075 {
1076#line 70
1077 tmp = w1_smem_init();
1078 }
1079#line 70
1080 return (tmp);
1081}
1082}
1083#line 71 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12361/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_smem.c.common.c"
1084void cleanup_module(void)
1085{
1086
1087 {
1088 {
1089#line 71
1090 w1_smem_fini();
1091 }
1092#line 71
1093 return;
1094}
1095}
1096#line 89
1097void ldv_check_final_state(void) ;
1098#line 95
1099extern void ldv_initialize(void) ;
1100#line 98
1101extern int __VERIFIER_nondet_int(void) ;
1102#line 101 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12361/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_smem.c.common.c"
1103int LDV_IN_INTERRUPT ;
1104#line 104 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12361/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_smem.c.common.c"
1105void main(void)
1106{ int tmp ;
1107 int tmp___0 ;
1108 int tmp___1 ;
1109
1110 {
1111 {
1112#line 116
1113 LDV_IN_INTERRUPT = 1;
1114#line 125
1115 ldv_initialize();
1116#line 131
1117 tmp = w1_smem_init();
1118 }
1119#line 131
1120 if (tmp) {
1121#line 132
1122 goto ldv_final;
1123 } else {
1124
1125 }
1126 {
1127#line 134
1128 while (1) {
1129 while_continue: ;
1130 {
1131#line 134
1132 tmp___1 = __VERIFIER_nondet_int();
1133 }
1134#line 134
1135 if (tmp___1) {
1136
1137 } else {
1138#line 134
1139 goto while_break;
1140 }
1141 {
1142#line 137
1143 tmp___0 = __VERIFIER_nondet_int();
1144 }
1145 {
1146#line 139
1147 goto switch_default;
1148#line 137
1149 if (0) {
1150 switch_default:
1151#line 139
1152 goto switch_break;
1153 } else {
1154 switch_break: ;
1155 }
1156 }
1157 }
1158 while_break: ;
1159 }
1160 {
1161#line 151
1162 w1_smem_fini();
1163 }
1164 ldv_final:
1165 {
1166#line 154
1167 ldv_check_final_state();
1168 }
1169#line 157
1170 return;
1171}
1172}
1173#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12361/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
1174void ldv_blast_assert(void)
1175{
1176
1177 {
1178 ERROR:
1179#line 6
1180 goto ERROR;
1181}
1182}
1183#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12361/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
1184extern int __VERIFIER_nondet_int(void) ;
1185#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12361/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1186int ldv_mutex = 1;
1187#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12361/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1188int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )
1189{ int nondetermined ;
1190
1191 {
1192#line 29
1193 if (ldv_mutex == 1) {
1194
1195 } else {
1196 {
1197#line 29
1198 ldv_blast_assert();
1199 }
1200 }
1201 {
1202#line 32
1203 nondetermined = __VERIFIER_nondet_int();
1204 }
1205#line 35
1206 if (nondetermined) {
1207#line 38
1208 ldv_mutex = 2;
1209#line 40
1210 return (0);
1211 } else {
1212#line 45
1213 return (-4);
1214 }
1215}
1216}
1217#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12361/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1218int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock )
1219{ int nondetermined ;
1220
1221 {
1222#line 57
1223 if (ldv_mutex == 1) {
1224
1225 } else {
1226 {
1227#line 57
1228 ldv_blast_assert();
1229 }
1230 }
1231 {
1232#line 60
1233 nondetermined = __VERIFIER_nondet_int();
1234 }
1235#line 63
1236 if (nondetermined) {
1237#line 66
1238 ldv_mutex = 2;
1239#line 68
1240 return (0);
1241 } else {
1242#line 73
1243 return (-4);
1244 }
1245}
1246}
1247#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12361/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1248int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock )
1249{ int atomic_value_after_dec ;
1250
1251 {
1252#line 83
1253 if (ldv_mutex == 1) {
1254
1255 } else {
1256 {
1257#line 83
1258 ldv_blast_assert();
1259 }
1260 }
1261 {
1262#line 86
1263 atomic_value_after_dec = __VERIFIER_nondet_int();
1264 }
1265#line 89
1266 if (atomic_value_after_dec == 0) {
1267#line 92
1268 ldv_mutex = 2;
1269#line 94
1270 return (1);
1271 } else {
1272
1273 }
1274#line 98
1275 return (0);
1276}
1277}
1278#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12361/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1279void mutex_lock(struct mutex *lock )
1280{
1281
1282 {
1283#line 108
1284 if (ldv_mutex == 1) {
1285
1286 } else {
1287 {
1288#line 108
1289 ldv_blast_assert();
1290 }
1291 }
1292#line 110
1293 ldv_mutex = 2;
1294#line 111
1295 return;
1296}
1297}
1298#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12361/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1299int mutex_trylock(struct mutex *lock )
1300{ int nondetermined ;
1301
1302 {
1303#line 121
1304 if (ldv_mutex == 1) {
1305
1306 } else {
1307 {
1308#line 121
1309 ldv_blast_assert();
1310 }
1311 }
1312 {
1313#line 124
1314 nondetermined = __VERIFIER_nondet_int();
1315 }
1316#line 127
1317 if (nondetermined) {
1318#line 130
1319 ldv_mutex = 2;
1320#line 132
1321 return (1);
1322 } else {
1323#line 137
1324 return (0);
1325 }
1326}
1327}
1328#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12361/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1329void mutex_unlock(struct mutex *lock )
1330{
1331
1332 {
1333#line 147
1334 if (ldv_mutex == 2) {
1335
1336 } else {
1337 {
1338#line 147
1339 ldv_blast_assert();
1340 }
1341 }
1342#line 149
1343 ldv_mutex = 1;
1344#line 150
1345 return;
1346}
1347}
1348#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12361/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1349void ldv_check_final_state(void)
1350{
1351
1352 {
1353#line 156
1354 if (ldv_mutex == 1) {
1355
1356 } else {
1357 {
1358#line 156
1359 ldv_blast_assert();
1360 }
1361 }
1362#line 157
1363 return;
1364}
1365}
1366#line 166 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12361/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_smem.c.common.c"
1367long s__builtin_expect(long val , long res )
1368{
1369
1370 {
1371#line 167
1372 return (val);
1373}
1374}