1
2
3
4#line 20 "include/asm-generic/int-ll64.h"
5typedef unsigned char __u8;
6#line 23 "include/asm-generic/int-ll64.h"
7typedef unsigned short __u16;
8#line 26 "include/asm-generic/int-ll64.h"
9typedef unsigned int __u32;
10#line 30 "include/asm-generic/int-ll64.h"
11typedef unsigned long long __u64;
12#line 43 "include/asm-generic/int-ll64.h"
13typedef unsigned char u8;
14#line 45 "include/asm-generic/int-ll64.h"
15typedef short s16;
16#line 46 "include/asm-generic/int-ll64.h"
17typedef unsigned short u16;
18#line 49 "include/asm-generic/int-ll64.h"
19typedef unsigned int u32;
20#line 14 "include/asm-generic/posix_types.h"
21typedef long __kernel_long_t;
22#line 15 "include/asm-generic/posix_types.h"
23typedef unsigned long __kernel_ulong_t;
24#line 75 "include/asm-generic/posix_types.h"
25typedef __kernel_ulong_t __kernel_size_t;
26#line 76 "include/asm-generic/posix_types.h"
27typedef __kernel_long_t __kernel_ssize_t;
28#line 27 "include/linux/types.h"
29typedef unsigned short umode_t;
30#line 63 "include/linux/types.h"
31typedef __kernel_size_t size_t;
32#line 68 "include/linux/types.h"
33typedef __kernel_ssize_t ssize_t;
34#line 202 "include/linux/types.h"
35typedef unsigned int gfp_t;
36#line 221 "include/linux/types.h"
37struct __anonstruct_atomic_t_6 {
38 int counter ;
39};
40#line 221 "include/linux/types.h"
41typedef struct __anonstruct_atomic_t_6 atomic_t;
42#line 226 "include/linux/types.h"
43struct __anonstruct_atomic64_t_7 {
44 long counter ;
45};
46#line 226 "include/linux/types.h"
47typedef struct __anonstruct_atomic64_t_7 atomic64_t;
48#line 227 "include/linux/types.h"
49struct list_head {
50 struct list_head *next ;
51 struct list_head *prev ;
52};
53#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
54struct module;
55#line 55
56struct module;
57#line 146 "include/linux/init.h"
58typedef void (*ctor_fn_t)(void);
59#line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
60struct page;
61#line 58
62struct page;
63#line 26 "include/asm-generic/getorder.h"
64struct task_struct;
65#line 26
66struct task_struct;
67#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
68struct arch_spinlock;
69#line 327
70struct arch_spinlock;
71#line 306 "include/linux/bitmap.h"
72struct bug_entry {
73 int bug_addr_disp ;
74 int file_disp ;
75 unsigned short line ;
76 unsigned short flags ;
77};
78#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
79struct static_key;
80#line 234
81struct static_key;
82#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
83struct kmem_cache;
84#line 23 "include/asm-generic/atomic-long.h"
85typedef atomic64_t atomic_long_t;
86#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
87typedef u16 __ticket_t;
88#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
89typedef u32 __ticketpair_t;
90#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
91struct __raw_tickets {
92 __ticket_t head ;
93 __ticket_t tail ;
94};
95#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
96union __anonunion_ldv_5907_29 {
97 __ticketpair_t head_tail ;
98 struct __raw_tickets tickets ;
99};
100#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
101struct arch_spinlock {
102 union __anonunion_ldv_5907_29 ldv_5907 ;
103};
104#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
105typedef struct arch_spinlock arch_spinlock_t;
106#line 34 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
107struct lockdep_map;
108#line 34
109struct lockdep_map;
110#line 55 "include/linux/debug_locks.h"
111struct stack_trace {
112 unsigned int nr_entries ;
113 unsigned int max_entries ;
114 unsigned long *entries ;
115 int skip ;
116};
117#line 26 "include/linux/stacktrace.h"
118struct lockdep_subclass_key {
119 char __one_byte ;
120};
121#line 53 "include/linux/lockdep.h"
122struct lock_class_key {
123 struct lockdep_subclass_key subkeys[8U] ;
124};
125#line 59 "include/linux/lockdep.h"
126struct lock_class {
127 struct list_head hash_entry ;
128 struct list_head lock_entry ;
129 struct lockdep_subclass_key *key ;
130 unsigned int subclass ;
131 unsigned int dep_gen_id ;
132 unsigned long usage_mask ;
133 struct stack_trace usage_traces[13U] ;
134 struct list_head locks_after ;
135 struct list_head locks_before ;
136 unsigned int version ;
137 unsigned long ops ;
138 char const *name ;
139 int name_version ;
140 unsigned long contention_point[4U] ;
141 unsigned long contending_point[4U] ;
142};
143#line 144 "include/linux/lockdep.h"
144struct lockdep_map {
145 struct lock_class_key *key ;
146 struct lock_class *class_cache[2U] ;
147 char const *name ;
148 int cpu ;
149 unsigned long ip ;
150};
151#line 556 "include/linux/lockdep.h"
152struct raw_spinlock {
153 arch_spinlock_t raw_lock ;
154 unsigned int magic ;
155 unsigned int owner_cpu ;
156 void *owner ;
157 struct lockdep_map dep_map ;
158};
159#line 33 "include/linux/spinlock_types.h"
160struct __anonstruct_ldv_6122_33 {
161 u8 __padding[24U] ;
162 struct lockdep_map dep_map ;
163};
164#line 33 "include/linux/spinlock_types.h"
165union __anonunion_ldv_6123_32 {
166 struct raw_spinlock rlock ;
167 struct __anonstruct_ldv_6122_33 ldv_6122 ;
168};
169#line 33 "include/linux/spinlock_types.h"
170struct spinlock {
171 union __anonunion_ldv_6123_32 ldv_6123 ;
172};
173#line 76 "include/linux/spinlock_types.h"
174typedef struct spinlock spinlock_t;
175#line 18 "include/linux/elf.h"
176typedef __u64 Elf64_Addr;
177#line 19 "include/linux/elf.h"
178typedef __u16 Elf64_Half;
179#line 23 "include/linux/elf.h"
180typedef __u32 Elf64_Word;
181#line 24 "include/linux/elf.h"
182typedef __u64 Elf64_Xword;
183#line 193 "include/linux/elf.h"
184struct elf64_sym {
185 Elf64_Word st_name ;
186 unsigned char st_info ;
187 unsigned char st_other ;
188 Elf64_Half st_shndx ;
189 Elf64_Addr st_value ;
190 Elf64_Xword st_size ;
191};
192#line 201 "include/linux/elf.h"
193typedef struct elf64_sym Elf64_Sym;
194#line 445
195struct sock;
196#line 445
197struct sock;
198#line 446
199struct kobject;
200#line 446
201struct kobject;
202#line 447
203enum kobj_ns_type {
204 KOBJ_NS_TYPE_NONE = 0,
205 KOBJ_NS_TYPE_NET = 1,
206 KOBJ_NS_TYPES = 2
207} ;
208#line 453 "include/linux/elf.h"
209struct kobj_ns_type_operations {
210 enum kobj_ns_type type ;
211 void *(*grab_current_ns)(void) ;
212 void const *(*netlink_ns)(struct sock * ) ;
213 void const *(*initial_ns)(void) ;
214 void (*drop_ns)(void * ) ;
215};
216#line 57 "include/linux/kobject_ns.h"
217struct attribute {
218 char const *name ;
219 umode_t mode ;
220 struct lock_class_key *key ;
221 struct lock_class_key skey ;
222};
223#line 98 "include/linux/sysfs.h"
224struct sysfs_ops {
225 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
226 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
227 void const *(*namespace)(struct kobject * , struct attribute const * ) ;
228};
229#line 117
230struct sysfs_dirent;
231#line 117
232struct sysfs_dirent;
233#line 182 "include/linux/sysfs.h"
234struct kref {
235 atomic_t refcount ;
236};
237#line 49 "include/linux/kobject.h"
238struct kset;
239#line 49
240struct kobj_type;
241#line 49 "include/linux/kobject.h"
242struct kobject {
243 char const *name ;
244 struct list_head entry ;
245 struct kobject *parent ;
246 struct kset *kset ;
247 struct kobj_type *ktype ;
248 struct sysfs_dirent *sd ;
249 struct kref kref ;
250 unsigned char state_initialized : 1 ;
251 unsigned char state_in_sysfs : 1 ;
252 unsigned char state_add_uevent_sent : 1 ;
253 unsigned char state_remove_uevent_sent : 1 ;
254 unsigned char uevent_suppress : 1 ;
255};
256#line 107 "include/linux/kobject.h"
257struct kobj_type {
258 void (*release)(struct kobject * ) ;
259 struct sysfs_ops const *sysfs_ops ;
260 struct attribute **default_attrs ;
261 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject * ) ;
262 void const *(*namespace)(struct kobject * ) ;
263};
264#line 115 "include/linux/kobject.h"
265struct kobj_uevent_env {
266 char *envp[32U] ;
267 int envp_idx ;
268 char buf[2048U] ;
269 int buflen ;
270};
271#line 122 "include/linux/kobject.h"
272struct kset_uevent_ops {
273 int (* const filter)(struct kset * , struct kobject * ) ;
274 char const *(* const name)(struct kset * , struct kobject * ) ;
275 int (* const uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
276};
277#line 139 "include/linux/kobject.h"
278struct kset {
279 struct list_head list ;
280 spinlock_t list_lock ;
281 struct kobject kobj ;
282 struct kset_uevent_ops const *uevent_ops ;
283};
284#line 215
285struct kernel_param;
286#line 215
287struct kernel_param;
288#line 216 "include/linux/kobject.h"
289struct kernel_param_ops {
290 int (*set)(char const * , struct kernel_param const * ) ;
291 int (*get)(char * , struct kernel_param const * ) ;
292 void (*free)(void * ) ;
293};
294#line 49 "include/linux/moduleparam.h"
295struct kparam_string;
296#line 49
297struct kparam_array;
298#line 49 "include/linux/moduleparam.h"
299union __anonunion_ldv_13371_134 {
300 void *arg ;
301 struct kparam_string const *str ;
302 struct kparam_array const *arr ;
303};
304#line 49 "include/linux/moduleparam.h"
305struct kernel_param {
306 char const *name ;
307 struct kernel_param_ops const *ops ;
308 u16 perm ;
309 s16 level ;
310 union __anonunion_ldv_13371_134 ldv_13371 ;
311};
312#line 61 "include/linux/moduleparam.h"
313struct kparam_string {
314 unsigned int maxlen ;
315 char *string ;
316};
317#line 67 "include/linux/moduleparam.h"
318struct kparam_array {
319 unsigned int max ;
320 unsigned int elemsize ;
321 unsigned int *num ;
322 struct kernel_param_ops const *ops ;
323 void *elem ;
324};
325#line 458 "include/linux/moduleparam.h"
326struct static_key {
327 atomic_t enabled ;
328};
329#line 225 "include/linux/jump_label.h"
330struct tracepoint;
331#line 225
332struct tracepoint;
333#line 226 "include/linux/jump_label.h"
334struct tracepoint_func {
335 void *func ;
336 void *data ;
337};
338#line 29 "include/linux/tracepoint.h"
339struct tracepoint {
340 char const *name ;
341 struct static_key key ;
342 void (*regfunc)(void) ;
343 void (*unregfunc)(void) ;
344 struct tracepoint_func *funcs ;
345};
346#line 86 "include/linux/tracepoint.h"
347struct kernel_symbol {
348 unsigned long value ;
349 char const *name ;
350};
351#line 27 "include/linux/export.h"
352struct mod_arch_specific {
353
354};
355#line 34 "include/linux/module.h"
356struct module_param_attrs;
357#line 34 "include/linux/module.h"
358struct module_kobject {
359 struct kobject kobj ;
360 struct module *mod ;
361 struct kobject *drivers_dir ;
362 struct module_param_attrs *mp ;
363};
364#line 43 "include/linux/module.h"
365struct module_attribute {
366 struct attribute attr ;
367 ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
368 ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const * ,
369 size_t ) ;
370 void (*setup)(struct module * , char const * ) ;
371 int (*test)(struct module * ) ;
372 void (*free)(struct module * ) ;
373};
374#line 69
375struct exception_table_entry;
376#line 69
377struct exception_table_entry;
378#line 198
379enum module_state {
380 MODULE_STATE_LIVE = 0,
381 MODULE_STATE_COMING = 1,
382 MODULE_STATE_GOING = 2
383} ;
384#line 204 "include/linux/module.h"
385struct module_ref {
386 unsigned long incs ;
387 unsigned long decs ;
388};
389#line 219
390struct module_sect_attrs;
391#line 219
392struct module_notes_attrs;
393#line 219
394struct ftrace_event_call;
395#line 219 "include/linux/module.h"
396struct module {
397 enum module_state state ;
398 struct list_head list ;
399 char name[56U] ;
400 struct module_kobject mkobj ;
401 struct module_attribute *modinfo_attrs ;
402 char const *version ;
403 char const *srcversion ;
404 struct kobject *holders_dir ;
405 struct kernel_symbol const *syms ;
406 unsigned long const *crcs ;
407 unsigned int num_syms ;
408 struct kernel_param *kp ;
409 unsigned int num_kp ;
410 unsigned int num_gpl_syms ;
411 struct kernel_symbol const *gpl_syms ;
412 unsigned long const *gpl_crcs ;
413 struct kernel_symbol const *unused_syms ;
414 unsigned long const *unused_crcs ;
415 unsigned int num_unused_syms ;
416 unsigned int num_unused_gpl_syms ;
417 struct kernel_symbol const *unused_gpl_syms ;
418 unsigned long const *unused_gpl_crcs ;
419 struct kernel_symbol const *gpl_future_syms ;
420 unsigned long const *gpl_future_crcs ;
421 unsigned int num_gpl_future_syms ;
422 unsigned int num_exentries ;
423 struct exception_table_entry *extable ;
424 int (*init)(void) ;
425 void *module_init ;
426 void *module_core ;
427 unsigned int init_size ;
428 unsigned int core_size ;
429 unsigned int init_text_size ;
430 unsigned int core_text_size ;
431 unsigned int init_ro_size ;
432 unsigned int core_ro_size ;
433 struct mod_arch_specific arch ;
434 unsigned int taints ;
435 unsigned int num_bugs ;
436 struct list_head bug_list ;
437 struct bug_entry *bug_table ;
438 Elf64_Sym *symtab ;
439 Elf64_Sym *core_symtab ;
440 unsigned int num_symtab ;
441 unsigned int core_num_syms ;
442 char *strtab ;
443 char *core_strtab ;
444 struct module_sect_attrs *sect_attrs ;
445 struct module_notes_attrs *notes_attrs ;
446 char *args ;
447 void *percpu ;
448 unsigned int percpu_size ;
449 unsigned int num_tracepoints ;
450 struct tracepoint * const *tracepoints_ptrs ;
451 unsigned int num_trace_bprintk_fmt ;
452 char const **trace_bprintk_fmt_start ;
453 struct ftrace_event_call **trace_events ;
454 unsigned int num_trace_events ;
455 struct list_head source_list ;
456 struct list_head target_list ;
457 struct task_struct *waiter ;
458 void (*exit)(void) ;
459 struct module_ref *refptr ;
460 ctor_fn_t (**ctors)(void) ;
461 unsigned int num_ctors ;
462};
463#line 88 "include/linux/kmemleak.h"
464struct kmem_cache_cpu {
465 void **freelist ;
466 unsigned long tid ;
467 struct page *page ;
468 struct page *partial ;
469 int node ;
470 unsigned int stat[26U] ;
471};
472#line 55 "include/linux/slub_def.h"
473struct kmem_cache_node {
474 spinlock_t list_lock ;
475 unsigned long nr_partial ;
476 struct list_head partial ;
477 atomic_long_t nr_slabs ;
478 atomic_long_t total_objects ;
479 struct list_head full ;
480};
481#line 66 "include/linux/slub_def.h"
482struct kmem_cache_order_objects {
483 unsigned long x ;
484};
485#line 76 "include/linux/slub_def.h"
486struct kmem_cache {
487 struct kmem_cache_cpu *cpu_slab ;
488 unsigned long flags ;
489 unsigned long min_partial ;
490 int size ;
491 int objsize ;
492 int offset ;
493 int cpu_partial ;
494 struct kmem_cache_order_objects oo ;
495 struct kmem_cache_order_objects max ;
496 struct kmem_cache_order_objects min ;
497 gfp_t allocflags ;
498 int refcount ;
499 void (*ctor)(void * ) ;
500 int inuse ;
501 int align ;
502 int reserved ;
503 char const *name ;
504 struct list_head list ;
505 struct kobject kobj ;
506 int remote_node_defrag_ratio ;
507 struct kmem_cache_node *node[1024U] ;
508};
509#line 119 "include/linux/ppp_defs.h"
510struct compstat {
511 __u32 unc_bytes ;
512 __u32 unc_packets ;
513 __u32 comp_bytes ;
514 __u32 comp_packets ;
515 __u32 inc_bytes ;
516 __u32 inc_packets ;
517 __u32 in_count ;
518 __u32 bytes_out ;
519 double ratio ;
520};
521#line 153 "include/linux/ppp_defs.h"
522struct compressor {
523 int compress_proto ;
524 void *(*comp_alloc)(unsigned char * , int ) ;
525 void (*comp_free)(void * ) ;
526 int (*comp_init)(void * , unsigned char * , int , int , int , int ) ;
527 void (*comp_reset)(void * ) ;
528 int (*compress)(void * , unsigned char * , unsigned char * , int , int ) ;
529 void (*comp_stat)(void * , struct compstat * ) ;
530 void *(*decomp_alloc)(unsigned char * , int ) ;
531 void (*decomp_free)(void * ) ;
532 int (*decomp_init)(void * , unsigned char * , int , int , int , int , int ) ;
533 void (*decomp_reset)(void * ) ;
534 int (*decompress)(void * , unsigned char * , int , unsigned char * , int ) ;
535 void (*incomp)(void * , unsigned char * , int ) ;
536 void (*decomp_stat)(void * , struct compstat * ) ;
537 struct module *owner ;
538 unsigned int comp_extra ;
539};
540#line 182 "include/linux/ppp-comp.h"
541struct __anonstruct_hs_136 {
542 unsigned short prefix ;
543 unsigned char suffix ;
544 unsigned char pad ;
545};
546#line 182 "include/linux/ppp-comp.h"
547union __anonunion_f_135 {
548 unsigned long fcode ;
549 struct __anonstruct_hs_136 hs ;
550};
551#line 182 "include/linux/ppp-comp.h"
552struct bsd_dict {
553 union __anonunion_f_135 f ;
554 unsigned short codem1 ;
555 unsigned short cptr ;
556};
557#line 150 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
558struct bsd_db {
559 int totlen ;
560 unsigned int hsize ;
561 unsigned char hshift ;
562 unsigned char n_bits ;
563 unsigned char maxbits ;
564 unsigned char debug ;
565 unsigned char unit ;
566 unsigned short seqno ;
567 unsigned int mru ;
568 unsigned int maxmaxcode ;
569 unsigned int max_ent ;
570 unsigned int in_count ;
571 unsigned int bytes_out ;
572 unsigned int ratio ;
573 unsigned int checkpoint ;
574 unsigned int clear_count ;
575 unsigned int incomp_count ;
576 unsigned int incomp_bytes ;
577 unsigned int uncomp_count ;
578 unsigned int uncomp_bytes ;
579 unsigned int comp_count ;
580 unsigned int comp_bytes ;
581 unsigned short *lens ;
582 struct bsd_dict *dict ;
583};
584#line 2
585void ldv_spin_lock(void) ;
586#line 3
587void ldv_spin_unlock(void) ;
588#line 4
589int ldv_spin_trylock(void) ;
590#line 101 "include/linux/printk.h"
591extern int printk(char const * , ...) ;
592#line 54 "include/linux/vmalloc.h"
593extern void *vmalloc(unsigned long ) ;
594#line 57
595void *ldv_vmalloc_19(unsigned long ldv_func_arg1 ) ;
596#line 61
597void *ldv_vmalloc_20(unsigned long ldv_func_arg1 ) ;
598#line 74
599extern void vfree(void const * ) ;
600#line 26 "include/linux/export.h"
601extern struct module __this_module ;
602#line 161 "include/linux/slab.h"
603extern void kfree(void const * ) ;
604#line 220 "include/linux/slub_def.h"
605extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t ) ;
606#line 223
607void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
608#line 353 "include/linux/slab.h"
609__inline static void *kzalloc(size_t size , gfp_t flags ) ;
610#line 10 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
611extern void *__VERIFIER_nondet_pointer(void) ;
612#line 11
613void ldv_check_alloc_flags(gfp_t flags ) ;
614#line 12
615void ldv_check_alloc_nonatomic(void) ;
616#line 14
617struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
618#line 180 "include/linux/ppp-comp.h"
619extern int ppp_register_compressor(struct compressor * ) ;
620#line 181
621extern void ppp_unregister_compressor(struct compressor * ) ;
622#line 183 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
623static void bsd_free(void *state ) ;
624#line 184
625static void *bsd_alloc(unsigned char *options , int opt_len , int decomp ) ;
626#line 185
627static void *bsd_comp_alloc(unsigned char *options , int opt_len ) ;
628#line 186
629static void *bsd_decomp_alloc(unsigned char *options , int opt_len ) ;
630#line 188
631static int bsd_init(void *state , unsigned char *options , int opt_len , int unit ,
632 int debug , int decomp ) ;
633#line 190
634static int bsd_comp_init(void *state , unsigned char *options , int opt_len , int unit ,
635 int opthdr , int debug ) ;
636#line 192
637static int bsd_decomp_init(void *state , unsigned char *options , int opt_len , int unit ,
638 int opthdr , int mru , int debug ) ;
639#line 196
640static void bsd_reset(void *state ) ;
641#line 197
642static void bsd_comp_stats(void *state , struct compstat *stats ) ;
643#line 199
644static int bsd_compress(void *state , unsigned char *rptr , unsigned char *obuf ,
645 int isize , int osize ) ;
646#line 201
647static void bsd_incomp(void *state , unsigned char *ibuf , int icnt ) ;
648#line 203
649static int bsd_decompress(void *state , unsigned char *ibuf , int isize , unsigned char *obuf ,
650 int osize ) ;
651#line 237 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
652static void bsd_clear(struct bsd_db *db )
653{ unsigned long __cil_tmp2 ;
654 unsigned long __cil_tmp3 ;
655 unsigned long __cil_tmp4 ;
656 unsigned long __cil_tmp5 ;
657 unsigned int __cil_tmp6 ;
658 unsigned long __cil_tmp7 ;
659 unsigned long __cil_tmp8 ;
660 unsigned long __cil_tmp9 ;
661 unsigned long __cil_tmp10 ;
662 unsigned long __cil_tmp11 ;
663 unsigned long __cil_tmp12 ;
664 unsigned long __cil_tmp13 ;
665 unsigned long __cil_tmp14 ;
666 unsigned long __cil_tmp15 ;
667 unsigned long __cil_tmp16 ;
668 unsigned long __cil_tmp17 ;
669 unsigned long __cil_tmp18 ;
670
671 {
672#line 239
673 __cil_tmp2 = (unsigned long )db;
674#line 239
675 __cil_tmp3 = __cil_tmp2 + 44;
676#line 239
677 __cil_tmp4 = (unsigned long )db;
678#line 239
679 __cil_tmp5 = __cil_tmp4 + 44;
680#line 239
681 __cil_tmp6 = *((unsigned int *)__cil_tmp5);
682#line 239
683 *((unsigned int *)__cil_tmp3) = __cil_tmp6 + 1U;
684#line 240
685 __cil_tmp7 = (unsigned long )db;
686#line 240
687 __cil_tmp8 = __cil_tmp7 + 24;
688#line 240
689 *((unsigned int *)__cil_tmp8) = 256U;
690#line 241
691 __cil_tmp9 = (unsigned long )db;
692#line 241
693 __cil_tmp10 = __cil_tmp9 + 9;
694#line 241
695 *((unsigned char *)__cil_tmp10) = (unsigned char)9;
696#line 242
697 __cil_tmp11 = (unsigned long )db;
698#line 242
699 __cil_tmp12 = __cil_tmp11 + 32;
700#line 242
701 *((unsigned int *)__cil_tmp12) = 0U;
702#line 243
703 __cil_tmp13 = (unsigned long )db;
704#line 243
705 __cil_tmp14 = __cil_tmp13 + 28;
706#line 243
707 *((unsigned int *)__cil_tmp14) = 0U;
708#line 244
709 __cil_tmp15 = (unsigned long )db;
710#line 244
711 __cil_tmp16 = __cil_tmp15 + 36;
712#line 244
713 *((unsigned int *)__cil_tmp16) = 0U;
714#line 245
715 __cil_tmp17 = (unsigned long )db;
716#line 245
717 __cil_tmp18 = __cil_tmp17 + 40;
718#line 245
719 *((unsigned int *)__cil_tmp18) = 10000U;
720#line 246
721 return;
722}
723}
724#line 262 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
725static int bsd_check(struct bsd_db *db )
726{ unsigned int new_ratio ;
727 unsigned long __cil_tmp3 ;
728 unsigned long __cil_tmp4 ;
729 unsigned int __cil_tmp5 ;
730 unsigned long __cil_tmp6 ;
731 unsigned long __cil_tmp7 ;
732 unsigned int __cil_tmp8 ;
733 unsigned long __cil_tmp9 ;
734 unsigned long __cil_tmp10 ;
735 unsigned int __cil_tmp11 ;
736 unsigned long __cil_tmp12 ;
737 unsigned long __cil_tmp13 ;
738 unsigned long __cil_tmp14 ;
739 unsigned long __cil_tmp15 ;
740 unsigned int __cil_tmp16 ;
741 unsigned int __cil_tmp17 ;
742 unsigned long __cil_tmp18 ;
743 unsigned long __cil_tmp19 ;
744 unsigned int __cil_tmp20 ;
745 unsigned long __cil_tmp21 ;
746 unsigned long __cil_tmp22 ;
747 unsigned long __cil_tmp23 ;
748 unsigned long __cil_tmp24 ;
749 unsigned int __cil_tmp25 ;
750 unsigned int __cil_tmp26 ;
751 unsigned long __cil_tmp27 ;
752 unsigned long __cil_tmp28 ;
753 unsigned int __cil_tmp29 ;
754 unsigned long __cil_tmp30 ;
755 unsigned long __cil_tmp31 ;
756 unsigned int __cil_tmp32 ;
757 unsigned long __cil_tmp33 ;
758 unsigned long __cil_tmp34 ;
759 unsigned long __cil_tmp35 ;
760 unsigned long __cil_tmp36 ;
761 unsigned int __cil_tmp37 ;
762 unsigned int __cil_tmp38 ;
763 unsigned long __cil_tmp39 ;
764 unsigned long __cil_tmp40 ;
765 unsigned int __cil_tmp41 ;
766 unsigned long __cil_tmp42 ;
767 unsigned long __cil_tmp43 ;
768 unsigned long __cil_tmp44 ;
769 unsigned long __cil_tmp45 ;
770 unsigned int __cil_tmp46 ;
771 unsigned int __cil_tmp47 ;
772 unsigned long __cil_tmp48 ;
773 unsigned long __cil_tmp49 ;
774 unsigned int __cil_tmp50 ;
775 unsigned long __cil_tmp51 ;
776 unsigned long __cil_tmp52 ;
777 unsigned long __cil_tmp53 ;
778 unsigned long __cil_tmp54 ;
779 unsigned int __cil_tmp55 ;
780 unsigned long __cil_tmp56 ;
781 unsigned long __cil_tmp57 ;
782 unsigned int __cil_tmp58 ;
783 unsigned long __cil_tmp59 ;
784 unsigned long __cil_tmp60 ;
785 unsigned int __cil_tmp61 ;
786 unsigned long __cil_tmp62 ;
787 unsigned long __cil_tmp63 ;
788 unsigned int __cil_tmp64 ;
789 unsigned long __cil_tmp65 ;
790 unsigned long __cil_tmp66 ;
791 unsigned int __cil_tmp67 ;
792 unsigned long __cil_tmp68 ;
793 unsigned long __cil_tmp69 ;
794 unsigned int __cil_tmp70 ;
795 unsigned long __cil_tmp71 ;
796 unsigned long __cil_tmp72 ;
797 unsigned int __cil_tmp73 ;
798 unsigned long __cil_tmp74 ;
799 unsigned long __cil_tmp75 ;
800
801 {
802 {
803#line 266
804 __cil_tmp3 = (unsigned long )db;
805#line 266
806 __cil_tmp4 = __cil_tmp3 + 40;
807#line 266
808 __cil_tmp5 = *((unsigned int *)__cil_tmp4);
809#line 266
810 __cil_tmp6 = (unsigned long )db;
811#line 266
812 __cil_tmp7 = __cil_tmp6 + 28;
813#line 266
814 __cil_tmp8 = *((unsigned int *)__cil_tmp7);
815#line 266
816 if (__cil_tmp8 >= __cil_tmp5) {
817 {
818#line 269
819 __cil_tmp9 = (unsigned long )db;
820#line 269
821 __cil_tmp10 = __cil_tmp9 + 28;
822#line 269
823 __cil_tmp11 = *((unsigned int *)__cil_tmp10);
824#line 269
825 if (__cil_tmp11 > 8388606U) {
826#line 271
827 __cil_tmp12 = (unsigned long )db;
828#line 271
829 __cil_tmp13 = __cil_tmp12 + 28;
830#line 271
831 __cil_tmp14 = (unsigned long )db;
832#line 271
833 __cil_tmp15 = __cil_tmp14 + 28;
834#line 271
835 __cil_tmp16 = *((unsigned int *)__cil_tmp15);
836#line 271
837 __cil_tmp17 = __cil_tmp16 >> 2;
838#line 271
839 __cil_tmp18 = (unsigned long )db;
840#line 271
841 __cil_tmp19 = __cil_tmp18 + 28;
842#line 271
843 __cil_tmp20 = *((unsigned int *)__cil_tmp19);
844#line 271
845 *((unsigned int *)__cil_tmp13) = __cil_tmp20 - __cil_tmp17;
846#line 272
847 __cil_tmp21 = (unsigned long )db;
848#line 272
849 __cil_tmp22 = __cil_tmp21 + 32;
850#line 272
851 __cil_tmp23 = (unsigned long )db;
852#line 272
853 __cil_tmp24 = __cil_tmp23 + 32;
854#line 272
855 __cil_tmp25 = *((unsigned int *)__cil_tmp24);
856#line 272
857 __cil_tmp26 = __cil_tmp25 >> 2;
858#line 272
859 __cil_tmp27 = (unsigned long )db;
860#line 272
861 __cil_tmp28 = __cil_tmp27 + 32;
862#line 272
863 __cil_tmp29 = *((unsigned int *)__cil_tmp28);
864#line 272
865 *((unsigned int *)__cil_tmp22) = __cil_tmp29 - __cil_tmp26;
866 } else {
867 {
868#line 269
869 __cil_tmp30 = (unsigned long )db;
870#line 269
871 __cil_tmp31 = __cil_tmp30 + 32;
872#line 269
873 __cil_tmp32 = *((unsigned int *)__cil_tmp31);
874#line 269
875 if (__cil_tmp32 > 8388606U) {
876#line 271
877 __cil_tmp33 = (unsigned long )db;
878#line 271
879 __cil_tmp34 = __cil_tmp33 + 28;
880#line 271
881 __cil_tmp35 = (unsigned long )db;
882#line 271
883 __cil_tmp36 = __cil_tmp35 + 28;
884#line 271
885 __cil_tmp37 = *((unsigned int *)__cil_tmp36);
886#line 271
887 __cil_tmp38 = __cil_tmp37 >> 2;
888#line 271
889 __cil_tmp39 = (unsigned long )db;
890#line 271
891 __cil_tmp40 = __cil_tmp39 + 28;
892#line 271
893 __cil_tmp41 = *((unsigned int *)__cil_tmp40);
894#line 271
895 *((unsigned int *)__cil_tmp34) = __cil_tmp41 - __cil_tmp38;
896#line 272
897 __cil_tmp42 = (unsigned long )db;
898#line 272
899 __cil_tmp43 = __cil_tmp42 + 32;
900#line 272
901 __cil_tmp44 = (unsigned long )db;
902#line 272
903 __cil_tmp45 = __cil_tmp44 + 32;
904#line 272
905 __cil_tmp46 = *((unsigned int *)__cil_tmp45);
906#line 272
907 __cil_tmp47 = __cil_tmp46 >> 2;
908#line 272
909 __cil_tmp48 = (unsigned long )db;
910#line 272
911 __cil_tmp49 = __cil_tmp48 + 32;
912#line 272
913 __cil_tmp50 = *((unsigned int *)__cil_tmp49);
914#line 272
915 *((unsigned int *)__cil_tmp43) = __cil_tmp50 - __cil_tmp47;
916 } else {
917
918 }
919 }
920 }
921 }
922#line 275
923 __cil_tmp51 = (unsigned long )db;
924#line 275
925 __cil_tmp52 = __cil_tmp51 + 40;
926#line 275
927 __cil_tmp53 = (unsigned long )db;
928#line 275
929 __cil_tmp54 = __cil_tmp53 + 28;
930#line 275
931 __cil_tmp55 = *((unsigned int *)__cil_tmp54);
932#line 275
933 *((unsigned int *)__cil_tmp52) = __cil_tmp55 + 10000U;
934 {
935#line 277
936 __cil_tmp56 = (unsigned long )db;
937#line 277
938 __cil_tmp57 = __cil_tmp56 + 20;
939#line 277
940 __cil_tmp58 = *((unsigned int *)__cil_tmp57);
941#line 277
942 __cil_tmp59 = (unsigned long )db;
943#line 277
944 __cil_tmp60 = __cil_tmp59 + 24;
945#line 277
946 __cil_tmp61 = *((unsigned int *)__cil_tmp60);
947#line 277
948 if (__cil_tmp61 >= __cil_tmp58) {
949#line 287
950 __cil_tmp62 = (unsigned long )db;
951#line 287
952 __cil_tmp63 = __cil_tmp62 + 28;
953#line 287
954 __cil_tmp64 = *((unsigned int *)__cil_tmp63);
955#line 287
956 new_ratio = __cil_tmp64 << 8;
957 {
958#line 288
959 __cil_tmp65 = (unsigned long )db;
960#line 288
961 __cil_tmp66 = __cil_tmp65 + 32;
962#line 288
963 __cil_tmp67 = *((unsigned int *)__cil_tmp66);
964#line 288
965 if (__cil_tmp67 != 0U) {
966#line 290
967 __cil_tmp68 = (unsigned long )db;
968#line 290
969 __cil_tmp69 = __cil_tmp68 + 32;
970#line 290
971 __cil_tmp70 = *((unsigned int *)__cil_tmp69);
972#line 290
973 new_ratio = new_ratio / __cil_tmp70;
974 } else {
975
976 }
977 }
978 {
979#line 293
980 __cil_tmp71 = (unsigned long )db;
981#line 293
982 __cil_tmp72 = __cil_tmp71 + 36;
983#line 293
984 __cil_tmp73 = *((unsigned int *)__cil_tmp72);
985#line 293
986 if (__cil_tmp73 > new_ratio) {
987 {
988#line 295
989 bsd_clear(db);
990 }
991#line 296
992 return (1);
993 } else
994#line 293
995 if (new_ratio <= 255U) {
996 {
997#line 295
998 bsd_clear(db);
999 }
1000#line 296
1001 return (1);
1002 } else {
1003
1004 }
1005 }
1006#line 298
1007 __cil_tmp74 = (unsigned long )db;
1008#line 298
1009 __cil_tmp75 = __cil_tmp74 + 36;
1010#line 298
1011 *((unsigned int *)__cil_tmp75) = new_ratio;
1012 } else {
1013
1014 }
1015 }
1016 } else {
1017
1018 }
1019 }
1020#line 301
1021 return (0);
1022}
1023}
1024#line 308 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
1025static void bsd_comp_stats(void *state , struct compstat *stats )
1026{ struct bsd_db *db ;
1027 unsigned long __cil_tmp4 ;
1028 unsigned long __cil_tmp5 ;
1029 unsigned long __cil_tmp6 ;
1030 unsigned long __cil_tmp7 ;
1031 unsigned long __cil_tmp8 ;
1032 unsigned long __cil_tmp9 ;
1033 unsigned long __cil_tmp10 ;
1034 unsigned long __cil_tmp11 ;
1035 unsigned long __cil_tmp12 ;
1036 unsigned long __cil_tmp13 ;
1037 unsigned long __cil_tmp14 ;
1038 unsigned long __cil_tmp15 ;
1039 unsigned long __cil_tmp16 ;
1040 unsigned long __cil_tmp17 ;
1041 unsigned long __cil_tmp18 ;
1042 unsigned long __cil_tmp19 ;
1043 unsigned long __cil_tmp20 ;
1044 unsigned long __cil_tmp21 ;
1045 unsigned long __cil_tmp22 ;
1046 unsigned long __cil_tmp23 ;
1047 unsigned long __cil_tmp24 ;
1048 unsigned long __cil_tmp25 ;
1049 unsigned long __cil_tmp26 ;
1050 unsigned long __cil_tmp27 ;
1051 unsigned long __cil_tmp28 ;
1052 unsigned long __cil_tmp29 ;
1053 unsigned long __cil_tmp30 ;
1054 unsigned long __cil_tmp31 ;
1055 unsigned long __cil_tmp32 ;
1056 unsigned long __cil_tmp33 ;
1057
1058 {
1059#line 310
1060 db = (struct bsd_db *)state;
1061#line 312
1062 __cil_tmp4 = (unsigned long )db;
1063#line 312
1064 __cil_tmp5 = __cil_tmp4 + 60;
1065#line 312
1066 *((__u32 *)stats) = *((unsigned int *)__cil_tmp5);
1067#line 313
1068 __cil_tmp6 = (unsigned long )stats;
1069#line 313
1070 __cil_tmp7 = __cil_tmp6 + 4;
1071#line 313
1072 __cil_tmp8 = (unsigned long )db;
1073#line 313
1074 __cil_tmp9 = __cil_tmp8 + 56;
1075#line 313
1076 *((__u32 *)__cil_tmp7) = *((unsigned int *)__cil_tmp9);
1077#line 314
1078 __cil_tmp10 = (unsigned long )stats;
1079#line 314
1080 __cil_tmp11 = __cil_tmp10 + 8;
1081#line 314
1082 __cil_tmp12 = (unsigned long )db;
1083#line 314
1084 __cil_tmp13 = __cil_tmp12 + 68;
1085#line 314
1086 *((__u32 *)__cil_tmp11) = *((unsigned int *)__cil_tmp13);
1087#line 315
1088 __cil_tmp14 = (unsigned long )stats;
1089#line 315
1090 __cil_tmp15 = __cil_tmp14 + 12;
1091#line 315
1092 __cil_tmp16 = (unsigned long )db;
1093#line 315
1094 __cil_tmp17 = __cil_tmp16 + 64;
1095#line 315
1096 *((__u32 *)__cil_tmp15) = *((unsigned int *)__cil_tmp17);
1097#line 316
1098 __cil_tmp18 = (unsigned long )stats;
1099#line 316
1100 __cil_tmp19 = __cil_tmp18 + 16;
1101#line 316
1102 __cil_tmp20 = (unsigned long )db;
1103#line 316
1104 __cil_tmp21 = __cil_tmp20 + 52;
1105#line 316
1106 *((__u32 *)__cil_tmp19) = *((unsigned int *)__cil_tmp21);
1107#line 317
1108 __cil_tmp22 = (unsigned long )stats;
1109#line 317
1110 __cil_tmp23 = __cil_tmp22 + 20;
1111#line 317
1112 __cil_tmp24 = (unsigned long )db;
1113#line 317
1114 __cil_tmp25 = __cil_tmp24 + 48;
1115#line 317
1116 *((__u32 *)__cil_tmp23) = *((unsigned int *)__cil_tmp25);
1117#line 318
1118 __cil_tmp26 = (unsigned long )stats;
1119#line 318
1120 __cil_tmp27 = __cil_tmp26 + 24;
1121#line 318
1122 __cil_tmp28 = (unsigned long )db;
1123#line 318
1124 __cil_tmp29 = __cil_tmp28 + 28;
1125#line 318
1126 *((__u32 *)__cil_tmp27) = *((unsigned int *)__cil_tmp29);
1127#line 319
1128 __cil_tmp30 = (unsigned long )stats;
1129#line 319
1130 __cil_tmp31 = __cil_tmp30 + 28;
1131#line 319
1132 __cil_tmp32 = (unsigned long )db;
1133#line 319
1134 __cil_tmp33 = __cil_tmp32 + 32;
1135#line 319
1136 *((__u32 *)__cil_tmp31) = *((unsigned int *)__cil_tmp33);
1137#line 320
1138 return;
1139}
1140}
1141#line 326 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
1142static void bsd_reset(void *state )
1143{ struct bsd_db *db ;
1144 unsigned long __cil_tmp3 ;
1145 unsigned long __cil_tmp4 ;
1146 unsigned long __cil_tmp5 ;
1147 unsigned long __cil_tmp6 ;
1148
1149 {
1150 {
1151#line 328
1152 db = (struct bsd_db *)state;
1153#line 330
1154 bsd_clear(db);
1155#line 332
1156 __cil_tmp3 = (unsigned long )db;
1157#line 332
1158 __cil_tmp4 = __cil_tmp3 + 14;
1159#line 332
1160 *((unsigned short *)__cil_tmp4) = (unsigned short)0;
1161#line 333
1162 __cil_tmp5 = (unsigned long )db;
1163#line 333
1164 __cil_tmp6 = __cil_tmp5 + 44;
1165#line 333
1166 *((unsigned int *)__cil_tmp6) = 0U;
1167 }
1168#line 334
1169 return;
1170}
1171}
1172#line 340 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
1173static void bsd_free(void *state )
1174{ struct bsd_db *db ;
1175 struct bsd_db *__cil_tmp3 ;
1176 unsigned long __cil_tmp4 ;
1177 unsigned long __cil_tmp5 ;
1178 unsigned long __cil_tmp6 ;
1179 unsigned long __cil_tmp7 ;
1180 struct bsd_dict *__cil_tmp8 ;
1181 void const *__cil_tmp9 ;
1182 unsigned long __cil_tmp10 ;
1183 unsigned long __cil_tmp11 ;
1184 unsigned long __cil_tmp12 ;
1185 unsigned long __cil_tmp13 ;
1186 unsigned short *__cil_tmp14 ;
1187 void const *__cil_tmp15 ;
1188 unsigned long __cil_tmp16 ;
1189 unsigned long __cil_tmp17 ;
1190 void const *__cil_tmp18 ;
1191
1192 {
1193#line 342
1194 db = (struct bsd_db *)state;
1195 {
1196#line 344
1197 __cil_tmp3 = (struct bsd_db *)0;
1198#line 344
1199 __cil_tmp4 = (unsigned long )__cil_tmp3;
1200#line 344
1201 __cil_tmp5 = (unsigned long )db;
1202#line 344
1203 if (__cil_tmp5 == __cil_tmp4) {
1204#line 345
1205 return;
1206 } else {
1207
1208 }
1209 }
1210 {
1211#line 350
1212 __cil_tmp6 = (unsigned long )db;
1213#line 350
1214 __cil_tmp7 = __cil_tmp6 + 80;
1215#line 350
1216 __cil_tmp8 = *((struct bsd_dict **)__cil_tmp7);
1217#line 350
1218 __cil_tmp9 = (void const *)__cil_tmp8;
1219#line 350
1220 vfree(__cil_tmp9);
1221#line 351
1222 __cil_tmp10 = (unsigned long )db;
1223#line 351
1224 __cil_tmp11 = __cil_tmp10 + 80;
1225#line 351
1226 *((struct bsd_dict **)__cil_tmp11) = (struct bsd_dict *)0;
1227#line 355
1228 __cil_tmp12 = (unsigned long )db;
1229#line 355
1230 __cil_tmp13 = __cil_tmp12 + 72;
1231#line 355
1232 __cil_tmp14 = *((unsigned short **)__cil_tmp13);
1233#line 355
1234 __cil_tmp15 = (void const *)__cil_tmp14;
1235#line 355
1236 vfree(__cil_tmp15);
1237#line 356
1238 __cil_tmp16 = (unsigned long )db;
1239#line 356
1240 __cil_tmp17 = __cil_tmp16 + 72;
1241#line 356
1242 *((unsigned short **)__cil_tmp17) = (unsigned short *)0;
1243#line 360
1244 __cil_tmp18 = (void const *)db;
1245#line 360
1246 kfree(__cil_tmp18);
1247 }
1248#line 361
1249 return;
1250}
1251}
1252#line 367 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
1253static void *bsd_alloc(unsigned char *options , int opt_len , int decomp )
1254{ int bits ;
1255 unsigned int hsize ;
1256 unsigned int hshift ;
1257 unsigned int maxmaxcode ;
1258 struct bsd_db *db ;
1259 void *tmp ;
1260 void *tmp___0 ;
1261 void *tmp___1 ;
1262 unsigned char __cil_tmp12 ;
1263 unsigned int __cil_tmp13 ;
1264 unsigned char *__cil_tmp14 ;
1265 unsigned char __cil_tmp15 ;
1266 unsigned int __cil_tmp16 ;
1267 unsigned char *__cil_tmp17 ;
1268 unsigned char __cil_tmp18 ;
1269 int __cil_tmp19 ;
1270 int __cil_tmp20 ;
1271 unsigned int __cil_tmp21 ;
1272 unsigned char *__cil_tmp22 ;
1273 unsigned char __cil_tmp23 ;
1274 int __cil_tmp24 ;
1275 int __cil_tmp25 ;
1276 int __cil_tmp26 ;
1277 struct bsd_db *__cil_tmp27 ;
1278 unsigned long __cil_tmp28 ;
1279 unsigned long __cil_tmp29 ;
1280 unsigned long __cil_tmp30 ;
1281 unsigned long __cil_tmp31 ;
1282 unsigned long __cil_tmp32 ;
1283 unsigned long __cil_tmp33 ;
1284 struct bsd_dict *__cil_tmp34 ;
1285 unsigned long __cil_tmp35 ;
1286 unsigned long __cil_tmp36 ;
1287 unsigned long __cil_tmp37 ;
1288 struct bsd_dict *__cil_tmp38 ;
1289 unsigned long __cil_tmp39 ;
1290 void *__cil_tmp40 ;
1291 unsigned long __cil_tmp41 ;
1292 unsigned long __cil_tmp42 ;
1293 unsigned int __cil_tmp43 ;
1294 unsigned long __cil_tmp44 ;
1295 unsigned long __cil_tmp45 ;
1296 unsigned long __cil_tmp46 ;
1297 unsigned long __cil_tmp47 ;
1298 unsigned short *__cil_tmp48 ;
1299 unsigned long __cil_tmp49 ;
1300 unsigned long __cil_tmp50 ;
1301 unsigned long __cil_tmp51 ;
1302 unsigned short *__cil_tmp52 ;
1303 unsigned long __cil_tmp53 ;
1304 void *__cil_tmp54 ;
1305 unsigned int __cil_tmp55 ;
1306 unsigned int __cil_tmp56 ;
1307 unsigned long __cil_tmp57 ;
1308 unsigned long __cil_tmp58 ;
1309 unsigned long __cil_tmp59 ;
1310 unsigned long __cil_tmp60 ;
1311 unsigned long __cil_tmp61 ;
1312 unsigned long __cil_tmp62 ;
1313 unsigned long __cil_tmp63 ;
1314 unsigned long __cil_tmp64 ;
1315
1316 {
1317#line 373
1318 if (opt_len != 3) {
1319#line 376
1320 return ((void *)0);
1321 } else {
1322 {
1323#line 373
1324 __cil_tmp12 = *options;
1325#line 373
1326 __cil_tmp13 = (unsigned int )__cil_tmp12;
1327#line 373
1328 if (__cil_tmp13 != 21U) {
1329#line 376
1330 return ((void *)0);
1331 } else {
1332 {
1333#line 373
1334 __cil_tmp14 = options + 1UL;
1335#line 373
1336 __cil_tmp15 = *__cil_tmp14;
1337#line 373
1338 __cil_tmp16 = (unsigned int )__cil_tmp15;
1339#line 373
1340 if (__cil_tmp16 != 3U) {
1341#line 376
1342 return ((void *)0);
1343 } else {
1344 {
1345#line 373
1346 __cil_tmp17 = options + 2UL;
1347#line 373
1348 __cil_tmp18 = *__cil_tmp17;
1349#line 373
1350 __cil_tmp19 = (int )__cil_tmp18;
1351#line 373
1352 __cil_tmp20 = __cil_tmp19 >> 5;
1353#line 373
1354 __cil_tmp21 = (unsigned int )__cil_tmp20;
1355#line 373
1356 if (__cil_tmp21 != 1U) {
1357#line 376
1358 return ((void *)0);
1359 } else {
1360
1361 }
1362 }
1363 }
1364 }
1365 }
1366 }
1367 }
1368#line 379
1369 __cil_tmp22 = options + 2UL;
1370#line 379
1371 __cil_tmp23 = *__cil_tmp22;
1372#line 379
1373 __cil_tmp24 = (int )__cil_tmp23;
1374#line 379
1375 bits = __cil_tmp24 & 31;
1376#line 383
1377 if (bits == 9) {
1378#line 383
1379 goto case_9;
1380 } else
1381#line 384
1382 if (bits == 10) {
1383#line 384
1384 goto case_10;
1385 } else
1386#line 385
1387 if (bits == 11) {
1388#line 385
1389 goto case_11;
1390 } else
1391#line 386
1392 if (bits == 12) {
1393#line 386
1394 goto case_12;
1395 } else
1396#line 390
1397 if (bits == 13) {
1398#line 390
1399 goto case_13;
1400 } else
1401#line 394
1402 if (bits == 14) {
1403#line 394
1404 goto case_14;
1405 } else
1406#line 398
1407 if (bits == 15) {
1408#line 398
1409 goto case_15;
1410 } else
1411#line 402
1412 if (bits == 16) {
1413#line 402
1414 goto case_16;
1415 } else {
1416 {
1417#line 406
1418 goto switch_default;
1419#line 381
1420 if (0) {
1421 case_9: ;
1422 case_10: ;
1423 case_11: ;
1424 case_12:
1425#line 387
1426 hsize = 5003U;
1427#line 388
1428 hshift = 4U;
1429#line 389
1430 goto ldv_14405;
1431 case_13:
1432#line 391
1433 hsize = 9001U;
1434#line 392
1435 hshift = 5U;
1436#line 393
1437 goto ldv_14405;
1438 case_14:
1439#line 395
1440 hsize = 18013U;
1441#line 396
1442 hshift = 6U;
1443#line 397
1444 goto ldv_14405;
1445 case_15:
1446#line 399
1447 hsize = 35023U;
1448#line 400
1449 hshift = 7U;
1450#line 401
1451 goto ldv_14405;
1452 case_16: ;
1453 switch_default: ;
1454#line 407
1455 return ((void *)0);
1456 } else {
1457 switch_break: ;
1458 }
1459 }
1460 }
1461 ldv_14405:
1462 {
1463#line 412
1464 __cil_tmp25 = 1 << bits;
1465#line 412
1466 __cil_tmp26 = __cil_tmp25 + -1;
1467#line 412
1468 maxmaxcode = (unsigned int )__cil_tmp26;
1469#line 413
1470 tmp = kzalloc(88UL, 208U);
1471#line 413
1472 db = (struct bsd_db *)tmp;
1473 }
1474 {
1475#line 415
1476 __cil_tmp27 = (struct bsd_db *)0;
1477#line 415
1478 __cil_tmp28 = (unsigned long )__cil_tmp27;
1479#line 415
1480 __cil_tmp29 = (unsigned long )db;
1481#line 415
1482 if (__cil_tmp29 == __cil_tmp28) {
1483#line 417
1484 return ((void *)0);
1485 } else {
1486
1487 }
1488 }
1489 {
1490#line 424
1491 __cil_tmp30 = (unsigned long )hsize;
1492#line 424
1493 __cil_tmp31 = __cil_tmp30 * 16UL;
1494#line 424
1495 tmp___0 = ldv_vmalloc_19(__cil_tmp31);
1496#line 424
1497 __cil_tmp32 = (unsigned long )db;
1498#line 424
1499 __cil_tmp33 = __cil_tmp32 + 80;
1500#line 424
1501 *((struct bsd_dict **)__cil_tmp33) = (struct bsd_dict *)tmp___0;
1502 }
1503 {
1504#line 425
1505 __cil_tmp34 = (struct bsd_dict *)0;
1506#line 425
1507 __cil_tmp35 = (unsigned long )__cil_tmp34;
1508#line 425
1509 __cil_tmp36 = (unsigned long )db;
1510#line 425
1511 __cil_tmp37 = __cil_tmp36 + 80;
1512#line 425
1513 __cil_tmp38 = *((struct bsd_dict **)__cil_tmp37);
1514#line 425
1515 __cil_tmp39 = (unsigned long )__cil_tmp38;
1516#line 425
1517 if (__cil_tmp39 == __cil_tmp35) {
1518 {
1519#line 427
1520 __cil_tmp40 = (void *)db;
1521#line 427
1522 bsd_free(__cil_tmp40);
1523 }
1524#line 428
1525 return ((void *)0);
1526 } else {
1527
1528 }
1529 }
1530#line 434
1531 if (decomp == 0) {
1532#line 436
1533 __cil_tmp41 = (unsigned long )db;
1534#line 436
1535 __cil_tmp42 = __cil_tmp41 + 72;
1536#line 436
1537 *((unsigned short **)__cil_tmp42) = (unsigned short *)0;
1538 } else {
1539 {
1540#line 443
1541 __cil_tmp43 = maxmaxcode + 1U;
1542#line 443
1543 __cil_tmp44 = (unsigned long )__cil_tmp43;
1544#line 443
1545 __cil_tmp45 = __cil_tmp44 * 2UL;
1546#line 443
1547 tmp___1 = ldv_vmalloc_20(__cil_tmp45);
1548#line 443
1549 __cil_tmp46 = (unsigned long )db;
1550#line 443
1551 __cil_tmp47 = __cil_tmp46 + 72;
1552#line 443
1553 *((unsigned short **)__cil_tmp47) = (unsigned short *)tmp___1;
1554 }
1555 {
1556#line 444
1557 __cil_tmp48 = (unsigned short *)0;
1558#line 444
1559 __cil_tmp49 = (unsigned long )__cil_tmp48;
1560#line 444
1561 __cil_tmp50 = (unsigned long )db;
1562#line 444
1563 __cil_tmp51 = __cil_tmp50 + 72;
1564#line 444
1565 __cil_tmp52 = *((unsigned short **)__cil_tmp51);
1566#line 444
1567 __cil_tmp53 = (unsigned long )__cil_tmp52;
1568#line 444
1569 if (__cil_tmp53 == __cil_tmp49) {
1570 {
1571#line 446
1572 __cil_tmp54 = (void *)db;
1573#line 446
1574 bsd_free(__cil_tmp54);
1575 }
1576#line 447
1577 return ((void *)0);
1578 } else {
1579
1580 }
1581 }
1582 }
1583#line 453
1584 __cil_tmp55 = hsize * 16U;
1585#line 453
1586 __cil_tmp56 = __cil_tmp55 + 88U;
1587#line 453
1588 *((int *)db) = (int )__cil_tmp56;
1589#line 456
1590 __cil_tmp57 = (unsigned long )db;
1591#line 456
1592 __cil_tmp58 = __cil_tmp57 + 4;
1593#line 456
1594 *((unsigned int *)__cil_tmp58) = hsize;
1595#line 457
1596 __cil_tmp59 = (unsigned long )db;
1597#line 457
1598 __cil_tmp60 = __cil_tmp59 + 8;
1599#line 457
1600 *((unsigned char *)__cil_tmp60) = (unsigned char )hshift;
1601#line 458
1602 __cil_tmp61 = (unsigned long )db;
1603#line 458
1604 __cil_tmp62 = __cil_tmp61 + 20;
1605#line 458
1606 *((unsigned int *)__cil_tmp62) = maxmaxcode;
1607#line 459
1608 __cil_tmp63 = (unsigned long )db;
1609#line 459
1610 __cil_tmp64 = __cil_tmp63 + 10;
1611#line 459
1612 *((unsigned char *)__cil_tmp64) = (unsigned char )bits;
1613#line 461
1614 return ((void *)db);
1615}
1616}
1617#line 464 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
1618static void *bsd_comp_alloc(unsigned char *options , int opt_len )
1619{ void *tmp ;
1620
1621 {
1622 {
1623#line 466
1624 tmp = bsd_alloc(options, opt_len, 0);
1625 }
1626#line 466
1627 return (tmp);
1628}
1629}
1630#line 469 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
1631static void *bsd_decomp_alloc(unsigned char *options , int opt_len )
1632{ void *tmp ;
1633
1634 {
1635 {
1636#line 471
1637 tmp = bsd_alloc(options, opt_len, 1);
1638 }
1639#line 471
1640 return (tmp);
1641}
1642}
1643#line 478 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
1644static int bsd_init(void *state , unsigned char *options , int opt_len , int unit ,
1645 int debug , int decomp )
1646{ struct bsd_db *db ;
1647 int indx ;
1648 int tmp ;
1649 int tmp___0 ;
1650 unsigned char __cil_tmp11 ;
1651 unsigned int __cil_tmp12 ;
1652 unsigned char *__cil_tmp13 ;
1653 unsigned char __cil_tmp14 ;
1654 unsigned int __cil_tmp15 ;
1655 unsigned char *__cil_tmp16 ;
1656 unsigned char __cil_tmp17 ;
1657 int __cil_tmp18 ;
1658 int __cil_tmp19 ;
1659 unsigned int __cil_tmp20 ;
1660 unsigned long __cil_tmp21 ;
1661 unsigned long __cil_tmp22 ;
1662 unsigned char __cil_tmp23 ;
1663 int __cil_tmp24 ;
1664 unsigned char *__cil_tmp25 ;
1665 unsigned char __cil_tmp26 ;
1666 int __cil_tmp27 ;
1667 int __cil_tmp28 ;
1668 unsigned short *__cil_tmp29 ;
1669 unsigned long __cil_tmp30 ;
1670 unsigned long __cil_tmp31 ;
1671 unsigned long __cil_tmp32 ;
1672 unsigned short *__cil_tmp33 ;
1673 unsigned long __cil_tmp34 ;
1674 unsigned long __cil_tmp35 ;
1675 unsigned long __cil_tmp36 ;
1676 unsigned long __cil_tmp37 ;
1677 unsigned short *__cil_tmp38 ;
1678 unsigned short *__cil_tmp39 ;
1679 unsigned long __cil_tmp40 ;
1680 unsigned long __cil_tmp41 ;
1681 unsigned int __cil_tmp42 ;
1682 unsigned long __cil_tmp43 ;
1683 unsigned long __cil_tmp44 ;
1684 unsigned long __cil_tmp45 ;
1685 struct bsd_dict *__cil_tmp46 ;
1686 struct bsd_dict *__cil_tmp47 ;
1687 unsigned long __cil_tmp48 ;
1688 unsigned long __cil_tmp49 ;
1689 unsigned long __cil_tmp50 ;
1690 unsigned long __cil_tmp51 ;
1691 unsigned long __cil_tmp52 ;
1692 struct bsd_dict *__cil_tmp53 ;
1693 struct bsd_dict *__cil_tmp54 ;
1694 unsigned long __cil_tmp55 ;
1695 unsigned long __cil_tmp56 ;
1696 unsigned long __cil_tmp57 ;
1697 unsigned long __cil_tmp58 ;
1698 unsigned long __cil_tmp59 ;
1699 unsigned long __cil_tmp60 ;
1700 unsigned long __cil_tmp61 ;
1701 unsigned long __cil_tmp62 ;
1702 void *__cil_tmp63 ;
1703
1704 {
1705#line 481
1706 db = (struct bsd_db *)state;
1707#line 484
1708 if (opt_len != 3) {
1709#line 489
1710 return (0);
1711 } else {
1712 {
1713#line 484
1714 __cil_tmp11 = *options;
1715#line 484
1716 __cil_tmp12 = (unsigned int )__cil_tmp11;
1717#line 484
1718 if (__cil_tmp12 != 21U) {
1719#line 489
1720 return (0);
1721 } else {
1722 {
1723#line 484
1724 __cil_tmp13 = options + 1UL;
1725#line 484
1726 __cil_tmp14 = *__cil_tmp13;
1727#line 484
1728 __cil_tmp15 = (unsigned int )__cil_tmp14;
1729#line 484
1730 if (__cil_tmp15 != 3U) {
1731#line 489
1732 return (0);
1733 } else {
1734 {
1735#line 484
1736 __cil_tmp16 = options + 2UL;
1737#line 484
1738 __cil_tmp17 = *__cil_tmp16;
1739#line 484
1740 __cil_tmp18 = (int )__cil_tmp17;
1741#line 484
1742 __cil_tmp19 = __cil_tmp18 >> 5;
1743#line 484
1744 __cil_tmp20 = (unsigned int )__cil_tmp19;
1745#line 484
1746 if (__cil_tmp20 != 1U) {
1747#line 489
1748 return (0);
1749 } else {
1750 {
1751#line 484
1752 __cil_tmp21 = (unsigned long )db;
1753#line 484
1754 __cil_tmp22 = __cil_tmp21 + 10;
1755#line 484
1756 __cil_tmp23 = *((unsigned char *)__cil_tmp22);
1757#line 484
1758 __cil_tmp24 = (int )__cil_tmp23;
1759#line 484
1760 __cil_tmp25 = options + 2UL;
1761#line 484
1762 __cil_tmp26 = *__cil_tmp25;
1763#line 484
1764 __cil_tmp27 = (int )__cil_tmp26;
1765#line 484
1766 __cil_tmp28 = __cil_tmp27 & 31;
1767#line 484
1768 if (__cil_tmp28 != __cil_tmp24) {
1769#line 489
1770 return (0);
1771 } else
1772#line 484
1773 if (decomp != 0) {
1774 {
1775#line 484
1776 __cil_tmp29 = (unsigned short *)0;
1777#line 484
1778 __cil_tmp30 = (unsigned long )__cil_tmp29;
1779#line 484
1780 __cil_tmp31 = (unsigned long )db;
1781#line 484
1782 __cil_tmp32 = __cil_tmp31 + 72;
1783#line 484
1784 __cil_tmp33 = *((unsigned short **)__cil_tmp32);
1785#line 484
1786 __cil_tmp34 = (unsigned long )__cil_tmp33;
1787#line 484
1788 if (__cil_tmp34 == __cil_tmp30) {
1789#line 489
1790 return (0);
1791 } else {
1792
1793 }
1794 }
1795 } else {
1796
1797 }
1798 }
1799 }
1800 }
1801 }
1802 }
1803 }
1804 }
1805 }
1806#line 492
1807 if (decomp != 0) {
1808#line 494
1809 indx = 255;
1810 ldv_14429:
1811#line 497
1812 __cil_tmp35 = (unsigned long )indx;
1813#line 497
1814 __cil_tmp36 = (unsigned long )db;
1815#line 497
1816 __cil_tmp37 = __cil_tmp36 + 72;
1817#line 497
1818 __cil_tmp38 = *((unsigned short **)__cil_tmp37);
1819#line 497
1820 __cil_tmp39 = __cil_tmp38 + __cil_tmp35;
1821#line 497
1822 *__cil_tmp39 = (unsigned short)1;
1823#line 499
1824 tmp = indx;
1825#line 499
1826 indx = indx - 1;
1827#line 499
1828 if (tmp > 0) {
1829#line 500
1830 goto ldv_14429;
1831 } else {
1832#line 502
1833 goto ldv_14430;
1834 }
1835 ldv_14430: ;
1836 } else {
1837
1838 }
1839#line 502
1840 __cil_tmp40 = (unsigned long )db;
1841#line 502
1842 __cil_tmp41 = __cil_tmp40 + 4;
1843#line 502
1844 __cil_tmp42 = *((unsigned int *)__cil_tmp41);
1845#line 502
1846 indx = (int )__cil_tmp42;
1847#line 503
1848 goto ldv_14432;
1849 ldv_14431:
1850#line 505
1851 __cil_tmp43 = (unsigned long )indx;
1852#line 505
1853 __cil_tmp44 = (unsigned long )db;
1854#line 505
1855 __cil_tmp45 = __cil_tmp44 + 80;
1856#line 505
1857 __cil_tmp46 = *((struct bsd_dict **)__cil_tmp45);
1858#line 505
1859 __cil_tmp47 = __cil_tmp46 + __cil_tmp43;
1860#line 505
1861 __cil_tmp48 = (unsigned long )__cil_tmp47;
1862#line 505
1863 __cil_tmp49 = __cil_tmp48 + 8;
1864#line 505
1865 *((unsigned short *)__cil_tmp49) = (unsigned short)32767;
1866#line 506
1867 __cil_tmp50 = (unsigned long )indx;
1868#line 506
1869 __cil_tmp51 = (unsigned long )db;
1870#line 506
1871 __cil_tmp52 = __cil_tmp51 + 80;
1872#line 506
1873 __cil_tmp53 = *((struct bsd_dict **)__cil_tmp52);
1874#line 506
1875 __cil_tmp54 = __cil_tmp53 + __cil_tmp50;
1876#line 506
1877 __cil_tmp55 = (unsigned long )__cil_tmp54;
1878#line 506
1879 __cil_tmp56 = __cil_tmp55 + 10;
1880#line 506
1881 *((unsigned short *)__cil_tmp56) = (unsigned short)0;
1882 ldv_14432:
1883#line 503
1884 tmp___0 = indx;
1885#line 503
1886 indx = indx - 1;
1887#line 503
1888 if (tmp___0 != 0) {
1889#line 504
1890 goto ldv_14431;
1891 } else {
1892#line 506
1893 goto ldv_14433;
1894 }
1895 ldv_14433:
1896#line 509
1897 __cil_tmp57 = (unsigned long )db;
1898#line 509
1899 __cil_tmp58 = __cil_tmp57 + 12;
1900#line 509
1901 *((unsigned char *)__cil_tmp58) = (unsigned char )unit;
1902#line 510
1903 __cil_tmp59 = (unsigned long )db;
1904#line 510
1905 __cil_tmp60 = __cil_tmp59 + 16;
1906#line 510
1907 *((unsigned int *)__cil_tmp60) = 0U;
1908#line 512
1909 if (debug != 0) {
1910#line 514
1911 __cil_tmp61 = (unsigned long )db;
1912#line 514
1913 __cil_tmp62 = __cil_tmp61 + 11;
1914#line 514
1915 *((unsigned char *)__cil_tmp62) = (unsigned char)1;
1916 } else {
1917
1918 }
1919 {
1920#line 516
1921 __cil_tmp63 = (void *)db;
1922#line 516
1923 bsd_reset(__cil_tmp63);
1924 }
1925#line 518
1926 return (1);
1927}
1928}
1929#line 521 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
1930static int bsd_comp_init(void *state , unsigned char *options , int opt_len , int unit ,
1931 int opthdr , int debug )
1932{ int tmp ;
1933
1934 {
1935 {
1936#line 524
1937 tmp = bsd_init(state, options, opt_len, unit, debug, 0);
1938 }
1939#line 524
1940 return (tmp);
1941}
1942}
1943#line 527 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
1944static int bsd_decomp_init(void *state , unsigned char *options , int opt_len , int unit ,
1945 int opthdr , int mru , int debug )
1946{ int tmp ;
1947
1948 {
1949 {
1950#line 531
1951 tmp = bsd_init(state, options, opt_len, unit, debug, 1);
1952 }
1953#line 531
1954 return (tmp);
1955}
1956}
1957#line 578 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
1958static int bsd_compress(void *state , unsigned char *rptr , unsigned char *obuf ,
1959 int isize , int osize )
1960{ struct bsd_db *db ;
1961 int hshift ;
1962 unsigned int max_ent ;
1963 unsigned int n_bits ;
1964 unsigned int bitno ;
1965 unsigned long accm ;
1966 int ent ;
1967 unsigned long fcode ;
1968 struct bsd_dict *dictp ;
1969 unsigned char c ;
1970 int hval ;
1971 int disp ;
1972 int ilen ;
1973 int mxcode ;
1974 unsigned char *wptr ;
1975 int olen ;
1976 unsigned char *tmp ;
1977 unsigned char *tmp___0 ;
1978 unsigned char *tmp___1 ;
1979 unsigned char *tmp___2 ;
1980 unsigned char *tmp___3 ;
1981 unsigned char *tmp___4 ;
1982 unsigned char *tmp___5 ;
1983 unsigned char *tmp___6 ;
1984 struct bsd_dict *dictp2 ;
1985 struct bsd_dict *dictp3 ;
1986 int indx ;
1987 unsigned short *len1 ;
1988 unsigned short *len2 ;
1989 unsigned char *tmp___7 ;
1990 unsigned char *tmp___8 ;
1991 int tmp___9 ;
1992 unsigned char *tmp___10 ;
1993 __u8 *__cil_tmp39 ;
1994 __u8 __cil_tmp40 ;
1995 int __cil_tmp41 ;
1996 __u8 *__cil_tmp42 ;
1997 __u8 __cil_tmp43 ;
1998 int __cil_tmp44 ;
1999 int __cil_tmp45 ;
2000 unsigned long __cil_tmp46 ;
2001 unsigned long __cil_tmp47 ;
2002 unsigned char __cil_tmp48 ;
2003 unsigned long __cil_tmp49 ;
2004 unsigned long __cil_tmp50 ;
2005 unsigned long __cil_tmp51 ;
2006 unsigned long __cil_tmp52 ;
2007 unsigned char __cil_tmp53 ;
2008 int __cil_tmp54 ;
2009 int __cil_tmp55 ;
2010 unsigned char *__cil_tmp56 ;
2011 unsigned long __cil_tmp57 ;
2012 unsigned long __cil_tmp58 ;
2013 __u8 *__cil_tmp59 ;
2014 unsigned long __cil_tmp60 ;
2015 unsigned long __cil_tmp61 ;
2016 unsigned short __cil_tmp62 ;
2017 int __cil_tmp63 ;
2018 int __cil_tmp64 ;
2019 unsigned long __cil_tmp65 ;
2020 unsigned long __cil_tmp66 ;
2021 unsigned short __cil_tmp67 ;
2022 unsigned long __cil_tmp68 ;
2023 unsigned long __cil_tmp69 ;
2024 unsigned long __cil_tmp70 ;
2025 unsigned int __cil_tmp71 ;
2026 unsigned long __cil_tmp72 ;
2027 unsigned long __cil_tmp73 ;
2028 unsigned int __cil_tmp74 ;
2029 unsigned int __cil_tmp75 ;
2030 unsigned long __cil_tmp76 ;
2031 unsigned long __cil_tmp77 ;
2032 unsigned long __cil_tmp78 ;
2033 struct bsd_dict *__cil_tmp79 ;
2034 unsigned long __cil_tmp80 ;
2035 unsigned long __cil_tmp81 ;
2036 unsigned short __cil_tmp82 ;
2037 unsigned int __cil_tmp83 ;
2038 unsigned long __cil_tmp84 ;
2039 unsigned long __cil_tmp85 ;
2040 unsigned long __cil_tmp86 ;
2041 unsigned short __cil_tmp87 ;
2042 int __cil_tmp88 ;
2043 unsigned long __cil_tmp89 ;
2044 unsigned long __cil_tmp90 ;
2045 unsigned int __cil_tmp91 ;
2046 unsigned int __cil_tmp92 ;
2047 unsigned long __cil_tmp93 ;
2048 unsigned long __cil_tmp94 ;
2049 unsigned int __cil_tmp95 ;
2050 unsigned int __cil_tmp96 ;
2051 unsigned int __cil_tmp97 ;
2052 unsigned long __cil_tmp98 ;
2053 unsigned long __cil_tmp99 ;
2054 unsigned long __cil_tmp100 ;
2055 struct bsd_dict *__cil_tmp101 ;
2056 unsigned long __cil_tmp102 ;
2057 unsigned long __cil_tmp103 ;
2058 unsigned short __cil_tmp104 ;
2059 unsigned int __cil_tmp105 ;
2060 unsigned long __cil_tmp106 ;
2061 unsigned long __cil_tmp107 ;
2062 unsigned long __cil_tmp108 ;
2063 unsigned short __cil_tmp109 ;
2064 int __cil_tmp110 ;
2065 int __cil_tmp111 ;
2066 int __cil_tmp112 ;
2067 unsigned long __cil_tmp113 ;
2068 unsigned char *__cil_tmp114 ;
2069 unsigned long __cil_tmp115 ;
2070 unsigned long __cil_tmp116 ;
2071 unsigned long __cil_tmp117 ;
2072 unsigned long __cil_tmp118 ;
2073 unsigned long __cil_tmp119 ;
2074 unsigned int __cil_tmp120 ;
2075 unsigned int __cil_tmp121 ;
2076 unsigned long __cil_tmp122 ;
2077 unsigned long __cil_tmp123 ;
2078 int __cil_tmp124 ;
2079 int __cil_tmp125 ;
2080 unsigned int __cil_tmp126 ;
2081 unsigned long __cil_tmp127 ;
2082 unsigned long __cil_tmp128 ;
2083 unsigned long __cil_tmp129 ;
2084 struct bsd_dict *__cil_tmp130 ;
2085 unsigned long __cil_tmp131 ;
2086 unsigned long __cil_tmp132 ;
2087 unsigned short __cil_tmp133 ;
2088 unsigned long __cil_tmp134 ;
2089 unsigned long __cil_tmp135 ;
2090 unsigned long __cil_tmp136 ;
2091 struct bsd_dict *__cil_tmp137 ;
2092 unsigned long __cil_tmp138 ;
2093 unsigned long __cil_tmp139 ;
2094 unsigned short __cil_tmp140 ;
2095 unsigned int __cil_tmp141 ;
2096 unsigned long __cil_tmp142 ;
2097 unsigned long __cil_tmp143 ;
2098 unsigned long __cil_tmp144 ;
2099 unsigned long __cil_tmp145 ;
2100 unsigned long __cil_tmp146 ;
2101 unsigned long __cil_tmp147 ;
2102 unsigned long __cil_tmp148 ;
2103 unsigned long __cil_tmp149 ;
2104 unsigned short *__cil_tmp150 ;
2105 unsigned long __cil_tmp151 ;
2106 unsigned long __cil_tmp152 ;
2107 unsigned long __cil_tmp153 ;
2108 unsigned short *__cil_tmp154 ;
2109 unsigned long __cil_tmp155 ;
2110 unsigned long __cil_tmp156 ;
2111 unsigned long __cil_tmp157 ;
2112 unsigned long __cil_tmp158 ;
2113 unsigned short *__cil_tmp159 ;
2114 unsigned long __cil_tmp160 ;
2115 unsigned long __cil_tmp161 ;
2116 unsigned long __cil_tmp162 ;
2117 unsigned short *__cil_tmp163 ;
2118 unsigned short __cil_tmp164 ;
2119 unsigned int __cil_tmp165 ;
2120 unsigned int __cil_tmp166 ;
2121 int __cil_tmp167 ;
2122 int __cil_tmp168 ;
2123 unsigned long __cil_tmp169 ;
2124 unsigned char *__cil_tmp170 ;
2125 unsigned long __cil_tmp171 ;
2126 unsigned long __cil_tmp172 ;
2127 unsigned long __cil_tmp173 ;
2128 unsigned long __cil_tmp174 ;
2129 unsigned long __cil_tmp175 ;
2130 unsigned int __cil_tmp176 ;
2131 unsigned long __cil_tmp177 ;
2132 unsigned long __cil_tmp178 ;
2133 unsigned int __cil_tmp179 ;
2134 unsigned int __cil_tmp180 ;
2135 unsigned long __cil_tmp181 ;
2136 unsigned long __cil_tmp182 ;
2137 unsigned int __cil_tmp183 ;
2138 unsigned long __cil_tmp184 ;
2139 unsigned long __cil_tmp185 ;
2140 unsigned int __cil_tmp186 ;
2141 unsigned long __cil_tmp187 ;
2142 unsigned long __cil_tmp188 ;
2143 unsigned int __cil_tmp189 ;
2144 unsigned long __cil_tmp190 ;
2145 unsigned long __cil_tmp191 ;
2146 unsigned int __cil_tmp192 ;
2147 unsigned long __cil_tmp193 ;
2148 unsigned long __cil_tmp194 ;
2149 unsigned long __cil_tmp195 ;
2150 unsigned long __cil_tmp196 ;
2151 unsigned int __cil_tmp197 ;
2152 unsigned long __cil_tmp198 ;
2153 unsigned long __cil_tmp199 ;
2154 unsigned long __cil_tmp200 ;
2155 unsigned long __cil_tmp201 ;
2156 unsigned short __cil_tmp202 ;
2157 int __cil_tmp203 ;
2158 int __cil_tmp204 ;
2159 unsigned long __cil_tmp205 ;
2160 unsigned long __cil_tmp206 ;
2161 unsigned long __cil_tmp207 ;
2162 unsigned long __cil_tmp208 ;
2163 unsigned int __cil_tmp209 ;
2164 int __cil_tmp210 ;
2165 int __cil_tmp211 ;
2166 unsigned long __cil_tmp212 ;
2167 unsigned char *__cil_tmp213 ;
2168 unsigned long __cil_tmp214 ;
2169 unsigned long __cil_tmp215 ;
2170 unsigned long __cil_tmp216 ;
2171 unsigned char *__cil_tmp217 ;
2172 unsigned long __cil_tmp218 ;
2173 unsigned long __cil_tmp219 ;
2174 unsigned int __cil_tmp220 ;
2175 int __cil_tmp221 ;
2176 int __cil_tmp222 ;
2177 unsigned long __cil_tmp223 ;
2178 unsigned long __cil_tmp224 ;
2179 unsigned long __cil_tmp225 ;
2180 unsigned int __cil_tmp226 ;
2181 unsigned long __cil_tmp227 ;
2182 unsigned long __cil_tmp228 ;
2183 unsigned int __cil_tmp229 ;
2184 unsigned long __cil_tmp230 ;
2185 unsigned long __cil_tmp231 ;
2186 unsigned long __cil_tmp232 ;
2187 unsigned long __cil_tmp233 ;
2188 unsigned char __cil_tmp234 ;
2189 int __cil_tmp235 ;
2190 int __cil_tmp236 ;
2191 unsigned char *__cil_tmp237 ;
2192 unsigned long __cil_tmp238 ;
2193 unsigned long __cil_tmp239 ;
2194 unsigned long __cil_tmp240 ;
2195 unsigned long __cil_tmp241 ;
2196 unsigned long __cil_tmp242 ;
2197 unsigned long __cil_tmp243 ;
2198 unsigned int __cil_tmp244 ;
2199 unsigned long __cil_tmp245 ;
2200 unsigned long __cil_tmp246 ;
2201 unsigned int __cil_tmp247 ;
2202 unsigned long __cil_tmp248 ;
2203 unsigned long __cil_tmp249 ;
2204 unsigned int __cil_tmp250 ;
2205 unsigned long __cil_tmp251 ;
2206 unsigned long __cil_tmp252 ;
2207 unsigned long __cil_tmp253 ;
2208 unsigned long __cil_tmp254 ;
2209 unsigned int __cil_tmp255 ;
2210 unsigned long __cil_tmp256 ;
2211 unsigned long __cil_tmp257 ;
2212 unsigned int __cil_tmp258 ;
2213 unsigned long __cil_tmp259 ;
2214 unsigned long __cil_tmp260 ;
2215 unsigned int __cil_tmp261 ;
2216
2217 {
2218#line 630
2219 __cil_tmp39 = rptr + 3UL;
2220#line 630
2221 __cil_tmp40 = *__cil_tmp39;
2222#line 630
2223 __cil_tmp41 = (int )__cil_tmp40;
2224#line 630
2225 __cil_tmp42 = rptr + 2UL;
2226#line 630
2227 __cil_tmp43 = *__cil_tmp42;
2228#line 630
2229 __cil_tmp44 = (int )__cil_tmp43;
2230#line 630
2231 __cil_tmp45 = __cil_tmp44 << 8;
2232#line 630
2233 ent = __cil_tmp45 + __cil_tmp41;
2234#line 631
2235 if (ent <= 32) {
2236#line 633
2237 return (0);
2238 } else
2239#line 631
2240 if (ent > 249) {
2241#line 633
2242 return (0);
2243 } else {
2244
2245 }
2246#line 636
2247 db = (struct bsd_db *)state;
2248#line 637
2249 __cil_tmp46 = (unsigned long )db;
2250#line 637
2251 __cil_tmp47 = __cil_tmp46 + 8;
2252#line 637
2253 __cil_tmp48 = *((unsigned char *)__cil_tmp47);
2254#line 637
2255 hshift = (int )__cil_tmp48;
2256#line 638
2257 __cil_tmp49 = (unsigned long )db;
2258#line 638
2259 __cil_tmp50 = __cil_tmp49 + 24;
2260#line 638
2261 max_ent = *((unsigned int *)__cil_tmp50);
2262#line 639
2263 __cil_tmp51 = (unsigned long )db;
2264#line 639
2265 __cil_tmp52 = __cil_tmp51 + 9;
2266#line 639
2267 __cil_tmp53 = *((unsigned char *)__cil_tmp52);
2268#line 639
2269 n_bits = (unsigned int )__cil_tmp53;
2270#line 640
2271 bitno = 32U;
2272#line 641
2273 accm = 0UL;
2274#line 642
2275 __cil_tmp54 = (int )n_bits;
2276#line 642
2277 __cil_tmp55 = 1 << __cil_tmp54;
2278#line 642
2279 mxcode = __cil_tmp55 + -1;
2280#line 645
2281 wptr = obuf;
2282#line 646
2283 olen = 6;
2284#line 648
2285 if (osize > isize) {
2286#line 650
2287 osize = isize;
2288 } else {
2289
2290 }
2291 {
2292#line 654
2293 __cil_tmp56 = (unsigned char *)0;
2294#line 654
2295 __cil_tmp57 = (unsigned long )__cil_tmp56;
2296#line 654
2297 __cil_tmp58 = (unsigned long )wptr;
2298#line 654
2299 if (__cil_tmp58 != __cil_tmp57) {
2300#line 656
2301 tmp = wptr;
2302#line 656
2303 wptr = wptr + 1;
2304#line 656
2305 *tmp = *rptr;
2306#line 657
2307 tmp___0 = wptr;
2308#line 657
2309 wptr = wptr + 1;
2310#line 657
2311 __cil_tmp59 = rptr + 1UL;
2312#line 657
2313 *tmp___0 = *__cil_tmp59;
2314#line 658
2315 tmp___1 = wptr;
2316#line 658
2317 wptr = wptr + 1;
2318#line 658
2319 *tmp___1 = (unsigned char)0;
2320#line 659
2321 tmp___2 = wptr;
2322#line 659
2323 wptr = wptr + 1;
2324#line 659
2325 *tmp___2 = (unsigned char)253;
2326#line 660
2327 tmp___3 = wptr;
2328#line 660
2329 wptr = wptr + 1;
2330#line 660
2331 __cil_tmp60 = (unsigned long )db;
2332#line 660
2333 __cil_tmp61 = __cil_tmp60 + 14;
2334#line 660
2335 __cil_tmp62 = *((unsigned short *)__cil_tmp61);
2336#line 660
2337 __cil_tmp63 = (int )__cil_tmp62;
2338#line 660
2339 __cil_tmp64 = __cil_tmp63 >> 8;
2340#line 660
2341 *tmp___3 = (unsigned char )__cil_tmp64;
2342#line 661
2343 tmp___4 = wptr;
2344#line 661
2345 wptr = wptr + 1;
2346#line 661
2347 __cil_tmp65 = (unsigned long )db;
2348#line 661
2349 __cil_tmp66 = __cil_tmp65 + 14;
2350#line 661
2351 __cil_tmp67 = *((unsigned short *)__cil_tmp66);
2352#line 661
2353 *tmp___4 = (unsigned char )__cil_tmp67;
2354 } else {
2355
2356 }
2357 }
2358#line 665
2359 rptr = rptr + 4UL;
2360#line 666
2361 isize = isize + -4;
2362#line 667
2363 isize = isize + 1;
2364#line 667
2365 ilen = isize;
2366#line 669
2367 goto ldv_14475;
2368 ldv_14485:
2369#line 671
2370 tmp___5 = rptr;
2371#line 671
2372 rptr = rptr + 1;
2373#line 671
2374 c = *tmp___5;
2375#line 672
2376 __cil_tmp68 = (unsigned long )ent;
2377#line 672
2378 __cil_tmp69 = (unsigned long )c;
2379#line 672
2380 __cil_tmp70 = __cil_tmp69 << 16;
2381#line 672
2382 fcode = __cil_tmp70 + __cil_tmp68;
2383#line 673
2384 __cil_tmp71 = (unsigned int )ent;
2385#line 673
2386 __cil_tmp72 = (unsigned long )c;
2387#line 673
2388 __cil_tmp73 = __cil_tmp72 << hshift;
2389#line 673
2390 __cil_tmp74 = (unsigned int )__cil_tmp73;
2391#line 673
2392 __cil_tmp75 = __cil_tmp74 ^ __cil_tmp71;
2393#line 673
2394 hval = (int )__cil_tmp75;
2395#line 674
2396 __cil_tmp76 = (unsigned long )hval;
2397#line 674
2398 __cil_tmp77 = (unsigned long )db;
2399#line 674
2400 __cil_tmp78 = __cil_tmp77 + 80;
2401#line 674
2402 __cil_tmp79 = *((struct bsd_dict **)__cil_tmp78);
2403#line 674
2404 dictp = __cil_tmp79 + __cil_tmp76;
2405 {
2406#line 677
2407 __cil_tmp80 = (unsigned long )dictp;
2408#line 677
2409 __cil_tmp81 = __cil_tmp80 + 8;
2410#line 677
2411 __cil_tmp82 = *((unsigned short *)__cil_tmp81);
2412#line 677
2413 __cil_tmp83 = (unsigned int )__cil_tmp82;
2414#line 677
2415 if (__cil_tmp83 >= max_ent) {
2416#line 679
2417 goto nomatch;
2418 } else {
2419
2420 }
2421 }
2422 {
2423#line 682
2424 __cil_tmp84 = *((unsigned long *)dictp);
2425#line 682
2426 if (__cil_tmp84 == fcode) {
2427#line 684
2428 __cil_tmp85 = (unsigned long )dictp;
2429#line 684
2430 __cil_tmp86 = __cil_tmp85 + 8;
2431#line 684
2432 __cil_tmp87 = *((unsigned short *)__cil_tmp86);
2433#line 684
2434 __cil_tmp88 = (int )__cil_tmp87;
2435#line 684
2436 ent = __cil_tmp88 + 1;
2437#line 685
2438 goto ldv_14475;
2439 } else {
2440
2441 }
2442 }
2443#line 689
2444 if (hval != 0) {
2445#line 689
2446 disp = hval;
2447 } else {
2448#line 689
2449 disp = 1;
2450 }
2451 ldv_14476:
2452#line 693
2453 hval = hval + disp;
2454 {
2455#line 694
2456 __cil_tmp89 = (unsigned long )db;
2457#line 694
2458 __cil_tmp90 = __cil_tmp89 + 4;
2459#line 694
2460 __cil_tmp91 = *((unsigned int *)__cil_tmp90);
2461#line 694
2462 __cil_tmp92 = (unsigned int )hval;
2463#line 694
2464 if (__cil_tmp92 >= __cil_tmp91) {
2465#line 696
2466 __cil_tmp93 = (unsigned long )db;
2467#line 696
2468 __cil_tmp94 = __cil_tmp93 + 4;
2469#line 696
2470 __cil_tmp95 = *((unsigned int *)__cil_tmp94);
2471#line 696
2472 __cil_tmp96 = (unsigned int )hval;
2473#line 696
2474 __cil_tmp97 = __cil_tmp96 - __cil_tmp95;
2475#line 696
2476 hval = (int )__cil_tmp97;
2477 } else {
2478
2479 }
2480 }
2481#line 698
2482 __cil_tmp98 = (unsigned long )hval;
2483#line 698
2484 __cil_tmp99 = (unsigned long )db;
2485#line 698
2486 __cil_tmp100 = __cil_tmp99 + 80;
2487#line 698
2488 __cil_tmp101 = *((struct bsd_dict **)__cil_tmp100);
2489#line 698
2490 dictp = __cil_tmp101 + __cil_tmp98;
2491 {
2492#line 699
2493 __cil_tmp102 = (unsigned long )dictp;
2494#line 699
2495 __cil_tmp103 = __cil_tmp102 + 8;
2496#line 699
2497 __cil_tmp104 = *((unsigned short *)__cil_tmp103);
2498#line 699
2499 __cil_tmp105 = (unsigned int )__cil_tmp104;
2500#line 699
2501 if (__cil_tmp105 >= max_ent) {
2502#line 701
2503 goto nomatch;
2504 } else {
2505
2506 }
2507 }
2508 {
2509#line 704
2510 __cil_tmp106 = *((unsigned long *)dictp);
2511#line 704
2512 if (__cil_tmp106 != fcode) {
2513#line 705
2514 goto ldv_14476;
2515 } else {
2516#line 707
2517 goto ldv_14477;
2518 }
2519 }
2520 ldv_14477:
2521#line 706
2522 __cil_tmp107 = (unsigned long )dictp;
2523#line 706
2524 __cil_tmp108 = __cil_tmp107 + 8;
2525#line 706
2526 __cil_tmp109 = *((unsigned short *)__cil_tmp108);
2527#line 706
2528 __cil_tmp110 = (int )__cil_tmp109;
2529#line 706
2530 ent = __cil_tmp110 + 1;
2531#line 707
2532 goto ldv_14475;
2533 nomatch:
2534#line 710
2535 bitno = bitno - n_bits;
2536#line 710
2537 __cil_tmp111 = (int )bitno;
2538#line 710
2539 __cil_tmp112 = ent << __cil_tmp111;
2540#line 710
2541 __cil_tmp113 = (unsigned long )__cil_tmp112;
2542#line 710
2543 accm = __cil_tmp113 | accm;
2544 ldv_14478:
2545#line 710
2546 olen = olen + 1;
2547 {
2548#line 710
2549 __cil_tmp114 = (unsigned char *)0;
2550#line 710
2551 __cil_tmp115 = (unsigned long )__cil_tmp114;
2552#line 710
2553 __cil_tmp116 = (unsigned long )wptr;
2554#line 710
2555 if (__cil_tmp116 != __cil_tmp115) {
2556#line 710
2557 tmp___6 = wptr;
2558#line 710
2559 wptr = wptr + 1;
2560#line 710
2561 __cil_tmp117 = accm >> 24;
2562#line 710
2563 *tmp___6 = (unsigned char )__cil_tmp117;
2564#line 710
2565 if (olen >= osize) {
2566#line 710
2567 wptr = (unsigned char *)0;
2568 } else {
2569
2570 }
2571 } else {
2572
2573 }
2574 }
2575#line 710
2576 accm = accm << 8;
2577#line 710
2578 bitno = bitno + 8U;
2579#line 710
2580 if (bitno <= 24U) {
2581#line 711
2582 goto ldv_14478;
2583 } else {
2584#line 713
2585 goto ldv_14479;
2586 }
2587 ldv_14479: ;
2588 {
2589#line 713
2590 __cil_tmp118 = (unsigned long )db;
2591#line 713
2592 __cil_tmp119 = __cil_tmp118 + 20;
2593#line 713
2594 __cil_tmp120 = *((unsigned int *)__cil_tmp119);
2595#line 713
2596 if (__cil_tmp120 > max_ent) {
2597 {
2598#line 720
2599 __cil_tmp121 = (unsigned int )mxcode;
2600#line 720
2601 if (__cil_tmp121 <= max_ent) {
2602#line 722
2603 n_bits = n_bits + 1U;
2604#line 722
2605 __cil_tmp122 = (unsigned long )db;
2606#line 722
2607 __cil_tmp123 = __cil_tmp122 + 9;
2608#line 722
2609 *((unsigned char *)__cil_tmp123) = (unsigned char )n_bits;
2610#line 723
2611 __cil_tmp124 = (int )n_bits;
2612#line 723
2613 __cil_tmp125 = 1 << __cil_tmp124;
2614#line 723
2615 mxcode = __cil_tmp125 + -1;
2616 } else {
2617
2618 }
2619 }
2620#line 730
2621 __cil_tmp126 = max_ent + 1U;
2622#line 730
2623 __cil_tmp127 = (unsigned long )__cil_tmp126;
2624#line 730
2625 __cil_tmp128 = (unsigned long )db;
2626#line 730
2627 __cil_tmp129 = __cil_tmp128 + 80;
2628#line 730
2629 __cil_tmp130 = *((struct bsd_dict **)__cil_tmp129);
2630#line 730
2631 dictp2 = __cil_tmp130 + __cil_tmp127;
2632#line 731
2633 __cil_tmp131 = (unsigned long )dictp2;
2634#line 731
2635 __cil_tmp132 = __cil_tmp131 + 10;
2636#line 731
2637 __cil_tmp133 = *((unsigned short *)__cil_tmp132);
2638#line 731
2639 indx = (int )__cil_tmp133;
2640#line 732
2641 __cil_tmp134 = (unsigned long )indx;
2642#line 732
2643 __cil_tmp135 = (unsigned long )db;
2644#line 732
2645 __cil_tmp136 = __cil_tmp135 + 80;
2646#line 732
2647 __cil_tmp137 = *((struct bsd_dict **)__cil_tmp136);
2648#line 732
2649 dictp3 = __cil_tmp137 + __cil_tmp134;
2650 {
2651#line 734
2652 __cil_tmp138 = (unsigned long )dictp3;
2653#line 734
2654 __cil_tmp139 = __cil_tmp138 + 8;
2655#line 734
2656 __cil_tmp140 = *((unsigned short *)__cil_tmp139);
2657#line 734
2658 __cil_tmp141 = (unsigned int )__cil_tmp140;
2659#line 734
2660 if (__cil_tmp141 == max_ent) {
2661#line 736
2662 __cil_tmp142 = (unsigned long )dictp3;
2663#line 736
2664 __cil_tmp143 = __cil_tmp142 + 8;
2665#line 736
2666 *((unsigned short *)__cil_tmp143) = (unsigned short)32767;
2667 } else {
2668
2669 }
2670 }
2671#line 739
2672 __cil_tmp144 = (unsigned long )dictp2;
2673#line 739
2674 __cil_tmp145 = __cil_tmp144 + 10;
2675#line 739
2676 *((unsigned short *)__cil_tmp145) = (unsigned short )hval;
2677#line 740
2678 __cil_tmp146 = (unsigned long )dictp;
2679#line 740
2680 __cil_tmp147 = __cil_tmp146 + 8;
2681#line 740
2682 *((unsigned short *)__cil_tmp147) = (unsigned short )max_ent;
2683#line 741
2684 *((unsigned long *)dictp) = fcode;
2685#line 742
2686 max_ent = max_ent + 1U;
2687#line 742
2688 __cil_tmp148 = (unsigned long )db;
2689#line 742
2690 __cil_tmp149 = __cil_tmp148 + 24;
2691#line 742
2692 *((unsigned int *)__cil_tmp149) = max_ent;
2693 {
2694#line 744
2695 __cil_tmp150 = (unsigned short *)0;
2696#line 744
2697 __cil_tmp151 = (unsigned long )__cil_tmp150;
2698#line 744
2699 __cil_tmp152 = (unsigned long )db;
2700#line 744
2701 __cil_tmp153 = __cil_tmp152 + 72;
2702#line 744
2703 __cil_tmp154 = *((unsigned short **)__cil_tmp153);
2704#line 744
2705 __cil_tmp155 = (unsigned long )__cil_tmp154;
2706#line 744
2707 if (__cil_tmp155 != __cil_tmp151) {
2708#line 746
2709 __cil_tmp156 = (unsigned long )max_ent;
2710#line 746
2711 __cil_tmp157 = (unsigned long )db;
2712#line 746
2713 __cil_tmp158 = __cil_tmp157 + 72;
2714#line 746
2715 __cil_tmp159 = *((unsigned short **)__cil_tmp158);
2716#line 746
2717 len1 = __cil_tmp159 + __cil_tmp156;
2718#line 747
2719 __cil_tmp160 = (unsigned long )ent;
2720#line 747
2721 __cil_tmp161 = (unsigned long )db;
2722#line 747
2723 __cil_tmp162 = __cil_tmp161 + 72;
2724#line 747
2725 __cil_tmp163 = *((unsigned short **)__cil_tmp162);
2726#line 747
2727 len2 = __cil_tmp163 + __cil_tmp160;
2728#line 748
2729 __cil_tmp164 = *len2;
2730#line 748
2731 __cil_tmp165 = (unsigned int )__cil_tmp164;
2732#line 748
2733 __cil_tmp166 = __cil_tmp165 + 1U;
2734#line 748
2735 *len1 = (unsigned short )__cil_tmp166;
2736 } else {
2737
2738 }
2739 }
2740 } else {
2741
2742 }
2743 }
2744#line 751
2745 ent = (int )c;
2746 ldv_14475:
2747#line 669
2748 ilen = ilen - 1;
2749#line 669
2750 if (ilen > 0) {
2751#line 670
2752 goto ldv_14485;
2753 } else {
2754#line 672
2755 goto ldv_14486;
2756 }
2757 ldv_14486:
2758#line 754
2759 bitno = bitno - n_bits;
2760#line 754
2761 __cil_tmp167 = (int )bitno;
2762#line 754
2763 __cil_tmp168 = ent << __cil_tmp167;
2764#line 754
2765 __cil_tmp169 = (unsigned long )__cil_tmp168;
2766#line 754
2767 accm = __cil_tmp169 | accm;
2768 ldv_14487:
2769#line 754
2770 olen = olen + 1;
2771 {
2772#line 754
2773 __cil_tmp170 = (unsigned char *)0;
2774#line 754
2775 __cil_tmp171 = (unsigned long )__cil_tmp170;
2776#line 754
2777 __cil_tmp172 = (unsigned long )wptr;
2778#line 754
2779 if (__cil_tmp172 != __cil_tmp171) {
2780#line 754
2781 tmp___7 = wptr;
2782#line 754
2783 wptr = wptr + 1;
2784#line 754
2785 __cil_tmp173 = accm >> 24;
2786#line 754
2787 *tmp___7 = (unsigned char )__cil_tmp173;
2788#line 754
2789 if (olen >= osize) {
2790#line 754
2791 wptr = (unsigned char *)0;
2792 } else {
2793
2794 }
2795 } else {
2796
2797 }
2798 }
2799#line 754
2800 accm = accm << 8;
2801#line 754
2802 bitno = bitno + 8U;
2803#line 754
2804 if (bitno <= 24U) {
2805#line 755
2806 goto ldv_14487;
2807 } else {
2808#line 757
2809 goto ldv_14488;
2810 }
2811 ldv_14488:
2812#line 756
2813 __cil_tmp174 = (unsigned long )db;
2814#line 756
2815 __cil_tmp175 = __cil_tmp174 + 32;
2816#line 756
2817 __cil_tmp176 = (unsigned int )olen;
2818#line 756
2819 __cil_tmp177 = (unsigned long )db;
2820#line 756
2821 __cil_tmp178 = __cil_tmp177 + 32;
2822#line 756
2823 __cil_tmp179 = *((unsigned int *)__cil_tmp178);
2824#line 756
2825 __cil_tmp180 = __cil_tmp179 + __cil_tmp176;
2826#line 756
2827 *((unsigned int *)__cil_tmp175) = __cil_tmp180 + 4294967290U;
2828#line 757
2829 __cil_tmp181 = (unsigned long )db;
2830#line 757
2831 __cil_tmp182 = __cil_tmp181 + 60;
2832#line 757
2833 __cil_tmp183 = (unsigned int )isize;
2834#line 757
2835 __cil_tmp184 = (unsigned long )db;
2836#line 757
2837 __cil_tmp185 = __cil_tmp184 + 60;
2838#line 757
2839 __cil_tmp186 = *((unsigned int *)__cil_tmp185);
2840#line 757
2841 *((unsigned int *)__cil_tmp182) = __cil_tmp186 + __cil_tmp183;
2842#line 758
2843 __cil_tmp187 = (unsigned long )db;
2844#line 758
2845 __cil_tmp188 = __cil_tmp187 + 28;
2846#line 758
2847 __cil_tmp189 = (unsigned int )isize;
2848#line 758
2849 __cil_tmp190 = (unsigned long )db;
2850#line 758
2851 __cil_tmp191 = __cil_tmp190 + 28;
2852#line 758
2853 __cil_tmp192 = *((unsigned int *)__cil_tmp191);
2854#line 758
2855 *((unsigned int *)__cil_tmp188) = __cil_tmp192 + __cil_tmp189;
2856#line 759
2857 __cil_tmp193 = (unsigned long )db;
2858#line 759
2859 __cil_tmp194 = __cil_tmp193 + 56;
2860#line 759
2861 __cil_tmp195 = (unsigned long )db;
2862#line 759
2863 __cil_tmp196 = __cil_tmp195 + 56;
2864#line 759
2865 __cil_tmp197 = *((unsigned int *)__cil_tmp196);
2866#line 759
2867 *((unsigned int *)__cil_tmp194) = __cil_tmp197 + 1U;
2868#line 760
2869 __cil_tmp198 = (unsigned long )db;
2870#line 760
2871 __cil_tmp199 = __cil_tmp198 + 14;
2872#line 760
2873 __cil_tmp200 = (unsigned long )db;
2874#line 760
2875 __cil_tmp201 = __cil_tmp200 + 14;
2876#line 760
2877 __cil_tmp202 = *((unsigned short *)__cil_tmp201);
2878#line 760
2879 __cil_tmp203 = (int )__cil_tmp202;
2880#line 760
2881 __cil_tmp204 = __cil_tmp203 + 1;
2882#line 760
2883 *((unsigned short *)__cil_tmp199) = (unsigned short )__cil_tmp204;
2884#line 762
2885 if (bitno <= 31U) {
2886#line 764
2887 __cil_tmp205 = (unsigned long )db;
2888#line 764
2889 __cil_tmp206 = __cil_tmp205 + 32;
2890#line 764
2891 __cil_tmp207 = (unsigned long )db;
2892#line 764
2893 __cil_tmp208 = __cil_tmp207 + 32;
2894#line 764
2895 __cil_tmp209 = *((unsigned int *)__cil_tmp208);
2896#line 764
2897 *((unsigned int *)__cil_tmp206) = __cil_tmp209 + 1U;
2898 } else {
2899
2900 }
2901 {
2902#line 771
2903 tmp___9 = bsd_check(db);
2904 }
2905#line 771
2906 if (tmp___9 != 0) {
2907#line 773
2908 bitno = bitno - n_bits;
2909#line 773
2910 __cil_tmp210 = (int )bitno;
2911#line 773
2912 __cil_tmp211 = 256 << __cil_tmp210;
2913#line 773
2914 __cil_tmp212 = (unsigned long )__cil_tmp211;
2915#line 773
2916 accm = __cil_tmp212 | accm;
2917 ldv_14489:
2918#line 773
2919 olen = olen + 1;
2920 {
2921#line 773
2922 __cil_tmp213 = (unsigned char *)0;
2923#line 773
2924 __cil_tmp214 = (unsigned long )__cil_tmp213;
2925#line 773
2926 __cil_tmp215 = (unsigned long )wptr;
2927#line 773
2928 if (__cil_tmp215 != __cil_tmp214) {
2929#line 773
2930 tmp___8 = wptr;
2931#line 773
2932 wptr = wptr + 1;
2933#line 773
2934 __cil_tmp216 = accm >> 24;
2935#line 773
2936 *tmp___8 = (unsigned char )__cil_tmp216;
2937#line 773
2938 if (olen >= osize) {
2939#line 773
2940 wptr = (unsigned char *)0;
2941 } else {
2942
2943 }
2944 } else {
2945
2946 }
2947 }
2948#line 773
2949 accm = accm << 8;
2950#line 773
2951 bitno = bitno + 8U;
2952#line 773
2953 if (bitno <= 24U) {
2954#line 774
2955 goto ldv_14489;
2956 } else {
2957#line 776
2958 goto ldv_14490;
2959 }
2960 ldv_14490: ;
2961 } else {
2962
2963 }
2964#line 781
2965 if (bitno != 32U) {
2966#line 783
2967 olen = olen + 1;
2968 {
2969#line 783
2970 __cil_tmp217 = (unsigned char *)0;
2971#line 783
2972 __cil_tmp218 = (unsigned long )__cil_tmp217;
2973#line 783
2974 __cil_tmp219 = (unsigned long )wptr;
2975#line 783
2976 if (__cil_tmp219 != __cil_tmp218) {
2977#line 783
2978 tmp___10 = wptr;
2979#line 783
2980 wptr = wptr + 1;
2981#line 783
2982 __cil_tmp220 = bitno - 8U;
2983#line 783
2984 __cil_tmp221 = (int )__cil_tmp220;
2985#line 783
2986 __cil_tmp222 = 255 << __cil_tmp221;
2987#line 783
2988 __cil_tmp223 = (unsigned long )__cil_tmp222;
2989#line 783
2990 __cil_tmp224 = __cil_tmp223 | accm;
2991#line 783
2992 __cil_tmp225 = __cil_tmp224 >> 24;
2993#line 783
2994 *tmp___10 = (unsigned char )__cil_tmp225;
2995#line 783
2996 if (olen >= osize) {
2997#line 783
2998 wptr = (unsigned char *)0;
2999 } else {
3000
3001 }
3002 } else {
3003
3004 }
3005 }
3006 } else {
3007
3008 }
3009 {
3010#line 791
3011 __cil_tmp226 = (unsigned int )mxcode;
3012#line 791
3013 if (__cil_tmp226 <= max_ent) {
3014 {
3015#line 791
3016 __cil_tmp227 = (unsigned long )db;
3017#line 791
3018 __cil_tmp228 = __cil_tmp227 + 20;
3019#line 791
3020 __cil_tmp229 = *((unsigned int *)__cil_tmp228);
3021#line 791
3022 if (__cil_tmp229 > max_ent) {
3023#line 793
3024 __cil_tmp230 = (unsigned long )db;
3025#line 793
3026 __cil_tmp231 = __cil_tmp230 + 9;
3027#line 793
3028 __cil_tmp232 = (unsigned long )db;
3029#line 793
3030 __cil_tmp233 = __cil_tmp232 + 9;
3031#line 793
3032 __cil_tmp234 = *((unsigned char *)__cil_tmp233);
3033#line 793
3034 __cil_tmp235 = (int )__cil_tmp234;
3035#line 793
3036 __cil_tmp236 = __cil_tmp235 + 1;
3037#line 793
3038 *((unsigned char *)__cil_tmp231) = (unsigned char )__cil_tmp236;
3039 } else {
3040
3041 }
3042 }
3043 } else {
3044
3045 }
3046 }
3047 {
3048#line 797
3049 __cil_tmp237 = (unsigned char *)0;
3050#line 797
3051 __cil_tmp238 = (unsigned long )__cil_tmp237;
3052#line 797
3053 __cil_tmp239 = (unsigned long )wptr;
3054#line 797
3055 if (__cil_tmp239 == __cil_tmp238) {
3056#line 799
3057 __cil_tmp240 = (unsigned long )db;
3058#line 799
3059 __cil_tmp241 = __cil_tmp240 + 48;
3060#line 799
3061 __cil_tmp242 = (unsigned long )db;
3062#line 799
3063 __cil_tmp243 = __cil_tmp242 + 48;
3064#line 799
3065 __cil_tmp244 = *((unsigned int *)__cil_tmp243);
3066#line 799
3067 *((unsigned int *)__cil_tmp241) = __cil_tmp244 + 1U;
3068#line 800
3069 __cil_tmp245 = (unsigned long )db;
3070#line 800
3071 __cil_tmp246 = __cil_tmp245 + 52;
3072#line 800
3073 __cil_tmp247 = (unsigned int )isize;
3074#line 800
3075 __cil_tmp248 = (unsigned long )db;
3076#line 800
3077 __cil_tmp249 = __cil_tmp248 + 52;
3078#line 800
3079 __cil_tmp250 = *((unsigned int *)__cil_tmp249);
3080#line 800
3081 *((unsigned int *)__cil_tmp246) = __cil_tmp250 + __cil_tmp247;
3082#line 801
3083 olen = 0;
3084 } else {
3085#line 805
3086 __cil_tmp251 = (unsigned long )db;
3087#line 805
3088 __cil_tmp252 = __cil_tmp251 + 64;
3089#line 805
3090 __cil_tmp253 = (unsigned long )db;
3091#line 805
3092 __cil_tmp254 = __cil_tmp253 + 64;
3093#line 805
3094 __cil_tmp255 = *((unsigned int *)__cil_tmp254);
3095#line 805
3096 *((unsigned int *)__cil_tmp252) = __cil_tmp255 + 1U;
3097#line 806
3098 __cil_tmp256 = (unsigned long )db;
3099#line 806
3100 __cil_tmp257 = __cil_tmp256 + 68;
3101#line 806
3102 __cil_tmp258 = (unsigned int )olen;
3103#line 806
3104 __cil_tmp259 = (unsigned long )db;
3105#line 806
3106 __cil_tmp260 = __cil_tmp259 + 68;
3107#line 806
3108 __cil_tmp261 = *((unsigned int *)__cil_tmp260);
3109#line 806
3110 *((unsigned int *)__cil_tmp257) = __cil_tmp261 + __cil_tmp258;
3111 }
3112 }
3113#line 810
3114 return (olen);
3115}
3116}
3117#line 820 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
3118static void bsd_incomp(void *state , unsigned char *ibuf , int icnt )
3119{ unsigned char *__cil_tmp4 ;
3120
3121 {
3122 {
3123#line 822
3124 __cil_tmp4 = (unsigned char *)0;
3125#line 822
3126 bsd_compress(state, ibuf, __cil_tmp4, icnt, 0);
3127 }
3128#line 823
3129 return;
3130}
3131}
3132#line 842 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
3133static int bsd_decompress(void *state , unsigned char *ibuf , int isize , unsigned char *obuf ,
3134 int osize )
3135{ struct bsd_db *db ;
3136 unsigned int max_ent ;
3137 unsigned long accm ;
3138 unsigned int bitno ;
3139 unsigned int n_bits ;
3140 unsigned int tgtbitno ;
3141 struct bsd_dict *dictp ;
3142 int explen ;
3143 int seq ;
3144 unsigned int incode ;
3145 unsigned int oldcode ;
3146 unsigned int finchar ;
3147 unsigned char *p ;
3148 unsigned char *wptr ;
3149 int adrs ;
3150 int ctrl ;
3151 int ilen ;
3152 int codelen ;
3153 int extra ;
3154 unsigned char *tmp ;
3155 unsigned char *tmp___0 ;
3156 unsigned char *tmp___1 ;
3157 int tmp___2 ;
3158 unsigned char *tmp___3 ;
3159 struct bsd_dict *dictp2 ;
3160 unsigned char *tmp___4 ;
3161 struct bsd_dict *dictp2___0 ;
3162 struct bsd_dict *dictp3 ;
3163 unsigned short *lens1 ;
3164 unsigned short *lens2 ;
3165 unsigned long fcode ;
3166 int hval ;
3167 int disp ;
3168 int indx ;
3169 int tmp___5 ;
3170 unsigned long __cil_tmp41 ;
3171 unsigned long __cil_tmp42 ;
3172 unsigned long __cil_tmp43 ;
3173 unsigned long __cil_tmp44 ;
3174 unsigned char __cil_tmp45 ;
3175 unsigned char __cil_tmp46 ;
3176 __u8 *__cil_tmp47 ;
3177 __u8 __cil_tmp48 ;
3178 unsigned char *__cil_tmp49 ;
3179 unsigned char __cil_tmp50 ;
3180 int __cil_tmp51 ;
3181 unsigned char *__cil_tmp52 ;
3182 unsigned char __cil_tmp53 ;
3183 int __cil_tmp54 ;
3184 int __cil_tmp55 ;
3185 unsigned long __cil_tmp56 ;
3186 unsigned long __cil_tmp57 ;
3187 unsigned short __cil_tmp58 ;
3188 int __cil_tmp59 ;
3189 unsigned long __cil_tmp60 ;
3190 unsigned long __cil_tmp61 ;
3191 unsigned char __cil_tmp62 ;
3192 unsigned int __cil_tmp63 ;
3193 unsigned long __cil_tmp64 ;
3194 unsigned long __cil_tmp65 ;
3195 unsigned char __cil_tmp66 ;
3196 int __cil_tmp67 ;
3197 unsigned long __cil_tmp68 ;
3198 unsigned long __cil_tmp69 ;
3199 unsigned short __cil_tmp70 ;
3200 int __cil_tmp71 ;
3201 int __cil_tmp72 ;
3202 unsigned long __cil_tmp73 ;
3203 unsigned long __cil_tmp74 ;
3204 unsigned long __cil_tmp75 ;
3205 unsigned long __cil_tmp76 ;
3206 unsigned short __cil_tmp77 ;
3207 int __cil_tmp78 ;
3208 int __cil_tmp79 ;
3209 unsigned long __cil_tmp80 ;
3210 unsigned long __cil_tmp81 ;
3211 unsigned int __cil_tmp82 ;
3212 unsigned long __cil_tmp83 ;
3213 unsigned long __cil_tmp84 ;
3214 unsigned int __cil_tmp85 ;
3215 unsigned long __cil_tmp86 ;
3216 unsigned long __cil_tmp87 ;
3217 unsigned int __cil_tmp88 ;
3218 unsigned long __cil_tmp89 ;
3219 unsigned long __cil_tmp90 ;
3220 unsigned int __cil_tmp91 ;
3221 unsigned int __cil_tmp92 ;
3222 int __cil_tmp93 ;
3223 unsigned char __cil_tmp94 ;
3224 int __cil_tmp95 ;
3225 int __cil_tmp96 ;
3226 unsigned long __cil_tmp97 ;
3227 int __cil_tmp98 ;
3228 unsigned long __cil_tmp99 ;
3229 int __cil_tmp100 ;
3230 unsigned long __cil_tmp101 ;
3231 unsigned long __cil_tmp102 ;
3232 unsigned char __cil_tmp103 ;
3233 unsigned int __cil_tmp104 ;
3234 unsigned long __cil_tmp105 ;
3235 unsigned long __cil_tmp106 ;
3236 unsigned char __cil_tmp107 ;
3237 int __cil_tmp108 ;
3238 unsigned int __cil_tmp109 ;
3239 unsigned long __cil_tmp110 ;
3240 unsigned long __cil_tmp111 ;
3241 unsigned int __cil_tmp112 ;
3242 unsigned long __cil_tmp113 ;
3243 unsigned long __cil_tmp114 ;
3244 unsigned char __cil_tmp115 ;
3245 unsigned int __cil_tmp116 ;
3246 unsigned long __cil_tmp117 ;
3247 unsigned long __cil_tmp118 ;
3248 unsigned char __cil_tmp119 ;
3249 int __cil_tmp120 ;
3250 unsigned long __cil_tmp121 ;
3251 unsigned long __cil_tmp122 ;
3252 unsigned short __cil_tmp123 ;
3253 int __cil_tmp124 ;
3254 unsigned long __cil_tmp125 ;
3255 unsigned long __cil_tmp126 ;
3256 unsigned long __cil_tmp127 ;
3257 unsigned short *__cil_tmp128 ;
3258 unsigned short *__cil_tmp129 ;
3259 unsigned short __cil_tmp130 ;
3260 int __cil_tmp131 ;
3261 unsigned long __cil_tmp132 ;
3262 unsigned long __cil_tmp133 ;
3263 unsigned char __cil_tmp134 ;
3264 unsigned int __cil_tmp135 ;
3265 unsigned long __cil_tmp136 ;
3266 unsigned long __cil_tmp137 ;
3267 unsigned char __cil_tmp138 ;
3268 int __cil_tmp139 ;
3269 unsigned long __cil_tmp140 ;
3270 unsigned long __cil_tmp141 ;
3271 unsigned long __cil_tmp142 ;
3272 unsigned long __cil_tmp143 ;
3273 struct bsd_dict *__cil_tmp144 ;
3274 unsigned long __cil_tmp145 ;
3275 unsigned long __cil_tmp146 ;
3276 unsigned short __cil_tmp147 ;
3277 unsigned long __cil_tmp148 ;
3278 unsigned long __cil_tmp149 ;
3279 unsigned long __cil_tmp150 ;
3280 struct bsd_dict *__cil_tmp151 ;
3281 unsigned long __cil_tmp152 ;
3282 unsigned long __cil_tmp153 ;
3283 unsigned long __cil_tmp154 ;
3284 unsigned long __cil_tmp155 ;
3285 unsigned short __cil_tmp156 ;
3286 unsigned long __cil_tmp157 ;
3287 unsigned long __cil_tmp158 ;
3288 unsigned int __cil_tmp159 ;
3289 unsigned long __cil_tmp160 ;
3290 unsigned long __cil_tmp161 ;
3291 unsigned long __cil_tmp162 ;
3292 unsigned long __cil_tmp163 ;
3293 unsigned long __cil_tmp164 ;
3294 unsigned char __cil_tmp165 ;
3295 int __cil_tmp166 ;
3296 unsigned long __cil_tmp167 ;
3297 unsigned long __cil_tmp168 ;
3298 unsigned int __cil_tmp169 ;
3299 unsigned int __cil_tmp170 ;
3300 unsigned long __cil_tmp171 ;
3301 unsigned long __cil_tmp172 ;
3302 unsigned long __cil_tmp173 ;
3303 struct bsd_dict *__cil_tmp174 ;
3304 unsigned long __cil_tmp175 ;
3305 unsigned long __cil_tmp176 ;
3306 unsigned short __cil_tmp177 ;
3307 unsigned int __cil_tmp178 ;
3308 unsigned long __cil_tmp179 ;
3309 unsigned long __cil_tmp180 ;
3310 unsigned int __cil_tmp181 ;
3311 unsigned int __cil_tmp182 ;
3312 unsigned long __cil_tmp183 ;
3313 unsigned long __cil_tmp184 ;
3314 unsigned int __cil_tmp185 ;
3315 unsigned int __cil_tmp186 ;
3316 unsigned int __cil_tmp187 ;
3317 unsigned long __cil_tmp188 ;
3318 unsigned long __cil_tmp189 ;
3319 unsigned long __cil_tmp190 ;
3320 struct bsd_dict *__cil_tmp191 ;
3321 unsigned long __cil_tmp192 ;
3322 unsigned long __cil_tmp193 ;
3323 unsigned short __cil_tmp194 ;
3324 unsigned int __cil_tmp195 ;
3325 unsigned int __cil_tmp196 ;
3326 unsigned long __cil_tmp197 ;
3327 unsigned long __cil_tmp198 ;
3328 unsigned long __cil_tmp199 ;
3329 struct bsd_dict *__cil_tmp200 ;
3330 unsigned long __cil_tmp201 ;
3331 unsigned long __cil_tmp202 ;
3332 unsigned short __cil_tmp203 ;
3333 unsigned long __cil_tmp204 ;
3334 unsigned long __cil_tmp205 ;
3335 unsigned long __cil_tmp206 ;
3336 struct bsd_dict *__cil_tmp207 ;
3337 unsigned long __cil_tmp208 ;
3338 unsigned long __cil_tmp209 ;
3339 unsigned short __cil_tmp210 ;
3340 unsigned int __cil_tmp211 ;
3341 unsigned long __cil_tmp212 ;
3342 unsigned long __cil_tmp213 ;
3343 unsigned long __cil_tmp214 ;
3344 unsigned long __cil_tmp215 ;
3345 unsigned long __cil_tmp216 ;
3346 unsigned long __cil_tmp217 ;
3347 unsigned long __cil_tmp218 ;
3348 unsigned long __cil_tmp219 ;
3349 unsigned long __cil_tmp220 ;
3350 unsigned long __cil_tmp221 ;
3351 unsigned long __cil_tmp222 ;
3352 unsigned short *__cil_tmp223 ;
3353 unsigned long __cil_tmp224 ;
3354 unsigned long __cil_tmp225 ;
3355 unsigned long __cil_tmp226 ;
3356 unsigned short *__cil_tmp227 ;
3357 unsigned short __cil_tmp228 ;
3358 unsigned int __cil_tmp229 ;
3359 unsigned int __cil_tmp230 ;
3360 int __cil_tmp231 ;
3361 int __cil_tmp232 ;
3362 int __cil_tmp233 ;
3363 unsigned int __cil_tmp234 ;
3364 unsigned long __cil_tmp235 ;
3365 unsigned long __cil_tmp236 ;
3366 unsigned int __cil_tmp237 ;
3367 unsigned long __cil_tmp238 ;
3368 unsigned long __cil_tmp239 ;
3369 unsigned long __cil_tmp240 ;
3370 unsigned long __cil_tmp241 ;
3371 unsigned long __cil_tmp242 ;
3372 unsigned long __cil_tmp243 ;
3373 unsigned int __cil_tmp244 ;
3374 unsigned long __cil_tmp245 ;
3375 unsigned long __cil_tmp246 ;
3376 unsigned long __cil_tmp247 ;
3377 unsigned long __cil_tmp248 ;
3378 unsigned int __cil_tmp249 ;
3379 unsigned long __cil_tmp250 ;
3380 unsigned long __cil_tmp251 ;
3381 unsigned int __cil_tmp252 ;
3382 unsigned long __cil_tmp253 ;
3383 unsigned long __cil_tmp254 ;
3384 unsigned int __cil_tmp255 ;
3385 unsigned int __cil_tmp256 ;
3386 unsigned long __cil_tmp257 ;
3387 unsigned long __cil_tmp258 ;
3388 unsigned int __cil_tmp259 ;
3389 unsigned long __cil_tmp260 ;
3390 unsigned long __cil_tmp261 ;
3391 unsigned int __cil_tmp262 ;
3392 unsigned long __cil_tmp263 ;
3393 unsigned long __cil_tmp264 ;
3394 unsigned char __cil_tmp265 ;
3395 unsigned int __cil_tmp266 ;
3396 unsigned long __cil_tmp267 ;
3397 unsigned long __cil_tmp268 ;
3398 unsigned char __cil_tmp269 ;
3399 int __cil_tmp270 ;
3400 unsigned long __cil_tmp271 ;
3401 unsigned long __cil_tmp272 ;
3402 unsigned short __cil_tmp273 ;
3403 int __cil_tmp274 ;
3404 int __cil_tmp275 ;
3405
3406 {
3407#line 865
3408 db = (struct bsd_db *)state;
3409#line 866
3410 __cil_tmp41 = (unsigned long )db;
3411#line 866
3412 __cil_tmp42 = __cil_tmp41 + 24;
3413#line 866
3414 max_ent = *((unsigned int *)__cil_tmp42);
3415#line 867
3416 accm = 0UL;
3417#line 868
3418 bitno = 32U;
3419#line 869
3420 __cil_tmp43 = (unsigned long )db;
3421#line 869
3422 __cil_tmp44 = __cil_tmp43 + 9;
3423#line 869
3424 __cil_tmp45 = *((unsigned char *)__cil_tmp44);
3425#line 869
3426 n_bits = (unsigned int )__cil_tmp45;
3427#line 870
3428 tgtbitno = 32U - n_bits;
3429#line 877
3430 __cil_tmp46 = *ibuf;
3431#line 877
3432 adrs = (int )__cil_tmp46;
3433#line 878
3434 __cil_tmp47 = ibuf + 1UL;
3435#line 878
3436 __cil_tmp48 = *__cil_tmp47;
3437#line 878
3438 ctrl = (int )__cil_tmp48;
3439#line 880
3440 __cil_tmp49 = ibuf + 5UL;
3441#line 880
3442 __cil_tmp50 = *__cil_tmp49;
3443#line 880
3444 __cil_tmp51 = (int )__cil_tmp50;
3445#line 880
3446 __cil_tmp52 = ibuf + 4UL;
3447#line 880
3448 __cil_tmp53 = *__cil_tmp52;
3449#line 880
3450 __cil_tmp54 = (int )__cil_tmp53;
3451#line 880
3452 __cil_tmp55 = __cil_tmp54 << 8;
3453#line 880
3454 seq = __cil_tmp55 + __cil_tmp51;
3455#line 882
3456 ibuf = ibuf + 6UL;
3457#line 883
3458 ilen = isize + -6;
3459 {
3460#line 890
3461 __cil_tmp56 = (unsigned long )db;
3462#line 890
3463 __cil_tmp57 = __cil_tmp56 + 14;
3464#line 890
3465 __cil_tmp58 = *((unsigned short *)__cil_tmp57);
3466#line 890
3467 __cil_tmp59 = (int )__cil_tmp58;
3468#line 890
3469 if (__cil_tmp59 != seq) {
3470 {
3471#line 892
3472 __cil_tmp60 = (unsigned long )db;
3473#line 892
3474 __cil_tmp61 = __cil_tmp60 + 11;
3475#line 892
3476 __cil_tmp62 = *((unsigned char *)__cil_tmp61);
3477#line 892
3478 __cil_tmp63 = (unsigned int )__cil_tmp62;
3479#line 892
3480 if (__cil_tmp63 != 0U) {
3481 {
3482#line 894
3483 __cil_tmp64 = (unsigned long )db;
3484#line 894
3485 __cil_tmp65 = __cil_tmp64 + 12;
3486#line 894
3487 __cil_tmp66 = *((unsigned char *)__cil_tmp65);
3488#line 894
3489 __cil_tmp67 = (int )__cil_tmp66;
3490#line 894
3491 __cil_tmp68 = (unsigned long )db;
3492#line 894
3493 __cil_tmp69 = __cil_tmp68 + 14;
3494#line 894
3495 __cil_tmp70 = *((unsigned short *)__cil_tmp69);
3496#line 894
3497 __cil_tmp71 = (int )__cil_tmp70;
3498#line 894
3499 __cil_tmp72 = __cil_tmp71 + -1;
3500#line 894
3501 printk("bsd_decomp%d: bad sequence # %d, expected %d\n", __cil_tmp67, seq, __cil_tmp72);
3502 }
3503 } else {
3504
3505 }
3506 }
3507#line 897
3508 return (-1);
3509 } else {
3510
3511 }
3512 }
3513#line 900
3514 __cil_tmp73 = (unsigned long )db;
3515#line 900
3516 __cil_tmp74 = __cil_tmp73 + 14;
3517#line 900
3518 __cil_tmp75 = (unsigned long )db;
3519#line 900
3520 __cil_tmp76 = __cil_tmp75 + 14;
3521#line 900
3522 __cil_tmp77 = *((unsigned short *)__cil_tmp76);
3523#line 900
3524 __cil_tmp78 = (int )__cil_tmp77;
3525#line 900
3526 __cil_tmp79 = __cil_tmp78 + 1;
3527#line 900
3528 *((unsigned short *)__cil_tmp74) = (unsigned short )__cil_tmp79;
3529#line 901
3530 __cil_tmp80 = (unsigned long )db;
3531#line 901
3532 __cil_tmp81 = __cil_tmp80 + 32;
3533#line 901
3534 __cil_tmp82 = (unsigned int )ilen;
3535#line 901
3536 __cil_tmp83 = (unsigned long )db;
3537#line 901
3538 __cil_tmp84 = __cil_tmp83 + 32;
3539#line 901
3540 __cil_tmp85 = *((unsigned int *)__cil_tmp84);
3541#line 901
3542 *((unsigned int *)__cil_tmp81) = __cil_tmp85 + __cil_tmp82;
3543#line 908
3544 wptr = obuf;
3545#line 909
3546 tmp = wptr;
3547#line 909
3548 wptr = wptr + 1;
3549#line 909
3550 *tmp = (unsigned char )adrs;
3551#line 910
3552 tmp___0 = wptr;
3553#line 910
3554 wptr = wptr + 1;
3555#line 910
3556 *tmp___0 = (unsigned char )ctrl;
3557#line 911
3558 tmp___1 = wptr;
3559#line 911
3560 wptr = wptr + 1;
3561#line 911
3562 *tmp___1 = (unsigned char)0;
3563#line 913
3564 oldcode = 256U;
3565#line 914
3566 explen = 3;
3567 ldv_14538:
3568#line 923
3569 tmp___2 = ilen;
3570#line 923
3571 ilen = ilen - 1;
3572#line 923
3573 if (tmp___2 <= 0) {
3574#line 925
3575 __cil_tmp86 = (unsigned long )db;
3576#line 925
3577 __cil_tmp87 = __cil_tmp86 + 28;
3578#line 925
3579 __cil_tmp88 = (unsigned int )explen;
3580#line 925
3581 __cil_tmp89 = (unsigned long )db;
3582#line 925
3583 __cil_tmp90 = __cil_tmp89 + 28;
3584#line 925
3585 __cil_tmp91 = *((unsigned int *)__cil_tmp90);
3586#line 925
3587 __cil_tmp92 = __cil_tmp91 + __cil_tmp88;
3588#line 925
3589 *((unsigned int *)__cil_tmp87) = __cil_tmp92 + 4294967293U;
3590#line 926
3591 goto ldv_14522;
3592 } else {
3593
3594 }
3595#line 935
3596 bitno = bitno - 8U;
3597#line 936
3598 tmp___3 = ibuf;
3599#line 936
3600 ibuf = ibuf + 1;
3601#line 936
3602 __cil_tmp93 = (int )bitno;
3603#line 936
3604 __cil_tmp94 = *tmp___3;
3605#line 936
3606 __cil_tmp95 = (int )__cil_tmp94;
3607#line 936
3608 __cil_tmp96 = __cil_tmp95 << __cil_tmp93;
3609#line 936
3610 __cil_tmp97 = (unsigned long )__cil_tmp96;
3611#line 936
3612 accm = __cil_tmp97 | accm;
3613#line 937
3614 if (tgtbitno < bitno) {
3615#line 939
3616 goto ldv_14523;
3617 } else {
3618
3619 }
3620#line 942
3621 __cil_tmp98 = (int )tgtbitno;
3622#line 942
3623 __cil_tmp99 = accm >> __cil_tmp98;
3624#line 942
3625 incode = (unsigned int )__cil_tmp99;
3626#line 943
3627 __cil_tmp100 = (int )n_bits;
3628#line 943
3629 accm = accm << __cil_tmp100;
3630#line 944
3631 bitno = bitno + n_bits;
3632#line 950
3633 if (incode == 256U) {
3634#line 952
3635 if (ilen > 0) {
3636 {
3637#line 954
3638 __cil_tmp101 = (unsigned long )db;
3639#line 954
3640 __cil_tmp102 = __cil_tmp101 + 11;
3641#line 954
3642 __cil_tmp103 = *((unsigned char *)__cil_tmp102);
3643#line 954
3644 __cil_tmp104 = (unsigned int )__cil_tmp103;
3645#line 954
3646 if (__cil_tmp104 != 0U) {
3647 {
3648#line 956
3649 __cil_tmp105 = (unsigned long )db;
3650#line 956
3651 __cil_tmp106 = __cil_tmp105 + 12;
3652#line 956
3653 __cil_tmp107 = *((unsigned char *)__cil_tmp106);
3654#line 956
3655 __cil_tmp108 = (int )__cil_tmp107;
3656#line 956
3657 printk("bsd_decomp%d: bad CLEAR\n", __cil_tmp108);
3658 }
3659 } else {
3660
3661 }
3662 }
3663#line 958
3664 return (-2);
3665 } else {
3666
3667 }
3668 {
3669#line 961
3670 bsd_clear(db);
3671 }
3672#line 962
3673 goto ldv_14522;
3674 } else {
3675
3676 }
3677 {
3678#line 965
3679 __cil_tmp109 = max_ent + 2U;
3680#line 965
3681 if (__cil_tmp109 < incode) {
3682#line 965
3683 goto _L;
3684 } else {
3685 {
3686#line 965
3687 __cil_tmp110 = (unsigned long )db;
3688#line 965
3689 __cil_tmp111 = __cil_tmp110 + 20;
3690#line 965
3691 __cil_tmp112 = *((unsigned int *)__cil_tmp111);
3692#line 965
3693 if (__cil_tmp112 < incode) {
3694#line 965
3695 goto _L;
3696 } else
3697#line 965
3698 if (incode > max_ent) {
3699#line 965
3700 if (oldcode == 256U) {
3701 _L:
3702 {
3703#line 968
3704 __cil_tmp113 = (unsigned long )db;
3705#line 968
3706 __cil_tmp114 = __cil_tmp113 + 11;
3707#line 968
3708 __cil_tmp115 = *((unsigned char *)__cil_tmp114);
3709#line 968
3710 __cil_tmp116 = (unsigned int )__cil_tmp115;
3711#line 968
3712 if (__cil_tmp116 != 0U) {
3713 {
3714#line 970
3715 __cil_tmp117 = (unsigned long )db;
3716#line 970
3717 __cil_tmp118 = __cil_tmp117 + 12;
3718#line 970
3719 __cil_tmp119 = *((unsigned char *)__cil_tmp118);
3720#line 970
3721 __cil_tmp120 = (int )__cil_tmp119;
3722#line 970
3723 printk("bsd_decomp%d: bad code 0x%x oldcode=0x%x ", __cil_tmp120, incode,
3724 oldcode);
3725#line 972
3726 __cil_tmp121 = (unsigned long )db;
3727#line 972
3728 __cil_tmp122 = __cil_tmp121 + 14;
3729#line 972
3730 __cil_tmp123 = *((unsigned short *)__cil_tmp122);
3731#line 972
3732 __cil_tmp124 = (int )__cil_tmp123;
3733#line 972
3734 printk("max_ent=0x%x explen=%d seqno=%d\n", max_ent, explen, __cil_tmp124);
3735 }
3736 } else {
3737
3738 }
3739 }
3740#line 975
3741 return (-2);
3742 } else {
3743
3744 }
3745 } else {
3746
3747 }
3748 }
3749 }
3750 }
3751#line 979
3752 if (incode > max_ent) {
3753#line 981
3754 finchar = oldcode;
3755#line 982
3756 extra = 1;
3757 } else {
3758#line 986
3759 finchar = incode;
3760#line 987
3761 extra = 0;
3762 }
3763#line 990
3764 __cil_tmp125 = (unsigned long )finchar;
3765#line 990
3766 __cil_tmp126 = (unsigned long )db;
3767#line 990
3768 __cil_tmp127 = __cil_tmp126 + 72;
3769#line 990
3770 __cil_tmp128 = *((unsigned short **)__cil_tmp127);
3771#line 990
3772 __cil_tmp129 = __cil_tmp128 + __cil_tmp125;
3773#line 990
3774 __cil_tmp130 = *__cil_tmp129;
3775#line 990
3776 codelen = (int )__cil_tmp130;
3777#line 991
3778 __cil_tmp131 = codelen + extra;
3779#line 991
3780 explen = __cil_tmp131 + explen;
3781#line 992
3782 if (explen > osize) {
3783 {
3784#line 994
3785 __cil_tmp132 = (unsigned long )db;
3786#line 994
3787 __cil_tmp133 = __cil_tmp132 + 11;
3788#line 994
3789 __cil_tmp134 = *((unsigned char *)__cil_tmp133);
3790#line 994
3791 __cil_tmp135 = (unsigned int )__cil_tmp134;
3792#line 994
3793 if (__cil_tmp135 != 0U) {
3794 {
3795#line 996
3796 __cil_tmp136 = (unsigned long )db;
3797#line 996
3798 __cil_tmp137 = __cil_tmp136 + 12;
3799#line 996
3800 __cil_tmp138 = *((unsigned char *)__cil_tmp137);
3801#line 996
3802 __cil_tmp139 = (int )__cil_tmp138;
3803#line 996
3804 printk("bsd_decomp%d: ran out of mru\n", __cil_tmp139);
3805 }
3806 } else {
3807
3808 }
3809 }
3810#line 1002
3811 return (-2);
3812 } else {
3813
3814 }
3815#line 1009
3816 __cil_tmp140 = (unsigned long )codelen;
3817#line 1009
3818 wptr = wptr + __cil_tmp140;
3819#line 1010
3820 p = wptr;
3821#line 1011
3822 goto ldv_14526;
3823 ldv_14525:
3824#line 1013
3825 __cil_tmp141 = (unsigned long )finchar;
3826#line 1013
3827 __cil_tmp142 = (unsigned long )db;
3828#line 1013
3829 __cil_tmp143 = __cil_tmp142 + 80;
3830#line 1013
3831 __cil_tmp144 = *((struct bsd_dict **)__cil_tmp143);
3832#line 1013
3833 dictp2 = __cil_tmp144 + __cil_tmp141;
3834#line 1015
3835 __cil_tmp145 = (unsigned long )dictp2;
3836#line 1015
3837 __cil_tmp146 = __cil_tmp145 + 10;
3838#line 1015
3839 __cil_tmp147 = *((unsigned short *)__cil_tmp146);
3840#line 1015
3841 __cil_tmp148 = (unsigned long )__cil_tmp147;
3842#line 1015
3843 __cil_tmp149 = (unsigned long )db;
3844#line 1015
3845 __cil_tmp150 = __cil_tmp149 + 80;
3846#line 1015
3847 __cil_tmp151 = *((struct bsd_dict **)__cil_tmp150);
3848#line 1015
3849 dictp = __cil_tmp151 + __cil_tmp148;
3850#line 1040
3851 p = p - 1;
3852#line 1040
3853 __cil_tmp152 = 0 + 2;
3854#line 1040
3855 __cil_tmp153 = 0 + __cil_tmp152;
3856#line 1040
3857 __cil_tmp154 = (unsigned long )dictp;
3858#line 1040
3859 __cil_tmp155 = __cil_tmp154 + __cil_tmp153;
3860#line 1040
3861 *p = *((unsigned char *)__cil_tmp155);
3862#line 1041
3863 __cil_tmp156 = *((unsigned short *)dictp);
3864#line 1041
3865 finchar = (unsigned int )__cil_tmp156;
3866 ldv_14526: ;
3867#line 1011
3868 if (finchar > 255U) {
3869#line 1012
3870 goto ldv_14525;
3871 } else {
3872#line 1014
3873 goto ldv_14527;
3874 }
3875 ldv_14527:
3876#line 1043
3877 p = p - 1;
3878#line 1043
3879 *p = (unsigned char )finchar;
3880#line 1053
3881 if (extra != 0) {
3882#line 1055
3883 tmp___4 = wptr;
3884#line 1055
3885 wptr = wptr + 1;
3886#line 1055
3887 *tmp___4 = (unsigned char )finchar;
3888 } else {
3889
3890 }
3891#line 1066
3892 if (oldcode != 256U) {
3893 {
3894#line 1066
3895 __cil_tmp157 = (unsigned long )db;
3896#line 1066
3897 __cil_tmp158 = __cil_tmp157 + 20;
3898#line 1066
3899 __cil_tmp159 = *((unsigned int *)__cil_tmp158);
3900#line 1066
3901 if (__cil_tmp159 > max_ent) {
3902#line 1073
3903 __cil_tmp160 = (unsigned long )oldcode;
3904#line 1073
3905 __cil_tmp161 = (unsigned long )finchar;
3906#line 1073
3907 __cil_tmp162 = __cil_tmp161 << 16;
3908#line 1073
3909 fcode = __cil_tmp162 + __cil_tmp160;
3910#line 1074
3911 __cil_tmp163 = (unsigned long )db;
3912#line 1074
3913 __cil_tmp164 = __cil_tmp163 + 8;
3914#line 1074
3915 __cil_tmp165 = *((unsigned char *)__cil_tmp164);
3916#line 1074
3917 __cil_tmp166 = (int )__cil_tmp165;
3918#line 1074
3919 __cil_tmp167 = (unsigned long )finchar;
3920#line 1074
3921 __cil_tmp168 = __cil_tmp167 << __cil_tmp166;
3922#line 1074
3923 __cil_tmp169 = (unsigned int )__cil_tmp168;
3924#line 1074
3925 __cil_tmp170 = __cil_tmp169 ^ oldcode;
3926#line 1074
3927 hval = (int )__cil_tmp170;
3928#line 1075
3929 __cil_tmp171 = (unsigned long )hval;
3930#line 1075
3931 __cil_tmp172 = (unsigned long )db;
3932#line 1075
3933 __cil_tmp173 = __cil_tmp172 + 80;
3934#line 1075
3935 __cil_tmp174 = *((struct bsd_dict **)__cil_tmp173);
3936#line 1075
3937 dictp = __cil_tmp174 + __cil_tmp171;
3938 {
3939#line 1078
3940 __cil_tmp175 = (unsigned long )dictp;
3941#line 1078
3942 __cil_tmp176 = __cil_tmp175 + 8;
3943#line 1078
3944 __cil_tmp177 = *((unsigned short *)__cil_tmp176);
3945#line 1078
3946 __cil_tmp178 = (unsigned int )__cil_tmp177;
3947#line 1078
3948 if (__cil_tmp178 < max_ent) {
3949#line 1080
3950 if (hval != 0) {
3951#line 1080
3952 disp = hval;
3953 } else {
3954#line 1080
3955 disp = 1;
3956 }
3957 ldv_14536:
3958#line 1083
3959 hval = hval + disp;
3960 {
3961#line 1084
3962 __cil_tmp179 = (unsigned long )db;
3963#line 1084
3964 __cil_tmp180 = __cil_tmp179 + 4;
3965#line 1084
3966 __cil_tmp181 = *((unsigned int *)__cil_tmp180);
3967#line 1084
3968 __cil_tmp182 = (unsigned int )hval;
3969#line 1084
3970 if (__cil_tmp182 >= __cil_tmp181) {
3971#line 1086
3972 __cil_tmp183 = (unsigned long )db;
3973#line 1086
3974 __cil_tmp184 = __cil_tmp183 + 4;
3975#line 1086
3976 __cil_tmp185 = *((unsigned int *)__cil_tmp184);
3977#line 1086
3978 __cil_tmp186 = (unsigned int )hval;
3979#line 1086
3980 __cil_tmp187 = __cil_tmp186 - __cil_tmp185;
3981#line 1086
3982 hval = (int )__cil_tmp187;
3983 } else {
3984
3985 }
3986 }
3987#line 1088
3988 __cil_tmp188 = (unsigned long )hval;
3989#line 1088
3990 __cil_tmp189 = (unsigned long )db;
3991#line 1088
3992 __cil_tmp190 = __cil_tmp189 + 80;
3993#line 1088
3994 __cil_tmp191 = *((struct bsd_dict **)__cil_tmp190);
3995#line 1088
3996 dictp = __cil_tmp191 + __cil_tmp188;
3997 {
3998#line 1090
3999 __cil_tmp192 = (unsigned long )dictp;
4000#line 1090
4001 __cil_tmp193 = __cil_tmp192 + 8;
4002#line 1090
4003 __cil_tmp194 = *((unsigned short *)__cil_tmp193);
4004#line 1090
4005 __cil_tmp195 = (unsigned int )__cil_tmp194;
4006#line 1090
4007 if (__cil_tmp195 < max_ent) {
4008#line 1091
4009 goto ldv_14536;
4010 } else {
4011#line 1093
4012 goto ldv_14537;
4013 }
4014 }
4015 ldv_14537: ;
4016 } else {
4017
4018 }
4019 }
4020#line 1098
4021 __cil_tmp196 = max_ent + 1U;
4022#line 1098
4023 __cil_tmp197 = (unsigned long )__cil_tmp196;
4024#line 1098
4025 __cil_tmp198 = (unsigned long )db;
4026#line 1098
4027 __cil_tmp199 = __cil_tmp198 + 80;
4028#line 1098
4029 __cil_tmp200 = *((struct bsd_dict **)__cil_tmp199);
4030#line 1098
4031 dictp2___0 = __cil_tmp200 + __cil_tmp197;
4032#line 1099
4033 __cil_tmp201 = (unsigned long )dictp2___0;
4034#line 1099
4035 __cil_tmp202 = __cil_tmp201 + 10;
4036#line 1099
4037 __cil_tmp203 = *((unsigned short *)__cil_tmp202);
4038#line 1099
4039 indx = (int )__cil_tmp203;
4040#line 1100
4041 __cil_tmp204 = (unsigned long )indx;
4042#line 1100
4043 __cil_tmp205 = (unsigned long )db;
4044#line 1100
4045 __cil_tmp206 = __cil_tmp205 + 80;
4046#line 1100
4047 __cil_tmp207 = *((struct bsd_dict **)__cil_tmp206);
4048#line 1100
4049 dictp3 = __cil_tmp207 + __cil_tmp204;
4050 {
4051#line 1102
4052 __cil_tmp208 = (unsigned long )dictp3;
4053#line 1102
4054 __cil_tmp209 = __cil_tmp208 + 8;
4055#line 1102
4056 __cil_tmp210 = *((unsigned short *)__cil_tmp209);
4057#line 1102
4058 __cil_tmp211 = (unsigned int )__cil_tmp210;
4059#line 1102
4060 if (__cil_tmp211 == max_ent) {
4061#line 1104
4062 __cil_tmp212 = (unsigned long )dictp3;
4063#line 1104
4064 __cil_tmp213 = __cil_tmp212 + 8;
4065#line 1104
4066 *((unsigned short *)__cil_tmp213) = (unsigned short)32767;
4067 } else {
4068
4069 }
4070 }
4071#line 1107
4072 __cil_tmp214 = (unsigned long )dictp2___0;
4073#line 1107
4074 __cil_tmp215 = __cil_tmp214 + 10;
4075#line 1107
4076 *((unsigned short *)__cil_tmp215) = (unsigned short )hval;
4077#line 1108
4078 __cil_tmp216 = (unsigned long )dictp;
4079#line 1108
4080 __cil_tmp217 = __cil_tmp216 + 8;
4081#line 1108
4082 *((unsigned short *)__cil_tmp217) = (unsigned short )max_ent;
4083#line 1109
4084 *((unsigned long *)dictp) = fcode;
4085#line 1110
4086 max_ent = max_ent + 1U;
4087#line 1110
4088 __cil_tmp218 = (unsigned long )db;
4089#line 1110
4090 __cil_tmp219 = __cil_tmp218 + 24;
4091#line 1110
4092 *((unsigned int *)__cil_tmp219) = max_ent;
4093#line 1113
4094 __cil_tmp220 = (unsigned long )max_ent;
4095#line 1113
4096 __cil_tmp221 = (unsigned long )db;
4097#line 1113
4098 __cil_tmp222 = __cil_tmp221 + 72;
4099#line 1113
4100 __cil_tmp223 = *((unsigned short **)__cil_tmp222);
4101#line 1113
4102 lens1 = __cil_tmp223 + __cil_tmp220;
4103#line 1114
4104 __cil_tmp224 = (unsigned long )oldcode;
4105#line 1114
4106 __cil_tmp225 = (unsigned long )db;
4107#line 1114
4108 __cil_tmp226 = __cil_tmp225 + 72;
4109#line 1114
4110 __cil_tmp227 = *((unsigned short **)__cil_tmp226);
4111#line 1114
4112 lens2 = __cil_tmp227 + __cil_tmp224;
4113#line 1115
4114 __cil_tmp228 = *lens2;
4115#line 1115
4116 __cil_tmp229 = (unsigned int )__cil_tmp228;
4117#line 1115
4118 __cil_tmp230 = __cil_tmp229 + 1U;
4119#line 1115
4120 *lens1 = (unsigned short )__cil_tmp230;
4121 {
4122#line 1118
4123 __cil_tmp231 = (int )n_bits;
4124#line 1118
4125 __cil_tmp232 = 1 << __cil_tmp231;
4126#line 1118
4127 __cil_tmp233 = __cil_tmp232 + -1;
4128#line 1118
4129 __cil_tmp234 = (unsigned int )__cil_tmp233;
4130#line 1118
4131 if (__cil_tmp234 <= max_ent) {
4132 {
4133#line 1118
4134 __cil_tmp235 = (unsigned long )db;
4135#line 1118
4136 __cil_tmp236 = __cil_tmp235 + 20;
4137#line 1118
4138 __cil_tmp237 = *((unsigned int *)__cil_tmp236);
4139#line 1118
4140 if (__cil_tmp237 > max_ent) {
4141#line 1120
4142 n_bits = n_bits + 1U;
4143#line 1120
4144 __cil_tmp238 = (unsigned long )db;
4145#line 1120
4146 __cil_tmp239 = __cil_tmp238 + 9;
4147#line 1120
4148 *((unsigned char *)__cil_tmp239) = (unsigned char )n_bits;
4149#line 1121
4150 tgtbitno = 32U - n_bits;
4151 } else {
4152
4153 }
4154 }
4155 } else {
4156
4157 }
4158 }
4159 } else {
4160
4161 }
4162 }
4163 } else {
4164
4165 }
4166#line 1124
4167 oldcode = incode;
4168 ldv_14523: ;
4169#line 1125
4170 goto ldv_14538;
4171 ldv_14522:
4172 {
4173#line 1127
4174 __cil_tmp240 = (unsigned long )db;
4175#line 1127
4176 __cil_tmp241 = __cil_tmp240 + 64;
4177#line 1127
4178 __cil_tmp242 = (unsigned long )db;
4179#line 1127
4180 __cil_tmp243 = __cil_tmp242 + 64;
4181#line 1127
4182 __cil_tmp244 = *((unsigned int *)__cil_tmp243);
4183#line 1127
4184 *((unsigned int *)__cil_tmp241) = __cil_tmp244 + 1U;
4185#line 1128
4186 __cil_tmp245 = (unsigned long )db;
4187#line 1128
4188 __cil_tmp246 = __cil_tmp245 + 56;
4189#line 1128
4190 __cil_tmp247 = (unsigned long )db;
4191#line 1128
4192 __cil_tmp248 = __cil_tmp247 + 56;
4193#line 1128
4194 __cil_tmp249 = *((unsigned int *)__cil_tmp248);
4195#line 1128
4196 *((unsigned int *)__cil_tmp246) = __cil_tmp249 + 1U;
4197#line 1129
4198 __cil_tmp250 = (unsigned long )db;
4199#line 1129
4200 __cil_tmp251 = __cil_tmp250 + 68;
4201#line 1129
4202 __cil_tmp252 = (unsigned int )isize;
4203#line 1129
4204 __cil_tmp253 = (unsigned long )db;
4205#line 1129
4206 __cil_tmp254 = __cil_tmp253 + 68;
4207#line 1129
4208 __cil_tmp255 = *((unsigned int *)__cil_tmp254);
4209#line 1129
4210 __cil_tmp256 = __cil_tmp255 + __cil_tmp252;
4211#line 1129
4212 *((unsigned int *)__cil_tmp251) = __cil_tmp256 + 4294967290U;
4213#line 1130
4214 __cil_tmp257 = (unsigned long )db;
4215#line 1130
4216 __cil_tmp258 = __cil_tmp257 + 60;
4217#line 1130
4218 __cil_tmp259 = (unsigned int )explen;
4219#line 1130
4220 __cil_tmp260 = (unsigned long )db;
4221#line 1130
4222 __cil_tmp261 = __cil_tmp260 + 60;
4223#line 1130
4224 __cil_tmp262 = *((unsigned int *)__cil_tmp261);
4225#line 1130
4226 *((unsigned int *)__cil_tmp258) = __cil_tmp262 + __cil_tmp259;
4227#line 1132
4228 tmp___5 = bsd_check(db);
4229 }
4230#line 1132
4231 if (tmp___5 != 0) {
4232 {
4233#line 1134
4234 __cil_tmp263 = (unsigned long )db;
4235#line 1134
4236 __cil_tmp264 = __cil_tmp263 + 11;
4237#line 1134
4238 __cil_tmp265 = *((unsigned char *)__cil_tmp264);
4239#line 1134
4240 __cil_tmp266 = (unsigned int )__cil_tmp265;
4241#line 1134
4242 if (__cil_tmp266 != 0U) {
4243 {
4244#line 1136
4245 __cil_tmp267 = (unsigned long )db;
4246#line 1136
4247 __cil_tmp268 = __cil_tmp267 + 12;
4248#line 1136
4249 __cil_tmp269 = *((unsigned char *)__cil_tmp268);
4250#line 1136
4251 __cil_tmp270 = (int )__cil_tmp269;
4252#line 1136
4253 __cil_tmp271 = (unsigned long )db;
4254#line 1136
4255 __cil_tmp272 = __cil_tmp271 + 14;
4256#line 1136
4257 __cil_tmp273 = *((unsigned short *)__cil_tmp272);
4258#line 1136
4259 __cil_tmp274 = (int )__cil_tmp273;
4260#line 1136
4261 __cil_tmp275 = __cil_tmp274 + -1;
4262#line 1136
4263 printk("bsd_decomp%d: peer should have cleared dictionary on %d\n", __cil_tmp270,
4264 __cil_tmp275);
4265 }
4266 } else {
4267
4268 }
4269 }
4270 } else {
4271
4272 }
4273#line 1140
4274 return (explen);
4275}
4276}
4277#line 1147 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
4278static struct compressor ppp_bsd_compress =
4279#line 1147
4280 {21, & bsd_comp_alloc, & bsd_free, & bsd_comp_init, & bsd_reset, & bsd_compress,
4281 & bsd_comp_stats, & bsd_decomp_alloc, & bsd_free, & bsd_decomp_init, & bsd_reset,
4282 & bsd_decompress, & bsd_incomp, & bsd_comp_stats, & __this_module, 0U};
4283#line 1169 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
4284static int bsdcomp_init(void)
4285{ int answer ;
4286 int tmp ;
4287
4288 {
4289 {
4290#line 1171
4291 tmp = ppp_register_compressor(& ppp_bsd_compress);
4292#line 1171
4293 answer = tmp;
4294 }
4295#line 1172
4296 if (answer == 0) {
4297 {
4298#line 1173
4299 printk("<6>PPP BSD Compression module registered\n");
4300 }
4301 } else {
4302
4303 }
4304#line 1174
4305 return (answer);
4306}
4307}
4308#line 1177 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
4309static void bsdcomp_cleanup(void)
4310{
4311
4312 {
4313 {
4314#line 1179
4315 ppp_unregister_compressor(& ppp_bsd_compress);
4316 }
4317#line 1180
4318 return;
4319}
4320}
4321#line 1203
4322extern void ldv_check_final_state(void) ;
4323#line 1209
4324extern void ldv_initialize(void) ;
4325#line 1212
4326extern int __VERIFIER_nondet_int(void) ;
4327#line 1215 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
4328int LDV_IN_INTERRUPT ;
4329#line 1218 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
4330void main(void)
4331{ unsigned char *var_bsd_comp_alloc_6_p0 ;
4332 int var_bsd_comp_alloc_6_p1 ;
4333 void *var_bsd_free_4_p0 ;
4334 void *var_bsd_comp_init_9_p0 ;
4335 unsigned char *var_bsd_comp_init_9_p1 ;
4336 int var_bsd_comp_init_9_p2 ;
4337 int var_bsd_comp_init_9_p3 ;
4338 int var_bsd_comp_init_9_p4 ;
4339 int var_bsd_comp_init_9_p5 ;
4340 void *var_bsd_reset_3_p0 ;
4341 void *var_bsd_compress_13_p0 ;
4342 unsigned char *var_bsd_compress_13_p1 ;
4343 unsigned char *var_bsd_compress_13_p2 ;
4344 int var_bsd_compress_13_p3 ;
4345 int var_bsd_compress_13_p4 ;
4346 void *var_bsd_comp_stats_2_p0 ;
4347 struct compstat *var_group1 ;
4348 unsigned char *var_bsd_decomp_alloc_7_p0 ;
4349 int var_bsd_decomp_alloc_7_p1 ;
4350 void *var_bsd_decomp_init_10_p0 ;
4351 unsigned char *var_bsd_decomp_init_10_p1 ;
4352 int var_bsd_decomp_init_10_p2 ;
4353 int var_bsd_decomp_init_10_p3 ;
4354 int var_bsd_decomp_init_10_p4 ;
4355 int var_bsd_decomp_init_10_p5 ;
4356 int var_bsd_decomp_init_10_p6 ;
4357 void *var_bsd_decompress_15_p0 ;
4358 unsigned char *var_bsd_decompress_15_p1 ;
4359 int var_bsd_decompress_15_p2 ;
4360 unsigned char *var_bsd_decompress_15_p3 ;
4361 int var_bsd_decompress_15_p4 ;
4362 void *var_bsd_incomp_14_p0 ;
4363 unsigned char *var_bsd_incomp_14_p1 ;
4364 int var_bsd_incomp_14_p2 ;
4365 int tmp ;
4366 int tmp___0 ;
4367 int tmp___1 ;
4368
4369 {
4370 {
4371#line 2006
4372 LDV_IN_INTERRUPT = 1;
4373#line 2015
4374 ldv_initialize();
4375#line 2091
4376 tmp = bsdcomp_init();
4377 }
4378#line 2091
4379 if (tmp != 0) {
4380#line 2092
4381 goto ldv_final;
4382 } else {
4383
4384 }
4385#line 2096
4386 goto ldv_14619;
4387 ldv_14618:
4388 {
4389#line 2099
4390 tmp___0 = __VERIFIER_nondet_int();
4391 }
4392#line 2101
4393 if (tmp___0 == 0) {
4394#line 2101
4395 goto case_0;
4396 } else
4397#line 2189
4398 if (tmp___0 == 1) {
4399#line 2189
4400 goto case_1;
4401 } else
4402#line 2277
4403 if (tmp___0 == 2) {
4404#line 2277
4405 goto case_2;
4406 } else
4407#line 2365
4408 if (tmp___0 == 3) {
4409#line 2365
4410 goto case_3;
4411 } else
4412#line 2453
4413 if (tmp___0 == 4) {
4414#line 2453
4415 goto case_4;
4416 } else
4417#line 2515
4418 if (tmp___0 == 5) {
4419#line 2515
4420 goto case_5;
4421 } else
4422#line 2603
4423 if (tmp___0 == 6) {
4424#line 2603
4425 goto case_6;
4426 } else
4427#line 2691
4428 if (tmp___0 == 7) {
4429#line 2691
4430 goto case_7;
4431 } else
4432#line 2779
4433 if (tmp___0 == 8) {
4434#line 2779
4435 goto case_8;
4436 } else
4437#line 2859
4438 if (tmp___0 == 9) {
4439#line 2859
4440 goto case_9;
4441 } else {
4442 {
4443#line 2947
4444 goto switch_default;
4445#line 2099
4446 if (0) {
4447 case_0:
4448 {
4449#line 2138
4450 bsd_comp_alloc(var_bsd_comp_alloc_6_p0, var_bsd_comp_alloc_6_p1);
4451 }
4452#line 2188
4453 goto ldv_14607;
4454 case_1:
4455 {
4456#line 2226
4457 bsd_free(var_bsd_free_4_p0);
4458 }
4459#line 2276
4460 goto ldv_14607;
4461 case_2:
4462 {
4463#line 2316
4464 bsd_comp_init(var_bsd_comp_init_9_p0, var_bsd_comp_init_9_p1, var_bsd_comp_init_9_p2,
4465 var_bsd_comp_init_9_p3, var_bsd_comp_init_9_p4, var_bsd_comp_init_9_p5);
4466 }
4467#line 2364
4468 goto ldv_14607;
4469 case_3:
4470 {
4471#line 2402
4472 bsd_reset(var_bsd_reset_3_p0);
4473 }
4474#line 2452
4475 goto ldv_14607;
4476 case_4:
4477 {
4478#line 2499
4479 bsd_compress(var_bsd_compress_13_p0, var_bsd_compress_13_p1, var_bsd_compress_13_p2,
4480 var_bsd_compress_13_p3, var_bsd_compress_13_p4);
4481 }
4482#line 2514
4483 goto ldv_14607;
4484 case_5:
4485 {
4486#line 2552
4487 bsd_comp_stats(var_bsd_comp_stats_2_p0, var_group1);
4488 }
4489#line 2602
4490 goto ldv_14607;
4491 case_6:
4492 {
4493#line 2640
4494 bsd_decomp_alloc(var_bsd_decomp_alloc_7_p0, var_bsd_decomp_alloc_7_p1);
4495 }
4496#line 2690
4497 goto ldv_14607;
4498 case_7:
4499 {
4500#line 2730
4501 bsd_decomp_init(var_bsd_decomp_init_10_p0, var_bsd_decomp_init_10_p1, var_bsd_decomp_init_10_p2,
4502 var_bsd_decomp_init_10_p3, var_bsd_decomp_init_10_p4, var_bsd_decomp_init_10_p5,
4503 var_bsd_decomp_init_10_p6);
4504 }
4505#line 2778
4506 goto ldv_14607;
4507 case_8:
4508 {
4509#line 2851
4510 bsd_decompress(var_bsd_decompress_15_p0, var_bsd_decompress_15_p1, var_bsd_decompress_15_p2,
4511 var_bsd_decompress_15_p3, var_bsd_decompress_15_p4);
4512 }
4513#line 2858
4514 goto ldv_14607;
4515 case_9:
4516 {
4517#line 2931
4518 bsd_incomp(var_bsd_incomp_14_p0, var_bsd_incomp_14_p1, var_bsd_incomp_14_p2);
4519 }
4520#line 2946
4521 goto ldv_14607;
4522 switch_default: ;
4523#line 2947
4524 goto ldv_14607;
4525 } else {
4526 switch_break: ;
4527 }
4528 }
4529 }
4530 ldv_14607: ;
4531 ldv_14619:
4532 {
4533#line 2096
4534 tmp___1 = __VERIFIER_nondet_int();
4535 }
4536#line 2096
4537 if (tmp___1 != 0) {
4538#line 2097
4539 goto ldv_14618;
4540 } else {
4541#line 2099
4542 goto ldv_14620;
4543 }
4544 ldv_14620: ;
4545 {
4546#line 3029
4547 bsdcomp_cleanup();
4548 }
4549 ldv_final:
4550 {
4551#line 3032
4552 ldv_check_final_state();
4553 }
4554#line 3035
4555 return;
4556}
4557}
4558#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4559void ldv_blast_assert(void)
4560{
4561
4562 {
4563 ERROR: ;
4564#line 6
4565 goto ERROR;
4566}
4567}
4568#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4569extern int __VERIFIER_nondet_int(void) ;
4570#line 3056 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
4571int ldv_spin = 0;
4572#line 3060 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
4573void ldv_check_alloc_flags(gfp_t flags )
4574{
4575
4576 {
4577#line 3063
4578 if (ldv_spin != 0) {
4579#line 3063
4580 if (flags != 32U) {
4581 {
4582#line 3063
4583 ldv_blast_assert();
4584 }
4585 } else {
4586
4587 }
4588 } else {
4589
4590 }
4591#line 3066
4592 return;
4593}
4594}
4595#line 3066
4596extern struct page *ldv_some_page(void) ;
4597#line 3069 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
4598struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags )
4599{ struct page *tmp ;
4600
4601 {
4602#line 3072
4603 if (ldv_spin != 0) {
4604#line 3072
4605 if (flags != 32U) {
4606 {
4607#line 3072
4608 ldv_blast_assert();
4609 }
4610 } else {
4611
4612 }
4613 } else {
4614
4615 }
4616 {
4617#line 3074
4618 tmp = ldv_some_page();
4619 }
4620#line 3074
4621 return (tmp);
4622}
4623}
4624#line 3078 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
4625void ldv_check_alloc_nonatomic(void)
4626{
4627
4628 {
4629#line 3081
4630 if (ldv_spin != 0) {
4631 {
4632#line 3081
4633 ldv_blast_assert();
4634 }
4635 } else {
4636
4637 }
4638#line 3084
4639 return;
4640}
4641}
4642#line 3085 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
4643void ldv_spin_lock(void)
4644{
4645
4646 {
4647#line 3088
4648 ldv_spin = 1;
4649#line 3089
4650 return;
4651}
4652}
4653#line 3092 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
4654void ldv_spin_unlock(void)
4655{
4656
4657 {
4658#line 3095
4659 ldv_spin = 0;
4660#line 3096
4661 return;
4662}
4663}
4664#line 3099 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
4665int ldv_spin_trylock(void)
4666{ int is_lock ;
4667
4668 {
4669 {
4670#line 3104
4671 is_lock = __VERIFIER_nondet_int();
4672 }
4673#line 3106
4674 if (is_lock != 0) {
4675#line 3109
4676 return (0);
4677 } else {
4678#line 3114
4679 ldv_spin = 1;
4680#line 3116
4681 return (1);
4682 }
4683}
4684}
4685#line 3283 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
4686void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 )
4687{
4688
4689 {
4690 {
4691#line 3289
4692 ldv_check_alloc_flags(ldv_func_arg2);
4693#line 3291
4694 kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
4695 }
4696#line 3292
4697 return ((void *)0);
4698}
4699}
4700#line 3294 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
4701__inline static void *kzalloc(size_t size , gfp_t flags )
4702{ void *tmp ;
4703
4704 {
4705 {
4706#line 3300
4707 ldv_check_alloc_flags(flags);
4708#line 3301
4709 tmp = __VERIFIER_nondet_pointer();
4710 }
4711#line 3301
4712 return (tmp);
4713}
4714}
4715#line 3315 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
4716void *ldv_vmalloc_19(unsigned long ldv_func_arg1 )
4717{
4718
4719 {
4720 {
4721#line 3320
4722 ldv_check_alloc_nonatomic();
4723#line 3322
4724 vmalloc(ldv_func_arg1);
4725 }
4726#line 3323
4727 return ((void *)0);
4728}
4729}
4730#line 3325 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
4731void *ldv_vmalloc_20(unsigned long ldv_func_arg1 )
4732{
4733
4734 {
4735 {
4736#line 3330
4737 ldv_check_alloc_nonatomic();
4738#line 3332
4739 vmalloc(ldv_func_arg1);
4740 }
4741#line 3333
4742 return ((void *)0);
4743}
4744}