1
2
3
4#line 43 "include/asm-generic/int-ll64.h"
5typedef unsigned char u8;
6#line 46 "include/asm-generic/int-ll64.h"
7typedef unsigned short u16;
8#line 49 "include/asm-generic/int-ll64.h"
9typedef unsigned int u32;
10#line 52 "include/asm-generic/int-ll64.h"
11typedef unsigned long long u64;
12#line 14 "include/asm-generic/posix_types.h"
13typedef long __kernel_long_t;
14#line 15 "include/asm-generic/posix_types.h"
15typedef unsigned long __kernel_ulong_t;
16#line 75 "include/asm-generic/posix_types.h"
17typedef __kernel_ulong_t __kernel_size_t;
18#line 76 "include/asm-generic/posix_types.h"
19typedef __kernel_long_t __kernel_ssize_t;
20#line 27 "include/linux/types.h"
21typedef unsigned short umode_t;
22#line 63 "include/linux/types.h"
23typedef __kernel_size_t size_t;
24#line 68 "include/linux/types.h"
25typedef __kernel_ssize_t ssize_t;
26#line 202 "include/linux/types.h"
27typedef unsigned int gfp_t;
28#line 221 "include/linux/types.h"
29struct __anonstruct_atomic_t_6 {
30 int counter ;
31};
32#line 221 "include/linux/types.h"
33typedef struct __anonstruct_atomic_t_6 atomic_t;
34#line 226 "include/linux/types.h"
35struct __anonstruct_atomic64_t_7 {
36 long counter ;
37};
38#line 226 "include/linux/types.h"
39typedef struct __anonstruct_atomic64_t_7 atomic64_t;
40#line 227 "include/linux/types.h"
41struct list_head {
42 struct list_head *next ;
43 struct list_head *prev ;
44};
45#line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
46struct page;
47#line 58
48struct page;
49#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
50struct arch_spinlock;
51#line 327
52struct arch_spinlock;
53#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
54struct kmem_cache;
55#line 23 "include/asm-generic/atomic-long.h"
56typedef atomic64_t atomic_long_t;
57#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
58typedef u16 __ticket_t;
59#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
60typedef u32 __ticketpair_t;
61#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
62struct __raw_tickets {
63 __ticket_t head ;
64 __ticket_t tail ;
65};
66#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
67union __anonunion_ldv_5907_29 {
68 __ticketpair_t head_tail ;
69 struct __raw_tickets tickets ;
70};
71#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
72struct arch_spinlock {
73 union __anonunion_ldv_5907_29 ldv_5907 ;
74};
75#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
76typedef struct arch_spinlock arch_spinlock_t;
77#line 34 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
78struct lockdep_map;
79#line 34
80struct lockdep_map;
81#line 55 "include/linux/debug_locks.h"
82struct stack_trace {
83 unsigned int nr_entries ;
84 unsigned int max_entries ;
85 unsigned long *entries ;
86 int skip ;
87};
88#line 26 "include/linux/stacktrace.h"
89struct lockdep_subclass_key {
90 char __one_byte ;
91};
92#line 53 "include/linux/lockdep.h"
93struct lock_class_key {
94 struct lockdep_subclass_key subkeys[8U] ;
95};
96#line 59 "include/linux/lockdep.h"
97struct lock_class {
98 struct list_head hash_entry ;
99 struct list_head lock_entry ;
100 struct lockdep_subclass_key *key ;
101 unsigned int subclass ;
102 unsigned int dep_gen_id ;
103 unsigned long usage_mask ;
104 struct stack_trace usage_traces[13U] ;
105 struct list_head locks_after ;
106 struct list_head locks_before ;
107 unsigned int version ;
108 unsigned long ops ;
109 char const *name ;
110 int name_version ;
111 unsigned long contention_point[4U] ;
112 unsigned long contending_point[4U] ;
113};
114#line 144 "include/linux/lockdep.h"
115struct lockdep_map {
116 struct lock_class_key *key ;
117 struct lock_class *class_cache[2U] ;
118 char const *name ;
119 int cpu ;
120 unsigned long ip ;
121};
122#line 556 "include/linux/lockdep.h"
123struct raw_spinlock {
124 arch_spinlock_t raw_lock ;
125 unsigned int magic ;
126 unsigned int owner_cpu ;
127 void *owner ;
128 struct lockdep_map dep_map ;
129};
130#line 33 "include/linux/spinlock_types.h"
131struct __anonstruct_ldv_6122_33 {
132 u8 __padding[24U] ;
133 struct lockdep_map dep_map ;
134};
135#line 33 "include/linux/spinlock_types.h"
136union __anonunion_ldv_6123_32 {
137 struct raw_spinlock rlock ;
138 struct __anonstruct_ldv_6122_33 ldv_6122 ;
139};
140#line 33 "include/linux/spinlock_types.h"
141struct spinlock {
142 union __anonunion_ldv_6123_32 ldv_6123 ;
143};
144#line 76 "include/linux/spinlock_types.h"
145typedef struct spinlock spinlock_t;
146#line 445 "include/linux/elf.h"
147struct sock;
148#line 445
149struct sock;
150#line 446
151struct kobject;
152#line 446
153struct kobject;
154#line 447
155enum kobj_ns_type {
156 KOBJ_NS_TYPE_NONE = 0,
157 KOBJ_NS_TYPE_NET = 1,
158 KOBJ_NS_TYPES = 2
159} ;
160#line 453 "include/linux/elf.h"
161struct kobj_ns_type_operations {
162 enum kobj_ns_type type ;
163 void *(*grab_current_ns)(void) ;
164 void const *(*netlink_ns)(struct sock * ) ;
165 void const *(*initial_ns)(void) ;
166 void (*drop_ns)(void * ) ;
167};
168#line 57 "include/linux/kobject_ns.h"
169struct attribute {
170 char const *name ;
171 umode_t mode ;
172 struct lock_class_key *key ;
173 struct lock_class_key skey ;
174};
175#line 98 "include/linux/sysfs.h"
176struct sysfs_ops {
177 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
178 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
179 void const *(*namespace)(struct kobject * , struct attribute const * ) ;
180};
181#line 117
182struct sysfs_dirent;
183#line 117
184struct sysfs_dirent;
185#line 182 "include/linux/sysfs.h"
186struct kref {
187 atomic_t refcount ;
188};
189#line 49 "include/linux/kobject.h"
190struct kset;
191#line 49
192struct kobj_type;
193#line 49 "include/linux/kobject.h"
194struct kobject {
195 char const *name ;
196 struct list_head entry ;
197 struct kobject *parent ;
198 struct kset *kset ;
199 struct kobj_type *ktype ;
200 struct sysfs_dirent *sd ;
201 struct kref kref ;
202 unsigned char state_initialized : 1 ;
203 unsigned char state_in_sysfs : 1 ;
204 unsigned char state_add_uevent_sent : 1 ;
205 unsigned char state_remove_uevent_sent : 1 ;
206 unsigned char uevent_suppress : 1 ;
207};
208#line 107 "include/linux/kobject.h"
209struct kobj_type {
210 void (*release)(struct kobject * ) ;
211 struct sysfs_ops const *sysfs_ops ;
212 struct attribute **default_attrs ;
213 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject * ) ;
214 void const *(*namespace)(struct kobject * ) ;
215};
216#line 115 "include/linux/kobject.h"
217struct kobj_uevent_env {
218 char *envp[32U] ;
219 int envp_idx ;
220 char buf[2048U] ;
221 int buflen ;
222};
223#line 122 "include/linux/kobject.h"
224struct kset_uevent_ops {
225 int (* const filter)(struct kset * , struct kobject * ) ;
226 char const *(* const name)(struct kset * , struct kobject * ) ;
227 int (* const uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
228};
229#line 139 "include/linux/kobject.h"
230struct kset {
231 struct list_head list ;
232 spinlock_t list_lock ;
233 struct kobject kobj ;
234 struct kset_uevent_ops const *uevent_ops ;
235};
236#line 88 "include/linux/kmemleak.h"
237struct kmem_cache_cpu {
238 void **freelist ;
239 unsigned long tid ;
240 struct page *page ;
241 struct page *partial ;
242 int node ;
243 unsigned int stat[26U] ;
244};
245#line 55 "include/linux/slub_def.h"
246struct kmem_cache_node {
247 spinlock_t list_lock ;
248 unsigned long nr_partial ;
249 struct list_head partial ;
250 atomic_long_t nr_slabs ;
251 atomic_long_t total_objects ;
252 struct list_head full ;
253};
254#line 66 "include/linux/slub_def.h"
255struct kmem_cache_order_objects {
256 unsigned long x ;
257};
258#line 76 "include/linux/slub_def.h"
259struct kmem_cache {
260 struct kmem_cache_cpu *cpu_slab ;
261 unsigned long flags ;
262 unsigned long min_partial ;
263 int size ;
264 int objsize ;
265 int offset ;
266 int cpu_partial ;
267 struct kmem_cache_order_objects oo ;
268 struct kmem_cache_order_objects max ;
269 struct kmem_cache_order_objects min ;
270 gfp_t allocflags ;
271 int refcount ;
272 void (*ctor)(void * ) ;
273 int inuse ;
274 int align ;
275 int reserved ;
276 char const *name ;
277 struct list_head list ;
278 struct kobject kobj ;
279 int remote_node_defrag_ratio ;
280 struct kmem_cache_node *node[1024U] ;
281};
282#line 1650 "include/linux/input.h"
283struct rc_map_table {
284 u32 scancode ;
285 u32 keycode ;
286};
287#line 35 "include/media/rc-map.h"
288struct rc_map {
289 struct rc_map_table *scan ;
290 unsigned int size ;
291 unsigned int len ;
292 unsigned int alloc ;
293 u64 rc_type ;
294 char const *name ;
295 spinlock_t lock ;
296};
297#line 45 "include/media/rc-map.h"
298struct rc_map_list {
299 struct list_head list ;
300 struct rc_map map ;
301};
302#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9139/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-dib0700-rc5.c.p"
303void ldv_spin_lock(void) ;
304#line 3
305void ldv_spin_unlock(void) ;
306#line 4
307int ldv_spin_trylock(void) ;
308#line 220 "include/linux/slub_def.h"
309extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t ) ;
310#line 223
311void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
312#line 11 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9139/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-dib0700-rc5.c.p"
313void ldv_check_alloc_flags(gfp_t flags ) ;
314#line 12
315void ldv_check_alloc_nonatomic(void) ;
316#line 14
317struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
318#line 53 "include/media/rc-map.h"
319extern int rc_map_register(struct rc_map_list * ) ;
320#line 54
321extern void rc_map_unregister(struct rc_map_list * ) ;
322#line 36 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9139/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-dib0700-rc5.c.p"
323static struct rc_map_table dib0700_rc5_table[180U] =
324#line 36 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9139/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-dib0700-rc5.c.p"
325 { {1792U, 113U},
326 {1793U, 139U},
327 {1849U, 116U},
328 {1795U, 115U},
329 {1801U, 114U},
330 {1798U, 402U},
331 {1804U, 403U},
332 {1807U, 2U},
333 {1813U, 3U},
334 {1808U, 4U},
335 {1816U, 5U},
336 {1819U, 6U},
337 {1822U, 7U},
338 {1809U, 8U},
339 {1825U, 9U},
340 {1810U, 10U},
341 {1831U, 11U},
342 {1828U, 375U},
343 {1834U, 388U},
344 {1837U, 168U},
345 {1840U, 207U},
346 {1843U, 208U},
347 {1846U, 167U},
348 {1852U, 128U},
349 {1855U, 223U},
350 {60161U, 116U},
351 {60162U, 2U},
352 {60163U, 3U},
353 {60164U, 4U},
354 {60165U, 5U},
355 {60166U, 6U},
356 {60167U, 7U},
357 {60168U, 8U},
358 {60169U, 9U},
359 {60170U, 10U},
360 {60171U, 393U},
361 {60172U, 11U},
362 {60173U, 173U},
363 {60175U, 365U},
364 {60176U, 103U},
365 {60177U, 105U},
366 {60178U, 352U},
367 {60179U, 106U},
368 {60180U, 108U},
369 {60182U, 358U},
370 {60183U, 398U},
371 {60184U, 399U},
372 {60185U, 400U},
373 {60186U, 401U},
374 {60187U, 402U},
375 {60188U, 115U},
376 {60189U, 113U},
377 {60190U, 114U},
378 {60191U, 403U},
379 {60224U, 119U},
380 {60225U, 102U},
381 {60226U, 139U},
382 {60227U, 370U},
383 {60228U, 388U},
384 {60229U, 111U},
385 {60230U, 377U},
386 {60231U, 389U},
387 {60232U, 128U},
388 {60233U, 393U},
389 {60234U, 392U},
390 {60235U, 375U},
391 {60236U, 207U},
392 {60237U, 158U},
393 {60238U, 168U},
394 {60239U, 208U},
395 {60244U, 412U},
396 {60248U, 167U},
397 {60252U, 407U},
398 {7680U, 11U},
399 {7681U, 2U},
400 {7682U, 3U},
401 {7683U, 4U},
402 {7684U, 5U},
403 {7685U, 6U},
404 {7686U, 7U},
405 {7687U, 8U},
406 {7688U, 9U},
407 {7689U, 10U},
408 {7690U, 55U},
409 {7691U, 398U},
410 {7692U, 385U},
411 {7693U, 139U},
412 {7694U, 41U},
413 {7695U, 113U},
414 {7696U, 115U},
415 {7697U, 114U},
416 {7698U, 363U},
417 {7700U, 103U},
418 {7701U, 108U},
419 {7702U, 105U},
420 {7703U, 106U},
421 {7704U, 393U},
422 {7705U, 392U},
423 {7706U, 226U},
424 {7707U, 365U},
425 {7708U, 377U},
426 {7710U, 407U},
427 {7711U, 158U},
428 {7712U, 402U},
429 {7713U, 403U},
430 {7716U, 405U},
431 {7717U, 352U},
432 {7721U, 401U},
433 {7726U, 399U},
434 {7728U, 119U},
435 {7730U, 168U},
436 {7732U, 208U},
437 {7733U, 207U},
438 {7734U, 128U},
439 {7735U, 167U},
440 {7736U, 400U},
441 {7739U, 354U},
442 {7741U, 116U},
443 {66U, 116U},
444 {1916U, 386U},
445 {3918U, 210U},
446 {2112U, 375U},
447 {3953U, 52U},
448 {1859U, 11U},
449 {3137U, 2U},
450 {1091U, 3U},
451 {2943U, 4U},
452 {3649U, 5U},
453 {1603U, 6U},
454 {2431U, 7U},
455 {3454U, 8U},
456 {1404U, 9U},
457 {2624U, 10U},
458 {3662U, 355U},
459 {1148U, 363U},
460 {3905U, 405U},
461 {834U, 113U},
462 {1612U, 0U},
463 {370U, 410U},
464 {3150U, 164U},
465 {2928U, 167U},
466 {893U, 115U},
467 {381U, 114U},
468 {578U, 402U},
469 {125U, 403U},
470 {7424U, 11U},
471 {7425U, 2U},
472 {7426U, 3U},
473 {7427U, 4U},
474 {7428U, 5U},
475 {7429U, 6U},
476 {7430U, 7U},
477 {7431U, 8U},
478 {7432U, 9U},
479 {7433U, 10U},
480 {7434U, 388U},
481 {7437U, 139U},
482 {7439U, 113U},
483 {7440U, 115U},
484 {7441U, 114U},
485 {7442U, 363U},
486 {7444U, 103U},
487 {7445U, 108U},
488 {7446U, 105U},
489 {7447U, 106U},
490 {7452U, 377U},
491 {7454U, 407U},
492 {7455U, 158U},
493 {7456U, 402U},
494 {7457U, 403U},
495 {7460U, 405U},
496 {7461U, 352U},
497 {7472U, 119U},
498 {7474U, 168U},
499 {7476U, 208U},
500 {7477U, 207U},
501 {7478U, 128U},
502 {7479U, 167U},
503 {7483U, 354U},
504 {7485U, 116U}};
505#line 228 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9139/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-dib0700-rc5.c.p"
506static struct rc_map_list dib0700_rc5_map = {{(struct list_head *)0, (struct list_head *)0}, {(struct rc_map_table *)(& dib0700_rc5_table),
507 180U, 0U, 0U, 1ULL, "rc-dib0700-rc5",
508 {{{{{0U}}, 0U, 0U, (void *)0,
509 {(struct lock_class_key *)0,
510 {(struct lock_class *)0,
511 (struct lock_class *)0},
512 (char const *)0, 0, 0UL}}}}}};
513#line 237 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9139/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-dib0700-rc5.c.p"
514static int init_rc_map(void)
515{ int tmp ;
516
517 {
518 {
519#line 239
520 tmp = rc_map_register(& dib0700_rc5_map);
521 }
522#line 239
523 return (tmp);
524}
525}
526#line 242 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9139/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-dib0700-rc5.c.p"
527static void exit_rc_map(void)
528{
529
530 {
531 {
532#line 244
533 rc_map_unregister(& dib0700_rc5_map);
534 }
535#line 245
536 return;
537}
538}
539#line 269
540extern void ldv_check_final_state(void) ;
541#line 275
542extern void ldv_initialize(void) ;
543#line 278
544extern int __VERIFIER_nondet_int(void) ;
545#line 281 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9139/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-dib0700-rc5.c.p"
546int LDV_IN_INTERRUPT ;
547#line 284 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9139/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-dib0700-rc5.c.p"
548void main(void)
549{ int tmp ;
550 int tmp___0 ;
551 int tmp___1 ;
552
553 {
554 {
555#line 296
556 LDV_IN_INTERRUPT = 1;
557#line 305
558 ldv_initialize();
559#line 311
560 tmp = init_rc_map();
561 }
562#line 311
563 if (tmp != 0) {
564#line 312
565 goto ldv_final;
566 } else {
567
568 }
569#line 314
570 goto ldv_19081;
571 ldv_19080:
572 {
573#line 317
574 tmp___0 = __VERIFIER_nondet_int();
575 }
576 {
577#line 319
578 goto switch_default;
579#line 317
580 if (0) {
581 switch_default: ;
582#line 319
583 goto ldv_19079;
584 } else {
585 switch_break: ;
586 }
587 }
588 ldv_19079: ;
589 ldv_19081:
590 {
591#line 314
592 tmp___1 = __VERIFIER_nondet_int();
593 }
594#line 314
595 if (tmp___1 != 0) {
596#line 315
597 goto ldv_19080;
598 } else {
599#line 317
600 goto ldv_19082;
601 }
602 ldv_19082: ;
603 {
604#line 331
605 exit_rc_map();
606 }
607 ldv_final:
608 {
609#line 334
610 ldv_check_final_state();
611 }
612#line 337
613 return;
614}
615}
616#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9139/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
617void ldv_blast_assert(void)
618{
619
620 {
621 ERROR: ;
622#line 6
623 goto ERROR;
624}
625}
626#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9139/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
627extern int __VERIFIER_nondet_int(void) ;
628#line 358 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9139/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-dib0700-rc5.c.p"
629int ldv_spin = 0;
630#line 362 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9139/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-dib0700-rc5.c.p"
631void ldv_check_alloc_flags(gfp_t flags )
632{
633
634 {
635#line 365
636 if (ldv_spin != 0) {
637#line 365
638 if (flags != 32U) {
639 {
640#line 365
641 ldv_blast_assert();
642 }
643 } else {
644
645 }
646 } else {
647
648 }
649#line 368
650 return;
651}
652}
653#line 368
654extern struct page *ldv_some_page(void) ;
655#line 371 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9139/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-dib0700-rc5.c.p"
656struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags )
657{ struct page *tmp ;
658
659 {
660#line 374
661 if (ldv_spin != 0) {
662#line 374
663 if (flags != 32U) {
664 {
665#line 374
666 ldv_blast_assert();
667 }
668 } else {
669
670 }
671 } else {
672
673 }
674 {
675#line 376
676 tmp = ldv_some_page();
677 }
678#line 376
679 return (tmp);
680}
681}
682#line 380 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9139/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-dib0700-rc5.c.p"
683void ldv_check_alloc_nonatomic(void)
684{
685
686 {
687#line 383
688 if (ldv_spin != 0) {
689 {
690#line 383
691 ldv_blast_assert();
692 }
693 } else {
694
695 }
696#line 386
697 return;
698}
699}
700#line 387 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9139/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-dib0700-rc5.c.p"
701void ldv_spin_lock(void)
702{
703
704 {
705#line 390
706 ldv_spin = 1;
707#line 391
708 return;
709}
710}
711#line 394 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9139/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-dib0700-rc5.c.p"
712void ldv_spin_unlock(void)
713{
714
715 {
716#line 397
717 ldv_spin = 0;
718#line 398
719 return;
720}
721}
722#line 401 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9139/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-dib0700-rc5.c.p"
723int ldv_spin_trylock(void)
724{ int is_lock ;
725
726 {
727 {
728#line 406
729 is_lock = __VERIFIER_nondet_int();
730 }
731#line 408
732 if (is_lock != 0) {
733#line 411
734 return (0);
735 } else {
736#line 416
737 ldv_spin = 1;
738#line 418
739 return (1);
740 }
741}
742}
743#line 585 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9139/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-dib0700-rc5.c.p"
744void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 )
745{
746
747 {
748 {
749#line 591
750 ldv_check_alloc_flags(ldv_func_arg2);
751#line 593
752 kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
753 }
754#line 594
755 return ((void *)0);
756}
757}