1
2
3
4#line 19 "include/asm-generic/int-ll64.h"
5typedef signed char __s8;
6#line 20 "include/asm-generic/int-ll64.h"
7typedef unsigned char __u8;
8#line 22 "include/asm-generic/int-ll64.h"
9typedef short __s16;
10#line 23 "include/asm-generic/int-ll64.h"
11typedef unsigned short __u16;
12#line 25 "include/asm-generic/int-ll64.h"
13typedef int __s32;
14#line 26 "include/asm-generic/int-ll64.h"
15typedef unsigned int __u32;
16#line 30 "include/asm-generic/int-ll64.h"
17typedef unsigned long long __u64;
18#line 43 "include/asm-generic/int-ll64.h"
19typedef unsigned char u8;
20#line 45 "include/asm-generic/int-ll64.h"
21typedef short s16;
22#line 46 "include/asm-generic/int-ll64.h"
23typedef unsigned short u16;
24#line 48 "include/asm-generic/int-ll64.h"
25typedef int s32;
26#line 49 "include/asm-generic/int-ll64.h"
27typedef unsigned int u32;
28#line 51 "include/asm-generic/int-ll64.h"
29typedef long long s64;
30#line 52 "include/asm-generic/int-ll64.h"
31typedef unsigned long long u64;
32#line 14 "include/asm-generic/posix_types.h"
33typedef long __kernel_long_t;
34#line 15 "include/asm-generic/posix_types.h"
35typedef unsigned long __kernel_ulong_t;
36#line 52 "include/asm-generic/posix_types.h"
37typedef unsigned int __kernel_uid32_t;
38#line 53 "include/asm-generic/posix_types.h"
39typedef unsigned int __kernel_gid32_t;
40#line 75 "include/asm-generic/posix_types.h"
41typedef __kernel_ulong_t __kernel_size_t;
42#line 76 "include/asm-generic/posix_types.h"
43typedef __kernel_long_t __kernel_ssize_t;
44#line 91 "include/asm-generic/posix_types.h"
45typedef long long __kernel_loff_t;
46#line 92 "include/asm-generic/posix_types.h"
47typedef __kernel_long_t __kernel_time_t;
48#line 21 "include/linux/types.h"
49typedef __u32 __kernel_dev_t;
50#line 24 "include/linux/types.h"
51typedef __kernel_dev_t dev_t;
52#line 27 "include/linux/types.h"
53typedef unsigned short umode_t;
54#line 38 "include/linux/types.h"
55typedef _Bool bool;
56#line 40 "include/linux/types.h"
57typedef __kernel_uid32_t uid_t;
58#line 41 "include/linux/types.h"
59typedef __kernel_gid32_t gid_t;
60#line 54 "include/linux/types.h"
61typedef __kernel_loff_t loff_t;
62#line 63 "include/linux/types.h"
63typedef __kernel_size_t size_t;
64#line 68 "include/linux/types.h"
65typedef __kernel_ssize_t ssize_t;
66#line 78 "include/linux/types.h"
67typedef __kernel_time_t time_t;
68#line 142 "include/linux/types.h"
69typedef unsigned long sector_t;
70#line 143 "include/linux/types.h"
71typedef unsigned long blkcnt_t;
72#line 202 "include/linux/types.h"
73typedef unsigned int gfp_t;
74#line 203 "include/linux/types.h"
75typedef unsigned int fmode_t;
76#line 206 "include/linux/types.h"
77typedef u64 phys_addr_t;
78#line 211 "include/linux/types.h"
79typedef phys_addr_t resource_size_t;
80#line 221 "include/linux/types.h"
81struct __anonstruct_atomic_t_6 {
82 int counter ;
83};
84#line 221 "include/linux/types.h"
85typedef struct __anonstruct_atomic_t_6 atomic_t;
86#line 226 "include/linux/types.h"
87struct __anonstruct_atomic64_t_7 {
88 long counter ;
89};
90#line 226 "include/linux/types.h"
91typedef struct __anonstruct_atomic64_t_7 atomic64_t;
92#line 227 "include/linux/types.h"
93struct list_head {
94 struct list_head *next ;
95 struct list_head *prev ;
96};
97#line 232
98struct hlist_node;
99#line 232 "include/linux/types.h"
100struct hlist_head {
101 struct hlist_node *first ;
102};
103#line 236 "include/linux/types.h"
104struct hlist_node {
105 struct hlist_node *next ;
106 struct hlist_node **pprev ;
107};
108#line 247 "include/linux/types.h"
109struct rcu_head {
110 struct rcu_head *next ;
111 void (*func)(struct rcu_head * ) ;
112};
113#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
114struct module;
115#line 55
116struct module;
117#line 146 "include/linux/init.h"
118typedef void (*ctor_fn_t)(void);
119#line 305 "include/linux/printk.h"
120struct _ddebug {
121 char const *modname ;
122 char const *function ;
123 char const *filename ;
124 char const *format ;
125 unsigned int lineno : 18 ;
126 unsigned char flags ;
127};
128#line 46 "include/linux/dynamic_debug.h"
129struct device;
130#line 46
131struct device;
132#line 348 "include/linux/kernel.h"
133struct pid;
134#line 348
135struct pid;
136#line 112 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/stat.h"
137struct timespec;
138#line 112
139struct timespec;
140#line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
141struct page;
142#line 58
143struct page;
144#line 26 "include/asm-generic/getorder.h"
145struct task_struct;
146#line 26
147struct task_struct;
148#line 290 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
149struct file;
150#line 290
151struct file;
152#line 305
153struct seq_file;
154#line 305
155struct seq_file;
156#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
157struct arch_spinlock;
158#line 327
159struct arch_spinlock;
160#line 306 "include/linux/bitmap.h"
161struct bug_entry {
162 int bug_addr_disp ;
163 int file_disp ;
164 unsigned short line ;
165 unsigned short flags ;
166};
167#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
168struct static_key;
169#line 234
170struct static_key;
171#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
172struct kmem_cache;
173#line 23 "include/asm-generic/atomic-long.h"
174typedef atomic64_t atomic_long_t;
175#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
176typedef u16 __ticket_t;
177#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
178typedef u32 __ticketpair_t;
179#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
180struct __raw_tickets {
181 __ticket_t head ;
182 __ticket_t tail ;
183};
184#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
185union __anonunion_ldv_5907_29 {
186 __ticketpair_t head_tail ;
187 struct __raw_tickets tickets ;
188};
189#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
190struct arch_spinlock {
191 union __anonunion_ldv_5907_29 ldv_5907 ;
192};
193#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
194typedef struct arch_spinlock arch_spinlock_t;
195#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
196struct __anonstruct_ldv_5914_31 {
197 u32 read ;
198 s32 write ;
199};
200#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
201union __anonunion_arch_rwlock_t_30 {
202 s64 lock ;
203 struct __anonstruct_ldv_5914_31 ldv_5914 ;
204};
205#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
206typedef union __anonunion_arch_rwlock_t_30 arch_rwlock_t;
207#line 34
208struct lockdep_map;
209#line 34
210struct lockdep_map;
211#line 55 "include/linux/debug_locks.h"
212struct stack_trace {
213 unsigned int nr_entries ;
214 unsigned int max_entries ;
215 unsigned long *entries ;
216 int skip ;
217};
218#line 26 "include/linux/stacktrace.h"
219struct lockdep_subclass_key {
220 char __one_byte ;
221};
222#line 53 "include/linux/lockdep.h"
223struct lock_class_key {
224 struct lockdep_subclass_key subkeys[8U] ;
225};
226#line 59 "include/linux/lockdep.h"
227struct lock_class {
228 struct list_head hash_entry ;
229 struct list_head lock_entry ;
230 struct lockdep_subclass_key *key ;
231 unsigned int subclass ;
232 unsigned int dep_gen_id ;
233 unsigned long usage_mask ;
234 struct stack_trace usage_traces[13U] ;
235 struct list_head locks_after ;
236 struct list_head locks_before ;
237 unsigned int version ;
238 unsigned long ops ;
239 char const *name ;
240 int name_version ;
241 unsigned long contention_point[4U] ;
242 unsigned long contending_point[4U] ;
243};
244#line 144 "include/linux/lockdep.h"
245struct lockdep_map {
246 struct lock_class_key *key ;
247 struct lock_class *class_cache[2U] ;
248 char const *name ;
249 int cpu ;
250 unsigned long ip ;
251};
252#line 556 "include/linux/lockdep.h"
253struct raw_spinlock {
254 arch_spinlock_t raw_lock ;
255 unsigned int magic ;
256 unsigned int owner_cpu ;
257 void *owner ;
258 struct lockdep_map dep_map ;
259};
260#line 32 "include/linux/spinlock_types.h"
261typedef struct raw_spinlock raw_spinlock_t;
262#line 33 "include/linux/spinlock_types.h"
263struct __anonstruct_ldv_6122_33 {
264 u8 __padding[24U] ;
265 struct lockdep_map dep_map ;
266};
267#line 33 "include/linux/spinlock_types.h"
268union __anonunion_ldv_6123_32 {
269 struct raw_spinlock rlock ;
270 struct __anonstruct_ldv_6122_33 ldv_6122 ;
271};
272#line 33 "include/linux/spinlock_types.h"
273struct spinlock {
274 union __anonunion_ldv_6123_32 ldv_6123 ;
275};
276#line 76 "include/linux/spinlock_types.h"
277typedef struct spinlock spinlock_t;
278#line 23 "include/linux/rwlock_types.h"
279struct __anonstruct_rwlock_t_34 {
280 arch_rwlock_t raw_lock ;
281 unsigned int magic ;
282 unsigned int owner_cpu ;
283 void *owner ;
284 struct lockdep_map dep_map ;
285};
286#line 23 "include/linux/rwlock_types.h"
287typedef struct __anonstruct_rwlock_t_34 rwlock_t;
288#line 110 "include/linux/seqlock.h"
289struct seqcount {
290 unsigned int sequence ;
291};
292#line 121 "include/linux/seqlock.h"
293typedef struct seqcount seqcount_t;
294#line 254 "include/linux/seqlock.h"
295struct timespec {
296 __kernel_time_t tv_sec ;
297 long tv_nsec ;
298};
299#line 286 "include/linux/time.h"
300struct kstat {
301 u64 ino ;
302 dev_t dev ;
303 umode_t mode ;
304 unsigned int nlink ;
305 uid_t uid ;
306 gid_t gid ;
307 dev_t rdev ;
308 loff_t size ;
309 struct timespec atime ;
310 struct timespec mtime ;
311 struct timespec ctime ;
312 unsigned long blksize ;
313 unsigned long long blocks ;
314};
315#line 48 "include/linux/wait.h"
316struct __wait_queue_head {
317 spinlock_t lock ;
318 struct list_head task_list ;
319};
320#line 53 "include/linux/wait.h"
321typedef struct __wait_queue_head wait_queue_head_t;
322#line 670 "include/linux/mmzone.h"
323struct mutex {
324 atomic_t count ;
325 spinlock_t wait_lock ;
326 struct list_head wait_list ;
327 struct task_struct *owner ;
328 char const *name ;
329 void *magic ;
330 struct lockdep_map dep_map ;
331};
332#line 171 "include/linux/mutex.h"
333struct rw_semaphore;
334#line 171
335struct rw_semaphore;
336#line 172 "include/linux/mutex.h"
337struct rw_semaphore {
338 long count ;
339 raw_spinlock_t wait_lock ;
340 struct list_head wait_list ;
341 struct lockdep_map dep_map ;
342};
343#line 188 "include/linux/rcupdate.h"
344struct notifier_block;
345#line 188
346struct notifier_block;
347#line 239 "include/linux/srcu.h"
348struct notifier_block {
349 int (*notifier_call)(struct notifier_block * , unsigned long , void * ) ;
350 struct notifier_block *next ;
351 int priority ;
352};
353#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/e820.h"
354struct resource {
355 resource_size_t start ;
356 resource_size_t end ;
357 char const *name ;
358 unsigned long flags ;
359 struct resource *parent ;
360 struct resource *sibling ;
361 struct resource *child ;
362};
363#line 18 "include/asm-generic/pci_iomap.h"
364struct vm_area_struct;
365#line 18
366struct vm_area_struct;
367#line 37 "include/linux/kmod.h"
368struct cred;
369#line 37
370struct cred;
371#line 18 "include/linux/elf.h"
372typedef __u64 Elf64_Addr;
373#line 19 "include/linux/elf.h"
374typedef __u16 Elf64_Half;
375#line 23 "include/linux/elf.h"
376typedef __u32 Elf64_Word;
377#line 24 "include/linux/elf.h"
378typedef __u64 Elf64_Xword;
379#line 193 "include/linux/elf.h"
380struct elf64_sym {
381 Elf64_Word st_name ;
382 unsigned char st_info ;
383 unsigned char st_other ;
384 Elf64_Half st_shndx ;
385 Elf64_Addr st_value ;
386 Elf64_Xword st_size ;
387};
388#line 201 "include/linux/elf.h"
389typedef struct elf64_sym Elf64_Sym;
390#line 445
391struct sock;
392#line 445
393struct sock;
394#line 446
395struct kobject;
396#line 446
397struct kobject;
398#line 447
399enum kobj_ns_type {
400 KOBJ_NS_TYPE_NONE = 0,
401 KOBJ_NS_TYPE_NET = 1,
402 KOBJ_NS_TYPES = 2
403} ;
404#line 453 "include/linux/elf.h"
405struct kobj_ns_type_operations {
406 enum kobj_ns_type type ;
407 void *(*grab_current_ns)(void) ;
408 void const *(*netlink_ns)(struct sock * ) ;
409 void const *(*initial_ns)(void) ;
410 void (*drop_ns)(void * ) ;
411};
412#line 57 "include/linux/kobject_ns.h"
413struct attribute {
414 char const *name ;
415 umode_t mode ;
416 struct lock_class_key *key ;
417 struct lock_class_key skey ;
418};
419#line 98 "include/linux/sysfs.h"
420struct sysfs_ops {
421 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
422 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
423 void const *(*namespace)(struct kobject * , struct attribute const * ) ;
424};
425#line 117
426struct sysfs_dirent;
427#line 117
428struct sysfs_dirent;
429#line 182 "include/linux/sysfs.h"
430struct kref {
431 atomic_t refcount ;
432};
433#line 49 "include/linux/kobject.h"
434struct kset;
435#line 49
436struct kobj_type;
437#line 49 "include/linux/kobject.h"
438struct kobject {
439 char const *name ;
440 struct list_head entry ;
441 struct kobject *parent ;
442 struct kset *kset ;
443 struct kobj_type *ktype ;
444 struct sysfs_dirent *sd ;
445 struct kref kref ;
446 unsigned char state_initialized : 1 ;
447 unsigned char state_in_sysfs : 1 ;
448 unsigned char state_add_uevent_sent : 1 ;
449 unsigned char state_remove_uevent_sent : 1 ;
450 unsigned char uevent_suppress : 1 ;
451};
452#line 107 "include/linux/kobject.h"
453struct kobj_type {
454 void (*release)(struct kobject * ) ;
455 struct sysfs_ops const *sysfs_ops ;
456 struct attribute **default_attrs ;
457 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject * ) ;
458 void const *(*namespace)(struct kobject * ) ;
459};
460#line 115 "include/linux/kobject.h"
461struct kobj_uevent_env {
462 char *envp[32U] ;
463 int envp_idx ;
464 char buf[2048U] ;
465 int buflen ;
466};
467#line 122 "include/linux/kobject.h"
468struct kset_uevent_ops {
469 int (* const filter)(struct kset * , struct kobject * ) ;
470 char const *(* const name)(struct kset * , struct kobject * ) ;
471 int (* const uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
472};
473#line 139 "include/linux/kobject.h"
474struct kset {
475 struct list_head list ;
476 spinlock_t list_lock ;
477 struct kobject kobj ;
478 struct kset_uevent_ops const *uevent_ops ;
479};
480#line 215
481struct kernel_param;
482#line 215
483struct kernel_param;
484#line 216 "include/linux/kobject.h"
485struct kernel_param_ops {
486 int (*set)(char const * , struct kernel_param const * ) ;
487 int (*get)(char * , struct kernel_param const * ) ;
488 void (*free)(void * ) ;
489};
490#line 49 "include/linux/moduleparam.h"
491struct kparam_string;
492#line 49
493struct kparam_array;
494#line 49 "include/linux/moduleparam.h"
495union __anonunion_ldv_13363_134 {
496 void *arg ;
497 struct kparam_string const *str ;
498 struct kparam_array const *arr ;
499};
500#line 49 "include/linux/moduleparam.h"
501struct kernel_param {
502 char const *name ;
503 struct kernel_param_ops const *ops ;
504 u16 perm ;
505 s16 level ;
506 union __anonunion_ldv_13363_134 ldv_13363 ;
507};
508#line 61 "include/linux/moduleparam.h"
509struct kparam_string {
510 unsigned int maxlen ;
511 char *string ;
512};
513#line 67 "include/linux/moduleparam.h"
514struct kparam_array {
515 unsigned int max ;
516 unsigned int elemsize ;
517 unsigned int *num ;
518 struct kernel_param_ops const *ops ;
519 void *elem ;
520};
521#line 458 "include/linux/moduleparam.h"
522struct static_key {
523 atomic_t enabled ;
524};
525#line 225 "include/linux/jump_label.h"
526struct tracepoint;
527#line 225
528struct tracepoint;
529#line 226 "include/linux/jump_label.h"
530struct tracepoint_func {
531 void *func ;
532 void *data ;
533};
534#line 29 "include/linux/tracepoint.h"
535struct tracepoint {
536 char const *name ;
537 struct static_key key ;
538 void (*regfunc)(void) ;
539 void (*unregfunc)(void) ;
540 struct tracepoint_func *funcs ;
541};
542#line 86 "include/linux/tracepoint.h"
543struct kernel_symbol {
544 unsigned long value ;
545 char const *name ;
546};
547#line 27 "include/linux/export.h"
548struct mod_arch_specific {
549
550};
551#line 34 "include/linux/module.h"
552struct module_param_attrs;
553#line 34 "include/linux/module.h"
554struct module_kobject {
555 struct kobject kobj ;
556 struct module *mod ;
557 struct kobject *drivers_dir ;
558 struct module_param_attrs *mp ;
559};
560#line 43 "include/linux/module.h"
561struct module_attribute {
562 struct attribute attr ;
563 ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
564 ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const * ,
565 size_t ) ;
566 void (*setup)(struct module * , char const * ) ;
567 int (*test)(struct module * ) ;
568 void (*free)(struct module * ) ;
569};
570#line 69
571struct exception_table_entry;
572#line 69
573struct exception_table_entry;
574#line 198
575enum module_state {
576 MODULE_STATE_LIVE = 0,
577 MODULE_STATE_COMING = 1,
578 MODULE_STATE_GOING = 2
579} ;
580#line 204 "include/linux/module.h"
581struct module_ref {
582 unsigned long incs ;
583 unsigned long decs ;
584};
585#line 219
586struct module_sect_attrs;
587#line 219
588struct module_notes_attrs;
589#line 219
590struct ftrace_event_call;
591#line 219 "include/linux/module.h"
592struct module {
593 enum module_state state ;
594 struct list_head list ;
595 char name[56U] ;
596 struct module_kobject mkobj ;
597 struct module_attribute *modinfo_attrs ;
598 char const *version ;
599 char const *srcversion ;
600 struct kobject *holders_dir ;
601 struct kernel_symbol const *syms ;
602 unsigned long const *crcs ;
603 unsigned int num_syms ;
604 struct kernel_param *kp ;
605 unsigned int num_kp ;
606 unsigned int num_gpl_syms ;
607 struct kernel_symbol const *gpl_syms ;
608 unsigned long const *gpl_crcs ;
609 struct kernel_symbol const *unused_syms ;
610 unsigned long const *unused_crcs ;
611 unsigned int num_unused_syms ;
612 unsigned int num_unused_gpl_syms ;
613 struct kernel_symbol const *unused_gpl_syms ;
614 unsigned long const *unused_gpl_crcs ;
615 struct kernel_symbol const *gpl_future_syms ;
616 unsigned long const *gpl_future_crcs ;
617 unsigned int num_gpl_future_syms ;
618 unsigned int num_exentries ;
619 struct exception_table_entry *extable ;
620 int (*init)(void) ;
621 void *module_init ;
622 void *module_core ;
623 unsigned int init_size ;
624 unsigned int core_size ;
625 unsigned int init_text_size ;
626 unsigned int core_text_size ;
627 unsigned int init_ro_size ;
628 unsigned int core_ro_size ;
629 struct mod_arch_specific arch ;
630 unsigned int taints ;
631 unsigned int num_bugs ;
632 struct list_head bug_list ;
633 struct bug_entry *bug_table ;
634 Elf64_Sym *symtab ;
635 Elf64_Sym *core_symtab ;
636 unsigned int num_symtab ;
637 unsigned int core_num_syms ;
638 char *strtab ;
639 char *core_strtab ;
640 struct module_sect_attrs *sect_attrs ;
641 struct module_notes_attrs *notes_attrs ;
642 char *args ;
643 void *percpu ;
644 unsigned int percpu_size ;
645 unsigned int num_tracepoints ;
646 struct tracepoint * const *tracepoints_ptrs ;
647 unsigned int num_trace_bprintk_fmt ;
648 char const **trace_bprintk_fmt_start ;
649 struct ftrace_event_call **trace_events ;
650 unsigned int num_trace_events ;
651 struct list_head source_list ;
652 struct list_head target_list ;
653 struct task_struct *waiter ;
654 void (*exit)(void) ;
655 struct module_ref *refptr ;
656 ctor_fn_t (**ctors)(void) ;
657 unsigned int num_ctors ;
658};
659#line 88 "include/linux/kmemleak.h"
660struct kmem_cache_cpu {
661 void **freelist ;
662 unsigned long tid ;
663 struct page *page ;
664 struct page *partial ;
665 int node ;
666 unsigned int stat[26U] ;
667};
668#line 55 "include/linux/slub_def.h"
669struct kmem_cache_node {
670 spinlock_t list_lock ;
671 unsigned long nr_partial ;
672 struct list_head partial ;
673 atomic_long_t nr_slabs ;
674 atomic_long_t total_objects ;
675 struct list_head full ;
676};
677#line 66 "include/linux/slub_def.h"
678struct kmem_cache_order_objects {
679 unsigned long x ;
680};
681#line 76 "include/linux/slub_def.h"
682struct kmem_cache {
683 struct kmem_cache_cpu *cpu_slab ;
684 unsigned long flags ;
685 unsigned long min_partial ;
686 int size ;
687 int objsize ;
688 int offset ;
689 int cpu_partial ;
690 struct kmem_cache_order_objects oo ;
691 struct kmem_cache_order_objects max ;
692 struct kmem_cache_order_objects min ;
693 gfp_t allocflags ;
694 int refcount ;
695 void (*ctor)(void * ) ;
696 int inuse ;
697 int align ;
698 int reserved ;
699 char const *name ;
700 struct list_head list ;
701 struct kobject kobj ;
702 int remote_node_defrag_ratio ;
703 struct kmem_cache_node *node[1024U] ;
704};
705#line 15 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
706struct file_operations;
707#line 15 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
708struct miscdevice {
709 int minor ;
710 char const *name ;
711 struct file_operations const *fops ;
712 struct list_head list ;
713 struct device *parent ;
714 struct device *this_device ;
715 char const *nodename ;
716 umode_t mode ;
717};
718#line 63 "include/linux/miscdevice.h"
719struct watchdog_info {
720 __u32 options ;
721 __u32 firmware_version ;
722 __u8 identity[32U] ;
723};
724#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/emergency-restart.h"
725struct block_device;
726#line 22
727struct block_device;
728#line 93 "include/linux/bit_spinlock.h"
729struct hlist_bl_node;
730#line 93 "include/linux/bit_spinlock.h"
731struct hlist_bl_head {
732 struct hlist_bl_node *first ;
733};
734#line 36 "include/linux/list_bl.h"
735struct hlist_bl_node {
736 struct hlist_bl_node *next ;
737 struct hlist_bl_node **pprev ;
738};
739#line 114 "include/linux/rculist_bl.h"
740struct nameidata;
741#line 114
742struct nameidata;
743#line 115
744struct path;
745#line 115
746struct path;
747#line 116
748struct vfsmount;
749#line 116
750struct vfsmount;
751#line 117 "include/linux/rculist_bl.h"
752struct qstr {
753 unsigned int hash ;
754 unsigned int len ;
755 unsigned char const *name ;
756};
757#line 72 "include/linux/dcache.h"
758struct inode;
759#line 72
760struct dentry_operations;
761#line 72
762struct super_block;
763#line 72 "include/linux/dcache.h"
764union __anonunion_d_u_135 {
765 struct list_head d_child ;
766 struct rcu_head d_rcu ;
767};
768#line 72 "include/linux/dcache.h"
769struct dentry {
770 unsigned int d_flags ;
771 seqcount_t d_seq ;
772 struct hlist_bl_node d_hash ;
773 struct dentry *d_parent ;
774 struct qstr d_name ;
775 struct inode *d_inode ;
776 unsigned char d_iname[32U] ;
777 unsigned int d_count ;
778 spinlock_t d_lock ;
779 struct dentry_operations const *d_op ;
780 struct super_block *d_sb ;
781 unsigned long d_time ;
782 void *d_fsdata ;
783 struct list_head d_lru ;
784 union __anonunion_d_u_135 d_u ;
785 struct list_head d_subdirs ;
786 struct list_head d_alias ;
787};
788#line 123 "include/linux/dcache.h"
789struct dentry_operations {
790 int (*d_revalidate)(struct dentry * , struct nameidata * ) ;
791 int (*d_hash)(struct dentry const * , struct inode const * , struct qstr * ) ;
792 int (*d_compare)(struct dentry const * , struct inode const * , struct dentry const * ,
793 struct inode const * , unsigned int , char const * , struct qstr const * ) ;
794 int (*d_delete)(struct dentry const * ) ;
795 void (*d_release)(struct dentry * ) ;
796 void (*d_prune)(struct dentry * ) ;
797 void (*d_iput)(struct dentry * , struct inode * ) ;
798 char *(*d_dname)(struct dentry * , char * , int ) ;
799 struct vfsmount *(*d_automount)(struct path * ) ;
800 int (*d_manage)(struct dentry * , bool ) ;
801};
802#line 402 "include/linux/dcache.h"
803struct path {
804 struct vfsmount *mnt ;
805 struct dentry *dentry ;
806};
807#line 58 "include/linux/radix-tree.h"
808struct radix_tree_node;
809#line 58 "include/linux/radix-tree.h"
810struct radix_tree_root {
811 unsigned int height ;
812 gfp_t gfp_mask ;
813 struct radix_tree_node *rnode ;
814};
815#line 377
816struct prio_tree_node;
817#line 19 "include/linux/prio_tree.h"
818struct prio_tree_node {
819 struct prio_tree_node *left ;
820 struct prio_tree_node *right ;
821 struct prio_tree_node *parent ;
822 unsigned long start ;
823 unsigned long last ;
824};
825#line 27 "include/linux/prio_tree.h"
826struct prio_tree_root {
827 struct prio_tree_node *prio_tree_node ;
828 unsigned short index_bits ;
829 unsigned short raw ;
830};
831#line 111
832enum pid_type {
833 PIDTYPE_PID = 0,
834 PIDTYPE_PGID = 1,
835 PIDTYPE_SID = 2,
836 PIDTYPE_MAX = 3
837} ;
838#line 118
839struct pid_namespace;
840#line 118 "include/linux/prio_tree.h"
841struct upid {
842 int nr ;
843 struct pid_namespace *ns ;
844 struct hlist_node pid_chain ;
845};
846#line 56 "include/linux/pid.h"
847struct pid {
848 atomic_t count ;
849 unsigned int level ;
850 struct hlist_head tasks[3U] ;
851 struct rcu_head rcu ;
852 struct upid numbers[1U] ;
853};
854#line 45 "include/linux/semaphore.h"
855struct fiemap_extent {
856 __u64 fe_logical ;
857 __u64 fe_physical ;
858 __u64 fe_length ;
859 __u64 fe_reserved64[2U] ;
860 __u32 fe_flags ;
861 __u32 fe_reserved[3U] ;
862};
863#line 38 "include/linux/fiemap.h"
864struct shrink_control {
865 gfp_t gfp_mask ;
866 unsigned long nr_to_scan ;
867};
868#line 14 "include/linux/shrinker.h"
869struct shrinker {
870 int (*shrink)(struct shrinker * , struct shrink_control * ) ;
871 int seeks ;
872 long batch ;
873 struct list_head list ;
874 atomic_long_t nr_in_batch ;
875};
876#line 43
877enum migrate_mode {
878 MIGRATE_ASYNC = 0,
879 MIGRATE_SYNC_LIGHT = 1,
880 MIGRATE_SYNC = 2
881} ;
882#line 49
883struct export_operations;
884#line 49
885struct export_operations;
886#line 51
887struct iovec;
888#line 51
889struct iovec;
890#line 52
891struct kiocb;
892#line 52
893struct kiocb;
894#line 53
895struct pipe_inode_info;
896#line 53
897struct pipe_inode_info;
898#line 54
899struct poll_table_struct;
900#line 54
901struct poll_table_struct;
902#line 55
903struct kstatfs;
904#line 55
905struct kstatfs;
906#line 435 "include/linux/fs.h"
907struct iattr {
908 unsigned int ia_valid ;
909 umode_t ia_mode ;
910 uid_t ia_uid ;
911 gid_t ia_gid ;
912 loff_t ia_size ;
913 struct timespec ia_atime ;
914 struct timespec ia_mtime ;
915 struct timespec ia_ctime ;
916 struct file *ia_file ;
917};
918#line 119 "include/linux/quota.h"
919struct if_dqinfo {
920 __u64 dqi_bgrace ;
921 __u64 dqi_igrace ;
922 __u32 dqi_flags ;
923 __u32 dqi_valid ;
924};
925#line 176 "include/linux/percpu_counter.h"
926struct fs_disk_quota {
927 __s8 d_version ;
928 __s8 d_flags ;
929 __u16 d_fieldmask ;
930 __u32 d_id ;
931 __u64 d_blk_hardlimit ;
932 __u64 d_blk_softlimit ;
933 __u64 d_ino_hardlimit ;
934 __u64 d_ino_softlimit ;
935 __u64 d_bcount ;
936 __u64 d_icount ;
937 __s32 d_itimer ;
938 __s32 d_btimer ;
939 __u16 d_iwarns ;
940 __u16 d_bwarns ;
941 __s32 d_padding2 ;
942 __u64 d_rtb_hardlimit ;
943 __u64 d_rtb_softlimit ;
944 __u64 d_rtbcount ;
945 __s32 d_rtbtimer ;
946 __u16 d_rtbwarns ;
947 __s16 d_padding3 ;
948 char d_padding4[8U] ;
949};
950#line 75 "include/linux/dqblk_xfs.h"
951struct fs_qfilestat {
952 __u64 qfs_ino ;
953 __u64 qfs_nblks ;
954 __u32 qfs_nextents ;
955};
956#line 150 "include/linux/dqblk_xfs.h"
957typedef struct fs_qfilestat fs_qfilestat_t;
958#line 151 "include/linux/dqblk_xfs.h"
959struct fs_quota_stat {
960 __s8 qs_version ;
961 __u16 qs_flags ;
962 __s8 qs_pad ;
963 fs_qfilestat_t qs_uquota ;
964 fs_qfilestat_t qs_gquota ;
965 __u32 qs_incoredqs ;
966 __s32 qs_btimelimit ;
967 __s32 qs_itimelimit ;
968 __s32 qs_rtbtimelimit ;
969 __u16 qs_bwarnlimit ;
970 __u16 qs_iwarnlimit ;
971};
972#line 165
973struct dquot;
974#line 165
975struct dquot;
976#line 185 "include/linux/quota.h"
977typedef __kernel_uid32_t qid_t;
978#line 186 "include/linux/quota.h"
979typedef long long qsize_t;
980#line 189 "include/linux/quota.h"
981struct mem_dqblk {
982 qsize_t dqb_bhardlimit ;
983 qsize_t dqb_bsoftlimit ;
984 qsize_t dqb_curspace ;
985 qsize_t dqb_rsvspace ;
986 qsize_t dqb_ihardlimit ;
987 qsize_t dqb_isoftlimit ;
988 qsize_t dqb_curinodes ;
989 time_t dqb_btime ;
990 time_t dqb_itime ;
991};
992#line 211
993struct quota_format_type;
994#line 211
995struct quota_format_type;
996#line 212 "include/linux/quota.h"
997struct mem_dqinfo {
998 struct quota_format_type *dqi_format ;
999 int dqi_fmt_id ;
1000 struct list_head dqi_dirty_list ;
1001 unsigned long dqi_flags ;
1002 unsigned int dqi_bgrace ;
1003 unsigned int dqi_igrace ;
1004 qsize_t dqi_maxblimit ;
1005 qsize_t dqi_maxilimit ;
1006 void *dqi_priv ;
1007};
1008#line 275 "include/linux/quota.h"
1009struct dquot {
1010 struct hlist_node dq_hash ;
1011 struct list_head dq_inuse ;
1012 struct list_head dq_free ;
1013 struct list_head dq_dirty ;
1014 struct mutex dq_lock ;
1015 atomic_t dq_count ;
1016 wait_queue_head_t dq_wait_unused ;
1017 struct super_block *dq_sb ;
1018 unsigned int dq_id ;
1019 loff_t dq_off ;
1020 unsigned long dq_flags ;
1021 short dq_type ;
1022 struct mem_dqblk dq_dqb ;
1023};
1024#line 303 "include/linux/quota.h"
1025struct quota_format_ops {
1026 int (*check_quota_file)(struct super_block * , int ) ;
1027 int (*read_file_info)(struct super_block * , int ) ;
1028 int (*write_file_info)(struct super_block * , int ) ;
1029 int (*free_file_info)(struct super_block * , int ) ;
1030 int (*read_dqblk)(struct dquot * ) ;
1031 int (*commit_dqblk)(struct dquot * ) ;
1032 int (*release_dqblk)(struct dquot * ) ;
1033};
1034#line 314 "include/linux/quota.h"
1035struct dquot_operations {
1036 int (*write_dquot)(struct dquot * ) ;
1037 struct dquot *(*alloc_dquot)(struct super_block * , int ) ;
1038 void (*destroy_dquot)(struct dquot * ) ;
1039 int (*acquire_dquot)(struct dquot * ) ;
1040 int (*release_dquot)(struct dquot * ) ;
1041 int (*mark_dirty)(struct dquot * ) ;
1042 int (*write_info)(struct super_block * , int ) ;
1043 qsize_t *(*get_reserved_space)(struct inode * ) ;
1044};
1045#line 328 "include/linux/quota.h"
1046struct quotactl_ops {
1047 int (*quota_on)(struct super_block * , int , int , struct path * ) ;
1048 int (*quota_on_meta)(struct super_block * , int , int ) ;
1049 int (*quota_off)(struct super_block * , int ) ;
1050 int (*quota_sync)(struct super_block * , int , int ) ;
1051 int (*get_info)(struct super_block * , int , struct if_dqinfo * ) ;
1052 int (*set_info)(struct super_block * , int , struct if_dqinfo * ) ;
1053 int (*get_dqblk)(struct super_block * , int , qid_t , struct fs_disk_quota * ) ;
1054 int (*set_dqblk)(struct super_block * , int , qid_t , struct fs_disk_quota * ) ;
1055 int (*get_xstate)(struct super_block * , struct fs_quota_stat * ) ;
1056 int (*set_xstate)(struct super_block * , unsigned int , int ) ;
1057};
1058#line 344 "include/linux/quota.h"
1059struct quota_format_type {
1060 int qf_fmt_id ;
1061 struct quota_format_ops const *qf_ops ;
1062 struct module *qf_owner ;
1063 struct quota_format_type *qf_next ;
1064};
1065#line 390 "include/linux/quota.h"
1066struct quota_info {
1067 unsigned int flags ;
1068 struct mutex dqio_mutex ;
1069 struct mutex dqonoff_mutex ;
1070 struct rw_semaphore dqptr_sem ;
1071 struct inode *files[2U] ;
1072 struct mem_dqinfo info[2U] ;
1073 struct quota_format_ops const *ops[2U] ;
1074};
1075#line 421
1076struct address_space;
1077#line 421
1078struct address_space;
1079#line 422
1080struct writeback_control;
1081#line 422
1082struct writeback_control;
1083#line 585 "include/linux/fs.h"
1084union __anonunion_arg_138 {
1085 char *buf ;
1086 void *data ;
1087};
1088#line 585 "include/linux/fs.h"
1089struct __anonstruct_read_descriptor_t_137 {
1090 size_t written ;
1091 size_t count ;
1092 union __anonunion_arg_138 arg ;
1093 int error ;
1094};
1095#line 585 "include/linux/fs.h"
1096typedef struct __anonstruct_read_descriptor_t_137 read_descriptor_t;
1097#line 588 "include/linux/fs.h"
1098struct address_space_operations {
1099 int (*writepage)(struct page * , struct writeback_control * ) ;
1100 int (*readpage)(struct file * , struct page * ) ;
1101 int (*writepages)(struct address_space * , struct writeback_control * ) ;
1102 int (*set_page_dirty)(struct page * ) ;
1103 int (*readpages)(struct file * , struct address_space * , struct list_head * ,
1104 unsigned int ) ;
1105 int (*write_begin)(struct file * , struct address_space * , loff_t , unsigned int ,
1106 unsigned int , struct page ** , void ** ) ;
1107 int (*write_end)(struct file * , struct address_space * , loff_t , unsigned int ,
1108 unsigned int , struct page * , void * ) ;
1109 sector_t (*bmap)(struct address_space * , sector_t ) ;
1110 void (*invalidatepage)(struct page * , unsigned long ) ;
1111 int (*releasepage)(struct page * , gfp_t ) ;
1112 void (*freepage)(struct page * ) ;
1113 ssize_t (*direct_IO)(int , struct kiocb * , struct iovec const * , loff_t ,
1114 unsigned long ) ;
1115 int (*get_xip_mem)(struct address_space * , unsigned long , int , void ** , unsigned long * ) ;
1116 int (*migratepage)(struct address_space * , struct page * , struct page * , enum migrate_mode ) ;
1117 int (*launder_page)(struct page * ) ;
1118 int (*is_partially_uptodate)(struct page * , read_descriptor_t * , unsigned long ) ;
1119 int (*error_remove_page)(struct address_space * , struct page * ) ;
1120};
1121#line 642
1122struct backing_dev_info;
1123#line 642
1124struct backing_dev_info;
1125#line 643 "include/linux/fs.h"
1126struct address_space {
1127 struct inode *host ;
1128 struct radix_tree_root page_tree ;
1129 spinlock_t tree_lock ;
1130 unsigned int i_mmap_writable ;
1131 struct prio_tree_root i_mmap ;
1132 struct list_head i_mmap_nonlinear ;
1133 struct mutex i_mmap_mutex ;
1134 unsigned long nrpages ;
1135 unsigned long writeback_index ;
1136 struct address_space_operations const *a_ops ;
1137 unsigned long flags ;
1138 struct backing_dev_info *backing_dev_info ;
1139 spinlock_t private_lock ;
1140 struct list_head private_list ;
1141 struct address_space *assoc_mapping ;
1142};
1143#line 664
1144struct request_queue;
1145#line 664
1146struct request_queue;
1147#line 665
1148struct hd_struct;
1149#line 665
1150struct gendisk;
1151#line 665 "include/linux/fs.h"
1152struct block_device {
1153 dev_t bd_dev ;
1154 int bd_openers ;
1155 struct inode *bd_inode ;
1156 struct super_block *bd_super ;
1157 struct mutex bd_mutex ;
1158 struct list_head bd_inodes ;
1159 void *bd_claiming ;
1160 void *bd_holder ;
1161 int bd_holders ;
1162 bool bd_write_holder ;
1163 struct list_head bd_holder_disks ;
1164 struct block_device *bd_contains ;
1165 unsigned int bd_block_size ;
1166 struct hd_struct *bd_part ;
1167 unsigned int bd_part_count ;
1168 int bd_invalidated ;
1169 struct gendisk *bd_disk ;
1170 struct request_queue *bd_queue ;
1171 struct list_head bd_list ;
1172 unsigned long bd_private ;
1173 int bd_fsfreeze_count ;
1174 struct mutex bd_fsfreeze_mutex ;
1175};
1176#line 737
1177struct posix_acl;
1178#line 737
1179struct posix_acl;
1180#line 738
1181struct inode_operations;
1182#line 738 "include/linux/fs.h"
1183union __anonunion_ldv_15849_139 {
1184 unsigned int const i_nlink ;
1185 unsigned int __i_nlink ;
1186};
1187#line 738 "include/linux/fs.h"
1188union __anonunion_ldv_15868_140 {
1189 struct list_head i_dentry ;
1190 struct rcu_head i_rcu ;
1191};
1192#line 738
1193struct file_lock;
1194#line 738
1195struct cdev;
1196#line 738 "include/linux/fs.h"
1197union __anonunion_ldv_15885_141 {
1198 struct pipe_inode_info *i_pipe ;
1199 struct block_device *i_bdev ;
1200 struct cdev *i_cdev ;
1201};
1202#line 738 "include/linux/fs.h"
1203struct inode {
1204 umode_t i_mode ;
1205 unsigned short i_opflags ;
1206 uid_t i_uid ;
1207 gid_t i_gid ;
1208 unsigned int i_flags ;
1209 struct posix_acl *i_acl ;
1210 struct posix_acl *i_default_acl ;
1211 struct inode_operations const *i_op ;
1212 struct super_block *i_sb ;
1213 struct address_space *i_mapping ;
1214 void *i_security ;
1215 unsigned long i_ino ;
1216 union __anonunion_ldv_15849_139 ldv_15849 ;
1217 dev_t i_rdev ;
1218 struct timespec i_atime ;
1219 struct timespec i_mtime ;
1220 struct timespec i_ctime ;
1221 spinlock_t i_lock ;
1222 unsigned short i_bytes ;
1223 blkcnt_t i_blocks ;
1224 loff_t i_size ;
1225 unsigned long i_state ;
1226 struct mutex i_mutex ;
1227 unsigned long dirtied_when ;
1228 struct hlist_node i_hash ;
1229 struct list_head i_wb_list ;
1230 struct list_head i_lru ;
1231 struct list_head i_sb_list ;
1232 union __anonunion_ldv_15868_140 ldv_15868 ;
1233 atomic_t i_count ;
1234 unsigned int i_blkbits ;
1235 u64 i_version ;
1236 atomic_t i_dio_count ;
1237 atomic_t i_writecount ;
1238 struct file_operations const *i_fop ;
1239 struct file_lock *i_flock ;
1240 struct address_space i_data ;
1241 struct dquot *i_dquot[2U] ;
1242 struct list_head i_devices ;
1243 union __anonunion_ldv_15885_141 ldv_15885 ;
1244 __u32 i_generation ;
1245 __u32 i_fsnotify_mask ;
1246 struct hlist_head i_fsnotify_marks ;
1247 atomic_t i_readcount ;
1248 void *i_private ;
1249};
1250#line 941 "include/linux/fs.h"
1251struct fown_struct {
1252 rwlock_t lock ;
1253 struct pid *pid ;
1254 enum pid_type pid_type ;
1255 uid_t uid ;
1256 uid_t euid ;
1257 int signum ;
1258};
1259#line 949 "include/linux/fs.h"
1260struct file_ra_state {
1261 unsigned long start ;
1262 unsigned int size ;
1263 unsigned int async_size ;
1264 unsigned int ra_pages ;
1265 unsigned int mmap_miss ;
1266 loff_t prev_pos ;
1267};
1268#line 972 "include/linux/fs.h"
1269union __anonunion_f_u_142 {
1270 struct list_head fu_list ;
1271 struct rcu_head fu_rcuhead ;
1272};
1273#line 972 "include/linux/fs.h"
1274struct file {
1275 union __anonunion_f_u_142 f_u ;
1276 struct path f_path ;
1277 struct file_operations const *f_op ;
1278 spinlock_t f_lock ;
1279 int f_sb_list_cpu ;
1280 atomic_long_t f_count ;
1281 unsigned int f_flags ;
1282 fmode_t f_mode ;
1283 loff_t f_pos ;
1284 struct fown_struct f_owner ;
1285 struct cred const *f_cred ;
1286 struct file_ra_state f_ra ;
1287 u64 f_version ;
1288 void *f_security ;
1289 void *private_data ;
1290 struct list_head f_ep_links ;
1291 struct list_head f_tfile_llink ;
1292 struct address_space *f_mapping ;
1293 unsigned long f_mnt_write_state ;
1294};
1295#line 1111
1296struct files_struct;
1297#line 1111 "include/linux/fs.h"
1298typedef struct files_struct *fl_owner_t;
1299#line 1112 "include/linux/fs.h"
1300struct file_lock_operations {
1301 void (*fl_copy_lock)(struct file_lock * , struct file_lock * ) ;
1302 void (*fl_release_private)(struct file_lock * ) ;
1303};
1304#line 1117 "include/linux/fs.h"
1305struct lock_manager_operations {
1306 int (*lm_compare_owner)(struct file_lock * , struct file_lock * ) ;
1307 void (*lm_notify)(struct file_lock * ) ;
1308 int (*lm_grant)(struct file_lock * , struct file_lock * , int ) ;
1309 void (*lm_release_private)(struct file_lock * ) ;
1310 void (*lm_break)(struct file_lock * ) ;
1311 int (*lm_change)(struct file_lock ** , int ) ;
1312};
1313#line 1134
1314struct nlm_lockowner;
1315#line 1134
1316struct nlm_lockowner;
1317#line 1135 "include/linux/fs.h"
1318struct nfs_lock_info {
1319 u32 state ;
1320 struct nlm_lockowner *owner ;
1321 struct list_head list ;
1322};
1323#line 14 "include/linux/nfs_fs_i.h"
1324struct nfs4_lock_state;
1325#line 14
1326struct nfs4_lock_state;
1327#line 15 "include/linux/nfs_fs_i.h"
1328struct nfs4_lock_info {
1329 struct nfs4_lock_state *owner ;
1330};
1331#line 19
1332struct fasync_struct;
1333#line 19 "include/linux/nfs_fs_i.h"
1334struct __anonstruct_afs_144 {
1335 struct list_head link ;
1336 int state ;
1337};
1338#line 19 "include/linux/nfs_fs_i.h"
1339union __anonunion_fl_u_143 {
1340 struct nfs_lock_info nfs_fl ;
1341 struct nfs4_lock_info nfs4_fl ;
1342 struct __anonstruct_afs_144 afs ;
1343};
1344#line 19 "include/linux/nfs_fs_i.h"
1345struct file_lock {
1346 struct file_lock *fl_next ;
1347 struct list_head fl_link ;
1348 struct list_head fl_block ;
1349 fl_owner_t fl_owner ;
1350 unsigned int fl_flags ;
1351 unsigned char fl_type ;
1352 unsigned int fl_pid ;
1353 struct pid *fl_nspid ;
1354 wait_queue_head_t fl_wait ;
1355 struct file *fl_file ;
1356 loff_t fl_start ;
1357 loff_t fl_end ;
1358 struct fasync_struct *fl_fasync ;
1359 unsigned long fl_break_time ;
1360 unsigned long fl_downgrade_time ;
1361 struct file_lock_operations const *fl_ops ;
1362 struct lock_manager_operations const *fl_lmops ;
1363 union __anonunion_fl_u_143 fl_u ;
1364};
1365#line 1221 "include/linux/fs.h"
1366struct fasync_struct {
1367 spinlock_t fa_lock ;
1368 int magic ;
1369 int fa_fd ;
1370 struct fasync_struct *fa_next ;
1371 struct file *fa_file ;
1372 struct rcu_head fa_rcu ;
1373};
1374#line 1417
1375struct file_system_type;
1376#line 1417
1377struct super_operations;
1378#line 1417
1379struct xattr_handler;
1380#line 1417
1381struct mtd_info;
1382#line 1417 "include/linux/fs.h"
1383struct super_block {
1384 struct list_head s_list ;
1385 dev_t s_dev ;
1386 unsigned char s_dirt ;
1387 unsigned char s_blocksize_bits ;
1388 unsigned long s_blocksize ;
1389 loff_t s_maxbytes ;
1390 struct file_system_type *s_type ;
1391 struct super_operations const *s_op ;
1392 struct dquot_operations const *dq_op ;
1393 struct quotactl_ops const *s_qcop ;
1394 struct export_operations const *s_export_op ;
1395 unsigned long s_flags ;
1396 unsigned long s_magic ;
1397 struct dentry *s_root ;
1398 struct rw_semaphore s_umount ;
1399 struct mutex s_lock ;
1400 int s_count ;
1401 atomic_t s_active ;
1402 void *s_security ;
1403 struct xattr_handler const **s_xattr ;
1404 struct list_head s_inodes ;
1405 struct hlist_bl_head s_anon ;
1406 struct list_head *s_files ;
1407 struct list_head s_mounts ;
1408 struct list_head s_dentry_lru ;
1409 int s_nr_dentry_unused ;
1410 spinlock_t s_inode_lru_lock ;
1411 struct list_head s_inode_lru ;
1412 int s_nr_inodes_unused ;
1413 struct block_device *s_bdev ;
1414 struct backing_dev_info *s_bdi ;
1415 struct mtd_info *s_mtd ;
1416 struct hlist_node s_instances ;
1417 struct quota_info s_dquot ;
1418 int s_frozen ;
1419 wait_queue_head_t s_wait_unfrozen ;
1420 char s_id[32U] ;
1421 u8 s_uuid[16U] ;
1422 void *s_fs_info ;
1423 unsigned int s_max_links ;
1424 fmode_t s_mode ;
1425 u32 s_time_gran ;
1426 struct mutex s_vfs_rename_mutex ;
1427 char *s_subtype ;
1428 char *s_options ;
1429 struct dentry_operations const *s_d_op ;
1430 int cleancache_poolid ;
1431 struct shrinker s_shrink ;
1432 atomic_long_t s_remove_count ;
1433 int s_readonly_remount ;
1434};
1435#line 1563 "include/linux/fs.h"
1436struct fiemap_extent_info {
1437 unsigned int fi_flags ;
1438 unsigned int fi_extents_mapped ;
1439 unsigned int fi_extents_max ;
1440 struct fiemap_extent *fi_extents_start ;
1441};
1442#line 1602 "include/linux/fs.h"
1443struct file_operations {
1444 struct module *owner ;
1445 loff_t (*llseek)(struct file * , loff_t , int ) ;
1446 ssize_t (*read)(struct file * , char * , size_t , loff_t * ) ;
1447 ssize_t (*write)(struct file * , char const * , size_t , loff_t * ) ;
1448 ssize_t (*aio_read)(struct kiocb * , struct iovec const * , unsigned long ,
1449 loff_t ) ;
1450 ssize_t (*aio_write)(struct kiocb * , struct iovec const * , unsigned long ,
1451 loff_t ) ;
1452 int (*readdir)(struct file * , void * , int (*)(void * , char const * , int ,
1453 loff_t , u64 , unsigned int ) ) ;
1454 unsigned int (*poll)(struct file * , struct poll_table_struct * ) ;
1455 long (*unlocked_ioctl)(struct file * , unsigned int , unsigned long ) ;
1456 long (*compat_ioctl)(struct file * , unsigned int , unsigned long ) ;
1457 int (*mmap)(struct file * , struct vm_area_struct * ) ;
1458 int (*open)(struct inode * , struct file * ) ;
1459 int (*flush)(struct file * , fl_owner_t ) ;
1460 int (*release)(struct inode * , struct file * ) ;
1461 int (*fsync)(struct file * , loff_t , loff_t , int ) ;
1462 int (*aio_fsync)(struct kiocb * , int ) ;
1463 int (*fasync)(int , struct file * , int ) ;
1464 int (*lock)(struct file * , int , struct file_lock * ) ;
1465 ssize_t (*sendpage)(struct file * , struct page * , int , size_t , loff_t * ,
1466 int ) ;
1467 unsigned long (*get_unmapped_area)(struct file * , unsigned long , unsigned long ,
1468 unsigned long , unsigned long ) ;
1469 int (*check_flags)(int ) ;
1470 int (*flock)(struct file * , int , struct file_lock * ) ;
1471 ssize_t (*splice_write)(struct pipe_inode_info * , struct file * , loff_t * , size_t ,
1472 unsigned int ) ;
1473 ssize_t (*splice_read)(struct file * , loff_t * , struct pipe_inode_info * , size_t ,
1474 unsigned int ) ;
1475 int (*setlease)(struct file * , long , struct file_lock ** ) ;
1476 long (*fallocate)(struct file * , int , loff_t , loff_t ) ;
1477};
1478#line 1637 "include/linux/fs.h"
1479struct inode_operations {
1480 struct dentry *(*lookup)(struct inode * , struct dentry * , struct nameidata * ) ;
1481 void *(*follow_link)(struct dentry * , struct nameidata * ) ;
1482 int (*permission)(struct inode * , int ) ;
1483 struct posix_acl *(*get_acl)(struct inode * , int ) ;
1484 int (*readlink)(struct dentry * , char * , int ) ;
1485 void (*put_link)(struct dentry * , struct nameidata * , void * ) ;
1486 int (*create)(struct inode * , struct dentry * , umode_t , struct nameidata * ) ;
1487 int (*link)(struct dentry * , struct inode * , struct dentry * ) ;
1488 int (*unlink)(struct inode * , struct dentry * ) ;
1489 int (*symlink)(struct inode * , struct dentry * , char const * ) ;
1490 int (*mkdir)(struct inode * , struct dentry * , umode_t ) ;
1491 int (*rmdir)(struct inode * , struct dentry * ) ;
1492 int (*mknod)(struct inode * , struct dentry * , umode_t , dev_t ) ;
1493 int (*rename)(struct inode * , struct dentry * , struct inode * , struct dentry * ) ;
1494 void (*truncate)(struct inode * ) ;
1495 int (*setattr)(struct dentry * , struct iattr * ) ;
1496 int (*getattr)(struct vfsmount * , struct dentry * , struct kstat * ) ;
1497 int (*setxattr)(struct dentry * , char const * , void const * , size_t , int ) ;
1498 ssize_t (*getxattr)(struct dentry * , char const * , void * , size_t ) ;
1499 ssize_t (*listxattr)(struct dentry * , char * , size_t ) ;
1500 int (*removexattr)(struct dentry * , char const * ) ;
1501 void (*truncate_range)(struct inode * , loff_t , loff_t ) ;
1502 int (*fiemap)(struct inode * , struct fiemap_extent_info * , u64 , u64 ) ;
1503};
1504#line 1682 "include/linux/fs.h"
1505struct super_operations {
1506 struct inode *(*alloc_inode)(struct super_block * ) ;
1507 void (*destroy_inode)(struct inode * ) ;
1508 void (*dirty_inode)(struct inode * , int ) ;
1509 int (*write_inode)(struct inode * , struct writeback_control * ) ;
1510 int (*drop_inode)(struct inode * ) ;
1511 void (*evict_inode)(struct inode * ) ;
1512 void (*put_super)(struct super_block * ) ;
1513 void (*write_super)(struct super_block * ) ;
1514 int (*sync_fs)(struct super_block * , int ) ;
1515 int (*freeze_fs)(struct super_block * ) ;
1516 int (*unfreeze_fs)(struct super_block * ) ;
1517 int (*statfs)(struct dentry * , struct kstatfs * ) ;
1518 int (*remount_fs)(struct super_block * , int * , char * ) ;
1519 void (*umount_begin)(struct super_block * ) ;
1520 int (*show_options)(struct seq_file * , struct dentry * ) ;
1521 int (*show_devname)(struct seq_file * , struct dentry * ) ;
1522 int (*show_path)(struct seq_file * , struct dentry * ) ;
1523 int (*show_stats)(struct seq_file * , struct dentry * ) ;
1524 ssize_t (*quota_read)(struct super_block * , int , char * , size_t , loff_t ) ;
1525 ssize_t (*quota_write)(struct super_block * , int , char const * , size_t ,
1526 loff_t ) ;
1527 int (*bdev_try_to_free_page)(struct super_block * , struct page * , gfp_t ) ;
1528 int (*nr_cached_objects)(struct super_block * ) ;
1529 void (*free_cached_objects)(struct super_block * , int ) ;
1530};
1531#line 1834 "include/linux/fs.h"
1532struct file_system_type {
1533 char const *name ;
1534 int fs_flags ;
1535 struct dentry *(*mount)(struct file_system_type * , int , char const * , void * ) ;
1536 void (*kill_sb)(struct super_block * ) ;
1537 struct module *owner ;
1538 struct file_system_type *next ;
1539 struct hlist_head fs_supers ;
1540 struct lock_class_key s_lock_key ;
1541 struct lock_class_key s_umount_key ;
1542 struct lock_class_key s_vfs_rename_key ;
1543 struct lock_class_key i_lock_key ;
1544 struct lock_class_key i_mutex_key ;
1545 struct lock_class_key i_mutex_dir_key ;
1546};
1547#line 2674 "include/linux/fs.h"
1548struct exception_table_entry {
1549 unsigned long insn ;
1550 unsigned long fixup ;
1551};
1552#line 1 "<compiler builtins>"
1553long __builtin_expect(long , long ) ;
1554#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
1555void ldv_spin_lock(void) ;
1556#line 3
1557void ldv_spin_unlock(void) ;
1558#line 4
1559int ldv_spin_trylock(void) ;
1560#line 98 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/bitops.h"
1561__inline static void clear_bit(int nr , unsigned long volatile *addr )
1562{ long volatile *__cil_tmp3 ;
1563
1564 {
1565#line 105
1566 __cil_tmp3 = (long volatile *)addr;
1567#line 105
1568 __asm__ volatile (".section .smp_locks,\"a\"\n.balign 4\n.long 671f - .\n.previous\n671:\n\tlock; btr %1,%0": "+m" (*__cil_tmp3): "Ir" (nr));
1569#line 107
1570 return;
1571}
1572}
1573#line 195 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/bitops.h"
1574__inline static int test_and_set_bit(int nr , unsigned long volatile *addr )
1575{ int oldbit ;
1576 long volatile *__cil_tmp4 ;
1577
1578 {
1579#line 199
1580 __cil_tmp4 = (long volatile *)addr;
1581#line 199
1582 __asm__ volatile (".section .smp_locks,\"a\"\n.balign 4\n.long 671f - .\n.previous\n671:\n\tlock; bts %2,%1\n\tsbb %0,%0": "=r" (oldbit),
1583 "+m" (*__cil_tmp4): "Ir" (nr): "memory");
1584#line 202
1585 return (oldbit);
1586}
1587}
1588#line 101 "include/linux/printk.h"
1589extern int printk(char const * , ...) ;
1590#line 45 "include/linux/dynamic_debug.h"
1591extern int __dynamic_pr_debug(struct _ddebug * , char const * , ...) ;
1592#line 192 "include/linux/kernel.h"
1593extern void might_fault(void) ;
1594#line 137 "include/linux/ioport.h"
1595extern struct resource ioport_resource ;
1596#line 181
1597extern struct resource *__request_region(struct resource * , resource_size_t , resource_size_t ,
1598 char const * , int ) ;
1599#line 192
1600extern void __release_region(struct resource * , resource_size_t , resource_size_t ) ;
1601#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
1602__inline static void outb(unsigned char value , int port )
1603{
1604
1605 {
1606#line 308
1607 __asm__ volatile ("outb %b0, %w1": : "a" (value), "Nd" (port));
1608#line 309
1609 return;
1610}
1611}
1612#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
1613__inline static unsigned char inb(int port )
1614{ unsigned char value ;
1615
1616 {
1617#line 308
1618 __asm__ volatile ("inb %w1, %b0": "=a" (value): "Nd" (port));
1619#line 308
1620 return (value);
1621}
1622}
1623#line 26 "include/linux/export.h"
1624extern struct module __this_module ;
1625#line 220 "include/linux/slub_def.h"
1626extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t ) ;
1627#line 223
1628void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
1629#line 11 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
1630void ldv_check_alloc_flags(gfp_t flags ) ;
1631#line 12
1632void ldv_check_alloc_nonatomic(void) ;
1633#line 14
1634struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
1635#line 61 "include/linux/miscdevice.h"
1636extern int misc_register(struct miscdevice * ) ;
1637#line 62
1638extern int misc_deregister(struct miscdevice * ) ;
1639#line 47 "include/linux/reboot.h"
1640extern int register_reboot_notifier(struct notifier_block * ) ;
1641#line 48
1642extern int unregister_reboot_notifier(struct notifier_block * ) ;
1643#line 2402 "include/linux/fs.h"
1644extern loff_t no_llseek(struct file * , loff_t , int ) ;
1645#line 2407
1646extern int nonseekable_open(struct inode * , struct file * ) ;
1647#line 40 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/uaccess_64.h"
1648extern unsigned long _copy_to_user(void * , void const * , unsigned int ) ;
1649#line 63 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/uaccess_64.h"
1650__inline static int copy_to_user(void *dst , void const *src , unsigned int size )
1651{ unsigned long tmp ;
1652
1653 {
1654 {
1655#line 65
1656 might_fault();
1657#line 67
1658 tmp = _copy_to_user(dst, src, size);
1659 }
1660#line 67
1661 return ((int )tmp);
1662}
1663}
1664#line 61 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
1665static int max_units = 255;
1666#line 62 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
1667static int margin = 60;
1668#line 66 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
1669static bool nowayout = (bool )1;
1670#line 70 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
1671static unsigned long wdt_open ;
1672#line 71 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
1673static unsigned int expect_close ;
1674#line 72 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
1675static unsigned char revision ;
1676#line 75 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
1677static unsigned short address ;
1678#line 105 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
1679static int wdt_control_reg = 16;
1680#line 113 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
1681static int superio_inb(int reg )
1682{ unsigned char tmp ;
1683 unsigned char __cil_tmp3 ;
1684 int __cil_tmp4 ;
1685 unsigned char __cil_tmp5 ;
1686
1687 {
1688 {
1689#line 115
1690 __cil_tmp3 = (unsigned char )reg;
1691#line 115
1692 __cil_tmp4 = (int )__cil_tmp3;
1693#line 115
1694 __cil_tmp5 = (unsigned char )__cil_tmp4;
1695#line 115
1696 outb(__cil_tmp5, 46);
1697#line 116
1698 tmp = inb(47);
1699 }
1700#line 116
1701 return ((int )tmp);
1702}
1703}
1704#line 119 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
1705static void superio_outb(int val , int reg )
1706{ unsigned char __cil_tmp3 ;
1707 int __cil_tmp4 ;
1708 unsigned char __cil_tmp5 ;
1709 unsigned char __cil_tmp6 ;
1710 int __cil_tmp7 ;
1711 unsigned char __cil_tmp8 ;
1712
1713 {
1714 {
1715#line 121
1716 __cil_tmp3 = (unsigned char )reg;
1717#line 121
1718 __cil_tmp4 = (int )__cil_tmp3;
1719#line 121
1720 __cil_tmp5 = (unsigned char )__cil_tmp4;
1721#line 121
1722 outb(__cil_tmp5, 46);
1723#line 122
1724 __cil_tmp6 = (unsigned char )val;
1725#line 122
1726 __cil_tmp7 = (int )__cil_tmp6;
1727#line 122
1728 __cil_tmp8 = (unsigned char )__cil_tmp7;
1729#line 122
1730 outb(__cil_tmp8, 47);
1731 }
1732#line 123
1733 return;
1734}
1735}
1736#line 125 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
1737static int superio_inw(int reg )
1738{ int val ;
1739 int tmp ;
1740 unsigned char tmp___0 ;
1741 unsigned char tmp___1 ;
1742 unsigned char __cil_tmp6 ;
1743 int __cil_tmp7 ;
1744 unsigned char __cil_tmp8 ;
1745 int __cil_tmp9 ;
1746 unsigned char __cil_tmp10 ;
1747 int __cil_tmp11 ;
1748 unsigned char __cil_tmp12 ;
1749 int __cil_tmp13 ;
1750
1751 {
1752 {
1753#line 128
1754 tmp = reg;
1755#line 128
1756 reg = reg + 1;
1757#line 128
1758 __cil_tmp6 = (unsigned char )tmp;
1759#line 128
1760 __cil_tmp7 = (int )__cil_tmp6;
1761#line 128
1762 __cil_tmp8 = (unsigned char )__cil_tmp7;
1763#line 128
1764 outb(__cil_tmp8, 46);
1765#line 129
1766 tmp___0 = inb(47);
1767#line 129
1768 __cil_tmp9 = (int )tmp___0;
1769#line 129
1770 val = __cil_tmp9 << 8;
1771#line 130
1772 __cil_tmp10 = (unsigned char )reg;
1773#line 130
1774 __cil_tmp11 = (int )__cil_tmp10;
1775#line 130
1776 __cil_tmp12 = (unsigned char )__cil_tmp11;
1777#line 130
1778 outb(__cil_tmp12, 46);
1779#line 131
1780 tmp___1 = inb(47);
1781#line 131
1782 __cil_tmp13 = (int )tmp___1;
1783#line 131
1784 val = __cil_tmp13 | val;
1785 }
1786#line 132
1787 return (val);
1788}
1789}
1790#line 135 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
1791__inline static void superio_select(int ldn )
1792{ unsigned char __cil_tmp2 ;
1793 int __cil_tmp3 ;
1794 unsigned char __cil_tmp4 ;
1795
1796 {
1797 {
1798#line 137
1799 outb((unsigned char)7, 46);
1800#line 138
1801 __cil_tmp2 = (unsigned char )ldn;
1802#line 138
1803 __cil_tmp3 = (int )__cil_tmp2;
1804#line 138
1805 __cil_tmp4 = (unsigned char )__cil_tmp3;
1806#line 138
1807 outb(__cil_tmp4, 47);
1808 }
1809#line 139
1810 return;
1811}
1812}
1813#line 141 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
1814__inline static int superio_enter(void)
1815{ struct resource *tmp ;
1816 struct resource *__cil_tmp2 ;
1817 unsigned long __cil_tmp3 ;
1818 unsigned long __cil_tmp4 ;
1819
1820 {
1821 {
1822#line 146
1823 tmp = __request_region(& ioport_resource, 46ULL, 2ULL, "it8712f_wdt", 4194304);
1824 }
1825 {
1826#line 146
1827 __cil_tmp2 = (struct resource *)0;
1828#line 146
1829 __cil_tmp3 = (unsigned long )__cil_tmp2;
1830#line 146
1831 __cil_tmp4 = (unsigned long )tmp;
1832#line 146
1833 if (__cil_tmp4 == __cil_tmp3) {
1834#line 147
1835 return (-16);
1836 } else {
1837
1838 }
1839 }
1840 {
1841#line 149
1842 outb((unsigned char)135, 46);
1843#line 150
1844 outb((unsigned char)1, 46);
1845#line 151
1846 outb((unsigned char)85, 46);
1847#line 152
1848 outb((unsigned char)85, 46);
1849 }
1850#line 153
1851 return (0);
1852}
1853}
1854#line 156 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
1855__inline static void superio_exit(void)
1856{
1857
1858 {
1859 {
1860#line 158
1861 outb((unsigned char)2, 46);
1862#line 159
1863 outb((unsigned char)2, 47);
1864#line 160
1865 __release_region(& ioport_resource, 46ULL, 2ULL);
1866 }
1867#line 161
1868 return;
1869}
1870}
1871#line 163 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
1872__inline static void it8712f_wdt_ping(void)
1873{ int *__cil_tmp1 ;
1874 int __cil_tmp2 ;
1875 int __cil_tmp3 ;
1876 unsigned short *__cil_tmp4 ;
1877 unsigned short __cil_tmp5 ;
1878 int __cil_tmp6 ;
1879
1880 {
1881 {
1882#line 165
1883 __cil_tmp1 = & wdt_control_reg;
1884#line 165
1885 __cil_tmp2 = *__cil_tmp1;
1886#line 165
1887 __cil_tmp3 = __cil_tmp2 & 16;
1888#line 165
1889 if (__cil_tmp3 != 0) {
1890 {
1891#line 166
1892 __cil_tmp4 = & address;
1893#line 166
1894 __cil_tmp5 = *__cil_tmp4;
1895#line 166
1896 __cil_tmp6 = (int )__cil_tmp5;
1897#line 166
1898 inb(__cil_tmp6);
1899 }
1900 } else {
1901
1902 }
1903 }
1904#line 167
1905 return;
1906}
1907}
1908#line 169 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
1909static void it8712f_wdt_update_margin(void)
1910{ int config ;
1911 int units ;
1912 int *__cil_tmp3 ;
1913 unsigned int __cil_tmp4 ;
1914 int __cil_tmp5 ;
1915
1916 {
1917#line 171
1918 config = 80;
1919#line 172
1920 __cil_tmp3 = & margin;
1921#line 172
1922 units = *__cil_tmp3;
1923#line 177
1924 if (units <= max_units) {
1925 {
1926#line 178
1927 config = config | 128;
1928#line 179
1929 printk("<6>it8712f_wdt: timer margin %d seconds\n", units);
1930 }
1931 } else {
1932 {
1933#line 181
1934 units = units / 60;
1935#line 182
1936 printk("<6>it8712f_wdt: timer margin %d minutes\n", units);
1937 }
1938 }
1939 {
1940#line 184
1941 superio_outb(config, 114);
1942 }
1943 {
1944#line 186
1945 __cil_tmp4 = (unsigned int )revision;
1946#line 186
1947 if (__cil_tmp4 > 7U) {
1948 {
1949#line 187
1950 __cil_tmp5 = units >> 8;
1951#line 187
1952 superio_outb(__cil_tmp5, 116);
1953 }
1954 } else {
1955
1956 }
1957 }
1958 {
1959#line 188
1960 superio_outb(units, 115);
1961 }
1962#line 189
1963 return;
1964}
1965}
1966#line 191 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
1967static int it8712f_wdt_get_status(void)
1968{ int tmp ;
1969
1970 {
1971 {
1972#line 193
1973 tmp = superio_inb(113);
1974 }
1975#line 193
1976 if (tmp & 1) {
1977#line 194
1978 return (32);
1979 } else {
1980#line 196
1981 return (0);
1982 }
1983}
1984}
1985#line 199 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
1986static int it8712f_wdt_enable(void)
1987{ int ret ;
1988 int tmp ;
1989 struct _ddebug descriptor ;
1990 long tmp___0 ;
1991 struct _ddebug *__cil_tmp5 ;
1992 unsigned long __cil_tmp6 ;
1993 unsigned long __cil_tmp7 ;
1994 unsigned long __cil_tmp8 ;
1995 unsigned long __cil_tmp9 ;
1996 unsigned long __cil_tmp10 ;
1997 unsigned long __cil_tmp11 ;
1998 unsigned char __cil_tmp12 ;
1999 long __cil_tmp13 ;
2000 long __cil_tmp14 ;
2001 int *__cil_tmp15 ;
2002 int __cil_tmp16 ;
2003
2004 {
2005 {
2006#line 201
2007 tmp = superio_enter();
2008#line 201
2009 ret = tmp;
2010 }
2011#line 202
2012 if (ret != 0) {
2013#line 203
2014 return (ret);
2015 } else {
2016
2017 }
2018 {
2019#line 205
2020 __cil_tmp5 = & descriptor;
2021#line 205
2022 *((char const **)__cil_tmp5) = "it8712f_wdt";
2023#line 205
2024 __cil_tmp6 = (unsigned long )(& descriptor) + 8;
2025#line 205
2026 *((char const **)__cil_tmp6) = "it8712f_wdt_enable";
2027#line 205
2028 __cil_tmp7 = (unsigned long )(& descriptor) + 16;
2029#line 205
2030 *((char const **)__cil_tmp7) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p";
2031#line 205
2032 __cil_tmp8 = (unsigned long )(& descriptor) + 24;
2033#line 205
2034 *((char const **)__cil_tmp8) = "enabling watchdog timer\n";
2035#line 205
2036 __cil_tmp9 = (unsigned long )(& descriptor) + 32;
2037#line 205
2038 *((unsigned int *)__cil_tmp9) = 205U;
2039#line 205
2040 __cil_tmp10 = (unsigned long )(& descriptor) + 35;
2041#line 205
2042 *((unsigned char *)__cil_tmp10) = (unsigned char)0;
2043#line 205
2044 __cil_tmp11 = (unsigned long )(& descriptor) + 35;
2045#line 205
2046 __cil_tmp12 = *((unsigned char *)__cil_tmp11);
2047#line 205
2048 __cil_tmp13 = (long )__cil_tmp12;
2049#line 205
2050 __cil_tmp14 = __cil_tmp13 & 1L;
2051#line 205
2052 tmp___0 = __builtin_expect(__cil_tmp14, 0L);
2053 }
2054#line 205
2055 if (tmp___0 != 0L) {
2056 {
2057#line 205
2058 __dynamic_pr_debug(& descriptor, "it8712f_wdt: enabling watchdog timer\n");
2059 }
2060 } else {
2061
2062 }
2063 {
2064#line 206
2065 superio_select(7);
2066#line 208
2067 __cil_tmp15 = & wdt_control_reg;
2068#line 208
2069 __cil_tmp16 = *__cil_tmp15;
2070#line 208
2071 superio_outb(__cil_tmp16, 113);
2072#line 210
2073 it8712f_wdt_update_margin();
2074#line 212
2075 superio_exit();
2076#line 214
2077 it8712f_wdt_ping();
2078 }
2079#line 216
2080 return (0);
2081}
2082}
2083#line 219 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
2084static int it8712f_wdt_disable(void)
2085{ int ret ;
2086 int tmp ;
2087 struct _ddebug descriptor ;
2088 long tmp___0 ;
2089 struct _ddebug *__cil_tmp5 ;
2090 unsigned long __cil_tmp6 ;
2091 unsigned long __cil_tmp7 ;
2092 unsigned long __cil_tmp8 ;
2093 unsigned long __cil_tmp9 ;
2094 unsigned long __cil_tmp10 ;
2095 unsigned long __cil_tmp11 ;
2096 unsigned char __cil_tmp12 ;
2097 long __cil_tmp13 ;
2098 long __cil_tmp14 ;
2099 unsigned int __cil_tmp15 ;
2100
2101 {
2102 {
2103#line 221
2104 tmp = superio_enter();
2105#line 221
2106 ret = tmp;
2107 }
2108#line 222
2109 if (ret != 0) {
2110#line 223
2111 return (ret);
2112 } else {
2113
2114 }
2115 {
2116#line 225
2117 __cil_tmp5 = & descriptor;
2118#line 225
2119 *((char const **)__cil_tmp5) = "it8712f_wdt";
2120#line 225
2121 __cil_tmp6 = (unsigned long )(& descriptor) + 8;
2122#line 225
2123 *((char const **)__cil_tmp6) = "it8712f_wdt_disable";
2124#line 225
2125 __cil_tmp7 = (unsigned long )(& descriptor) + 16;
2126#line 225
2127 *((char const **)__cil_tmp7) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p";
2128#line 225
2129 __cil_tmp8 = (unsigned long )(& descriptor) + 24;
2130#line 225
2131 *((char const **)__cil_tmp8) = "disabling watchdog timer\n";
2132#line 225
2133 __cil_tmp9 = (unsigned long )(& descriptor) + 32;
2134#line 225
2135 *((unsigned int *)__cil_tmp9) = 225U;
2136#line 225
2137 __cil_tmp10 = (unsigned long )(& descriptor) + 35;
2138#line 225
2139 *((unsigned char *)__cil_tmp10) = (unsigned char)0;
2140#line 225
2141 __cil_tmp11 = (unsigned long )(& descriptor) + 35;
2142#line 225
2143 __cil_tmp12 = *((unsigned char *)__cil_tmp11);
2144#line 225
2145 __cil_tmp13 = (long )__cil_tmp12;
2146#line 225
2147 __cil_tmp14 = __cil_tmp13 & 1L;
2148#line 225
2149 tmp___0 = __builtin_expect(__cil_tmp14, 0L);
2150 }
2151#line 225
2152 if (tmp___0 != 0L) {
2153 {
2154#line 225
2155 __dynamic_pr_debug(& descriptor, "it8712f_wdt: disabling watchdog timer\n");
2156 }
2157 } else {
2158
2159 }
2160 {
2161#line 226
2162 superio_select(7);
2163#line 228
2164 superio_outb(0, 114);
2165#line 229
2166 superio_outb(0, 113);
2167 }
2168 {
2169#line 230
2170 __cil_tmp15 = (unsigned int )revision;
2171#line 230
2172 if (__cil_tmp15 > 7U) {
2173 {
2174#line 231
2175 superio_outb(0, 116);
2176 }
2177 } else {
2178
2179 }
2180 }
2181 {
2182#line 232
2183 superio_outb(0, 115);
2184#line 234
2185 superio_exit();
2186 }
2187#line 235
2188 return (0);
2189}
2190}
2191#line 238 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
2192static int it8712f_wdt_notify(struct notifier_block *this , unsigned long code , void *unused )
2193{ bool *__cil_tmp4 ;
2194 bool __cil_tmp5 ;
2195
2196 {
2197#line 241
2198 if (code == 2UL) {
2199#line 241
2200 goto _L;
2201 } else
2202#line 241
2203 if (code == 3UL) {
2204 _L:
2205 {
2206#line 242
2207 __cil_tmp4 = & nowayout;
2208#line 242
2209 __cil_tmp5 = *__cil_tmp4;
2210#line 242
2211 if (! __cil_tmp5) {
2212 {
2213#line 243
2214 it8712f_wdt_disable();
2215 }
2216 } else {
2217
2218 }
2219 }
2220 } else {
2221
2222 }
2223#line 245
2224 return (0);
2225}
2226}
2227#line 248 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
2228static struct notifier_block it8712f_wdt_notifier = {& it8712f_wdt_notify, (struct notifier_block *)0, 0};
2229#line 252 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
2230static ssize_t it8712f_wdt_write(struct file *file , char const *data , size_t len ,
2231 loff_t *ppos )
2232{ size_t i ;
2233 char c ;
2234 int __ret_gu ;
2235 unsigned long __val_gu ;
2236 signed char __cil_tmp9 ;
2237 int __cil_tmp10 ;
2238
2239 {
2240#line 256
2241 if (len != 0UL) {
2242 {
2243#line 259
2244 it8712f_wdt_ping();
2245#line 261
2246 expect_close = 0U;
2247#line 262
2248 i = 0UL;
2249 }
2250#line 262
2251 goto ldv_18106;
2252 ldv_18105:
2253 {
2254#line 264
2255 might_fault();
2256 }
2257#line 264
2258 if (1 == 1) {
2259#line 264
2260 goto case_1;
2261 } else
2262#line 264
2263 if (1 == 2) {
2264#line 264
2265 goto case_2;
2266 } else
2267#line 264
2268 if (1 == 4) {
2269#line 264
2270 goto case_4;
2271 } else
2272#line 264
2273 if (1 == 8) {
2274#line 264
2275 goto case_8;
2276 } else {
2277 {
2278#line 264
2279 goto switch_default;
2280#line 264
2281 if (0) {
2282 case_1:
2283#line 264
2284 __asm__ volatile ("call __get_user_1": "=a" (__ret_gu), "=d" (__val_gu): "0" (data + i));
2285#line 264
2286 goto ldv_18099;
2287 case_2:
2288#line 264
2289 __asm__ volatile ("call __get_user_2": "=a" (__ret_gu), "=d" (__val_gu): "0" (data + i));
2290#line 264
2291 goto ldv_18099;
2292 case_4:
2293#line 264
2294 __asm__ volatile ("call __get_user_4": "=a" (__ret_gu), "=d" (__val_gu): "0" (data + i));
2295#line 264
2296 goto ldv_18099;
2297 case_8:
2298#line 264
2299 __asm__ volatile ("call __get_user_8": "=a" (__ret_gu), "=d" (__val_gu): "0" (data + i));
2300#line 264
2301 goto ldv_18099;
2302 switch_default:
2303#line 264
2304 __asm__ volatile ("call __get_user_X": "=a" (__ret_gu), "=d" (__val_gu): "0" (data + i));
2305#line 264
2306 goto ldv_18099;
2307 } else {
2308 switch_break: ;
2309 }
2310 }
2311 }
2312 ldv_18099:
2313#line 264
2314 c = (char )__val_gu;
2315#line 264
2316 if (__ret_gu != 0) {
2317#line 265
2318 return (-14L);
2319 } else {
2320
2321 }
2322 {
2323#line 266
2324 __cil_tmp9 = (signed char )c;
2325#line 266
2326 __cil_tmp10 = (int )__cil_tmp9;
2327#line 266
2328 if (__cil_tmp10 == 86) {
2329#line 267
2330 expect_close = 42U;
2331 } else {
2332
2333 }
2334 }
2335#line 262
2336 i = i + 1UL;
2337 ldv_18106: ;
2338#line 262
2339 if (i < len) {
2340#line 263
2341 goto ldv_18105;
2342 } else {
2343#line 265
2344 goto ldv_18107;
2345 }
2346 ldv_18107: ;
2347 } else {
2348
2349 }
2350#line 271
2351 return ((ssize_t )len);
2352}
2353}
2354#line 274 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
2355static long it8712f_wdt_ioctl(struct file *file , unsigned int cmd , unsigned long arg )
2356{ void *argp ;
2357 int *p ;
2358 struct watchdog_info ident ;
2359 int value ;
2360 int ret ;
2361 int tmp ;
2362 int __ret_pu ;
2363 int __pu_val ;
2364 int __ret_pu___0 ;
2365 int __pu_val___0 ;
2366 int __ret_gu ;
2367 unsigned long __val_gu ;
2368 int __ret_pu___1 ;
2369 int __pu_val___1 ;
2370 struct watchdog_info *__cil_tmp18 ;
2371 unsigned long __cil_tmp19 ;
2372 unsigned long __cil_tmp20 ;
2373 unsigned long __cil_tmp21 ;
2374 unsigned long __cil_tmp22 ;
2375 unsigned long __cil_tmp23 ;
2376 unsigned long __cil_tmp24 ;
2377 unsigned long __cil_tmp25 ;
2378 unsigned long __cil_tmp26 ;
2379 unsigned long __cil_tmp27 ;
2380 unsigned long __cil_tmp28 ;
2381 unsigned long __cil_tmp29 ;
2382 unsigned long __cil_tmp30 ;
2383 unsigned long __cil_tmp31 ;
2384 unsigned long __cil_tmp32 ;
2385 unsigned long __cil_tmp33 ;
2386 unsigned long __cil_tmp34 ;
2387 unsigned long __cil_tmp35 ;
2388 unsigned long __cil_tmp36 ;
2389 unsigned long __cil_tmp37 ;
2390 unsigned long __cil_tmp38 ;
2391 unsigned long __cil_tmp39 ;
2392 unsigned long __cil_tmp40 ;
2393 unsigned long __cil_tmp41 ;
2394 unsigned long __cil_tmp42 ;
2395 unsigned long __cil_tmp43 ;
2396 unsigned long __cil_tmp44 ;
2397 unsigned long __cil_tmp45 ;
2398 unsigned long __cil_tmp46 ;
2399 unsigned long __cil_tmp47 ;
2400 unsigned long __cil_tmp48 ;
2401 unsigned long __cil_tmp49 ;
2402 unsigned long __cil_tmp50 ;
2403 unsigned long __cil_tmp51 ;
2404 unsigned long __cil_tmp52 ;
2405 unsigned long __cil_tmp53 ;
2406 unsigned long __cil_tmp54 ;
2407 unsigned long __cil_tmp55 ;
2408 unsigned long __cil_tmp56 ;
2409 unsigned long __cil_tmp57 ;
2410 unsigned long __cil_tmp58 ;
2411 unsigned long __cil_tmp59 ;
2412 unsigned long __cil_tmp60 ;
2413 unsigned long __cil_tmp61 ;
2414 unsigned long __cil_tmp62 ;
2415 unsigned long __cil_tmp63 ;
2416 unsigned long __cil_tmp64 ;
2417 unsigned long __cil_tmp65 ;
2418 unsigned long __cil_tmp66 ;
2419 unsigned long __cil_tmp67 ;
2420 unsigned long __cil_tmp68 ;
2421 unsigned long __cil_tmp69 ;
2422 unsigned long __cil_tmp70 ;
2423 unsigned long __cil_tmp71 ;
2424 unsigned long __cil_tmp72 ;
2425 unsigned long __cil_tmp73 ;
2426 unsigned long __cil_tmp74 ;
2427 unsigned long __cil_tmp75 ;
2428 unsigned long __cil_tmp76 ;
2429 unsigned long __cil_tmp77 ;
2430 unsigned long __cil_tmp78 ;
2431 unsigned long __cil_tmp79 ;
2432 unsigned long __cil_tmp80 ;
2433 unsigned long __cil_tmp81 ;
2434 unsigned long __cil_tmp82 ;
2435 unsigned long __cil_tmp83 ;
2436 unsigned long __cil_tmp84 ;
2437 unsigned long __cil_tmp85 ;
2438 unsigned long __cil_tmp86 ;
2439 unsigned long __cil_tmp87 ;
2440 unsigned long __cil_tmp88 ;
2441 unsigned long __cil_tmp89 ;
2442 unsigned long __cil_tmp90 ;
2443 unsigned long __cil_tmp91 ;
2444 unsigned long __cil_tmp92 ;
2445 unsigned long __cil_tmp93 ;
2446 unsigned long __cil_tmp94 ;
2447 unsigned long __cil_tmp95 ;
2448 unsigned long __cil_tmp96 ;
2449 unsigned long __cil_tmp97 ;
2450 unsigned long __cil_tmp98 ;
2451 unsigned long __cil_tmp99 ;
2452 unsigned long __cil_tmp100 ;
2453 unsigned long __cil_tmp101 ;
2454 unsigned long __cil_tmp102 ;
2455 unsigned long __cil_tmp103 ;
2456 unsigned long __cil_tmp104 ;
2457 unsigned long __cil_tmp105 ;
2458 unsigned long __cil_tmp106 ;
2459 unsigned long __cil_tmp107 ;
2460 unsigned long __cil_tmp108 ;
2461 unsigned long __cil_tmp109 ;
2462 unsigned long __cil_tmp110 ;
2463 unsigned long __cil_tmp111 ;
2464 unsigned long __cil_tmp112 ;
2465 unsigned long __cil_tmp113 ;
2466 unsigned long __cil_tmp114 ;
2467 unsigned long __cil_tmp115 ;
2468 void const *__cil_tmp116 ;
2469 int __cil_tmp117 ;
2470 int *__cil_tmp118 ;
2471 int *__cil_tmp119 ;
2472
2473 {
2474#line 277
2475 argp = (void *)arg;
2476#line 278
2477 p = (int *)argp;
2478#line 279
2479 __cil_tmp18 = & ident;
2480#line 279
2481 *((__u32 *)__cil_tmp18) = 33152U;
2482#line 279
2483 __cil_tmp19 = (unsigned long )(& ident) + 4;
2484#line 279
2485 *((__u32 *)__cil_tmp19) = 1U;
2486#line 279
2487 __cil_tmp20 = 0 * 1UL;
2488#line 279
2489 __cil_tmp21 = 8 + __cil_tmp20;
2490#line 279
2491 __cil_tmp22 = (unsigned long )(& ident) + __cil_tmp21;
2492#line 279
2493 *((__u8 *)__cil_tmp22) = (__u8 )'I';
2494#line 279
2495 __cil_tmp23 = 1 * 1UL;
2496#line 279
2497 __cil_tmp24 = 8 + __cil_tmp23;
2498#line 279
2499 __cil_tmp25 = (unsigned long )(& ident) + __cil_tmp24;
2500#line 279
2501 *((__u8 *)__cil_tmp25) = (__u8 )'T';
2502#line 279
2503 __cil_tmp26 = 2 * 1UL;
2504#line 279
2505 __cil_tmp27 = 8 + __cil_tmp26;
2506#line 279
2507 __cil_tmp28 = (unsigned long )(& ident) + __cil_tmp27;
2508#line 279
2509 *((__u8 *)__cil_tmp28) = (__u8 )'8';
2510#line 279
2511 __cil_tmp29 = 3 * 1UL;
2512#line 279
2513 __cil_tmp30 = 8 + __cil_tmp29;
2514#line 279
2515 __cil_tmp31 = (unsigned long )(& ident) + __cil_tmp30;
2516#line 279
2517 *((__u8 *)__cil_tmp31) = (__u8 )'7';
2518#line 279
2519 __cil_tmp32 = 4 * 1UL;
2520#line 279
2521 __cil_tmp33 = 8 + __cil_tmp32;
2522#line 279
2523 __cil_tmp34 = (unsigned long )(& ident) + __cil_tmp33;
2524#line 279
2525 *((__u8 *)__cil_tmp34) = (__u8 )'1';
2526#line 279
2527 __cil_tmp35 = 5 * 1UL;
2528#line 279
2529 __cil_tmp36 = 8 + __cil_tmp35;
2530#line 279
2531 __cil_tmp37 = (unsigned long )(& ident) + __cil_tmp36;
2532#line 279
2533 *((__u8 *)__cil_tmp37) = (__u8 )'2';
2534#line 279
2535 __cil_tmp38 = 6 * 1UL;
2536#line 279
2537 __cil_tmp39 = 8 + __cil_tmp38;
2538#line 279
2539 __cil_tmp40 = (unsigned long )(& ident) + __cil_tmp39;
2540#line 279
2541 *((__u8 *)__cil_tmp40) = (__u8 )'F';
2542#line 279
2543 __cil_tmp41 = 7 * 1UL;
2544#line 279
2545 __cil_tmp42 = 8 + __cil_tmp41;
2546#line 279
2547 __cil_tmp43 = (unsigned long )(& ident) + __cil_tmp42;
2548#line 279
2549 *((__u8 *)__cil_tmp43) = (__u8 )' ';
2550#line 279
2551 __cil_tmp44 = 8 * 1UL;
2552#line 279
2553 __cil_tmp45 = 8 + __cil_tmp44;
2554#line 279
2555 __cil_tmp46 = (unsigned long )(& ident) + __cil_tmp45;
2556#line 279
2557 *((__u8 *)__cil_tmp46) = (__u8 )'W';
2558#line 279
2559 __cil_tmp47 = 9 * 1UL;
2560#line 279
2561 __cil_tmp48 = 8 + __cil_tmp47;
2562#line 279
2563 __cil_tmp49 = (unsigned long )(& ident) + __cil_tmp48;
2564#line 279
2565 *((__u8 *)__cil_tmp49) = (__u8 )'a';
2566#line 279
2567 __cil_tmp50 = 10 * 1UL;
2568#line 279
2569 __cil_tmp51 = 8 + __cil_tmp50;
2570#line 279
2571 __cil_tmp52 = (unsigned long )(& ident) + __cil_tmp51;
2572#line 279
2573 *((__u8 *)__cil_tmp52) = (__u8 )'t';
2574#line 279
2575 __cil_tmp53 = 11 * 1UL;
2576#line 279
2577 __cil_tmp54 = 8 + __cil_tmp53;
2578#line 279
2579 __cil_tmp55 = (unsigned long )(& ident) + __cil_tmp54;
2580#line 279
2581 *((__u8 *)__cil_tmp55) = (__u8 )'c';
2582#line 279
2583 __cil_tmp56 = 12 * 1UL;
2584#line 279
2585 __cil_tmp57 = 8 + __cil_tmp56;
2586#line 279
2587 __cil_tmp58 = (unsigned long )(& ident) + __cil_tmp57;
2588#line 279
2589 *((__u8 *)__cil_tmp58) = (__u8 )'h';
2590#line 279
2591 __cil_tmp59 = 13 * 1UL;
2592#line 279
2593 __cil_tmp60 = 8 + __cil_tmp59;
2594#line 279
2595 __cil_tmp61 = (unsigned long )(& ident) + __cil_tmp60;
2596#line 279
2597 *((__u8 *)__cil_tmp61) = (__u8 )'d';
2598#line 279
2599 __cil_tmp62 = 14 * 1UL;
2600#line 279
2601 __cil_tmp63 = 8 + __cil_tmp62;
2602#line 279
2603 __cil_tmp64 = (unsigned long )(& ident) + __cil_tmp63;
2604#line 279
2605 *((__u8 *)__cil_tmp64) = (__u8 )'o';
2606#line 279
2607 __cil_tmp65 = 15 * 1UL;
2608#line 279
2609 __cil_tmp66 = 8 + __cil_tmp65;
2610#line 279
2611 __cil_tmp67 = (unsigned long )(& ident) + __cil_tmp66;
2612#line 279
2613 *((__u8 *)__cil_tmp67) = (__u8 )'g';
2614#line 279
2615 __cil_tmp68 = 16 * 1UL;
2616#line 279
2617 __cil_tmp69 = 8 + __cil_tmp68;
2618#line 279
2619 __cil_tmp70 = (unsigned long )(& ident) + __cil_tmp69;
2620#line 279
2621 *((__u8 *)__cil_tmp70) = (__u8 )'\000';
2622#line 279
2623 __cil_tmp71 = 17 * 1UL;
2624#line 279
2625 __cil_tmp72 = 8 + __cil_tmp71;
2626#line 279
2627 __cil_tmp73 = (unsigned long )(& ident) + __cil_tmp72;
2628#line 279
2629 *((__u8 *)__cil_tmp73) = (unsigned char)0;
2630#line 279
2631 __cil_tmp74 = 18 * 1UL;
2632#line 279
2633 __cil_tmp75 = 8 + __cil_tmp74;
2634#line 279
2635 __cil_tmp76 = (unsigned long )(& ident) + __cil_tmp75;
2636#line 279
2637 *((__u8 *)__cil_tmp76) = (unsigned char)0;
2638#line 279
2639 __cil_tmp77 = 19 * 1UL;
2640#line 279
2641 __cil_tmp78 = 8 + __cil_tmp77;
2642#line 279
2643 __cil_tmp79 = (unsigned long )(& ident) + __cil_tmp78;
2644#line 279
2645 *((__u8 *)__cil_tmp79) = (unsigned char)0;
2646#line 279
2647 __cil_tmp80 = 20 * 1UL;
2648#line 279
2649 __cil_tmp81 = 8 + __cil_tmp80;
2650#line 279
2651 __cil_tmp82 = (unsigned long )(& ident) + __cil_tmp81;
2652#line 279
2653 *((__u8 *)__cil_tmp82) = (unsigned char)0;
2654#line 279
2655 __cil_tmp83 = 21 * 1UL;
2656#line 279
2657 __cil_tmp84 = 8 + __cil_tmp83;
2658#line 279
2659 __cil_tmp85 = (unsigned long )(& ident) + __cil_tmp84;
2660#line 279
2661 *((__u8 *)__cil_tmp85) = (unsigned char)0;
2662#line 279
2663 __cil_tmp86 = 22 * 1UL;
2664#line 279
2665 __cil_tmp87 = 8 + __cil_tmp86;
2666#line 279
2667 __cil_tmp88 = (unsigned long )(& ident) + __cil_tmp87;
2668#line 279
2669 *((__u8 *)__cil_tmp88) = (unsigned char)0;
2670#line 279
2671 __cil_tmp89 = 23 * 1UL;
2672#line 279
2673 __cil_tmp90 = 8 + __cil_tmp89;
2674#line 279
2675 __cil_tmp91 = (unsigned long )(& ident) + __cil_tmp90;
2676#line 279
2677 *((__u8 *)__cil_tmp91) = (unsigned char)0;
2678#line 279
2679 __cil_tmp92 = 24 * 1UL;
2680#line 279
2681 __cil_tmp93 = 8 + __cil_tmp92;
2682#line 279
2683 __cil_tmp94 = (unsigned long )(& ident) + __cil_tmp93;
2684#line 279
2685 *((__u8 *)__cil_tmp94) = (unsigned char)0;
2686#line 279
2687 __cil_tmp95 = 25 * 1UL;
2688#line 279
2689 __cil_tmp96 = 8 + __cil_tmp95;
2690#line 279
2691 __cil_tmp97 = (unsigned long )(& ident) + __cil_tmp96;
2692#line 279
2693 *((__u8 *)__cil_tmp97) = (unsigned char)0;
2694#line 279
2695 __cil_tmp98 = 26 * 1UL;
2696#line 279
2697 __cil_tmp99 = 8 + __cil_tmp98;
2698#line 279
2699 __cil_tmp100 = (unsigned long )(& ident) + __cil_tmp99;
2700#line 279
2701 *((__u8 *)__cil_tmp100) = (unsigned char)0;
2702#line 279
2703 __cil_tmp101 = 27 * 1UL;
2704#line 279
2705 __cil_tmp102 = 8 + __cil_tmp101;
2706#line 279
2707 __cil_tmp103 = (unsigned long )(& ident) + __cil_tmp102;
2708#line 279
2709 *((__u8 *)__cil_tmp103) = (unsigned char)0;
2710#line 279
2711 __cil_tmp104 = 28 * 1UL;
2712#line 279
2713 __cil_tmp105 = 8 + __cil_tmp104;
2714#line 279
2715 __cil_tmp106 = (unsigned long )(& ident) + __cil_tmp105;
2716#line 279
2717 *((__u8 *)__cil_tmp106) = (unsigned char)0;
2718#line 279
2719 __cil_tmp107 = 29 * 1UL;
2720#line 279
2721 __cil_tmp108 = 8 + __cil_tmp107;
2722#line 279
2723 __cil_tmp109 = (unsigned long )(& ident) + __cil_tmp108;
2724#line 279
2725 *((__u8 *)__cil_tmp109) = (unsigned char)0;
2726#line 279
2727 __cil_tmp110 = 30 * 1UL;
2728#line 279
2729 __cil_tmp111 = 8 + __cil_tmp110;
2730#line 279
2731 __cil_tmp112 = (unsigned long )(& ident) + __cil_tmp111;
2732#line 279
2733 *((__u8 *)__cil_tmp112) = (unsigned char)0;
2734#line 279
2735 __cil_tmp113 = 31 * 1UL;
2736#line 279
2737 __cil_tmp114 = 8 + __cil_tmp113;
2738#line 279
2739 __cil_tmp115 = (unsigned long )(& ident) + __cil_tmp114;
2740#line 279
2741 *((__u8 *)__cil_tmp115) = (unsigned char)0;
2742#line 289
2743 if ((int )cmd == -2144839936) {
2744#line 289
2745 goto case_neg_2144839936;
2746 } else
2747#line 293
2748 if ((int )cmd == -2147199231) {
2749#line 293
2750 goto case_neg_2147199231;
2751 } else
2752#line 304
2753 if ((int )cmd == -2147199230) {
2754#line 304
2755 goto case_neg_2147199230;
2756 } else
2757#line 306
2758 if ((int )cmd == -2147199227) {
2759#line 306
2760 goto case_neg_2147199227;
2761 } else
2762#line 309
2763 if ((int )cmd == -1073457402) {
2764#line 309
2765 goto case_neg_1073457402;
2766 } else
2767#line 327
2768 if ((int )cmd == -2147199225) {
2769#line 327
2770 goto case_neg_2147199225;
2771 } else {
2772 {
2773#line 331
2774 goto switch_default___3;
2775#line 288
2776 if (0) {
2777 case_neg_2144839936:
2778 {
2779#line 290
2780 __cil_tmp116 = (void const *)(& ident);
2781#line 290
2782 tmp = copy_to_user(argp, __cil_tmp116, 40U);
2783 }
2784#line 290
2785 if (tmp != 0) {
2786#line 291
2787 return (-14L);
2788 } else {
2789
2790 }
2791#line 292
2792 return (0L);
2793 case_neg_2147199231:
2794 {
2795#line 294
2796 ret = superio_enter();
2797 }
2798#line 295
2799 if (ret != 0) {
2800#line 296
2801 return ((long )ret);
2802 } else {
2803
2804 }
2805 {
2806#line 297
2807 superio_select(7);
2808#line 299
2809 value = it8712f_wdt_get_status();
2810#line 301
2811 superio_exit();
2812#line 303
2813 might_fault();
2814#line 303
2815 __pu_val = value;
2816 }
2817#line 303
2818 if (4 == 1) {
2819#line 303
2820 goto case_1;
2821 } else
2822#line 303
2823 if (4 == 2) {
2824#line 303
2825 goto case_2;
2826 } else
2827#line 303
2828 if (4 == 4) {
2829#line 303
2830 goto case_4;
2831 } else
2832#line 303
2833 if (4 == 8) {
2834#line 303
2835 goto case_8;
2836 } else {
2837 {
2838#line 303
2839 goto switch_default;
2840#line 303
2841 if (0) {
2842 case_1:
2843#line 303
2844 __asm__ volatile ("call __put_user_1": "=a" (__ret_pu): "0" (__pu_val),
2845 "c" (p): "ebx");
2846#line 303
2847 goto ldv_18123;
2848 case_2:
2849#line 303
2850 __asm__ volatile ("call __put_user_2": "=a" (__ret_pu): "0" (__pu_val),
2851 "c" (p): "ebx");
2852#line 303
2853 goto ldv_18123;
2854 case_4:
2855#line 303
2856 __asm__ volatile ("call __put_user_4": "=a" (__ret_pu): "0" (__pu_val),
2857 "c" (p): "ebx");
2858#line 303
2859 goto ldv_18123;
2860 case_8:
2861#line 303
2862 __asm__ volatile ("call __put_user_8": "=a" (__ret_pu): "0" (__pu_val),
2863 "c" (p): "ebx");
2864#line 303
2865 goto ldv_18123;
2866 switch_default:
2867#line 303
2868 __asm__ volatile ("call __put_user_X": "=a" (__ret_pu): "0" (__pu_val),
2869 "c" (p): "ebx");
2870#line 303
2871 goto ldv_18123;
2872 } else {
2873 switch_break___0: ;
2874 }
2875 }
2876 }
2877 ldv_18123: ;
2878#line 303
2879 return ((long )__ret_pu);
2880 case_neg_2147199230:
2881 {
2882#line 305
2883 might_fault();
2884#line 305
2885 __pu_val___0 = 0;
2886 }
2887#line 305
2888 if (4 == 1) {
2889#line 305
2890 goto case_1___0;
2891 } else
2892#line 305
2893 if (4 == 2) {
2894#line 305
2895 goto case_2___0;
2896 } else
2897#line 305
2898 if (4 == 4) {
2899#line 305
2900 goto case_4___0;
2901 } else
2902#line 305
2903 if (4 == 8) {
2904#line 305
2905 goto case_8___0;
2906 } else {
2907 {
2908#line 305
2909 goto switch_default___0;
2910#line 305
2911 if (0) {
2912 case_1___0:
2913#line 305
2914 __asm__ volatile ("call __put_user_1": "=a" (__ret_pu___0): "0" (__pu_val___0),
2915 "c" (p): "ebx");
2916#line 305
2917 goto ldv_18133;
2918 case_2___0:
2919#line 305
2920 __asm__ volatile ("call __put_user_2": "=a" (__ret_pu___0): "0" (__pu_val___0),
2921 "c" (p): "ebx");
2922#line 305
2923 goto ldv_18133;
2924 case_4___0:
2925#line 305
2926 __asm__ volatile ("call __put_user_4": "=a" (__ret_pu___0): "0" (__pu_val___0),
2927 "c" (p): "ebx");
2928#line 305
2929 goto ldv_18133;
2930 case_8___0:
2931#line 305
2932 __asm__ volatile ("call __put_user_8": "=a" (__ret_pu___0): "0" (__pu_val___0),
2933 "c" (p): "ebx");
2934#line 305
2935 goto ldv_18133;
2936 switch_default___0:
2937#line 305
2938 __asm__ volatile ("call __put_user_X": "=a" (__ret_pu___0): "0" (__pu_val___0),
2939 "c" (p): "ebx");
2940#line 305
2941 goto ldv_18133;
2942 } else {
2943 switch_break___1: ;
2944 }
2945 }
2946 }
2947 ldv_18133: ;
2948#line 305
2949 return ((long )__ret_pu___0);
2950 case_neg_2147199227:
2951 {
2952#line 307
2953 it8712f_wdt_ping();
2954 }
2955#line 308
2956 return (0L);
2957 case_neg_1073457402:
2958 {
2959#line 310
2960 might_fault();
2961 }
2962#line 310
2963 if (4 == 1) {
2964#line 310
2965 goto case_1___1;
2966 } else
2967#line 310
2968 if (4 == 2) {
2969#line 310
2970 goto case_2___1;
2971 } else
2972#line 310
2973 if (4 == 4) {
2974#line 310
2975 goto case_4___1;
2976 } else
2977#line 310
2978 if (4 == 8) {
2979#line 310
2980 goto case_8___1;
2981 } else {
2982 {
2983#line 310
2984 goto switch_default___1;
2985#line 310
2986 if (0) {
2987 case_1___1:
2988#line 310
2989 __asm__ volatile ("call __get_user_1": "=a" (__ret_gu), "=d" (__val_gu): "0" (p));
2990#line 310
2991 goto ldv_18144;
2992 case_2___1:
2993#line 310
2994 __asm__ volatile ("call __get_user_2": "=a" (__ret_gu), "=d" (__val_gu): "0" (p));
2995#line 310
2996 goto ldv_18144;
2997 case_4___1:
2998#line 310
2999 __asm__ volatile ("call __get_user_4": "=a" (__ret_gu), "=d" (__val_gu): "0" (p));
3000#line 310
3001 goto ldv_18144;
3002 case_8___1:
3003#line 310
3004 __asm__ volatile ("call __get_user_8": "=a" (__ret_gu), "=d" (__val_gu): "0" (p));
3005#line 310
3006 goto ldv_18144;
3007 switch_default___1:
3008#line 310
3009 __asm__ volatile ("call __get_user_X": "=a" (__ret_gu), "=d" (__val_gu): "0" (p));
3010#line 310
3011 goto ldv_18144;
3012 } else {
3013 switch_break___2: ;
3014 }
3015 }
3016 }
3017 ldv_18144:
3018#line 310
3019 value = (int )__val_gu;
3020#line 310
3021 if (__ret_gu != 0) {
3022#line 311
3023 return (-14L);
3024 } else {
3025
3026 }
3027#line 312
3028 if (value <= 0) {
3029#line 313
3030 return (-22L);
3031 } else {
3032
3033 }
3034 {
3035#line 314
3036 __cil_tmp117 = max_units * 60;
3037#line 314
3038 if (__cil_tmp117 < value) {
3039#line 315
3040 return (-22L);
3041 } else {
3042
3043 }
3044 }
3045 {
3046#line 316
3047 __cil_tmp118 = & margin;
3048#line 316
3049 *__cil_tmp118 = value;
3050#line 317
3051 ret = superio_enter();
3052 }
3053#line 318
3054 if (ret != 0) {
3055#line 319
3056 return ((long )ret);
3057 } else {
3058
3059 }
3060 {
3061#line 320
3062 superio_select(7);
3063#line 322
3064 it8712f_wdt_update_margin();
3065#line 324
3066 superio_exit();
3067#line 325
3068 it8712f_wdt_ping();
3069 }
3070 case_neg_2147199225:
3071 {
3072#line 328
3073 might_fault();
3074#line 328
3075 __cil_tmp119 = & margin;
3076#line 328
3077 __pu_val___1 = *__cil_tmp119;
3078 }
3079#line 328
3080 if (4 == 1) {
3081#line 328
3082 goto case_1___2;
3083 } else
3084#line 328
3085 if (4 == 2) {
3086#line 328
3087 goto case_2___2;
3088 } else
3089#line 328
3090 if (4 == 4) {
3091#line 328
3092 goto case_4___2;
3093 } else
3094#line 328
3095 if (4 == 8) {
3096#line 328
3097 goto case_8___2;
3098 } else {
3099 {
3100#line 328
3101 goto switch_default___2;
3102#line 328
3103 if (0) {
3104 case_1___2:
3105#line 328
3106 __asm__ volatile ("call __put_user_1": "=a" (__ret_pu___1): "0" (__pu_val___1),
3107 "c" (p): "ebx");
3108#line 328
3109 goto ldv_18154;
3110 case_2___2:
3111#line 328
3112 __asm__ volatile ("call __put_user_2": "=a" (__ret_pu___1): "0" (__pu_val___1),
3113 "c" (p): "ebx");
3114#line 328
3115 goto ldv_18154;
3116 case_4___2:
3117#line 328
3118 __asm__ volatile ("call __put_user_4": "=a" (__ret_pu___1): "0" (__pu_val___1),
3119 "c" (p): "ebx");
3120#line 328
3121 goto ldv_18154;
3122 case_8___2:
3123#line 328
3124 __asm__ volatile ("call __put_user_8": "=a" (__ret_pu___1): "0" (__pu_val___1),
3125 "c" (p): "ebx");
3126#line 328
3127 goto ldv_18154;
3128 switch_default___2:
3129#line 328
3130 __asm__ volatile ("call __put_user_X": "=a" (__ret_pu___1): "0" (__pu_val___1),
3131 "c" (p): "ebx");
3132#line 328
3133 goto ldv_18154;
3134 } else {
3135 switch_break___3: ;
3136 }
3137 }
3138 }
3139 ldv_18154: ;
3140#line 328
3141 if (__ret_pu___1 != 0) {
3142#line 329
3143 return (-14L);
3144 } else {
3145
3146 }
3147#line 330
3148 return (0L);
3149 switch_default___3: ;
3150#line 332
3151 return (-25L);
3152 } else {
3153 switch_break: ;
3154 }
3155 }
3156 }
3157}
3158}
3159#line 336 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
3160static int it8712f_wdt_open(struct inode *inode , struct file *file )
3161{ int ret ;
3162 int tmp ;
3163 int tmp___0 ;
3164 unsigned long volatile *__cil_tmp6 ;
3165
3166 {
3167 {
3168#line 340
3169 __cil_tmp6 = (unsigned long volatile *)(& wdt_open);
3170#line 340
3171 tmp = test_and_set_bit(0, __cil_tmp6);
3172 }
3173#line 340
3174 if (tmp != 0) {
3175#line 341
3176 return (-16);
3177 } else {
3178
3179 }
3180 {
3181#line 343
3182 ret = it8712f_wdt_enable();
3183 }
3184#line 344
3185 if (ret != 0) {
3186#line 345
3187 return (ret);
3188 } else {
3189
3190 }
3191 {
3192#line 346
3193 tmp___0 = nonseekable_open(inode, file);
3194 }
3195#line 346
3196 return (tmp___0);
3197}
3198}
3199#line 349 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
3200static int it8712f_wdt_release(struct inode *inode , struct file *file )
3201{ int tmp ;
3202 bool *__cil_tmp4 ;
3203 bool __cil_tmp5 ;
3204 unsigned long volatile *__cil_tmp6 ;
3205
3206 {
3207#line 351
3208 if (expect_close != 42U) {
3209 {
3210#line 352
3211 printk("<4>it8712f_wdt: watchdog device closed unexpectedly, will not disable the watchdog timer\n");
3212 }
3213 } else {
3214 {
3215#line 353
3216 __cil_tmp4 = & nowayout;
3217#line 353
3218 __cil_tmp5 = *__cil_tmp4;
3219#line 353
3220 if (! __cil_tmp5) {
3221 {
3222#line 354
3223 tmp = it8712f_wdt_disable();
3224 }
3225#line 354
3226 if (tmp != 0) {
3227 {
3228#line 355
3229 printk("<4>it8712f_wdt: Watchdog disable failed\n");
3230 }
3231 } else {
3232
3233 }
3234 } else {
3235
3236 }
3237 }
3238 }
3239 {
3240#line 357
3241 expect_close = 0U;
3242#line 358
3243 __cil_tmp6 = (unsigned long volatile *)(& wdt_open);
3244#line 358
3245 clear_bit(0, __cil_tmp6);
3246 }
3247#line 360
3248 return (0);
3249}
3250}
3251#line 363 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
3252static struct file_operations const it8712f_wdt_fops =
3253#line 363
3254 {& __this_module, & no_llseek, (ssize_t (*)(struct file * , char * , size_t ,
3255 loff_t * ))0, & it8712f_wdt_write,
3256 (ssize_t (*)(struct kiocb * , struct iovec const * , unsigned long , loff_t ))0,
3257 (ssize_t (*)(struct kiocb * , struct iovec const * , unsigned long , loff_t ))0,
3258 (int (*)(struct file * , void * , int (*)(void * , char const * , int , loff_t ,
3259 u64 , unsigned int ) ))0, (unsigned int (*)(struct file * ,
3260 struct poll_table_struct * ))0,
3261 & it8712f_wdt_ioctl, (long (*)(struct file * , unsigned int , unsigned long ))0,
3262 (int (*)(struct file * , struct vm_area_struct * ))0, & it8712f_wdt_open, (int (*)(struct file * ,
3263 fl_owner_t ))0,
3264 & it8712f_wdt_release, (int (*)(struct file * , loff_t , loff_t , int ))0,
3265 (int (*)(struct kiocb * , int ))0, (int (*)(int , struct file * , int ))0,
3266 (int (*)(struct file * , int , struct file_lock * ))0, (ssize_t (*)(struct file * ,
3267 struct page * ,
3268 int , size_t ,
3269 loff_t * ,
3270 int ))0,
3271 (unsigned long (*)(struct file * , unsigned long , unsigned long , unsigned long ,
3272 unsigned long ))0, (int (*)(int ))0, (int (*)(struct file * ,
3273 int , struct file_lock * ))0,
3274 (ssize_t (*)(struct pipe_inode_info * , struct file * , loff_t * , size_t , unsigned int ))0,
3275 (ssize_t (*)(struct file * , loff_t * , struct pipe_inode_info * , size_t , unsigned int ))0,
3276 (int (*)(struct file * , long , struct file_lock ** ))0, (long (*)(struct file * ,
3277 int , loff_t ,
3278 loff_t ))0};
3279#line 372 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
3280static struct miscdevice it8712f_wdt_miscdev =
3281#line 372
3282 {130, "watchdog", & it8712f_wdt_fops, {(struct list_head *)0, (struct list_head *)0},
3283 (struct device *)0, (struct device *)0, (char const *)0, (unsigned short)0};
3284#line 378 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
3285static int it8712f_wdt_find(unsigned short *address___0 )
3286{ int err ;
3287 int chip_type ;
3288 int ret ;
3289 int tmp ;
3290 int tmp___0 ;
3291 int tmp___1 ;
3292 int tmp___2 ;
3293 int __cil_tmp9 ;
3294 unsigned short __cil_tmp10 ;
3295 unsigned int __cil_tmp11 ;
3296 unsigned char __cil_tmp12 ;
3297 unsigned int __cil_tmp13 ;
3298 unsigned int __cil_tmp14 ;
3299 unsigned int __cil_tmp15 ;
3300 int *__cil_tmp16 ;
3301 int __cil_tmp17 ;
3302 int __cil_tmp18 ;
3303 int *__cil_tmp19 ;
3304 int __cil_tmp20 ;
3305 unsigned short __cil_tmp21 ;
3306 int __cil_tmp22 ;
3307
3308 {
3309 {
3310#line 380
3311 err = -19;
3312#line 382
3313 tmp = superio_enter();
3314#line 382
3315 ret = tmp;
3316 }
3317#line 383
3318 if (ret != 0) {
3319#line 384
3320 return (ret);
3321 } else {
3322
3323 }
3324 {
3325#line 386
3326 chip_type = superio_inw(32);
3327 }
3328#line 387
3329 if (chip_type != 34578) {
3330#line 388
3331 goto exit;
3332 } else {
3333
3334 }
3335 {
3336#line 390
3337 superio_select(9);
3338#line 391
3339 superio_outb(1, 48);
3340#line 392
3341 tmp___0 = superio_inb(48);
3342 }
3343 {
3344#line 392
3345 __cil_tmp9 = tmp___0 & 1;
3346#line 392
3347 if (__cil_tmp9 == 0) {
3348 {
3349#line 393
3350 printk("<3>it8712f_wdt: Device not activated, skipping\n");
3351 }
3352#line 394
3353 goto exit;
3354 } else {
3355
3356 }
3357 }
3358 {
3359#line 397
3360 tmp___1 = superio_inw(96);
3361#line 397
3362 *address___0 = (unsigned short )tmp___1;
3363 }
3364 {
3365#line 398
3366 __cil_tmp10 = *address___0;
3367#line 398
3368 __cil_tmp11 = (unsigned int )__cil_tmp10;
3369#line 398
3370 if (__cil_tmp11 == 0U) {
3371 {
3372#line 399
3373 printk("<3>it8712f_wdt: Base address not set, skipping\n");
3374 }
3375#line 400
3376 goto exit;
3377 } else {
3378
3379 }
3380 }
3381 {
3382#line 403
3383 err = 0;
3384#line 404
3385 tmp___2 = superio_inb(34);
3386#line 404
3387 __cil_tmp12 = (unsigned char )tmp___2;
3388#line 404
3389 __cil_tmp13 = (unsigned int )__cil_tmp12;
3390#line 404
3391 __cil_tmp14 = __cil_tmp13 & 15U;
3392#line 404
3393 revision = (unsigned char )__cil_tmp14;
3394 }
3395 {
3396#line 407
3397 __cil_tmp15 = (unsigned int )revision;
3398#line 407
3399 if (__cil_tmp15 > 7U) {
3400#line 408
3401 max_units = 65535;
3402 } else {
3403
3404 }
3405 }
3406 {
3407#line 410
3408 __cil_tmp16 = & margin;
3409#line 410
3410 __cil_tmp17 = *__cil_tmp16;
3411#line 410
3412 __cil_tmp18 = max_units * 60;
3413#line 410
3414 if (__cil_tmp18 < __cil_tmp17) {
3415#line 411
3416 __cil_tmp19 = & margin;
3417#line 411
3418 *__cil_tmp19 = max_units * 60;
3419 } else {
3420
3421 }
3422 }
3423 {
3424#line 413
3425 __cil_tmp20 = (int )revision;
3426#line 413
3427 __cil_tmp21 = *address___0;
3428#line 413
3429 __cil_tmp22 = (int )__cil_tmp21;
3430#line 413
3431 printk("<6>it8712f_wdt: Found IT%04xF chip revision %d - using DogFood address 0x%x\n",
3432 chip_type, __cil_tmp20, __cil_tmp22);
3433 }
3434 exit:
3435 {
3436#line 417
3437 superio_exit();
3438 }
3439#line 418
3440 return (err);
3441}
3442}
3443#line 421 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
3444static int it8712f_wdt_init(void)
3445{ int err ;
3446 int tmp ;
3447 struct resource *tmp___0 ;
3448 unsigned short *__cil_tmp4 ;
3449 unsigned short __cil_tmp5 ;
3450 resource_size_t __cil_tmp6 ;
3451 struct resource *__cil_tmp7 ;
3452 unsigned long __cil_tmp8 ;
3453 unsigned long __cil_tmp9 ;
3454 unsigned short *__cil_tmp10 ;
3455 unsigned short __cil_tmp11 ;
3456 resource_size_t __cil_tmp12 ;
3457
3458 {
3459 {
3460#line 423
3461 err = 0;
3462#line 425
3463 tmp = it8712f_wdt_find(& address);
3464 }
3465#line 425
3466 if (tmp != 0) {
3467#line 426
3468 return (-19);
3469 } else {
3470
3471 }
3472 {
3473#line 428
3474 __cil_tmp4 = & address;
3475#line 428
3476 __cil_tmp5 = *__cil_tmp4;
3477#line 428
3478 __cil_tmp6 = (resource_size_t )__cil_tmp5;
3479#line 428
3480 tmp___0 = __request_region(& ioport_resource, __cil_tmp6, 1ULL, "IT8712F Watchdog",
3481 0);
3482 }
3483 {
3484#line 428
3485 __cil_tmp7 = (struct resource *)0;
3486#line 428
3487 __cil_tmp8 = (unsigned long )__cil_tmp7;
3488#line 428
3489 __cil_tmp9 = (unsigned long )tmp___0;
3490#line 428
3491 if (__cil_tmp9 == __cil_tmp8) {
3492 {
3493#line 429
3494 printk("<4>it8712f_wdt: watchdog I/O region busy\n");
3495 }
3496#line 430
3497 return (-16);
3498 } else {
3499
3500 }
3501 }
3502 {
3503#line 433
3504 err = it8712f_wdt_disable();
3505 }
3506#line 434
3507 if (err != 0) {
3508 {
3509#line 435
3510 printk("<3>it8712f_wdt: unable to disable watchdog timer\n");
3511 }
3512#line 436
3513 goto out;
3514 } else {
3515
3516 }
3517 {
3518#line 439
3519 err = register_reboot_notifier(& it8712f_wdt_notifier);
3520 }
3521#line 440
3522 if (err != 0) {
3523 {
3524#line 441
3525 printk("<3>it8712f_wdt: unable to register reboot notifier\n");
3526 }
3527#line 442
3528 goto out;
3529 } else {
3530
3531 }
3532 {
3533#line 445
3534 err = misc_register(& it8712f_wdt_miscdev);
3535 }
3536#line 446
3537 if (err != 0) {
3538 {
3539#line 447
3540 printk("<3>it8712f_wdt: cannot register miscdev on minor=%d (err=%d)\n", 130,
3541 err);
3542 }
3543#line 449
3544 goto reboot_out;
3545 } else {
3546
3547 }
3548#line 452
3549 return (0);
3550 reboot_out:
3551 {
3552#line 456
3553 unregister_reboot_notifier(& it8712f_wdt_notifier);
3554 }
3555 out:
3556 {
3557#line 458
3558 __cil_tmp10 = & address;
3559#line 458
3560 __cil_tmp11 = *__cil_tmp10;
3561#line 458
3562 __cil_tmp12 = (resource_size_t )__cil_tmp11;
3563#line 458
3564 __release_region(& ioport_resource, __cil_tmp12, 1ULL);
3565 }
3566#line 459
3567 return (err);
3568}
3569}
3570#line 462 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
3571static void it8712f_wdt_exit(void)
3572{ unsigned short *__cil_tmp1 ;
3573 unsigned short __cil_tmp2 ;
3574 resource_size_t __cil_tmp3 ;
3575
3576 {
3577 {
3578#line 464
3579 misc_deregister(& it8712f_wdt_miscdev);
3580#line 465
3581 unregister_reboot_notifier(& it8712f_wdt_notifier);
3582#line 466
3583 __cil_tmp1 = & address;
3584#line 466
3585 __cil_tmp2 = *__cil_tmp1;
3586#line 466
3587 __cil_tmp3 = (resource_size_t )__cil_tmp2;
3588#line 466
3589 __release_region(& ioport_resource, __cil_tmp3, 1ULL);
3590 }
3591#line 467
3592 return;
3593}
3594}
3595#line 488
3596extern void ldv_check_final_state(void) ;
3597#line 491
3598extern void ldv_check_return_value(int ) ;
3599#line 494
3600extern void ldv_initialize(void) ;
3601#line 497
3602extern int __VERIFIER_nondet_int(void) ;
3603#line 500 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
3604int LDV_IN_INTERRUPT ;
3605#line 503 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
3606void main(void)
3607{ struct notifier_block *var_group1 ;
3608 unsigned long var_it8712f_wdt_notify_11_p1 ;
3609 void *var_it8712f_wdt_notify_11_p2 ;
3610 struct file *var_group2 ;
3611 char const *var_it8712f_wdt_write_12_p1 ;
3612 size_t var_it8712f_wdt_write_12_p2 ;
3613 loff_t *var_it8712f_wdt_write_12_p3 ;
3614 ssize_t res_it8712f_wdt_write_12 ;
3615 unsigned int var_it8712f_wdt_ioctl_13_p1 ;
3616 unsigned long var_it8712f_wdt_ioctl_13_p2 ;
3617 struct inode *var_group3 ;
3618 int res_it8712f_wdt_open_14 ;
3619 int ldv_s_it8712f_wdt_fops_file_operations ;
3620 int tmp ;
3621 int tmp___0 ;
3622 int tmp___1 ;
3623 int __cil_tmp17 ;
3624
3625 {
3626 {
3627#line 716
3628 ldv_s_it8712f_wdt_fops_file_operations = 0;
3629#line 673
3630 LDV_IN_INTERRUPT = 1;
3631#line 682
3632 ldv_initialize();
3633#line 712
3634 tmp = it8712f_wdt_init();
3635 }
3636#line 712
3637 if (tmp != 0) {
3638#line 713
3639 goto ldv_final;
3640 } else {
3641
3642 }
3643#line 720
3644 goto ldv_18233;
3645 ldv_18232:
3646 {
3647#line 724
3648 tmp___0 = __VERIFIER_nondet_int();
3649 }
3650#line 726
3651 if (tmp___0 == 0) {
3652#line 726
3653 goto case_0;
3654 } else
3655#line 766
3656 if (tmp___0 == 1) {
3657#line 766
3658 goto case_1;
3659 } else
3660#line 809
3661 if (tmp___0 == 2) {
3662#line 809
3663 goto case_2;
3664 } else
3665#line 852
3666 if (tmp___0 == 3) {
3667#line 852
3668 goto case_3;
3669 } else
3670#line 892
3671 if (tmp___0 == 4) {
3672#line 892
3673 goto case_4;
3674 } else {
3675 {
3676#line 932
3677 goto switch_default;
3678#line 724
3679 if (0) {
3680 case_0:
3681 {
3682#line 758
3683 it8712f_wdt_notify(var_group1, var_it8712f_wdt_notify_11_p1, var_it8712f_wdt_notify_11_p2);
3684 }
3685#line 765
3686 goto ldv_18225;
3687 case_1: ;
3688#line 769
3689 if (ldv_s_it8712f_wdt_fops_file_operations == 0) {
3690 {
3691#line 798
3692 res_it8712f_wdt_open_14 = it8712f_wdt_open(var_group3, var_group2);
3693#line 799
3694 ldv_check_return_value(res_it8712f_wdt_open_14);
3695 }
3696#line 800
3697 if (res_it8712f_wdt_open_14 != 0) {
3698#line 801
3699 goto ldv_module_exit;
3700 } else {
3701
3702 }
3703#line 802
3704 ldv_s_it8712f_wdt_fops_file_operations = ldv_s_it8712f_wdt_fops_file_operations + 1;
3705 } else {
3706
3707 }
3708#line 808
3709 goto ldv_18225;
3710 case_2: ;
3711#line 812
3712 if (ldv_s_it8712f_wdt_fops_file_operations == 1) {
3713 {
3714#line 841
3715 res_it8712f_wdt_write_12 = it8712f_wdt_write(var_group2, var_it8712f_wdt_write_12_p1,
3716 var_it8712f_wdt_write_12_p2,
3717 var_it8712f_wdt_write_12_p3);
3718#line 842
3719 __cil_tmp17 = (int )res_it8712f_wdt_write_12;
3720#line 842
3721 ldv_check_return_value(__cil_tmp17);
3722 }
3723#line 843
3724 if (res_it8712f_wdt_write_12 < 0L) {
3725#line 844
3726 goto ldv_module_exit;
3727 } else {
3728
3729 }
3730#line 845
3731 ldv_s_it8712f_wdt_fops_file_operations = ldv_s_it8712f_wdt_fops_file_operations + 1;
3732 } else {
3733
3734 }
3735#line 851
3736 goto ldv_18225;
3737 case_3: ;
3738#line 855
3739 if (ldv_s_it8712f_wdt_fops_file_operations == 2) {
3740 {
3741#line 884
3742 it8712f_wdt_release(var_group3, var_group2);
3743#line 885
3744 ldv_s_it8712f_wdt_fops_file_operations = 0;
3745 }
3746 } else {
3747
3748 }
3749#line 891
3750 goto ldv_18225;
3751 case_4:
3752 {
3753#line 924
3754 it8712f_wdt_ioctl(var_group2, var_it8712f_wdt_ioctl_13_p1, var_it8712f_wdt_ioctl_13_p2);
3755 }
3756#line 931
3757 goto ldv_18225;
3758 switch_default: ;
3759#line 932
3760 goto ldv_18225;
3761 } else {
3762 switch_break: ;
3763 }
3764 }
3765 }
3766 ldv_18225: ;
3767 ldv_18233:
3768 {
3769#line 720
3770 tmp___1 = __VERIFIER_nondet_int();
3771 }
3772#line 720
3773 if (tmp___1 != 0) {
3774#line 722
3775 goto ldv_18232;
3776 } else
3777#line 720
3778 if (ldv_s_it8712f_wdt_fops_file_operations != 0) {
3779#line 722
3780 goto ldv_18232;
3781 } else {
3782#line 724
3783 goto ldv_18234;
3784 }
3785 ldv_18234: ;
3786 ldv_module_exit:
3787 {
3788#line 968
3789 it8712f_wdt_exit();
3790 }
3791 ldv_final:
3792 {
3793#line 971
3794 ldv_check_final_state();
3795 }
3796#line 974
3797 return;
3798}
3799}
3800#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3801void ldv_blast_assert(void)
3802{
3803
3804 {
3805 ERROR: ;
3806#line 6
3807 goto ERROR;
3808}
3809}
3810#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3811extern int __VERIFIER_nondet_int(void) ;
3812#line 995 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
3813int ldv_spin = 0;
3814#line 999 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
3815void ldv_check_alloc_flags(gfp_t flags )
3816{
3817
3818 {
3819#line 1002
3820 if (ldv_spin != 0) {
3821#line 1002
3822 if (flags != 32U) {
3823 {
3824#line 1002
3825 ldv_blast_assert();
3826 }
3827 } else {
3828
3829 }
3830 } else {
3831
3832 }
3833#line 1005
3834 return;
3835}
3836}
3837#line 1005
3838extern struct page *ldv_some_page(void) ;
3839#line 1008 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
3840struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags )
3841{ struct page *tmp ;
3842
3843 {
3844#line 1011
3845 if (ldv_spin != 0) {
3846#line 1011
3847 if (flags != 32U) {
3848 {
3849#line 1011
3850 ldv_blast_assert();
3851 }
3852 } else {
3853
3854 }
3855 } else {
3856
3857 }
3858 {
3859#line 1013
3860 tmp = ldv_some_page();
3861 }
3862#line 1013
3863 return (tmp);
3864}
3865}
3866#line 1017 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
3867void ldv_check_alloc_nonatomic(void)
3868{
3869
3870 {
3871#line 1020
3872 if (ldv_spin != 0) {
3873 {
3874#line 1020
3875 ldv_blast_assert();
3876 }
3877 } else {
3878
3879 }
3880#line 1023
3881 return;
3882}
3883}
3884#line 1024 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
3885void ldv_spin_lock(void)
3886{
3887
3888 {
3889#line 1027
3890 ldv_spin = 1;
3891#line 1028
3892 return;
3893}
3894}
3895#line 1031 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
3896void ldv_spin_unlock(void)
3897{
3898
3899 {
3900#line 1034
3901 ldv_spin = 0;
3902#line 1035
3903 return;
3904}
3905}
3906#line 1038 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
3907int ldv_spin_trylock(void)
3908{ int is_lock ;
3909
3910 {
3911 {
3912#line 1043
3913 is_lock = __VERIFIER_nondet_int();
3914 }
3915#line 1045
3916 if (is_lock != 0) {
3917#line 1048
3918 return (0);
3919 } else {
3920#line 1053
3921 ldv_spin = 1;
3922#line 1055
3923 return (1);
3924 }
3925}
3926}
3927#line 1222 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17349/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/it8712f_wdt.c.p"
3928void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 )
3929{
3930
3931 {
3932 {
3933#line 1228
3934 ldv_check_alloc_flags(ldv_func_arg2);
3935#line 1230
3936 kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
3937 }
3938#line 1231
3939 return ((void *)0);
3940}
3941}