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