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