Showing error 971

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-linux-3.4/43_1a_cilled_safe_ok_nondet_linux-43_1a-drivers--media--rc--keymaps--rc-avermedia-m135a.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 520
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

  1/* Generated by CIL v. 1.3.7 */
  2/* print_CIL_Input is true */
  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/9127/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-avermedia-m135a.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/9127/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-avermedia-m135a.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 41 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9127/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-avermedia-m135a.c.p"
323static struct rc_map_table avermedia_m135a[79U]  = 
324#line 41 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9127/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-avermedia-m135a.c.p"
325  {      {512U, 356U}, 
326        {558U, 52U}, 
327        {513U, 373U}, 
328        {517U, 2U}, 
329        {518U, 3U}, 
330        {519U, 4U}, 
331        {521U, 5U}, 
332        {522U, 6U}, 
333        {523U, 7U}, 
334        {525U, 8U}, 
335        {526U, 9U}, 
336        {527U, 10U}, 
337        {529U, 11U}, 
338        {531U, 106U}, 
339        {530U, 105U}, 
340        {535U, 142U}, 
341        {528U, 410U}, 
342        {771U, 402U}, 
343        {770U, 403U}, 
344        {543U, 115U}, 
345        {542U, 114U}, 
346        {524U, 28U}, 
347        {532U, 113U}, 
348        {520U, 392U}, 
349        {515U, 388U}, 
350        {516U, 365U}, 
351        {555U, 378U}, 
352        {541U, 398U}, 
353        {540U, 400U}, 
354        {769U, 399U}, 
355        {768U, 401U}, 
356        {538U, 164U}, 
357        {537U, 167U}, 
358        {536U, 207U}, 
359        {539U, 128U}, 
360        {1025U, 356U}, 
361        {1030U, 113U}, 
362        {1032U, 373U}, 
363        {1033U, 2U}, 
364        {1034U, 3U}, 
365        {1035U, 4U}, 
366        {1036U, 5U}, 
367        {1037U, 6U}, 
368        {1038U, 7U}, 
369        {1039U, 8U}, 
370        {1040U, 9U}, 
371        {1041U, 10U}, 
372        {1100U, 52U}, 
373        {1042U, 11U}, 
374        {1031U, 173U}, 
375        {1043U, 392U}, 
376        {1088U, 375U}, 
377        {1089U, 102U}, 
378        {1090U, 158U}, 
379        {1095U, 103U}, 
380        {1096U, 108U}, 
381        {1097U, 105U}, 
382        {1098U, 106U}, 
383        {1099U, 352U}, 
384        {1028U, 115U}, 
385        {1029U, 114U}, 
386        {1026U, 402U}, 
387        {1027U, 403U}, 
388        {1091U, 398U}, 
389        {1092U, 399U}, 
390        {1093U, 400U}, 
391        {1094U, 401U}, 
392        {1044U, 388U}, 
393        {1045U, 365U}, 
394        {1050U, 378U}, 
395        {1051U, 212U}, 
396        {1047U, 167U}, 
397        {1046U, 164U}, 
398        {1048U, 128U}, 
399        {1049U, 119U}, 
400        {1055U, 412U}, 
401        {1052U, 168U}, 
402        {1053U, 159U}, 
403        {1054U, 407U}};
404#line 140 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9127/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-avermedia-m135a.c.p"
405static struct rc_map_list avermedia_m135a_map  =    {{(struct list_head *)0, (struct list_head *)0}, {(struct rc_map_table *)(& avermedia_m135a),
406                                                     79U, 0U, 0U, 2ULL, "rc-avermedia-m135a",
407                                                     {{{{{0U}}, 0U, 0U, (void *)0,
408                                                        {(struct lock_class_key *)0,
409                                                         {(struct lock_class *)0,
410                                                          (struct lock_class *)0},
411                                                         (char const   *)0, 0, 0UL}}}}}};
412#line 149 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9127/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-avermedia-m135a.c.p"
413static int init_rc_map_avermedia_m135a(void) 
414{ int tmp ;
415
416  {
417  {
418#line 151
419  tmp = rc_map_register(& avermedia_m135a_map);
420  }
421#line 151
422  return (tmp);
423}
424}
425#line 154 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9127/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-avermedia-m135a.c.p"
426static void exit_rc_map_avermedia_m135a(void) 
427{ 
428
429  {
430  {
431#line 156
432  rc_map_unregister(& avermedia_m135a_map);
433  }
434#line 157
435  return;
436}
437}
438#line 181
439extern void ldv_check_final_state(void) ;
440#line 187
441extern void ldv_initialize(void) ;
442#line 190
443extern int __VERIFIER_nondet_int(void) ;
444#line 193 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9127/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-avermedia-m135a.c.p"
445int LDV_IN_INTERRUPT  ;
446#line 196 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9127/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-avermedia-m135a.c.p"
447void main(void) 
448{ int tmp ;
449  int tmp___0 ;
450  int tmp___1 ;
451
452  {
453  {
454#line 208
455  LDV_IN_INTERRUPT = 1;
456#line 217
457  ldv_initialize();
458#line 223
459  tmp = init_rc_map_avermedia_m135a();
460  }
461#line 223
462  if (tmp != 0) {
463#line 224
464    goto ldv_final;
465  } else {
466
467  }
468#line 226
469  goto ldv_19081;
470  ldv_19080: 
471  {
472#line 229
473  tmp___0 = __VERIFIER_nondet_int();
474  }
475  {
476#line 231
477  goto switch_default;
478#line 229
479  if (0) {
480    switch_default: /* CIL Label */ ;
481#line 231
482    goto ldv_19079;
483  } else {
484    switch_break: /* CIL Label */ ;
485  }
486  }
487  ldv_19079: ;
488  ldv_19081: 
489  {
490#line 226
491  tmp___1 = __VERIFIER_nondet_int();
492  }
493#line 226
494  if (tmp___1 != 0) {
495#line 227
496    goto ldv_19080;
497  } else {
498#line 229
499    goto ldv_19082;
500  }
501  ldv_19082: ;
502  {
503#line 243
504  exit_rc_map_avermedia_m135a();
505  }
506  ldv_final: 
507  {
508#line 246
509  ldv_check_final_state();
510  }
511#line 249
512  return;
513}
514}
515#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9127/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
516void ldv_blast_assert(void) 
517{ 
518
519  {
520  ERROR: ;
521#line 6
522  goto ERROR;
523}
524}
525#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9127/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
526extern int __VERIFIER_nondet_int(void) ;
527#line 270 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9127/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-avermedia-m135a.c.p"
528int ldv_spin  =    0;
529#line 274 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9127/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-avermedia-m135a.c.p"
530void ldv_check_alloc_flags(gfp_t flags ) 
531{ 
532
533  {
534#line 277
535  if (ldv_spin != 0) {
536#line 277
537    if (flags != 32U) {
538      {
539#line 277
540      ldv_blast_assert();
541      }
542    } else {
543
544    }
545  } else {
546
547  }
548#line 280
549  return;
550}
551}
552#line 280
553extern struct page *ldv_some_page(void) ;
554#line 283 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9127/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-avermedia-m135a.c.p"
555struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) 
556{ struct page *tmp ;
557
558  {
559#line 286
560  if (ldv_spin != 0) {
561#line 286
562    if (flags != 32U) {
563      {
564#line 286
565      ldv_blast_assert();
566      }
567    } else {
568
569    }
570  } else {
571
572  }
573  {
574#line 288
575  tmp = ldv_some_page();
576  }
577#line 288
578  return (tmp);
579}
580}
581#line 292 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9127/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-avermedia-m135a.c.p"
582void ldv_check_alloc_nonatomic(void) 
583{ 
584
585  {
586#line 295
587  if (ldv_spin != 0) {
588    {
589#line 295
590    ldv_blast_assert();
591    }
592  } else {
593
594  }
595#line 298
596  return;
597}
598}
599#line 299 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9127/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-avermedia-m135a.c.p"
600void ldv_spin_lock(void) 
601{ 
602
603  {
604#line 302
605  ldv_spin = 1;
606#line 303
607  return;
608}
609}
610#line 306 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9127/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-avermedia-m135a.c.p"
611void ldv_spin_unlock(void) 
612{ 
613
614  {
615#line 309
616  ldv_spin = 0;
617#line 310
618  return;
619}
620}
621#line 313 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9127/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-avermedia-m135a.c.p"
622int ldv_spin_trylock(void) 
623{ int is_lock ;
624
625  {
626  {
627#line 318
628  is_lock = __VERIFIER_nondet_int();
629  }
630#line 320
631  if (is_lock != 0) {
632#line 323
633    return (0);
634  } else {
635#line 328
636    ldv_spin = 1;
637#line 330
638    return (1);
639  }
640}
641}
642#line 497 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9127/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-avermedia-m135a.c.p"
643void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) 
644{ 
645
646  {
647  {
648#line 503
649  ldv_check_alloc_flags(ldv_func_arg2);
650#line 505
651  kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
652  }
653#line 506
654  return ((void *)0);
655}
656}