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