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 14 "include/asm-generic/posix_types.h"
11typedef long __kernel_long_t;
12#line 15 "include/asm-generic/posix_types.h"
13typedef unsigned long __kernel_ulong_t;
14#line 75 "include/asm-generic/posix_types.h"
15typedef __kernel_ulong_t __kernel_size_t;
16#line 76 "include/asm-generic/posix_types.h"
17typedef __kernel_long_t __kernel_ssize_t;
18#line 27 "include/linux/types.h"
19typedef unsigned short umode_t;
20#line 38 "include/linux/types.h"
21typedef _Bool bool;
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 221 "include/linux/types.h"
29struct __anonstruct_atomic_t_6 {
30 int counter ;
31};
32#line 221 "include/linux/types.h"
33typedef struct __anonstruct_atomic_t_6 atomic_t;
34#line 226 "include/linux/types.h"
35struct __anonstruct_atomic64_t_7 {
36 long counter ;
37};
38#line 226 "include/linux/types.h"
39typedef struct __anonstruct_atomic64_t_7 atomic64_t;
40#line 227 "include/linux/types.h"
41struct list_head {
42 struct list_head *next ;
43 struct list_head *prev ;
44};
45#line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
46struct page;
47#line 58
48struct page;
49#line 26 "include/asm-generic/getorder.h"
50struct task_struct;
51#line 26
52struct task_struct;
53#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
54struct arch_spinlock;
55#line 327
56struct arch_spinlock;
57#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
58struct kmem_cache;
59#line 23 "include/asm-generic/atomic-long.h"
60typedef atomic64_t atomic_long_t;
61#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
62typedef u16 __ticket_t;
63#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
64typedef u32 __ticketpair_t;
65#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
66struct __raw_tickets {
67 __ticket_t head ;
68 __ticket_t tail ;
69};
70#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
71union __anonunion_ldv_5907_29 {
72 __ticketpair_t head_tail ;
73 struct __raw_tickets tickets ;
74};
75#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
76struct arch_spinlock {
77 union __anonunion_ldv_5907_29 ldv_5907 ;
78};
79#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
80typedef struct arch_spinlock arch_spinlock_t;
81#line 34 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
82struct lockdep_map;
83#line 34
84struct lockdep_map;
85#line 55 "include/linux/debug_locks.h"
86struct stack_trace {
87 unsigned int nr_entries ;
88 unsigned int max_entries ;
89 unsigned long *entries ;
90 int skip ;
91};
92#line 26 "include/linux/stacktrace.h"
93struct lockdep_subclass_key {
94 char __one_byte ;
95};
96#line 53 "include/linux/lockdep.h"
97struct lock_class_key {
98 struct lockdep_subclass_key subkeys[8U] ;
99};
100#line 59 "include/linux/lockdep.h"
101struct lock_class {
102 struct list_head hash_entry ;
103 struct list_head lock_entry ;
104 struct lockdep_subclass_key *key ;
105 unsigned int subclass ;
106 unsigned int dep_gen_id ;
107 unsigned long usage_mask ;
108 struct stack_trace usage_traces[13U] ;
109 struct list_head locks_after ;
110 struct list_head locks_before ;
111 unsigned int version ;
112 unsigned long ops ;
113 char const *name ;
114 int name_version ;
115 unsigned long contention_point[4U] ;
116 unsigned long contending_point[4U] ;
117};
118#line 144 "include/linux/lockdep.h"
119struct lockdep_map {
120 struct lock_class_key *key ;
121 struct lock_class *class_cache[2U] ;
122 char const *name ;
123 int cpu ;
124 unsigned long ip ;
125};
126#line 556 "include/linux/lockdep.h"
127struct raw_spinlock {
128 arch_spinlock_t raw_lock ;
129 unsigned int magic ;
130 unsigned int owner_cpu ;
131 void *owner ;
132 struct lockdep_map dep_map ;
133};
134#line 33 "include/linux/spinlock_types.h"
135struct __anonstruct_ldv_6122_33 {
136 u8 __padding[24U] ;
137 struct lockdep_map dep_map ;
138};
139#line 33 "include/linux/spinlock_types.h"
140union __anonunion_ldv_6123_32 {
141 struct raw_spinlock rlock ;
142 struct __anonstruct_ldv_6122_33 ldv_6122 ;
143};
144#line 33 "include/linux/spinlock_types.h"
145struct spinlock {
146 union __anonunion_ldv_6123_32 ldv_6123 ;
147};
148#line 76 "include/linux/spinlock_types.h"
149typedef struct spinlock spinlock_t;
150#line 670 "include/linux/mmzone.h"
151struct mutex {
152 atomic_t count ;
153 spinlock_t wait_lock ;
154 struct list_head wait_list ;
155 struct task_struct *owner ;
156 char const *name ;
157 void *magic ;
158 struct lockdep_map dep_map ;
159};
160#line 341 "include/linux/ktime.h"
161struct tvec_base;
162#line 341
163struct tvec_base;
164#line 342 "include/linux/ktime.h"
165struct timer_list {
166 struct list_head entry ;
167 unsigned long expires ;
168 struct tvec_base *base ;
169 void (*function)(unsigned long ) ;
170 unsigned long data ;
171 int slack ;
172 int start_pid ;
173 void *start_site ;
174 char start_comm[16U] ;
175 struct lockdep_map lockdep_map ;
176};
177#line 301 "include/linux/timer.h"
178struct workqueue_struct;
179#line 301
180struct workqueue_struct;
181#line 302
182struct work_struct;
183#line 302
184struct work_struct;
185#line 45 "include/linux/workqueue.h"
186struct work_struct {
187 atomic_long_t data ;
188 struct list_head entry ;
189 void (*func)(struct work_struct * ) ;
190 struct lockdep_map lockdep_map ;
191};
192#line 86 "include/linux/workqueue.h"
193struct delayed_work {
194 struct work_struct work ;
195 struct timer_list timer ;
196};
197#line 445 "include/linux/elf.h"
198struct sock;
199#line 445
200struct sock;
201#line 446
202struct kobject;
203#line 446
204struct kobject;
205#line 447
206enum kobj_ns_type {
207 KOBJ_NS_TYPE_NONE = 0,
208 KOBJ_NS_TYPE_NET = 1,
209 KOBJ_NS_TYPES = 2
210} ;
211#line 453 "include/linux/elf.h"
212struct kobj_ns_type_operations {
213 enum kobj_ns_type type ;
214 void *(*grab_current_ns)(void) ;
215 void const *(*netlink_ns)(struct sock * ) ;
216 void const *(*initial_ns)(void) ;
217 void (*drop_ns)(void * ) ;
218};
219#line 57 "include/linux/kobject_ns.h"
220struct attribute {
221 char const *name ;
222 umode_t mode ;
223 struct lock_class_key *key ;
224 struct lock_class_key skey ;
225};
226#line 98 "include/linux/sysfs.h"
227struct sysfs_ops {
228 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
229 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
230 void const *(*namespace)(struct kobject * , struct attribute const * ) ;
231};
232#line 117
233struct sysfs_dirent;
234#line 117
235struct sysfs_dirent;
236#line 182 "include/linux/sysfs.h"
237struct kref {
238 atomic_t refcount ;
239};
240#line 49 "include/linux/kobject.h"
241struct kset;
242#line 49
243struct kobj_type;
244#line 49 "include/linux/kobject.h"
245struct kobject {
246 char const *name ;
247 struct list_head entry ;
248 struct kobject *parent ;
249 struct kset *kset ;
250 struct kobj_type *ktype ;
251 struct sysfs_dirent *sd ;
252 struct kref kref ;
253 unsigned char state_initialized : 1 ;
254 unsigned char state_in_sysfs : 1 ;
255 unsigned char state_add_uevent_sent : 1 ;
256 unsigned char state_remove_uevent_sent : 1 ;
257 unsigned char uevent_suppress : 1 ;
258};
259#line 107 "include/linux/kobject.h"
260struct kobj_type {
261 void (*release)(struct kobject * ) ;
262 struct sysfs_ops const *sysfs_ops ;
263 struct attribute **default_attrs ;
264 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject * ) ;
265 void const *(*namespace)(struct kobject * ) ;
266};
267#line 115 "include/linux/kobject.h"
268struct kobj_uevent_env {
269 char *envp[32U] ;
270 int envp_idx ;
271 char buf[2048U] ;
272 int buflen ;
273};
274#line 122 "include/linux/kobject.h"
275struct kset_uevent_ops {
276 int (* const filter)(struct kset * , struct kobject * ) ;
277 char const *(* const name)(struct kset * , struct kobject * ) ;
278 int (* const uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
279};
280#line 139 "include/linux/kobject.h"
281struct kset {
282 struct list_head list ;
283 spinlock_t list_lock ;
284 struct kobject kobj ;
285 struct kset_uevent_ops const *uevent_ops ;
286};
287#line 88 "include/linux/kmemleak.h"
288struct kmem_cache_cpu {
289 void **freelist ;
290 unsigned long tid ;
291 struct page *page ;
292 struct page *partial ;
293 int node ;
294 unsigned int stat[26U] ;
295};
296#line 55 "include/linux/slub_def.h"
297struct kmem_cache_node {
298 spinlock_t list_lock ;
299 unsigned long nr_partial ;
300 struct list_head partial ;
301 atomic_long_t nr_slabs ;
302 atomic_long_t total_objects ;
303 struct list_head full ;
304};
305#line 66 "include/linux/slub_def.h"
306struct kmem_cache_order_objects {
307 unsigned long x ;
308};
309#line 76 "include/linux/slub_def.h"
310struct kmem_cache {
311 struct kmem_cache_cpu *cpu_slab ;
312 unsigned long flags ;
313 unsigned long min_partial ;
314 int size ;
315 int objsize ;
316 int offset ;
317 int cpu_partial ;
318 struct kmem_cache_order_objects oo ;
319 struct kmem_cache_order_objects max ;
320 struct kmem_cache_order_objects min ;
321 gfp_t allocflags ;
322 int refcount ;
323 void (*ctor)(void * ) ;
324 int inuse ;
325 int align ;
326 int reserved ;
327 char const *name ;
328 struct list_head list ;
329 struct kobject kobj ;
330 int remote_node_defrag_ratio ;
331 struct kmem_cache_node *node[1024U] ;
332};
333#line 1 "<compiler builtins>"
334
335#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
336void ldv_spin_lock(void) ;
337#line 3
338void ldv_spin_unlock(void) ;
339#line 4
340int ldv_spin_trylock(void) ;
341#line 98 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/bitops.h"
342__inline static void clear_bit(int nr , unsigned long volatile *addr )
343{ long volatile *__cil_tmp3 ;
344
345 {
346#line 105
347 __cil_tmp3 = (long volatile *)addr;
348#line 105
349 __asm__ volatile (".section .smp_locks,\"a\"\n.balign 4\n.long 671f - .\n.previous\n671:\n\tlock; btr %1,%0": "+m" (*__cil_tmp3): "Ir" (nr));
350#line 107
351 return;
352}
353}
354#line 101 "include/linux/printk.h"
355extern int printk(char const * , ...) ;
356#line 34 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/string_64.h"
357extern void *__memcpy(void * , void const * , size_t ) ;
358#line 60
359extern int memcmp(void const * , void const * , size_t ) ;
360#line 134 "include/linux/mutex.h"
361extern void mutex_lock_nested(struct mutex * , unsigned int ) ;
362#line 169
363extern void mutex_unlock(struct mutex * ) ;
364#line 36 "include/linux/timer.h"
365extern struct tvec_base boot_tvec_bases ;
366#line 280
367extern int del_timer_sync(struct timer_list * ) ;
368#line 304 "include/linux/workqueue.h"
369extern struct workqueue_struct *__alloc_workqueue_key(char const * , unsigned int ,
370 int , struct lock_class_key * ,
371 char const * , ...) ;
372#line 366
373extern void destroy_workqueue(struct workqueue_struct * ) ;
374#line 371
375extern int queue_delayed_work(struct workqueue_struct * , struct delayed_work * ,
376 unsigned long ) ;
377#line 376
378extern void flush_workqueue(struct workqueue_struct * ) ;
379#line 410 "include/linux/workqueue.h"
380__inline static bool cancel_delayed_work(struct delayed_work *work )
381{ bool ret ;
382 int tmp ;
383 unsigned long __cil_tmp4 ;
384 unsigned long __cil_tmp5 ;
385 struct timer_list *__cil_tmp6 ;
386 int __cil_tmp7 ;
387 atomic_long_t *__cil_tmp8 ;
388 unsigned long volatile *__cil_tmp9 ;
389
390 {
391 {
392#line 414
393 __cil_tmp4 = (unsigned long )work;
394#line 414
395 __cil_tmp5 = __cil_tmp4 + 80;
396#line 414
397 __cil_tmp6 = (struct timer_list *)__cil_tmp5;
398#line 414
399 tmp = del_timer_sync(__cil_tmp6);
400#line 414
401 __cil_tmp7 = tmp != 0;
402#line 414
403 ret = (bool )__cil_tmp7;
404 }
405#line 415
406 if ((int )ret) {
407 {
408#line 416
409 __cil_tmp8 = (atomic_long_t *)work;
410#line 416
411 __cil_tmp9 = (unsigned long volatile *)__cil_tmp8;
412#line 416
413 clear_bit(0, __cil_tmp9);
414 }
415 } else {
416
417 }
418#line 417
419 return (ret);
420}
421}
422#line 347 "include/linux/gfp.h"
423extern unsigned long get_zeroed_page(gfp_t ) ;
424#line 361
425extern void free_pages(unsigned long , unsigned int ) ;
426#line 161 "include/linux/slab.h"
427extern void kfree(void const * ) ;
428#line 220 "include/linux/slub_def.h"
429extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t ) ;
430#line 223
431void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
432#line 225
433extern void *__kmalloc(size_t , gfp_t ) ;
434#line 268 "include/linux/slub_def.h"
435__inline static void *ldv_kmalloc_12(size_t size , gfp_t flags )
436{ void *tmp___2 ;
437
438 {
439 {
440#line 283
441 tmp___2 = __kmalloc(size, flags);
442 }
443#line 283
444 return (tmp___2);
445}
446}
447#line 268
448__inline static void *kmalloc(size_t size , gfp_t flags ) ;
449#line 11 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
450void ldv_check_alloc_flags(gfp_t flags ) ;
451#line 12
452void ldv_check_alloc_nonatomic(void) ;
453#line 14
454struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
455#line 29 "include/linux/ks0108.h"
456extern void ks0108_writedata(unsigned char ) ;
457#line 32
458extern void ks0108_writecontrol(unsigned char ) ;
459#line 35
460extern void ks0108_displaystate(unsigned char ) ;
461#line 38
462extern void ks0108_startline(unsigned char ) ;
463#line 41
464extern void ks0108_address(unsigned char ) ;
465#line 44
466extern void ks0108_page(unsigned char ) ;
467#line 47
468extern unsigned char ks0108_isinited(void) ;
469#line 42 "include/linux/cfag12864b.h"
470unsigned char *cfag12864b_buffer ;
471#line 49
472unsigned int cfag12864b_getrate(void) ;
473#line 57
474unsigned char cfag12864b_enable(void) ;
475#line 64
476void cfag12864b_disable(void) ;
477#line 74
478unsigned char cfag12864b_isenabled(void) ;
479#line 79
480unsigned char cfag12864b_isinited(void) ;
481#line 64 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
482static unsigned int cfag12864b_rate = 20U;
483#line 69 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
484unsigned int cfag12864b_getrate(void)
485{ unsigned int *__cil_tmp1 ;
486
487 {
488 {
489#line 71
490 __cil_tmp1 = & cfag12864b_rate;
491#line 71
492 return (*__cil_tmp1);
493 }
494}
495}
496#line 100 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
497static unsigned char cfag12864b_state ;
498#line 102 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
499static void cfag12864b_set(void)
500{ int __cil_tmp1 ;
501 unsigned char __cil_tmp2 ;
502
503 {
504 {
505#line 104
506 __cil_tmp1 = (int )cfag12864b_state;
507#line 104
508 __cil_tmp2 = (unsigned char )__cil_tmp1;
509#line 104
510 ks0108_writecontrol(__cil_tmp2);
511 }
512#line 105
513 return;
514}
515}
516#line 107 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
517static void cfag12864b_setbit(unsigned char state , unsigned char n )
518{ unsigned int __cil_tmp3 ;
519 signed char __cil_tmp4 ;
520 int __cil_tmp5 ;
521 int __cil_tmp6 ;
522 int __cil_tmp7 ;
523 signed char __cil_tmp8 ;
524 int __cil_tmp9 ;
525 int __cil_tmp10 ;
526 signed char __cil_tmp11 ;
527 int __cil_tmp12 ;
528 int __cil_tmp13 ;
529 int __cil_tmp14 ;
530 signed char __cil_tmp15 ;
531 int __cil_tmp16 ;
532 int __cil_tmp17 ;
533 int __cil_tmp18 ;
534
535 {
536 {
537#line 109
538 __cil_tmp3 = (unsigned int )state;
539#line 109
540 if (__cil_tmp3 != 0U) {
541#line 110
542 __cil_tmp4 = (signed char )cfag12864b_state;
543#line 110
544 __cil_tmp5 = (int )__cil_tmp4;
545#line 110
546 __cil_tmp6 = (int )n;
547#line 110
548 __cil_tmp7 = 1 << __cil_tmp6;
549#line 110
550 __cil_tmp8 = (signed char )__cil_tmp7;
551#line 110
552 __cil_tmp9 = (int )__cil_tmp8;
553#line 110
554 __cil_tmp10 = __cil_tmp9 | __cil_tmp5;
555#line 110
556 cfag12864b_state = (unsigned char )__cil_tmp10;
557 } else {
558#line 112
559 __cil_tmp11 = (signed char )cfag12864b_state;
560#line 112
561 __cil_tmp12 = (int )__cil_tmp11;
562#line 112
563 __cil_tmp13 = (int )n;
564#line 112
565 __cil_tmp14 = 1 << __cil_tmp13;
566#line 112
567 __cil_tmp15 = (signed char )__cil_tmp14;
568#line 112
569 __cil_tmp16 = (int )__cil_tmp15;
570#line 112
571 __cil_tmp17 = ~ __cil_tmp16;
572#line 112
573 __cil_tmp18 = __cil_tmp17 & __cil_tmp12;
574#line 112
575 cfag12864b_state = (unsigned char )__cil_tmp18;
576 }
577 }
578#line 113
579 return;
580}
581}
582#line 115 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
583static void cfag12864b_e(unsigned char state )
584{ int __cil_tmp2 ;
585 unsigned char __cil_tmp3 ;
586
587 {
588 {
589#line 117
590 __cil_tmp2 = (int )state;
591#line 117
592 __cil_tmp3 = (unsigned char )__cil_tmp2;
593#line 117
594 cfag12864b_setbit(__cil_tmp3, (unsigned char)0);
595#line 118
596 cfag12864b_set();
597 }
598#line 119
599 return;
600}
601}
602#line 121 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
603static void cfag12864b_cs1(unsigned char state )
604{ int __cil_tmp2 ;
605 unsigned char __cil_tmp3 ;
606
607 {
608 {
609#line 123
610 __cil_tmp2 = (int )state;
611#line 123
612 __cil_tmp3 = (unsigned char )__cil_tmp2;
613#line 123
614 cfag12864b_setbit(__cil_tmp3, (unsigned char)2);
615 }
616#line 124
617 return;
618}
619}
620#line 126 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
621static void cfag12864b_cs2(unsigned char state )
622{ int __cil_tmp2 ;
623 unsigned char __cil_tmp3 ;
624
625 {
626 {
627#line 128
628 __cil_tmp2 = (int )state;
629#line 128
630 __cil_tmp3 = (unsigned char )__cil_tmp2;
631#line 128
632 cfag12864b_setbit(__cil_tmp3, (unsigned char)1);
633 }
634#line 129
635 return;
636}
637}
638#line 131 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
639static void cfag12864b_di(unsigned char state )
640{ int __cil_tmp2 ;
641 unsigned char __cil_tmp3 ;
642
643 {
644 {
645#line 133
646 __cil_tmp2 = (int )state;
647#line 133
648 __cil_tmp3 = (unsigned char )__cil_tmp2;
649#line 133
650 cfag12864b_setbit(__cil_tmp3, (unsigned char)3);
651 }
652#line 134
653 return;
654}
655}
656#line 136 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
657static void cfag12864b_setcontrollers(unsigned char first , unsigned char second )
658{ unsigned int __cil_tmp3 ;
659 unsigned int __cil_tmp4 ;
660
661 {
662 {
663#line 139
664 __cil_tmp3 = (unsigned int )first;
665#line 139
666 if (__cil_tmp3 != 0U) {
667 {
668#line 140
669 cfag12864b_cs1((unsigned char)0);
670 }
671 } else {
672 {
673#line 142
674 cfag12864b_cs1((unsigned char)1);
675 }
676 }
677 }
678 {
679#line 144
680 __cil_tmp4 = (unsigned int )second;
681#line 144
682 if (__cil_tmp4 != 0U) {
683 {
684#line 145
685 cfag12864b_cs2((unsigned char)0);
686 }
687 } else {
688 {
689#line 147
690 cfag12864b_cs2((unsigned char)1);
691 }
692 }
693 }
694#line 148
695 return;
696}
697}
698#line 150 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
699static void cfag12864b_controller(unsigned char which )
700{ unsigned int __cil_tmp2 ;
701 unsigned int __cil_tmp3 ;
702
703 {
704 {
705#line 152
706 __cil_tmp2 = (unsigned int )which;
707#line 152
708 if (__cil_tmp2 == 0U) {
709 {
710#line 153
711 cfag12864b_setcontrollers((unsigned char)1, (unsigned char)0);
712 }
713 } else {
714 {
715#line 154
716 __cil_tmp3 = (unsigned int )which;
717#line 154
718 if (__cil_tmp3 == 1U) {
719 {
720#line 155
721 cfag12864b_setcontrollers((unsigned char)0, (unsigned char)1);
722 }
723 } else {
724
725 }
726 }
727 }
728 }
729#line 156
730 return;
731}
732}
733#line 158 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
734static void cfag12864b_displaystate(unsigned char state )
735{ int __cil_tmp2 ;
736 unsigned char __cil_tmp3 ;
737
738 {
739 {
740#line 160
741 cfag12864b_di((unsigned char)0);
742#line 161
743 cfag12864b_e((unsigned char)1);
744#line 162
745 __cil_tmp2 = (int )state;
746#line 162
747 __cil_tmp3 = (unsigned char )__cil_tmp2;
748#line 162
749 ks0108_displaystate(__cil_tmp3);
750#line 163
751 cfag12864b_e((unsigned char)0);
752 }
753#line 164
754 return;
755}
756}
757#line 166 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
758static void cfag12864b_address(unsigned char address )
759{ int __cil_tmp2 ;
760 unsigned char __cil_tmp3 ;
761
762 {
763 {
764#line 168
765 cfag12864b_di((unsigned char)0);
766#line 169
767 cfag12864b_e((unsigned char)1);
768#line 170
769 __cil_tmp2 = (int )address;
770#line 170
771 __cil_tmp3 = (unsigned char )__cil_tmp2;
772#line 170
773 ks0108_address(__cil_tmp3);
774#line 171
775 cfag12864b_e((unsigned char)0);
776 }
777#line 172
778 return;
779}
780}
781#line 174 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
782static void cfag12864b_page(unsigned char page )
783{ int __cil_tmp2 ;
784 unsigned char __cil_tmp3 ;
785
786 {
787 {
788#line 176
789 cfag12864b_di((unsigned char)0);
790#line 177
791 cfag12864b_e((unsigned char)1);
792#line 178
793 __cil_tmp2 = (int )page;
794#line 178
795 __cil_tmp3 = (unsigned char )__cil_tmp2;
796#line 178
797 ks0108_page(__cil_tmp3);
798#line 179
799 cfag12864b_e((unsigned char)0);
800 }
801#line 180
802 return;
803}
804}
805#line 182 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
806static void cfag12864b_startline(unsigned char startline )
807{ int __cil_tmp2 ;
808 unsigned char __cil_tmp3 ;
809
810 {
811 {
812#line 184
813 cfag12864b_di((unsigned char)0);
814#line 185
815 cfag12864b_e((unsigned char)1);
816#line 186
817 __cil_tmp2 = (int )startline;
818#line 186
819 __cil_tmp3 = (unsigned char )__cil_tmp2;
820#line 186
821 ks0108_startline(__cil_tmp3);
822#line 187
823 cfag12864b_e((unsigned char)0);
824 }
825#line 188
826 return;
827}
828}
829#line 190 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
830static void cfag12864b_writebyte(unsigned char byte )
831{ int __cil_tmp2 ;
832 unsigned char __cil_tmp3 ;
833
834 {
835 {
836#line 192
837 cfag12864b_di((unsigned char)1);
838#line 193
839 cfag12864b_e((unsigned char)1);
840#line 194
841 __cil_tmp2 = (int )byte;
842#line 194
843 __cil_tmp3 = (unsigned char )__cil_tmp2;
844#line 194
845 ks0108_writedata(__cil_tmp3);
846#line 195
847 cfag12864b_e((unsigned char)0);
848 }
849#line 196
850 return;
851}
852}
853#line 198 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
854static void cfag12864b_nop(void)
855{
856
857 {
858 {
859#line 200
860 cfag12864b_startline((unsigned char)0);
861 }
862#line 201
863 return;
864}
865}
866#line 207 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
867static void cfag12864b_on(void)
868{
869
870 {
871 {
872#line 209
873 cfag12864b_setcontrollers((unsigned char)1, (unsigned char)1);
874#line 210
875 cfag12864b_displaystate((unsigned char)1);
876 }
877#line 211
878 return;
879}
880}
881#line 213 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
882static void cfag12864b_off(void)
883{
884
885 {
886 {
887#line 215
888 cfag12864b_setcontrollers((unsigned char)1, (unsigned char)1);
889#line 216
890 cfag12864b_displaystate((unsigned char)0);
891 }
892#line 217
893 return;
894}
895}
896#line 219 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
897static void cfag12864b_clear(void)
898{ unsigned char i ;
899 unsigned char j ;
900 int __cil_tmp3 ;
901 unsigned char __cil_tmp4 ;
902 int __cil_tmp5 ;
903 int __cil_tmp6 ;
904 unsigned int __cil_tmp7 ;
905 int __cil_tmp8 ;
906 int __cil_tmp9 ;
907 unsigned int __cil_tmp10 ;
908
909 {
910 {
911#line 223
912 cfag12864b_setcontrollers((unsigned char)1, (unsigned char)1);
913#line 224
914 i = (unsigned char)0;
915 }
916#line 224
917 goto ldv_18762;
918 ldv_18761:
919 {
920#line 225
921 __cil_tmp3 = (int )i;
922#line 225
923 __cil_tmp4 = (unsigned char )__cil_tmp3;
924#line 225
925 cfag12864b_page(__cil_tmp4);
926#line 226
927 cfag12864b_address((unsigned char)0);
928#line 227
929 j = (unsigned char)0;
930 }
931#line 227
932 goto ldv_18759;
933 ldv_18758:
934 {
935#line 228
936 cfag12864b_writebyte((unsigned char)0);
937#line 227
938 __cil_tmp5 = (int )j;
939#line 227
940 __cil_tmp6 = __cil_tmp5 + 1;
941#line 227
942 j = (unsigned char )__cil_tmp6;
943 }
944 ldv_18759: ;
945 {
946#line 227
947 __cil_tmp7 = (unsigned int )j;
948#line 227
949 if (__cil_tmp7 <= 63U) {
950#line 228
951 goto ldv_18758;
952 } else {
953#line 230
954 goto ldv_18760;
955 }
956 }
957 ldv_18760:
958#line 224
959 __cil_tmp8 = (int )i;
960#line 224
961 __cil_tmp9 = __cil_tmp8 + 1;
962#line 224
963 i = (unsigned char )__cil_tmp9;
964 ldv_18762: ;
965 {
966#line 224
967 __cil_tmp10 = (unsigned int )i;
968#line 224
969 if (__cil_tmp10 <= 7U) {
970#line 225
971 goto ldv_18761;
972 } else {
973#line 227
974 goto ldv_18763;
975 }
976 }
977 ldv_18763: ;
978#line 229
979 return;
980}
981}
982#line 237 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
983static unsigned char *cfag12864b_cache ;
984#line 238 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
985static struct mutex cfag12864b_mutex = {{1}, {{{{{0U}}, 3735899821U, 4294967295U, (void *)0xffffffffffffffffUL, {(struct lock_class_key *)0,
986 {(struct lock_class *)0,
987 (struct lock_class *)0},
988 "cfag12864b_mutex.wait_lock",
989 0, 0UL}}}},
990 {& cfag12864b_mutex.wait_list, & cfag12864b_mutex.wait_list}, (struct task_struct *)0,
991 (char const *)0, (void *)(& cfag12864b_mutex), {(struct lock_class_key *)0,
992 {(struct lock_class *)0, (struct lock_class *)0},
993 "cfag12864b_mutex", 0, 0UL}};
994#line 239 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
995static unsigned char cfag12864b_updating ;
996#line 240
997static void cfag12864b_update(struct work_struct *work ) ;
998#line 241 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
999static struct workqueue_struct *cfag12864b_workqueue ;
1000#line 242 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
1001static struct delayed_work cfag12864b_work = {{{2097680L}, {& cfag12864b_work.work.entry, & cfag12864b_work.work.entry}, & cfag12864b_update,
1002 {(struct lock_class_key *)(& cfag12864b_work.work), {(struct lock_class *)0,
1003 (struct lock_class *)0},
1004 "(cfag12864b_work).work", 0, 0UL}}, {{(struct list_head *)0, (struct list_head *)1953723489},
1005 0UL, & boot_tvec_bases, (void (*)(unsigned long ))0,
1006 0UL, -1, 0, (void *)0, {(char)0, (char)0,
1007 (char)0, (char)0,
1008 (char)0, (char)0,
1009 (char)0, (char)0,
1010 (char)0, (char)0,
1011 (char)0, (char)0,
1012 (char)0, (char)0,
1013 (char)0, (char)0},
1014 {(struct lock_class_key *)"/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p:242",
1015 {(struct lock_class *)0, (struct lock_class *)0},
1016 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p:242",
1017 0, 0UL}}};
1018#line 244 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
1019static void cfag12864b_queue(void)
1020{ unsigned int *__cil_tmp1 ;
1021 unsigned int __cil_tmp2 ;
1022 unsigned int __cil_tmp3 ;
1023 unsigned long __cil_tmp4 ;
1024
1025 {
1026 {
1027#line 246
1028 __cil_tmp1 = & cfag12864b_rate;
1029#line 246
1030 __cil_tmp2 = *__cil_tmp1;
1031#line 246
1032 __cil_tmp3 = 250U / __cil_tmp2;
1033#line 246
1034 __cil_tmp4 = (unsigned long )__cil_tmp3;
1035#line 246
1036 queue_delayed_work(cfag12864b_workqueue, & cfag12864b_work, __cil_tmp4);
1037 }
1038#line 248
1039 return;
1040}
1041}
1042#line 250 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
1043unsigned char cfag12864b_enable(void)
1044{ unsigned char ret ;
1045 unsigned int __cil_tmp2 ;
1046
1047 {
1048 {
1049#line 254
1050 mutex_lock_nested(& cfag12864b_mutex, 0U);
1051 }
1052 {
1053#line 256
1054 __cil_tmp2 = (unsigned int )cfag12864b_updating;
1055#line 256
1056 if (__cil_tmp2 == 0U) {
1057 {
1058#line 257
1059 cfag12864b_updating = (unsigned char)1;
1060#line 258
1061 cfag12864b_queue();
1062#line 259
1063 ret = (unsigned char)0;
1064 }
1065 } else {
1066#line 261
1067 ret = (unsigned char)1;
1068 }
1069 }
1070 {
1071#line 263
1072 mutex_unlock(& cfag12864b_mutex);
1073 }
1074#line 265
1075 return (ret);
1076}
1077}
1078#line 268 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
1079void cfag12864b_disable(void)
1080{ unsigned int __cil_tmp1 ;
1081
1082 {
1083 {
1084#line 270
1085 mutex_lock_nested(& cfag12864b_mutex, 0U);
1086 }
1087 {
1088#line 272
1089 __cil_tmp1 = (unsigned int )cfag12864b_updating;
1090#line 272
1091 if (__cil_tmp1 != 0U) {
1092 {
1093#line 273
1094 cfag12864b_updating = (unsigned char)0;
1095#line 274
1096 cancel_delayed_work(& cfag12864b_work);
1097#line 275
1098 flush_workqueue(cfag12864b_workqueue);
1099 }
1100 } else {
1101
1102 }
1103 }
1104 {
1105#line 278
1106 mutex_unlock(& cfag12864b_mutex);
1107 }
1108#line 279
1109 return;
1110}
1111}
1112#line 281 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
1113unsigned char cfag12864b_isenabled(void)
1114{
1115
1116 {
1117#line 283
1118 return (cfag12864b_updating);
1119}
1120}
1121#line 286 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
1122static void cfag12864b_update(struct work_struct *work )
1123{ unsigned char c ;
1124 unsigned short i ;
1125 unsigned short j ;
1126 unsigned short k ;
1127 unsigned short b ;
1128 size_t __len ;
1129 void *__ret ;
1130 int tmp ;
1131 void const *__cil_tmp10 ;
1132 unsigned char **__cil_tmp11 ;
1133 unsigned char *__cil_tmp12 ;
1134 void const *__cil_tmp13 ;
1135 unsigned char __cil_tmp14 ;
1136 int __cil_tmp15 ;
1137 unsigned char __cil_tmp16 ;
1138 unsigned char __cil_tmp17 ;
1139 int __cil_tmp18 ;
1140 unsigned char __cil_tmp19 ;
1141 int __cil_tmp20 ;
1142 int __cil_tmp21 ;
1143 int __cil_tmp22 ;
1144 int __cil_tmp23 ;
1145 int __cil_tmp24 ;
1146 int __cil_tmp25 ;
1147 int __cil_tmp26 ;
1148 int __cil_tmp27 ;
1149 unsigned int __cil_tmp28 ;
1150 unsigned int __cil_tmp29 ;
1151 int __cil_tmp30 ;
1152 int __cil_tmp31 ;
1153 int __cil_tmp32 ;
1154 int __cil_tmp33 ;
1155 int __cil_tmp34 ;
1156 int __cil_tmp35 ;
1157 unsigned long __cil_tmp36 ;
1158 unsigned char **__cil_tmp37 ;
1159 unsigned char *__cil_tmp38 ;
1160 unsigned char *__cil_tmp39 ;
1161 unsigned char __cil_tmp40 ;
1162 int __cil_tmp41 ;
1163 int __cil_tmp42 ;
1164 signed char __cil_tmp43 ;
1165 int __cil_tmp44 ;
1166 int __cil_tmp45 ;
1167 int __cil_tmp46 ;
1168 signed char __cil_tmp47 ;
1169 int __cil_tmp48 ;
1170 int __cil_tmp49 ;
1171 int __cil_tmp50 ;
1172 int __cil_tmp51 ;
1173 unsigned int __cil_tmp52 ;
1174 int __cil_tmp53 ;
1175 unsigned char __cil_tmp54 ;
1176 int __cil_tmp55 ;
1177 int __cil_tmp56 ;
1178 unsigned int __cil_tmp57 ;
1179 int __cil_tmp58 ;
1180 int __cil_tmp59 ;
1181 unsigned int __cil_tmp60 ;
1182 int __cil_tmp61 ;
1183 int __cil_tmp62 ;
1184 unsigned int __cil_tmp63 ;
1185 void *__cil_tmp64 ;
1186 unsigned char **__cil_tmp65 ;
1187 unsigned char *__cil_tmp66 ;
1188 void const *__cil_tmp67 ;
1189 void *__cil_tmp68 ;
1190 unsigned char **__cil_tmp69 ;
1191 unsigned char *__cil_tmp70 ;
1192 void const *__cil_tmp71 ;
1193 unsigned int __cil_tmp72 ;
1194
1195 {
1196 {
1197#line 291
1198 __cil_tmp10 = (void const *)cfag12864b_cache;
1199#line 291
1200 __cil_tmp11 = & cfag12864b_buffer;
1201#line 291
1202 __cil_tmp12 = *__cil_tmp11;
1203#line 291
1204 __cil_tmp13 = (void const *)__cil_tmp12;
1205#line 291
1206 tmp = memcmp(__cil_tmp10, __cil_tmp13, 1024UL);
1207 }
1208#line 291
1209 if (tmp != 0) {
1210#line 292
1211 i = (unsigned short)0;
1212#line 292
1213 goto ldv_18804;
1214 ldv_18803:
1215 {
1216#line 293
1217 __cil_tmp14 = (unsigned char )i;
1218#line 293
1219 __cil_tmp15 = (int )__cil_tmp14;
1220#line 293
1221 __cil_tmp16 = (unsigned char )__cil_tmp15;
1222#line 293
1223 cfag12864b_controller(__cil_tmp16);
1224#line 294
1225 cfag12864b_nop();
1226#line 295
1227 j = (unsigned short)0;
1228 }
1229#line 295
1230 goto ldv_18801;
1231 ldv_18800:
1232 {
1233#line 296
1234 __cil_tmp17 = (unsigned char )j;
1235#line 296
1236 __cil_tmp18 = (int )__cil_tmp17;
1237#line 296
1238 __cil_tmp19 = (unsigned char )__cil_tmp18;
1239#line 296
1240 cfag12864b_page(__cil_tmp19);
1241#line 297
1242 cfag12864b_nop();
1243#line 298
1244 cfag12864b_address((unsigned char)0);
1245#line 299
1246 cfag12864b_nop();
1247#line 300
1248 k = (unsigned short)0;
1249 }
1250#line 300
1251 goto ldv_18798;
1252 ldv_18797:
1253#line 301
1254 c = (unsigned char)0;
1255#line 301
1256 b = (unsigned short)0;
1257#line 301
1258 goto ldv_18795;
1259 ldv_18794: ;
1260 {
1261#line 302
1262 __cil_tmp20 = (int )k;
1263#line 302
1264 __cil_tmp21 = __cil_tmp20 & 7;
1265#line 302
1266 __cil_tmp22 = (int )b;
1267#line 302
1268 __cil_tmp23 = (int )j;
1269#line 302
1270 __cil_tmp24 = __cil_tmp23 * 8;
1271#line 302
1272 __cil_tmp25 = __cil_tmp24 + __cil_tmp22;
1273#line 302
1274 __cil_tmp26 = __cil_tmp25 * 128;
1275#line 302
1276 __cil_tmp27 = __cil_tmp26 / 8;
1277#line 302
1278 __cil_tmp28 = (unsigned int )k;
1279#line 302
1280 __cil_tmp29 = __cil_tmp28 / 8U;
1281#line 302
1282 __cil_tmp30 = (int )__cil_tmp29;
1283#line 302
1284 __cil_tmp31 = (int )i;
1285#line 302
1286 __cil_tmp32 = __cil_tmp31 * 64;
1287#line 302
1288 __cil_tmp33 = __cil_tmp32 / 8;
1289#line 302
1290 __cil_tmp34 = __cil_tmp33 + __cil_tmp30;
1291#line 302
1292 __cil_tmp35 = __cil_tmp34 + __cil_tmp27;
1293#line 302
1294 __cil_tmp36 = (unsigned long )__cil_tmp35;
1295#line 302
1296 __cil_tmp37 = & cfag12864b_buffer;
1297#line 302
1298 __cil_tmp38 = *__cil_tmp37;
1299#line 302
1300 __cil_tmp39 = __cil_tmp38 + __cil_tmp36;
1301#line 302
1302 __cil_tmp40 = *__cil_tmp39;
1303#line 302
1304 __cil_tmp41 = (int )__cil_tmp40;
1305#line 302
1306 __cil_tmp42 = __cil_tmp41 >> __cil_tmp21;
1307#line 302
1308 if (__cil_tmp42 & 1) {
1309#line 307
1310 __cil_tmp43 = (signed char )c;
1311#line 307
1312 __cil_tmp44 = (int )__cil_tmp43;
1313#line 307
1314 __cil_tmp45 = (int )b;
1315#line 307
1316 __cil_tmp46 = 1 << __cil_tmp45;
1317#line 307
1318 __cil_tmp47 = (signed char )__cil_tmp46;
1319#line 307
1320 __cil_tmp48 = (int )__cil_tmp47;
1321#line 307
1322 __cil_tmp49 = __cil_tmp48 | __cil_tmp44;
1323#line 307
1324 c = (unsigned char )__cil_tmp49;
1325 } else {
1326
1327 }
1328 }
1329#line 301
1330 __cil_tmp50 = (int )b;
1331#line 301
1332 __cil_tmp51 = __cil_tmp50 + 1;
1333#line 301
1334 b = (unsigned short )__cil_tmp51;
1335 ldv_18795: ;
1336 {
1337#line 301
1338 __cil_tmp52 = (unsigned int )b;
1339#line 301
1340 if (__cil_tmp52 <= 7U) {
1341#line 302
1342 goto ldv_18794;
1343 } else {
1344#line 304
1345 goto ldv_18796;
1346 }
1347 }
1348 ldv_18796:
1349 {
1350#line 308
1351 __cil_tmp53 = (int )c;
1352#line 308
1353 __cil_tmp54 = (unsigned char )__cil_tmp53;
1354#line 308
1355 cfag12864b_writebyte(__cil_tmp54);
1356#line 300
1357 __cil_tmp55 = (int )k;
1358#line 300
1359 __cil_tmp56 = __cil_tmp55 + 1;
1360#line 300
1361 k = (unsigned short )__cil_tmp56;
1362 }
1363 ldv_18798: ;
1364 {
1365#line 300
1366 __cil_tmp57 = (unsigned int )k;
1367#line 300
1368 if (__cil_tmp57 <= 63U) {
1369#line 301
1370 goto ldv_18797;
1371 } else {
1372#line 303
1373 goto ldv_18799;
1374 }
1375 }
1376 ldv_18799:
1377#line 295
1378 __cil_tmp58 = (int )j;
1379#line 295
1380 __cil_tmp59 = __cil_tmp58 + 1;
1381#line 295
1382 j = (unsigned short )__cil_tmp59;
1383 ldv_18801: ;
1384 {
1385#line 295
1386 __cil_tmp60 = (unsigned int )j;
1387#line 295
1388 if (__cil_tmp60 <= 7U) {
1389#line 296
1390 goto ldv_18800;
1391 } else {
1392#line 298
1393 goto ldv_18802;
1394 }
1395 }
1396 ldv_18802:
1397#line 292
1398 __cil_tmp61 = (int )i;
1399#line 292
1400 __cil_tmp62 = __cil_tmp61 + 1;
1401#line 292
1402 i = (unsigned short )__cil_tmp62;
1403 ldv_18804: ;
1404 {
1405#line 292
1406 __cil_tmp63 = (unsigned int )i;
1407#line 292
1408 if (__cil_tmp63 <= 1U) {
1409#line 293
1410 goto ldv_18803;
1411 } else {
1412#line 295
1413 goto ldv_18805;
1414 }
1415 }
1416 ldv_18805:
1417#line 313
1418 __len = 1024UL;
1419#line 313
1420 if (__len > 63UL) {
1421 {
1422#line 313
1423 __cil_tmp64 = (void *)cfag12864b_cache;
1424#line 313
1425 __cil_tmp65 = & cfag12864b_buffer;
1426#line 313
1427 __cil_tmp66 = *__cil_tmp65;
1428#line 313
1429 __cil_tmp67 = (void const *)__cil_tmp66;
1430#line 313
1431 __ret = __memcpy(__cil_tmp64, __cil_tmp67, __len);
1432 }
1433 } else {
1434 {
1435#line 313
1436 __cil_tmp68 = (void *)cfag12864b_cache;
1437#line 313
1438 __cil_tmp69 = & cfag12864b_buffer;
1439#line 313
1440 __cil_tmp70 = *__cil_tmp69;
1441#line 313
1442 __cil_tmp71 = (void const *)__cil_tmp70;
1443#line 313
1444 __ret = __builtin_memcpy(__cil_tmp68, __cil_tmp71, __len);
1445 }
1446 }
1447 } else {
1448
1449 }
1450 {
1451#line 316
1452 __cil_tmp72 = (unsigned int )cfag12864b_updating;
1453#line 316
1454 if (__cil_tmp72 != 0U) {
1455 {
1456#line 317
1457 cfag12864b_queue();
1458 }
1459 } else {
1460
1461 }
1462 }
1463#line 318
1464 return;
1465}
1466}
1467#line 334 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
1468static unsigned char cfag12864b_inited ;
1469#line 335 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
1470unsigned char cfag12864b_isinited(void)
1471{
1472
1473 {
1474#line 337
1475 return (cfag12864b_inited);
1476}
1477}
1478#line 345 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
1479static int cfag12864b_init(void)
1480{ int ret ;
1481 unsigned char tmp ;
1482 unsigned long tmp___0 ;
1483 void *tmp___1 ;
1484 struct lock_class_key __key ;
1485 char const *__lock_name ;
1486 struct workqueue_struct *tmp___2 ;
1487 unsigned int __cil_tmp8 ;
1488 unsigned char **__cil_tmp9 ;
1489 unsigned char *__cil_tmp10 ;
1490 unsigned long __cil_tmp11 ;
1491 unsigned char **__cil_tmp12 ;
1492 unsigned char *__cil_tmp13 ;
1493 unsigned long __cil_tmp14 ;
1494 unsigned char *__cil_tmp15 ;
1495 unsigned long __cil_tmp16 ;
1496 unsigned long __cil_tmp17 ;
1497 struct workqueue_struct *__cil_tmp18 ;
1498 unsigned long __cil_tmp19 ;
1499 unsigned long __cil_tmp20 ;
1500 void const *__cil_tmp21 ;
1501 unsigned char **__cil_tmp22 ;
1502 unsigned char *__cil_tmp23 ;
1503 unsigned long __cil_tmp24 ;
1504
1505 {
1506 {
1507#line 347
1508 ret = -22;
1509#line 350
1510 tmp = ks0108_isinited();
1511 }
1512 {
1513#line 350
1514 __cil_tmp8 = (unsigned int )tmp;
1515#line 350
1516 if (__cil_tmp8 == 0U) {
1517 {
1518#line 351
1519 printk("<3>cfag12864b: ERROR: ks0108 is not initialized\n");
1520 }
1521#line 353
1522 goto none;
1523 } else {
1524
1525 }
1526 }
1527 {
1528#line 357
1529 tmp___0 = get_zeroed_page(208U);
1530#line 357
1531 __cil_tmp9 = & cfag12864b_buffer;
1532#line 357
1533 *__cil_tmp9 = (unsigned char *)tmp___0;
1534 }
1535 {
1536#line 358
1537 __cil_tmp10 = (unsigned char *)0;
1538#line 358
1539 __cil_tmp11 = (unsigned long )__cil_tmp10;
1540#line 358
1541 __cil_tmp12 = & cfag12864b_buffer;
1542#line 358
1543 __cil_tmp13 = *__cil_tmp12;
1544#line 358
1545 __cil_tmp14 = (unsigned long )__cil_tmp13;
1546#line 358
1547 if (__cil_tmp14 == __cil_tmp11) {
1548 {
1549#line 359
1550 printk("<3>cfag12864b: ERROR: can\'t get a free page\n");
1551#line 361
1552 ret = -12;
1553 }
1554#line 362
1555 goto none;
1556 } else {
1557
1558 }
1559 }
1560 {
1561#line 365
1562 tmp___1 = kmalloc(1024UL, 208U);
1563#line 365
1564 cfag12864b_cache = (unsigned char *)tmp___1;
1565 }
1566 {
1567#line 367
1568 __cil_tmp15 = (unsigned char *)0;
1569#line 367
1570 __cil_tmp16 = (unsigned long )__cil_tmp15;
1571#line 367
1572 __cil_tmp17 = (unsigned long )cfag12864b_cache;
1573#line 367
1574 if (__cil_tmp17 == __cil_tmp16) {
1575 {
1576#line 368
1577 printk("<3>cfag12864b: ERROR: can\'t alloc cache buffer (%i bytes)\n", 1024);
1578#line 371
1579 ret = -12;
1580 }
1581#line 372
1582 goto bufferalloced;
1583 } else {
1584
1585 }
1586 }
1587 {
1588#line 375
1589 __lock_name = "cfag12864b";
1590#line 375
1591 tmp___2 = __alloc_workqueue_key("cfag12864b", 10U, 1, & __key, __lock_name);
1592#line 375
1593 cfag12864b_workqueue = tmp___2;
1594 }
1595 {
1596#line 376
1597 __cil_tmp18 = (struct workqueue_struct *)0;
1598#line 376
1599 __cil_tmp19 = (unsigned long )__cil_tmp18;
1600#line 376
1601 __cil_tmp20 = (unsigned long )cfag12864b_workqueue;
1602#line 376
1603 if (__cil_tmp20 == __cil_tmp19) {
1604#line 377
1605 goto cachealloced;
1606 } else {
1607
1608 }
1609 }
1610 {
1611#line 379
1612 cfag12864b_clear();
1613#line 380
1614 cfag12864b_on();
1615#line 382
1616 cfag12864b_inited = (unsigned char)1;
1617 }
1618#line 383
1619 return (0);
1620 cachealloced:
1621 {
1622#line 386
1623 __cil_tmp21 = (void const *)cfag12864b_cache;
1624#line 386
1625 kfree(__cil_tmp21);
1626 }
1627 bufferalloced:
1628 {
1629#line 389
1630 __cil_tmp22 = & cfag12864b_buffer;
1631#line 389
1632 __cil_tmp23 = *__cil_tmp22;
1633#line 389
1634 __cil_tmp24 = (unsigned long )__cil_tmp23;
1635#line 389
1636 free_pages(__cil_tmp24, 0U);
1637 }
1638 none: ;
1639#line 392
1640 return (ret);
1641}
1642}
1643#line 395 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
1644static void cfag12864b_exit(void)
1645{ void const *__cil_tmp1 ;
1646 unsigned char **__cil_tmp2 ;
1647 unsigned char *__cil_tmp3 ;
1648 unsigned long __cil_tmp4 ;
1649
1650 {
1651 {
1652#line 397
1653 cfag12864b_disable();
1654#line 398
1655 cfag12864b_off();
1656#line 399
1657 destroy_workqueue(cfag12864b_workqueue);
1658#line 400
1659 __cil_tmp1 = (void const *)cfag12864b_cache;
1660#line 400
1661 kfree(__cil_tmp1);
1662#line 401
1663 __cil_tmp2 = & cfag12864b_buffer;
1664#line 401
1665 __cil_tmp3 = *__cil_tmp2;
1666#line 401
1667 __cil_tmp4 = (unsigned long )__cil_tmp3;
1668#line 401
1669 free_pages(__cil_tmp4, 0U);
1670 }
1671#line 402
1672 return;
1673}
1674}
1675#line 427
1676extern void ldv_check_final_state(void) ;
1677#line 433
1678extern void ldv_initialize(void) ;
1679#line 436
1680extern int __VERIFIER_nondet_int(void) ;
1681#line 439 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
1682int LDV_IN_INTERRUPT ;
1683#line 442 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
1684void main(void)
1685{ int tmp ;
1686 int tmp___0 ;
1687 int tmp___1 ;
1688
1689 {
1690 {
1691#line 454
1692 LDV_IN_INTERRUPT = 1;
1693#line 463
1694 ldv_initialize();
1695#line 476
1696 tmp = cfag12864b_init();
1697 }
1698#line 476
1699 if (tmp != 0) {
1700#line 477
1701 goto ldv_final;
1702 } else {
1703
1704 }
1705#line 479
1706 goto ldv_18885;
1707 ldv_18884:
1708 {
1709#line 482
1710 tmp___0 = __VERIFIER_nondet_int();
1711 }
1712 {
1713#line 484
1714 goto switch_default;
1715#line 482
1716 if (0) {
1717 switch_default: ;
1718#line 484
1719 goto ldv_18883;
1720 } else {
1721 switch_break: ;
1722 }
1723 }
1724 ldv_18883: ;
1725 ldv_18885:
1726 {
1727#line 479
1728 tmp___1 = __VERIFIER_nondet_int();
1729 }
1730#line 479
1731 if (tmp___1 != 0) {
1732#line 480
1733 goto ldv_18884;
1734 } else {
1735#line 482
1736 goto ldv_18886;
1737 }
1738 ldv_18886: ;
1739 {
1740#line 503
1741 cfag12864b_exit();
1742 }
1743 ldv_final:
1744 {
1745#line 506
1746 ldv_check_final_state();
1747 }
1748#line 509
1749 return;
1750}
1751}
1752#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
1753void ldv_blast_assert(void)
1754{
1755
1756 {
1757 ERROR: ;
1758#line 6
1759 goto ERROR;
1760}
1761}
1762#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
1763extern int __VERIFIER_nondet_int(void) ;
1764#line 530 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
1765int ldv_spin = 0;
1766#line 534 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
1767void ldv_check_alloc_flags(gfp_t flags )
1768{
1769
1770 {
1771#line 537
1772 if (ldv_spin != 0) {
1773#line 537
1774 if (flags != 32U) {
1775 {
1776#line 537
1777 ldv_blast_assert();
1778 }
1779 } else {
1780
1781 }
1782 } else {
1783
1784 }
1785#line 540
1786 return;
1787}
1788}
1789#line 540
1790extern struct page *ldv_some_page(void) ;
1791#line 543 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
1792struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags )
1793{ struct page *tmp ;
1794
1795 {
1796#line 546
1797 if (ldv_spin != 0) {
1798#line 546
1799 if (flags != 32U) {
1800 {
1801#line 546
1802 ldv_blast_assert();
1803 }
1804 } else {
1805
1806 }
1807 } else {
1808
1809 }
1810 {
1811#line 548
1812 tmp = ldv_some_page();
1813 }
1814#line 548
1815 return (tmp);
1816}
1817}
1818#line 552 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
1819void ldv_check_alloc_nonatomic(void)
1820{
1821
1822 {
1823#line 555
1824 if (ldv_spin != 0) {
1825 {
1826#line 555
1827 ldv_blast_assert();
1828 }
1829 } else {
1830
1831 }
1832#line 558
1833 return;
1834}
1835}
1836#line 559 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
1837void ldv_spin_lock(void)
1838{
1839
1840 {
1841#line 562
1842 ldv_spin = 1;
1843#line 563
1844 return;
1845}
1846}
1847#line 566 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
1848void ldv_spin_unlock(void)
1849{
1850
1851 {
1852#line 569
1853 ldv_spin = 0;
1854#line 570
1855 return;
1856}
1857}
1858#line 573 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
1859int ldv_spin_trylock(void)
1860{ int is_lock ;
1861
1862 {
1863 {
1864#line 578
1865 is_lock = __VERIFIER_nondet_int();
1866 }
1867#line 580
1868 if (is_lock != 0) {
1869#line 583
1870 return (0);
1871 } else {
1872#line 588
1873 ldv_spin = 1;
1874#line 590
1875 return (1);
1876 }
1877}
1878}
1879#line 712 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
1880__inline static void *kmalloc(size_t size , gfp_t flags )
1881{
1882
1883 {
1884 {
1885#line 718
1886 ldv_check_alloc_flags(flags);
1887#line 720
1888 ldv_kmalloc_12(size, flags);
1889 }
1890#line 721
1891 return ((void *)0);
1892}
1893}
1894#line 757 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17287/dscv_tempdir/dscv/ri/43_1a/drivers/auxdisplay/cfag12864b.c.p"
1895void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 )
1896{
1897
1898 {
1899 {
1900#line 763
1901 ldv_check_alloc_flags(ldv_func_arg2);
1902#line 765
1903 kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
1904 }
1905#line 766
1906 return ((void *)0);
1907}
1908}