1
2
3
4#line 20 "include/asm-generic/int-ll64.h"
5typedef unsigned char __u8;
6#line 23 "include/asm-generic/int-ll64.h"
7typedef unsigned short __u16;
8#line 25 "include/asm-generic/int-ll64.h"
9typedef int __s32;
10#line 26 "include/asm-generic/int-ll64.h"
11typedef unsigned int __u32;
12#line 30 "include/asm-generic/int-ll64.h"
13typedef unsigned long long __u64;
14#line 43 "include/asm-generic/int-ll64.h"
15typedef unsigned char u8;
16#line 45 "include/asm-generic/int-ll64.h"
17typedef short s16;
18#line 46 "include/asm-generic/int-ll64.h"
19typedef unsigned short u16;
20#line 49 "include/asm-generic/int-ll64.h"
21typedef unsigned int u32;
22#line 51 "include/asm-generic/int-ll64.h"
23typedef long long s64;
24#line 52 "include/asm-generic/int-ll64.h"
25typedef unsigned long long u64;
26#line 14 "include/asm-generic/posix_types.h"
27typedef long __kernel_long_t;
28#line 15 "include/asm-generic/posix_types.h"
29typedef unsigned long __kernel_ulong_t;
30#line 31 "include/asm-generic/posix_types.h"
31typedef int __kernel_pid_t;
32#line 52 "include/asm-generic/posix_types.h"
33typedef unsigned int __kernel_uid32_t;
34#line 53 "include/asm-generic/posix_types.h"
35typedef unsigned int __kernel_gid32_t;
36#line 75 "include/asm-generic/posix_types.h"
37typedef __kernel_ulong_t __kernel_size_t;
38#line 76 "include/asm-generic/posix_types.h"
39typedef __kernel_long_t __kernel_ssize_t;
40#line 91 "include/asm-generic/posix_types.h"
41typedef long long __kernel_loff_t;
42#line 92 "include/asm-generic/posix_types.h"
43typedef __kernel_long_t __kernel_time_t;
44#line 93 "include/asm-generic/posix_types.h"
45typedef __kernel_long_t __kernel_clock_t;
46#line 94 "include/asm-generic/posix_types.h"
47typedef int __kernel_timer_t;
48#line 95 "include/asm-generic/posix_types.h"
49typedef int __kernel_clockid_t;
50#line 21 "include/linux/types.h"
51typedef __u32 __kernel_dev_t;
52#line 24 "include/linux/types.h"
53typedef __kernel_dev_t dev_t;
54#line 27 "include/linux/types.h"
55typedef unsigned short umode_t;
56#line 30 "include/linux/types.h"
57typedef __kernel_pid_t pid_t;
58#line 35 "include/linux/types.h"
59typedef __kernel_clockid_t clockid_t;
60#line 38 "include/linux/types.h"
61typedef _Bool bool;
62#line 40 "include/linux/types.h"
63typedef __kernel_uid32_t uid_t;
64#line 41 "include/linux/types.h"
65typedef __kernel_gid32_t gid_t;
66#line 54 "include/linux/types.h"
67typedef __kernel_loff_t loff_t;
68#line 63 "include/linux/types.h"
69typedef __kernel_size_t size_t;
70#line 68 "include/linux/types.h"
71typedef __kernel_ssize_t ssize_t;
72#line 78 "include/linux/types.h"
73typedef __kernel_time_t time_t;
74#line 92 "include/linux/types.h"
75typedef unsigned char u_char;
76#line 95 "include/linux/types.h"
77typedef unsigned long u_long;
78#line 111 "include/linux/types.h"
79typedef __s32 int32_t;
80#line 115 "include/linux/types.h"
81typedef __u8 uint8_t;
82#line 117 "include/linux/types.h"
83typedef __u32 uint32_t;
84#line 120 "include/linux/types.h"
85typedef __u64 uint64_t;
86#line 202 "include/linux/types.h"
87typedef unsigned int gfp_t;
88#line 206 "include/linux/types.h"
89typedef u64 phys_addr_t;
90#line 211 "include/linux/types.h"
91typedef phys_addr_t resource_size_t;
92#line 221 "include/linux/types.h"
93struct __anonstruct_atomic_t_6 {
94 int counter ;
95};
96#line 221 "include/linux/types.h"
97typedef struct __anonstruct_atomic_t_6 atomic_t;
98#line 226 "include/linux/types.h"
99struct __anonstruct_atomic64_t_7 {
100 long counter ;
101};
102#line 226 "include/linux/types.h"
103typedef struct __anonstruct_atomic64_t_7 atomic64_t;
104#line 227 "include/linux/types.h"
105struct list_head {
106 struct list_head *next ;
107 struct list_head *prev ;
108};
109#line 232
110struct hlist_node;
111#line 232 "include/linux/types.h"
112struct hlist_head {
113 struct hlist_node *first ;
114};
115#line 236 "include/linux/types.h"
116struct hlist_node {
117 struct hlist_node *next ;
118 struct hlist_node **pprev ;
119};
120#line 247 "include/linux/types.h"
121struct rcu_head {
122 struct rcu_head *next ;
123 void (*func)(struct rcu_head * ) ;
124};
125#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
126struct module;
127#line 55
128struct module;
129#line 146 "include/linux/init.h"
130typedef void (*ctor_fn_t)(void);
131#line 46 "include/linux/dynamic_debug.h"
132struct device;
133#line 46
134struct device;
135#line 57
136struct completion;
137#line 57
138struct completion;
139#line 58
140struct pt_regs;
141#line 58
142struct pt_regs;
143#line 348 "include/linux/kernel.h"
144struct pid;
145#line 348
146struct pid;
147#line 112 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/stat.h"
148struct timespec;
149#line 112
150struct timespec;
151#line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
152struct page;
153#line 58
154struct page;
155#line 26 "include/asm-generic/getorder.h"
156struct task_struct;
157#line 26
158struct task_struct;
159#line 28
160struct mm_struct;
161#line 28
162struct mm_struct;
163#line 268 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/segment.h"
164struct pt_regs {
165 unsigned long r15 ;
166 unsigned long r14 ;
167 unsigned long r13 ;
168 unsigned long r12 ;
169 unsigned long bp ;
170 unsigned long bx ;
171 unsigned long r11 ;
172 unsigned long r10 ;
173 unsigned long r9 ;
174 unsigned long r8 ;
175 unsigned long ax ;
176 unsigned long cx ;
177 unsigned long dx ;
178 unsigned long si ;
179 unsigned long di ;
180 unsigned long orig_ax ;
181 unsigned long ip ;
182 unsigned long cs ;
183 unsigned long flags ;
184 unsigned long sp ;
185 unsigned long ss ;
186};
187#line 125 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
188struct __anonstruct_ldv_2180_13 {
189 unsigned int a ;
190 unsigned int b ;
191};
192#line 125 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
193struct __anonstruct_ldv_2195_14 {
194 u16 limit0 ;
195 u16 base0 ;
196 unsigned char base1 ;
197 unsigned char type : 4 ;
198 unsigned char s : 1 ;
199 unsigned char dpl : 2 ;
200 unsigned char p : 1 ;
201 unsigned char limit : 4 ;
202 unsigned char avl : 1 ;
203 unsigned char l : 1 ;
204 unsigned char d : 1 ;
205 unsigned char g : 1 ;
206 unsigned char base2 ;
207};
208#line 125 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
209union __anonunion_ldv_2196_12 {
210 struct __anonstruct_ldv_2180_13 ldv_2180 ;
211 struct __anonstruct_ldv_2195_14 ldv_2195 ;
212};
213#line 125 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
214struct desc_struct {
215 union __anonunion_ldv_2196_12 ldv_2196 ;
216};
217#line 13 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
218typedef unsigned long pgdval_t;
219#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
220typedef unsigned long pgprotval_t;
221#line 18 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
222struct pgprot {
223 pgprotval_t pgprot ;
224};
225#line 192 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
226typedef struct pgprot pgprot_t;
227#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
228struct __anonstruct_pgd_t_16 {
229 pgdval_t pgd ;
230};
231#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
232typedef struct __anonstruct_pgd_t_16 pgd_t;
233#line 282 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
234typedef struct page *pgtable_t;
235#line 290
236struct file;
237#line 290
238struct file;
239#line 337
240struct thread_struct;
241#line 337
242struct thread_struct;
243#line 339
244struct cpumask;
245#line 339
246struct cpumask;
247#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
248struct arch_spinlock;
249#line 327
250struct arch_spinlock;
251#line 300 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
252struct kernel_vm86_regs {
253 struct pt_regs pt ;
254 unsigned short es ;
255 unsigned short __esh ;
256 unsigned short ds ;
257 unsigned short __dsh ;
258 unsigned short fs ;
259 unsigned short __fsh ;
260 unsigned short gs ;
261 unsigned short __gsh ;
262};
263#line 203 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/vm86.h"
264union __anonunion_ldv_2824_19 {
265 struct pt_regs *regs ;
266 struct kernel_vm86_regs *vm86 ;
267};
268#line 203 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/vm86.h"
269struct math_emu_info {
270 long ___orig_eip ;
271 union __anonunion_ldv_2824_19 ldv_2824 ;
272};
273#line 306 "include/linux/bitmap.h"
274struct bug_entry {
275 int bug_addr_disp ;
276 int file_disp ;
277 unsigned short line ;
278 unsigned short flags ;
279};
280#line 89 "include/linux/bug.h"
281struct cpumask {
282 unsigned long bits[64U] ;
283};
284#line 14 "include/linux/cpumask.h"
285typedef struct cpumask cpumask_t;
286#line 637 "include/linux/cpumask.h"
287typedef struct cpumask *cpumask_var_t;
288#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
289struct static_key;
290#line 234
291struct static_key;
292#line 287 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
293struct i387_fsave_struct {
294 u32 cwd ;
295 u32 swd ;
296 u32 twd ;
297 u32 fip ;
298 u32 fcs ;
299 u32 foo ;
300 u32 fos ;
301 u32 st_space[20U] ;
302 u32 status ;
303};
304#line 305 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
305struct __anonstruct_ldv_5180_24 {
306 u64 rip ;
307 u64 rdp ;
308};
309#line 305 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
310struct __anonstruct_ldv_5186_25 {
311 u32 fip ;
312 u32 fcs ;
313 u32 foo ;
314 u32 fos ;
315};
316#line 305 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
317union __anonunion_ldv_5187_23 {
318 struct __anonstruct_ldv_5180_24 ldv_5180 ;
319 struct __anonstruct_ldv_5186_25 ldv_5186 ;
320};
321#line 305 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
322union __anonunion_ldv_5196_26 {
323 u32 padding1[12U] ;
324 u32 sw_reserved[12U] ;
325};
326#line 305 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
327struct i387_fxsave_struct {
328 u16 cwd ;
329 u16 swd ;
330 u16 twd ;
331 u16 fop ;
332 union __anonunion_ldv_5187_23 ldv_5187 ;
333 u32 mxcsr ;
334 u32 mxcsr_mask ;
335 u32 st_space[32U] ;
336 u32 xmm_space[64U] ;
337 u32 padding[12U] ;
338 union __anonunion_ldv_5196_26 ldv_5196 ;
339};
340#line 339 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
341struct i387_soft_struct {
342 u32 cwd ;
343 u32 swd ;
344 u32 twd ;
345 u32 fip ;
346 u32 fcs ;
347 u32 foo ;
348 u32 fos ;
349 u32 st_space[20U] ;
350 u8 ftop ;
351 u8 changed ;
352 u8 lookahead ;
353 u8 no_update ;
354 u8 rm ;
355 u8 alimit ;
356 struct math_emu_info *info ;
357 u32 entry_eip ;
358};
359#line 360 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
360struct ymmh_struct {
361 u32 ymmh_space[64U] ;
362};
363#line 365 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
364struct xsave_hdr_struct {
365 u64 xstate_bv ;
366 u64 reserved1[2U] ;
367 u64 reserved2[5U] ;
368};
369#line 371 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
370struct xsave_struct {
371 struct i387_fxsave_struct i387 ;
372 struct xsave_hdr_struct xsave_hdr ;
373 struct ymmh_struct ymmh ;
374};
375#line 377 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
376union thread_xstate {
377 struct i387_fsave_struct fsave ;
378 struct i387_fxsave_struct fxsave ;
379 struct i387_soft_struct soft ;
380 struct xsave_struct xsave ;
381};
382#line 385 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
383struct fpu {
384 unsigned int last_cpu ;
385 unsigned int has_fpu ;
386 union thread_xstate *state ;
387};
388#line 433
389struct kmem_cache;
390#line 434
391struct perf_event;
392#line 434
393struct perf_event;
394#line 435 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
395struct thread_struct {
396 struct desc_struct tls_array[3U] ;
397 unsigned long sp0 ;
398 unsigned long sp ;
399 unsigned long usersp ;
400 unsigned short es ;
401 unsigned short ds ;
402 unsigned short fsindex ;
403 unsigned short gsindex ;
404 unsigned long fs ;
405 unsigned long gs ;
406 struct perf_event *ptrace_bps[4U] ;
407 unsigned long debugreg6 ;
408 unsigned long ptrace_dr7 ;
409 unsigned long cr2 ;
410 unsigned long trap_nr ;
411 unsigned long error_code ;
412 struct fpu fpu ;
413 unsigned long *io_bitmap_ptr ;
414 unsigned long iopl ;
415 unsigned int io_bitmap_max ;
416};
417#line 23 "include/asm-generic/atomic-long.h"
418typedef atomic64_t atomic_long_t;
419#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
420typedef u16 __ticket_t;
421#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
422typedef u32 __ticketpair_t;
423#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
424struct __raw_tickets {
425 __ticket_t head ;
426 __ticket_t tail ;
427};
428#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
429union __anonunion_ldv_5907_29 {
430 __ticketpair_t head_tail ;
431 struct __raw_tickets tickets ;
432};
433#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
434struct arch_spinlock {
435 union __anonunion_ldv_5907_29 ldv_5907 ;
436};
437#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
438typedef struct arch_spinlock arch_spinlock_t;
439#line 34 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
440struct lockdep_map;
441#line 34
442struct lockdep_map;
443#line 55 "include/linux/debug_locks.h"
444struct stack_trace {
445 unsigned int nr_entries ;
446 unsigned int max_entries ;
447 unsigned long *entries ;
448 int skip ;
449};
450#line 26 "include/linux/stacktrace.h"
451struct lockdep_subclass_key {
452 char __one_byte ;
453};
454#line 53 "include/linux/lockdep.h"
455struct lock_class_key {
456 struct lockdep_subclass_key subkeys[8U] ;
457};
458#line 59 "include/linux/lockdep.h"
459struct lock_class {
460 struct list_head hash_entry ;
461 struct list_head lock_entry ;
462 struct lockdep_subclass_key *key ;
463 unsigned int subclass ;
464 unsigned int dep_gen_id ;
465 unsigned long usage_mask ;
466 struct stack_trace usage_traces[13U] ;
467 struct list_head locks_after ;
468 struct list_head locks_before ;
469 unsigned int version ;
470 unsigned long ops ;
471 char const *name ;
472 int name_version ;
473 unsigned long contention_point[4U] ;
474 unsigned long contending_point[4U] ;
475};
476#line 144 "include/linux/lockdep.h"
477struct lockdep_map {
478 struct lock_class_key *key ;
479 struct lock_class *class_cache[2U] ;
480 char const *name ;
481 int cpu ;
482 unsigned long ip ;
483};
484#line 187 "include/linux/lockdep.h"
485struct held_lock {
486 u64 prev_chain_key ;
487 unsigned long acquire_ip ;
488 struct lockdep_map *instance ;
489 struct lockdep_map *nest_lock ;
490 u64 waittime_stamp ;
491 u64 holdtime_stamp ;
492 unsigned short class_idx : 13 ;
493 unsigned char irq_context : 2 ;
494 unsigned char trylock : 1 ;
495 unsigned char read : 2 ;
496 unsigned char check : 2 ;
497 unsigned char hardirqs_off : 1 ;
498 unsigned short references : 11 ;
499};
500#line 556 "include/linux/lockdep.h"
501struct raw_spinlock {
502 arch_spinlock_t raw_lock ;
503 unsigned int magic ;
504 unsigned int owner_cpu ;
505 void *owner ;
506 struct lockdep_map dep_map ;
507};
508#line 32 "include/linux/spinlock_types.h"
509typedef struct raw_spinlock raw_spinlock_t;
510#line 33 "include/linux/spinlock_types.h"
511struct __anonstruct_ldv_6122_33 {
512 u8 __padding[24U] ;
513 struct lockdep_map dep_map ;
514};
515#line 33 "include/linux/spinlock_types.h"
516union __anonunion_ldv_6123_32 {
517 struct raw_spinlock rlock ;
518 struct __anonstruct_ldv_6122_33 ldv_6122 ;
519};
520#line 33 "include/linux/spinlock_types.h"
521struct spinlock {
522 union __anonunion_ldv_6123_32 ldv_6123 ;
523};
524#line 76 "include/linux/spinlock_types.h"
525typedef struct spinlock spinlock_t;
526#line 110 "include/linux/seqlock.h"
527struct seqcount {
528 unsigned int sequence ;
529};
530#line 121 "include/linux/seqlock.h"
531typedef struct seqcount seqcount_t;
532#line 254 "include/linux/seqlock.h"
533struct timespec {
534 __kernel_time_t tv_sec ;
535 long tv_nsec ;
536};
537#line 27 "include/linux/wait.h"
538struct __wait_queue;
539#line 27 "include/linux/wait.h"
540typedef struct __wait_queue wait_queue_t;
541#line 30 "include/linux/wait.h"
542struct __wait_queue {
543 unsigned int flags ;
544 void *private ;
545 int (*func)(wait_queue_t * , unsigned int , int , void * ) ;
546 struct list_head task_list ;
547};
548#line 48 "include/linux/wait.h"
549struct __wait_queue_head {
550 spinlock_t lock ;
551 struct list_head task_list ;
552};
553#line 53 "include/linux/wait.h"
554typedef struct __wait_queue_head wait_queue_head_t;
555#line 98 "include/linux/nodemask.h"
556struct __anonstruct_nodemask_t_36 {
557 unsigned long bits[16U] ;
558};
559#line 98 "include/linux/nodemask.h"
560typedef struct __anonstruct_nodemask_t_36 nodemask_t;
561#line 670 "include/linux/mmzone.h"
562struct mutex {
563 atomic_t count ;
564 spinlock_t wait_lock ;
565 struct list_head wait_list ;
566 struct task_struct *owner ;
567 char const *name ;
568 void *magic ;
569 struct lockdep_map dep_map ;
570};
571#line 63 "include/linux/mutex.h"
572struct mutex_waiter {
573 struct list_head list ;
574 struct task_struct *task ;
575 void *magic ;
576};
577#line 171
578struct rw_semaphore;
579#line 171
580struct rw_semaphore;
581#line 172 "include/linux/mutex.h"
582struct rw_semaphore {
583 long count ;
584 raw_spinlock_t wait_lock ;
585 struct list_head wait_list ;
586 struct lockdep_map dep_map ;
587};
588#line 128 "include/linux/rwsem.h"
589struct completion {
590 unsigned int done ;
591 wait_queue_head_t wait ;
592};
593#line 188 "include/linux/rcupdate.h"
594struct notifier_block;
595#line 188
596struct notifier_block;
597#line 239 "include/linux/srcu.h"
598struct notifier_block {
599 int (*notifier_call)(struct notifier_block * , unsigned long , void * ) ;
600 struct notifier_block *next ;
601 int priority ;
602};
603#line 312 "include/linux/jiffies.h"
604union ktime {
605 s64 tv64 ;
606};
607#line 59 "include/linux/ktime.h"
608typedef union ktime ktime_t;
609#line 341
610struct tvec_base;
611#line 341
612struct tvec_base;
613#line 342 "include/linux/ktime.h"
614struct timer_list {
615 struct list_head entry ;
616 unsigned long expires ;
617 struct tvec_base *base ;
618 void (*function)(unsigned long ) ;
619 unsigned long data ;
620 int slack ;
621 int start_pid ;
622 void *start_site ;
623 char start_comm[16U] ;
624 struct lockdep_map lockdep_map ;
625};
626#line 289 "include/linux/timer.h"
627struct hrtimer;
628#line 289
629struct hrtimer;
630#line 290
631enum hrtimer_restart;
632#line 302
633struct work_struct;
634#line 302
635struct work_struct;
636#line 45 "include/linux/workqueue.h"
637struct work_struct {
638 atomic_long_t data ;
639 struct list_head entry ;
640 void (*func)(struct work_struct * ) ;
641 struct lockdep_map lockdep_map ;
642};
643#line 46 "include/linux/pm.h"
644struct pm_message {
645 int event ;
646};
647#line 52 "include/linux/pm.h"
648typedef struct pm_message pm_message_t;
649#line 53 "include/linux/pm.h"
650struct dev_pm_ops {
651 int (*prepare)(struct device * ) ;
652 void (*complete)(struct device * ) ;
653 int (*suspend)(struct device * ) ;
654 int (*resume)(struct device * ) ;
655 int (*freeze)(struct device * ) ;
656 int (*thaw)(struct device * ) ;
657 int (*poweroff)(struct device * ) ;
658 int (*restore)(struct device * ) ;
659 int (*suspend_late)(struct device * ) ;
660 int (*resume_early)(struct device * ) ;
661 int (*freeze_late)(struct device * ) ;
662 int (*thaw_early)(struct device * ) ;
663 int (*poweroff_late)(struct device * ) ;
664 int (*restore_early)(struct device * ) ;
665 int (*suspend_noirq)(struct device * ) ;
666 int (*resume_noirq)(struct device * ) ;
667 int (*freeze_noirq)(struct device * ) ;
668 int (*thaw_noirq)(struct device * ) ;
669 int (*poweroff_noirq)(struct device * ) ;
670 int (*restore_noirq)(struct device * ) ;
671 int (*runtime_suspend)(struct device * ) ;
672 int (*runtime_resume)(struct device * ) ;
673 int (*runtime_idle)(struct device * ) ;
674};
675#line 289
676enum rpm_status {
677 RPM_ACTIVE = 0,
678 RPM_RESUMING = 1,
679 RPM_SUSPENDED = 2,
680 RPM_SUSPENDING = 3
681} ;
682#line 296
683enum rpm_request {
684 RPM_REQ_NONE = 0,
685 RPM_REQ_IDLE = 1,
686 RPM_REQ_SUSPEND = 2,
687 RPM_REQ_AUTOSUSPEND = 3,
688 RPM_REQ_RESUME = 4
689} ;
690#line 304
691struct wakeup_source;
692#line 304
693struct wakeup_source;
694#line 494 "include/linux/pm.h"
695struct pm_subsys_data {
696 spinlock_t lock ;
697 unsigned int refcount ;
698};
699#line 499
700struct dev_pm_qos_request;
701#line 499
702struct pm_qos_constraints;
703#line 499 "include/linux/pm.h"
704struct dev_pm_info {
705 pm_message_t power_state ;
706 unsigned char can_wakeup : 1 ;
707 unsigned char async_suspend : 1 ;
708 bool is_prepared ;
709 bool is_suspended ;
710 bool ignore_children ;
711 spinlock_t lock ;
712 struct list_head entry ;
713 struct completion completion ;
714 struct wakeup_source *wakeup ;
715 bool wakeup_path ;
716 struct timer_list suspend_timer ;
717 unsigned long timer_expires ;
718 struct work_struct work ;
719 wait_queue_head_t wait_queue ;
720 atomic_t usage_count ;
721 atomic_t child_count ;
722 unsigned char disable_depth : 3 ;
723 unsigned char idle_notification : 1 ;
724 unsigned char request_pending : 1 ;
725 unsigned char deferred_resume : 1 ;
726 unsigned char run_wake : 1 ;
727 unsigned char runtime_auto : 1 ;
728 unsigned char no_callbacks : 1 ;
729 unsigned char irq_safe : 1 ;
730 unsigned char use_autosuspend : 1 ;
731 unsigned char timer_autosuspends : 1 ;
732 enum rpm_request request ;
733 enum rpm_status runtime_status ;
734 int runtime_error ;
735 int autosuspend_delay ;
736 unsigned long last_busy ;
737 unsigned long active_jiffies ;
738 unsigned long suspended_jiffies ;
739 unsigned long accounting_timestamp ;
740 ktime_t suspend_time ;
741 s64 max_time_suspended_ns ;
742 struct dev_pm_qos_request *pq_req ;
743 struct pm_subsys_data *subsys_data ;
744 struct pm_qos_constraints *constraints ;
745};
746#line 558 "include/linux/pm.h"
747struct dev_pm_domain {
748 struct dev_pm_ops ops ;
749};
750#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
751struct __anonstruct_mm_context_t_101 {
752 void *ldt ;
753 int size ;
754 unsigned short ia32_compat ;
755 struct mutex lock ;
756 void *vdso ;
757};
758#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
759typedef struct __anonstruct_mm_context_t_101 mm_context_t;
760#line 18 "include/asm-generic/pci_iomap.h"
761struct vm_area_struct;
762#line 18
763struct vm_area_struct;
764#line 835 "include/linux/sysctl.h"
765struct rb_node {
766 unsigned long rb_parent_color ;
767 struct rb_node *rb_right ;
768 struct rb_node *rb_left ;
769};
770#line 108 "include/linux/rbtree.h"
771struct rb_root {
772 struct rb_node *rb_node ;
773};
774#line 176
775struct nsproxy;
776#line 176
777struct nsproxy;
778#line 37 "include/linux/kmod.h"
779struct cred;
780#line 37
781struct cred;
782#line 18 "include/linux/elf.h"
783typedef __u64 Elf64_Addr;
784#line 19 "include/linux/elf.h"
785typedef __u16 Elf64_Half;
786#line 23 "include/linux/elf.h"
787typedef __u32 Elf64_Word;
788#line 24 "include/linux/elf.h"
789typedef __u64 Elf64_Xword;
790#line 193 "include/linux/elf.h"
791struct elf64_sym {
792 Elf64_Word st_name ;
793 unsigned char st_info ;
794 unsigned char st_other ;
795 Elf64_Half st_shndx ;
796 Elf64_Addr st_value ;
797 Elf64_Xword st_size ;
798};
799#line 201 "include/linux/elf.h"
800typedef struct elf64_sym Elf64_Sym;
801#line 445
802struct sock;
803#line 445
804struct sock;
805#line 446
806struct kobject;
807#line 446
808struct kobject;
809#line 447
810enum kobj_ns_type {
811 KOBJ_NS_TYPE_NONE = 0,
812 KOBJ_NS_TYPE_NET = 1,
813 KOBJ_NS_TYPES = 2
814} ;
815#line 453 "include/linux/elf.h"
816struct kobj_ns_type_operations {
817 enum kobj_ns_type type ;
818 void *(*grab_current_ns)(void) ;
819 void const *(*netlink_ns)(struct sock * ) ;
820 void const *(*initial_ns)(void) ;
821 void (*drop_ns)(void * ) ;
822};
823#line 57 "include/linux/kobject_ns.h"
824struct attribute {
825 char const *name ;
826 umode_t mode ;
827 struct lock_class_key *key ;
828 struct lock_class_key skey ;
829};
830#line 33 "include/linux/sysfs.h"
831struct attribute_group {
832 char const *name ;
833 umode_t (*is_visible)(struct kobject * , struct attribute * , int ) ;
834 struct attribute **attrs ;
835};
836#line 62 "include/linux/sysfs.h"
837struct bin_attribute {
838 struct attribute attr ;
839 size_t size ;
840 void *private ;
841 ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
842 loff_t , size_t ) ;
843 ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
844 loff_t , size_t ) ;
845 int (*mmap)(struct file * , struct kobject * , struct bin_attribute * , struct vm_area_struct * ) ;
846};
847#line 98 "include/linux/sysfs.h"
848struct sysfs_ops {
849 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
850 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
851 void const *(*namespace)(struct kobject * , struct attribute const * ) ;
852};
853#line 117
854struct sysfs_dirent;
855#line 117
856struct sysfs_dirent;
857#line 182 "include/linux/sysfs.h"
858struct kref {
859 atomic_t refcount ;
860};
861#line 49 "include/linux/kobject.h"
862struct kset;
863#line 49
864struct kobj_type;
865#line 49 "include/linux/kobject.h"
866struct kobject {
867 char const *name ;
868 struct list_head entry ;
869 struct kobject *parent ;
870 struct kset *kset ;
871 struct kobj_type *ktype ;
872 struct sysfs_dirent *sd ;
873 struct kref kref ;
874 unsigned char state_initialized : 1 ;
875 unsigned char state_in_sysfs : 1 ;
876 unsigned char state_add_uevent_sent : 1 ;
877 unsigned char state_remove_uevent_sent : 1 ;
878 unsigned char uevent_suppress : 1 ;
879};
880#line 107 "include/linux/kobject.h"
881struct kobj_type {
882 void (*release)(struct kobject * ) ;
883 struct sysfs_ops const *sysfs_ops ;
884 struct attribute **default_attrs ;
885 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject * ) ;
886 void const *(*namespace)(struct kobject * ) ;
887};
888#line 115 "include/linux/kobject.h"
889struct kobj_uevent_env {
890 char *envp[32U] ;
891 int envp_idx ;
892 char buf[2048U] ;
893 int buflen ;
894};
895#line 122 "include/linux/kobject.h"
896struct kset_uevent_ops {
897 int (* const filter)(struct kset * , struct kobject * ) ;
898 char const *(* const name)(struct kset * , struct kobject * ) ;
899 int (* const uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
900};
901#line 139 "include/linux/kobject.h"
902struct kset {
903 struct list_head list ;
904 spinlock_t list_lock ;
905 struct kobject kobj ;
906 struct kset_uevent_ops const *uevent_ops ;
907};
908#line 215
909struct kernel_param;
910#line 215
911struct kernel_param;
912#line 216 "include/linux/kobject.h"
913struct kernel_param_ops {
914 int (*set)(char const * , struct kernel_param const * ) ;
915 int (*get)(char * , struct kernel_param const * ) ;
916 void (*free)(void * ) ;
917};
918#line 49 "include/linux/moduleparam.h"
919struct kparam_string;
920#line 49
921struct kparam_array;
922#line 49 "include/linux/moduleparam.h"
923union __anonunion_ldv_13371_134 {
924 void *arg ;
925 struct kparam_string const *str ;
926 struct kparam_array const *arr ;
927};
928#line 49 "include/linux/moduleparam.h"
929struct kernel_param {
930 char const *name ;
931 struct kernel_param_ops const *ops ;
932 u16 perm ;
933 s16 level ;
934 union __anonunion_ldv_13371_134 ldv_13371 ;
935};
936#line 61 "include/linux/moduleparam.h"
937struct kparam_string {
938 unsigned int maxlen ;
939 char *string ;
940};
941#line 67 "include/linux/moduleparam.h"
942struct kparam_array {
943 unsigned int max ;
944 unsigned int elemsize ;
945 unsigned int *num ;
946 struct kernel_param_ops const *ops ;
947 void *elem ;
948};
949#line 458 "include/linux/moduleparam.h"
950struct static_key {
951 atomic_t enabled ;
952};
953#line 225 "include/linux/jump_label.h"
954struct tracepoint;
955#line 225
956struct tracepoint;
957#line 226 "include/linux/jump_label.h"
958struct tracepoint_func {
959 void *func ;
960 void *data ;
961};
962#line 29 "include/linux/tracepoint.h"
963struct tracepoint {
964 char const *name ;
965 struct static_key key ;
966 void (*regfunc)(void) ;
967 void (*unregfunc)(void) ;
968 struct tracepoint_func *funcs ;
969};
970#line 86 "include/linux/tracepoint.h"
971struct kernel_symbol {
972 unsigned long value ;
973 char const *name ;
974};
975#line 27 "include/linux/export.h"
976struct mod_arch_specific {
977
978};
979#line 34 "include/linux/module.h"
980struct module_param_attrs;
981#line 34 "include/linux/module.h"
982struct module_kobject {
983 struct kobject kobj ;
984 struct module *mod ;
985 struct kobject *drivers_dir ;
986 struct module_param_attrs *mp ;
987};
988#line 43 "include/linux/module.h"
989struct module_attribute {
990 struct attribute attr ;
991 ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
992 ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const * ,
993 size_t ) ;
994 void (*setup)(struct module * , char const * ) ;
995 int (*test)(struct module * ) ;
996 void (*free)(struct module * ) ;
997};
998#line 69
999struct exception_table_entry;
1000#line 69
1001struct exception_table_entry;
1002#line 198
1003enum module_state {
1004 MODULE_STATE_LIVE = 0,
1005 MODULE_STATE_COMING = 1,
1006 MODULE_STATE_GOING = 2
1007} ;
1008#line 204 "include/linux/module.h"
1009struct module_ref {
1010 unsigned long incs ;
1011 unsigned long decs ;
1012};
1013#line 219
1014struct module_sect_attrs;
1015#line 219
1016struct module_notes_attrs;
1017#line 219
1018struct ftrace_event_call;
1019#line 219 "include/linux/module.h"
1020struct module {
1021 enum module_state state ;
1022 struct list_head list ;
1023 char name[56U] ;
1024 struct module_kobject mkobj ;
1025 struct module_attribute *modinfo_attrs ;
1026 char const *version ;
1027 char const *srcversion ;
1028 struct kobject *holders_dir ;
1029 struct kernel_symbol const *syms ;
1030 unsigned long const *crcs ;
1031 unsigned int num_syms ;
1032 struct kernel_param *kp ;
1033 unsigned int num_kp ;
1034 unsigned int num_gpl_syms ;
1035 struct kernel_symbol const *gpl_syms ;
1036 unsigned long const *gpl_crcs ;
1037 struct kernel_symbol const *unused_syms ;
1038 unsigned long const *unused_crcs ;
1039 unsigned int num_unused_syms ;
1040 unsigned int num_unused_gpl_syms ;
1041 struct kernel_symbol const *unused_gpl_syms ;
1042 unsigned long const *unused_gpl_crcs ;
1043 struct kernel_symbol const *gpl_future_syms ;
1044 unsigned long const *gpl_future_crcs ;
1045 unsigned int num_gpl_future_syms ;
1046 unsigned int num_exentries ;
1047 struct exception_table_entry *extable ;
1048 int (*init)(void) ;
1049 void *module_init ;
1050 void *module_core ;
1051 unsigned int init_size ;
1052 unsigned int core_size ;
1053 unsigned int init_text_size ;
1054 unsigned int core_text_size ;
1055 unsigned int init_ro_size ;
1056 unsigned int core_ro_size ;
1057 struct mod_arch_specific arch ;
1058 unsigned int taints ;
1059 unsigned int num_bugs ;
1060 struct list_head bug_list ;
1061 struct bug_entry *bug_table ;
1062 Elf64_Sym *symtab ;
1063 Elf64_Sym *core_symtab ;
1064 unsigned int num_symtab ;
1065 unsigned int core_num_syms ;
1066 char *strtab ;
1067 char *core_strtab ;
1068 struct module_sect_attrs *sect_attrs ;
1069 struct module_notes_attrs *notes_attrs ;
1070 char *args ;
1071 void *percpu ;
1072 unsigned int percpu_size ;
1073 unsigned int num_tracepoints ;
1074 struct tracepoint * const *tracepoints_ptrs ;
1075 unsigned int num_trace_bprintk_fmt ;
1076 char const **trace_bprintk_fmt_start ;
1077 struct ftrace_event_call **trace_events ;
1078 unsigned int num_trace_events ;
1079 struct list_head source_list ;
1080 struct list_head target_list ;
1081 struct task_struct *waiter ;
1082 void (*exit)(void) ;
1083 struct module_ref *refptr ;
1084 ctor_fn_t (**ctors)(void) ;
1085 unsigned int num_ctors ;
1086};
1087#line 88 "include/linux/kmemleak.h"
1088struct kmem_cache_cpu {
1089 void **freelist ;
1090 unsigned long tid ;
1091 struct page *page ;
1092 struct page *partial ;
1093 int node ;
1094 unsigned int stat[26U] ;
1095};
1096#line 55 "include/linux/slub_def.h"
1097struct kmem_cache_node {
1098 spinlock_t list_lock ;
1099 unsigned long nr_partial ;
1100 struct list_head partial ;
1101 atomic_long_t nr_slabs ;
1102 atomic_long_t total_objects ;
1103 struct list_head full ;
1104};
1105#line 66 "include/linux/slub_def.h"
1106struct kmem_cache_order_objects {
1107 unsigned long x ;
1108};
1109#line 76 "include/linux/slub_def.h"
1110struct kmem_cache {
1111 struct kmem_cache_cpu *cpu_slab ;
1112 unsigned long flags ;
1113 unsigned long min_partial ;
1114 int size ;
1115 int objsize ;
1116 int offset ;
1117 int cpu_partial ;
1118 struct kmem_cache_order_objects oo ;
1119 struct kmem_cache_order_objects max ;
1120 struct kmem_cache_order_objects min ;
1121 gfp_t allocflags ;
1122 int refcount ;
1123 void (*ctor)(void * ) ;
1124 int inuse ;
1125 int align ;
1126 int reserved ;
1127 char const *name ;
1128 struct list_head list ;
1129 struct kobject kobj ;
1130 int remote_node_defrag_ratio ;
1131 struct kmem_cache_node *node[1024U] ;
1132};
1133#line 18 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
1134struct tty_struct;
1135#line 18
1136struct tty_struct;
1137#line 93 "include/linux/capability.h"
1138struct kernel_cap_struct {
1139 __u32 cap[2U] ;
1140};
1141#line 96 "include/linux/capability.h"
1142typedef struct kernel_cap_struct kernel_cap_t;
1143#line 105
1144struct user_namespace;
1145#line 105
1146struct user_namespace;
1147#line 554
1148struct prio_tree_node;
1149#line 554 "include/linux/capability.h"
1150struct raw_prio_tree_node {
1151 struct prio_tree_node *left ;
1152 struct prio_tree_node *right ;
1153 struct prio_tree_node *parent ;
1154};
1155#line 19 "include/linux/prio_tree.h"
1156struct prio_tree_node {
1157 struct prio_tree_node *left ;
1158 struct prio_tree_node *right ;
1159 struct prio_tree_node *parent ;
1160 unsigned long start ;
1161 unsigned long last ;
1162};
1163#line 116
1164struct address_space;
1165#line 116
1166struct address_space;
1167#line 117 "include/linux/prio_tree.h"
1168union __anonunion_ldv_14567_137 {
1169 unsigned long index ;
1170 void *freelist ;
1171};
1172#line 117 "include/linux/prio_tree.h"
1173struct __anonstruct_ldv_14577_141 {
1174 unsigned short inuse ;
1175 unsigned short objects : 15 ;
1176 unsigned char frozen : 1 ;
1177};
1178#line 117 "include/linux/prio_tree.h"
1179union __anonunion_ldv_14578_140 {
1180 atomic_t _mapcount ;
1181 struct __anonstruct_ldv_14577_141 ldv_14577 ;
1182};
1183#line 117 "include/linux/prio_tree.h"
1184struct __anonstruct_ldv_14580_139 {
1185 union __anonunion_ldv_14578_140 ldv_14578 ;
1186 atomic_t _count ;
1187};
1188#line 117 "include/linux/prio_tree.h"
1189union __anonunion_ldv_14581_138 {
1190 unsigned long counters ;
1191 struct __anonstruct_ldv_14580_139 ldv_14580 ;
1192};
1193#line 117 "include/linux/prio_tree.h"
1194struct __anonstruct_ldv_14582_136 {
1195 union __anonunion_ldv_14567_137 ldv_14567 ;
1196 union __anonunion_ldv_14581_138 ldv_14581 ;
1197};
1198#line 117 "include/linux/prio_tree.h"
1199struct __anonstruct_ldv_14589_143 {
1200 struct page *next ;
1201 int pages ;
1202 int pobjects ;
1203};
1204#line 117 "include/linux/prio_tree.h"
1205union __anonunion_ldv_14590_142 {
1206 struct list_head lru ;
1207 struct __anonstruct_ldv_14589_143 ldv_14589 ;
1208};
1209#line 117 "include/linux/prio_tree.h"
1210union __anonunion_ldv_14595_144 {
1211 unsigned long private ;
1212 struct kmem_cache *slab ;
1213 struct page *first_page ;
1214};
1215#line 117 "include/linux/prio_tree.h"
1216struct page {
1217 unsigned long flags ;
1218 struct address_space *mapping ;
1219 struct __anonstruct_ldv_14582_136 ldv_14582 ;
1220 union __anonunion_ldv_14590_142 ldv_14590 ;
1221 union __anonunion_ldv_14595_144 ldv_14595 ;
1222 unsigned long debug_flags ;
1223};
1224#line 192 "include/linux/mm_types.h"
1225struct __anonstruct_vm_set_146 {
1226 struct list_head list ;
1227 void *parent ;
1228 struct vm_area_struct *head ;
1229};
1230#line 192 "include/linux/mm_types.h"
1231union __anonunion_shared_145 {
1232 struct __anonstruct_vm_set_146 vm_set ;
1233 struct raw_prio_tree_node prio_tree_node ;
1234};
1235#line 192
1236struct anon_vma;
1237#line 192
1238struct vm_operations_struct;
1239#line 192
1240struct mempolicy;
1241#line 192 "include/linux/mm_types.h"
1242struct vm_area_struct {
1243 struct mm_struct *vm_mm ;
1244 unsigned long vm_start ;
1245 unsigned long vm_end ;
1246 struct vm_area_struct *vm_next ;
1247 struct vm_area_struct *vm_prev ;
1248 pgprot_t vm_page_prot ;
1249 unsigned long vm_flags ;
1250 struct rb_node vm_rb ;
1251 union __anonunion_shared_145 shared ;
1252 struct list_head anon_vma_chain ;
1253 struct anon_vma *anon_vma ;
1254 struct vm_operations_struct const *vm_ops ;
1255 unsigned long vm_pgoff ;
1256 struct file *vm_file ;
1257 void *vm_private_data ;
1258 struct mempolicy *vm_policy ;
1259};
1260#line 255 "include/linux/mm_types.h"
1261struct core_thread {
1262 struct task_struct *task ;
1263 struct core_thread *next ;
1264};
1265#line 261 "include/linux/mm_types.h"
1266struct core_state {
1267 atomic_t nr_threads ;
1268 struct core_thread dumper ;
1269 struct completion startup ;
1270};
1271#line 274 "include/linux/mm_types.h"
1272struct mm_rss_stat {
1273 atomic_long_t count[3U] ;
1274};
1275#line 287
1276struct linux_binfmt;
1277#line 287
1278struct mmu_notifier_mm;
1279#line 287 "include/linux/mm_types.h"
1280struct mm_struct {
1281 struct vm_area_struct *mmap ;
1282 struct rb_root mm_rb ;
1283 struct vm_area_struct *mmap_cache ;
1284 unsigned long (*get_unmapped_area)(struct file * , unsigned long , unsigned long ,
1285 unsigned long , unsigned long ) ;
1286 void (*unmap_area)(struct mm_struct * , unsigned long ) ;
1287 unsigned long mmap_base ;
1288 unsigned long task_size ;
1289 unsigned long cached_hole_size ;
1290 unsigned long free_area_cache ;
1291 pgd_t *pgd ;
1292 atomic_t mm_users ;
1293 atomic_t mm_count ;
1294 int map_count ;
1295 spinlock_t page_table_lock ;
1296 struct rw_semaphore mmap_sem ;
1297 struct list_head mmlist ;
1298 unsigned long hiwater_rss ;
1299 unsigned long hiwater_vm ;
1300 unsigned long total_vm ;
1301 unsigned long locked_vm ;
1302 unsigned long pinned_vm ;
1303 unsigned long shared_vm ;
1304 unsigned long exec_vm ;
1305 unsigned long stack_vm ;
1306 unsigned long reserved_vm ;
1307 unsigned long def_flags ;
1308 unsigned long nr_ptes ;
1309 unsigned long start_code ;
1310 unsigned long end_code ;
1311 unsigned long start_data ;
1312 unsigned long end_data ;
1313 unsigned long start_brk ;
1314 unsigned long brk ;
1315 unsigned long start_stack ;
1316 unsigned long arg_start ;
1317 unsigned long arg_end ;
1318 unsigned long env_start ;
1319 unsigned long env_end ;
1320 unsigned long saved_auxv[44U] ;
1321 struct mm_rss_stat rss_stat ;
1322 struct linux_binfmt *binfmt ;
1323 cpumask_var_t cpu_vm_mask_var ;
1324 mm_context_t context ;
1325 unsigned int faultstamp ;
1326 unsigned int token_priority ;
1327 unsigned int last_interval ;
1328 unsigned long flags ;
1329 struct core_state *core_state ;
1330 spinlock_t ioctx_lock ;
1331 struct hlist_head ioctx_list ;
1332 struct task_struct *owner ;
1333 struct file *exe_file ;
1334 unsigned long num_exe_file_vmas ;
1335 struct mmu_notifier_mm *mmu_notifier_mm ;
1336 pgtable_t pmd_huge_pte ;
1337 struct cpumask cpumask_allocation ;
1338};
1339#line 7 "include/asm-generic/cputime.h"
1340typedef unsigned long cputime_t;
1341#line 98 "include/linux/sem.h"
1342struct sem_undo_list;
1343#line 98 "include/linux/sem.h"
1344struct sysv_sem {
1345 struct sem_undo_list *undo_list ;
1346};
1347#line 107
1348struct siginfo;
1349#line 107
1350struct siginfo;
1351#line 32 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1352struct __anonstruct_sigset_t_147 {
1353 unsigned long sig[1U] ;
1354};
1355#line 32 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1356typedef struct __anonstruct_sigset_t_147 sigset_t;
1357#line 17 "include/asm-generic/signal-defs.h"
1358typedef void __signalfn_t(int );
1359#line 18 "include/asm-generic/signal-defs.h"
1360typedef __signalfn_t *__sighandler_t;
1361#line 20 "include/asm-generic/signal-defs.h"
1362typedef void __restorefn_t(void);
1363#line 21 "include/asm-generic/signal-defs.h"
1364typedef __restorefn_t *__sigrestore_t;
1365#line 126 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1366struct sigaction {
1367 __sighandler_t sa_handler ;
1368 unsigned long sa_flags ;
1369 __sigrestore_t sa_restorer ;
1370 sigset_t sa_mask ;
1371};
1372#line 173 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1373struct k_sigaction {
1374 struct sigaction sa ;
1375};
1376#line 185 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/signal.h"
1377union sigval {
1378 int sival_int ;
1379 void *sival_ptr ;
1380};
1381#line 10 "include/asm-generic/siginfo.h"
1382typedef union sigval sigval_t;
1383#line 11 "include/asm-generic/siginfo.h"
1384struct __anonstruct__kill_149 {
1385 __kernel_pid_t _pid ;
1386 __kernel_uid32_t _uid ;
1387};
1388#line 11 "include/asm-generic/siginfo.h"
1389struct __anonstruct__timer_150 {
1390 __kernel_timer_t _tid ;
1391 int _overrun ;
1392 char _pad[0U] ;
1393 sigval_t _sigval ;
1394 int _sys_private ;
1395};
1396#line 11 "include/asm-generic/siginfo.h"
1397struct __anonstruct__rt_151 {
1398 __kernel_pid_t _pid ;
1399 __kernel_uid32_t _uid ;
1400 sigval_t _sigval ;
1401};
1402#line 11 "include/asm-generic/siginfo.h"
1403struct __anonstruct__sigchld_152 {
1404 __kernel_pid_t _pid ;
1405 __kernel_uid32_t _uid ;
1406 int _status ;
1407 __kernel_clock_t _utime ;
1408 __kernel_clock_t _stime ;
1409};
1410#line 11 "include/asm-generic/siginfo.h"
1411struct __anonstruct__sigfault_153 {
1412 void *_addr ;
1413 short _addr_lsb ;
1414};
1415#line 11 "include/asm-generic/siginfo.h"
1416struct __anonstruct__sigpoll_154 {
1417 long _band ;
1418 int _fd ;
1419};
1420#line 11 "include/asm-generic/siginfo.h"
1421union __anonunion__sifields_148 {
1422 int _pad[28U] ;
1423 struct __anonstruct__kill_149 _kill ;
1424 struct __anonstruct__timer_150 _timer ;
1425 struct __anonstruct__rt_151 _rt ;
1426 struct __anonstruct__sigchld_152 _sigchld ;
1427 struct __anonstruct__sigfault_153 _sigfault ;
1428 struct __anonstruct__sigpoll_154 _sigpoll ;
1429};
1430#line 11 "include/asm-generic/siginfo.h"
1431struct siginfo {
1432 int si_signo ;
1433 int si_errno ;
1434 int si_code ;
1435 union __anonunion__sifields_148 _sifields ;
1436};
1437#line 102 "include/asm-generic/siginfo.h"
1438typedef struct siginfo siginfo_t;
1439#line 14 "include/linux/signal.h"
1440struct user_struct;
1441#line 24 "include/linux/signal.h"
1442struct sigpending {
1443 struct list_head list ;
1444 sigset_t signal ;
1445};
1446#line 395
1447struct pid_namespace;
1448#line 395 "include/linux/signal.h"
1449struct upid {
1450 int nr ;
1451 struct pid_namespace *ns ;
1452 struct hlist_node pid_chain ;
1453};
1454#line 56 "include/linux/pid.h"
1455struct pid {
1456 atomic_t count ;
1457 unsigned int level ;
1458 struct hlist_head tasks[3U] ;
1459 struct rcu_head rcu ;
1460 struct upid numbers[1U] ;
1461};
1462#line 68 "include/linux/pid.h"
1463struct pid_link {
1464 struct hlist_node node ;
1465 struct pid *pid ;
1466};
1467#line 10 "include/linux/seccomp.h"
1468struct __anonstruct_seccomp_t_157 {
1469 int mode ;
1470};
1471#line 10 "include/linux/seccomp.h"
1472typedef struct __anonstruct_seccomp_t_157 seccomp_t;
1473#line 427 "include/linux/rculist.h"
1474struct plist_head {
1475 struct list_head node_list ;
1476};
1477#line 84 "include/linux/plist.h"
1478struct plist_node {
1479 int prio ;
1480 struct list_head prio_list ;
1481 struct list_head node_list ;
1482};
1483#line 38 "include/linux/rtmutex.h"
1484struct rt_mutex_waiter;
1485#line 38
1486struct rt_mutex_waiter;
1487#line 41 "include/linux/resource.h"
1488struct rlimit {
1489 unsigned long rlim_cur ;
1490 unsigned long rlim_max ;
1491};
1492#line 85 "include/linux/resource.h"
1493struct timerqueue_node {
1494 struct rb_node node ;
1495 ktime_t expires ;
1496};
1497#line 12 "include/linux/timerqueue.h"
1498struct timerqueue_head {
1499 struct rb_root head ;
1500 struct timerqueue_node *next ;
1501};
1502#line 50
1503struct hrtimer_clock_base;
1504#line 50
1505struct hrtimer_clock_base;
1506#line 51
1507struct hrtimer_cpu_base;
1508#line 51
1509struct hrtimer_cpu_base;
1510#line 60
1511enum hrtimer_restart {
1512 HRTIMER_NORESTART = 0,
1513 HRTIMER_RESTART = 1
1514} ;
1515#line 65 "include/linux/timerqueue.h"
1516struct hrtimer {
1517 struct timerqueue_node node ;
1518 ktime_t _softexpires ;
1519 enum hrtimer_restart (*function)(struct hrtimer * ) ;
1520 struct hrtimer_clock_base *base ;
1521 unsigned long state ;
1522 int start_pid ;
1523 void *start_site ;
1524 char start_comm[16U] ;
1525};
1526#line 132 "include/linux/hrtimer.h"
1527struct hrtimer_clock_base {
1528 struct hrtimer_cpu_base *cpu_base ;
1529 int index ;
1530 clockid_t clockid ;
1531 struct timerqueue_head active ;
1532 ktime_t resolution ;
1533 ktime_t (*get_time)(void) ;
1534 ktime_t softirq_time ;
1535 ktime_t offset ;
1536};
1537#line 162 "include/linux/hrtimer.h"
1538struct hrtimer_cpu_base {
1539 raw_spinlock_t lock ;
1540 unsigned long active_bases ;
1541 ktime_t expires_next ;
1542 int hres_active ;
1543 int hang_detected ;
1544 unsigned long nr_events ;
1545 unsigned long nr_retries ;
1546 unsigned long nr_hangs ;
1547 ktime_t max_hang_time ;
1548 struct hrtimer_clock_base clock_base[3U] ;
1549};
1550#line 452 "include/linux/hrtimer.h"
1551struct task_io_accounting {
1552 u64 rchar ;
1553 u64 wchar ;
1554 u64 syscr ;
1555 u64 syscw ;
1556 u64 read_bytes ;
1557 u64 write_bytes ;
1558 u64 cancelled_write_bytes ;
1559};
1560#line 45 "include/linux/task_io_accounting.h"
1561struct latency_record {
1562 unsigned long backtrace[12U] ;
1563 unsigned int count ;
1564 unsigned long time ;
1565 unsigned long max ;
1566};
1567#line 29 "include/linux/key.h"
1568typedef int32_t key_serial_t;
1569#line 32 "include/linux/key.h"
1570typedef uint32_t key_perm_t;
1571#line 33
1572struct key;
1573#line 33
1574struct key;
1575#line 34
1576struct signal_struct;
1577#line 34
1578struct signal_struct;
1579#line 35
1580struct key_type;
1581#line 35
1582struct key_type;
1583#line 37
1584struct keyring_list;
1585#line 37
1586struct keyring_list;
1587#line 115
1588struct key_user;
1589#line 115 "include/linux/key.h"
1590union __anonunion_ldv_15831_158 {
1591 time_t expiry ;
1592 time_t revoked_at ;
1593};
1594#line 115 "include/linux/key.h"
1595union __anonunion_type_data_159 {
1596 struct list_head link ;
1597 unsigned long x[2U] ;
1598 void *p[2U] ;
1599 int reject_error ;
1600};
1601#line 115 "include/linux/key.h"
1602union __anonunion_payload_160 {
1603 unsigned long value ;
1604 void *rcudata ;
1605 void *data ;
1606 struct keyring_list *subscriptions ;
1607};
1608#line 115 "include/linux/key.h"
1609struct key {
1610 atomic_t usage ;
1611 key_serial_t serial ;
1612 struct rb_node serial_node ;
1613 struct key_type *type ;
1614 struct rw_semaphore sem ;
1615 struct key_user *user ;
1616 void *security ;
1617 union __anonunion_ldv_15831_158 ldv_15831 ;
1618 uid_t uid ;
1619 gid_t gid ;
1620 key_perm_t perm ;
1621 unsigned short quotalen ;
1622 unsigned short datalen ;
1623 unsigned long flags ;
1624 char *description ;
1625 union __anonunion_type_data_159 type_data ;
1626 union __anonunion_payload_160 payload ;
1627};
1628#line 316
1629struct audit_context;
1630#line 316
1631struct audit_context;
1632#line 28 "include/linux/selinux.h"
1633struct group_info {
1634 atomic_t usage ;
1635 int ngroups ;
1636 int nblocks ;
1637 gid_t small_block[32U] ;
1638 gid_t *blocks[0U] ;
1639};
1640#line 77 "include/linux/cred.h"
1641struct thread_group_cred {
1642 atomic_t usage ;
1643 pid_t tgid ;
1644 spinlock_t lock ;
1645 struct key *session_keyring ;
1646 struct key *process_keyring ;
1647 struct rcu_head rcu ;
1648};
1649#line 91 "include/linux/cred.h"
1650struct cred {
1651 atomic_t usage ;
1652 atomic_t subscribers ;
1653 void *put_addr ;
1654 unsigned int magic ;
1655 uid_t uid ;
1656 gid_t gid ;
1657 uid_t suid ;
1658 gid_t sgid ;
1659 uid_t euid ;
1660 gid_t egid ;
1661 uid_t fsuid ;
1662 gid_t fsgid ;
1663 unsigned int securebits ;
1664 kernel_cap_t cap_inheritable ;
1665 kernel_cap_t cap_permitted ;
1666 kernel_cap_t cap_effective ;
1667 kernel_cap_t cap_bset ;
1668 unsigned char jit_keyring ;
1669 struct key *thread_keyring ;
1670 struct key *request_key_auth ;
1671 struct thread_group_cred *tgcred ;
1672 void *security ;
1673 struct user_struct *user ;
1674 struct user_namespace *user_ns ;
1675 struct group_info *group_info ;
1676 struct rcu_head rcu ;
1677};
1678#line 264
1679struct llist_node;
1680#line 64 "include/linux/llist.h"
1681struct llist_node {
1682 struct llist_node *next ;
1683};
1684#line 185
1685struct futex_pi_state;
1686#line 185
1687struct futex_pi_state;
1688#line 186
1689struct robust_list_head;
1690#line 186
1691struct robust_list_head;
1692#line 187
1693struct bio_list;
1694#line 187
1695struct bio_list;
1696#line 188
1697struct fs_struct;
1698#line 188
1699struct fs_struct;
1700#line 189
1701struct perf_event_context;
1702#line 189
1703struct perf_event_context;
1704#line 190
1705struct blk_plug;
1706#line 190
1707struct blk_plug;
1708#line 149 "include/linux/sched.h"
1709struct cfs_rq;
1710#line 149
1711struct cfs_rq;
1712#line 21 "include/linux/uio.h"
1713struct kvec {
1714 void *iov_base ;
1715 size_t iov_len ;
1716};
1717#line 406 "include/linux/sched.h"
1718struct sighand_struct {
1719 atomic_t count ;
1720 struct k_sigaction action[64U] ;
1721 spinlock_t siglock ;
1722 wait_queue_head_t signalfd_wqh ;
1723};
1724#line 449 "include/linux/sched.h"
1725struct pacct_struct {
1726 int ac_flag ;
1727 long ac_exitcode ;
1728 unsigned long ac_mem ;
1729 cputime_t ac_utime ;
1730 cputime_t ac_stime ;
1731 unsigned long ac_minflt ;
1732 unsigned long ac_majflt ;
1733};
1734#line 457 "include/linux/sched.h"
1735struct cpu_itimer {
1736 cputime_t expires ;
1737 cputime_t incr ;
1738 u32 error ;
1739 u32 incr_error ;
1740};
1741#line 464 "include/linux/sched.h"
1742struct task_cputime {
1743 cputime_t utime ;
1744 cputime_t stime ;
1745 unsigned long long sum_exec_runtime ;
1746};
1747#line 481 "include/linux/sched.h"
1748struct thread_group_cputimer {
1749 struct task_cputime cputime ;
1750 int running ;
1751 raw_spinlock_t lock ;
1752};
1753#line 517
1754struct autogroup;
1755#line 517
1756struct autogroup;
1757#line 518
1758struct taskstats;
1759#line 518
1760struct tty_audit_buf;
1761#line 518 "include/linux/sched.h"
1762struct signal_struct {
1763 atomic_t sigcnt ;
1764 atomic_t live ;
1765 int nr_threads ;
1766 wait_queue_head_t wait_chldexit ;
1767 struct task_struct *curr_target ;
1768 struct sigpending shared_pending ;
1769 int group_exit_code ;
1770 int notify_count ;
1771 struct task_struct *group_exit_task ;
1772 int group_stop_count ;
1773 unsigned int flags ;
1774 unsigned char is_child_subreaper : 1 ;
1775 unsigned char has_child_subreaper : 1 ;
1776 struct list_head posix_timers ;
1777 struct hrtimer real_timer ;
1778 struct pid *leader_pid ;
1779 ktime_t it_real_incr ;
1780 struct cpu_itimer it[2U] ;
1781 struct thread_group_cputimer cputimer ;
1782 struct task_cputime cputime_expires ;
1783 struct list_head cpu_timers[3U] ;
1784 struct pid *tty_old_pgrp ;
1785 int leader ;
1786 struct tty_struct *tty ;
1787 struct autogroup *autogroup ;
1788 cputime_t utime ;
1789 cputime_t stime ;
1790 cputime_t cutime ;
1791 cputime_t cstime ;
1792 cputime_t gtime ;
1793 cputime_t cgtime ;
1794 cputime_t prev_utime ;
1795 cputime_t prev_stime ;
1796 unsigned long nvcsw ;
1797 unsigned long nivcsw ;
1798 unsigned long cnvcsw ;
1799 unsigned long cnivcsw ;
1800 unsigned long min_flt ;
1801 unsigned long maj_flt ;
1802 unsigned long cmin_flt ;
1803 unsigned long cmaj_flt ;
1804 unsigned long inblock ;
1805 unsigned long oublock ;
1806 unsigned long cinblock ;
1807 unsigned long coublock ;
1808 unsigned long maxrss ;
1809 unsigned long cmaxrss ;
1810 struct task_io_accounting ioac ;
1811 unsigned long long sum_sched_runtime ;
1812 struct rlimit rlim[16U] ;
1813 struct pacct_struct pacct ;
1814 struct taskstats *stats ;
1815 unsigned int audit_tty ;
1816 struct tty_audit_buf *tty_audit_buf ;
1817 struct rw_semaphore group_rwsem ;
1818 int oom_adj ;
1819 int oom_score_adj ;
1820 int oom_score_adj_min ;
1821 struct mutex cred_guard_mutex ;
1822};
1823#line 699 "include/linux/sched.h"
1824struct user_struct {
1825 atomic_t __count ;
1826 atomic_t processes ;
1827 atomic_t files ;
1828 atomic_t sigpending ;
1829 atomic_t inotify_watches ;
1830 atomic_t inotify_devs ;
1831 atomic_t fanotify_listeners ;
1832 atomic_long_t epoll_watches ;
1833 unsigned long mq_bytes ;
1834 unsigned long locked_shm ;
1835 struct key *uid_keyring ;
1836 struct key *session_keyring ;
1837 struct hlist_node uidhash_node ;
1838 uid_t uid ;
1839 struct user_namespace *user_ns ;
1840 atomic_long_t locked_vm ;
1841};
1842#line 744
1843struct backing_dev_info;
1844#line 744
1845struct backing_dev_info;
1846#line 745
1847struct reclaim_state;
1848#line 745
1849struct reclaim_state;
1850#line 746 "include/linux/sched.h"
1851struct sched_info {
1852 unsigned long pcount ;
1853 unsigned long long run_delay ;
1854 unsigned long long last_arrival ;
1855 unsigned long long last_queued ;
1856};
1857#line 760 "include/linux/sched.h"
1858struct task_delay_info {
1859 spinlock_t lock ;
1860 unsigned int flags ;
1861 struct timespec blkio_start ;
1862 struct timespec blkio_end ;
1863 u64 blkio_delay ;
1864 u64 swapin_delay ;
1865 u32 blkio_count ;
1866 u32 swapin_count ;
1867 struct timespec freepages_start ;
1868 struct timespec freepages_end ;
1869 u64 freepages_delay ;
1870 u32 freepages_count ;
1871};
1872#line 1069
1873struct io_context;
1874#line 1069
1875struct io_context;
1876#line 1097
1877struct pipe_inode_info;
1878#line 1097
1879struct pipe_inode_info;
1880#line 1099
1881struct rq;
1882#line 1099
1883struct rq;
1884#line 1100 "include/linux/sched.h"
1885struct sched_class {
1886 struct sched_class const *next ;
1887 void (*enqueue_task)(struct rq * , struct task_struct * , int ) ;
1888 void (*dequeue_task)(struct rq * , struct task_struct * , int ) ;
1889 void (*yield_task)(struct rq * ) ;
1890 bool (*yield_to_task)(struct rq * , struct task_struct * , bool ) ;
1891 void (*check_preempt_curr)(struct rq * , struct task_struct * , int ) ;
1892 struct task_struct *(*pick_next_task)(struct rq * ) ;
1893 void (*put_prev_task)(struct rq * , struct task_struct * ) ;
1894 int (*select_task_rq)(struct task_struct * , int , int ) ;
1895 void (*pre_schedule)(struct rq * , struct task_struct * ) ;
1896 void (*post_schedule)(struct rq * ) ;
1897 void (*task_waking)(struct task_struct * ) ;
1898 void (*task_woken)(struct rq * , struct task_struct * ) ;
1899 void (*set_cpus_allowed)(struct task_struct * , struct cpumask const * ) ;
1900 void (*rq_online)(struct rq * ) ;
1901 void (*rq_offline)(struct rq * ) ;
1902 void (*set_curr_task)(struct rq * ) ;
1903 void (*task_tick)(struct rq * , struct task_struct * , int ) ;
1904 void (*task_fork)(struct task_struct * ) ;
1905 void (*switched_from)(struct rq * , struct task_struct * ) ;
1906 void (*switched_to)(struct rq * , struct task_struct * ) ;
1907 void (*prio_changed)(struct rq * , struct task_struct * , int ) ;
1908 unsigned int (*get_rr_interval)(struct rq * , struct task_struct * ) ;
1909 void (*task_move_group)(struct task_struct * , int ) ;
1910};
1911#line 1165 "include/linux/sched.h"
1912struct load_weight {
1913 unsigned long weight ;
1914 unsigned long inv_weight ;
1915};
1916#line 1170 "include/linux/sched.h"
1917struct sched_statistics {
1918 u64 wait_start ;
1919 u64 wait_max ;
1920 u64 wait_count ;
1921 u64 wait_sum ;
1922 u64 iowait_count ;
1923 u64 iowait_sum ;
1924 u64 sleep_start ;
1925 u64 sleep_max ;
1926 s64 sum_sleep_runtime ;
1927 u64 block_start ;
1928 u64 block_max ;
1929 u64 exec_max ;
1930 u64 slice_max ;
1931 u64 nr_migrations_cold ;
1932 u64 nr_failed_migrations_affine ;
1933 u64 nr_failed_migrations_running ;
1934 u64 nr_failed_migrations_hot ;
1935 u64 nr_forced_migrations ;
1936 u64 nr_wakeups ;
1937 u64 nr_wakeups_sync ;
1938 u64 nr_wakeups_migrate ;
1939 u64 nr_wakeups_local ;
1940 u64 nr_wakeups_remote ;
1941 u64 nr_wakeups_affine ;
1942 u64 nr_wakeups_affine_attempts ;
1943 u64 nr_wakeups_passive ;
1944 u64 nr_wakeups_idle ;
1945};
1946#line 1205 "include/linux/sched.h"
1947struct sched_entity {
1948 struct load_weight load ;
1949 struct rb_node run_node ;
1950 struct list_head group_node ;
1951 unsigned int on_rq ;
1952 u64 exec_start ;
1953 u64 sum_exec_runtime ;
1954 u64 vruntime ;
1955 u64 prev_sum_exec_runtime ;
1956 u64 nr_migrations ;
1957 struct sched_statistics statistics ;
1958 struct sched_entity *parent ;
1959 struct cfs_rq *cfs_rq ;
1960 struct cfs_rq *my_q ;
1961};
1962#line 1231
1963struct rt_rq;
1964#line 1231 "include/linux/sched.h"
1965struct sched_rt_entity {
1966 struct list_head run_list ;
1967 unsigned long timeout ;
1968 unsigned int time_slice ;
1969 int nr_cpus_allowed ;
1970 struct sched_rt_entity *back ;
1971 struct sched_rt_entity *parent ;
1972 struct rt_rq *rt_rq ;
1973 struct rt_rq *my_q ;
1974};
1975#line 1255
1976struct mem_cgroup;
1977#line 1255 "include/linux/sched.h"
1978struct memcg_batch_info {
1979 int do_batch ;
1980 struct mem_cgroup *memcg ;
1981 unsigned long nr_pages ;
1982 unsigned long memsw_nr_pages ;
1983};
1984#line 1616
1985struct files_struct;
1986#line 1616
1987struct css_set;
1988#line 1616
1989struct compat_robust_list_head;
1990#line 1616 "include/linux/sched.h"
1991struct task_struct {
1992 long volatile state ;
1993 void *stack ;
1994 atomic_t usage ;
1995 unsigned int flags ;
1996 unsigned int ptrace ;
1997 struct llist_node wake_entry ;
1998 int on_cpu ;
1999 int on_rq ;
2000 int prio ;
2001 int static_prio ;
2002 int normal_prio ;
2003 unsigned int rt_priority ;
2004 struct sched_class const *sched_class ;
2005 struct sched_entity se ;
2006 struct sched_rt_entity rt ;
2007 struct hlist_head preempt_notifiers ;
2008 unsigned char fpu_counter ;
2009 unsigned int policy ;
2010 cpumask_t cpus_allowed ;
2011 struct sched_info sched_info ;
2012 struct list_head tasks ;
2013 struct plist_node pushable_tasks ;
2014 struct mm_struct *mm ;
2015 struct mm_struct *active_mm ;
2016 unsigned char brk_randomized : 1 ;
2017 int exit_state ;
2018 int exit_code ;
2019 int exit_signal ;
2020 int pdeath_signal ;
2021 unsigned int jobctl ;
2022 unsigned int personality ;
2023 unsigned char did_exec : 1 ;
2024 unsigned char in_execve : 1 ;
2025 unsigned char in_iowait : 1 ;
2026 unsigned char sched_reset_on_fork : 1 ;
2027 unsigned char sched_contributes_to_load : 1 ;
2028 unsigned char irq_thread : 1 ;
2029 pid_t pid ;
2030 pid_t tgid ;
2031 unsigned long stack_canary ;
2032 struct task_struct *real_parent ;
2033 struct task_struct *parent ;
2034 struct list_head children ;
2035 struct list_head sibling ;
2036 struct task_struct *group_leader ;
2037 struct list_head ptraced ;
2038 struct list_head ptrace_entry ;
2039 struct pid_link pids[3U] ;
2040 struct list_head thread_group ;
2041 struct completion *vfork_done ;
2042 int *set_child_tid ;
2043 int *clear_child_tid ;
2044 cputime_t utime ;
2045 cputime_t stime ;
2046 cputime_t utimescaled ;
2047 cputime_t stimescaled ;
2048 cputime_t gtime ;
2049 cputime_t prev_utime ;
2050 cputime_t prev_stime ;
2051 unsigned long nvcsw ;
2052 unsigned long nivcsw ;
2053 struct timespec start_time ;
2054 struct timespec real_start_time ;
2055 unsigned long min_flt ;
2056 unsigned long maj_flt ;
2057 struct task_cputime cputime_expires ;
2058 struct list_head cpu_timers[3U] ;
2059 struct cred const *real_cred ;
2060 struct cred const *cred ;
2061 struct cred *replacement_session_keyring ;
2062 char comm[16U] ;
2063 int link_count ;
2064 int total_link_count ;
2065 struct sysv_sem sysvsem ;
2066 unsigned long last_switch_count ;
2067 struct thread_struct thread ;
2068 struct fs_struct *fs ;
2069 struct files_struct *files ;
2070 struct nsproxy *nsproxy ;
2071 struct signal_struct *signal ;
2072 struct sighand_struct *sighand ;
2073 sigset_t blocked ;
2074 sigset_t real_blocked ;
2075 sigset_t saved_sigmask ;
2076 struct sigpending pending ;
2077 unsigned long sas_ss_sp ;
2078 size_t sas_ss_size ;
2079 int (*notifier)(void * ) ;
2080 void *notifier_data ;
2081 sigset_t *notifier_mask ;
2082 struct audit_context *audit_context ;
2083 uid_t loginuid ;
2084 unsigned int sessionid ;
2085 seccomp_t seccomp ;
2086 u32 parent_exec_id ;
2087 u32 self_exec_id ;
2088 spinlock_t alloc_lock ;
2089 raw_spinlock_t pi_lock ;
2090 struct plist_head pi_waiters ;
2091 struct rt_mutex_waiter *pi_blocked_on ;
2092 struct mutex_waiter *blocked_on ;
2093 unsigned int irq_events ;
2094 unsigned long hardirq_enable_ip ;
2095 unsigned long hardirq_disable_ip ;
2096 unsigned int hardirq_enable_event ;
2097 unsigned int hardirq_disable_event ;
2098 int hardirqs_enabled ;
2099 int hardirq_context ;
2100 unsigned long softirq_disable_ip ;
2101 unsigned long softirq_enable_ip ;
2102 unsigned int softirq_disable_event ;
2103 unsigned int softirq_enable_event ;
2104 int softirqs_enabled ;
2105 int softirq_context ;
2106 u64 curr_chain_key ;
2107 int lockdep_depth ;
2108 unsigned int lockdep_recursion ;
2109 struct held_lock held_locks[48U] ;
2110 gfp_t lockdep_reclaim_gfp ;
2111 void *journal_info ;
2112 struct bio_list *bio_list ;
2113 struct blk_plug *plug ;
2114 struct reclaim_state *reclaim_state ;
2115 struct backing_dev_info *backing_dev_info ;
2116 struct io_context *io_context ;
2117 unsigned long ptrace_message ;
2118 siginfo_t *last_siginfo ;
2119 struct task_io_accounting ioac ;
2120 u64 acct_rss_mem1 ;
2121 u64 acct_vm_mem1 ;
2122 cputime_t acct_timexpd ;
2123 nodemask_t mems_allowed ;
2124 seqcount_t mems_allowed_seq ;
2125 int cpuset_mem_spread_rotor ;
2126 int cpuset_slab_spread_rotor ;
2127 struct css_set *cgroups ;
2128 struct list_head cg_list ;
2129 struct robust_list_head *robust_list ;
2130 struct compat_robust_list_head *compat_robust_list ;
2131 struct list_head pi_state_list ;
2132 struct futex_pi_state *pi_state_cache ;
2133 struct perf_event_context *perf_event_ctxp[2U] ;
2134 struct mutex perf_event_mutex ;
2135 struct list_head perf_event_list ;
2136 struct mempolicy *mempolicy ;
2137 short il_next ;
2138 short pref_node_fork ;
2139 struct rcu_head rcu ;
2140 struct pipe_inode_info *splice_pipe ;
2141 struct task_delay_info *delays ;
2142 int make_it_fail ;
2143 int nr_dirtied ;
2144 int nr_dirtied_pause ;
2145 unsigned long dirty_paused_when ;
2146 int latency_record_count ;
2147 struct latency_record latency_record[32U] ;
2148 unsigned long timer_slack_ns ;
2149 unsigned long default_timer_slack_ns ;
2150 struct list_head *scm_work_list ;
2151 unsigned long trace ;
2152 unsigned long trace_recursion ;
2153 struct memcg_batch_info memcg_batch ;
2154 atomic_t ptrace_bp_refcnt ;
2155};
2156#line 41 "include/asm-generic/sections.h"
2157struct exception_table_entry {
2158 unsigned long insn ;
2159 unsigned long fixup ;
2160};
2161#line 702 "include/linux/interrupt.h"
2162struct klist_node;
2163#line 702
2164struct klist_node;
2165#line 37 "include/linux/klist.h"
2166struct klist_node {
2167 void *n_klist ;
2168 struct list_head n_node ;
2169 struct kref n_ref ;
2170};
2171#line 67
2172struct dma_map_ops;
2173#line 67 "include/linux/klist.h"
2174struct dev_archdata {
2175 void *acpi_handle ;
2176 struct dma_map_ops *dma_ops ;
2177 void *iommu ;
2178};
2179#line 17 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
2180struct device_private;
2181#line 17
2182struct device_private;
2183#line 18
2184struct device_driver;
2185#line 18
2186struct device_driver;
2187#line 19
2188struct driver_private;
2189#line 19
2190struct driver_private;
2191#line 20
2192struct class;
2193#line 20
2194struct class;
2195#line 21
2196struct subsys_private;
2197#line 21
2198struct subsys_private;
2199#line 22
2200struct bus_type;
2201#line 22
2202struct bus_type;
2203#line 23
2204struct device_node;
2205#line 23
2206struct device_node;
2207#line 24
2208struct iommu_ops;
2209#line 24
2210struct iommu_ops;
2211#line 25 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
2212struct bus_attribute {
2213 struct attribute attr ;
2214 ssize_t (*show)(struct bus_type * , char * ) ;
2215 ssize_t (*store)(struct bus_type * , char const * , size_t ) ;
2216};
2217#line 51 "include/linux/device.h"
2218struct device_attribute;
2219#line 51
2220struct driver_attribute;
2221#line 51 "include/linux/device.h"
2222struct bus_type {
2223 char const *name ;
2224 char const *dev_name ;
2225 struct device *dev_root ;
2226 struct bus_attribute *bus_attrs ;
2227 struct device_attribute *dev_attrs ;
2228 struct driver_attribute *drv_attrs ;
2229 int (*match)(struct device * , struct device_driver * ) ;
2230 int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
2231 int (*probe)(struct device * ) ;
2232 int (*remove)(struct device * ) ;
2233 void (*shutdown)(struct device * ) ;
2234 int (*suspend)(struct device * , pm_message_t ) ;
2235 int (*resume)(struct device * ) ;
2236 struct dev_pm_ops const *pm ;
2237 struct iommu_ops *iommu_ops ;
2238 struct subsys_private *p ;
2239};
2240#line 125
2241struct device_type;
2242#line 182
2243struct of_device_id;
2244#line 182 "include/linux/device.h"
2245struct device_driver {
2246 char const *name ;
2247 struct bus_type *bus ;
2248 struct module *owner ;
2249 char const *mod_name ;
2250 bool suppress_bind_attrs ;
2251 struct of_device_id const *of_match_table ;
2252 int (*probe)(struct device * ) ;
2253 int (*remove)(struct device * ) ;
2254 void (*shutdown)(struct device * ) ;
2255 int (*suspend)(struct device * , pm_message_t ) ;
2256 int (*resume)(struct device * ) ;
2257 struct attribute_group const **groups ;
2258 struct dev_pm_ops const *pm ;
2259 struct driver_private *p ;
2260};
2261#line 245 "include/linux/device.h"
2262struct driver_attribute {
2263 struct attribute attr ;
2264 ssize_t (*show)(struct device_driver * , char * ) ;
2265 ssize_t (*store)(struct device_driver * , char const * , size_t ) ;
2266};
2267#line 299
2268struct class_attribute;
2269#line 299 "include/linux/device.h"
2270struct class {
2271 char const *name ;
2272 struct module *owner ;
2273 struct class_attribute *class_attrs ;
2274 struct device_attribute *dev_attrs ;
2275 struct bin_attribute *dev_bin_attrs ;
2276 struct kobject *dev_kobj ;
2277 int (*dev_uevent)(struct device * , struct kobj_uevent_env * ) ;
2278 char *(*devnode)(struct device * , umode_t * ) ;
2279 void (*class_release)(struct class * ) ;
2280 void (*dev_release)(struct device * ) ;
2281 int (*suspend)(struct device * , pm_message_t ) ;
2282 int (*resume)(struct device * ) ;
2283 struct kobj_ns_type_operations const *ns_type ;
2284 void const *(*namespace)(struct device * ) ;
2285 struct dev_pm_ops const *pm ;
2286 struct subsys_private *p ;
2287};
2288#line 394 "include/linux/device.h"
2289struct class_attribute {
2290 struct attribute attr ;
2291 ssize_t (*show)(struct class * , struct class_attribute * , char * ) ;
2292 ssize_t (*store)(struct class * , struct class_attribute * , char const * , size_t ) ;
2293 void const *(*namespace)(struct class * , struct class_attribute const * ) ;
2294};
2295#line 447 "include/linux/device.h"
2296struct device_type {
2297 char const *name ;
2298 struct attribute_group const **groups ;
2299 int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
2300 char *(*devnode)(struct device * , umode_t * ) ;
2301 void (*release)(struct device * ) ;
2302 struct dev_pm_ops const *pm ;
2303};
2304#line 474 "include/linux/device.h"
2305struct device_attribute {
2306 struct attribute attr ;
2307 ssize_t (*show)(struct device * , struct device_attribute * , char * ) ;
2308 ssize_t (*store)(struct device * , struct device_attribute * , char const * ,
2309 size_t ) ;
2310};
2311#line 557 "include/linux/device.h"
2312struct device_dma_parameters {
2313 unsigned int max_segment_size ;
2314 unsigned long segment_boundary_mask ;
2315};
2316#line 567
2317struct dma_coherent_mem;
2318#line 567 "include/linux/device.h"
2319struct device {
2320 struct device *parent ;
2321 struct device_private *p ;
2322 struct kobject kobj ;
2323 char const *init_name ;
2324 struct device_type const *type ;
2325 struct mutex mutex ;
2326 struct bus_type *bus ;
2327 struct device_driver *driver ;
2328 void *platform_data ;
2329 struct dev_pm_info power ;
2330 struct dev_pm_domain *pm_domain ;
2331 int numa_node ;
2332 u64 *dma_mask ;
2333 u64 coherent_dma_mask ;
2334 struct device_dma_parameters *dma_parms ;
2335 struct list_head dma_pools ;
2336 struct dma_coherent_mem *dma_mem ;
2337 struct dev_archdata archdata ;
2338 struct device_node *of_node ;
2339 dev_t devt ;
2340 u32 id ;
2341 spinlock_t devres_lock ;
2342 struct list_head devres_head ;
2343 struct klist_node knode_class ;
2344 struct class *class ;
2345 struct attribute_group const **groups ;
2346 void (*release)(struct device * ) ;
2347};
2348#line 681 "include/linux/device.h"
2349struct wakeup_source {
2350 char const *name ;
2351 struct list_head entry ;
2352 spinlock_t lock ;
2353 struct timer_list timer ;
2354 unsigned long timer_expires ;
2355 ktime_t total_time ;
2356 ktime_t max_time ;
2357 ktime_t last_time ;
2358 unsigned long event_count ;
2359 unsigned long active_count ;
2360 unsigned long relax_count ;
2361 unsigned long hit_count ;
2362 unsigned char active : 1 ;
2363};
2364#line 142 "include/mtd/mtd-abi.h"
2365struct otp_info {
2366 __u32 start ;
2367 __u32 length ;
2368 __u32 locked ;
2369};
2370#line 216 "include/mtd/mtd-abi.h"
2371struct nand_oobfree {
2372 __u32 offset ;
2373 __u32 length ;
2374};
2375#line 238 "include/mtd/mtd-abi.h"
2376struct mtd_ecc_stats {
2377 __u32 corrected ;
2378 __u32 failed ;
2379 __u32 badblocks ;
2380 __u32 bbtblocks ;
2381};
2382#line 260
2383struct mtd_info;
2384#line 260 "include/mtd/mtd-abi.h"
2385struct erase_info {
2386 struct mtd_info *mtd ;
2387 uint64_t addr ;
2388 uint64_t len ;
2389 uint64_t fail_addr ;
2390 u_long time ;
2391 u_long retries ;
2392 unsigned int dev ;
2393 unsigned int cell ;
2394 void (*callback)(struct erase_info * ) ;
2395 u_long priv ;
2396 u_char state ;
2397 struct erase_info *next ;
2398};
2399#line 62 "include/linux/mtd/mtd.h"
2400struct mtd_erase_region_info {
2401 uint64_t offset ;
2402 uint32_t erasesize ;
2403 uint32_t numblocks ;
2404 unsigned long *lockmap ;
2405};
2406#line 69 "include/linux/mtd/mtd.h"
2407struct mtd_oob_ops {
2408 unsigned int mode ;
2409 size_t len ;
2410 size_t retlen ;
2411 size_t ooblen ;
2412 size_t oobretlen ;
2413 uint32_t ooboffs ;
2414 uint8_t *datbuf ;
2415 uint8_t *oobbuf ;
2416};
2417#line 99 "include/linux/mtd/mtd.h"
2418struct nand_ecclayout {
2419 __u32 eccbytes ;
2420 __u32 eccpos[448U] ;
2421 __u32 oobavail ;
2422 struct nand_oobfree oobfree[32U] ;
2423};
2424#line 114 "include/linux/mtd/mtd.h"
2425struct mtd_info {
2426 u_char type ;
2427 uint32_t flags ;
2428 uint64_t size ;
2429 uint32_t erasesize ;
2430 uint32_t writesize ;
2431 uint32_t writebufsize ;
2432 uint32_t oobsize ;
2433 uint32_t oobavail ;
2434 unsigned int erasesize_shift ;
2435 unsigned int writesize_shift ;
2436 unsigned int erasesize_mask ;
2437 unsigned int writesize_mask ;
2438 char const *name ;
2439 int index ;
2440 struct nand_ecclayout *ecclayout ;
2441 unsigned int ecc_strength ;
2442 int numeraseregions ;
2443 struct mtd_erase_region_info *eraseregions ;
2444 int (*_erase)(struct mtd_info * , struct erase_info * ) ;
2445 int (*_point)(struct mtd_info * , loff_t , size_t , size_t * , void ** , resource_size_t * ) ;
2446 int (*_unpoint)(struct mtd_info * , loff_t , size_t ) ;
2447 unsigned long (*_get_unmapped_area)(struct mtd_info * , unsigned long , unsigned long ,
2448 unsigned long ) ;
2449 int (*_read)(struct mtd_info * , loff_t , size_t , size_t * , u_char * ) ;
2450 int (*_write)(struct mtd_info * , loff_t , size_t , size_t * , u_char const * ) ;
2451 int (*_panic_write)(struct mtd_info * , loff_t , size_t , size_t * , u_char const * ) ;
2452 int (*_read_oob)(struct mtd_info * , loff_t , struct mtd_oob_ops * ) ;
2453 int (*_write_oob)(struct mtd_info * , loff_t , struct mtd_oob_ops * ) ;
2454 int (*_get_fact_prot_info)(struct mtd_info * , struct otp_info * , size_t ) ;
2455 int (*_read_fact_prot_reg)(struct mtd_info * , loff_t , size_t , size_t * , u_char * ) ;
2456 int (*_get_user_prot_info)(struct mtd_info * , struct otp_info * , size_t ) ;
2457 int (*_read_user_prot_reg)(struct mtd_info * , loff_t , size_t , size_t * , u_char * ) ;
2458 int (*_write_user_prot_reg)(struct mtd_info * , loff_t , size_t , size_t * ,
2459 u_char * ) ;
2460 int (*_lock_user_prot_reg)(struct mtd_info * , loff_t , size_t ) ;
2461 int (*_writev)(struct mtd_info * , struct kvec const * , unsigned long , loff_t ,
2462 size_t * ) ;
2463 void (*_sync)(struct mtd_info * ) ;
2464 int (*_lock)(struct mtd_info * , loff_t , uint64_t ) ;
2465 int (*_unlock)(struct mtd_info * , loff_t , uint64_t ) ;
2466 int (*_is_locked)(struct mtd_info * , loff_t , uint64_t ) ;
2467 int (*_block_isbad)(struct mtd_info * , loff_t ) ;
2468 int (*_block_markbad)(struct mtd_info * , loff_t ) ;
2469 int (*_suspend)(struct mtd_info * ) ;
2470 void (*_resume)(struct mtd_info * ) ;
2471 int (*_get_device)(struct mtd_info * ) ;
2472 void (*_put_device)(struct mtd_info * ) ;
2473 struct backing_dev_info *backing_dev_info ;
2474 struct notifier_block reboot_notifier ;
2475 struct mtd_ecc_stats ecc_stats ;
2476 int subpage_sft ;
2477 void *priv ;
2478 struct module *owner ;
2479 struct device dev ;
2480 int usecount ;
2481};
2482#line 375 "include/linux/mtd/mtd.h"
2483struct mtd_notifier {
2484 void (*add)(struct mtd_info * ) ;
2485 void (*remove)(struct mtd_info * ) ;
2486 struct list_head list ;
2487};
2488#line 401
2489enum kmsg_dump_reason {
2490 KMSG_DUMP_PANIC = 0,
2491 KMSG_DUMP_OOPS = 1,
2492 KMSG_DUMP_EMERG = 2,
2493 KMSG_DUMP_RESTART = 3,
2494 KMSG_DUMP_HALT = 4,
2495 KMSG_DUMP_POWEROFF = 5
2496} ;
2497#line 410 "include/linux/mtd/mtd.h"
2498struct kmsg_dumper {
2499 void (*dump)(struct kmsg_dumper * , enum kmsg_dump_reason , char const * , unsigned long ,
2500 char const * , unsigned long ) ;
2501 struct list_head list ;
2502 int registered ;
2503};
2504#line 71 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
2505struct mtdoops_context {
2506 struct kmsg_dumper dump ;
2507 int mtd_index ;
2508 struct work_struct work_erase ;
2509 struct work_struct work_write ;
2510 struct mtd_info *mtd ;
2511 int oops_pages ;
2512 int nextpage ;
2513 int nextcount ;
2514 unsigned long *oops_page_used ;
2515 void *oops_buf ;
2516};
2517#line 1 "<compiler builtins>"
2518
2519#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
2520void ldv_spin_lock(void) ;
2521#line 3
2522void ldv_spin_unlock(void) ;
2523#line 4
2524int ldv_spin_trylock(void) ;
2525#line 60 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/bitops.h"
2526__inline static void set_bit(unsigned int nr , unsigned long volatile *addr )
2527{ long volatile *__cil_tmp3 ;
2528
2529 {
2530#line 68
2531 __cil_tmp3 = (long volatile *)addr;
2532#line 68
2533 __asm__ volatile (".section .smp_locks,\"a\"\n.balign 4\n.long 671f - .\n.previous\n671:\n\tlock; bts %1,%0": "+m" (*__cil_tmp3): "Ir" (nr): "memory");
2534#line 70
2535 return;
2536}
2537}
2538#line 98 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/bitops.h"
2539__inline static void clear_bit(int nr , unsigned long volatile *addr )
2540{ long volatile *__cil_tmp3 ;
2541
2542 {
2543#line 105
2544 __cil_tmp3 = (long volatile *)addr;
2545#line 105
2546 __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));
2547#line 107
2548 return;
2549}
2550}
2551#line 315 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/bitops.h"
2552__inline static int variable_test_bit(int nr , unsigned long const volatile *addr )
2553{ int oldbit ;
2554 unsigned long *__cil_tmp4 ;
2555
2556 {
2557#line 319
2558 __cil_tmp4 = (unsigned long *)addr;
2559#line 319
2560 __asm__ volatile ("bt %2,%1\n\tsbb %0,%0": "=r" (oldbit): "m" (*__cil_tmp4),
2561 "Ir" (nr));
2562#line 324
2563 return (oldbit);
2564}
2565}
2566#line 101 "include/linux/printk.h"
2567extern int printk(char const * , ...) ;
2568#line 307 "include/linux/kernel.h"
2569extern unsigned long simple_strtoul(char const * , char ** , unsigned int ) ;
2570#line 24 "include/linux/list.h"
2571__inline static void INIT_LIST_HEAD(struct list_head *list )
2572{ unsigned long __cil_tmp2 ;
2573 unsigned long __cil_tmp3 ;
2574
2575 {
2576#line 26
2577 *((struct list_head **)list) = list;
2578#line 27
2579 __cil_tmp2 = (unsigned long )list;
2580#line 27
2581 __cil_tmp3 = __cil_tmp2 + 8;
2582#line 27
2583 *((struct list_head **)__cil_tmp3) = list;
2584#line 28
2585 return;
2586}
2587}
2588#line 88 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/percpu.h"
2589extern void __bad_percpu_size(void) ;
2590#line 10 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
2591extern struct task_struct *current_task ;
2592#line 12 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
2593__inline static struct task_struct *get_current(void)
2594{ struct task_struct *pfo_ret__ ;
2595
2596 {
2597#line 14
2598 if (8 == 1) {
2599#line 14
2600 goto case_1;
2601 } else
2602#line 14
2603 if (8 == 2) {
2604#line 14
2605 goto case_2;
2606 } else
2607#line 14
2608 if (8 == 4) {
2609#line 14
2610 goto case_4;
2611 } else
2612#line 14
2613 if (8 == 8) {
2614#line 14
2615 goto case_8;
2616 } else {
2617 {
2618#line 14
2619 goto switch_default;
2620#line 14
2621 if (0) {
2622 case_1:
2623#line 14
2624 __asm__ ("movb %%gs:%P1,%0": "=q" (pfo_ret__): "p" (& current_task));
2625#line 14
2626 goto ldv_2918;
2627 case_2:
2628#line 14
2629 __asm__ ("movw %%gs:%P1,%0": "=r" (pfo_ret__): "p" (& current_task));
2630#line 14
2631 goto ldv_2918;
2632 case_4:
2633#line 14
2634 __asm__ ("movl %%gs:%P1,%0": "=r" (pfo_ret__): "p" (& current_task));
2635#line 14
2636 goto ldv_2918;
2637 case_8:
2638#line 14
2639 __asm__ ("movq %%gs:%P1,%0": "=r" (pfo_ret__): "p" (& current_task));
2640#line 14
2641 goto ldv_2918;
2642 switch_default:
2643 {
2644#line 14
2645 __bad_percpu_size();
2646 }
2647 } else {
2648 switch_break: ;
2649 }
2650 }
2651 }
2652 ldv_2918: ;
2653#line 14
2654 return (pfo_ret__);
2655}
2656}
2657#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/string_64.h"
2658extern void *memset(void * , int , size_t ) ;
2659#line 61
2660extern size_t strlen(char const * ) ;
2661#line 64
2662extern int strcmp(char const * , char const * ) ;
2663#line 17 "include/linux/math64.h"
2664__inline static u64 div_u64_rem(u64 dividend , u32 divisor , u32 *remainder )
2665{ u64 __cil_tmp4 ;
2666 unsigned long long __cil_tmp5 ;
2667 u64 __cil_tmp6 ;
2668
2669 {
2670#line 19
2671 __cil_tmp4 = (u64 )divisor;
2672#line 19
2673 __cil_tmp5 = dividend % __cil_tmp4;
2674#line 19
2675 *remainder = (u32 )__cil_tmp5;
2676 {
2677#line 20
2678 __cil_tmp6 = (u64 )divisor;
2679#line 20
2680 return (dividend / __cil_tmp6);
2681 }
2682}
2683}
2684#line 82 "include/linux/math64.h"
2685__inline static u64 div_u64(u64 dividend , u32 divisor )
2686{ u32 remainder ;
2687 u64 tmp ;
2688
2689 {
2690 {
2691#line 85
2692 tmp = div_u64_rem(dividend, divisor, & remainder);
2693 }
2694#line 85
2695 return (tmp);
2696}
2697}
2698#line 11 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/cmpxchg.h"
2699extern void __xchg_wrong_size(void) ;
2700#line 261 "include/linux/lockdep.h"
2701extern void lockdep_init_map(struct lockdep_map * , char const * , struct lock_class_key * ,
2702 int ) ;
2703#line 29 "include/linux/wait.h"
2704extern int default_wake_function(wait_queue_t * , unsigned int , int , void * ) ;
2705#line 79
2706extern void __init_waitqueue_head(wait_queue_head_t * , char const * , struct lock_class_key * ) ;
2707#line 117
2708extern void add_wait_queue(wait_queue_head_t * , wait_queue_t * ) ;
2709#line 119
2710extern void remove_wait_queue(wait_queue_head_t * , wait_queue_t * ) ;
2711#line 155
2712extern void __wake_up(wait_queue_head_t * , unsigned int , int , void * ) ;
2713#line 156 "include/linux/workqueue.h"
2714extern void __init_work(struct work_struct * , int ) ;
2715#line 380
2716extern int schedule_work(struct work_struct * ) ;
2717#line 391
2718extern bool flush_work_sync(struct work_struct * ) ;
2719#line 54 "include/linux/vmalloc.h"
2720extern void *vmalloc(unsigned long ) ;
2721#line 57
2722void *ldv_vmalloc_19(unsigned long ldv_func_arg1 ) ;
2723#line 61
2724void *ldv_vmalloc_20(unsigned long ldv_func_arg1 ) ;
2725#line 74
2726extern void vfree(void const * ) ;
2727#line 220 "include/linux/slub_def.h"
2728extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t ) ;
2729#line 223
2730void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
2731#line 11 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
2732void ldv_check_alloc_flags(gfp_t flags ) ;
2733#line 12
2734void ldv_check_alloc_nonatomic(void) ;
2735#line 14
2736struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
2737#line 362 "include/linux/sched.h"
2738extern void schedule(void) ;
2739#line 246 "include/linux/mtd/mtd.h"
2740extern int mtd_erase(struct mtd_info * , struct erase_info * ) ;
2741#line 252
2742extern int mtd_read(struct mtd_info * , loff_t , size_t , size_t * , u_char * ) ;
2743#line 254
2744extern int mtd_write(struct mtd_info * , loff_t , size_t , size_t * , u_char const * ) ;
2745#line 256
2746extern int mtd_panic_write(struct mtd_info * , loff_t , size_t , size_t * , u_char const * ) ;
2747#line 303
2748extern int mtd_block_isbad(struct mtd_info * , loff_t ) ;
2749#line 304
2750extern int mtd_block_markbad(struct mtd_info * , loff_t ) ;
2751#line 317 "include/linux/mtd/mtd.h"
2752__inline static uint32_t mtd_div_by_eb(uint64_t sz , struct mtd_info *mtd )
2753{ uint32_t __base ;
2754 uint32_t __rem ;
2755 unsigned long __cil_tmp5 ;
2756 unsigned long __cil_tmp6 ;
2757 unsigned int __cil_tmp7 ;
2758 unsigned long __cil_tmp8 ;
2759 unsigned long __cil_tmp9 ;
2760 unsigned int __cil_tmp10 ;
2761 int __cil_tmp11 ;
2762 uint64_t __cil_tmp12 ;
2763 unsigned long __cil_tmp13 ;
2764 unsigned long __cil_tmp14 ;
2765 uint64_t __cil_tmp15 ;
2766 unsigned long long __cil_tmp16 ;
2767 uint64_t __cil_tmp17 ;
2768
2769 {
2770 {
2771#line 319
2772 __cil_tmp5 = (unsigned long )mtd;
2773#line 319
2774 __cil_tmp6 = __cil_tmp5 + 36;
2775#line 319
2776 __cil_tmp7 = *((unsigned int *)__cil_tmp6);
2777#line 319
2778 if (__cil_tmp7 != 0U) {
2779 {
2780#line 320
2781 __cil_tmp8 = (unsigned long )mtd;
2782#line 320
2783 __cil_tmp9 = __cil_tmp8 + 36;
2784#line 320
2785 __cil_tmp10 = *((unsigned int *)__cil_tmp9);
2786#line 320
2787 __cil_tmp11 = (int )__cil_tmp10;
2788#line 320
2789 __cil_tmp12 = sz >> __cil_tmp11;
2790#line 320
2791 return ((uint32_t )__cil_tmp12);
2792 }
2793 } else {
2794
2795 }
2796 }
2797#line 321
2798 __cil_tmp13 = (unsigned long )mtd;
2799#line 321
2800 __cil_tmp14 = __cil_tmp13 + 16;
2801#line 321
2802 __base = *((uint32_t *)__cil_tmp14);
2803#line 321
2804 __cil_tmp15 = (uint64_t )__base;
2805#line 321
2806 __cil_tmp16 = sz % __cil_tmp15;
2807#line 321
2808 __rem = (uint32_t )__cil_tmp16;
2809#line 321
2810 __cil_tmp17 = (uint64_t )__base;
2811#line 321
2812 sz = sz / __cil_tmp17;
2813#line 322
2814 return ((uint32_t )sz);
2815}
2816}
2817#line 384
2818extern void register_mtd_user(struct mtd_notifier * ) ;
2819#line 385
2820extern int unregister_mtd_user(struct mtd_notifier * ) ;
2821#line 390 "include/linux/mtd/mtd.h"
2822__inline static int mtd_is_bitflip(int err )
2823{
2824
2825 {
2826#line 391
2827 return (err == -117);
2828}
2829}
2830#line 51 "include/linux/kmsg_dump.h"
2831extern int kmsg_dump_register(struct kmsg_dumper * ) ;
2832#line 53
2833extern int kmsg_dump_unregister(struct kmsg_dumper * ) ;
2834#line 57 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
2835static unsigned long record_size = 4096UL;
2836#line 62 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
2837static char mtddev[80U] ;
2838#line 67 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
2839static int dump_oops = 1;
2840#line 85 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
2841static struct mtdoops_context oops_cxt ;
2842#line 87 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
2843static void mark_page_used(struct mtdoops_context *cxt , int page )
2844{ unsigned int __cil_tmp3 ;
2845 unsigned long __cil_tmp4 ;
2846 unsigned long __cil_tmp5 ;
2847 unsigned long *__cil_tmp6 ;
2848 unsigned long volatile *__cil_tmp7 ;
2849
2850 {
2851 {
2852#line 89
2853 __cil_tmp3 = (unsigned int )page;
2854#line 89
2855 __cil_tmp4 = (unsigned long )cxt;
2856#line 89
2857 __cil_tmp5 = __cil_tmp4 + 224;
2858#line 89
2859 __cil_tmp6 = *((unsigned long **)__cil_tmp5);
2860#line 89
2861 __cil_tmp7 = (unsigned long volatile *)__cil_tmp6;
2862#line 89
2863 set_bit(__cil_tmp3, __cil_tmp7);
2864 }
2865#line 90
2866 return;
2867}
2868}
2869#line 92 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
2870static void mark_page_unused(struct mtdoops_context *cxt , int page )
2871{ unsigned long __cil_tmp3 ;
2872 unsigned long __cil_tmp4 ;
2873 unsigned long *__cil_tmp5 ;
2874 unsigned long volatile *__cil_tmp6 ;
2875
2876 {
2877 {
2878#line 94
2879 __cil_tmp3 = (unsigned long )cxt;
2880#line 94
2881 __cil_tmp4 = __cil_tmp3 + 224;
2882#line 94
2883 __cil_tmp5 = *((unsigned long **)__cil_tmp4);
2884#line 94
2885 __cil_tmp6 = (unsigned long volatile *)__cil_tmp5;
2886#line 94
2887 clear_bit(page, __cil_tmp6);
2888 }
2889#line 95
2890 return;
2891}
2892}
2893#line 97 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
2894static int page_is_used(struct mtdoops_context *cxt , int page )
2895{ int tmp ;
2896 unsigned long __cil_tmp4 ;
2897 unsigned long __cil_tmp5 ;
2898 unsigned long *__cil_tmp6 ;
2899 unsigned long const volatile *__cil_tmp7 ;
2900
2901 {
2902 {
2903#line 99
2904 __cil_tmp4 = (unsigned long )cxt;
2905#line 99
2906 __cil_tmp5 = __cil_tmp4 + 224;
2907#line 99
2908 __cil_tmp6 = *((unsigned long **)__cil_tmp5);
2909#line 99
2910 __cil_tmp7 = (unsigned long const volatile *)__cil_tmp6;
2911#line 99
2912 tmp = variable_test_bit(page, __cil_tmp7);
2913 }
2914#line 99
2915 return (tmp);
2916}
2917}
2918#line 102 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
2919static void mtdoops_erase_callback(struct erase_info *done )
2920{ wait_queue_head_t *wait_q ;
2921 unsigned long __cil_tmp3 ;
2922 unsigned long __cil_tmp4 ;
2923 u_long __cil_tmp5 ;
2924 void *__cil_tmp6 ;
2925
2926 {
2927 {
2928#line 104
2929 __cil_tmp3 = (unsigned long )done;
2930#line 104
2931 __cil_tmp4 = __cil_tmp3 + 64;
2932#line 104
2933 __cil_tmp5 = *((u_long *)__cil_tmp4);
2934#line 104
2935 wait_q = (wait_queue_head_t *)__cil_tmp5;
2936#line 105
2937 __cil_tmp6 = (void *)0;
2938#line 105
2939 __wake_up(wait_q, 3U, 1, __cil_tmp6);
2940 }
2941#line 106
2942 return;
2943}
2944}
2945#line 108 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
2946static int mtdoops_erase_block(struct mtdoops_context *cxt , int offset )
2947{ struct mtd_info *mtd ;
2948 u32 start_page_offset ;
2949 uint32_t tmp ;
2950 u32 start_page ;
2951 u32 erase_pages ;
2952 struct erase_info erase ;
2953 wait_queue_t wait ;
2954 struct task_struct *tmp___0 ;
2955 wait_queue_head_t wait_q ;
2956 int ret ;
2957 int page ;
2958 struct lock_class_key __key ;
2959 long volatile __ret ;
2960 struct task_struct *tmp___1 ;
2961 struct task_struct *tmp___2 ;
2962 struct task_struct *tmp___3 ;
2963 struct task_struct *tmp___4 ;
2964 long volatile __ret___0 ;
2965 struct task_struct *tmp___5 ;
2966 struct task_struct *tmp___6 ;
2967 struct task_struct *tmp___7 ;
2968 struct task_struct *tmp___8 ;
2969 unsigned long __cil_tmp25 ;
2970 unsigned long __cil_tmp26 ;
2971 uint64_t __cil_tmp27 ;
2972 unsigned long __cil_tmp28 ;
2973 unsigned long __cil_tmp29 ;
2974 uint32_t __cil_tmp30 ;
2975 unsigned long *__cil_tmp31 ;
2976 unsigned long __cil_tmp32 ;
2977 unsigned long __cil_tmp33 ;
2978 unsigned long __cil_tmp34 ;
2979 unsigned long *__cil_tmp35 ;
2980 unsigned long __cil_tmp36 ;
2981 unsigned long __cil_tmp37 ;
2982 unsigned long __cil_tmp38 ;
2983 uint32_t __cil_tmp39 ;
2984 unsigned long __cil_tmp40 ;
2985 unsigned long __cil_tmp41 ;
2986 wait_queue_t *__cil_tmp42 ;
2987 unsigned long __cil_tmp43 ;
2988 unsigned long __cil_tmp44 ;
2989 unsigned long __cil_tmp45 ;
2990 unsigned long __cil_tmp46 ;
2991 unsigned long __cil_tmp47 ;
2992 struct erase_info *__cil_tmp48 ;
2993 unsigned long __cil_tmp49 ;
2994 unsigned long __cil_tmp50 ;
2995 unsigned long __cil_tmp51 ;
2996 unsigned long __cil_tmp52 ;
2997 unsigned long __cil_tmp53 ;
2998 uint32_t __cil_tmp54 ;
2999 unsigned long __cil_tmp55 ;
3000 unsigned long __cil_tmp56 ;
3001 uint64_t __cil_tmp57 ;
3002 unsigned long __cil_tmp58 ;
3003 uint64_t __cil_tmp59 ;
3004 char *__cil_tmp60 ;
3005 u32 __cil_tmp61 ;
3006 u32 __cil_tmp62 ;
3007
3008 {
3009 {
3010#line 110
3011 __cil_tmp25 = (unsigned long )cxt;
3012#line 110
3013 __cil_tmp26 = __cil_tmp25 + 200;
3014#line 110
3015 mtd = *((struct mtd_info **)__cil_tmp26);
3016#line 111
3017 __cil_tmp27 = (uint64_t )offset;
3018#line 111
3019 tmp = mtd_div_by_eb(__cil_tmp27, mtd);
3020#line 111
3021 __cil_tmp28 = (unsigned long )mtd;
3022#line 111
3023 __cil_tmp29 = __cil_tmp28 + 16;
3024#line 111
3025 __cil_tmp30 = *((uint32_t *)__cil_tmp29);
3026#line 111
3027 start_page_offset = tmp * __cil_tmp30;
3028#line 112
3029 __cil_tmp31 = & record_size;
3030#line 112
3031 __cil_tmp32 = *__cil_tmp31;
3032#line 112
3033 __cil_tmp33 = (unsigned long )start_page_offset;
3034#line 112
3035 __cil_tmp34 = __cil_tmp33 / __cil_tmp32;
3036#line 112
3037 start_page = (u32 )__cil_tmp34;
3038#line 113
3039 __cil_tmp35 = & record_size;
3040#line 113
3041 __cil_tmp36 = *__cil_tmp35;
3042#line 113
3043 __cil_tmp37 = (unsigned long )mtd;
3044#line 113
3045 __cil_tmp38 = __cil_tmp37 + 16;
3046#line 113
3047 __cil_tmp39 = *((uint32_t *)__cil_tmp38);
3048#line 113
3049 __cil_tmp40 = (unsigned long )__cil_tmp39;
3050#line 113
3051 __cil_tmp41 = __cil_tmp40 / __cil_tmp36;
3052#line 113
3053 erase_pages = (u32 )__cil_tmp41;
3054#line 115
3055 tmp___0 = get_current();
3056#line 115
3057 __cil_tmp42 = & wait;
3058#line 115
3059 *((unsigned int *)__cil_tmp42) = 0U;
3060#line 115
3061 __cil_tmp43 = (unsigned long )(& wait) + 8;
3062#line 115
3063 *((void **)__cil_tmp43) = (void *)tmp___0;
3064#line 115
3065 __cil_tmp44 = (unsigned long )(& wait) + 16;
3066#line 115
3067 *((int (**)(wait_queue_t * , unsigned int , int , void * ))__cil_tmp44) = & default_wake_function;
3068#line 115
3069 __cil_tmp45 = (unsigned long )(& wait) + 24;
3070#line 115
3071 *((struct list_head **)__cil_tmp45) = (struct list_head *)0;
3072#line 115
3073 __cil_tmp46 = 24 + 8;
3074#line 115
3075 __cil_tmp47 = (unsigned long )(& wait) + __cil_tmp46;
3076#line 115
3077 *((struct list_head **)__cil_tmp47) = (struct list_head *)0;
3078#line 120
3079 __init_waitqueue_head(& wait_q, "&wait_q", & __key);
3080#line 121
3081 __cil_tmp48 = & erase;
3082#line 121
3083 *((struct mtd_info **)__cil_tmp48) = mtd;
3084#line 122
3085 __cil_tmp49 = (unsigned long )(& erase) + 56;
3086#line 122
3087 *((void (**)(struct erase_info * ))__cil_tmp49) = & mtdoops_erase_callback;
3088#line 123
3089 __cil_tmp50 = (unsigned long )(& erase) + 8;
3090#line 123
3091 *((uint64_t *)__cil_tmp50) = (uint64_t )offset;
3092#line 124
3093 __cil_tmp51 = (unsigned long )(& erase) + 16;
3094#line 124
3095 __cil_tmp52 = (unsigned long )mtd;
3096#line 124
3097 __cil_tmp53 = __cil_tmp52 + 16;
3098#line 124
3099 __cil_tmp54 = *((uint32_t *)__cil_tmp53);
3100#line 124
3101 *((uint64_t *)__cil_tmp51) = (uint64_t )__cil_tmp54;
3102#line 125
3103 __cil_tmp55 = (unsigned long )(& erase) + 64;
3104#line 125
3105 *((u_long *)__cil_tmp55) = (unsigned long )(& wait_q);
3106#line 127
3107 __ret = (long volatile )1L;
3108 }
3109#line 127
3110 if (8 == 1) {
3111#line 127
3112 goto case_1;
3113 } else
3114#line 127
3115 if (8 == 2) {
3116#line 127
3117 goto case_2;
3118 } else
3119#line 127
3120 if (8 == 4) {
3121#line 127
3122 goto case_4;
3123 } else
3124#line 127
3125 if (8 == 8) {
3126#line 127
3127 goto case_8;
3128 } else {
3129 {
3130#line 127
3131 goto switch_default;
3132#line 127
3133 if (0) {
3134 case_1:
3135 {
3136#line 127
3137 tmp___1 = get_current();
3138#line 127
3139 __asm__ volatile ("xchgb %b0, %1\n": "+q" (__ret), "+m" (*((long volatile *)tmp___1)): : "memory",
3140 "cc");
3141 }
3142#line 127
3143 goto ldv_20346;
3144 case_2:
3145 {
3146#line 127
3147 tmp___2 = get_current();
3148#line 127
3149 __asm__ volatile ("xchgw %w0, %1\n": "+r" (__ret), "+m" (*((long volatile *)tmp___2)): : "memory",
3150 "cc");
3151 }
3152#line 127
3153 goto ldv_20346;
3154 case_4:
3155 {
3156#line 127
3157 tmp___3 = get_current();
3158#line 127
3159 __asm__ volatile ("xchgl %0, %1\n": "+r" (__ret), "+m" (*((long volatile *)tmp___3)): : "memory",
3160 "cc");
3161 }
3162#line 127
3163 goto ldv_20346;
3164 case_8:
3165 {
3166#line 127
3167 tmp___4 = get_current();
3168#line 127
3169 __asm__ volatile ("xchgq %q0, %1\n": "+r" (__ret), "+m" (*((long volatile *)tmp___4)): : "memory",
3170 "cc");
3171 }
3172#line 127
3173 goto ldv_20346;
3174 switch_default:
3175 {
3176#line 127
3177 __xchg_wrong_size();
3178 }
3179 } else {
3180 switch_break: ;
3181 }
3182 }
3183 }
3184 ldv_20346:
3185 {
3186#line 128
3187 add_wait_queue(& wait_q, & wait);
3188#line 130
3189 ret = mtd_erase(mtd, & erase);
3190 }
3191#line 131
3192 if (ret != 0) {
3193#line 132
3194 __ret___0 = (long volatile )0L;
3195#line 132
3196 if (8 == 1) {
3197#line 132
3198 goto case_1___0;
3199 } else
3200#line 132
3201 if (8 == 2) {
3202#line 132
3203 goto case_2___0;
3204 } else
3205#line 132
3206 if (8 == 4) {
3207#line 132
3208 goto case_4___0;
3209 } else
3210#line 132
3211 if (8 == 8) {
3212#line 132
3213 goto case_8___0;
3214 } else {
3215 {
3216#line 132
3217 goto switch_default___0;
3218#line 132
3219 if (0) {
3220 case_1___0:
3221 {
3222#line 132
3223 tmp___5 = get_current();
3224#line 132
3225 __asm__ volatile ("xchgb %b0, %1\n": "+q" (__ret___0), "+m" (*((long volatile *)tmp___5)): : "memory",
3226 "cc");
3227 }
3228#line 132
3229 goto ldv_20354;
3230 case_2___0:
3231 {
3232#line 132
3233 tmp___6 = get_current();
3234#line 132
3235 __asm__ volatile ("xchgw %w0, %1\n": "+r" (__ret___0), "+m" (*((long volatile *)tmp___6)): : "memory",
3236 "cc");
3237 }
3238#line 132
3239 goto ldv_20354;
3240 case_4___0:
3241 {
3242#line 132
3243 tmp___7 = get_current();
3244#line 132
3245 __asm__ volatile ("xchgl %0, %1\n": "+r" (__ret___0), "+m" (*((long volatile *)tmp___7)): : "memory",
3246 "cc");
3247 }
3248#line 132
3249 goto ldv_20354;
3250 case_8___0:
3251 {
3252#line 132
3253 tmp___8 = get_current();
3254#line 132
3255 __asm__ volatile ("xchgq %q0, %1\n": "+r" (__ret___0), "+m" (*((long volatile *)tmp___8)): : "memory",
3256 "cc");
3257 }
3258#line 132
3259 goto ldv_20354;
3260 switch_default___0:
3261 {
3262#line 132
3263 __xchg_wrong_size();
3264 }
3265 } else {
3266 switch_break___0: ;
3267 }
3268 }
3269 }
3270 ldv_20354:
3271 {
3272#line 133
3273 remove_wait_queue(& wait_q, & wait);
3274#line 134
3275 __cil_tmp56 = (unsigned long )(& erase) + 8;
3276#line 134
3277 __cil_tmp57 = *((uint64_t *)__cil_tmp56);
3278#line 134
3279 __cil_tmp58 = (unsigned long )(& erase) + 16;
3280#line 134
3281 __cil_tmp59 = *((uint64_t *)__cil_tmp58);
3282#line 134
3283 __cil_tmp60 = (char *)(& mtddev);
3284#line 134
3285 printk("<4>mtdoops: erase of region [0x%llx, 0x%llx] on \"%s\" failed\n", __cil_tmp57,
3286 __cil_tmp59, __cil_tmp60);
3287 }
3288#line 137
3289 return (ret);
3290 } else {
3291
3292 }
3293 {
3294#line 140
3295 schedule();
3296#line 141
3297 remove_wait_queue(& wait_q, & wait);
3298#line 144
3299 page = (int )start_page;
3300 }
3301#line 144
3302 goto ldv_20361;
3303 ldv_20360:
3304 {
3305#line 145
3306 mark_page_unused(cxt, page);
3307#line 144
3308 page = page + 1;
3309 }
3310 ldv_20361: ;
3311 {
3312#line 144
3313 __cil_tmp61 = start_page + erase_pages;
3314#line 144
3315 __cil_tmp62 = (u32 )page;
3316#line 144
3317 if (__cil_tmp62 < __cil_tmp61) {
3318#line 145
3319 goto ldv_20360;
3320 } else {
3321#line 147
3322 goto ldv_20362;
3323 }
3324 }
3325 ldv_20362: ;
3326#line 147
3327 return (0);
3328}
3329}
3330#line 150 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
3331static void mtdoops_inc_counter(struct mtdoops_context *cxt )
3332{ int tmp ;
3333 unsigned long __cil_tmp3 ;
3334 unsigned long __cil_tmp4 ;
3335 unsigned long __cil_tmp5 ;
3336 unsigned long __cil_tmp6 ;
3337 int __cil_tmp7 ;
3338 unsigned long __cil_tmp8 ;
3339 unsigned long __cil_tmp9 ;
3340 int __cil_tmp10 ;
3341 unsigned long __cil_tmp11 ;
3342 unsigned long __cil_tmp12 ;
3343 int __cil_tmp13 ;
3344 unsigned long __cil_tmp14 ;
3345 unsigned long __cil_tmp15 ;
3346 unsigned long __cil_tmp16 ;
3347 unsigned long __cil_tmp17 ;
3348 unsigned long __cil_tmp18 ;
3349 unsigned long __cil_tmp19 ;
3350 int __cil_tmp20 ;
3351 unsigned long __cil_tmp21 ;
3352 unsigned long __cil_tmp22 ;
3353 int __cil_tmp23 ;
3354 unsigned long __cil_tmp24 ;
3355 unsigned long __cil_tmp25 ;
3356 unsigned long __cil_tmp26 ;
3357 unsigned long __cil_tmp27 ;
3358 int __cil_tmp28 ;
3359 unsigned long __cil_tmp29 ;
3360 unsigned long __cil_tmp30 ;
3361 struct work_struct *__cil_tmp31 ;
3362 unsigned long __cil_tmp32 ;
3363 unsigned long __cil_tmp33 ;
3364 int __cil_tmp34 ;
3365 unsigned long __cil_tmp35 ;
3366 unsigned long __cil_tmp36 ;
3367 int __cil_tmp37 ;
3368
3369 {
3370#line 152
3371 __cil_tmp3 = (unsigned long )cxt;
3372#line 152
3373 __cil_tmp4 = __cil_tmp3 + 212;
3374#line 152
3375 __cil_tmp5 = (unsigned long )cxt;
3376#line 152
3377 __cil_tmp6 = __cil_tmp5 + 212;
3378#line 152
3379 __cil_tmp7 = *((int *)__cil_tmp6);
3380#line 152
3381 *((int *)__cil_tmp4) = __cil_tmp7 + 1;
3382 {
3383#line 153
3384 __cil_tmp8 = (unsigned long )cxt;
3385#line 153
3386 __cil_tmp9 = __cil_tmp8 + 208;
3387#line 153
3388 __cil_tmp10 = *((int *)__cil_tmp9);
3389#line 153
3390 __cil_tmp11 = (unsigned long )cxt;
3391#line 153
3392 __cil_tmp12 = __cil_tmp11 + 212;
3393#line 153
3394 __cil_tmp13 = *((int *)__cil_tmp12);
3395#line 153
3396 if (__cil_tmp13 >= __cil_tmp10) {
3397#line 154
3398 __cil_tmp14 = (unsigned long )cxt;
3399#line 154
3400 __cil_tmp15 = __cil_tmp14 + 212;
3401#line 154
3402 *((int *)__cil_tmp15) = 0;
3403 } else {
3404
3405 }
3406 }
3407#line 155
3408 __cil_tmp16 = (unsigned long )cxt;
3409#line 155
3410 __cil_tmp17 = __cil_tmp16 + 216;
3411#line 155
3412 __cil_tmp18 = (unsigned long )cxt;
3413#line 155
3414 __cil_tmp19 = __cil_tmp18 + 216;
3415#line 155
3416 __cil_tmp20 = *((int *)__cil_tmp19);
3417#line 155
3418 *((int *)__cil_tmp17) = __cil_tmp20 + 1;
3419 {
3420#line 156
3421 __cil_tmp21 = (unsigned long )cxt;
3422#line 156
3423 __cil_tmp22 = __cil_tmp21 + 216;
3424#line 156
3425 __cil_tmp23 = *((int *)__cil_tmp22);
3426#line 156
3427 if (__cil_tmp23 == -1) {
3428#line 157
3429 __cil_tmp24 = (unsigned long )cxt;
3430#line 157
3431 __cil_tmp25 = __cil_tmp24 + 216;
3432#line 157
3433 *((int *)__cil_tmp25) = 0;
3434 } else {
3435
3436 }
3437 }
3438 {
3439#line 159
3440 __cil_tmp26 = (unsigned long )cxt;
3441#line 159
3442 __cil_tmp27 = __cil_tmp26 + 212;
3443#line 159
3444 __cil_tmp28 = *((int *)__cil_tmp27);
3445#line 159
3446 tmp = page_is_used(cxt, __cil_tmp28);
3447 }
3448#line 159
3449 if (tmp != 0) {
3450 {
3451#line 160
3452 __cil_tmp29 = (unsigned long )cxt;
3453#line 160
3454 __cil_tmp30 = __cil_tmp29 + 40;
3455#line 160
3456 __cil_tmp31 = (struct work_struct *)__cil_tmp30;
3457#line 160
3458 schedule_work(__cil_tmp31);
3459 }
3460#line 161
3461 return;
3462 } else {
3463
3464 }
3465 {
3466#line 164
3467 __cil_tmp32 = (unsigned long )cxt;
3468#line 164
3469 __cil_tmp33 = __cil_tmp32 + 212;
3470#line 164
3471 __cil_tmp34 = *((int *)__cil_tmp33);
3472#line 164
3473 __cil_tmp35 = (unsigned long )cxt;
3474#line 164
3475 __cil_tmp36 = __cil_tmp35 + 216;
3476#line 164
3477 __cil_tmp37 = *((int *)__cil_tmp36);
3478#line 164
3479 printk("<7>mtdoops: ready %d, %d (no erase)\n", __cil_tmp34, __cil_tmp37);
3480 }
3481#line 166
3482 return;
3483}
3484}
3485#line 169 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
3486static void mtdoops_workfunc_erase(struct work_struct *work )
3487{ struct mtdoops_context *cxt ;
3488 struct work_struct const *__mptr ;
3489 struct mtd_info *mtd ;
3490 int i ;
3491 int j ;
3492 int ret ;
3493 int mod ;
3494 struct mtdoops_context *__cil_tmp9 ;
3495 unsigned long __cil_tmp10 ;
3496 unsigned long __cil_tmp11 ;
3497 struct mtd_info *__cil_tmp12 ;
3498 unsigned long __cil_tmp13 ;
3499 unsigned long __cil_tmp14 ;
3500 unsigned long __cil_tmp15 ;
3501 unsigned long __cil_tmp16 ;
3502 uint32_t __cil_tmp17 ;
3503 unsigned long __cil_tmp18 ;
3504 unsigned long *__cil_tmp19 ;
3505 unsigned long __cil_tmp20 ;
3506 unsigned long __cil_tmp21 ;
3507 unsigned long __cil_tmp22 ;
3508 int __cil_tmp23 ;
3509 unsigned long __cil_tmp24 ;
3510 unsigned long __cil_tmp25 ;
3511 unsigned long __cil_tmp26 ;
3512 unsigned long __cil_tmp27 ;
3513 unsigned long __cil_tmp28 ;
3514 unsigned long *__cil_tmp29 ;
3515 unsigned long __cil_tmp30 ;
3516 uint32_t __cil_tmp31 ;
3517 unsigned long __cil_tmp32 ;
3518 unsigned long __cil_tmp33 ;
3519 uint32_t __cil_tmp34 ;
3520 uint32_t __cil_tmp35 ;
3521 unsigned long __cil_tmp36 ;
3522 unsigned long __cil_tmp37 ;
3523 unsigned int __cil_tmp38 ;
3524 unsigned long __cil_tmp39 ;
3525 unsigned long __cil_tmp40 ;
3526 int __cil_tmp41 ;
3527 unsigned int __cil_tmp42 ;
3528 unsigned int __cil_tmp43 ;
3529 unsigned long __cil_tmp44 ;
3530 unsigned long __cil_tmp45 ;
3531 int __cil_tmp46 ;
3532 unsigned long __cil_tmp47 ;
3533 unsigned long __cil_tmp48 ;
3534 int __cil_tmp49 ;
3535 unsigned long __cil_tmp50 ;
3536 unsigned long __cil_tmp51 ;
3537 unsigned long *__cil_tmp52 ;
3538 unsigned long __cil_tmp53 ;
3539 unsigned long __cil_tmp54 ;
3540 unsigned long __cil_tmp55 ;
3541 int __cil_tmp56 ;
3542 unsigned long __cil_tmp57 ;
3543 unsigned long __cil_tmp58 ;
3544 loff_t __cil_tmp59 ;
3545 unsigned long *__cil_tmp60 ;
3546 unsigned long __cil_tmp61 ;
3547 unsigned long __cil_tmp62 ;
3548 unsigned long __cil_tmp63 ;
3549 int __cil_tmp64 ;
3550 unsigned long __cil_tmp65 ;
3551 unsigned long __cil_tmp66 ;
3552 unsigned long __cil_tmp67 ;
3553 unsigned long __cil_tmp68 ;
3554 unsigned long *__cil_tmp69 ;
3555 unsigned long __cil_tmp70 ;
3556 unsigned long __cil_tmp71 ;
3557 unsigned long __cil_tmp72 ;
3558 uint32_t __cil_tmp73 ;
3559 unsigned long __cil_tmp74 ;
3560 unsigned long __cil_tmp75 ;
3561 unsigned int __cil_tmp76 ;
3562 unsigned long __cil_tmp77 ;
3563 unsigned long __cil_tmp78 ;
3564 int __cil_tmp79 ;
3565 unsigned int __cil_tmp80 ;
3566 unsigned int __cil_tmp81 ;
3567 unsigned long __cil_tmp82 ;
3568 unsigned long __cil_tmp83 ;
3569 int __cil_tmp84 ;
3570 unsigned long __cil_tmp85 ;
3571 unsigned long __cil_tmp86 ;
3572 int __cil_tmp87 ;
3573 unsigned long __cil_tmp88 ;
3574 unsigned long __cil_tmp89 ;
3575 unsigned long *__cil_tmp90 ;
3576 unsigned long __cil_tmp91 ;
3577 unsigned long __cil_tmp92 ;
3578 unsigned long __cil_tmp93 ;
3579 uint32_t __cil_tmp94 ;
3580 unsigned long __cil_tmp95 ;
3581 unsigned long __cil_tmp96 ;
3582 unsigned long __cil_tmp97 ;
3583 unsigned long __cil_tmp98 ;
3584 int __cil_tmp99 ;
3585 unsigned long __cil_tmp100 ;
3586 unsigned long __cil_tmp101 ;
3587 unsigned long __cil_tmp102 ;
3588 unsigned long *__cil_tmp103 ;
3589 unsigned long __cil_tmp104 ;
3590 unsigned int __cil_tmp105 ;
3591 unsigned long __cil_tmp106 ;
3592 unsigned long __cil_tmp107 ;
3593 int __cil_tmp108 ;
3594 unsigned long __cil_tmp109 ;
3595 unsigned int __cil_tmp110 ;
3596 unsigned int __cil_tmp111 ;
3597 int __cil_tmp112 ;
3598 unsigned long __cil_tmp113 ;
3599 unsigned long __cil_tmp114 ;
3600 int __cil_tmp115 ;
3601 unsigned long __cil_tmp116 ;
3602 unsigned long __cil_tmp117 ;
3603 int __cil_tmp118 ;
3604 unsigned long *__cil_tmp119 ;
3605 unsigned long __cil_tmp120 ;
3606 unsigned long __cil_tmp121 ;
3607 unsigned long __cil_tmp122 ;
3608 int __cil_tmp123 ;
3609 unsigned long __cil_tmp124 ;
3610 unsigned long __cil_tmp125 ;
3611 loff_t __cil_tmp126 ;
3612
3613 {
3614#line 172
3615 __mptr = (struct work_struct const *)work;
3616#line 172
3617 __cil_tmp9 = (struct mtdoops_context *)__mptr;
3618#line 172
3619 cxt = __cil_tmp9 + 0xffffffffffffffd8UL;
3620#line 173
3621 __cil_tmp10 = (unsigned long )cxt;
3622#line 173
3623 __cil_tmp11 = __cil_tmp10 + 200;
3624#line 173
3625 mtd = *((struct mtd_info **)__cil_tmp11);
3626#line 174
3627 i = 0;
3628 {
3629#line 177
3630 __cil_tmp12 = (struct mtd_info *)0;
3631#line 177
3632 __cil_tmp13 = (unsigned long )__cil_tmp12;
3633#line 177
3634 __cil_tmp14 = (unsigned long )mtd;
3635#line 177
3636 if (__cil_tmp14 == __cil_tmp13) {
3637#line 178
3638 return;
3639 } else {
3640
3641 }
3642 }
3643#line 180
3644 __cil_tmp15 = (unsigned long )mtd;
3645#line 180
3646 __cil_tmp16 = __cil_tmp15 + 16;
3647#line 180
3648 __cil_tmp17 = *((uint32_t *)__cil_tmp16);
3649#line 180
3650 __cil_tmp18 = (unsigned long )__cil_tmp17;
3651#line 180
3652 __cil_tmp19 = & record_size;
3653#line 180
3654 __cil_tmp20 = *__cil_tmp19;
3655#line 180
3656 __cil_tmp21 = (unsigned long )cxt;
3657#line 180
3658 __cil_tmp22 = __cil_tmp21 + 212;
3659#line 180
3660 __cil_tmp23 = *((int *)__cil_tmp22);
3661#line 180
3662 __cil_tmp24 = (unsigned long )__cil_tmp23;
3663#line 180
3664 __cil_tmp25 = __cil_tmp24 * __cil_tmp20;
3665#line 180
3666 __cil_tmp26 = __cil_tmp25 % __cil_tmp18;
3667#line 180
3668 mod = (int )__cil_tmp26;
3669#line 181
3670 if (mod != 0) {
3671#line 182
3672 __cil_tmp27 = (unsigned long )cxt;
3673#line 182
3674 __cil_tmp28 = __cil_tmp27 + 212;
3675#line 182
3676 __cil_tmp29 = & record_size;
3677#line 182
3678 __cil_tmp30 = *__cil_tmp29;
3679#line 182
3680 __cil_tmp31 = (uint32_t )mod;
3681#line 182
3682 __cil_tmp32 = (unsigned long )mtd;
3683#line 182
3684 __cil_tmp33 = __cil_tmp32 + 16;
3685#line 182
3686 __cil_tmp34 = *((uint32_t *)__cil_tmp33);
3687#line 182
3688 __cil_tmp35 = __cil_tmp34 - __cil_tmp31;
3689#line 182
3690 __cil_tmp36 = (unsigned long )__cil_tmp35;
3691#line 182
3692 __cil_tmp37 = __cil_tmp36 / __cil_tmp30;
3693#line 182
3694 __cil_tmp38 = (unsigned int )__cil_tmp37;
3695#line 182
3696 __cil_tmp39 = (unsigned long )cxt;
3697#line 182
3698 __cil_tmp40 = __cil_tmp39 + 212;
3699#line 182
3700 __cil_tmp41 = *((int *)__cil_tmp40);
3701#line 182
3702 __cil_tmp42 = (unsigned int )__cil_tmp41;
3703#line 182
3704 __cil_tmp43 = __cil_tmp42 + __cil_tmp38;
3705#line 182
3706 *((int *)__cil_tmp28) = (int )__cil_tmp43;
3707 {
3708#line 183
3709 __cil_tmp44 = (unsigned long )cxt;
3710#line 183
3711 __cil_tmp45 = __cil_tmp44 + 208;
3712#line 183
3713 __cil_tmp46 = *((int *)__cil_tmp45);
3714#line 183
3715 __cil_tmp47 = (unsigned long )cxt;
3716#line 183
3717 __cil_tmp48 = __cil_tmp47 + 212;
3718#line 183
3719 __cil_tmp49 = *((int *)__cil_tmp48);
3720#line 183
3721 if (__cil_tmp49 >= __cil_tmp46) {
3722#line 184
3723 __cil_tmp50 = (unsigned long )cxt;
3724#line 184
3725 __cil_tmp51 = __cil_tmp50 + 212;
3726#line 184
3727 *((int *)__cil_tmp51) = 0;
3728 } else {
3729
3730 }
3731 }
3732 } else {
3733
3734 }
3735 ldv_20379:
3736 {
3737#line 188
3738 __cil_tmp52 = & record_size;
3739#line 188
3740 __cil_tmp53 = *__cil_tmp52;
3741#line 188
3742 __cil_tmp54 = (unsigned long )cxt;
3743#line 188
3744 __cil_tmp55 = __cil_tmp54 + 212;
3745#line 188
3746 __cil_tmp56 = *((int *)__cil_tmp55);
3747#line 188
3748 __cil_tmp57 = (unsigned long )__cil_tmp56;
3749#line 188
3750 __cil_tmp58 = __cil_tmp57 * __cil_tmp53;
3751#line 188
3752 __cil_tmp59 = (loff_t )__cil_tmp58;
3753#line 188
3754 ret = mtd_block_isbad(mtd, __cil_tmp59);
3755 }
3756#line 189
3757 if (ret == 0) {
3758#line 190
3759 goto ldv_20377;
3760 } else {
3761
3762 }
3763#line 191
3764 if (ret < 0) {
3765 {
3766#line 192
3767 printk("<3>mtdoops: block_isbad failed, aborting\n");
3768 }
3769#line 193
3770 return;
3771 } else {
3772
3773 }
3774 badblock:
3775 {
3776#line 196
3777 __cil_tmp60 = & record_size;
3778#line 196
3779 __cil_tmp61 = *__cil_tmp60;
3780#line 196
3781 __cil_tmp62 = (unsigned long )cxt;
3782#line 196
3783 __cil_tmp63 = __cil_tmp62 + 212;
3784#line 196
3785 __cil_tmp64 = *((int *)__cil_tmp63);
3786#line 196
3787 __cil_tmp65 = (unsigned long )__cil_tmp64;
3788#line 196
3789 __cil_tmp66 = __cil_tmp65 * __cil_tmp61;
3790#line 196
3791 printk("<4>mtdoops: bad block at %08lx\n", __cil_tmp66);
3792#line 198
3793 i = i + 1;
3794#line 199
3795 __cil_tmp67 = (unsigned long )cxt;
3796#line 199
3797 __cil_tmp68 = __cil_tmp67 + 212;
3798#line 199
3799 __cil_tmp69 = & record_size;
3800#line 199
3801 __cil_tmp70 = *__cil_tmp69;
3802#line 199
3803 __cil_tmp71 = (unsigned long )mtd;
3804#line 199
3805 __cil_tmp72 = __cil_tmp71 + 16;
3806#line 199
3807 __cil_tmp73 = *((uint32_t *)__cil_tmp72);
3808#line 199
3809 __cil_tmp74 = (unsigned long )__cil_tmp73;
3810#line 199
3811 __cil_tmp75 = __cil_tmp74 / __cil_tmp70;
3812#line 199
3813 __cil_tmp76 = (unsigned int )__cil_tmp75;
3814#line 199
3815 __cil_tmp77 = (unsigned long )cxt;
3816#line 199
3817 __cil_tmp78 = __cil_tmp77 + 212;
3818#line 199
3819 __cil_tmp79 = *((int *)__cil_tmp78);
3820#line 199
3821 __cil_tmp80 = (unsigned int )__cil_tmp79;
3822#line 199
3823 __cil_tmp81 = __cil_tmp80 + __cil_tmp76;
3824#line 199
3825 *((int *)__cil_tmp68) = (int )__cil_tmp81;
3826 }
3827 {
3828#line 200
3829 __cil_tmp82 = (unsigned long )cxt;
3830#line 200
3831 __cil_tmp83 = __cil_tmp82 + 208;
3832#line 200
3833 __cil_tmp84 = *((int *)__cil_tmp83);
3834#line 200
3835 __cil_tmp85 = (unsigned long )cxt;
3836#line 200
3837 __cil_tmp86 = __cil_tmp85 + 212;
3838#line 200
3839 __cil_tmp87 = *((int *)__cil_tmp86);
3840#line 200
3841 if (__cil_tmp87 >= __cil_tmp84) {
3842#line 201
3843 __cil_tmp88 = (unsigned long )cxt;
3844#line 201
3845 __cil_tmp89 = __cil_tmp88 + 212;
3846#line 201
3847 *((int *)__cil_tmp89) = 0;
3848 } else {
3849
3850 }
3851 }
3852 {
3853#line 202
3854 __cil_tmp90 = & record_size;
3855#line 202
3856 __cil_tmp91 = *__cil_tmp90;
3857#line 202
3858 __cil_tmp92 = (unsigned long )mtd;
3859#line 202
3860 __cil_tmp93 = __cil_tmp92 + 16;
3861#line 202
3862 __cil_tmp94 = *((uint32_t *)__cil_tmp93);
3863#line 202
3864 __cil_tmp95 = (unsigned long )__cil_tmp94;
3865#line 202
3866 __cil_tmp96 = __cil_tmp95 / __cil_tmp91;
3867#line 202
3868 __cil_tmp97 = (unsigned long )cxt;
3869#line 202
3870 __cil_tmp98 = __cil_tmp97 + 208;
3871#line 202
3872 __cil_tmp99 = *((int *)__cil_tmp98);
3873#line 202
3874 __cil_tmp100 = (unsigned long )__cil_tmp99;
3875#line 202
3876 __cil_tmp101 = __cil_tmp100 / __cil_tmp96;
3877#line 202
3878 __cil_tmp102 = (unsigned long )i;
3879#line 202
3880 if (__cil_tmp102 == __cil_tmp101) {
3881 {
3882#line 203
3883 printk("<3>mtdoops: all blocks bad!\n");
3884 }
3885#line 204
3886 return;
3887 } else {
3888
3889 }
3890 }
3891#line 206
3892 goto ldv_20379;
3893 ldv_20377:
3894#line 208
3895 j = 0;
3896#line 208
3897 ret = -1;
3898#line 208
3899 goto ldv_20381;
3900 ldv_20380:
3901 {
3902#line 209
3903 __cil_tmp103 = & record_size;
3904#line 209
3905 __cil_tmp104 = *__cil_tmp103;
3906#line 209
3907 __cil_tmp105 = (unsigned int )__cil_tmp104;
3908#line 209
3909 __cil_tmp106 = (unsigned long )cxt;
3910#line 209
3911 __cil_tmp107 = __cil_tmp106 + 212;
3912#line 209
3913 __cil_tmp108 = *((int *)__cil_tmp107);
3914#line 209
3915 __cil_tmp109 = (unsigned long )__cil_tmp108;
3916#line 209
3917 __cil_tmp110 = (unsigned int )__cil_tmp109;
3918#line 209
3919 __cil_tmp111 = __cil_tmp110 * __cil_tmp105;
3920#line 209
3921 __cil_tmp112 = (int )__cil_tmp111;
3922#line 209
3923 ret = mtdoops_erase_block(cxt, __cil_tmp112);
3924#line 208
3925 j = j + 1;
3926 }
3927 ldv_20381: ;
3928#line 208
3929 if (j <= 2) {
3930#line 208
3931 if (ret < 0) {
3932#line 209
3933 goto ldv_20380;
3934 } else {
3935#line 211
3936 goto ldv_20382;
3937 }
3938 } else {
3939#line 211
3940 goto ldv_20382;
3941 }
3942 ldv_20382: ;
3943#line 211
3944 if (ret >= 0) {
3945 {
3946#line 212
3947 __cil_tmp113 = (unsigned long )cxt;
3948#line 212
3949 __cil_tmp114 = __cil_tmp113 + 212;
3950#line 212
3951 __cil_tmp115 = *((int *)__cil_tmp114);
3952#line 212
3953 __cil_tmp116 = (unsigned long )cxt;
3954#line 212
3955 __cil_tmp117 = __cil_tmp116 + 216;
3956#line 212
3957 __cil_tmp118 = *((int *)__cil_tmp117);
3958#line 212
3959 printk("<7>mtdoops: ready %d, %d\n", __cil_tmp115, __cil_tmp118);
3960 }
3961#line 214
3962 return;
3963 } else {
3964
3965 }
3966#line 217
3967 if (ret == -5) {
3968 {
3969#line 218
3970 __cil_tmp119 = & record_size;
3971#line 218
3972 __cil_tmp120 = *__cil_tmp119;
3973#line 218
3974 __cil_tmp121 = (unsigned long )cxt;
3975#line 218
3976 __cil_tmp122 = __cil_tmp121 + 212;
3977#line 218
3978 __cil_tmp123 = *((int *)__cil_tmp122);
3979#line 218
3980 __cil_tmp124 = (unsigned long )__cil_tmp123;
3981#line 218
3982 __cil_tmp125 = __cil_tmp124 * __cil_tmp120;
3983#line 218
3984 __cil_tmp126 = (loff_t )__cil_tmp125;
3985#line 218
3986 ret = mtd_block_markbad(mtd, __cil_tmp126);
3987 }
3988#line 219
3989 if (ret < 0) {
3990#line 219
3991 if (ret != -95) {
3992 {
3993#line 220
3994 printk("<3>mtdoops: block_markbad failed, aborting\n");
3995 }
3996#line 221
3997 return;
3998 } else {
3999
4000 }
4001 } else {
4002
4003 }
4004 } else {
4005
4006 }
4007#line 224
4008 goto badblock;
4009}
4010}
4011#line 227 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
4012static void mtdoops_write(struct mtdoops_context *cxt , int panic___0 )
4013{ struct mtd_info *mtd ;
4014 size_t retlen ;
4015 u32 *hdr ;
4016 int ret ;
4017 unsigned long __cil_tmp7 ;
4018 unsigned long __cil_tmp8 ;
4019 unsigned long __cil_tmp9 ;
4020 unsigned long __cil_tmp10 ;
4021 void *__cil_tmp11 ;
4022 unsigned long __cil_tmp12 ;
4023 unsigned long __cil_tmp13 ;
4024 int __cil_tmp14 ;
4025 u32 *__cil_tmp15 ;
4026 unsigned long *__cil_tmp16 ;
4027 unsigned long __cil_tmp17 ;
4028 unsigned long __cil_tmp18 ;
4029 unsigned long __cil_tmp19 ;
4030 int __cil_tmp20 ;
4031 unsigned long __cil_tmp21 ;
4032 unsigned long __cil_tmp22 ;
4033 loff_t __cil_tmp23 ;
4034 unsigned long *__cil_tmp24 ;
4035 unsigned long __cil_tmp25 ;
4036 unsigned long __cil_tmp26 ;
4037 unsigned long __cil_tmp27 ;
4038 void *__cil_tmp28 ;
4039 u_char const *__cil_tmp29 ;
4040 unsigned long *__cil_tmp30 ;
4041 unsigned long __cil_tmp31 ;
4042 unsigned long __cil_tmp32 ;
4043 unsigned long __cil_tmp33 ;
4044 int __cil_tmp34 ;
4045 unsigned long __cil_tmp35 ;
4046 unsigned long __cil_tmp36 ;
4047 loff_t __cil_tmp37 ;
4048 unsigned long *__cil_tmp38 ;
4049 unsigned long __cil_tmp39 ;
4050 unsigned long __cil_tmp40 ;
4051 unsigned long __cil_tmp41 ;
4052 void *__cil_tmp42 ;
4053 u_char const *__cil_tmp43 ;
4054 unsigned long *__cil_tmp44 ;
4055 unsigned long __cil_tmp45 ;
4056 size_t *__cil_tmp46 ;
4057 size_t __cil_tmp47 ;
4058 unsigned long *__cil_tmp48 ;
4059 unsigned long __cil_tmp49 ;
4060 unsigned long __cil_tmp50 ;
4061 unsigned long __cil_tmp51 ;
4062 int __cil_tmp52 ;
4063 unsigned long __cil_tmp53 ;
4064 unsigned long __cil_tmp54 ;
4065 size_t *__cil_tmp55 ;
4066 size_t __cil_tmp56 ;
4067 unsigned long *__cil_tmp57 ;
4068 unsigned long __cil_tmp58 ;
4069 unsigned long *__cil_tmp59 ;
4070 unsigned long __cil_tmp60 ;
4071 unsigned long __cil_tmp61 ;
4072 unsigned long __cil_tmp62 ;
4073 int __cil_tmp63 ;
4074 unsigned long __cil_tmp64 ;
4075 unsigned long __cil_tmp65 ;
4076 size_t *__cil_tmp66 ;
4077 size_t __cil_tmp67 ;
4078 unsigned long *__cil_tmp68 ;
4079 unsigned long __cil_tmp69 ;
4080 unsigned long __cil_tmp70 ;
4081 unsigned long __cil_tmp71 ;
4082 int __cil_tmp72 ;
4083 unsigned long __cil_tmp73 ;
4084 unsigned long __cil_tmp74 ;
4085 void *__cil_tmp75 ;
4086 unsigned long *__cil_tmp76 ;
4087 unsigned long __cil_tmp77 ;
4088
4089 {
4090#line 229
4091 __cil_tmp7 = (unsigned long )cxt;
4092#line 229
4093 __cil_tmp8 = __cil_tmp7 + 200;
4094#line 229
4095 mtd = *((struct mtd_info **)__cil_tmp8);
4096#line 235
4097 __cil_tmp9 = (unsigned long )cxt;
4098#line 235
4099 __cil_tmp10 = __cil_tmp9 + 232;
4100#line 235
4101 __cil_tmp11 = *((void **)__cil_tmp10);
4102#line 235
4103 hdr = (u32 *)__cil_tmp11;
4104#line 236
4105 __cil_tmp12 = (unsigned long )cxt;
4106#line 236
4107 __cil_tmp13 = __cil_tmp12 + 216;
4108#line 236
4109 __cil_tmp14 = *((int *)__cil_tmp13);
4110#line 236
4111 *hdr = (u32 )__cil_tmp14;
4112#line 237
4113 __cil_tmp15 = hdr + 1UL;
4114#line 237
4115 *__cil_tmp15 = 1560304896U;
4116#line 239
4117 if (panic___0 != 0) {
4118 {
4119#line 240
4120 __cil_tmp16 = & record_size;
4121#line 240
4122 __cil_tmp17 = *__cil_tmp16;
4123#line 240
4124 __cil_tmp18 = (unsigned long )cxt;
4125#line 240
4126 __cil_tmp19 = __cil_tmp18 + 212;
4127#line 240
4128 __cil_tmp20 = *((int *)__cil_tmp19);
4129#line 240
4130 __cil_tmp21 = (unsigned long )__cil_tmp20;
4131#line 240
4132 __cil_tmp22 = __cil_tmp21 * __cil_tmp17;
4133#line 240
4134 __cil_tmp23 = (loff_t )__cil_tmp22;
4135#line 240
4136 __cil_tmp24 = & record_size;
4137#line 240
4138 __cil_tmp25 = *__cil_tmp24;
4139#line 240
4140 __cil_tmp26 = (unsigned long )cxt;
4141#line 240
4142 __cil_tmp27 = __cil_tmp26 + 232;
4143#line 240
4144 __cil_tmp28 = *((void **)__cil_tmp27);
4145#line 240
4146 __cil_tmp29 = (u_char const *)__cil_tmp28;
4147#line 240
4148 ret = mtd_panic_write(mtd, __cil_tmp23, __cil_tmp25, & retlen, __cil_tmp29);
4149 }
4150#line 242
4151 if (ret == -95) {
4152 {
4153#line 243
4154 printk("<3>mtdoops: Cannot write from panic without panic_write\n");
4155 }
4156#line 244
4157 return;
4158 } else {
4159
4160 }
4161 } else {
4162 {
4163#line 247
4164 __cil_tmp30 = & record_size;
4165#line 247
4166 __cil_tmp31 = *__cil_tmp30;
4167#line 247
4168 __cil_tmp32 = (unsigned long )cxt;
4169#line 247
4170 __cil_tmp33 = __cil_tmp32 + 212;
4171#line 247
4172 __cil_tmp34 = *((int *)__cil_tmp33);
4173#line 247
4174 __cil_tmp35 = (unsigned long )__cil_tmp34;
4175#line 247
4176 __cil_tmp36 = __cil_tmp35 * __cil_tmp31;
4177#line 247
4178 __cil_tmp37 = (loff_t )__cil_tmp36;
4179#line 247
4180 __cil_tmp38 = & record_size;
4181#line 247
4182 __cil_tmp39 = *__cil_tmp38;
4183#line 247
4184 __cil_tmp40 = (unsigned long )cxt;
4185#line 247
4186 __cil_tmp41 = __cil_tmp40 + 232;
4187#line 247
4188 __cil_tmp42 = *((void **)__cil_tmp41);
4189#line 247
4190 __cil_tmp43 = (u_char const *)__cil_tmp42;
4191#line 247
4192 ret = mtd_write(mtd, __cil_tmp37, __cil_tmp39, & retlen, __cil_tmp43);
4193 }
4194 }
4195 {
4196#line 250
4197 __cil_tmp44 = & record_size;
4198#line 250
4199 __cil_tmp45 = *__cil_tmp44;
4200#line 250
4201 __cil_tmp46 = & retlen;
4202#line 250
4203 __cil_tmp47 = *__cil_tmp46;
4204#line 250
4205 if (__cil_tmp47 != __cil_tmp45) {
4206 {
4207#line 251
4208 __cil_tmp48 = & record_size;
4209#line 251
4210 __cil_tmp49 = *__cil_tmp48;
4211#line 251
4212 __cil_tmp50 = (unsigned long )cxt;
4213#line 251
4214 __cil_tmp51 = __cil_tmp50 + 212;
4215#line 251
4216 __cil_tmp52 = *((int *)__cil_tmp51);
4217#line 251
4218 __cil_tmp53 = (unsigned long )__cil_tmp52;
4219#line 251
4220 __cil_tmp54 = __cil_tmp53 * __cil_tmp49;
4221#line 251
4222 __cil_tmp55 = & retlen;
4223#line 251
4224 __cil_tmp56 = *__cil_tmp55;
4225#line 251
4226 __cil_tmp57 = & record_size;
4227#line 251
4228 __cil_tmp58 = *__cil_tmp57;
4229#line 251
4230 printk("<3>mtdoops: write failure at %ld (%td of %ld written), error %d\n", __cil_tmp54,
4231 __cil_tmp56, __cil_tmp58, ret);
4232 }
4233 } else
4234#line 250
4235 if (ret < 0) {
4236 {
4237#line 251
4238 __cil_tmp59 = & record_size;
4239#line 251
4240 __cil_tmp60 = *__cil_tmp59;
4241#line 251
4242 __cil_tmp61 = (unsigned long )cxt;
4243#line 251
4244 __cil_tmp62 = __cil_tmp61 + 212;
4245#line 251
4246 __cil_tmp63 = *((int *)__cil_tmp62);
4247#line 251
4248 __cil_tmp64 = (unsigned long )__cil_tmp63;
4249#line 251
4250 __cil_tmp65 = __cil_tmp64 * __cil_tmp60;
4251#line 251
4252 __cil_tmp66 = & retlen;
4253#line 251
4254 __cil_tmp67 = *__cil_tmp66;
4255#line 251
4256 __cil_tmp68 = & record_size;
4257#line 251
4258 __cil_tmp69 = *__cil_tmp68;
4259#line 251
4260 printk("<3>mtdoops: write failure at %ld (%td of %ld written), error %d\n", __cil_tmp65,
4261 __cil_tmp67, __cil_tmp69, ret);
4262 }
4263 } else {
4264
4265 }
4266 }
4267 {
4268#line 253
4269 __cil_tmp70 = (unsigned long )cxt;
4270#line 253
4271 __cil_tmp71 = __cil_tmp70 + 212;
4272#line 253
4273 __cil_tmp72 = *((int *)__cil_tmp71);
4274#line 253
4275 mark_page_used(cxt, __cil_tmp72);
4276#line 254
4277 __cil_tmp73 = (unsigned long )cxt;
4278#line 254
4279 __cil_tmp74 = __cil_tmp73 + 232;
4280#line 254
4281 __cil_tmp75 = *((void **)__cil_tmp74);
4282#line 254
4283 __cil_tmp76 = & record_size;
4284#line 254
4285 __cil_tmp77 = *__cil_tmp76;
4286#line 254
4287 memset(__cil_tmp75, 255, __cil_tmp77);
4288#line 256
4289 mtdoops_inc_counter(cxt);
4290 }
4291#line 257
4292 return;
4293}
4294}
4295#line 259 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
4296static void mtdoops_workfunc_write(struct work_struct *work )
4297{ struct mtdoops_context *cxt ;
4298 struct work_struct const *__mptr ;
4299 struct mtdoops_context *__cil_tmp4 ;
4300
4301 {
4302 {
4303#line 262
4304 __mptr = (struct work_struct const *)work;
4305#line 262
4306 __cil_tmp4 = (struct mtdoops_context *)__mptr;
4307#line 262
4308 cxt = __cil_tmp4 + 0xffffffffffffff88UL;
4309#line 264
4310 mtdoops_write(cxt, 0);
4311 }
4312#line 265
4313 return;
4314}
4315}
4316#line 267 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
4317static void find_next_position(struct mtdoops_context *cxt )
4318{ struct mtd_info *mtd ;
4319 int ret ;
4320 int page ;
4321 int maxpos ;
4322 u32 count[2U] ;
4323 u32 maxcount ;
4324 size_t retlen ;
4325 int tmp ;
4326 int tmp___0 ;
4327 unsigned long __cil_tmp11 ;
4328 unsigned long __cil_tmp12 ;
4329 unsigned long *__cil_tmp13 ;
4330 unsigned long __cil_tmp14 ;
4331 unsigned long __cil_tmp15 ;
4332 unsigned long __cil_tmp16 ;
4333 loff_t __cil_tmp17 ;
4334 unsigned long *__cil_tmp18 ;
4335 unsigned long __cil_tmp19 ;
4336 unsigned long __cil_tmp20 ;
4337 unsigned long __cil_tmp21 ;
4338 loff_t __cil_tmp22 ;
4339 u_char *__cil_tmp23 ;
4340 size_t *__cil_tmp24 ;
4341 size_t __cil_tmp25 ;
4342 unsigned long *__cil_tmp26 ;
4343 unsigned long __cil_tmp27 ;
4344 unsigned long __cil_tmp28 ;
4345 unsigned long __cil_tmp29 ;
4346 size_t *__cil_tmp30 ;
4347 size_t __cil_tmp31 ;
4348 unsigned long *__cil_tmp32 ;
4349 unsigned long __cil_tmp33 ;
4350 unsigned long __cil_tmp34 ;
4351 unsigned long __cil_tmp35 ;
4352 size_t *__cil_tmp36 ;
4353 size_t __cil_tmp37 ;
4354 unsigned long __cil_tmp38 ;
4355 unsigned long __cil_tmp39 ;
4356 u32 __cil_tmp40 ;
4357 unsigned long __cil_tmp41 ;
4358 unsigned long __cil_tmp42 ;
4359 u32 __cil_tmp43 ;
4360 unsigned long __cil_tmp44 ;
4361 unsigned long __cil_tmp45 ;
4362 u32 __cil_tmp46 ;
4363 unsigned long __cil_tmp47 ;
4364 unsigned long __cil_tmp48 ;
4365 unsigned long __cil_tmp49 ;
4366 unsigned long __cil_tmp50 ;
4367 u32 __cil_tmp51 ;
4368 unsigned long __cil_tmp52 ;
4369 unsigned long __cil_tmp53 ;
4370 unsigned long __cil_tmp54 ;
4371 unsigned long __cil_tmp55 ;
4372 u32 __cil_tmp56 ;
4373 unsigned long __cil_tmp57 ;
4374 unsigned long __cil_tmp58 ;
4375 u32 __cil_tmp59 ;
4376 unsigned long __cil_tmp60 ;
4377 unsigned long __cil_tmp61 ;
4378 unsigned long __cil_tmp62 ;
4379 unsigned long __cil_tmp63 ;
4380 u32 __cil_tmp64 ;
4381 unsigned long __cil_tmp65 ;
4382 unsigned long __cil_tmp66 ;
4383 u32 __cil_tmp67 ;
4384 unsigned long __cil_tmp68 ;
4385 unsigned long __cil_tmp69 ;
4386 unsigned long __cil_tmp70 ;
4387 unsigned long __cil_tmp71 ;
4388 int __cil_tmp72 ;
4389 unsigned long __cil_tmp73 ;
4390 unsigned long __cil_tmp74 ;
4391 unsigned long __cil_tmp75 ;
4392 unsigned long __cil_tmp76 ;
4393 unsigned long __cil_tmp77 ;
4394 unsigned long __cil_tmp78 ;
4395 struct work_struct *__cil_tmp79 ;
4396 unsigned long __cil_tmp80 ;
4397 unsigned long __cil_tmp81 ;
4398 unsigned long __cil_tmp82 ;
4399 unsigned long __cil_tmp83 ;
4400
4401 {
4402#line 269
4403 __cil_tmp11 = (unsigned long )cxt;
4404#line 269
4405 __cil_tmp12 = __cil_tmp11 + 200;
4406#line 269
4407 mtd = *((struct mtd_info **)__cil_tmp12);
4408#line 270
4409 maxpos = 0;
4410#line 271
4411 maxcount = 4294967295U;
4412#line 274
4413 page = 0;
4414#line 274
4415 goto ldv_20409;
4416 ldv_20408:
4417 {
4418#line 275
4419 __cil_tmp13 = & record_size;
4420#line 275
4421 __cil_tmp14 = *__cil_tmp13;
4422#line 275
4423 __cil_tmp15 = (unsigned long )page;
4424#line 275
4425 __cil_tmp16 = __cil_tmp15 * __cil_tmp14;
4426#line 275
4427 __cil_tmp17 = (loff_t )__cil_tmp16;
4428#line 275
4429 tmp = mtd_block_isbad(mtd, __cil_tmp17);
4430 }
4431#line 275
4432 if (tmp != 0) {
4433#line 276
4434 goto ldv_20407;
4435 } else {
4436
4437 }
4438 {
4439#line 278
4440 mark_page_used(cxt, page);
4441#line 279
4442 __cil_tmp18 = & record_size;
4443#line 279
4444 __cil_tmp19 = *__cil_tmp18;
4445#line 279
4446 __cil_tmp20 = (unsigned long )page;
4447#line 279
4448 __cil_tmp21 = __cil_tmp20 * __cil_tmp19;
4449#line 279
4450 __cil_tmp22 = (loff_t )__cil_tmp21;
4451#line 279
4452 __cil_tmp23 = (u_char *)(& count);
4453#line 279
4454 ret = mtd_read(mtd, __cil_tmp22, 8UL, & retlen, __cil_tmp23);
4455 }
4456 {
4457#line 281
4458 __cil_tmp24 = & retlen;
4459#line 281
4460 __cil_tmp25 = *__cil_tmp24;
4461#line 281
4462 if (__cil_tmp25 != 8UL) {
4463 {
4464#line 283
4465 __cil_tmp26 = & record_size;
4466#line 283
4467 __cil_tmp27 = *__cil_tmp26;
4468#line 283
4469 __cil_tmp28 = (unsigned long )page;
4470#line 283
4471 __cil_tmp29 = __cil_tmp28 * __cil_tmp27;
4472#line 283
4473 __cil_tmp30 = & retlen;
4474#line 283
4475 __cil_tmp31 = *__cil_tmp30;
4476#line 283
4477 printk("<3>mtdoops: read failure at %ld (%td of %d read), err %d\n", __cil_tmp29,
4478 __cil_tmp31, 8, ret);
4479 }
4480#line 286
4481 goto ldv_20407;
4482 } else
4483#line 281
4484 if (ret < 0) {
4485 {
4486#line 281
4487 tmp___0 = mtd_is_bitflip(ret);
4488 }
4489#line 281
4490 if (tmp___0 == 0) {
4491 {
4492#line 283
4493 __cil_tmp32 = & record_size;
4494#line 283
4495 __cil_tmp33 = *__cil_tmp32;
4496#line 283
4497 __cil_tmp34 = (unsigned long )page;
4498#line 283
4499 __cil_tmp35 = __cil_tmp34 * __cil_tmp33;
4500#line 283
4501 __cil_tmp36 = & retlen;
4502#line 283
4503 __cil_tmp37 = *__cil_tmp36;
4504#line 283
4505 printk("<3>mtdoops: read failure at %ld (%td of %d read), err %d\n", __cil_tmp35,
4506 __cil_tmp37, 8, ret);
4507 }
4508#line 286
4509 goto ldv_20407;
4510 } else {
4511
4512 }
4513 } else {
4514
4515 }
4516 }
4517 {
4518#line 289
4519 __cil_tmp38 = 0 * 4UL;
4520#line 289
4521 __cil_tmp39 = (unsigned long )(count) + __cil_tmp38;
4522#line 289
4523 __cil_tmp40 = *((u32 *)__cil_tmp39);
4524#line 289
4525 if (__cil_tmp40 == 4294967295U) {
4526 {
4527#line 289
4528 __cil_tmp41 = 1 * 4UL;
4529#line 289
4530 __cil_tmp42 = (unsigned long )(count) + __cil_tmp41;
4531#line 289
4532 __cil_tmp43 = *((u32 *)__cil_tmp42);
4533#line 289
4534 if (__cil_tmp43 == 4294967295U) {
4535 {
4536#line 290
4537 mark_page_unused(cxt, page);
4538 }
4539 } else {
4540
4541 }
4542 }
4543 } else {
4544
4545 }
4546 }
4547 {
4548#line 291
4549 __cil_tmp44 = 0 * 4UL;
4550#line 291
4551 __cil_tmp45 = (unsigned long )(count) + __cil_tmp44;
4552#line 291
4553 __cil_tmp46 = *((u32 *)__cil_tmp45);
4554#line 291
4555 if (__cil_tmp46 == 4294967295U) {
4556#line 292
4557 goto ldv_20407;
4558 } else {
4559
4560 }
4561 }
4562#line 293
4563 if (maxcount == 4294967295U) {
4564#line 294
4565 __cil_tmp47 = 0 * 4UL;
4566#line 294
4567 __cil_tmp48 = (unsigned long )(count) + __cil_tmp47;
4568#line 294
4569 maxcount = *((u32 *)__cil_tmp48);
4570#line 295
4571 maxpos = page;
4572 } else {
4573 {
4574#line 296
4575 __cil_tmp49 = 0 * 4UL;
4576#line 296
4577 __cil_tmp50 = (unsigned long )(count) + __cil_tmp49;
4578#line 296
4579 __cil_tmp51 = *((u32 *)__cil_tmp50);
4580#line 296
4581 if (__cil_tmp51 <= 1073741823U) {
4582#line 296
4583 if (maxcount > 3221225472U) {
4584#line 297
4585 __cil_tmp52 = 0 * 4UL;
4586#line 297
4587 __cil_tmp53 = (unsigned long )(count) + __cil_tmp52;
4588#line 297
4589 maxcount = *((u32 *)__cil_tmp53);
4590#line 298
4591 maxpos = page;
4592 } else {
4593#line 296
4594 goto _L___0;
4595 }
4596 } else {
4597 _L___0:
4598 {
4599#line 299
4600 __cil_tmp54 = 0 * 4UL;
4601#line 299
4602 __cil_tmp55 = (unsigned long )(count) + __cil_tmp54;
4603#line 299
4604 __cil_tmp56 = *((u32 *)__cil_tmp55);
4605#line 299
4606 if (__cil_tmp56 > maxcount) {
4607 {
4608#line 299
4609 __cil_tmp57 = 0 * 4UL;
4610#line 299
4611 __cil_tmp58 = (unsigned long )(count) + __cil_tmp57;
4612#line 299
4613 __cil_tmp59 = *((u32 *)__cil_tmp58);
4614#line 299
4615 if (__cil_tmp59 <= 3221225471U) {
4616#line 300
4617 __cil_tmp60 = 0 * 4UL;
4618#line 300
4619 __cil_tmp61 = (unsigned long )(count) + __cil_tmp60;
4620#line 300
4621 maxcount = *((u32 *)__cil_tmp61);
4622#line 301
4623 maxpos = page;
4624 } else {
4625#line 299
4626 goto _L;
4627 }
4628 }
4629 } else {
4630 _L:
4631 {
4632#line 302
4633 __cil_tmp62 = 0 * 4UL;
4634#line 302
4635 __cil_tmp63 = (unsigned long )(count) + __cil_tmp62;
4636#line 302
4637 __cil_tmp64 = *((u32 *)__cil_tmp63);
4638#line 302
4639 if (__cil_tmp64 > maxcount) {
4640 {
4641#line 302
4642 __cil_tmp65 = 0 * 4UL;
4643#line 302
4644 __cil_tmp66 = (unsigned long )(count) + __cil_tmp65;
4645#line 302
4646 __cil_tmp67 = *((u32 *)__cil_tmp66);
4647#line 302
4648 if (__cil_tmp67 > 3221225472U) {
4649#line 302
4650 if (maxcount > 2147483648U) {
4651#line 304
4652 __cil_tmp68 = 0 * 4UL;
4653#line 304
4654 __cil_tmp69 = (unsigned long )(count) + __cil_tmp68;
4655#line 304
4656 maxcount = *((u32 *)__cil_tmp69);
4657#line 305
4658 maxpos = page;
4659 } else {
4660
4661 }
4662 } else {
4663
4664 }
4665 }
4666 } else {
4667
4668 }
4669 }
4670 }
4671 }
4672 }
4673 }
4674 }
4675 ldv_20407:
4676#line 274
4677 page = page + 1;
4678 ldv_20409: ;
4679 {
4680#line 274
4681 __cil_tmp70 = (unsigned long )cxt;
4682#line 274
4683 __cil_tmp71 = __cil_tmp70 + 208;
4684#line 274
4685 __cil_tmp72 = *((int *)__cil_tmp71);
4686#line 274
4687 if (__cil_tmp72 > page) {
4688#line 275
4689 goto ldv_20408;
4690 } else {
4691#line 277
4692 goto ldv_20410;
4693 }
4694 }
4695 ldv_20410: ;
4696#line 308
4697 if (maxcount == 4294967295U) {
4698 {
4699#line 309
4700 __cil_tmp73 = (unsigned long )cxt;
4701#line 309
4702 __cil_tmp74 = __cil_tmp73 + 212;
4703#line 309
4704 *((int *)__cil_tmp74) = 0;
4705#line 310
4706 __cil_tmp75 = (unsigned long )cxt;
4707#line 310
4708 __cil_tmp76 = __cil_tmp75 + 216;
4709#line 310
4710 *((int *)__cil_tmp76) = 1;
4711#line 311
4712 __cil_tmp77 = (unsigned long )cxt;
4713#line 311
4714 __cil_tmp78 = __cil_tmp77 + 40;
4715#line 311
4716 __cil_tmp79 = (struct work_struct *)__cil_tmp78;
4717#line 311
4718 schedule_work(__cil_tmp79);
4719 }
4720#line 312
4721 return;
4722 } else {
4723
4724 }
4725 {
4726#line 315
4727 __cil_tmp80 = (unsigned long )cxt;
4728#line 315
4729 __cil_tmp81 = __cil_tmp80 + 212;
4730#line 315
4731 *((int *)__cil_tmp81) = maxpos;
4732#line 316
4733 __cil_tmp82 = (unsigned long )cxt;
4734#line 316
4735 __cil_tmp83 = __cil_tmp82 + 216;
4736#line 316
4737 *((int *)__cil_tmp83) = (int )maxcount;
4738#line 318
4739 mtdoops_inc_counter(cxt);
4740 }
4741#line 319
4742 return;
4743}
4744}
4745#line 321 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
4746static void mtdoops_do_dump(struct kmsg_dumper *dumper , enum kmsg_dump_reason reason ,
4747 char const *s1 , unsigned long l1 , char const *s2 ,
4748 unsigned long l2 )
4749{ struct mtdoops_context *cxt ;
4750 struct kmsg_dumper const *__mptr ;
4751 unsigned long s1_start ;
4752 unsigned long s2_start ;
4753 unsigned long l1_cpy ;
4754 unsigned long l2_cpy ;
4755 char *dst ;
4756 unsigned long _min1 ;
4757 unsigned long _min2 ;
4758 unsigned long tmp ;
4759 unsigned long _min1___0 ;
4760 unsigned long _min2___0 ;
4761 unsigned long tmp___0 ;
4762 size_t __len ;
4763 void *__ret ;
4764 size_t __len___0 ;
4765 void *__ret___0 ;
4766 unsigned int __cil_tmp24 ;
4767 unsigned int __cil_tmp25 ;
4768 unsigned int __cil_tmp26 ;
4769 int *__cil_tmp27 ;
4770 int __cil_tmp28 ;
4771 unsigned long __cil_tmp29 ;
4772 unsigned long __cil_tmp30 ;
4773 void *__cil_tmp31 ;
4774 char *__cil_tmp32 ;
4775 unsigned long *__cil_tmp33 ;
4776 unsigned long __cil_tmp34 ;
4777 unsigned long *__cil_tmp35 ;
4778 unsigned long __cil_tmp36 ;
4779 unsigned long __cil_tmp37 ;
4780 void *__cil_tmp38 ;
4781 char const *__cil_tmp39 ;
4782 void const *__cil_tmp40 ;
4783 char *__cil_tmp41 ;
4784 void *__cil_tmp42 ;
4785 char const *__cil_tmp43 ;
4786 void const *__cil_tmp44 ;
4787 unsigned int __cil_tmp45 ;
4788 unsigned long __cil_tmp46 ;
4789 unsigned long __cil_tmp47 ;
4790 struct work_struct *__cil_tmp48 ;
4791
4792 {
4793#line 325
4794 __mptr = (struct kmsg_dumper const *)dumper;
4795#line 325
4796 cxt = (struct mtdoops_context *)__mptr;
4797 {
4798#line 331
4799 __cil_tmp24 = (unsigned int )reason;
4800#line 331
4801 if (__cil_tmp24 != 1U) {
4802 {
4803#line 331
4804 __cil_tmp25 = (unsigned int )reason;
4805#line 331
4806 if (__cil_tmp25 != 0U) {
4807#line 333
4808 return;
4809 } else {
4810
4811 }
4812 }
4813 } else {
4814
4815 }
4816 }
4817 {
4818#line 336
4819 __cil_tmp26 = (unsigned int )reason;
4820#line 336
4821 if (__cil_tmp26 == 1U) {
4822 {
4823#line 336
4824 __cil_tmp27 = & dump_oops;
4825#line 336
4826 __cil_tmp28 = *__cil_tmp27;
4827#line 336
4828 if (__cil_tmp28 == 0) {
4829#line 337
4830 return;
4831 } else {
4832
4833 }
4834 }
4835 } else {
4836
4837 }
4838 }
4839#line 339
4840 __cil_tmp29 = (unsigned long )cxt;
4841#line 339
4842 __cil_tmp30 = __cil_tmp29 + 232;
4843#line 339
4844 __cil_tmp31 = *((void **)__cil_tmp30);
4845#line 339
4846 __cil_tmp32 = (char *)__cil_tmp31;
4847#line 339
4848 dst = __cil_tmp32 + 8U;
4849#line 340
4850 _min1 = l2;
4851#line 340
4852 __cil_tmp33 = & record_size;
4853#line 340
4854 __cil_tmp34 = *__cil_tmp33;
4855#line 340
4856 _min2 = __cil_tmp34 - 8UL;
4857#line 340
4858 if (_min1 < _min2) {
4859#line 340
4860 tmp = _min1;
4861 } else {
4862#line 340
4863 tmp = _min2;
4864 }
4865#line 340
4866 l2_cpy = tmp;
4867#line 341
4868 _min1___0 = l1;
4869#line 341
4870 __cil_tmp35 = & record_size;
4871#line 341
4872 __cil_tmp36 = *__cil_tmp35;
4873#line 341
4874 __cil_tmp37 = __cil_tmp36 - l2_cpy;
4875#line 341
4876 _min2___0 = __cil_tmp37 - 8UL;
4877#line 341
4878 if (_min1___0 < _min2___0) {
4879#line 341
4880 tmp___0 = _min1___0;
4881 } else {
4882#line 341
4883 tmp___0 = _min2___0;
4884 }
4885 {
4886#line 341
4887 l1_cpy = tmp___0;
4888#line 343
4889 s2_start = l2 - l2_cpy;
4890#line 344
4891 s1_start = l1 - l1_cpy;
4892#line 346
4893 __len = l1_cpy;
4894#line 346
4895 __cil_tmp38 = (void *)dst;
4896#line 346
4897 __cil_tmp39 = s1 + s1_start;
4898#line 346
4899 __cil_tmp40 = (void const *)__cil_tmp39;
4900#line 346
4901 __ret = __builtin_memcpy(__cil_tmp38, __cil_tmp40, __len);
4902#line 347
4903 __len___0 = l2_cpy;
4904#line 347
4905 __cil_tmp41 = dst + l1_cpy;
4906#line 347
4907 __cil_tmp42 = (void *)__cil_tmp41;
4908#line 347
4909 __cil_tmp43 = s2 + s2_start;
4910#line 347
4911 __cil_tmp44 = (void const *)__cil_tmp43;
4912#line 347
4913 __ret___0 = __builtin_memcpy(__cil_tmp42, __cil_tmp44, __len___0);
4914 }
4915 {
4916#line 350
4917 __cil_tmp45 = (unsigned int )reason;
4918#line 350
4919 if (__cil_tmp45 != 1U) {
4920 {
4921#line 351
4922 mtdoops_write(cxt, 1);
4923 }
4924 } else {
4925
4926 }
4927 }
4928 {
4929#line 354
4930 __cil_tmp46 = (unsigned long )cxt;
4931#line 354
4932 __cil_tmp47 = __cil_tmp46 + 120;
4933#line 354
4934 __cil_tmp48 = (struct work_struct *)__cil_tmp47;
4935#line 354
4936 schedule_work(__cil_tmp48);
4937 }
4938#line 355
4939 return;
4940}
4941}
4942#line 357 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
4943static void mtdoops_notify_add(struct mtd_info *mtd )
4944{ struct mtdoops_context *cxt ;
4945 u64 mtdoops_pages ;
4946 u64 tmp ;
4947 int err ;
4948 int tmp___0 ;
4949 void *tmp___1 ;
4950 unsigned long __cil_tmp8 ;
4951 unsigned long __cil_tmp9 ;
4952 uint64_t __cil_tmp10 ;
4953 unsigned long *__cil_tmp11 ;
4954 unsigned long __cil_tmp12 ;
4955 u32 __cil_tmp13 ;
4956 unsigned long __cil_tmp14 ;
4957 unsigned long __cil_tmp15 ;
4958 char const *__cil_tmp16 ;
4959 char const *__cil_tmp17 ;
4960 unsigned long __cil_tmp18 ;
4961 unsigned long __cil_tmp19 ;
4962 unsigned long __cil_tmp20 ;
4963 unsigned long __cil_tmp21 ;
4964 unsigned long __cil_tmp22 ;
4965 unsigned long __cil_tmp23 ;
4966 int __cil_tmp24 ;
4967 unsigned long __cil_tmp25 ;
4968 unsigned long __cil_tmp26 ;
4969 int __cil_tmp27 ;
4970 unsigned long __cil_tmp28 ;
4971 unsigned long __cil_tmp29 ;
4972 int __cil_tmp30 ;
4973 unsigned long __cil_tmp31 ;
4974 unsigned long __cil_tmp32 ;
4975 uint32_t __cil_tmp33 ;
4976 uint32_t __cil_tmp34 ;
4977 uint64_t __cil_tmp35 ;
4978 unsigned long __cil_tmp36 ;
4979 unsigned long __cil_tmp37 ;
4980 uint64_t __cil_tmp38 ;
4981 unsigned long __cil_tmp39 ;
4982 unsigned long __cil_tmp40 ;
4983 int __cil_tmp41 ;
4984 unsigned long *__cil_tmp42 ;
4985 unsigned long __cil_tmp43 ;
4986 unsigned long __cil_tmp44 ;
4987 unsigned long __cil_tmp45 ;
4988 uint32_t __cil_tmp46 ;
4989 unsigned long __cil_tmp47 ;
4990 unsigned long __cil_tmp48 ;
4991 unsigned long __cil_tmp49 ;
4992 int __cil_tmp50 ;
4993 unsigned long __cil_tmp51 ;
4994 unsigned long __cil_tmp52 ;
4995 uint64_t __cil_tmp53 ;
4996 unsigned long __cil_tmp54 ;
4997 unsigned long __cil_tmp55 ;
4998 int __cil_tmp56 ;
4999 u64 __cil_tmp57 ;
5000 u64 __cil_tmp58 ;
5001 unsigned long long __cil_tmp59 ;
5002 unsigned long __cil_tmp60 ;
5003 unsigned long __cil_tmp61 ;
5004 unsigned long __cil_tmp62 ;
5005 unsigned long *__cil_tmp63 ;
5006 unsigned long __cil_tmp64 ;
5007 unsigned long __cil_tmp65 ;
5008 unsigned long __cil_tmp66 ;
5009 unsigned long *__cil_tmp67 ;
5010 unsigned long __cil_tmp68 ;
5011 struct kmsg_dumper *__cil_tmp69 ;
5012 unsigned long __cil_tmp70 ;
5013 unsigned long __cil_tmp71 ;
5014 unsigned long *__cil_tmp72 ;
5015 void const *__cil_tmp73 ;
5016 unsigned long __cil_tmp74 ;
5017 unsigned long __cil_tmp75 ;
5018 unsigned long __cil_tmp76 ;
5019 unsigned long __cil_tmp77 ;
5020 unsigned long __cil_tmp78 ;
5021 unsigned long __cil_tmp79 ;
5022 unsigned long *__cil_tmp80 ;
5023 unsigned long __cil_tmp81 ;
5024 unsigned long __cil_tmp82 ;
5025 unsigned long __cil_tmp83 ;
5026 uint64_t __cil_tmp84 ;
5027 int __cil_tmp85 ;
5028 unsigned long __cil_tmp86 ;
5029 unsigned long __cil_tmp87 ;
5030 unsigned long __cil_tmp88 ;
5031 unsigned long __cil_tmp89 ;
5032 int __cil_tmp90 ;
5033
5034 {
5035 {
5036#line 359
5037 cxt = & oops_cxt;
5038#line 360
5039 __cil_tmp8 = (unsigned long )mtd;
5040#line 360
5041 __cil_tmp9 = __cil_tmp8 + 8;
5042#line 360
5043 __cil_tmp10 = *((uint64_t *)__cil_tmp9);
5044#line 360
5045 __cil_tmp11 = & record_size;
5046#line 360
5047 __cil_tmp12 = *__cil_tmp11;
5048#line 360
5049 __cil_tmp13 = (u32 )__cil_tmp12;
5050#line 360
5051 tmp = div_u64(__cil_tmp10, __cil_tmp13);
5052#line 360
5053 mtdoops_pages = tmp;
5054#line 363
5055 __cil_tmp14 = (unsigned long )mtd;
5056#line 363
5057 __cil_tmp15 = __cil_tmp14 + 56;
5058#line 363
5059 __cil_tmp16 = *((char const **)__cil_tmp15);
5060#line 363
5061 __cil_tmp17 = (char const *)(& mtddev);
5062#line 363
5063 tmp___0 = strcmp(__cil_tmp16, __cil_tmp17);
5064 }
5065#line 363
5066 if (tmp___0 == 0) {
5067#line 364
5068 __cil_tmp18 = (unsigned long )cxt;
5069#line 364
5070 __cil_tmp19 = __cil_tmp18 + 32;
5071#line 364
5072 __cil_tmp20 = (unsigned long )mtd;
5073#line 364
5074 __cil_tmp21 = __cil_tmp20 + 64;
5075#line 364
5076 *((int *)__cil_tmp19) = *((int *)__cil_tmp21);
5077 } else {
5078
5079 }
5080 {
5081#line 366
5082 __cil_tmp22 = (unsigned long )cxt;
5083#line 366
5084 __cil_tmp23 = __cil_tmp22 + 32;
5085#line 366
5086 __cil_tmp24 = *((int *)__cil_tmp23);
5087#line 366
5088 __cil_tmp25 = (unsigned long )mtd;
5089#line 366
5090 __cil_tmp26 = __cil_tmp25 + 64;
5091#line 366
5092 __cil_tmp27 = *((int *)__cil_tmp26);
5093#line 366
5094 if (__cil_tmp27 != __cil_tmp24) {
5095#line 367
5096 return;
5097 } else {
5098 {
5099#line 366
5100 __cil_tmp28 = (unsigned long )cxt;
5101#line 366
5102 __cil_tmp29 = __cil_tmp28 + 32;
5103#line 366
5104 __cil_tmp30 = *((int *)__cil_tmp29);
5105#line 366
5106 if (__cil_tmp30 < 0) {
5107#line 367
5108 return;
5109 } else {
5110
5111 }
5112 }
5113 }
5114 }
5115 {
5116#line 369
5117 __cil_tmp31 = (unsigned long )mtd;
5118#line 369
5119 __cil_tmp32 = __cil_tmp31 + 16;
5120#line 369
5121 __cil_tmp33 = *((uint32_t *)__cil_tmp32);
5122#line 369
5123 __cil_tmp34 = __cil_tmp33 * 2U;
5124#line 369
5125 __cil_tmp35 = (uint64_t )__cil_tmp34;
5126#line 369
5127 __cil_tmp36 = (unsigned long )mtd;
5128#line 369
5129 __cil_tmp37 = __cil_tmp36 + 8;
5130#line 369
5131 __cil_tmp38 = *((uint64_t *)__cil_tmp37);
5132#line 369
5133 if (__cil_tmp38 < __cil_tmp35) {
5134 {
5135#line 370
5136 __cil_tmp39 = (unsigned long )mtd;
5137#line 370
5138 __cil_tmp40 = __cil_tmp39 + 64;
5139#line 370
5140 __cil_tmp41 = *((int *)__cil_tmp40);
5141#line 370
5142 printk("<3>mtdoops: MTD partition %d not big enough for mtdoops\n", __cil_tmp41);
5143 }
5144#line 372
5145 return;
5146 } else {
5147
5148 }
5149 }
5150 {
5151#line 374
5152 __cil_tmp42 = & record_size;
5153#line 374
5154 __cil_tmp43 = *__cil_tmp42;
5155#line 374
5156 __cil_tmp44 = (unsigned long )mtd;
5157#line 374
5158 __cil_tmp45 = __cil_tmp44 + 16;
5159#line 374
5160 __cil_tmp46 = *((uint32_t *)__cil_tmp45);
5161#line 374
5162 __cil_tmp47 = (unsigned long )__cil_tmp46;
5163#line 374
5164 if (__cil_tmp47 < __cil_tmp43) {
5165 {
5166#line 375
5167 __cil_tmp48 = (unsigned long )mtd;
5168#line 375
5169 __cil_tmp49 = __cil_tmp48 + 64;
5170#line 375
5171 __cil_tmp50 = *((int *)__cil_tmp49);
5172#line 375
5173 printk("<3>mtdoops: eraseblock size of MTD partition %d too small\n", __cil_tmp50);
5174 }
5175#line 377
5176 return;
5177 } else {
5178
5179 }
5180 }
5181 {
5182#line 379
5183 __cil_tmp51 = (unsigned long )mtd;
5184#line 379
5185 __cil_tmp52 = __cil_tmp51 + 8;
5186#line 379
5187 __cil_tmp53 = *((uint64_t *)__cil_tmp52);
5188#line 379
5189 if (__cil_tmp53 > 8388608ULL) {
5190 {
5191#line 380
5192 __cil_tmp54 = (unsigned long )mtd;
5193#line 380
5194 __cil_tmp55 = __cil_tmp54 + 64;
5195#line 380
5196 __cil_tmp56 = *((int *)__cil_tmp55);
5197#line 380
5198 printk("<3>mtdoops: mtd%d is too large (limit is %d MiB)\n", __cil_tmp56, 8);
5199 }
5200#line 382
5201 return;
5202 } else {
5203
5204 }
5205 }
5206 {
5207#line 386
5208 __cil_tmp57 = mtdoops_pages + 63ULL;
5209#line 386
5210 __cil_tmp58 = __cil_tmp57 / 64ULL;
5211#line 386
5212 __cil_tmp59 = __cil_tmp58 * 8ULL;
5213#line 386
5214 __cil_tmp60 = (unsigned long )__cil_tmp59;
5215#line 386
5216 tmp___1 = ldv_vmalloc_19(__cil_tmp60);
5217#line 386
5218 __cil_tmp61 = (unsigned long )cxt;
5219#line 386
5220 __cil_tmp62 = __cil_tmp61 + 224;
5221#line 386
5222 *((unsigned long **)__cil_tmp62) = (unsigned long *)tmp___1;
5223 }
5224 {
5225#line 388
5226 __cil_tmp63 = (unsigned long *)0;
5227#line 388
5228 __cil_tmp64 = (unsigned long )__cil_tmp63;
5229#line 388
5230 __cil_tmp65 = (unsigned long )cxt;
5231#line 388
5232 __cil_tmp66 = __cil_tmp65 + 224;
5233#line 388
5234 __cil_tmp67 = *((unsigned long **)__cil_tmp66);
5235#line 388
5236 __cil_tmp68 = (unsigned long )__cil_tmp67;
5237#line 388
5238 if (__cil_tmp68 == __cil_tmp64) {
5239 {
5240#line 389
5241 printk("<3>mtdoops: could not allocate page array\n");
5242 }
5243#line 390
5244 return;
5245 } else {
5246
5247 }
5248 }
5249 {
5250#line 393
5251 *((void (**)(struct kmsg_dumper * , enum kmsg_dump_reason , char const * , unsigned long ,
5252 char const * , unsigned long ))cxt) = & mtdoops_do_dump;
5253#line 394
5254 __cil_tmp69 = (struct kmsg_dumper *)cxt;
5255#line 394
5256 err = kmsg_dump_register(__cil_tmp69);
5257 }
5258#line 395
5259 if (err != 0) {
5260 {
5261#line 396
5262 printk("<3>mtdoops: registering kmsg dumper failed, error %d\n", err);
5263#line 397
5264 __cil_tmp70 = (unsigned long )cxt;
5265#line 397
5266 __cil_tmp71 = __cil_tmp70 + 224;
5267#line 397
5268 __cil_tmp72 = *((unsigned long **)__cil_tmp71);
5269#line 397
5270 __cil_tmp73 = (void const *)__cil_tmp72;
5271#line 397
5272 vfree(__cil_tmp73);
5273#line 398
5274 __cil_tmp74 = (unsigned long )cxt;
5275#line 398
5276 __cil_tmp75 = __cil_tmp74 + 224;
5277#line 398
5278 *((unsigned long **)__cil_tmp75) = (unsigned long *)0;
5279 }
5280#line 399
5281 return;
5282 } else {
5283
5284 }
5285 {
5286#line 402
5287 __cil_tmp76 = (unsigned long )cxt;
5288#line 402
5289 __cil_tmp77 = __cil_tmp76 + 200;
5290#line 402
5291 *((struct mtd_info **)__cil_tmp77) = mtd;
5292#line 403
5293 __cil_tmp78 = (unsigned long )cxt;
5294#line 403
5295 __cil_tmp79 = __cil_tmp78 + 208;
5296#line 403
5297 __cil_tmp80 = & record_size;
5298#line 403
5299 __cil_tmp81 = *__cil_tmp80;
5300#line 403
5301 __cil_tmp82 = (unsigned long )mtd;
5302#line 403
5303 __cil_tmp83 = __cil_tmp82 + 8;
5304#line 403
5305 __cil_tmp84 = *((uint64_t *)__cil_tmp83);
5306#line 403
5307 __cil_tmp85 = (int )__cil_tmp84;
5308#line 403
5309 __cil_tmp86 = (unsigned long )__cil_tmp85;
5310#line 403
5311 __cil_tmp87 = __cil_tmp86 / __cil_tmp81;
5312#line 403
5313 *((int *)__cil_tmp79) = (int )__cil_tmp87;
5314#line 404
5315 find_next_position(cxt);
5316#line 405
5317 __cil_tmp88 = (unsigned long )mtd;
5318#line 405
5319 __cil_tmp89 = __cil_tmp88 + 64;
5320#line 405
5321 __cil_tmp90 = *((int *)__cil_tmp89);
5322#line 405
5323 printk("<6>mtdoops: Attached to MTD device %d\n", __cil_tmp90);
5324 }
5325#line 406
5326 return;
5327}
5328}
5329#line 408 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
5330static void mtdoops_notify_remove(struct mtd_info *mtd )
5331{ struct mtdoops_context *cxt ;
5332 int tmp ;
5333 unsigned long __cil_tmp4 ;
5334 unsigned long __cil_tmp5 ;
5335 int __cil_tmp6 ;
5336 unsigned long __cil_tmp7 ;
5337 unsigned long __cil_tmp8 ;
5338 int __cil_tmp9 ;
5339 unsigned long __cil_tmp10 ;
5340 unsigned long __cil_tmp11 ;
5341 int __cil_tmp12 ;
5342 struct kmsg_dumper *__cil_tmp13 ;
5343 unsigned long __cil_tmp14 ;
5344 unsigned long __cil_tmp15 ;
5345 unsigned long __cil_tmp16 ;
5346 unsigned long __cil_tmp17 ;
5347 struct work_struct *__cil_tmp18 ;
5348 unsigned long __cil_tmp19 ;
5349 unsigned long __cil_tmp20 ;
5350 struct work_struct *__cil_tmp21 ;
5351
5352 {
5353#line 410
5354 cxt = & oops_cxt;
5355 {
5356#line 412
5357 __cil_tmp4 = (unsigned long )cxt;
5358#line 412
5359 __cil_tmp5 = __cil_tmp4 + 32;
5360#line 412
5361 __cil_tmp6 = *((int *)__cil_tmp5);
5362#line 412
5363 __cil_tmp7 = (unsigned long )mtd;
5364#line 412
5365 __cil_tmp8 = __cil_tmp7 + 64;
5366#line 412
5367 __cil_tmp9 = *((int *)__cil_tmp8);
5368#line 412
5369 if (__cil_tmp9 != __cil_tmp6) {
5370#line 413
5371 return;
5372 } else {
5373 {
5374#line 412
5375 __cil_tmp10 = (unsigned long )cxt;
5376#line 412
5377 __cil_tmp11 = __cil_tmp10 + 32;
5378#line 412
5379 __cil_tmp12 = *((int *)__cil_tmp11);
5380#line 412
5381 if (__cil_tmp12 < 0) {
5382#line 413
5383 return;
5384 } else {
5385
5386 }
5387 }
5388 }
5389 }
5390 {
5391#line 415
5392 __cil_tmp13 = (struct kmsg_dumper *)cxt;
5393#line 415
5394 tmp = kmsg_dump_unregister(__cil_tmp13);
5395 }
5396#line 415
5397 if (tmp < 0) {
5398 {
5399#line 416
5400 printk("<4>mtdoops: could not unregister kmsg_dumper\n");
5401 }
5402 } else {
5403
5404 }
5405 {
5406#line 418
5407 __cil_tmp14 = (unsigned long )cxt;
5408#line 418
5409 __cil_tmp15 = __cil_tmp14 + 200;
5410#line 418
5411 *((struct mtd_info **)__cil_tmp15) = (struct mtd_info *)0;
5412#line 419
5413 __cil_tmp16 = (unsigned long )cxt;
5414#line 419
5415 __cil_tmp17 = __cil_tmp16 + 40;
5416#line 419
5417 __cil_tmp18 = (struct work_struct *)__cil_tmp17;
5418#line 419
5419 flush_work_sync(__cil_tmp18);
5420#line 420
5421 __cil_tmp19 = (unsigned long )cxt;
5422#line 420
5423 __cil_tmp20 = __cil_tmp19 + 120;
5424#line 420
5425 __cil_tmp21 = (struct work_struct *)__cil_tmp20;
5426#line 420
5427 flush_work_sync(__cil_tmp21);
5428 }
5429#line 421
5430 return;
5431}
5432}
5433#line 424 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
5434static struct mtd_notifier mtdoops_notifier = {& mtdoops_notify_add, & mtdoops_notify_remove, {(struct list_head *)0, (struct list_head *)0}};
5435#line 429 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
5436static int mtdoops_init(void)
5437{ struct mtdoops_context *cxt ;
5438 int mtd_index ;
5439 char *endp ;
5440 size_t tmp ;
5441 unsigned long tmp___0 ;
5442 struct lock_class_key __key ;
5443 atomic_long_t __constr_expr_0 ;
5444 struct lock_class_key __key___0 ;
5445 atomic_long_t __constr_expr_1 ;
5446 char const *__cil_tmp10 ;
5447 unsigned long *__cil_tmp11 ;
5448 unsigned long __cil_tmp12 ;
5449 unsigned long __cil_tmp13 ;
5450 unsigned long *__cil_tmp14 ;
5451 unsigned long __cil_tmp15 ;
5452 unsigned long __cil_tmp16 ;
5453 unsigned long __cil_tmp17 ;
5454 char const *__cil_tmp18 ;
5455 char **__cil_tmp19 ;
5456 char *__cil_tmp20 ;
5457 char __cil_tmp21 ;
5458 signed char __cil_tmp22 ;
5459 int __cil_tmp23 ;
5460 unsigned long __cil_tmp24 ;
5461 unsigned long __cil_tmp25 ;
5462 unsigned long __cil_tmp26 ;
5463 unsigned long __cil_tmp27 ;
5464 unsigned long *__cil_tmp28 ;
5465 unsigned long __cil_tmp29 ;
5466 void *__cil_tmp30 ;
5467 unsigned long __cil_tmp31 ;
5468 unsigned long __cil_tmp32 ;
5469 unsigned long __cil_tmp33 ;
5470 void *__cil_tmp34 ;
5471 unsigned long __cil_tmp35 ;
5472 unsigned long __cil_tmp36 ;
5473 unsigned long __cil_tmp37 ;
5474 void *__cil_tmp38 ;
5475 unsigned long *__cil_tmp39 ;
5476 unsigned long __cil_tmp40 ;
5477 unsigned long __cil_tmp41 ;
5478 unsigned long __cil_tmp42 ;
5479 struct work_struct *__cil_tmp43 ;
5480 unsigned long __cil_tmp44 ;
5481 unsigned long __cil_tmp45 ;
5482 unsigned long __cil_tmp46 ;
5483 unsigned long __cil_tmp47 ;
5484 unsigned long __cil_tmp48 ;
5485 struct lockdep_map *__cil_tmp49 ;
5486 unsigned long __cil_tmp50 ;
5487 unsigned long __cil_tmp51 ;
5488 unsigned long __cil_tmp52 ;
5489 struct list_head *__cil_tmp53 ;
5490 unsigned long __cil_tmp54 ;
5491 unsigned long __cil_tmp55 ;
5492 unsigned long __cil_tmp56 ;
5493 unsigned long __cil_tmp57 ;
5494 unsigned long __cil_tmp58 ;
5495 struct work_struct *__cil_tmp59 ;
5496 unsigned long __cil_tmp60 ;
5497 unsigned long __cil_tmp61 ;
5498 unsigned long __cil_tmp62 ;
5499 unsigned long __cil_tmp63 ;
5500 unsigned long __cil_tmp64 ;
5501 struct lockdep_map *__cil_tmp65 ;
5502 unsigned long __cil_tmp66 ;
5503 unsigned long __cil_tmp67 ;
5504 unsigned long __cil_tmp68 ;
5505 struct list_head *__cil_tmp69 ;
5506 unsigned long __cil_tmp70 ;
5507 unsigned long __cil_tmp71 ;
5508 unsigned long __cil_tmp72 ;
5509 long __constr_expr_0_counter73 ;
5510 long __constr_expr_1_counter74 ;
5511
5512 {
5513 {
5514#line 431
5515 cxt = & oops_cxt;
5516#line 435
5517 __cil_tmp10 = (char const *)(& mtddev);
5518#line 435
5519 tmp = strlen(__cil_tmp10);
5520 }
5521#line 435
5522 if (tmp == 0UL) {
5523 {
5524#line 436
5525 printk("<3>mtdoops: mtd device (mtddev=name/number) must be supplied\n");
5526 }
5527#line 437
5528 return (-22);
5529 } else {
5530
5531 }
5532 {
5533#line 439
5534 __cil_tmp11 = & record_size;
5535#line 439
5536 __cil_tmp12 = *__cil_tmp11;
5537#line 439
5538 __cil_tmp13 = __cil_tmp12 & 4095UL;
5539#line 439
5540 if (__cil_tmp13 != 0UL) {
5541 {
5542#line 440
5543 printk("<3>mtdoops: record_size must be a multiple of 4096\n");
5544 }
5545#line 441
5546 return (-22);
5547 } else {
5548
5549 }
5550 }
5551 {
5552#line 443
5553 __cil_tmp14 = & record_size;
5554#line 443
5555 __cil_tmp15 = *__cil_tmp14;
5556#line 443
5557 if (__cil_tmp15 <= 4095UL) {
5558 {
5559#line 444
5560 printk("<3>mtdoops: record_size must be over 4096 bytes\n");
5561 }
5562#line 445
5563 return (-22);
5564 } else {
5565
5566 }
5567 }
5568 {
5569#line 449
5570 __cil_tmp16 = (unsigned long )cxt;
5571#line 449
5572 __cil_tmp17 = __cil_tmp16 + 32;
5573#line 449
5574 *((int *)__cil_tmp17) = -1;
5575#line 450
5576 __cil_tmp18 = (char const *)(& mtddev);
5577#line 450
5578 tmp___0 = simple_strtoul(__cil_tmp18, & endp, 0U);
5579#line 450
5580 mtd_index = (int )tmp___0;
5581 }
5582 {
5583#line 451
5584 __cil_tmp19 = & endp;
5585#line 451
5586 __cil_tmp20 = *__cil_tmp19;
5587#line 451
5588 __cil_tmp21 = *__cil_tmp20;
5589#line 451
5590 __cil_tmp22 = (signed char )__cil_tmp21;
5591#line 451
5592 __cil_tmp23 = (int )__cil_tmp22;
5593#line 451
5594 if (__cil_tmp23 == 0) {
5595#line 452
5596 __cil_tmp24 = (unsigned long )cxt;
5597#line 452
5598 __cil_tmp25 = __cil_tmp24 + 32;
5599#line 452
5600 *((int *)__cil_tmp25) = mtd_index;
5601 } else {
5602
5603 }
5604 }
5605 {
5606#line 454
5607 __cil_tmp26 = (unsigned long )cxt;
5608#line 454
5609 __cil_tmp27 = __cil_tmp26 + 232;
5610#line 454
5611 __cil_tmp28 = & record_size;
5612#line 454
5613 __cil_tmp29 = *__cil_tmp28;
5614#line 454
5615 *((void **)__cil_tmp27) = ldv_vmalloc_20(__cil_tmp29);
5616 }
5617 {
5618#line 455
5619 __cil_tmp30 = (void *)0;
5620#line 455
5621 __cil_tmp31 = (unsigned long )__cil_tmp30;
5622#line 455
5623 __cil_tmp32 = (unsigned long )cxt;
5624#line 455
5625 __cil_tmp33 = __cil_tmp32 + 232;
5626#line 455
5627 __cil_tmp34 = *((void **)__cil_tmp33);
5628#line 455
5629 __cil_tmp35 = (unsigned long )__cil_tmp34;
5630#line 455
5631 if (__cil_tmp35 == __cil_tmp31) {
5632 {
5633#line 456
5634 printk("<3>mtdoops: failed to allocate buffer workspace\n");
5635 }
5636#line 457
5637 return (-12);
5638 } else {
5639
5640 }
5641 }
5642 {
5643#line 459
5644 __cil_tmp36 = (unsigned long )cxt;
5645#line 459
5646 __cil_tmp37 = __cil_tmp36 + 232;
5647#line 459
5648 __cil_tmp38 = *((void **)__cil_tmp37);
5649#line 459
5650 __cil_tmp39 = & record_size;
5651#line 459
5652 __cil_tmp40 = *__cil_tmp39;
5653#line 459
5654 memset(__cil_tmp38, 255, __cil_tmp40);
5655#line 461
5656 __cil_tmp41 = (unsigned long )cxt;
5657#line 461
5658 __cil_tmp42 = __cil_tmp41 + 40;
5659#line 461
5660 __cil_tmp43 = (struct work_struct *)__cil_tmp42;
5661#line 461
5662 __init_work(__cil_tmp43, 0);
5663#line 461
5664 __constr_expr_0_counter73 = 2097664L;
5665#line 461
5666 __cil_tmp44 = (unsigned long )cxt;
5667#line 461
5668 __cil_tmp45 = __cil_tmp44 + 40;
5669#line 461
5670 ((atomic_long_t *)__cil_tmp45)->counter = __constr_expr_0_counter73;
5671#line 461
5672 __cil_tmp46 = 40 + 32;
5673#line 461
5674 __cil_tmp47 = (unsigned long )cxt;
5675#line 461
5676 __cil_tmp48 = __cil_tmp47 + __cil_tmp46;
5677#line 461
5678 __cil_tmp49 = (struct lockdep_map *)__cil_tmp48;
5679#line 461
5680 lockdep_init_map(__cil_tmp49, "(&cxt->work_erase)", & __key, 0);
5681#line 461
5682 __cil_tmp50 = 40 + 8;
5683#line 461
5684 __cil_tmp51 = (unsigned long )cxt;
5685#line 461
5686 __cil_tmp52 = __cil_tmp51 + __cil_tmp50;
5687#line 461
5688 __cil_tmp53 = (struct list_head *)__cil_tmp52;
5689#line 461
5690 INIT_LIST_HEAD(__cil_tmp53);
5691#line 461
5692 __cil_tmp54 = 40 + 24;
5693#line 461
5694 __cil_tmp55 = (unsigned long )cxt;
5695#line 461
5696 __cil_tmp56 = __cil_tmp55 + __cil_tmp54;
5697#line 461
5698 *((void (**)(struct work_struct * ))__cil_tmp56) = & mtdoops_workfunc_erase;
5699#line 462
5700 __cil_tmp57 = (unsigned long )cxt;
5701#line 462
5702 __cil_tmp58 = __cil_tmp57 + 120;
5703#line 462
5704 __cil_tmp59 = (struct work_struct *)__cil_tmp58;
5705#line 462
5706 __init_work(__cil_tmp59, 0);
5707#line 462
5708 __constr_expr_1_counter74 = 2097664L;
5709#line 462
5710 __cil_tmp60 = (unsigned long )cxt;
5711#line 462
5712 __cil_tmp61 = __cil_tmp60 + 120;
5713#line 462
5714 ((atomic_long_t *)__cil_tmp61)->counter = __constr_expr_1_counter74;
5715#line 462
5716 __cil_tmp62 = 120 + 32;
5717#line 462
5718 __cil_tmp63 = (unsigned long )cxt;
5719#line 462
5720 __cil_tmp64 = __cil_tmp63 + __cil_tmp62;
5721#line 462
5722 __cil_tmp65 = (struct lockdep_map *)__cil_tmp64;
5723#line 462
5724 lockdep_init_map(__cil_tmp65, "(&cxt->work_write)", & __key___0, 0);
5725#line 462
5726 __cil_tmp66 = 120 + 8;
5727#line 462
5728 __cil_tmp67 = (unsigned long )cxt;
5729#line 462
5730 __cil_tmp68 = __cil_tmp67 + __cil_tmp66;
5731#line 462
5732 __cil_tmp69 = (struct list_head *)__cil_tmp68;
5733#line 462
5734 INIT_LIST_HEAD(__cil_tmp69);
5735#line 462
5736 __cil_tmp70 = 120 + 24;
5737#line 462
5738 __cil_tmp71 = (unsigned long )cxt;
5739#line 462
5740 __cil_tmp72 = __cil_tmp71 + __cil_tmp70;
5741#line 462
5742 *((void (**)(struct work_struct * ))__cil_tmp72) = & mtdoops_workfunc_write;
5743#line 464
5744 register_mtd_user(& mtdoops_notifier);
5745 }
5746#line 465
5747 return (0);
5748}
5749}
5750#line 468 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
5751static void mtdoops_exit(void)
5752{ struct mtdoops_context *cxt ;
5753 unsigned long __cil_tmp2 ;
5754 unsigned long __cil_tmp3 ;
5755 void *__cil_tmp4 ;
5756 void const *__cil_tmp5 ;
5757 unsigned long __cil_tmp6 ;
5758 unsigned long __cil_tmp7 ;
5759 unsigned long *__cil_tmp8 ;
5760 void const *__cil_tmp9 ;
5761
5762 {
5763 {
5764#line 470
5765 cxt = & oops_cxt;
5766#line 472
5767 unregister_mtd_user(& mtdoops_notifier);
5768#line 473
5769 __cil_tmp2 = (unsigned long )cxt;
5770#line 473
5771 __cil_tmp3 = __cil_tmp2 + 232;
5772#line 473
5773 __cil_tmp4 = *((void **)__cil_tmp3);
5774#line 473
5775 __cil_tmp5 = (void const *)__cil_tmp4;
5776#line 473
5777 vfree(__cil_tmp5);
5778#line 474
5779 __cil_tmp6 = (unsigned long )cxt;
5780#line 474
5781 __cil_tmp7 = __cil_tmp6 + 224;
5782#line 474
5783 __cil_tmp8 = *((unsigned long **)__cil_tmp7);
5784#line 474
5785 __cil_tmp9 = (void const *)__cil_tmp8;
5786#line 474
5787 vfree(__cil_tmp9);
5788 }
5789#line 475
5790 return;
5791}
5792}
5793#line 501
5794extern void ldv_check_final_state(void) ;
5795#line 507
5796extern void ldv_initialize(void) ;
5797#line 510
5798extern int __VERIFIER_nondet_int(void) ;
5799#line 513 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
5800int LDV_IN_INTERRUPT ;
5801#line 516 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
5802void main(void)
5803{ struct mtd_info *var_group1 ;
5804 int tmp ;
5805 int tmp___0 ;
5806 int tmp___1 ;
5807
5808 {
5809 {
5810#line 544
5811 LDV_IN_INTERRUPT = 1;
5812#line 553
5813 ldv_initialize();
5814#line 563
5815 tmp = mtdoops_init();
5816 }
5817#line 563
5818 if (tmp != 0) {
5819#line 564
5820 goto ldv_final;
5821 } else {
5822
5823 }
5824#line 568
5825 goto ldv_20496;
5826 ldv_20495:
5827 {
5828#line 571
5829 tmp___0 = __VERIFIER_nondet_int();
5830 }
5831#line 573
5832 if (tmp___0 == 0) {
5833#line 573
5834 goto case_0;
5835 } else
5836#line 593
5837 if (tmp___0 == 1) {
5838#line 593
5839 goto case_1;
5840 } else {
5841 {
5842#line 613
5843 goto switch_default;
5844#line 571
5845 if (0) {
5846 case_0:
5847 {
5848#line 585
5849 mtdoops_notify_add(var_group1);
5850 }
5851#line 592
5852 goto ldv_20492;
5853 case_1:
5854 {
5855#line 605
5856 mtdoops_notify_remove(var_group1);
5857 }
5858#line 612
5859 goto ldv_20492;
5860 switch_default: ;
5861#line 613
5862 goto ldv_20492;
5863 } else {
5864 switch_break: ;
5865 }
5866 }
5867 }
5868 ldv_20492: ;
5869 ldv_20496:
5870 {
5871#line 568
5872 tmp___1 = __VERIFIER_nondet_int();
5873 }
5874#line 568
5875 if (tmp___1 != 0) {
5876#line 569
5877 goto ldv_20495;
5878 } else {
5879#line 571
5880 goto ldv_20497;
5881 }
5882 ldv_20497: ;
5883 {
5884#line 629
5885 mtdoops_exit();
5886 }
5887 ldv_final:
5888 {
5889#line 632
5890 ldv_check_final_state();
5891 }
5892#line 635
5893 return;
5894}
5895}
5896#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
5897void ldv_blast_assert(void)
5898{
5899
5900 {
5901 ERROR: ;
5902#line 6
5903 goto ERROR;
5904}
5905}
5906#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
5907extern int __VERIFIER_nondet_int(void) ;
5908#line 656 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
5909int ldv_spin = 0;
5910#line 660 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
5911void ldv_check_alloc_flags(gfp_t flags )
5912{
5913
5914 {
5915#line 663
5916 if (ldv_spin != 0) {
5917#line 663
5918 if (flags != 32U) {
5919 {
5920#line 663
5921 ldv_blast_assert();
5922 }
5923 } else {
5924
5925 }
5926 } else {
5927
5928 }
5929#line 666
5930 return;
5931}
5932}
5933#line 666
5934extern struct page *ldv_some_page(void) ;
5935#line 669 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
5936struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags )
5937{ struct page *tmp ;
5938
5939 {
5940#line 672
5941 if (ldv_spin != 0) {
5942#line 672
5943 if (flags != 32U) {
5944 {
5945#line 672
5946 ldv_blast_assert();
5947 }
5948 } else {
5949
5950 }
5951 } else {
5952
5953 }
5954 {
5955#line 674
5956 tmp = ldv_some_page();
5957 }
5958#line 674
5959 return (tmp);
5960}
5961}
5962#line 678 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
5963void ldv_check_alloc_nonatomic(void)
5964{
5965
5966 {
5967#line 681
5968 if (ldv_spin != 0) {
5969 {
5970#line 681
5971 ldv_blast_assert();
5972 }
5973 } else {
5974
5975 }
5976#line 684
5977 return;
5978}
5979}
5980#line 685 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
5981void ldv_spin_lock(void)
5982{
5983
5984 {
5985#line 688
5986 ldv_spin = 1;
5987#line 689
5988 return;
5989}
5990}
5991#line 692 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
5992void ldv_spin_unlock(void)
5993{
5994
5995 {
5996#line 695
5997 ldv_spin = 0;
5998#line 696
5999 return;
6000}
6001}
6002#line 699 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
6003int ldv_spin_trylock(void)
6004{ int is_lock ;
6005
6006 {
6007 {
6008#line 704
6009 is_lock = __VERIFIER_nondet_int();
6010 }
6011#line 706
6012 if (is_lock != 0) {
6013#line 709
6014 return (0);
6015 } else {
6016#line 714
6017 ldv_spin = 1;
6018#line 716
6019 return (1);
6020 }
6021}
6022}
6023#line 883 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
6024void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 )
6025{
6026
6027 {
6028 {
6029#line 889
6030 ldv_check_alloc_flags(ldv_func_arg2);
6031#line 891
6032 kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
6033 }
6034#line 892
6035 return ((void *)0);
6036}
6037}
6038#line 915 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
6039void *ldv_vmalloc_19(unsigned long ldv_func_arg1 )
6040{
6041
6042 {
6043 {
6044#line 920
6045 ldv_check_alloc_nonatomic();
6046#line 922
6047 vmalloc(ldv_func_arg1);
6048 }
6049#line 923
6050 return ((void *)0);
6051}
6052}
6053#line 925 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
6054void *ldv_vmalloc_20(unsigned long ldv_func_arg1 )
6055{
6056
6057 {
6058 {
6059#line 930
6060 ldv_check_alloc_nonatomic();
6061#line 932
6062 vmalloc(ldv_func_arg1);
6063 }
6064#line 933
6065 return ((void *)0);
6066}
6067}