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