1
2
3
4#line 23 "include/asm-generic/int-ll64.h"
5typedef unsigned short __u16;
6#line 25 "include/asm-generic/int-ll64.h"
7typedef int __s32;
8#line 26 "include/asm-generic/int-ll64.h"
9typedef unsigned int __u32;
10#line 29 "include/asm-generic/int-ll64.h"
11typedef long long __s64;
12#line 30 "include/asm-generic/int-ll64.h"
13typedef unsigned long long __u64;
14#line 45 "include/asm-generic/int-ll64.h"
15typedef short s16;
16#line 46 "include/asm-generic/int-ll64.h"
17typedef unsigned short u16;
18#line 49 "include/asm-generic/int-ll64.h"
19typedef unsigned int u32;
20#line 51 "include/asm-generic/int-ll64.h"
21typedef long long s64;
22#line 52 "include/asm-generic/int-ll64.h"
23typedef unsigned long long u64;
24#line 14 "include/asm-generic/posix_types.h"
25typedef long __kernel_long_t;
26#line 15 "include/asm-generic/posix_types.h"
27typedef unsigned long __kernel_ulong_t;
28#line 75 "include/asm-generic/posix_types.h"
29typedef __kernel_ulong_t __kernel_size_t;
30#line 76 "include/asm-generic/posix_types.h"
31typedef __kernel_long_t __kernel_ssize_t;
32#line 91 "include/asm-generic/posix_types.h"
33typedef long long __kernel_loff_t;
34#line 92 "include/asm-generic/posix_types.h"
35typedef __kernel_long_t __kernel_time_t;
36#line 21 "include/linux/types.h"
37typedef __u32 __kernel_dev_t;
38#line 24 "include/linux/types.h"
39typedef __kernel_dev_t dev_t;
40#line 27 "include/linux/types.h"
41typedef unsigned short umode_t;
42#line 38 "include/linux/types.h"
43typedef _Bool bool;
44#line 54 "include/linux/types.h"
45typedef __kernel_loff_t loff_t;
46#line 63 "include/linux/types.h"
47typedef __kernel_size_t size_t;
48#line 68 "include/linux/types.h"
49typedef __kernel_ssize_t ssize_t;
50#line 219 "include/linux/types.h"
51struct __anonstruct_atomic_t_7 {
52 int counter ;
53};
54#line 219 "include/linux/types.h"
55typedef struct __anonstruct_atomic_t_7 atomic_t;
56#line 224 "include/linux/types.h"
57struct __anonstruct_atomic64_t_8 {
58 long counter ;
59};
60#line 224 "include/linux/types.h"
61typedef struct __anonstruct_atomic64_t_8 atomic64_t;
62#line 229 "include/linux/types.h"
63struct list_head {
64 struct list_head *next ;
65 struct list_head *prev ;
66};
67#line 56 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
68struct module;
69#line 56
70struct module;
71#line 146 "include/linux/init.h"
72typedef void (*ctor_fn_t)(void);
73#line 47 "include/linux/dynamic_debug.h"
74struct device;
75#line 47
76struct device;
77#line 135 "include/linux/kernel.h"
78struct completion;
79#line 135
80struct completion;
81#line 12 "include/linux/thread_info.h"
82struct timespec;
83#line 12
84struct timespec;
85#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
86struct task_struct;
87#line 20
88struct task_struct;
89#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
90struct task_struct;
91#line 295 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
92struct file;
93#line 295
94struct file;
95#line 52 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
96struct task_struct;
97#line 329
98struct arch_spinlock;
99#line 329
100struct arch_spinlock;
101#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
102struct task_struct;
103#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
104struct task_struct;
105#line 10 "include/asm-generic/bug.h"
106struct bug_entry {
107 int bug_addr_disp ;
108 int file_disp ;
109 unsigned short line ;
110 unsigned short flags ;
111};
112#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
113struct static_key;
114#line 234
115struct static_key;
116#line 23 "include/asm-generic/atomic-long.h"
117typedef atomic64_t atomic_long_t;
118#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
119typedef u16 __ticket_t;
120#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
121typedef u32 __ticketpair_t;
122#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
123struct __raw_tickets {
124 __ticket_t head ;
125 __ticket_t tail ;
126};
127#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
128union __anonunion____missing_field_name_36 {
129 __ticketpair_t head_tail ;
130 struct __raw_tickets tickets ;
131};
132#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
133struct arch_spinlock {
134 union __anonunion____missing_field_name_36 __annonCompField17 ;
135};
136#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
137typedef struct arch_spinlock arch_spinlock_t;
138#line 12 "include/linux/lockdep.h"
139struct task_struct;
140#line 391 "include/linux/lockdep.h"
141struct lock_class_key {
142
143};
144#line 20 "include/linux/spinlock_types.h"
145struct raw_spinlock {
146 arch_spinlock_t raw_lock ;
147 unsigned int magic ;
148 unsigned int owner_cpu ;
149 void *owner ;
150};
151#line 64 "include/linux/spinlock_types.h"
152union __anonunion____missing_field_name_39 {
153 struct raw_spinlock rlock ;
154};
155#line 64 "include/linux/spinlock_types.h"
156struct spinlock {
157 union __anonunion____missing_field_name_39 __annonCompField19 ;
158};
159#line 64 "include/linux/spinlock_types.h"
160typedef struct spinlock spinlock_t;
161#line 14 "include/linux/time.h"
162struct timespec {
163 __kernel_time_t tv_sec ;
164 long tv_nsec ;
165};
166#line 49 "include/linux/wait.h"
167struct __wait_queue_head {
168 spinlock_t lock ;
169 struct list_head task_list ;
170};
171#line 53 "include/linux/wait.h"
172typedef struct __wait_queue_head wait_queue_head_t;
173#line 55
174struct task_struct;
175#line 48 "include/linux/mutex.h"
176struct mutex {
177 atomic_t count ;
178 spinlock_t wait_lock ;
179 struct list_head wait_list ;
180 struct task_struct *owner ;
181 char const *name ;
182 void *magic ;
183};
184#line 25 "include/linux/completion.h"
185struct completion {
186 unsigned int done ;
187 wait_queue_head_t wait ;
188};
189#line 202 "include/linux/ioport.h"
190struct device;
191#line 103 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mpspec.h"
192struct device;
193#line 46 "include/linux/ktime.h"
194union ktime {
195 s64 tv64 ;
196};
197#line 59 "include/linux/ktime.h"
198typedef union ktime ktime_t;
199#line 10 "include/linux/timer.h"
200struct tvec_base;
201#line 10
202struct tvec_base;
203#line 12 "include/linux/timer.h"
204struct timer_list {
205 struct list_head entry ;
206 unsigned long expires ;
207 struct tvec_base *base ;
208 void (*function)(unsigned long ) ;
209 unsigned long data ;
210 int slack ;
211 int start_pid ;
212 void *start_site ;
213 char start_comm[16] ;
214};
215#line 17 "include/linux/workqueue.h"
216struct work_struct;
217#line 17
218struct work_struct;
219#line 79 "include/linux/workqueue.h"
220struct work_struct {
221 atomic_long_t data ;
222 struct list_head entry ;
223 void (*func)(struct work_struct *work ) ;
224};
225#line 42 "include/linux/pm.h"
226struct device;
227#line 50 "include/linux/pm.h"
228struct pm_message {
229 int event ;
230};
231#line 50 "include/linux/pm.h"
232typedef struct pm_message pm_message_t;
233#line 264 "include/linux/pm.h"
234struct dev_pm_ops {
235 int (*prepare)(struct device *dev ) ;
236 void (*complete)(struct device *dev ) ;
237 int (*suspend)(struct device *dev ) ;
238 int (*resume)(struct device *dev ) ;
239 int (*freeze)(struct device *dev ) ;
240 int (*thaw)(struct device *dev ) ;
241 int (*poweroff)(struct device *dev ) ;
242 int (*restore)(struct device *dev ) ;
243 int (*suspend_late)(struct device *dev ) ;
244 int (*resume_early)(struct device *dev ) ;
245 int (*freeze_late)(struct device *dev ) ;
246 int (*thaw_early)(struct device *dev ) ;
247 int (*poweroff_late)(struct device *dev ) ;
248 int (*restore_early)(struct device *dev ) ;
249 int (*suspend_noirq)(struct device *dev ) ;
250 int (*resume_noirq)(struct device *dev ) ;
251 int (*freeze_noirq)(struct device *dev ) ;
252 int (*thaw_noirq)(struct device *dev ) ;
253 int (*poweroff_noirq)(struct device *dev ) ;
254 int (*restore_noirq)(struct device *dev ) ;
255 int (*runtime_suspend)(struct device *dev ) ;
256 int (*runtime_resume)(struct device *dev ) ;
257 int (*runtime_idle)(struct device *dev ) ;
258};
259#line 458
260enum rpm_status {
261 RPM_ACTIVE = 0,
262 RPM_RESUMING = 1,
263 RPM_SUSPENDED = 2,
264 RPM_SUSPENDING = 3
265} ;
266#line 480
267enum rpm_request {
268 RPM_REQ_NONE = 0,
269 RPM_REQ_IDLE = 1,
270 RPM_REQ_SUSPEND = 2,
271 RPM_REQ_AUTOSUSPEND = 3,
272 RPM_REQ_RESUME = 4
273} ;
274#line 488
275struct wakeup_source;
276#line 488
277struct wakeup_source;
278#line 495 "include/linux/pm.h"
279struct pm_subsys_data {
280 spinlock_t lock ;
281 unsigned int refcount ;
282};
283#line 506
284struct dev_pm_qos_request;
285#line 506
286struct pm_qos_constraints;
287#line 506 "include/linux/pm.h"
288struct dev_pm_info {
289 pm_message_t power_state ;
290 unsigned int can_wakeup : 1 ;
291 unsigned int async_suspend : 1 ;
292 bool is_prepared : 1 ;
293 bool is_suspended : 1 ;
294 bool ignore_children : 1 ;
295 spinlock_t lock ;
296 struct list_head entry ;
297 struct completion completion ;
298 struct wakeup_source *wakeup ;
299 bool wakeup_path : 1 ;
300 struct timer_list suspend_timer ;
301 unsigned long timer_expires ;
302 struct work_struct work ;
303 wait_queue_head_t wait_queue ;
304 atomic_t usage_count ;
305 atomic_t child_count ;
306 unsigned int disable_depth : 3 ;
307 unsigned int idle_notification : 1 ;
308 unsigned int request_pending : 1 ;
309 unsigned int deferred_resume : 1 ;
310 unsigned int run_wake : 1 ;
311 unsigned int runtime_auto : 1 ;
312 unsigned int no_callbacks : 1 ;
313 unsigned int irq_safe : 1 ;
314 unsigned int use_autosuspend : 1 ;
315 unsigned int timer_autosuspends : 1 ;
316 enum rpm_request request ;
317 enum rpm_status runtime_status ;
318 int runtime_error ;
319 int autosuspend_delay ;
320 unsigned long last_busy ;
321 unsigned long active_jiffies ;
322 unsigned long suspended_jiffies ;
323 unsigned long accounting_timestamp ;
324 ktime_t suspend_time ;
325 s64 max_time_suspended_ns ;
326 struct dev_pm_qos_request *pq_req ;
327 struct pm_subsys_data *subsys_data ;
328 struct pm_qos_constraints *constraints ;
329};
330#line 564 "include/linux/pm.h"
331struct dev_pm_domain {
332 struct dev_pm_ops ops ;
333};
334#line 8 "include/linux/vmalloc.h"
335struct vm_area_struct;
336#line 8
337struct vm_area_struct;
338#line 10 "include/linux/gfp.h"
339struct vm_area_struct;
340#line 29 "include/linux/sysctl.h"
341struct completion;
342#line 49 "include/linux/kmod.h"
343struct file;
344#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
345struct task_struct;
346#line 18 "include/linux/elf.h"
347typedef __u64 Elf64_Addr;
348#line 19 "include/linux/elf.h"
349typedef __u16 Elf64_Half;
350#line 23 "include/linux/elf.h"
351typedef __u32 Elf64_Word;
352#line 24 "include/linux/elf.h"
353typedef __u64 Elf64_Xword;
354#line 194 "include/linux/elf.h"
355struct elf64_sym {
356 Elf64_Word st_name ;
357 unsigned char st_info ;
358 unsigned char st_other ;
359 Elf64_Half st_shndx ;
360 Elf64_Addr st_value ;
361 Elf64_Xword st_size ;
362};
363#line 194 "include/linux/elf.h"
364typedef struct elf64_sym Elf64_Sym;
365#line 438
366struct file;
367#line 20 "include/linux/kobject_ns.h"
368struct sock;
369#line 20
370struct sock;
371#line 21
372struct kobject;
373#line 21
374struct kobject;
375#line 27
376enum kobj_ns_type {
377 KOBJ_NS_TYPE_NONE = 0,
378 KOBJ_NS_TYPE_NET = 1,
379 KOBJ_NS_TYPES = 2
380} ;
381#line 40 "include/linux/kobject_ns.h"
382struct kobj_ns_type_operations {
383 enum kobj_ns_type type ;
384 void *(*grab_current_ns)(void) ;
385 void const *(*netlink_ns)(struct sock *sk ) ;
386 void const *(*initial_ns)(void) ;
387 void (*drop_ns)(void * ) ;
388};
389#line 22 "include/linux/sysfs.h"
390struct kobject;
391#line 23
392struct module;
393#line 24
394enum kobj_ns_type;
395#line 26 "include/linux/sysfs.h"
396struct attribute {
397 char const *name ;
398 umode_t mode ;
399};
400#line 56 "include/linux/sysfs.h"
401struct attribute_group {
402 char const *name ;
403 umode_t (*is_visible)(struct kobject * , struct attribute * , int ) ;
404 struct attribute **attrs ;
405};
406#line 85
407struct file;
408#line 86
409struct vm_area_struct;
410#line 88 "include/linux/sysfs.h"
411struct bin_attribute {
412 struct attribute attr ;
413 size_t size ;
414 void *private ;
415 ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
416 loff_t , size_t ) ;
417 ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
418 loff_t , size_t ) ;
419 int (*mmap)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ) ;
420};
421#line 112 "include/linux/sysfs.h"
422struct sysfs_ops {
423 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
424 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
425 void const *(*namespace)(struct kobject * , struct attribute const * ) ;
426};
427#line 118
428struct sysfs_dirent;
429#line 118
430struct sysfs_dirent;
431#line 22 "include/linux/kref.h"
432struct kref {
433 atomic_t refcount ;
434};
435#line 60 "include/linux/kobject.h"
436struct kset;
437#line 60
438struct kobj_type;
439#line 60 "include/linux/kobject.h"
440struct kobject {
441 char const *name ;
442 struct list_head entry ;
443 struct kobject *parent ;
444 struct kset *kset ;
445 struct kobj_type *ktype ;
446 struct sysfs_dirent *sd ;
447 struct kref kref ;
448 unsigned int state_initialized : 1 ;
449 unsigned int state_in_sysfs : 1 ;
450 unsigned int state_add_uevent_sent : 1 ;
451 unsigned int state_remove_uevent_sent : 1 ;
452 unsigned int uevent_suppress : 1 ;
453};
454#line 108 "include/linux/kobject.h"
455struct kobj_type {
456 void (*release)(struct kobject *kobj ) ;
457 struct sysfs_ops const *sysfs_ops ;
458 struct attribute **default_attrs ;
459 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject *kobj ) ;
460 void const *(*namespace)(struct kobject *kobj ) ;
461};
462#line 116 "include/linux/kobject.h"
463struct kobj_uevent_env {
464 char *envp[32] ;
465 int envp_idx ;
466 char buf[2048] ;
467 int buflen ;
468};
469#line 123 "include/linux/kobject.h"
470struct kset_uevent_ops {
471 int (* const filter)(struct kset *kset , struct kobject *kobj ) ;
472 char const *(* const name)(struct kset *kset , struct kobject *kobj ) ;
473 int (* const uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
474};
475#line 140
476struct sock;
477#line 159 "include/linux/kobject.h"
478struct kset {
479 struct list_head list ;
480 spinlock_t list_lock ;
481 struct kobject kobj ;
482 struct kset_uevent_ops const *uevent_ops ;
483};
484#line 39 "include/linux/moduleparam.h"
485struct kernel_param;
486#line 39
487struct kernel_param;
488#line 41 "include/linux/moduleparam.h"
489struct kernel_param_ops {
490 int (*set)(char const *val , struct kernel_param const *kp ) ;
491 int (*get)(char *buffer , struct kernel_param const *kp ) ;
492 void (*free)(void *arg ) ;
493};
494#line 50
495struct kparam_string;
496#line 50
497struct kparam_array;
498#line 50 "include/linux/moduleparam.h"
499union __anonunion____missing_field_name_199 {
500 void *arg ;
501 struct kparam_string const *str ;
502 struct kparam_array const *arr ;
503};
504#line 50 "include/linux/moduleparam.h"
505struct kernel_param {
506 char const *name ;
507 struct kernel_param_ops const *ops ;
508 u16 perm ;
509 s16 level ;
510 union __anonunion____missing_field_name_199 __annonCompField32 ;
511};
512#line 63 "include/linux/moduleparam.h"
513struct kparam_string {
514 unsigned int maxlen ;
515 char *string ;
516};
517#line 69 "include/linux/moduleparam.h"
518struct kparam_array {
519 unsigned int max ;
520 unsigned int elemsize ;
521 unsigned int *num ;
522 struct kernel_param_ops const *ops ;
523 void *elem ;
524};
525#line 445
526struct module;
527#line 80 "include/linux/jump_label.h"
528struct module;
529#line 143 "include/linux/jump_label.h"
530struct static_key {
531 atomic_t enabled ;
532};
533#line 22 "include/linux/tracepoint.h"
534struct module;
535#line 23
536struct tracepoint;
537#line 23
538struct tracepoint;
539#line 25 "include/linux/tracepoint.h"
540struct tracepoint_func {
541 void *func ;
542 void *data ;
543};
544#line 30 "include/linux/tracepoint.h"
545struct tracepoint {
546 char const *name ;
547 struct static_key key ;
548 void (*regfunc)(void) ;
549 void (*unregfunc)(void) ;
550 struct tracepoint_func *funcs ;
551};
552#line 19 "include/linux/export.h"
553struct kernel_symbol {
554 unsigned long value ;
555 char const *name ;
556};
557#line 8 "include/asm-generic/module.h"
558struct mod_arch_specific {
559
560};
561#line 35 "include/linux/module.h"
562struct module;
563#line 37
564struct module_param_attrs;
565#line 37 "include/linux/module.h"
566struct module_kobject {
567 struct kobject kobj ;
568 struct module *mod ;
569 struct kobject *drivers_dir ;
570 struct module_param_attrs *mp ;
571};
572#line 44 "include/linux/module.h"
573struct module_attribute {
574 struct attribute attr ;
575 ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
576 ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const * ,
577 size_t count ) ;
578 void (*setup)(struct module * , char const * ) ;
579 int (*test)(struct module * ) ;
580 void (*free)(struct module * ) ;
581};
582#line 71
583struct exception_table_entry;
584#line 71
585struct exception_table_entry;
586#line 199
587enum module_state {
588 MODULE_STATE_LIVE = 0,
589 MODULE_STATE_COMING = 1,
590 MODULE_STATE_GOING = 2
591} ;
592#line 215 "include/linux/module.h"
593struct module_ref {
594 unsigned long incs ;
595 unsigned long decs ;
596} __attribute__((__aligned__((2) * (sizeof(unsigned long )) ))) ;
597#line 220
598struct module_sect_attrs;
599#line 220
600struct module_notes_attrs;
601#line 220
602struct ftrace_event_call;
603#line 220 "include/linux/module.h"
604struct module {
605 enum module_state state ;
606 struct list_head list ;
607 char name[64UL - sizeof(unsigned long )] ;
608 struct module_kobject mkobj ;
609 struct module_attribute *modinfo_attrs ;
610 char const *version ;
611 char const *srcversion ;
612 struct kobject *holders_dir ;
613 struct kernel_symbol const *syms ;
614 unsigned long const *crcs ;
615 unsigned int num_syms ;
616 struct kernel_param *kp ;
617 unsigned int num_kp ;
618 unsigned int num_gpl_syms ;
619 struct kernel_symbol const *gpl_syms ;
620 unsigned long const *gpl_crcs ;
621 struct kernel_symbol const *unused_syms ;
622 unsigned long const *unused_crcs ;
623 unsigned int num_unused_syms ;
624 unsigned int num_unused_gpl_syms ;
625 struct kernel_symbol const *unused_gpl_syms ;
626 unsigned long const *unused_gpl_crcs ;
627 struct kernel_symbol const *gpl_future_syms ;
628 unsigned long const *gpl_future_crcs ;
629 unsigned int num_gpl_future_syms ;
630 unsigned int num_exentries ;
631 struct exception_table_entry *extable ;
632 int (*init)(void) ;
633 void *module_init ;
634 void *module_core ;
635 unsigned int init_size ;
636 unsigned int core_size ;
637 unsigned int init_text_size ;
638 unsigned int core_text_size ;
639 unsigned int init_ro_size ;
640 unsigned int core_ro_size ;
641 struct mod_arch_specific arch ;
642 unsigned int taints ;
643 unsigned int num_bugs ;
644 struct list_head bug_list ;
645 struct bug_entry *bug_table ;
646 Elf64_Sym *symtab ;
647 Elf64_Sym *core_symtab ;
648 unsigned int num_symtab ;
649 unsigned int core_num_syms ;
650 char *strtab ;
651 char *core_strtab ;
652 struct module_sect_attrs *sect_attrs ;
653 struct module_notes_attrs *notes_attrs ;
654 char *args ;
655 void *percpu ;
656 unsigned int percpu_size ;
657 unsigned int num_tracepoints ;
658 struct tracepoint * const *tracepoints_ptrs ;
659 unsigned int num_trace_bprintk_fmt ;
660 char const **trace_bprintk_fmt_start ;
661 struct ftrace_event_call **trace_events ;
662 unsigned int num_trace_events ;
663 struct list_head source_list ;
664 struct list_head target_list ;
665 struct task_struct *waiter ;
666 void (*exit)(void) ;
667 struct module_ref *refptr ;
668 ctor_fn_t *ctors ;
669 unsigned int num_ctors ;
670};
671#line 53 "include/linux/pps.h"
672struct pps_ktime {
673 __s64 sec ;
674 __s32 nsec ;
675 __u32 flags ;
676};
677#line 68 "include/linux/pps.h"
678struct pps_kparams {
679 int api_version ;
680 int mode ;
681 struct pps_ktime assert_off_tu ;
682 struct pps_ktime clear_off_tu ;
683};
684#line 8 "include/linux/cdev.h"
685struct file_operations;
686#line 8
687struct file_operations;
688#line 10
689struct module;
690#line 12 "include/linux/cdev.h"
691struct cdev {
692 struct kobject kobj ;
693 struct module *owner ;
694 struct file_operations const *ops ;
695 struct list_head list ;
696 dev_t dev ;
697 unsigned int count ;
698};
699#line 19 "include/linux/klist.h"
700struct klist_node;
701#line 19
702struct klist_node;
703#line 39 "include/linux/klist.h"
704struct klist_node {
705 void *n_klist ;
706 struct list_head n_node ;
707 struct kref n_ref ;
708};
709#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
710struct dma_map_ops;
711#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
712struct dev_archdata {
713 void *acpi_handle ;
714 struct dma_map_ops *dma_ops ;
715 void *iommu ;
716};
717#line 28 "include/linux/device.h"
718struct device;
719#line 29
720struct device_private;
721#line 29
722struct device_private;
723#line 30
724struct device_driver;
725#line 30
726struct device_driver;
727#line 31
728struct driver_private;
729#line 31
730struct driver_private;
731#line 32
732struct module;
733#line 33
734struct class;
735#line 33
736struct class;
737#line 34
738struct subsys_private;
739#line 34
740struct subsys_private;
741#line 35
742struct bus_type;
743#line 35
744struct bus_type;
745#line 36
746struct device_node;
747#line 36
748struct device_node;
749#line 37
750struct iommu_ops;
751#line 37
752struct iommu_ops;
753#line 39 "include/linux/device.h"
754struct bus_attribute {
755 struct attribute attr ;
756 ssize_t (*show)(struct bus_type *bus , char *buf ) ;
757 ssize_t (*store)(struct bus_type *bus , char const *buf , size_t count ) ;
758};
759#line 89
760struct device_attribute;
761#line 89
762struct driver_attribute;
763#line 89 "include/linux/device.h"
764struct bus_type {
765 char const *name ;
766 char const *dev_name ;
767 struct device *dev_root ;
768 struct bus_attribute *bus_attrs ;
769 struct device_attribute *dev_attrs ;
770 struct driver_attribute *drv_attrs ;
771 int (*match)(struct device *dev , struct device_driver *drv ) ;
772 int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
773 int (*probe)(struct device *dev ) ;
774 int (*remove)(struct device *dev ) ;
775 void (*shutdown)(struct device *dev ) ;
776 int (*suspend)(struct device *dev , pm_message_t state ) ;
777 int (*resume)(struct device *dev ) ;
778 struct dev_pm_ops const *pm ;
779 struct iommu_ops *iommu_ops ;
780 struct subsys_private *p ;
781};
782#line 127
783struct device_type;
784#line 214
785struct of_device_id;
786#line 214 "include/linux/device.h"
787struct device_driver {
788 char const *name ;
789 struct bus_type *bus ;
790 struct module *owner ;
791 char const *mod_name ;
792 bool suppress_bind_attrs ;
793 struct of_device_id const *of_match_table ;
794 int (*probe)(struct device *dev ) ;
795 int (*remove)(struct device *dev ) ;
796 void (*shutdown)(struct device *dev ) ;
797 int (*suspend)(struct device *dev , pm_message_t state ) ;
798 int (*resume)(struct device *dev ) ;
799 struct attribute_group const **groups ;
800 struct dev_pm_ops const *pm ;
801 struct driver_private *p ;
802};
803#line 249 "include/linux/device.h"
804struct driver_attribute {
805 struct attribute attr ;
806 ssize_t (*show)(struct device_driver *driver , char *buf ) ;
807 ssize_t (*store)(struct device_driver *driver , char const *buf , size_t count ) ;
808};
809#line 330
810struct class_attribute;
811#line 330 "include/linux/device.h"
812struct class {
813 char const *name ;
814 struct module *owner ;
815 struct class_attribute *class_attrs ;
816 struct device_attribute *dev_attrs ;
817 struct bin_attribute *dev_bin_attrs ;
818 struct kobject *dev_kobj ;
819 int (*dev_uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
820 char *(*devnode)(struct device *dev , umode_t *mode ) ;
821 void (*class_release)(struct class *class ) ;
822 void (*dev_release)(struct device *dev ) ;
823 int (*suspend)(struct device *dev , pm_message_t state ) ;
824 int (*resume)(struct device *dev ) ;
825 struct kobj_ns_type_operations const *ns_type ;
826 void const *(*namespace)(struct device *dev ) ;
827 struct dev_pm_ops const *pm ;
828 struct subsys_private *p ;
829};
830#line 397 "include/linux/device.h"
831struct class_attribute {
832 struct attribute attr ;
833 ssize_t (*show)(struct class *class , struct class_attribute *attr , char *buf ) ;
834 ssize_t (*store)(struct class *class , struct class_attribute *attr , char const *buf ,
835 size_t count ) ;
836 void const *(*namespace)(struct class *class , struct class_attribute const *attr ) ;
837};
838#line 465 "include/linux/device.h"
839struct device_type {
840 char const *name ;
841 struct attribute_group const **groups ;
842 int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
843 char *(*devnode)(struct device *dev , umode_t *mode ) ;
844 void (*release)(struct device *dev ) ;
845 struct dev_pm_ops const *pm ;
846};
847#line 476 "include/linux/device.h"
848struct device_attribute {
849 struct attribute attr ;
850 ssize_t (*show)(struct device *dev , struct device_attribute *attr , char *buf ) ;
851 ssize_t (*store)(struct device *dev , struct device_attribute *attr , char const *buf ,
852 size_t count ) ;
853};
854#line 559 "include/linux/device.h"
855struct device_dma_parameters {
856 unsigned int max_segment_size ;
857 unsigned long segment_boundary_mask ;
858};
859#line 627
860struct dma_coherent_mem;
861#line 627 "include/linux/device.h"
862struct device {
863 struct device *parent ;
864 struct device_private *p ;
865 struct kobject kobj ;
866 char const *init_name ;
867 struct device_type const *type ;
868 struct mutex mutex ;
869 struct bus_type *bus ;
870 struct device_driver *driver ;
871 void *platform_data ;
872 struct dev_pm_info power ;
873 struct dev_pm_domain *pm_domain ;
874 int numa_node ;
875 u64 *dma_mask ;
876 u64 coherent_dma_mask ;
877 struct device_dma_parameters *dma_parms ;
878 struct list_head dma_pools ;
879 struct dma_coherent_mem *dma_mem ;
880 struct dev_archdata archdata ;
881 struct device_node *of_node ;
882 dev_t devt ;
883 u32 id ;
884 spinlock_t devres_lock ;
885 struct list_head devres_head ;
886 struct klist_node knode_class ;
887 struct class *class ;
888 struct attribute_group const **groups ;
889 void (*release)(struct device *dev ) ;
890};
891#line 43 "include/linux/pm_wakeup.h"
892struct wakeup_source {
893 char const *name ;
894 struct list_head entry ;
895 spinlock_t lock ;
896 struct timer_list timer ;
897 unsigned long timer_expires ;
898 ktime_t total_time ;
899 ktime_t max_time ;
900 ktime_t last_time ;
901 unsigned long event_count ;
902 unsigned long active_count ;
903 unsigned long relax_count ;
904 unsigned long hit_count ;
905 unsigned int active : 1 ;
906};
907#line 34 "include/linux/pps_kernel.h"
908struct pps_device;
909#line 34
910struct pps_device;
911#line 37 "include/linux/pps_kernel.h"
912struct pps_source_info {
913 char name[32] ;
914 char path[32] ;
915 int mode ;
916 void (*echo)(struct pps_device *pps , int event , void *data ) ;
917 struct module *owner ;
918 struct device *dev ;
919};
920#line 49 "include/linux/pps_kernel.h"
921struct pps_event_time {
922 struct timespec ts_real ;
923};
924#line 57
925struct fasync_struct;
926#line 57 "include/linux/pps_kernel.h"
927struct pps_device {
928 struct pps_source_info info ;
929 struct pps_kparams params ;
930 __u32 assert_sequence ;
931 __u32 clear_sequence ;
932 struct pps_ktime assert_tu ;
933 struct pps_ktime clear_tu ;
934 int current_mode ;
935 unsigned int last_ev ;
936 wait_queue_head_t queue ;
937 unsigned int id ;
938 struct cdev cdev ;
939 struct device *dev ;
940 struct fasync_struct *async_queue ;
941 spinlock_t lock ;
942};
943#line 1 "<compiler builtins>"
944long __builtin_expect(long val , long res ) ;
945#line 100 "include/linux/printk.h"
946extern int ( printk)(char const *fmt , ...) ;
947#line 159 "include/linux/time.h"
948extern void getnstimeofday(struct timespec *tv ) ;
949#line 152 "include/linux/mutex.h"
950void mutex_lock(struct mutex *lock ) ;
951#line 153
952int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock ) ;
953#line 154
954int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock ) ;
955#line 168
956int mutex_trylock(struct mutex *lock ) ;
957#line 169
958void mutex_unlock(struct mutex *lock ) ;
959#line 170
960int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
961#line 82 "include/linux/jiffies.h"
962extern unsigned long volatile jiffies __attribute__((__section__(".data"))) ;
963#line 91 "include/linux/timer.h"
964extern void init_timer_key(struct timer_list *timer , char const *name , struct lock_class_key *key ) ;
965#line 166
966__inline static void setup_timer_key(struct timer_list *timer , char const *name ,
967 struct lock_class_key *key , void (*function)(unsigned long ) ,
968 unsigned long data ) __attribute__((__no_instrument_function__)) ;
969#line 166 "include/linux/timer.h"
970__inline static void setup_timer_key(struct timer_list *timer , char const *name ,
971 struct lock_class_key *key , void (*function)(unsigned long ) ,
972 unsigned long data )
973{ unsigned long __cil_tmp6 ;
974 unsigned long __cil_tmp7 ;
975 unsigned long __cil_tmp8 ;
976 unsigned long __cil_tmp9 ;
977
978 {
979 {
980#line 172
981 __cil_tmp6 = (unsigned long )timer;
982#line 172
983 __cil_tmp7 = __cil_tmp6 + 32;
984#line 172
985 *((void (**)(unsigned long ))__cil_tmp7) = function;
986#line 173
987 __cil_tmp8 = (unsigned long )timer;
988#line 173
989 __cil_tmp9 = __cil_tmp8 + 40;
990#line 173
991 *((unsigned long *)__cil_tmp9) = data;
992#line 174
993 init_timer_key(timer, name, key);
994 }
995#line 175
996 return;
997}
998}
999#line 211
1000extern int mod_timer(struct timer_list *timer , unsigned long expires ) ;
1001#line 280
1002extern int del_timer_sync(struct timer_list *timer ) ;
1003#line 26 "include/linux/export.h"
1004extern struct module __this_module ;
1005#line 67 "include/linux/module.h"
1006int init_module(void) ;
1007#line 68
1008void cleanup_module(void) ;
1009#line 897 "include/linux/device.h"
1010extern int ( _dev_info)(struct device const *dev , char const *fmt
1011 , ...) ;
1012#line 88 "include/linux/pps_kernel.h"
1013extern struct pps_device *pps_register_source(struct pps_source_info *info , int default_params ) ;
1014#line 90
1015extern void pps_unregister_source(struct pps_device *pps ) ;
1016#line 93
1017extern void pps_event(struct pps_device *pps , struct pps_event_time *ts , int event ,
1018 void *data ) ;
1019#line 112
1020__inline static void pps_get_ts(struct pps_event_time *ts ) __attribute__((__no_instrument_function__)) ;
1021#line 112 "include/linux/pps_kernel.h"
1022__inline static void pps_get_ts(struct pps_event_time *ts )
1023{ struct timespec *__cil_tmp2 ;
1024
1025 {
1026 {
1027#line 114
1028 __cil_tmp2 = (struct timespec *)ts;
1029#line 114
1030 getnstimeofday(__cil_tmp2);
1031 }
1032#line 115
1033 return;
1034}
1035}
1036#line 36 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4609/dscv_tempdir/dscv/ri/32_1/drivers/pps/clients/pps-ktimer.c.common.c"
1037static struct pps_device *pps ;
1038#line 37 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4609/dscv_tempdir/dscv/ri/32_1/drivers/pps/clients/pps-ktimer.c.common.c"
1039static struct timer_list ktimer ;
1040#line 43 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4609/dscv_tempdir/dscv/ri/32_1/drivers/pps/clients/pps-ktimer.c.common.c"
1041static void pps_ktimer_event(unsigned long ptr )
1042{ struct pps_event_time ts ;
1043 void *__cil_tmp3 ;
1044 unsigned long volatile __cil_tmp4 ;
1045 unsigned long volatile __cil_tmp5 ;
1046 unsigned long __cil_tmp6 ;
1047
1048 {
1049 {
1050#line 48
1051 pps_get_ts(& ts);
1052#line 50
1053 __cil_tmp3 = (void *)0;
1054#line 50
1055 pps_event(pps, & ts, 1, __cil_tmp3);
1056#line 52
1057 __cil_tmp4 = (unsigned long volatile )250;
1058#line 52
1059 __cil_tmp5 = jiffies + __cil_tmp4;
1060#line 52
1061 __cil_tmp6 = (unsigned long )__cil_tmp5;
1062#line 52
1063 mod_timer(& ktimer, __cil_tmp6);
1064 }
1065#line 53
1066 return;
1067}
1068}
1069#line 59 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4609/dscv_tempdir/dscv/ri/32_1/drivers/pps/clients/pps-ktimer.c.common.c"
1070static struct pps_source_info pps_ktimer_info = {{(char )'k', (char )'t', (char )'i', (char )'m', (char )'e', (char )'r', (char )'\000'},
1071 {(char )'\000'}, 4433, (void (*)(struct pps_device *pps , int event , void *data ))0,
1072 & __this_module, (struct device *)0};
1073#line 72
1074static void pps_ktimer_exit(void) __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
1075#line 72 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4609/dscv_tempdir/dscv/ri/32_1/drivers/pps/clients/pps-ktimer.c.common.c"
1076static void pps_ktimer_exit(void)
1077{ unsigned long __cil_tmp1 ;
1078 unsigned long __cil_tmp2 ;
1079 struct device *__cil_tmp3 ;
1080 struct device const *__cil_tmp4 ;
1081
1082 {
1083 {
1084#line 74
1085 __cil_tmp1 = (unsigned long )pps;
1086#line 74
1087 __cil_tmp2 = __cil_tmp1 + 336;
1088#line 74
1089 __cil_tmp3 = *((struct device **)__cil_tmp2);
1090#line 74
1091 __cil_tmp4 = (struct device const *)__cil_tmp3;
1092#line 74
1093 _dev_info(__cil_tmp4, "ktimer PPS source unregistered\n");
1094#line 76
1095 del_timer_sync(& ktimer);
1096#line 77
1097 pps_unregister_source(pps);
1098 }
1099#line 78
1100 return;
1101}
1102}
1103#line 80
1104static int pps_ktimer_init(void) __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
1105#line 80 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4609/dscv_tempdir/dscv/ri/32_1/drivers/pps/clients/pps-ktimer.c.common.c"
1106static int pps_ktimer_init(void)
1107{ void *__cil_tmp1 ;
1108 unsigned long __cil_tmp2 ;
1109 unsigned long __cil_tmp3 ;
1110 void *__cil_tmp4 ;
1111 char const *__cil_tmp5 ;
1112 void *__cil_tmp6 ;
1113 struct lock_class_key *__cil_tmp7 ;
1114 unsigned long volatile __cil_tmp8 ;
1115 unsigned long volatile __cil_tmp9 ;
1116 unsigned long __cil_tmp10 ;
1117 unsigned long __cil_tmp11 ;
1118 unsigned long __cil_tmp12 ;
1119 struct device *__cil_tmp13 ;
1120 struct device const *__cil_tmp14 ;
1121
1122 {
1123 {
1124#line 82
1125 pps = pps_register_source(& pps_ktimer_info, 17);
1126 }
1127 {
1128#line 84
1129 __cil_tmp1 = (void *)0;
1130#line 84
1131 __cil_tmp2 = (unsigned long )__cil_tmp1;
1132#line 84
1133 __cil_tmp3 = (unsigned long )pps;
1134#line 84
1135 if (__cil_tmp3 == __cil_tmp2) {
1136 {
1137#line 85
1138 printk("<3>pps_ktimer: cannot register PPS source\n");
1139 }
1140#line 86
1141 return (-12);
1142 } else {
1143
1144 }
1145 }
1146 {
1147#line 89
1148 __cil_tmp4 = (void *)0;
1149#line 89
1150 __cil_tmp5 = (char const *)__cil_tmp4;
1151#line 89
1152 __cil_tmp6 = (void *)0;
1153#line 89
1154 __cil_tmp7 = (struct lock_class_key *)__cil_tmp6;
1155#line 89
1156 setup_timer_key(& ktimer, __cil_tmp5, __cil_tmp7, & pps_ktimer_event, 0UL);
1157#line 90
1158 __cil_tmp8 = (unsigned long volatile )250;
1159#line 90
1160 __cil_tmp9 = jiffies + __cil_tmp8;
1161#line 90
1162 __cil_tmp10 = (unsigned long )__cil_tmp9;
1163#line 90
1164 mod_timer(& ktimer, __cil_tmp10);
1165#line 92
1166 __cil_tmp11 = (unsigned long )pps;
1167#line 92
1168 __cil_tmp12 = __cil_tmp11 + 336;
1169#line 92
1170 __cil_tmp13 = *((struct device **)__cil_tmp12);
1171#line 92
1172 __cil_tmp14 = (struct device const *)__cil_tmp13;
1173#line 92
1174 _dev_info(__cil_tmp14, "ktimer PPS source registered\n");
1175 }
1176#line 94
1177 return (0);
1178}
1179}
1180#line 97 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4609/dscv_tempdir/dscv/ri/32_1/drivers/pps/clients/pps-ktimer.c.common.c"
1181int init_module(void)
1182{ int tmp ;
1183
1184 {
1185 {
1186#line 97
1187 tmp = pps_ktimer_init();
1188 }
1189#line 97
1190 return (tmp);
1191}
1192}
1193#line 98 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4609/dscv_tempdir/dscv/ri/32_1/drivers/pps/clients/pps-ktimer.c.common.c"
1194void cleanup_module(void)
1195{
1196
1197 {
1198 {
1199#line 98
1200 pps_ktimer_exit();
1201 }
1202#line 98
1203 return;
1204}
1205}
1206#line 100 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4609/dscv_tempdir/dscv/ri/32_1/drivers/pps/clients/pps-ktimer.c.common.c"
1207static char const __mod_author100[44] __attribute__((__used__, __unused__, __section__(".modinfo"),
1208__aligned__(1))) =
1209#line 100
1210 { (char const )'a', (char const )'u', (char const )'t', (char const )'h',
1211 (char const )'o', (char const )'r', (char const )'=', (char const )'R',
1212 (char const )'o', (char const )'d', (char const )'o', (char const )'l',
1213 (char const )'f', (char const )'o', (char const )' ', (char const )'G',
1214 (char const )'i', (char const )'o', (char const )'m', (char const )'e',
1215 (char const )'t', (char const )'t', (char const )'i', (char const )' ',
1216 (char const )'<', (char const )'g', (char const )'i', (char const )'o',
1217 (char const )'m', (char const )'e', (char const )'t', (char const )'t',
1218 (char const )'i', (char const )'@', (char const )'l', (char const )'i',
1219 (char const )'n', (char const )'u', (char const )'x', (char const )'.',
1220 (char const )'i', (char const )'t', (char const )'>', (char const )'\000'};
1221#line 101 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4609/dscv_tempdir/dscv/ri/32_1/drivers/pps/clients/pps-ktimer.c.common.c"
1222static char const __mod_description101[70] __attribute__((__used__, __unused__,
1223__section__(".modinfo"), __aligned__(1))) =
1224#line 101
1225 { (char const )'d', (char const )'e', (char const )'s', (char const )'c',
1226 (char const )'r', (char const )'i', (char const )'p', (char const )'t',
1227 (char const )'i', (char const )'o', (char const )'n', (char const )'=',
1228 (char const )'d', (char const )'u', (char const )'m', (char const )'m',
1229 (char const )'y', (char const )' ', (char const )'P', (char const )'P',
1230 (char const )'S', (char const )' ', (char const )'s', (char const )'o',
1231 (char const )'u', (char const )'r', (char const )'c', (char const )'e',
1232 (char const )' ', (char const )'b', (char const )'y', (char const )' ',
1233 (char const )'u', (char const )'s', (char const )'i', (char const )'n',
1234 (char const )'g', (char const )' ', (char const )'a', (char const )' ',
1235 (char const )'k', (char const )'e', (char const )'r', (char const )'n',
1236 (char const )'e', (char const )'l', (char const )' ', (char const )'t',
1237 (char const )'i', (char const )'m', (char const )'e', (char const )'r',
1238 (char const )' ', (char const )'(', (char const )'j', (char const )'u',
1239 (char const )'s', (char const )'t', (char const )' ', (char const )'f',
1240 (char const )'o', (char const )'r', (char const )' ', (char const )'d',
1241 (char const )'e', (char const )'b', (char const )'u', (char const )'g',
1242 (char const )')', (char const )'\000'};
1243#line 102 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4609/dscv_tempdir/dscv/ri/32_1/drivers/pps/clients/pps-ktimer.c.common.c"
1244static char const __mod_license102[12] __attribute__((__used__, __unused__, __section__(".modinfo"),
1245__aligned__(1))) =
1246#line 102
1247 { (char const )'l', (char const )'i', (char const )'c', (char const )'e',
1248 (char const )'n', (char const )'s', (char const )'e', (char const )'=',
1249 (char const )'G', (char const )'P', (char const )'L', (char const )'\000'};
1250#line 120
1251void ldv_check_final_state(void) ;
1252#line 126
1253extern void ldv_initialize(void) ;
1254#line 129
1255extern int __VERIFIER_nondet_int(void) ;
1256#line 132 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4609/dscv_tempdir/dscv/ri/32_1/drivers/pps/clients/pps-ktimer.c.common.c"
1257int LDV_IN_INTERRUPT ;
1258#line 135 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4609/dscv_tempdir/dscv/ri/32_1/drivers/pps/clients/pps-ktimer.c.common.c"
1259void main(void)
1260{ int tmp ;
1261 int tmp___0 ;
1262 int tmp___1 ;
1263
1264 {
1265 {
1266#line 147
1267 LDV_IN_INTERRUPT = 1;
1268#line 156
1269 ldv_initialize();
1270#line 164
1271 tmp = pps_ktimer_init();
1272 }
1273#line 164
1274 if (tmp) {
1275#line 165
1276 goto ldv_final;
1277 } else {
1278
1279 }
1280 {
1281#line 167
1282 while (1) {
1283 while_continue: ;
1284 {
1285#line 167
1286 tmp___1 = __VERIFIER_nondet_int();
1287 }
1288#line 167
1289 if (tmp___1) {
1290
1291 } else {
1292#line 167
1293 goto while_break;
1294 }
1295 {
1296#line 170
1297 tmp___0 = __VERIFIER_nondet_int();
1298 }
1299 {
1300#line 172
1301 goto switch_default;
1302#line 170
1303 if (0) {
1304 switch_default:
1305#line 172
1306 goto switch_break;
1307 } else {
1308 switch_break: ;
1309 }
1310 }
1311 }
1312 while_break: ;
1313 }
1314 {
1315#line 186
1316 pps_ktimer_exit();
1317 }
1318 ldv_final:
1319 {
1320#line 189
1321 ldv_check_final_state();
1322 }
1323#line 192
1324 return;
1325}
1326}
1327#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4609/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
1328void ldv_blast_assert(void)
1329{
1330
1331 {
1332 ERROR:
1333#line 6
1334 goto ERROR;
1335}
1336}
1337#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4609/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
1338extern int __VERIFIER_nondet_int(void) ;
1339#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4609/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1340int ldv_mutex = 1;
1341#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4609/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1342int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )
1343{ int nondetermined ;
1344
1345 {
1346#line 29
1347 if (ldv_mutex == 1) {
1348
1349 } else {
1350 {
1351#line 29
1352 ldv_blast_assert();
1353 }
1354 }
1355 {
1356#line 32
1357 nondetermined = __VERIFIER_nondet_int();
1358 }
1359#line 35
1360 if (nondetermined) {
1361#line 38
1362 ldv_mutex = 2;
1363#line 40
1364 return (0);
1365 } else {
1366#line 45
1367 return (-4);
1368 }
1369}
1370}
1371#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4609/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1372int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock )
1373{ int nondetermined ;
1374
1375 {
1376#line 57
1377 if (ldv_mutex == 1) {
1378
1379 } else {
1380 {
1381#line 57
1382 ldv_blast_assert();
1383 }
1384 }
1385 {
1386#line 60
1387 nondetermined = __VERIFIER_nondet_int();
1388 }
1389#line 63
1390 if (nondetermined) {
1391#line 66
1392 ldv_mutex = 2;
1393#line 68
1394 return (0);
1395 } else {
1396#line 73
1397 return (-4);
1398 }
1399}
1400}
1401#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4609/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1402int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock )
1403{ int atomic_value_after_dec ;
1404
1405 {
1406#line 83
1407 if (ldv_mutex == 1) {
1408
1409 } else {
1410 {
1411#line 83
1412 ldv_blast_assert();
1413 }
1414 }
1415 {
1416#line 86
1417 atomic_value_after_dec = __VERIFIER_nondet_int();
1418 }
1419#line 89
1420 if (atomic_value_after_dec == 0) {
1421#line 92
1422 ldv_mutex = 2;
1423#line 94
1424 return (1);
1425 } else {
1426
1427 }
1428#line 98
1429 return (0);
1430}
1431}
1432#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4609/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1433void mutex_lock(struct mutex *lock )
1434{
1435
1436 {
1437#line 108
1438 if (ldv_mutex == 1) {
1439
1440 } else {
1441 {
1442#line 108
1443 ldv_blast_assert();
1444 }
1445 }
1446#line 110
1447 ldv_mutex = 2;
1448#line 111
1449 return;
1450}
1451}
1452#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4609/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1453int mutex_trylock(struct mutex *lock )
1454{ int nondetermined ;
1455
1456 {
1457#line 121
1458 if (ldv_mutex == 1) {
1459
1460 } else {
1461 {
1462#line 121
1463 ldv_blast_assert();
1464 }
1465 }
1466 {
1467#line 124
1468 nondetermined = __VERIFIER_nondet_int();
1469 }
1470#line 127
1471 if (nondetermined) {
1472#line 130
1473 ldv_mutex = 2;
1474#line 132
1475 return (1);
1476 } else {
1477#line 137
1478 return (0);
1479 }
1480}
1481}
1482#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4609/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1483void mutex_unlock(struct mutex *lock )
1484{
1485
1486 {
1487#line 147
1488 if (ldv_mutex == 2) {
1489
1490 } else {
1491 {
1492#line 147
1493 ldv_blast_assert();
1494 }
1495 }
1496#line 149
1497 ldv_mutex = 1;
1498#line 150
1499 return;
1500}
1501}
1502#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4609/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1503void ldv_check_final_state(void)
1504{
1505
1506 {
1507#line 156
1508 if (ldv_mutex == 1) {
1509
1510 } else {
1511 {
1512#line 156
1513 ldv_blast_assert();
1514 }
1515 }
1516#line 157
1517 return;
1518}
1519}
1520#line 201 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4609/dscv_tempdir/dscv/ri/32_1/drivers/pps/clients/pps-ktimer.c.common.c"
1521long s__builtin_expect(long val , long res )
1522{
1523
1524 {
1525#line 202
1526 return (val);
1527}
1528}