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