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 62 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12928/dscv_tempdir/dscv/ri/32_1/drivers/media/rc/keymaps/rc-pixelview-new.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 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12928/dscv_tempdir/dscv/ri/32_1/drivers/media/rc/keymaps/rc-pixelview-new.c.common.c"
138static struct rc_map_table pixelview_new[31] =
139#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12928/dscv_tempdir/dscv/ri/32_1/drivers/media/rc/keymaps/rc-pixelview-new.c.common.c"
140 { {(u32 )60, (u32 )359},
141 {(u32 )18, (u32 )116},
142 {(u32 )61, (u32 )2},
143 {(u32 )56, (u32 )3},
144 {(u32 )24, (u32 )4},
145 {(u32 )53, (u32 )5},
146 {(u32 )57, (u32 )6},
147 {(u32 )21, (u32 )7},
148 {(u32 )54, (u32 )8},
149 {(u32 )58, (u32 )9},
150 {(u32 )30, (u32 )10},
151 {(u32 )62, (u32 )11},
152 {(u32 )28, (u32 )129},
153 {(u32 )63, (u32 )393},
154 {(u32 )31, (u32 )405},
155 {(u32 )27, (u32 )113},
156 {(u32 )23, (u32 )403},
157 {(u32 )22, (u32 )402},
158 {(u32 )16, (u32 )115},
159 {(u32 )20, (u32 )114},
160 {(u32 )19, (u32 )372},
161 {(u32 )25, (u32 )212},
162 {(u32 )26, (u32 )217},
163 {(u32 )55, (u32 )168},
164 {(u32 )50, (u32 )167},
165 {(u32 )51, (u32 )159},
166 {(u32 )17, (u32 )128},
167 {(u32 )59, (u32 )207},
168 {(u32 )48, (u32 )164},
169 {(u32 )49, (u32 )377},
170 {(u32 )52, (u32 )385}};
171#line 62 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12928/dscv_tempdir/dscv/ri/32_1/drivers/media/rc/keymaps/rc-pixelview-new.c.common.c"
172static struct rc_map_list pixelview_new_map = {{(struct list_head *)0, (struct list_head *)0}, {pixelview_new, (unsigned int )(sizeof(pixelview_new) / sizeof(pixelview_new[0]) + sizeof(struct __anonstruct_220 )),
173 0U, 0U, (u64 )0, "rc-pixelview-new",
174 {{{{{0U}}, 0U, 0U, (void *)0}}}}};
175#line 71
176static int init_rc_map_pixelview_new(void) __attribute__((__section__(".init.text"),
177__no_instrument_function__)) ;
178#line 71 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12928/dscv_tempdir/dscv/ri/32_1/drivers/media/rc/keymaps/rc-pixelview-new.c.common.c"
179static int init_rc_map_pixelview_new(void)
180{ int tmp ;
181
182 {
183 {
184#line 73
185 tmp = rc_map_register(& pixelview_new_map);
186 }
187#line 73
188 return (tmp);
189}
190}
191#line 76
192static void exit_rc_map_pixelview_new(void) __attribute__((__section__(".exit.text"),
193__no_instrument_function__)) ;
194#line 76 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12928/dscv_tempdir/dscv/ri/32_1/drivers/media/rc/keymaps/rc-pixelview-new.c.common.c"
195static void exit_rc_map_pixelview_new(void)
196{
197
198 {
199 {
200#line 78
201 rc_map_unregister(& pixelview_new_map);
202 }
203#line 79
204 return;
205}
206}
207#line 81 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12928/dscv_tempdir/dscv/ri/32_1/drivers/media/rc/keymaps/rc-pixelview-new.c.common.c"
208int init_module(void)
209{ int tmp ;
210
211 {
212 {
213#line 81
214 tmp = init_rc_map_pixelview_new();
215 }
216#line 81
217 return (tmp);
218}
219}
220#line 82 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12928/dscv_tempdir/dscv/ri/32_1/drivers/media/rc/keymaps/rc-pixelview-new.c.common.c"
221void cleanup_module(void)
222{
223
224 {
225 {
226#line 82
227 exit_rc_map_pixelview_new();
228 }
229#line 82
230 return;
231}
232}
233#line 84 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12928/dscv_tempdir/dscv/ri/32_1/drivers/media/rc/keymaps/rc-pixelview-new.c.common.c"
234static char const __mod_license84[12] __attribute__((__used__, __unused__, __section__(".modinfo"),
235__aligned__(1))) =
236#line 84
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 85 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12928/dscv_tempdir/dscv/ri/32_1/drivers/media/rc/keymaps/rc-pixelview-new.c.common.c"
241static char const __mod_author85[50] __attribute__((__used__, __unused__, __section__(".modinfo"),
242__aligned__(1))) =
243#line 85
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 103
258void ldv_check_final_state(void) ;
259#line 109
260extern void ldv_initialize(void) ;
261#line 112
262extern int __VERIFIER_nondet_int(void) ;
263#line 115 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12928/dscv_tempdir/dscv/ri/32_1/drivers/media/rc/keymaps/rc-pixelview-new.c.common.c"
264int LDV_IN_INTERRUPT ;
265#line 118 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12928/dscv_tempdir/dscv/ri/32_1/drivers/media/rc/keymaps/rc-pixelview-new.c.common.c"
266void main(void)
267{ int tmp ;
268 int tmp___0 ;
269 int tmp___1 ;
270
271 {
272 {
273#line 130
274 LDV_IN_INTERRUPT = 1;
275#line 139
276 ldv_initialize();
277#line 145
278 tmp = init_rc_map_pixelview_new();
279 }
280#line 145
281 if (tmp) {
282#line 146
283 goto ldv_final;
284 } else {
285
286 }
287 {
288#line 148
289 while (1) {
290 while_continue: ;
291 {
292#line 148
293 tmp___1 = __VERIFIER_nondet_int();
294 }
295#line 148
296 if (tmp___1) {
297
298 } else {
299#line 148
300 goto while_break;
301 }
302 {
303#line 151
304 tmp___0 = __VERIFIER_nondet_int();
305 }
306 {
307#line 153
308 goto switch_default;
309#line 151
310 if (0) {
311 switch_default:
312#line 153
313 goto switch_break;
314 } else {
315 switch_break: ;
316 }
317 }
318 }
319 while_break: ;
320 }
321 {
322#line 165
323 exit_rc_map_pixelview_new();
324 }
325 ldv_final:
326 {
327#line 168
328 ldv_check_final_state();
329 }
330#line 171
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/12928/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/12928/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/12928/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/12928/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/12928/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/12928/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/12928/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/12928/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/12928/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/12928/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 180 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12928/dscv_tempdir/dscv/ri/32_1/drivers/media/rc/keymaps/rc-pixelview-new.c.common.c"
528long s__builtin_expect(long val , long res )
529{
530
531 {
532#line 181
533 return (val);
534}
535}