1
2
3
4#line 46 "include/asm-generic/int-ll64.h"
5typedef unsigned short u16;
6#line 49 "include/asm-generic/int-ll64.h"
7typedef unsigned int u32;
8#line 52 "include/asm-generic/int-ll64.h"
9typedef unsigned long long u64;
10#line 219 "include/linux/types.h"
11struct __anonstruct_atomic_t_7 {
12 int counter ;
13};
14#line 219 "include/linux/types.h"
15typedef struct __anonstruct_atomic_t_7 atomic_t;
16#line 229 "include/linux/types.h"
17struct list_head {
18 struct list_head *next ;
19 struct list_head *prev ;
20};
21#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
22struct task_struct;
23#line 20
24struct task_struct;
25#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
26struct task_struct;
27#line 52 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
28struct task_struct;
29#line 329
30struct arch_spinlock;
31#line 329
32struct arch_spinlock;
33#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
34struct task_struct;
35#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
36struct task_struct;
37#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
38typedef u16 __ticket_t;
39#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
40typedef u32 __ticketpair_t;
41#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
42struct __raw_tickets {
43 __ticket_t head ;
44 __ticket_t tail ;
45};
46#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
47union __anonunion____missing_field_name_36 {
48 __ticketpair_t head_tail ;
49 struct __raw_tickets tickets ;
50};
51#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
52struct arch_spinlock {
53 union __anonunion____missing_field_name_36 __annonCompField17 ;
54};
55#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
56typedef struct arch_spinlock arch_spinlock_t;
57#line 12 "include/linux/lockdep.h"
58struct task_struct;
59#line 20 "include/linux/spinlock_types.h"
60struct raw_spinlock {
61 arch_spinlock_t raw_lock ;
62 unsigned int magic ;
63 unsigned int owner_cpu ;
64 void *owner ;
65};
66#line 64 "include/linux/spinlock_types.h"
67union __anonunion____missing_field_name_39 {
68 struct raw_spinlock rlock ;
69};
70#line 64 "include/linux/spinlock_types.h"
71struct spinlock {
72 union __anonunion____missing_field_name_39 __annonCompField19 ;
73};
74#line 64 "include/linux/spinlock_types.h"
75typedef struct spinlock spinlock_t;
76#line 55 "include/linux/wait.h"
77struct task_struct;
78#line 48 "include/linux/mutex.h"
79struct mutex {
80 atomic_t count ;
81 spinlock_t wait_lock ;
82 struct list_head wait_list ;
83 struct task_struct *owner ;
84 char const *name ;
85 void *magic ;
86};
87#line 18 "include/linux/capability.h"
88struct task_struct;
89#line 31 "include/media/rc-map.h"
90struct rc_map_table {
91 u32 scancode ;
92 u32 keycode ;
93};
94#line 36 "include/media/rc-map.h"
95struct rc_map {
96 struct rc_map_table *scan ;
97 unsigned int size ;
98 unsigned int len ;
99 unsigned int alloc ;
100 u64 rc_type ;
101 char const *name ;
102 spinlock_t lock ;
103};
104#line 46 "include/media/rc-map.h"
105struct rc_map_list {
106 struct list_head list ;
107 struct rc_map map ;
108};
109#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
110struct task_struct;
111#line 91 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12889/dscv_tempdir/dscv/ri/32_1/drivers/media/rc/keymaps/rc-encore-enltv.c.common.c"
112struct __anonstruct_220 {
113 int : 0 ;
114};
115#line 1 "<compiler builtins>"
116long __builtin_expect(long val , long res ) ;
117#line 152 "include/linux/mutex.h"
118void mutex_lock(struct mutex *lock ) ;
119#line 153
120int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock ) ;
121#line 154
122int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock ) ;
123#line 168
124int mutex_trylock(struct mutex *lock ) ;
125#line 169
126void mutex_unlock(struct mutex *lock ) ;
127#line 170
128int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
129#line 53 "include/media/rc-map.h"
130extern int rc_map_register(struct rc_map_list *map ) ;
131#line 54
132extern void rc_map_unregister(struct rc_map_list *map ) ;
133#line 67 "include/linux/module.h"
134int init_module(void) ;
135#line 68
136void cleanup_module(void) ;
137#line 20 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12889/dscv_tempdir/dscv/ri/32_1/drivers/media/rc/keymaps/rc-encore-enltv.c.common.c"
138static struct rc_map_table encore_enltv[52] =
139#line 20 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12889/dscv_tempdir/dscv/ri/32_1/drivers/media/rc/keymaps/rc-encore-enltv.c.common.c"
140 { {(u32 )13, (u32 )113},
141 {(u32 )30, (u32 )377},
142 {(u32 )0, (u32 )393},
143 {(u32 )1, (u32 )392},
144 {(u32 )2, (u32 )212},
145 {(u32 )31, (u32 )2},
146 {(u32 )3, (u32 )3},
147 {(u32 )4, (u32 )4},
148 {(u32 )5, (u32 )5},
149 {(u32 )28, (u32 )6},
150 {(u32 )6, (u32 )7},
151 {(u32 )7, (u32 )8},
152 {(u32 )8, (u32 )9},
153 {(u32 )29, (u32 )10},
154 {(u32 )10, (u32 )11},
155 {(u32 )9, (u32 )395},
156 {(u32 )11, (u32 )405},
157 {(u32 )20, (u32 )102},
158 {(u32 )21, (u32 )174},
159 {(u32 )22, (u32 )402},
160 {(u32 )18, (u32 )403},
161 {(u32 )12, (u32 )115},
162 {(u32 )23, (u32 )114},
163 {(u32 )24, (u32 )28},
164 {(u32 )14, (u32 )1},
165 {(u32 )19, (u32 )154},
166 {(u32 )17, (u32 )15},
167 {(u32 )25, (u32 )227},
168 {(u32 )26, (u32 )139},
169 {(u32 )27, (u32 )372},
170 {(u32 )68, (u32 )359},
171 {(u32 )64, (u32 )373},
172 {(u32 )90, (u32 )167},
173 {(u32 )66, (u32 )207},
174 {(u32 )69, (u32 )128},
175 {(u32 )67, (u32 )212},
176 {(u32 )72, (u32 )168},
177 {(u32 )74, (u32 )208},
178 {(u32 )73, (u32 )412},
179 {(u32 )75, (u32 )407},
180 {(u32 )76, (u32 )364},
181 {(u32 )77, (u32 )213},
182 {(u32 )78, (u32 )368},
183 {(u32 )79, (u32 )388},
184 {(u32 )80, (u32 )142},
185 {(u32 )81, (u32 )373},
186 {(u32 )82, (u32 )353},
187 {(u32 )83, (u32 )388},
188 {(u32 )89, (u32 )398},
189 {(u32 )65, (u32 )399},
190 {(u32 )71, (u32 )400},
191 {(u32 )87, (u32 )401}};
192#line 91 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12889/dscv_tempdir/dscv/ri/32_1/drivers/media/rc/keymaps/rc-encore-enltv.c.common.c"
193static struct rc_map_list encore_enltv_map = {{(struct list_head *)0, (struct list_head *)0}, {encore_enltv, (unsigned int )(sizeof(encore_enltv) / sizeof(encore_enltv[0]) + sizeof(struct __anonstruct_220 )),
194 0U, 0U, (u64 )0, "rc-encore-enltv",
195 {{{{{0U}}, 0U, 0U, (void *)0}}}}};
196#line 100
197static int init_rc_map_encore_enltv(void) __attribute__((__section__(".init.text"),
198__no_instrument_function__)) ;
199#line 100 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12889/dscv_tempdir/dscv/ri/32_1/drivers/media/rc/keymaps/rc-encore-enltv.c.common.c"
200static int init_rc_map_encore_enltv(void)
201{ int tmp ;
202
203 {
204 {
205#line 102
206 tmp = rc_map_register(& encore_enltv_map);
207 }
208#line 102
209 return (tmp);
210}
211}
212#line 105
213static void exit_rc_map_encore_enltv(void) __attribute__((__section__(".exit.text"),
214__no_instrument_function__)) ;
215#line 105 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12889/dscv_tempdir/dscv/ri/32_1/drivers/media/rc/keymaps/rc-encore-enltv.c.common.c"
216static void exit_rc_map_encore_enltv(void)
217{
218
219 {
220 {
221#line 107
222 rc_map_unregister(& encore_enltv_map);
223 }
224#line 108
225 return;
226}
227}
228#line 110 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12889/dscv_tempdir/dscv/ri/32_1/drivers/media/rc/keymaps/rc-encore-enltv.c.common.c"
229int init_module(void)
230{ int tmp ;
231
232 {
233 {
234#line 110
235 tmp = init_rc_map_encore_enltv();
236 }
237#line 110
238 return (tmp);
239}
240}
241#line 111 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12889/dscv_tempdir/dscv/ri/32_1/drivers/media/rc/keymaps/rc-encore-enltv.c.common.c"
242void cleanup_module(void)
243{
244
245 {
246 {
247#line 111
248 exit_rc_map_encore_enltv();
249 }
250#line 111
251 return;
252}
253}
254#line 113 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12889/dscv_tempdir/dscv/ri/32_1/drivers/media/rc/keymaps/rc-encore-enltv.c.common.c"
255static char const __mod_license113[12] __attribute__((__used__, __unused__, __section__(".modinfo"),
256__aligned__(1))) =
257#line 113
258 { (char const )'l', (char const )'i', (char const )'c', (char const )'e',
259 (char const )'n', (char const )'s', (char const )'e', (char const )'=',
260 (char const )'G', (char const )'P', (char const )'L', (char const )'\000'};
261#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12889/dscv_tempdir/dscv/ri/32_1/drivers/media/rc/keymaps/rc-encore-enltv.c.common.c"
262static char const __mod_author114[50] __attribute__((__used__, __unused__, __section__(".modinfo"),
263__aligned__(1))) =
264#line 114
265 { (char const )'a', (char const )'u', (char const )'t', (char const )'h',
266 (char const )'o', (char const )'r', (char const )'=', (char const )'M',
267 (char const )'a', (char const )'u', (char const )'r', (char const )'o',
268 (char const )' ', (char const )'C', (char const )'a', (char const )'r',
269 (char const )'v', (char const )'a', (char const )'l', (char const )'h',
270 (char const )'o', (char const )' ', (char const )'C', (char const )'h',
271 (char const )'e', (char const )'h', (char const )'a', (char const )'b',
272 (char const )' ', (char const )'<', (char const )'m', (char const )'c',
273 (char const )'h', (char const )'e', (char const )'h', (char const )'a',
274 (char const )'b', (char const )'@', (char const )'r', (char const )'e',
275 (char const )'d', (char const )'h', (char const )'a', (char const )'t',
276 (char const )'.', (char const )'c', (char const )'o', (char const )'m',
277 (char const )'>', (char const )'\000'};
278#line 132
279void ldv_check_final_state(void) ;
280#line 138
281extern void ldv_initialize(void) ;
282#line 141
283extern int __VERIFIER_nondet_int(void) ;
284#line 144 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12889/dscv_tempdir/dscv/ri/32_1/drivers/media/rc/keymaps/rc-encore-enltv.c.common.c"
285int LDV_IN_INTERRUPT ;
286#line 147 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12889/dscv_tempdir/dscv/ri/32_1/drivers/media/rc/keymaps/rc-encore-enltv.c.common.c"
287void main(void)
288{ int tmp ;
289 int tmp___0 ;
290 int tmp___1 ;
291
292 {
293 {
294#line 159
295 LDV_IN_INTERRUPT = 1;
296#line 168
297 ldv_initialize();
298#line 174
299 tmp = init_rc_map_encore_enltv();
300 }
301#line 174
302 if (tmp) {
303#line 175
304 goto ldv_final;
305 } else {
306
307 }
308 {
309#line 177
310 while (1) {
311 while_continue: ;
312 {
313#line 177
314 tmp___1 = __VERIFIER_nondet_int();
315 }
316#line 177
317 if (tmp___1) {
318
319 } else {
320#line 177
321 goto while_break;
322 }
323 {
324#line 180
325 tmp___0 = __VERIFIER_nondet_int();
326 }
327 {
328#line 182
329 goto switch_default;
330#line 180
331 if (0) {
332 switch_default:
333#line 182
334 goto switch_break;
335 } else {
336 switch_break: ;
337 }
338 }
339 }
340 while_break: ;
341 }
342 {
343#line 194
344 exit_rc_map_encore_enltv();
345 }
346 ldv_final:
347 {
348#line 197
349 ldv_check_final_state();
350 }
351#line 200
352 return;
353}
354}
355#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12889/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
356void ldv_blast_assert(void)
357{
358
359 {
360 ERROR:
361#line 6
362 goto ERROR;
363}
364}
365#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12889/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
366extern int __VERIFIER_nondet_int(void) ;
367#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12889/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
368int ldv_mutex = 1;
369#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12889/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
370int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )
371{ int nondetermined ;
372
373 {
374#line 29
375 if (ldv_mutex == 1) {
376
377 } else {
378 {
379#line 29
380 ldv_blast_assert();
381 }
382 }
383 {
384#line 32
385 nondetermined = __VERIFIER_nondet_int();
386 }
387#line 35
388 if (nondetermined) {
389#line 38
390 ldv_mutex = 2;
391#line 40
392 return (0);
393 } else {
394#line 45
395 return (-4);
396 }
397}
398}
399#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12889/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
400int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock )
401{ int nondetermined ;
402
403 {
404#line 57
405 if (ldv_mutex == 1) {
406
407 } else {
408 {
409#line 57
410 ldv_blast_assert();
411 }
412 }
413 {
414#line 60
415 nondetermined = __VERIFIER_nondet_int();
416 }
417#line 63
418 if (nondetermined) {
419#line 66
420 ldv_mutex = 2;
421#line 68
422 return (0);
423 } else {
424#line 73
425 return (-4);
426 }
427}
428}
429#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12889/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
430int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock )
431{ int atomic_value_after_dec ;
432
433 {
434#line 83
435 if (ldv_mutex == 1) {
436
437 } else {
438 {
439#line 83
440 ldv_blast_assert();
441 }
442 }
443 {
444#line 86
445 atomic_value_after_dec = __VERIFIER_nondet_int();
446 }
447#line 89
448 if (atomic_value_after_dec == 0) {
449#line 92
450 ldv_mutex = 2;
451#line 94
452 return (1);
453 } else {
454
455 }
456#line 98
457 return (0);
458}
459}
460#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12889/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
461void mutex_lock(struct mutex *lock )
462{
463
464 {
465#line 108
466 if (ldv_mutex == 1) {
467
468 } else {
469 {
470#line 108
471 ldv_blast_assert();
472 }
473 }
474#line 110
475 ldv_mutex = 2;
476#line 111
477 return;
478}
479}
480#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12889/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
481int mutex_trylock(struct mutex *lock )
482{ int nondetermined ;
483
484 {
485#line 121
486 if (ldv_mutex == 1) {
487
488 } else {
489 {
490#line 121
491 ldv_blast_assert();
492 }
493 }
494 {
495#line 124
496 nondetermined = __VERIFIER_nondet_int();
497 }
498#line 127
499 if (nondetermined) {
500#line 130
501 ldv_mutex = 2;
502#line 132
503 return (1);
504 } else {
505#line 137
506 return (0);
507 }
508}
509}
510#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12889/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
511void mutex_unlock(struct mutex *lock )
512{
513
514 {
515#line 147
516 if (ldv_mutex == 2) {
517
518 } else {
519 {
520#line 147
521 ldv_blast_assert();
522 }
523 }
524#line 149
525 ldv_mutex = 1;
526#line 150
527 return;
528}
529}
530#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12889/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
531void ldv_check_final_state(void)
532{
533
534 {
535#line 156
536 if (ldv_mutex == 1) {
537
538 } else {
539 {
540#line 156
541 ldv_blast_assert();
542 }
543 }
544#line 157
545 return;
546}
547}
548#line 209 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12889/dscv_tempdir/dscv/ri/32_1/drivers/media/rc/keymaps/rc-encore-enltv.c.common.c"
549long s__builtin_expect(long val , long res )
550{
551
552 {
553#line 210
554 return (val);
555}
556}