1
2
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 206 "include/linux/types.h"
13typedef u64 phys_addr_t;
14#line 211 "include/linux/types.h"
15typedef phys_addr_t resource_size_t;
16#line 219 "include/linux/types.h"
17struct __anonstruct_atomic_t_7 {
18 int counter ;
19};
20#line 219 "include/linux/types.h"
21typedef struct __anonstruct_atomic_t_7 atomic_t;
22#line 229 "include/linux/types.h"
23struct list_head {
24 struct list_head *next ;
25 struct list_head *prev ;
26};
27#line 47 "include/linux/dynamic_debug.h"
28struct device;
29#line 47
30struct device;
31#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
32struct task_struct;
33#line 20
34struct task_struct;
35#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
36struct task_struct;
37#line 52 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
38struct task_struct;
39#line 329
40struct arch_spinlock;
41#line 329
42struct arch_spinlock;
43#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
44struct task_struct;
45#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
46struct task_struct;
47#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
48typedef u16 __ticket_t;
49#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
50typedef u32 __ticketpair_t;
51#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
52struct __raw_tickets {
53 __ticket_t head ;
54 __ticket_t tail ;
55};
56#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
57union __anonunion____missing_field_name_36 {
58 __ticketpair_t head_tail ;
59 struct __raw_tickets tickets ;
60};
61#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
62struct arch_spinlock {
63 union __anonunion____missing_field_name_36 __annonCompField17 ;
64};
65#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
66typedef struct arch_spinlock arch_spinlock_t;
67#line 12 "include/linux/lockdep.h"
68struct task_struct;
69#line 20 "include/linux/spinlock_types.h"
70struct raw_spinlock {
71 arch_spinlock_t raw_lock ;
72 unsigned int magic ;
73 unsigned int owner_cpu ;
74 void *owner ;
75};
76#line 64 "include/linux/spinlock_types.h"
77union __anonunion____missing_field_name_39 {
78 struct raw_spinlock rlock ;
79};
80#line 64 "include/linux/spinlock_types.h"
81struct spinlock {
82 union __anonunion____missing_field_name_39 __annonCompField19 ;
83};
84#line 64 "include/linux/spinlock_types.h"
85typedef struct spinlock spinlock_t;
86#line 55 "include/linux/wait.h"
87struct task_struct;
88#line 48 "include/linux/mutex.h"
89struct mutex {
90 atomic_t count ;
91 spinlock_t wait_lock ;
92 struct list_head wait_list ;
93 struct task_struct *owner ;
94 char const *name ;
95 void *magic ;
96};
97#line 18 "include/linux/ioport.h"
98struct resource {
99 resource_size_t start ;
100 resource_size_t end ;
101 char const *name ;
102 unsigned long flags ;
103 struct resource *parent ;
104 struct resource *sibling ;
105 struct resource *child ;
106};
107#line 202
108struct device;
109#line 103 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mpspec.h"
110struct device;
111#line 42 "include/linux/pm.h"
112struct device;
113#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
114struct task_struct;
115#line 25 "include/linux/io.h"
116struct device;
117#line 16 "include/linux/c2port.h"
118struct device;
119#line 23
120struct c2port_ops;
121#line 23
122struct c2port_ops;
123#line 24 "include/linux/c2port.h"
124struct c2port_device {
125 unsigned int access : 1 ;
126 unsigned int flash_access : 1 ;
127 int id ;
128 char name[32] ;
129 struct c2port_ops *ops ;
130 struct mutex mutex ;
131 struct device *dev ;
132 void *private_data ;
133};
134#line 41 "include/linux/c2port.h"
135struct c2port_ops {
136 unsigned short block_size ;
137 unsigned short blocks_num ;
138 void (*access)(struct c2port_device *dev , int status ) ;
139 void (*c2d_dir)(struct c2port_device *dev , int dir ) ;
140 int (*c2d_get)(struct c2port_device *dev ) ;
141 void (*c2d_set)(struct c2port_device *dev , int status ) ;
142 void (*c2ck_set)(struct c2port_device *dev , int status ) ;
143};
144#line 1 "<compiler builtins>"
145long __builtin_expect(long val , long res ) ;
146#line 152 "include/linux/mutex.h"
147void mutex_lock(struct mutex *lock ) ;
148#line 153
149int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock ) ;
150#line 154
151int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock ) ;
152#line 168
153int mutex_trylock(struct mutex *lock ) ;
154#line 169
155void mutex_unlock(struct mutex *lock ) ;
156#line 170
157int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
158#line 137 "include/linux/ioport.h"
159extern struct resource ioport_resource ;
160#line 181
161extern struct resource *__request_region(struct resource * , resource_size_t start ,
162 resource_size_t n , char const *name ,
163 int flags ) ;
164#line 192
165extern void __release_region(struct resource * , resource_size_t , resource_size_t ) ;
166#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
167__inline static void outb(unsigned char value , int port ) __attribute__((__no_instrument_function__)) ;
168#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
169__inline static void outb(unsigned char value , int port )
170{
171
172 {
173#line 308
174 __asm__ volatile ("out"
175 "b"
176 " %"
177 "b"
178 "0, %w1": : "a" (value), "Nd" (port));
179#line 308
180 return;
181}
182}
183#line 308
184__inline static unsigned char inb(int port ) __attribute__((__no_instrument_function__)) ;
185#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
186__inline static unsigned char inb(int port )
187{ unsigned char value ;
188
189 {
190#line 308
191 __asm__ volatile ("in"
192 "b"
193 " %w1, %"
194 "b"
195 "0": "=a" (value): "Nd" (port));
196#line 308
197 return (value);
198}
199}
200#line 67 "include/linux/module.h"
201int init_module(void) ;
202#line 68
203void cleanup_module(void) ;
204#line 64 "include/linux/c2port.h"
205extern struct c2port_device *c2port_device_register(char *name , struct c2port_ops *ops ,
206 void *devdata ) ;
207#line 66
208extern void c2port_device_unregister(struct c2port_device *dev ) ;
209#line 27 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4773/dscv_tempdir/dscv/ri/32_1/drivers/misc/c2port/c2port-duramar2150.c.common.c"
210static struct mutex update_lock = {{1}, {{{{{(__ticketpair_t )0}}, 3735899821U, 4294967295U, (void *)-1L}}}, {& update_lock.wait_list,
211 & update_lock.wait_list},
212 (struct task_struct *)0, (char const *)0, (void *)(& update_lock)};
213#line 33 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4773/dscv_tempdir/dscv/ri/32_1/drivers/misc/c2port/c2port-duramar2150.c.common.c"
214static void duramar2150_c2port_access(struct c2port_device *dev , int status )
215{ u8 v ;
216 int __cil_tmp4 ;
217 int __cil_tmp5 ;
218 int __cil_tmp6 ;
219 int __cil_tmp7 ;
220 unsigned char __cil_tmp8 ;
221 int __cil_tmp9 ;
222 int __cil_tmp10 ;
223 int __cil_tmp11 ;
224 int __cil_tmp12 ;
225 int __cil_tmp13 ;
226 unsigned char __cil_tmp14 ;
227
228 {
229 {
230#line 37
231 mutex_lock(& update_lock);
232#line 39
233 v = inb(806);
234 }
235#line 42
236 if (status) {
237 {
238#line 43
239 __cil_tmp4 = 1 << 1;
240#line 43
241 __cil_tmp5 = 1 | __cil_tmp4;
242#line 43
243 __cil_tmp6 = (int )v;
244#line 43
245 __cil_tmp7 = __cil_tmp6 | __cil_tmp5;
246#line 43
247 __cil_tmp8 = (unsigned char )__cil_tmp7;
248#line 43
249 outb(__cil_tmp8, 806);
250 }
251 } else {
252 {
253#line 47
254 __cil_tmp9 = 1 << 1;
255#line 47
256 __cil_tmp10 = 1 | __cil_tmp9;
257#line 47
258 __cil_tmp11 = ~ __cil_tmp10;
259#line 47
260 __cil_tmp12 = (int )v;
261#line 47
262 __cil_tmp13 = __cil_tmp12 & __cil_tmp11;
263#line 47
264 __cil_tmp14 = (unsigned char )__cil_tmp13;
265#line 47
266 outb(__cil_tmp14, 806);
267 }
268 }
269 {
270#line 49
271 mutex_unlock(& update_lock);
272 }
273#line 50
274 return;
275}
276}
277#line 52 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4773/dscv_tempdir/dscv/ri/32_1/drivers/misc/c2port/c2port-duramar2150.c.common.c"
278static void duramar2150_c2port_c2d_dir(struct c2port_device *dev , int dir )
279{ u8 v ;
280 int __cil_tmp4 ;
281 int __cil_tmp5 ;
282 unsigned char __cil_tmp6 ;
283 int __cil_tmp7 ;
284 int __cil_tmp8 ;
285 unsigned char __cil_tmp9 ;
286
287 {
288 {
289#line 56
290 mutex_lock(& update_lock);
291#line 58
292 v = inb(806);
293 }
294#line 60
295 if (dir) {
296 {
297#line 61
298 __cil_tmp4 = (int )v;
299#line 61
300 __cil_tmp5 = __cil_tmp4 & -2;
301#line 61
302 __cil_tmp6 = (unsigned char )__cil_tmp5;
303#line 61
304 outb(__cil_tmp6, 806);
305 }
306 } else {
307 {
308#line 63
309 __cil_tmp7 = (int )v;
310#line 63
311 __cil_tmp8 = __cil_tmp7 | 1;
312#line 63
313 __cil_tmp9 = (unsigned char )__cil_tmp8;
314#line 63
315 outb(__cil_tmp9, 806);
316 }
317 }
318 {
319#line 65
320 mutex_unlock(& update_lock);
321 }
322#line 66
323 return;
324}
325}
326#line 68 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4773/dscv_tempdir/dscv/ri/32_1/drivers/misc/c2port/c2port-duramar2150.c.common.c"
327static int duramar2150_c2port_c2d_get(struct c2port_device *dev )
328{ unsigned char tmp ;
329 int __cil_tmp3 ;
330
331 {
332 {
333#line 70
334 tmp = inb(805);
335 }
336 {
337#line 70
338 __cil_tmp3 = (int )tmp;
339#line 70
340 return (__cil_tmp3 & 1);
341 }
342}
343}
344#line 73 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4773/dscv_tempdir/dscv/ri/32_1/drivers/misc/c2port/c2port-duramar2150.c.common.c"
345static void duramar2150_c2port_c2d_set(struct c2port_device *dev , int status )
346{ u8 v ;
347 int __cil_tmp4 ;
348 int __cil_tmp5 ;
349 unsigned char __cil_tmp6 ;
350 int __cil_tmp7 ;
351 int __cil_tmp8 ;
352 unsigned char __cil_tmp9 ;
353
354 {
355 {
356#line 77
357 mutex_lock(& update_lock);
358#line 79
359 v = inb(805);
360 }
361#line 81
362 if (status) {
363 {
364#line 82
365 __cil_tmp4 = (int )v;
366#line 82
367 __cil_tmp5 = __cil_tmp4 | 1;
368#line 82
369 __cil_tmp6 = (unsigned char )__cil_tmp5;
370#line 82
371 outb(__cil_tmp6, 805);
372 }
373 } else {
374 {
375#line 84
376 __cil_tmp7 = (int )v;
377#line 84
378 __cil_tmp8 = __cil_tmp7 & -2;
379#line 84
380 __cil_tmp9 = (unsigned char )__cil_tmp8;
381#line 84
382 outb(__cil_tmp9, 805);
383 }
384 }
385 {
386#line 86
387 mutex_unlock(& update_lock);
388 }
389#line 87
390 return;
391}
392}
393#line 89 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4773/dscv_tempdir/dscv/ri/32_1/drivers/misc/c2port/c2port-duramar2150.c.common.c"
394static void duramar2150_c2port_c2ck_set(struct c2port_device *dev , int status )
395{ u8 v ;
396 int __cil_tmp4 ;
397 int __cil_tmp5 ;
398 int __cil_tmp6 ;
399 unsigned char __cil_tmp7 ;
400 int __cil_tmp8 ;
401 int __cil_tmp9 ;
402 int __cil_tmp10 ;
403 int __cil_tmp11 ;
404 unsigned char __cil_tmp12 ;
405
406 {
407 {
408#line 93
409 mutex_lock(& update_lock);
410#line 95
411 v = inb(805);
412 }
413#line 97
414 if (status) {
415 {
416#line 98
417 __cil_tmp4 = 1 << 1;
418#line 98
419 __cil_tmp5 = (int )v;
420#line 98
421 __cil_tmp6 = __cil_tmp5 | __cil_tmp4;
422#line 98
423 __cil_tmp7 = (unsigned char )__cil_tmp6;
424#line 98
425 outb(__cil_tmp7, 805);
426 }
427 } else {
428 {
429#line 100
430 __cil_tmp8 = 1 << 1;
431#line 100
432 __cil_tmp9 = ~ __cil_tmp8;
433#line 100
434 __cil_tmp10 = (int )v;
435#line 100
436 __cil_tmp11 = __cil_tmp10 & __cil_tmp9;
437#line 100
438 __cil_tmp12 = (unsigned char )__cil_tmp11;
439#line 100
440 outb(__cil_tmp12, 805);
441 }
442 }
443 {
444#line 102
445 mutex_unlock(& update_lock);
446 }
447#line 103
448 return;
449}
450}
451#line 105 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4773/dscv_tempdir/dscv/ri/32_1/drivers/misc/c2port/c2port-duramar2150.c.common.c"
452static struct c2port_ops duramar2150_c2port_ops = {(unsigned short)512, (unsigned short)30, & duramar2150_c2port_access, & duramar2150_c2port_c2d_dir,
453 & duramar2150_c2port_c2d_get, & duramar2150_c2port_c2d_set, & duramar2150_c2port_c2ck_set};
454#line 116 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4773/dscv_tempdir/dscv/ri/32_1/drivers/misc/c2port/c2port-duramar2150.c.common.c"
455static struct c2port_device *duramar2150_c2port_dev ;
456#line 122
457static int duramar2150_c2port_init(void) __attribute__((__section__(".init.text"),
458__no_instrument_function__)) ;
459#line 122 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4773/dscv_tempdir/dscv/ri/32_1/drivers/misc/c2port/c2port-duramar2150.c.common.c"
460static int duramar2150_c2port_init(void)
461{ struct resource *res ;
462 int ret ;
463 resource_size_t __cil_tmp3 ;
464 resource_size_t __cil_tmp4 ;
465 char *__cil_tmp5 ;
466 void *__cil_tmp6 ;
467 resource_size_t __cil_tmp7 ;
468 resource_size_t __cil_tmp8 ;
469
470 {
471 {
472#line 125
473 ret = 0;
474#line 127
475 __cil_tmp3 = (resource_size_t )805;
476#line 127
477 __cil_tmp4 = (resource_size_t )2;
478#line 127
479 res = __request_region(& ioport_resource, __cil_tmp3, __cil_tmp4, "c2port", 0);
480 }
481#line 128
482 if (! res) {
483#line 129
484 return (-16);
485 } else {
486
487 }
488 {
489#line 131
490 __cil_tmp5 = (char *)"uc";
491#line 131
492 __cil_tmp6 = (void *)0;
493#line 131
494 duramar2150_c2port_dev = c2port_device_register(__cil_tmp5, & duramar2150_c2port_ops,
495 __cil_tmp6);
496 }
497#line 133
498 if (! duramar2150_c2port_dev) {
499#line 134
500 ret = -19;
501#line 135
502 goto free_region;
503 } else {
504
505 }
506#line 138
507 return (0);
508 free_region:
509 {
510#line 141
511 __cil_tmp7 = (resource_size_t )805;
512#line 141
513 __cil_tmp8 = (resource_size_t )2;
514#line 141
515 __release_region(& ioport_resource, __cil_tmp7, __cil_tmp8);
516 }
517#line 142
518 return (ret);
519}
520}
521#line 145
522static void duramar2150_c2port_exit(void) __attribute__((__section__(".exit.text"),
523__no_instrument_function__)) ;
524#line 145 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4773/dscv_tempdir/dscv/ri/32_1/drivers/misc/c2port/c2port-duramar2150.c.common.c"
525static void duramar2150_c2port_exit(void)
526{ resource_size_t __cil_tmp1 ;
527 resource_size_t __cil_tmp2 ;
528
529 {
530 {
531#line 148
532 duramar2150_c2port_access(duramar2150_c2port_dev, 0);
533#line 150
534 c2port_device_unregister(duramar2150_c2port_dev);
535#line 152
536 __cil_tmp1 = (resource_size_t )805;
537#line 152
538 __cil_tmp2 = (resource_size_t )2;
539#line 152
540 __release_region(& ioport_resource, __cil_tmp1, __cil_tmp2);
541 }
542#line 153
543 return;
544}
545}
546#line 155 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4773/dscv_tempdir/dscv/ri/32_1/drivers/misc/c2port/c2port-duramar2150.c.common.c"
547int init_module(void)
548{ int tmp ;
549
550 {
551 {
552#line 155
553 tmp = duramar2150_c2port_init();
554 }
555#line 155
556 return (tmp);
557}
558}
559#line 156 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4773/dscv_tempdir/dscv/ri/32_1/drivers/misc/c2port/c2port-duramar2150.c.common.c"
560void cleanup_module(void)
561{
562
563 {
564 {
565#line 156
566 duramar2150_c2port_exit();
567 }
568#line 156
569 return;
570}
571}
572#line 158 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4773/dscv_tempdir/dscv/ri/32_1/drivers/misc/c2port/c2port-duramar2150.c.common.c"
573static char const __mod_author158[44] __attribute__((__used__, __unused__, __section__(".modinfo"),
574__aligned__(1))) =
575#line 158
576 { (char const )'a', (char const )'u', (char const )'t', (char const )'h',
577 (char const )'o', (char const )'r', (char const )'=', (char const )'R',
578 (char const )'o', (char const )'d', (char const )'o', (char const )'l',
579 (char const )'f', (char const )'o', (char const )' ', (char const )'G',
580 (char const )'i', (char const )'o', (char const )'m', (char const )'e',
581 (char const )'t', (char const )'t', (char const )'i', (char const )' ',
582 (char const )'<', (char const )'g', (char const )'i', (char const )'o',
583 (char const )'m', (char const )'e', (char const )'t', (char const )'t',
584 (char const )'i', (char const )'@', (char const )'l', (char const )'i',
585 (char const )'n', (char const )'u', (char const )'x', (char const )'.',
586 (char const )'i', (char const )'t', (char const )'>', (char const )'\000'};
587#line 159 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4773/dscv_tempdir/dscv/ri/32_1/drivers/misc/c2port/c2port-duramar2150.c.common.c"
588static char const __mod_description159[64] __attribute__((__used__, __unused__,
589__section__(".modinfo"), __aligned__(1))) =
590#line 159
591 { (char const )'d', (char const )'e', (char const )'s', (char const )'c',
592 (char const )'r', (char const )'i', (char const )'p', (char const )'t',
593 (char const )'i', (char const )'o', (char const )'n', (char const )'=',
594 (char const )'S', (char const )'i', (char const )'l', (char const )'i',
595 (char const )'c', (char const )'o', (char const )'n', (char const )' ',
596 (char const )'L', (char const )'a', (char const )'b', (char const )'s',
597 (char const )' ', (char const )'C', (char const )'2', (char const )' ',
598 (char const )'p', (char const )'o', (char const )'r', (char const )'t',
599 (char const )' ', (char const )'L', (char const )'i', (char const )'n',
600 (char const )'u', (char const )'x', (char const )' ', (char const )'s',
601 (char const )'u', (char const )'p', (char const )'p', (char const )'o',
602 (char const )'r', (char const )'t', (char const )' ', (char const )'f',
603 (char const )'o', (char const )'r', (char const )' ', (char const )'D',
604 (char const )'u', (char const )'r', (char const )'a', (char const )'m',
605 (char const )'a', (char const )'r', (char const )' ', (char const )'2',
606 (char const )'1', (char const )'5', (char const )'0', (char const )'\000'};
607#line 160 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4773/dscv_tempdir/dscv/ri/32_1/drivers/misc/c2port/c2port-duramar2150.c.common.c"
608static char const __mod_license160[12] __attribute__((__used__, __unused__, __section__(".modinfo"),
609__aligned__(1))) =
610#line 160
611 { (char const )'l', (char const )'i', (char const )'c', (char const )'e',
612 (char const )'n', (char const )'s', (char const )'e', (char const )'=',
613 (char const )'G', (char const )'P', (char const )'L', (char const )'\000'};
614#line 178
615void ldv_check_final_state(void) ;
616#line 184
617extern void ldv_initialize(void) ;
618#line 187
619extern int __VERIFIER_nondet_int(void) ;
620#line 190 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4773/dscv_tempdir/dscv/ri/32_1/drivers/misc/c2port/c2port-duramar2150.c.common.c"
621int LDV_IN_INTERRUPT ;
622#line 193 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4773/dscv_tempdir/dscv/ri/32_1/drivers/misc/c2port/c2port-duramar2150.c.common.c"
623void main(void)
624{ struct c2port_device *var_group1 ;
625 int var_duramar2150_c2port_access_0_p1 ;
626 int var_duramar2150_c2port_c2d_dir_1_p1 ;
627 int var_duramar2150_c2port_c2d_set_3_p1 ;
628 int var_duramar2150_c2port_c2ck_set_4_p1 ;
629 int tmp ;
630 int tmp___0 ;
631 int tmp___1 ;
632
633 {
634 {
635#line 252
636 LDV_IN_INTERRUPT = 1;
637#line 261
638 ldv_initialize();
639#line 272
640 tmp = duramar2150_c2port_init();
641 }
642#line 272
643 if (tmp) {
644#line 273
645 goto ldv_final;
646 } else {
647
648 }
649 {
650#line 277
651 while (1) {
652 while_continue: ;
653 {
654#line 277
655 tmp___1 = __VERIFIER_nondet_int();
656 }
657#line 277
658 if (tmp___1) {
659
660 } else {
661#line 277
662 goto while_break;
663 }
664 {
665#line 280
666 tmp___0 = __VERIFIER_nondet_int();
667 }
668#line 282
669 if (tmp___0 == 0) {
670#line 282
671 goto case_0;
672 } else
673#line 303
674 if (tmp___0 == 1) {
675#line 303
676 goto case_1;
677 } else
678#line 324
679 if (tmp___0 == 2) {
680#line 324
681 goto case_2;
682 } else
683#line 345
684 if (tmp___0 == 3) {
685#line 345
686 goto case_3;
687 } else
688#line 366
689 if (tmp___0 == 4) {
690#line 366
691 goto case_4;
692 } else {
693 {
694#line 387
695 goto switch_default;
696#line 280
697 if (0) {
698 case_0:
699 {
700#line 295
701 duramar2150_c2port_access(var_group1, var_duramar2150_c2port_access_0_p1);
702 }
703#line 302
704 goto switch_break;
705 case_1:
706 {
707#line 316
708 duramar2150_c2port_c2d_dir(var_group1, var_duramar2150_c2port_c2d_dir_1_p1);
709 }
710#line 323
711 goto switch_break;
712 case_2:
713 {
714#line 337
715 duramar2150_c2port_c2d_get(var_group1);
716 }
717#line 344
718 goto switch_break;
719 case_3:
720 {
721#line 358
722 duramar2150_c2port_c2d_set(var_group1, var_duramar2150_c2port_c2d_set_3_p1);
723 }
724#line 365
725 goto switch_break;
726 case_4:
727 {
728#line 379
729 duramar2150_c2port_c2ck_set(var_group1, var_duramar2150_c2port_c2ck_set_4_p1);
730 }
731#line 386
732 goto switch_break;
733 switch_default:
734#line 387
735 goto switch_break;
736 } else {
737 switch_break: ;
738 }
739 }
740 }
741 }
742 while_break: ;
743 }
744 {
745#line 404
746 duramar2150_c2port_exit();
747 }
748 ldv_final:
749 {
750#line 407
751 ldv_check_final_state();
752 }
753#line 410
754 return;
755}
756}
757#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4773/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
758void ldv_blast_assert(void)
759{
760
761 {
762 ERROR:
763#line 6
764 goto ERROR;
765}
766}
767#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4773/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
768extern int __VERIFIER_nondet_int(void) ;
769#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4773/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
770int ldv_mutex = 1;
771#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4773/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
772int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )
773{ int nondetermined ;
774
775 {
776#line 29
777 if (ldv_mutex == 1) {
778
779 } else {
780 {
781#line 29
782 ldv_blast_assert();
783 }
784 }
785 {
786#line 32
787 nondetermined = __VERIFIER_nondet_int();
788 }
789#line 35
790 if (nondetermined) {
791#line 38
792 ldv_mutex = 2;
793#line 40
794 return (0);
795 } else {
796#line 45
797 return (-4);
798 }
799}
800}
801#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4773/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
802int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock )
803{ int nondetermined ;
804
805 {
806#line 57
807 if (ldv_mutex == 1) {
808
809 } else {
810 {
811#line 57
812 ldv_blast_assert();
813 }
814 }
815 {
816#line 60
817 nondetermined = __VERIFIER_nondet_int();
818 }
819#line 63
820 if (nondetermined) {
821#line 66
822 ldv_mutex = 2;
823#line 68
824 return (0);
825 } else {
826#line 73
827 return (-4);
828 }
829}
830}
831#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4773/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
832int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock )
833{ int atomic_value_after_dec ;
834
835 {
836#line 83
837 if (ldv_mutex == 1) {
838
839 } else {
840 {
841#line 83
842 ldv_blast_assert();
843 }
844 }
845 {
846#line 86
847 atomic_value_after_dec = __VERIFIER_nondet_int();
848 }
849#line 89
850 if (atomic_value_after_dec == 0) {
851#line 92
852 ldv_mutex = 2;
853#line 94
854 return (1);
855 } else {
856
857 }
858#line 98
859 return (0);
860}
861}
862#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4773/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
863void mutex_lock(struct mutex *lock )
864{
865
866 {
867#line 108
868 if (ldv_mutex == 1) {
869
870 } else {
871 {
872#line 108
873 ldv_blast_assert();
874 }
875 }
876#line 110
877 ldv_mutex = 2;
878#line 111
879 return;
880}
881}
882#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4773/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
883int mutex_trylock(struct mutex *lock )
884{ int nondetermined ;
885
886 {
887#line 121
888 if (ldv_mutex == 1) {
889
890 } else {
891 {
892#line 121
893 ldv_blast_assert();
894 }
895 }
896 {
897#line 124
898 nondetermined = __VERIFIER_nondet_int();
899 }
900#line 127
901 if (nondetermined) {
902#line 130
903 ldv_mutex = 2;
904#line 132
905 return (1);
906 } else {
907#line 137
908 return (0);
909 }
910}
911}
912#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4773/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
913void mutex_unlock(struct mutex *lock )
914{
915
916 {
917#line 147
918 if (ldv_mutex == 2) {
919
920 } else {
921 {
922#line 147
923 ldv_blast_assert();
924 }
925 }
926#line 149
927 ldv_mutex = 1;
928#line 150
929 return;
930}
931}
932#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4773/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
933void ldv_check_final_state(void)
934{
935
936 {
937#line 156
938 if (ldv_mutex == 1) {
939
940 } else {
941 {
942#line 156
943 ldv_blast_assert();
944 }
945 }
946#line 157
947 return;
948}
949}
950#line 419 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4773/dscv_tempdir/dscv/ri/32_1/drivers/misc/c2port/c2port-duramar2150.c.common.c"
951long s__builtin_expect(long val , long res )
952{
953
954 {
955#line 420
956 return (val);
957}
958}