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 14 "include/asm-generic/posix_types.h"
13typedef long __kernel_long_t;
14#line 15 "include/asm-generic/posix_types.h"
15typedef unsigned long __kernel_ulong_t;
16#line 75 "include/asm-generic/posix_types.h"
17typedef __kernel_ulong_t __kernel_size_t;
18#line 76 "include/asm-generic/posix_types.h"
19typedef __kernel_long_t __kernel_ssize_t;
20#line 27 "include/linux/types.h"
21typedef unsigned short umode_t;
22#line 63 "include/linux/types.h"
23typedef __kernel_size_t size_t;
24#line 68 "include/linux/types.h"
25typedef __kernel_ssize_t ssize_t;
26#line 202 "include/linux/types.h"
27typedef unsigned int gfp_t;
28#line 206 "include/linux/types.h"
29typedef u64 phys_addr_t;
30#line 211 "include/linux/types.h"
31typedef phys_addr_t resource_size_t;
32#line 221 "include/linux/types.h"
33struct __anonstruct_atomic_t_6 {
34 int counter ;
35};
36#line 221 "include/linux/types.h"
37typedef struct __anonstruct_atomic_t_6 atomic_t;
38#line 226 "include/linux/types.h"
39struct __anonstruct_atomic64_t_7 {
40 long counter ;
41};
42#line 226 "include/linux/types.h"
43typedef struct __anonstruct_atomic64_t_7 atomic64_t;
44#line 227 "include/linux/types.h"
45struct list_head {
46 struct list_head *next ;
47 struct list_head *prev ;
48};
49#line 46 "include/linux/dynamic_debug.h"
50struct device;
51#line 46
52struct device;
53#line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
54struct page;
55#line 58
56struct page;
57#line 26 "include/asm-generic/getorder.h"
58struct task_struct;
59#line 26
60struct task_struct;
61#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
62struct arch_spinlock;
63#line 327
64struct arch_spinlock;
65#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
66struct kmem_cache;
67#line 23 "include/asm-generic/atomic-long.h"
68typedef atomic64_t atomic_long_t;
69#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
70typedef u16 __ticket_t;
71#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
72typedef u32 __ticketpair_t;
73#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
74struct __raw_tickets {
75 __ticket_t head ;
76 __ticket_t tail ;
77};
78#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
79union __anonunion_ldv_5907_29 {
80 __ticketpair_t head_tail ;
81 struct __raw_tickets tickets ;
82};
83#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
84struct arch_spinlock {
85 union __anonunion_ldv_5907_29 ldv_5907 ;
86};
87#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
88typedef struct arch_spinlock arch_spinlock_t;
89#line 34 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
90struct lockdep_map;
91#line 34
92struct lockdep_map;
93#line 55 "include/linux/debug_locks.h"
94struct stack_trace {
95 unsigned int nr_entries ;
96 unsigned int max_entries ;
97 unsigned long *entries ;
98 int skip ;
99};
100#line 26 "include/linux/stacktrace.h"
101struct lockdep_subclass_key {
102 char __one_byte ;
103};
104#line 53 "include/linux/lockdep.h"
105struct lock_class_key {
106 struct lockdep_subclass_key subkeys[8U] ;
107};
108#line 59 "include/linux/lockdep.h"
109struct lock_class {
110 struct list_head hash_entry ;
111 struct list_head lock_entry ;
112 struct lockdep_subclass_key *key ;
113 unsigned int subclass ;
114 unsigned int dep_gen_id ;
115 unsigned long usage_mask ;
116 struct stack_trace usage_traces[13U] ;
117 struct list_head locks_after ;
118 struct list_head locks_before ;
119 unsigned int version ;
120 unsigned long ops ;
121 char const *name ;
122 int name_version ;
123 unsigned long contention_point[4U] ;
124 unsigned long contending_point[4U] ;
125};
126#line 144 "include/linux/lockdep.h"
127struct lockdep_map {
128 struct lock_class_key *key ;
129 struct lock_class *class_cache[2U] ;
130 char const *name ;
131 int cpu ;
132 unsigned long ip ;
133};
134#line 556 "include/linux/lockdep.h"
135struct raw_spinlock {
136 arch_spinlock_t raw_lock ;
137 unsigned int magic ;
138 unsigned int owner_cpu ;
139 void *owner ;
140 struct lockdep_map dep_map ;
141};
142#line 33 "include/linux/spinlock_types.h"
143struct __anonstruct_ldv_6122_33 {
144 u8 __padding[24U] ;
145 struct lockdep_map dep_map ;
146};
147#line 33 "include/linux/spinlock_types.h"
148union __anonunion_ldv_6123_32 {
149 struct raw_spinlock rlock ;
150 struct __anonstruct_ldv_6122_33 ldv_6122 ;
151};
152#line 33 "include/linux/spinlock_types.h"
153struct spinlock {
154 union __anonunion_ldv_6123_32 ldv_6123 ;
155};
156#line 76 "include/linux/spinlock_types.h"
157typedef struct spinlock spinlock_t;
158#line 670 "include/linux/mmzone.h"
159struct mutex {
160 atomic_t count ;
161 spinlock_t wait_lock ;
162 struct list_head wait_list ;
163 struct task_struct *owner ;
164 char const *name ;
165 void *magic ;
166 struct lockdep_map dep_map ;
167};
168#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/e820.h"
169struct resource {
170 resource_size_t start ;
171 resource_size_t end ;
172 char const *name ;
173 unsigned long flags ;
174 struct resource *parent ;
175 struct resource *sibling ;
176 struct resource *child ;
177};
178#line 445 "include/linux/elf.h"
179struct sock;
180#line 445
181struct sock;
182#line 446
183struct kobject;
184#line 446
185struct kobject;
186#line 447
187enum kobj_ns_type {
188 KOBJ_NS_TYPE_NONE = 0,
189 KOBJ_NS_TYPE_NET = 1,
190 KOBJ_NS_TYPES = 2
191} ;
192#line 453 "include/linux/elf.h"
193struct kobj_ns_type_operations {
194 enum kobj_ns_type type ;
195 void *(*grab_current_ns)(void) ;
196 void const *(*netlink_ns)(struct sock * ) ;
197 void const *(*initial_ns)(void) ;
198 void (*drop_ns)(void * ) ;
199};
200#line 57 "include/linux/kobject_ns.h"
201struct attribute {
202 char const *name ;
203 umode_t mode ;
204 struct lock_class_key *key ;
205 struct lock_class_key skey ;
206};
207#line 98 "include/linux/sysfs.h"
208struct sysfs_ops {
209 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
210 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
211 void const *(*namespace)(struct kobject * , struct attribute const * ) ;
212};
213#line 117
214struct sysfs_dirent;
215#line 117
216struct sysfs_dirent;
217#line 182 "include/linux/sysfs.h"
218struct kref {
219 atomic_t refcount ;
220};
221#line 49 "include/linux/kobject.h"
222struct kset;
223#line 49
224struct kobj_type;
225#line 49 "include/linux/kobject.h"
226struct kobject {
227 char const *name ;
228 struct list_head entry ;
229 struct kobject *parent ;
230 struct kset *kset ;
231 struct kobj_type *ktype ;
232 struct sysfs_dirent *sd ;
233 struct kref kref ;
234 unsigned char state_initialized : 1 ;
235 unsigned char state_in_sysfs : 1 ;
236 unsigned char state_add_uevent_sent : 1 ;
237 unsigned char state_remove_uevent_sent : 1 ;
238 unsigned char uevent_suppress : 1 ;
239};
240#line 107 "include/linux/kobject.h"
241struct kobj_type {
242 void (*release)(struct kobject * ) ;
243 struct sysfs_ops const *sysfs_ops ;
244 struct attribute **default_attrs ;
245 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject * ) ;
246 void const *(*namespace)(struct kobject * ) ;
247};
248#line 115 "include/linux/kobject.h"
249struct kobj_uevent_env {
250 char *envp[32U] ;
251 int envp_idx ;
252 char buf[2048U] ;
253 int buflen ;
254};
255#line 122 "include/linux/kobject.h"
256struct kset_uevent_ops {
257 int (* const filter)(struct kset * , struct kobject * ) ;
258 char const *(* const name)(struct kset * , struct kobject * ) ;
259 int (* const uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
260};
261#line 139 "include/linux/kobject.h"
262struct kset {
263 struct list_head list ;
264 spinlock_t list_lock ;
265 struct kobject kobj ;
266 struct kset_uevent_ops const *uevent_ops ;
267};
268#line 88 "include/linux/kmemleak.h"
269struct kmem_cache_cpu {
270 void **freelist ;
271 unsigned long tid ;
272 struct page *page ;
273 struct page *partial ;
274 int node ;
275 unsigned int stat[26U] ;
276};
277#line 55 "include/linux/slub_def.h"
278struct kmem_cache_node {
279 spinlock_t list_lock ;
280 unsigned long nr_partial ;
281 struct list_head partial ;
282 atomic_long_t nr_slabs ;
283 atomic_long_t total_objects ;
284 struct list_head full ;
285};
286#line 66 "include/linux/slub_def.h"
287struct kmem_cache_order_objects {
288 unsigned long x ;
289};
290#line 76 "include/linux/slub_def.h"
291struct kmem_cache {
292 struct kmem_cache_cpu *cpu_slab ;
293 unsigned long flags ;
294 unsigned long min_partial ;
295 int size ;
296 int objsize ;
297 int offset ;
298 int cpu_partial ;
299 struct kmem_cache_order_objects oo ;
300 struct kmem_cache_order_objects max ;
301 struct kmem_cache_order_objects min ;
302 gfp_t allocflags ;
303 int refcount ;
304 void (*ctor)(void * ) ;
305 int inuse ;
306 int align ;
307 int reserved ;
308 char const *name ;
309 struct list_head list ;
310 struct kobject kobj ;
311 int remote_node_defrag_ratio ;
312 struct kmem_cache_node *node[1024U] ;
313};
314#line 116 "include/linux/prio_tree.h"
315struct address_space;
316#line 116
317struct address_space;
318#line 117 "include/linux/prio_tree.h"
319union __anonunion_ldv_14282_136 {
320 unsigned long index ;
321 void *freelist ;
322};
323#line 117 "include/linux/prio_tree.h"
324struct __anonstruct_ldv_14292_140 {
325 unsigned short inuse ;
326 unsigned short objects : 15 ;
327 unsigned char frozen : 1 ;
328};
329#line 117 "include/linux/prio_tree.h"
330union __anonunion_ldv_14293_139 {
331 atomic_t _mapcount ;
332 struct __anonstruct_ldv_14292_140 ldv_14292 ;
333};
334#line 117 "include/linux/prio_tree.h"
335struct __anonstruct_ldv_14295_138 {
336 union __anonunion_ldv_14293_139 ldv_14293 ;
337 atomic_t _count ;
338};
339#line 117 "include/linux/prio_tree.h"
340union __anonunion_ldv_14296_137 {
341 unsigned long counters ;
342 struct __anonstruct_ldv_14295_138 ldv_14295 ;
343};
344#line 117 "include/linux/prio_tree.h"
345struct __anonstruct_ldv_14297_135 {
346 union __anonunion_ldv_14282_136 ldv_14282 ;
347 union __anonunion_ldv_14296_137 ldv_14296 ;
348};
349#line 117 "include/linux/prio_tree.h"
350struct __anonstruct_ldv_14304_142 {
351 struct page *next ;
352 int pages ;
353 int pobjects ;
354};
355#line 117 "include/linux/prio_tree.h"
356union __anonunion_ldv_14305_141 {
357 struct list_head lru ;
358 struct __anonstruct_ldv_14304_142 ldv_14304 ;
359};
360#line 117 "include/linux/prio_tree.h"
361union __anonunion_ldv_14310_143 {
362 unsigned long private ;
363 struct kmem_cache *slab ;
364 struct page *first_page ;
365};
366#line 117 "include/linux/prio_tree.h"
367struct page {
368 unsigned long flags ;
369 struct address_space *mapping ;
370 struct __anonstruct_ldv_14297_135 ldv_14297 ;
371 union __anonunion_ldv_14305_141 ldv_14305 ;
372 union __anonunion_ldv_14310_143 ldv_14310 ;
373 unsigned long debug_flags ;
374};
375#line 158 "include/linux/kmemcheck.h"
376struct c2port_ops;
377#line 158
378struct c2port_ops;
379#line 159 "include/linux/kmemcheck.h"
380struct c2port_device {
381 unsigned char access : 1 ;
382 unsigned char flash_access : 1 ;
383 int id ;
384 char name[32U] ;
385 struct c2port_ops *ops ;
386 struct mutex mutex ;
387 struct device *dev ;
388 void *private_data ;
389};
390#line 39 "include/linux/c2port.h"
391struct c2port_ops {
392 unsigned short block_size ;
393 unsigned short blocks_num ;
394 void (*access)(struct c2port_device * , int ) ;
395 void (*c2d_dir)(struct c2port_device * , int ) ;
396 int (*c2d_get)(struct c2port_device * ) ;
397 void (*c2d_set)(struct c2port_device * , int ) ;
398 void (*c2ck_set)(struct c2port_device * , int ) ;
399};
400#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12478/dscv_tempdir/dscv/ri/43_1a/drivers/misc/c2port/c2port-duramar2150.c.p"
401void ldv_spin_lock(void) ;
402#line 3
403void ldv_spin_unlock(void) ;
404#line 4
405int ldv_spin_trylock(void) ;
406#line 134 "include/linux/mutex.h"
407extern void mutex_lock_nested(struct mutex * , unsigned int ) ;
408#line 169
409extern void mutex_unlock(struct mutex * ) ;
410#line 137 "include/linux/ioport.h"
411extern struct resource ioport_resource ;
412#line 181
413extern struct resource *__request_region(struct resource * , resource_size_t , resource_size_t ,
414 char const * , int ) ;
415#line 192
416extern void __release_region(struct resource * , resource_size_t , resource_size_t ) ;
417#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
418__inline static void outb(unsigned char value , int port )
419{
420
421 {
422#line 308
423 __asm__ volatile ("outb %b0, %w1": : "a" (value), "Nd" (port));
424#line 309
425 return;
426}
427}
428#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
429__inline static unsigned char inb(int port )
430{ unsigned char value ;
431
432 {
433#line 308
434 __asm__ volatile ("inb %w1, %b0": "=a" (value): "Nd" (port));
435#line 308
436 return (value);
437}
438}
439#line 220 "include/linux/slub_def.h"
440extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t ) ;
441#line 223
442void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
443#line 11 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12478/dscv_tempdir/dscv/ri/43_1a/drivers/misc/c2port/c2port-duramar2150.c.p"
444void ldv_check_alloc_flags(gfp_t flags ) ;
445#line 12
446void ldv_check_alloc_nonatomic(void) ;
447#line 14
448struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
449#line 64 "include/linux/c2port.h"
450extern struct c2port_device *c2port_device_register(char * , struct c2port_ops * ,
451 void * ) ;
452#line 66
453extern void c2port_device_unregister(struct c2port_device * ) ;
454#line 41 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12478/dscv_tempdir/dscv/ri/43_1a/drivers/misc/c2port/c2port-duramar2150.c.p"
455static struct mutex update_lock = {{1}, {{{{{0U}}, 3735899821U, 4294967295U, (void *)0xffffffffffffffffUL, {(struct lock_class_key *)0,
456 {(struct lock_class *)0,
457 (struct lock_class *)0},
458 "update_lock.wait_lock",
459 0, 0UL}}}},
460 {& update_lock.wait_list, & update_lock.wait_list}, (struct task_struct *)0, (char const *)0,
461 (void *)(& update_lock), {(struct lock_class_key *)0, {(struct lock_class *)0,
462 (struct lock_class *)0},
463 "update_lock", 0, 0UL}};
464#line 47 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12478/dscv_tempdir/dscv/ri/43_1a/drivers/misc/c2port/c2port-duramar2150.c.p"
465static void duramar2150_c2port_access(struct c2port_device *dev , int status )
466{ u8 v ;
467 unsigned int __cil_tmp4 ;
468 unsigned int __cil_tmp5 ;
469 int __cil_tmp6 ;
470 unsigned char __cil_tmp7 ;
471 int __cil_tmp8 ;
472 int __cil_tmp9 ;
473 unsigned char __cil_tmp10 ;
474
475 {
476 {
477#line 51
478 mutex_lock_nested(& update_lock, 0U);
479#line 53
480 v = inb(806);
481 }
482#line 56
483 if (status != 0) {
484 {
485#line 57
486 __cil_tmp4 = (unsigned int )v;
487#line 57
488 __cil_tmp5 = __cil_tmp4 | 3U;
489#line 57
490 __cil_tmp6 = (int )__cil_tmp5;
491#line 57
492 __cil_tmp7 = (unsigned char )__cil_tmp6;
493#line 57
494 outb(__cil_tmp7, 806);
495 }
496 } else {
497 {
498#line 61
499 __cil_tmp8 = (int )v;
500#line 61
501 __cil_tmp9 = __cil_tmp8 & 252;
502#line 61
503 __cil_tmp10 = (unsigned char )__cil_tmp9;
504#line 61
505 outb(__cil_tmp10, 806);
506 }
507 }
508 {
509#line 63
510 mutex_unlock(& update_lock);
511 }
512#line 64
513 return;
514}
515}
516#line 66 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12478/dscv_tempdir/dscv/ri/43_1a/drivers/misc/c2port/c2port-duramar2150.c.p"
517static void duramar2150_c2port_c2d_dir(struct c2port_device *dev , int dir )
518{ u8 v ;
519 int __cil_tmp4 ;
520 int __cil_tmp5 ;
521 unsigned char __cil_tmp6 ;
522 unsigned int __cil_tmp7 ;
523 unsigned int __cil_tmp8 ;
524 int __cil_tmp9 ;
525 unsigned char __cil_tmp10 ;
526
527 {
528 {
529#line 70
530 mutex_lock_nested(& update_lock, 0U);
531#line 72
532 v = inb(806);
533 }
534#line 74
535 if (dir != 0) {
536 {
537#line 75
538 __cil_tmp4 = (int )v;
539#line 75
540 __cil_tmp5 = __cil_tmp4 & 254;
541#line 75
542 __cil_tmp6 = (unsigned char )__cil_tmp5;
543#line 75
544 outb(__cil_tmp6, 806);
545 }
546 } else {
547 {
548#line 77
549 __cil_tmp7 = (unsigned int )v;
550#line 77
551 __cil_tmp8 = __cil_tmp7 | 1U;
552#line 77
553 __cil_tmp9 = (int )__cil_tmp8;
554#line 77
555 __cil_tmp10 = (unsigned char )__cil_tmp9;
556#line 77
557 outb(__cil_tmp10, 806);
558 }
559 }
560 {
561#line 79
562 mutex_unlock(& update_lock);
563 }
564#line 80
565 return;
566}
567}
568#line 82 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12478/dscv_tempdir/dscv/ri/43_1a/drivers/misc/c2port/c2port-duramar2150.c.p"
569static int duramar2150_c2port_c2d_get(struct c2port_device *dev )
570{ unsigned char tmp ;
571 int __cil_tmp3 ;
572
573 {
574 {
575#line 84
576 tmp = inb(805);
577 }
578 {
579#line 84
580 __cil_tmp3 = (int )tmp;
581#line 84
582 return (__cil_tmp3 & 1);
583 }
584}
585}
586#line 87 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12478/dscv_tempdir/dscv/ri/43_1a/drivers/misc/c2port/c2port-duramar2150.c.p"
587static void duramar2150_c2port_c2d_set(struct c2port_device *dev , int status )
588{ u8 v ;
589 unsigned int __cil_tmp4 ;
590 unsigned int __cil_tmp5 ;
591 int __cil_tmp6 ;
592 unsigned char __cil_tmp7 ;
593 int __cil_tmp8 ;
594 int __cil_tmp9 ;
595 unsigned char __cil_tmp10 ;
596
597 {
598 {
599#line 91
600 mutex_lock_nested(& update_lock, 0U);
601#line 93
602 v = inb(805);
603 }
604#line 95
605 if (status != 0) {
606 {
607#line 96
608 __cil_tmp4 = (unsigned int )v;
609#line 96
610 __cil_tmp5 = __cil_tmp4 | 1U;
611#line 96
612 __cil_tmp6 = (int )__cil_tmp5;
613#line 96
614 __cil_tmp7 = (unsigned char )__cil_tmp6;
615#line 96
616 outb(__cil_tmp7, 805);
617 }
618 } else {
619 {
620#line 98
621 __cil_tmp8 = (int )v;
622#line 98
623 __cil_tmp9 = __cil_tmp8 & 254;
624#line 98
625 __cil_tmp10 = (unsigned char )__cil_tmp9;
626#line 98
627 outb(__cil_tmp10, 805);
628 }
629 }
630 {
631#line 100
632 mutex_unlock(& update_lock);
633 }
634#line 101
635 return;
636}
637}
638#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12478/dscv_tempdir/dscv/ri/43_1a/drivers/misc/c2port/c2port-duramar2150.c.p"
639static void duramar2150_c2port_c2ck_set(struct c2port_device *dev , int status )
640{ u8 v ;
641 unsigned int __cil_tmp4 ;
642 unsigned int __cil_tmp5 ;
643 int __cil_tmp6 ;
644 unsigned char __cil_tmp7 ;
645 int __cil_tmp8 ;
646 int __cil_tmp9 ;
647 unsigned char __cil_tmp10 ;
648
649 {
650 {
651#line 107
652 mutex_lock_nested(& update_lock, 0U);
653#line 109
654 v = inb(805);
655 }
656#line 111
657 if (status != 0) {
658 {
659#line 112
660 __cil_tmp4 = (unsigned int )v;
661#line 112
662 __cil_tmp5 = __cil_tmp4 | 2U;
663#line 112
664 __cil_tmp6 = (int )__cil_tmp5;
665#line 112
666 __cil_tmp7 = (unsigned char )__cil_tmp6;
667#line 112
668 outb(__cil_tmp7, 805);
669 }
670 } else {
671 {
672#line 114
673 __cil_tmp8 = (int )v;
674#line 114
675 __cil_tmp9 = __cil_tmp8 & 253;
676#line 114
677 __cil_tmp10 = (unsigned char )__cil_tmp9;
678#line 114
679 outb(__cil_tmp10, 805);
680 }
681 }
682 {
683#line 116
684 mutex_unlock(& update_lock);
685 }
686#line 117
687 return;
688}
689}
690#line 119 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12478/dscv_tempdir/dscv/ri/43_1a/drivers/misc/c2port/c2port-duramar2150.c.p"
691static struct c2port_ops duramar2150_c2port_ops = {(unsigned short)512, (unsigned short)30, & duramar2150_c2port_access, & duramar2150_c2port_c2d_dir,
692 & duramar2150_c2port_c2d_get, & duramar2150_c2port_c2d_set, & duramar2150_c2port_c2ck_set};
693#line 130 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12478/dscv_tempdir/dscv/ri/43_1a/drivers/misc/c2port/c2port-duramar2150.c.p"
694static struct c2port_device *duramar2150_c2port_dev ;
695#line 136 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12478/dscv_tempdir/dscv/ri/43_1a/drivers/misc/c2port/c2port-duramar2150.c.p"
696static int duramar2150_c2port_init(void)
697{ struct resource *res ;
698 int ret ;
699 struct resource *__cil_tmp3 ;
700 unsigned long __cil_tmp4 ;
701 unsigned long __cil_tmp5 ;
702 char *__cil_tmp6 ;
703 void *__cil_tmp7 ;
704 struct c2port_device *__cil_tmp8 ;
705 unsigned long __cil_tmp9 ;
706 unsigned long __cil_tmp10 ;
707
708 {
709 {
710#line 139
711 ret = 0;
712#line 141
713 res = __request_region(& ioport_resource, 805ULL, 2ULL, "c2port", 0);
714 }
715 {
716#line 142
717 __cil_tmp3 = (struct resource *)0;
718#line 142
719 __cil_tmp4 = (unsigned long )__cil_tmp3;
720#line 142
721 __cil_tmp5 = (unsigned long )res;
722#line 142
723 if (__cil_tmp5 == __cil_tmp4) {
724#line 143
725 return (-16);
726 } else {
727
728 }
729 }
730 {
731#line 145
732 __cil_tmp6 = (char *)"uc";
733#line 145
734 __cil_tmp7 = (void *)0;
735#line 145
736 duramar2150_c2port_dev = c2port_device_register(__cil_tmp6, & duramar2150_c2port_ops,
737 __cil_tmp7);
738 }
739 {
740#line 147
741 __cil_tmp8 = (struct c2port_device *)0;
742#line 147
743 __cil_tmp9 = (unsigned long )__cil_tmp8;
744#line 147
745 __cil_tmp10 = (unsigned long )duramar2150_c2port_dev;
746#line 147
747 if (__cil_tmp10 == __cil_tmp9) {
748#line 148
749 ret = -19;
750#line 149
751 goto free_region;
752 } else {
753
754 }
755 }
756#line 152
757 return (0);
758 free_region:
759 {
760#line 155
761 __release_region(& ioport_resource, 805ULL, 2ULL);
762 }
763#line 156
764 return (ret);
765}
766}
767#line 159 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12478/dscv_tempdir/dscv/ri/43_1a/drivers/misc/c2port/c2port-duramar2150.c.p"
768static void duramar2150_c2port_exit(void)
769{
770
771 {
772 {
773#line 162
774 duramar2150_c2port_access(duramar2150_c2port_dev, 0);
775#line 164
776 c2port_device_unregister(duramar2150_c2port_dev);
777#line 166
778 __release_region(& ioport_resource, 805ULL, 2ULL);
779 }
780#line 167
781 return;
782}
783}
784#line 192
785extern void ldv_check_final_state(void) ;
786#line 198
787extern void ldv_initialize(void) ;
788#line 201
789extern int __VERIFIER_nondet_int(void) ;
790#line 204 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12478/dscv_tempdir/dscv/ri/43_1a/drivers/misc/c2port/c2port-duramar2150.c.p"
791int LDV_IN_INTERRUPT ;
792#line 207 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12478/dscv_tempdir/dscv/ri/43_1a/drivers/misc/c2port/c2port-duramar2150.c.p"
793void main(void)
794{ struct c2port_device *var_group1 ;
795 int var_duramar2150_c2port_access_0_p1 ;
796 int var_duramar2150_c2port_c2d_dir_1_p1 ;
797 int var_duramar2150_c2port_c2d_set_3_p1 ;
798 int var_duramar2150_c2port_c2ck_set_4_p1 ;
799 int tmp ;
800 int tmp___0 ;
801 int tmp___1 ;
802
803 {
804 {
805#line 266
806 LDV_IN_INTERRUPT = 1;
807#line 275
808 ldv_initialize();
809#line 286
810 tmp = duramar2150_c2port_init();
811 }
812#line 286
813 if (tmp != 0) {
814#line 287
815 goto ldv_final;
816 } else {
817
818 }
819#line 291
820 goto ldv_14606;
821 ldv_14605:
822 {
823#line 294
824 tmp___0 = __VERIFIER_nondet_int();
825 }
826#line 296
827 if (tmp___0 == 0) {
828#line 296
829 goto case_0;
830 } else
831#line 317
832 if (tmp___0 == 1) {
833#line 317
834 goto case_1;
835 } else
836#line 338
837 if (tmp___0 == 2) {
838#line 338
839 goto case_2;
840 } else
841#line 359
842 if (tmp___0 == 3) {
843#line 359
844 goto case_3;
845 } else
846#line 380
847 if (tmp___0 == 4) {
848#line 380
849 goto case_4;
850 } else {
851 {
852#line 401
853 goto switch_default;
854#line 294
855 if (0) {
856 case_0:
857 {
858#line 309
859 duramar2150_c2port_access(var_group1, var_duramar2150_c2port_access_0_p1);
860 }
861#line 316
862 goto ldv_14599;
863 case_1:
864 {
865#line 330
866 duramar2150_c2port_c2d_dir(var_group1, var_duramar2150_c2port_c2d_dir_1_p1);
867 }
868#line 337
869 goto ldv_14599;
870 case_2:
871 {
872#line 351
873 duramar2150_c2port_c2d_get(var_group1);
874 }
875#line 358
876 goto ldv_14599;
877 case_3:
878 {
879#line 372
880 duramar2150_c2port_c2d_set(var_group1, var_duramar2150_c2port_c2d_set_3_p1);
881 }
882#line 379
883 goto ldv_14599;
884 case_4:
885 {
886#line 393
887 duramar2150_c2port_c2ck_set(var_group1, var_duramar2150_c2port_c2ck_set_4_p1);
888 }
889#line 400
890 goto ldv_14599;
891 switch_default: ;
892#line 401
893 goto ldv_14599;
894 } else {
895 switch_break: ;
896 }
897 }
898 }
899 ldv_14599: ;
900 ldv_14606:
901 {
902#line 291
903 tmp___1 = __VERIFIER_nondet_int();
904 }
905#line 291
906 if (tmp___1 != 0) {
907#line 292
908 goto ldv_14605;
909 } else {
910#line 294
911 goto ldv_14607;
912 }
913 ldv_14607: ;
914 {
915#line 418
916 duramar2150_c2port_exit();
917 }
918 ldv_final:
919 {
920#line 421
921 ldv_check_final_state();
922 }
923#line 424
924 return;
925}
926}
927#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12478/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
928void ldv_blast_assert(void)
929{
930
931 {
932 ERROR: ;
933#line 6
934 goto ERROR;
935}
936}
937#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12478/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
938extern int __VERIFIER_nondet_int(void) ;
939#line 445 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12478/dscv_tempdir/dscv/ri/43_1a/drivers/misc/c2port/c2port-duramar2150.c.p"
940int ldv_spin = 0;
941#line 449 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12478/dscv_tempdir/dscv/ri/43_1a/drivers/misc/c2port/c2port-duramar2150.c.p"
942void ldv_check_alloc_flags(gfp_t flags )
943{
944
945 {
946#line 452
947 if (ldv_spin != 0) {
948#line 452
949 if (flags != 32U) {
950 {
951#line 452
952 ldv_blast_assert();
953 }
954 } else {
955
956 }
957 } else {
958
959 }
960#line 455
961 return;
962}
963}
964#line 455
965extern struct page *ldv_some_page(void) ;
966#line 458 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12478/dscv_tempdir/dscv/ri/43_1a/drivers/misc/c2port/c2port-duramar2150.c.p"
967struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags )
968{ struct page *tmp ;
969
970 {
971#line 461
972 if (ldv_spin != 0) {
973#line 461
974 if (flags != 32U) {
975 {
976#line 461
977 ldv_blast_assert();
978 }
979 } else {
980
981 }
982 } else {
983
984 }
985 {
986#line 463
987 tmp = ldv_some_page();
988 }
989#line 463
990 return (tmp);
991}
992}
993#line 467 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12478/dscv_tempdir/dscv/ri/43_1a/drivers/misc/c2port/c2port-duramar2150.c.p"
994void ldv_check_alloc_nonatomic(void)
995{
996
997 {
998#line 470
999 if (ldv_spin != 0) {
1000 {
1001#line 470
1002 ldv_blast_assert();
1003 }
1004 } else {
1005
1006 }
1007#line 473
1008 return;
1009}
1010}
1011#line 474 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12478/dscv_tempdir/dscv/ri/43_1a/drivers/misc/c2port/c2port-duramar2150.c.p"
1012void ldv_spin_lock(void)
1013{
1014
1015 {
1016#line 477
1017 ldv_spin = 1;
1018#line 478
1019 return;
1020}
1021}
1022#line 481 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12478/dscv_tempdir/dscv/ri/43_1a/drivers/misc/c2port/c2port-duramar2150.c.p"
1023void ldv_spin_unlock(void)
1024{
1025
1026 {
1027#line 484
1028 ldv_spin = 0;
1029#line 485
1030 return;
1031}
1032}
1033#line 488 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12478/dscv_tempdir/dscv/ri/43_1a/drivers/misc/c2port/c2port-duramar2150.c.p"
1034int ldv_spin_trylock(void)
1035{ int is_lock ;
1036
1037 {
1038 {
1039#line 493
1040 is_lock = __VERIFIER_nondet_int();
1041 }
1042#line 495
1043 if (is_lock != 0) {
1044#line 498
1045 return (0);
1046 } else {
1047#line 503
1048 ldv_spin = 1;
1049#line 505
1050 return (1);
1051 }
1052}
1053}
1054#line 672 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12478/dscv_tempdir/dscv/ri/43_1a/drivers/misc/c2port/c2port-duramar2150.c.p"
1055void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 )
1056{
1057
1058 {
1059 {
1060#line 678
1061 ldv_check_alloc_flags(ldv_func_arg2);
1062#line 680
1063 kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
1064 }
1065#line 681
1066 return ((void *)0);
1067}
1068}