1
2
3
4#line 43 "include/asm-generic/int-ll64.h"
5typedef unsigned char u8;
6#line 46 "include/asm-generic/int-ll64.h"
7typedef unsigned short u16;
8#line 49 "include/asm-generic/int-ll64.h"
9typedef unsigned int u32;
10#line 52 "include/asm-generic/int-ll64.h"
11typedef unsigned long long u64;
12#line 14 "include/asm-generic/posix_types.h"
13typedef long __kernel_long_t;
14#line 15 "include/asm-generic/posix_types.h"
15typedef unsigned long __kernel_ulong_t;
16#line 75 "include/asm-generic/posix_types.h"
17typedef __kernel_ulong_t __kernel_size_t;
18#line 76 "include/asm-generic/posix_types.h"
19typedef __kernel_long_t __kernel_ssize_t;
20#line 91 "include/asm-generic/posix_types.h"
21typedef long long __kernel_loff_t;
22#line 27 "include/linux/types.h"
23typedef unsigned short umode_t;
24#line 38 "include/linux/types.h"
25typedef _Bool bool;
26#line 54 "include/linux/types.h"
27typedef __kernel_loff_t loff_t;
28#line 63 "include/linux/types.h"
29typedef __kernel_size_t size_t;
30#line 68 "include/linux/types.h"
31typedef __kernel_ssize_t ssize_t;
32#line 202 "include/linux/types.h"
33typedef unsigned int gfp_t;
34#line 206 "include/linux/types.h"
35typedef u64 phys_addr_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 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
54struct page;
55#line 58
56struct page;
57#line 290 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
58struct file;
59#line 290
60struct file;
61#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
62struct arch_spinlock;
63#line 327
64struct arch_spinlock;
65#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
66struct kmem_cache;
67#line 23 "include/asm-generic/atomic-long.h"
68typedef atomic64_t atomic_long_t;
69#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
70typedef u16 __ticket_t;
71#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
72typedef u32 __ticketpair_t;
73#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
74struct __raw_tickets {
75 __ticket_t head ;
76 __ticket_t tail ;
77};
78#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
79union __anonunion_ldv_5907_29 {
80 __ticketpair_t head_tail ;
81 struct __raw_tickets tickets ;
82};
83#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
84struct arch_spinlock {
85 union __anonunion_ldv_5907_29 ldv_5907 ;
86};
87#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
88typedef struct arch_spinlock arch_spinlock_t;
89#line 34 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
90struct lockdep_map;
91#line 34
92struct lockdep_map;
93#line 55 "include/linux/debug_locks.h"
94struct stack_trace {
95 unsigned int nr_entries ;
96 unsigned int max_entries ;
97 unsigned long *entries ;
98 int skip ;
99};
100#line 26 "include/linux/stacktrace.h"
101struct lockdep_subclass_key {
102 char __one_byte ;
103};
104#line 53 "include/linux/lockdep.h"
105struct lock_class_key {
106 struct lockdep_subclass_key subkeys[8U] ;
107};
108#line 59 "include/linux/lockdep.h"
109struct lock_class {
110 struct list_head hash_entry ;
111 struct list_head lock_entry ;
112 struct lockdep_subclass_key *key ;
113 unsigned int subclass ;
114 unsigned int dep_gen_id ;
115 unsigned long usage_mask ;
116 struct stack_trace usage_traces[13U] ;
117 struct list_head locks_after ;
118 struct list_head locks_before ;
119 unsigned int version ;
120 unsigned long ops ;
121 char const *name ;
122 int name_version ;
123 unsigned long contention_point[4U] ;
124 unsigned long contending_point[4U] ;
125};
126#line 144 "include/linux/lockdep.h"
127struct lockdep_map {
128 struct lock_class_key *key ;
129 struct lock_class *class_cache[2U] ;
130 char const *name ;
131 int cpu ;
132 unsigned long ip ;
133};
134#line 556 "include/linux/lockdep.h"
135struct raw_spinlock {
136 arch_spinlock_t raw_lock ;
137 unsigned int magic ;
138 unsigned int owner_cpu ;
139 void *owner ;
140 struct lockdep_map dep_map ;
141};
142#line 33 "include/linux/spinlock_types.h"
143struct __anonstruct_ldv_6122_33 {
144 u8 __padding[24U] ;
145 struct lockdep_map dep_map ;
146};
147#line 33 "include/linux/spinlock_types.h"
148union __anonunion_ldv_6123_32 {
149 struct raw_spinlock rlock ;
150 struct __anonstruct_ldv_6122_33 ldv_6122 ;
151};
152#line 33 "include/linux/spinlock_types.h"
153struct spinlock {
154 union __anonunion_ldv_6123_32 ldv_6123 ;
155};
156#line 76 "include/linux/spinlock_types.h"
157typedef struct spinlock spinlock_t;
158#line 18 "include/asm-generic/pci_iomap.h"
159struct vm_area_struct;
160#line 18
161struct vm_area_struct;
162#line 445 "include/linux/elf.h"
163struct sock;
164#line 445
165struct sock;
166#line 446
167struct kobject;
168#line 446
169struct kobject;
170#line 447
171enum kobj_ns_type {
172 KOBJ_NS_TYPE_NONE = 0,
173 KOBJ_NS_TYPE_NET = 1,
174 KOBJ_NS_TYPES = 2
175} ;
176#line 453 "include/linux/elf.h"
177struct kobj_ns_type_operations {
178 enum kobj_ns_type type ;
179 void *(*grab_current_ns)(void) ;
180 void const *(*netlink_ns)(struct sock * ) ;
181 void const *(*initial_ns)(void) ;
182 void (*drop_ns)(void * ) ;
183};
184#line 57 "include/linux/kobject_ns.h"
185struct attribute {
186 char const *name ;
187 umode_t mode ;
188 struct lock_class_key *key ;
189 struct lock_class_key skey ;
190};
191#line 62 "include/linux/sysfs.h"
192struct bin_attribute {
193 struct attribute attr ;
194 size_t size ;
195 void *private ;
196 ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
197 loff_t , size_t ) ;
198 ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
199 loff_t , size_t ) ;
200 int (*mmap)(struct file * , struct kobject * , struct bin_attribute * , struct vm_area_struct * ) ;
201};
202#line 98 "include/linux/sysfs.h"
203struct sysfs_ops {
204 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
205 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
206 void const *(*namespace)(struct kobject * , struct attribute const * ) ;
207};
208#line 117
209struct sysfs_dirent;
210#line 117
211struct sysfs_dirent;
212#line 182 "include/linux/sysfs.h"
213struct kref {
214 atomic_t refcount ;
215};
216#line 49 "include/linux/kobject.h"
217struct kset;
218#line 49
219struct kobj_type;
220#line 49 "include/linux/kobject.h"
221struct kobject {
222 char const *name ;
223 struct list_head entry ;
224 struct kobject *parent ;
225 struct kset *kset ;
226 struct kobj_type *ktype ;
227 struct sysfs_dirent *sd ;
228 struct kref kref ;
229 unsigned char state_initialized : 1 ;
230 unsigned char state_in_sysfs : 1 ;
231 unsigned char state_add_uevent_sent : 1 ;
232 unsigned char state_remove_uevent_sent : 1 ;
233 unsigned char uevent_suppress : 1 ;
234};
235#line 107 "include/linux/kobject.h"
236struct kobj_type {
237 void (*release)(struct kobject * ) ;
238 struct sysfs_ops const *sysfs_ops ;
239 struct attribute **default_attrs ;
240 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject * ) ;
241 void const *(*namespace)(struct kobject * ) ;
242};
243#line 115 "include/linux/kobject.h"
244struct kobj_uevent_env {
245 char *envp[32U] ;
246 int envp_idx ;
247 char buf[2048U] ;
248 int buflen ;
249};
250#line 122 "include/linux/kobject.h"
251struct kset_uevent_ops {
252 int (* const filter)(struct kset * , struct kobject * ) ;
253 char const *(* const name)(struct kset * , struct kobject * ) ;
254 int (* const uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
255};
256#line 139 "include/linux/kobject.h"
257struct kset {
258 struct list_head list ;
259 spinlock_t list_lock ;
260 struct kobject kobj ;
261 struct kset_uevent_ops const *uevent_ops ;
262};
263#line 88 "include/linux/kmemleak.h"
264struct kmem_cache_cpu {
265 void **freelist ;
266 unsigned long tid ;
267 struct page *page ;
268 struct page *partial ;
269 int node ;
270 unsigned int stat[26U] ;
271};
272#line 55 "include/linux/slub_def.h"
273struct kmem_cache_node {
274 spinlock_t list_lock ;
275 unsigned long nr_partial ;
276 struct list_head partial ;
277 atomic_long_t nr_slabs ;
278 atomic_long_t total_objects ;
279 struct list_head full ;
280};
281#line 66 "include/linux/slub_def.h"
282struct kmem_cache_order_objects {
283 unsigned long x ;
284};
285#line 76 "include/linux/slub_def.h"
286struct kmem_cache {
287 struct kmem_cache_cpu *cpu_slab ;
288 unsigned long flags ;
289 unsigned long min_partial ;
290 int size ;
291 int objsize ;
292 int offset ;
293 int cpu_partial ;
294 struct kmem_cache_order_objects oo ;
295 struct kmem_cache_order_objects max ;
296 struct kmem_cache_order_objects min ;
297 gfp_t allocflags ;
298 int refcount ;
299 void (*ctor)(void * ) ;
300 int inuse ;
301 int align ;
302 int reserved ;
303 char const *name ;
304 struct list_head list ;
305 struct kobject kobj ;
306 int remote_node_defrag_ratio ;
307 struct kmem_cache_node *node[1024U] ;
308};
309#line 469 "include/linux/mod_devicetable.h"
310struct dmi_strmatch {
311 unsigned char slot ;
312 char substr[79U] ;
313};
314#line 476 "include/linux/mod_devicetable.h"
315struct dmi_system_id {
316 int (*callback)(struct dmi_system_id const * ) ;
317 char const *ident ;
318 struct dmi_strmatch matches[4U] ;
319 void *driver_data ;
320};
321#line 50 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/bios_ebda.h"
322struct __anonstruct_v1_137 {
323 u8 enabled ;
324 u32 buffer_addr ;
325 u16 start ;
326 u16 end ;
327 u16 num_chars ;
328 u8 wrapped ;
329};
330#line 50 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/bios_ebda.h"
331struct __anonstruct_v2_138 {
332 u32 buffer_addr ;
333 u16 num_bytes ;
334 u16 start ;
335 u16 end ;
336};
337#line 50 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/bios_ebda.h"
338union __anonunion_ldv_14501_136 {
339 struct __anonstruct_v1_137 v1 ;
340 struct __anonstruct_v2_138 v2 ;
341};
342#line 50 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/bios_ebda.h"
343struct biosmemcon_ebda {
344 u32 signature ;
345 union __anonunion_ldv_14501_136 ldv_14501 ;
346};
347#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4503/dscv_tempdir/dscv/ri/43_1a/drivers/firmware/google/memconsole.c.p"
348void ldv_spin_lock(void) ;
349#line 3
350void ldv_spin_unlock(void) ;
351#line 4
352int ldv_spin_trylock(void) ;
353#line 101 "include/linux/printk.h"
354extern int printk(char const * , ...) ;
355#line 135 "include/linux/string.h"
356extern ssize_t memory_read_from_buffer(void * , size_t , loff_t * , void const * ,
357 size_t ) ;
358#line 129 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
359__inline static void *phys_to_virt(phys_addr_t address )
360{ unsigned long __cil_tmp2 ;
361 unsigned long __cil_tmp3 ;
362
363 {
364 {
365#line 131
366 __cil_tmp2 = (unsigned long )address;
367#line 131
368 __cil_tmp3 = __cil_tmp2 + 0xffff880000000000UL;
369#line 131
370 return ((void *)__cil_tmp3);
371 }
372}
373}
374#line 140 "include/linux/sysfs.h"
375extern int sysfs_create_bin_file(struct kobject * , struct bin_attribute const * ) ;
376#line 142
377extern void sysfs_remove_bin_file(struct kobject * , struct bin_attribute const * ) ;
378#line 204 "include/linux/kobject.h"
379extern struct kobject *firmware_kobj ;
380#line 220 "include/linux/slub_def.h"
381extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t ) ;
382#line 223
383void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
384#line 11 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4503/dscv_tempdir/dscv/ri/43_1a/drivers/firmware/google/memconsole.c.p"
385void ldv_check_alloc_flags(gfp_t flags ) ;
386#line 12
387void ldv_check_alloc_nonatomic(void) ;
388#line 14
389struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
390#line 96 "include/linux/dmi.h"
391extern int dmi_check_system(struct dmi_system_id const * ) ;
392#line 9 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/bios_ebda.h"
393__inline static unsigned int get_bios_ebda(void)
394{ unsigned int address ;
395 void *tmp ;
396 unsigned short *__cil_tmp3 ;
397 unsigned short __cil_tmp4 ;
398
399 {
400 {
401#line 15
402 tmp = phys_to_virt(1038ULL);
403#line 15
404 __cil_tmp3 = (unsigned short *)tmp;
405#line 15
406 __cil_tmp4 = *__cil_tmp3;
407#line 15
408 address = (unsigned int )__cil_tmp4;
409#line 16
410 address = address << 4;
411 }
412#line 17
413 return (address);
414}
415}
416#line 59 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4503/dscv_tempdir/dscv/ri/43_1a/drivers/firmware/google/memconsole.c.p"
417static char *memconsole_baseaddr ;
418#line 60 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4503/dscv_tempdir/dscv/ri/43_1a/drivers/firmware/google/memconsole.c.p"
419static size_t memconsole_length ;
420#line 62 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4503/dscv_tempdir/dscv/ri/43_1a/drivers/firmware/google/memconsole.c.p"
421static ssize_t memconsole_read(struct file *filp , struct kobject *kobp , struct bin_attribute *bin_attr ,
422 char *buf , loff_t pos , size_t count )
423{ ssize_t tmp ;
424 void *__cil_tmp8 ;
425 void const *__cil_tmp9 ;
426
427 {
428 {
429#line 66
430 __cil_tmp8 = (void *)buf;
431#line 66
432 __cil_tmp9 = (void const *)memconsole_baseaddr;
433#line 66
434 tmp = memory_read_from_buffer(__cil_tmp8, count, & pos, __cil_tmp9, memconsole_length);
435 }
436#line 66
437 return (tmp);
438}
439}
440#line 70 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4503/dscv_tempdir/dscv/ri/43_1a/drivers/firmware/google/memconsole.c.p"
441static struct bin_attribute memconsole_bin_attr = {{"log", (umode_t )292U, (struct lock_class_key *)0, {{{(char)0}, {(char)0}, {(char)0},
442 {(char)0}, {(char)0}, {(char)0},
443 {(char)0}, {(char)0}}}},
444 0UL, (void *)0, & memconsole_read, (ssize_t (*)(struct file * , struct kobject * ,
445 struct bin_attribute * , char * ,
446 loff_t , size_t ))0, (int (*)(struct file * ,
447 struct kobject * ,
448 struct bin_attribute * ,
449 struct vm_area_struct * ))0};
450#line 76 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4503/dscv_tempdir/dscv/ri/43_1a/drivers/firmware/google/memconsole.c.p"
451static void found_v1_header(struct biosmemcon_ebda *hdr )
452{ void *tmp ;
453 unsigned long __cil_tmp3 ;
454 unsigned long __cil_tmp4 ;
455 unsigned long __cil_tmp5 ;
456 unsigned long __cil_tmp6 ;
457 u32 __cil_tmp7 ;
458 unsigned long __cil_tmp8 ;
459 unsigned long __cil_tmp9 ;
460 unsigned long __cil_tmp10 ;
461 unsigned long __cil_tmp11 ;
462 u16 __cil_tmp12 ;
463 int __cil_tmp13 ;
464 unsigned long __cil_tmp14 ;
465 unsigned long __cil_tmp15 ;
466 unsigned long __cil_tmp16 ;
467 unsigned long __cil_tmp17 ;
468 u16 __cil_tmp18 ;
469 int __cil_tmp19 ;
470 unsigned long __cil_tmp20 ;
471 unsigned long __cil_tmp21 ;
472 unsigned long __cil_tmp22 ;
473 unsigned long __cil_tmp23 ;
474 u16 __cil_tmp24 ;
475 int __cil_tmp25 ;
476 unsigned long __cil_tmp26 ;
477 unsigned long __cil_tmp27 ;
478 unsigned long __cil_tmp28 ;
479 unsigned long __cil_tmp29 ;
480 u16 __cil_tmp30 ;
481 unsigned long __cil_tmp31 ;
482 unsigned long __cil_tmp32 ;
483 unsigned long __cil_tmp33 ;
484 unsigned long __cil_tmp34 ;
485 u32 __cil_tmp35 ;
486 phys_addr_t __cil_tmp36 ;
487
488 {
489 {
490#line 78
491 printk("<6>BIOS console v1 EBDA structure found at %p\n", hdr);
492#line 79
493 __cil_tmp3 = 0 + 4;
494#line 79
495 __cil_tmp4 = 4 + __cil_tmp3;
496#line 79
497 __cil_tmp5 = (unsigned long )hdr;
498#line 79
499 __cil_tmp6 = __cil_tmp5 + __cil_tmp4;
500#line 79
501 __cil_tmp7 = *((u32 *)__cil_tmp6);
502#line 79
503 __cil_tmp8 = 0 + 8;
504#line 79
505 __cil_tmp9 = 4 + __cil_tmp8;
506#line 79
507 __cil_tmp10 = (unsigned long )hdr;
508#line 79
509 __cil_tmp11 = __cil_tmp10 + __cil_tmp9;
510#line 79
511 __cil_tmp12 = *((u16 *)__cil_tmp11);
512#line 79
513 __cil_tmp13 = (int )__cil_tmp12;
514#line 79
515 __cil_tmp14 = 0 + 10;
516#line 79
517 __cil_tmp15 = 4 + __cil_tmp14;
518#line 79
519 __cil_tmp16 = (unsigned long )hdr;
520#line 79
521 __cil_tmp17 = __cil_tmp16 + __cil_tmp15;
522#line 79
523 __cil_tmp18 = *((u16 *)__cil_tmp17);
524#line 79
525 __cil_tmp19 = (int )__cil_tmp18;
526#line 79
527 __cil_tmp20 = 0 + 12;
528#line 79
529 __cil_tmp21 = 4 + __cil_tmp20;
530#line 79
531 __cil_tmp22 = (unsigned long )hdr;
532#line 79
533 __cil_tmp23 = __cil_tmp22 + __cil_tmp21;
534#line 79
535 __cil_tmp24 = *((u16 *)__cil_tmp23);
536#line 79
537 __cil_tmp25 = (int )__cil_tmp24;
538#line 79
539 printk("<6>BIOS console buffer at 0x%.8x, start = %d, end = %d, num = %d\n", __cil_tmp7,
540 __cil_tmp13, __cil_tmp19, __cil_tmp25);
541#line 84
542 __cil_tmp26 = 0 + 12;
543#line 84
544 __cil_tmp27 = 4 + __cil_tmp26;
545#line 84
546 __cil_tmp28 = (unsigned long )hdr;
547#line 84
548 __cil_tmp29 = __cil_tmp28 + __cil_tmp27;
549#line 84
550 __cil_tmp30 = *((u16 *)__cil_tmp29);
551#line 84
552 memconsole_length = (size_t )__cil_tmp30;
553#line 85
554 __cil_tmp31 = 0 + 4;
555#line 85
556 __cil_tmp32 = 4 + __cil_tmp31;
557#line 85
558 __cil_tmp33 = (unsigned long )hdr;
559#line 85
560 __cil_tmp34 = __cil_tmp33 + __cil_tmp32;
561#line 85
562 __cil_tmp35 = *((u32 *)__cil_tmp34);
563#line 85
564 __cil_tmp36 = (phys_addr_t )__cil_tmp35;
565#line 85
566 tmp = phys_to_virt(__cil_tmp36);
567#line 85
568 memconsole_baseaddr = (char *)tmp;
569 }
570#line 86
571 return;
572}
573}
574#line 88 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4503/dscv_tempdir/dscv/ri/43_1a/drivers/firmware/google/memconsole.c.p"
575static void found_v2_header(struct biosmemcon_ebda *hdr )
576{ void *tmp ;
577 unsigned long __cil_tmp3 ;
578 unsigned long __cil_tmp4 ;
579 u32 __cil_tmp5 ;
580 unsigned long __cil_tmp6 ;
581 unsigned long __cil_tmp7 ;
582 unsigned long __cil_tmp8 ;
583 unsigned long __cil_tmp9 ;
584 u16 __cil_tmp10 ;
585 int __cil_tmp11 ;
586 unsigned long __cil_tmp12 ;
587 unsigned long __cil_tmp13 ;
588 unsigned long __cil_tmp14 ;
589 unsigned long __cil_tmp15 ;
590 u16 __cil_tmp16 ;
591 int __cil_tmp17 ;
592 unsigned long __cil_tmp18 ;
593 unsigned long __cil_tmp19 ;
594 unsigned long __cil_tmp20 ;
595 unsigned long __cil_tmp21 ;
596 u16 __cil_tmp22 ;
597 int __cil_tmp23 ;
598 unsigned long __cil_tmp24 ;
599 unsigned long __cil_tmp25 ;
600 unsigned long __cil_tmp26 ;
601 unsigned long __cil_tmp27 ;
602 u16 __cil_tmp28 ;
603 int __cil_tmp29 ;
604 unsigned long __cil_tmp30 ;
605 unsigned long __cil_tmp31 ;
606 unsigned long __cil_tmp32 ;
607 unsigned long __cil_tmp33 ;
608 u16 __cil_tmp34 ;
609 int __cil_tmp35 ;
610 int __cil_tmp36 ;
611 unsigned long __cil_tmp37 ;
612 unsigned long __cil_tmp38 ;
613 unsigned long __cil_tmp39 ;
614 unsigned long __cil_tmp40 ;
615 u16 __cil_tmp41 ;
616 u32 __cil_tmp42 ;
617 unsigned long __cil_tmp43 ;
618 unsigned long __cil_tmp44 ;
619 u32 __cil_tmp45 ;
620 u32 __cil_tmp46 ;
621 phys_addr_t __cil_tmp47 ;
622
623 {
624 {
625#line 90
626 printk("<6>BIOS console v2 EBDA structure found at %p\n", hdr);
627#line 91
628 __cil_tmp3 = (unsigned long )hdr;
629#line 91
630 __cil_tmp4 = __cil_tmp3 + 4;
631#line 91
632 __cil_tmp5 = *((u32 *)__cil_tmp4);
633#line 91
634 __cil_tmp6 = 0 + 6;
635#line 91
636 __cil_tmp7 = 4 + __cil_tmp6;
637#line 91
638 __cil_tmp8 = (unsigned long )hdr;
639#line 91
640 __cil_tmp9 = __cil_tmp8 + __cil_tmp7;
641#line 91
642 __cil_tmp10 = *((u16 *)__cil_tmp9);
643#line 91
644 __cil_tmp11 = (int )__cil_tmp10;
645#line 91
646 __cil_tmp12 = 0 + 8;
647#line 91
648 __cil_tmp13 = 4 + __cil_tmp12;
649#line 91
650 __cil_tmp14 = (unsigned long )hdr;
651#line 91
652 __cil_tmp15 = __cil_tmp14 + __cil_tmp13;
653#line 91
654 __cil_tmp16 = *((u16 *)__cil_tmp15);
655#line 91
656 __cil_tmp17 = (int )__cil_tmp16;
657#line 91
658 __cil_tmp18 = 0 + 4;
659#line 91
660 __cil_tmp19 = 4 + __cil_tmp18;
661#line 91
662 __cil_tmp20 = (unsigned long )hdr;
663#line 91
664 __cil_tmp21 = __cil_tmp20 + __cil_tmp19;
665#line 91
666 __cil_tmp22 = *((u16 *)__cil_tmp21);
667#line 91
668 __cil_tmp23 = (int )__cil_tmp22;
669#line 91
670 printk("<6>BIOS console buffer at 0x%.8x, start = %d, end = %d, num_bytes = %d\n",
671 __cil_tmp5, __cil_tmp11, __cil_tmp17, __cil_tmp23);
672#line 96
673 __cil_tmp24 = 0 + 6;
674#line 96
675 __cil_tmp25 = 4 + __cil_tmp24;
676#line 96
677 __cil_tmp26 = (unsigned long )hdr;
678#line 96
679 __cil_tmp27 = __cil_tmp26 + __cil_tmp25;
680#line 96
681 __cil_tmp28 = *((u16 *)__cil_tmp27);
682#line 96
683 __cil_tmp29 = (int )__cil_tmp28;
684#line 96
685 __cil_tmp30 = 0 + 8;
686#line 96
687 __cil_tmp31 = 4 + __cil_tmp30;
688#line 96
689 __cil_tmp32 = (unsigned long )hdr;
690#line 96
691 __cil_tmp33 = __cil_tmp32 + __cil_tmp31;
692#line 96
693 __cil_tmp34 = *((u16 *)__cil_tmp33);
694#line 96
695 __cil_tmp35 = (int )__cil_tmp34;
696#line 96
697 __cil_tmp36 = __cil_tmp35 - __cil_tmp29;
698#line 96
699 memconsole_length = (size_t )__cil_tmp36;
700#line 97
701 __cil_tmp37 = 0 + 6;
702#line 97
703 __cil_tmp38 = 4 + __cil_tmp37;
704#line 97
705 __cil_tmp39 = (unsigned long )hdr;
706#line 97
707 __cil_tmp40 = __cil_tmp39 + __cil_tmp38;
708#line 97
709 __cil_tmp41 = *((u16 *)__cil_tmp40);
710#line 97
711 __cil_tmp42 = (u32 )__cil_tmp41;
712#line 97
713 __cil_tmp43 = (unsigned long )hdr;
714#line 97
715 __cil_tmp44 = __cil_tmp43 + 4;
716#line 97
717 __cil_tmp45 = *((u32 *)__cil_tmp44);
718#line 97
719 __cil_tmp46 = __cil_tmp45 + __cil_tmp42;
720#line 97
721 __cil_tmp47 = (phys_addr_t )__cil_tmp46;
722#line 97
723 tmp = phys_to_virt(__cil_tmp47);
724#line 97
725 memconsole_baseaddr = (char *)tmp;
726 }
727#line 99
728 return;
729}
730}
731#line 105 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4503/dscv_tempdir/dscv/ri/43_1a/drivers/firmware/google/memconsole.c.p"
732static bool found_memconsole(void)
733{ unsigned int address ;
734 size_t length ;
735 size_t cur ;
736 void *tmp ;
737 struct biosmemcon_ebda *hdr ;
738 void *tmp___0 ;
739 phys_addr_t __cil_tmp7 ;
740 u8 *__cil_tmp8 ;
741 u8 __cil_tmp9 ;
742 size_t __cil_tmp10 ;
743 size_t __cil_tmp11 ;
744 phys_addr_t __cil_tmp12 ;
745 u32 __cil_tmp13 ;
746 u32 __cil_tmp14 ;
747
748 {
749 {
750#line 110
751 address = get_bios_ebda();
752 }
753#line 111
754 if (address == 0U) {
755 {
756#line 112
757 printk("<6>BIOS EBDA non-existent.\n");
758 }
759#line 113
760 return ((bool )0);
761 } else {
762
763 }
764 {
765#line 117
766 __cil_tmp7 = (phys_addr_t )address;
767#line 117
768 tmp = phys_to_virt(__cil_tmp7);
769#line 117
770 __cil_tmp8 = (u8 *)tmp;
771#line 117
772 __cil_tmp9 = *__cil_tmp8;
773#line 117
774 length = (size_t )__cil_tmp9;
775#line 118
776 length = length << 10;
777#line 124
778 cur = 0UL;
779 }
780#line 124
781 goto ldv_14527;
782 ldv_14526:
783 {
784#line 125
785 __cil_tmp10 = (size_t )address;
786#line 125
787 __cil_tmp11 = __cil_tmp10 + cur;
788#line 125
789 __cil_tmp12 = (phys_addr_t )__cil_tmp11;
790#line 125
791 tmp___0 = phys_to_virt(__cil_tmp12);
792#line 125
793 hdr = (struct biosmemcon_ebda *)tmp___0;
794 }
795 {
796#line 128
797 __cil_tmp13 = *((u32 *)hdr);
798#line 128
799 if (__cil_tmp13 == 3735927486U) {
800 {
801#line 129
802 found_v1_header(hdr);
803 }
804#line 130
805 return ((bool )1);
806 } else {
807
808 }
809 }
810 {
811#line 134
812 __cil_tmp14 = *((u32 *)hdr);
813#line 134
814 if (__cil_tmp14 == 1313817421U) {
815 {
816#line 135
817 found_v2_header(hdr);
818 }
819#line 136
820 return ((bool )1);
821 } else {
822
823 }
824 }
825#line 124
826 cur = cur + 1UL;
827 ldv_14527: ;
828#line 124
829 if (cur < length) {
830#line 125
831 goto ldv_14526;
832 } else {
833#line 127
834 goto ldv_14528;
835 }
836 ldv_14528:
837 {
838#line 140
839 printk("<6>BIOS console EBDA structure not found!\n");
840 }
841#line 141
842 return ((bool )0);
843}
844}
845#line 144 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4503/dscv_tempdir/dscv/ri/43_1a/drivers/firmware/google/memconsole.c.p"
846static struct dmi_system_id memconsole_dmi_table[2U] = { {(int (*)(struct dmi_system_id const * ))0, "Google Board", {{(unsigned char)9,
847 {(char )'G',
848 (char )'o',
849 (char )'o',
850 (char )'g',
851 (char )'l',
852 (char )'e',
853 (char )',',
854 (char )' ',
855 (char )'I',
856 (char )'n',
857 (char )'c',
858 (char )'.',
859 (char )'\000'}},
860 {(unsigned char)0,
861 {(char)0, (char)0,
862 (char)0, (char)0,
863 (char)0, (char)0,
864 (char)0, (char)0,
865 (char)0, (char)0,
866 (char)0, (char)0,
867 (char)0, (char)0,
868 (char)0, (char)0,
869 (char)0, (char)0,
870 (char)0, (char)0,
871 (char)0, (char)0,
872 (char)0, (char)0,
873 (char)0, (char)0,
874 (char)0, (char)0,
875 (char)0, (char)0,
876 (char)0, (char)0,
877 (char)0, (char)0,
878 (char)0, (char)0,
879 (char)0, (char)0,
880 (char)0, (char)0,
881 (char)0, (char)0,
882 (char)0, (char)0,
883 (char)0, (char)0,
884 (char)0, (char)0,
885 (char)0, (char)0,
886 (char)0, (char)0,
887 (char)0, (char)0,
888 (char)0, (char)0,
889 (char)0, (char)0,
890 (char)0, (char)0,
891 (char)0, (char)0,
892 (char)0, (char)0,
893 (char)0, (char)0,
894 (char)0, (char)0,
895 (char)0, (char)0,
896 (char)0, (char)0,
897 (char)0, (char)0,
898 (char)0, (char)0,
899 (char)0, (char)0,
900 (char)0}}, {(unsigned char)0,
901 {(char)0,
902 (char)0,
903 (char)0,
904 (char)0,
905 (char)0,
906 (char)0,
907 (char)0,
908 (char)0,
909 (char)0,
910 (char)0,
911 (char)0,
912 (char)0,
913 (char)0,
914 (char)0,
915 (char)0,
916 (char)0,
917 (char)0,
918 (char)0,
919 (char)0,
920 (char)0,
921 (char)0,
922 (char)0,
923 (char)0,
924 (char)0,
925 (char)0,
926 (char)0,
927 (char)0,
928 (char)0,
929 (char)0,
930 (char)0,
931 (char)0,
932 (char)0,
933 (char)0,
934 (char)0,
935 (char)0,
936 (char)0,
937 (char)0,
938 (char)0,
939 (char)0,
940 (char)0,
941 (char)0,
942 (char)0,
943 (char)0,
944 (char)0,
945 (char)0,
946 (char)0,
947 (char)0,
948 (char)0,
949 (char)0,
950 (char)0,
951 (char)0,
952 (char)0,
953 (char)0,
954 (char)0,
955 (char)0,
956 (char)0,
957 (char)0,
958 (char)0,
959 (char)0,
960 (char)0,
961 (char)0,
962 (char)0,
963 (char)0,
964 (char)0,
965 (char)0,
966 (char)0,
967 (char)0,
968 (char)0,
969 (char)0,
970 (char)0,
971 (char)0,
972 (char)0,
973 (char)0,
974 (char)0,
975 (char)0,
976 (char)0,
977 (char)0,
978 (char)0,
979 (char)0}},
980 {(unsigned char)0,
981 {(char)0, (char)0,
982 (char)0, (char)0,
983 (char)0, (char)0,
984 (char)0, (char)0,
985 (char)0, (char)0,
986 (char)0, (char)0,
987 (char)0, (char)0,
988 (char)0, (char)0,
989 (char)0, (char)0,
990 (char)0, (char)0,
991 (char)0, (char)0,
992 (char)0, (char)0,
993 (char)0, (char)0,
994 (char)0, (char)0,
995 (char)0, (char)0,
996 (char)0, (char)0,
997 (char)0, (char)0,
998 (char)0, (char)0,
999 (char)0, (char)0,
1000 (char)0, (char)0,
1001 (char)0, (char)0,
1002 (char)0, (char)0,
1003 (char)0, (char)0,
1004 (char)0, (char)0,
1005 (char)0, (char)0,
1006 (char)0, (char)0,
1007 (char)0, (char)0,
1008 (char)0, (char)0,
1009 (char)0, (char)0,
1010 (char)0, (char)0,
1011 (char)0, (char)0,
1012 (char)0, (char)0,
1013 (char)0, (char)0,
1014 (char)0, (char)0,
1015 (char)0, (char)0,
1016 (char)0, (char)0,
1017 (char)0, (char)0,
1018 (char)0, (char)0,
1019 (char)0, (char)0,
1020 (char)0}}},
1021 (void *)0},
1022 {(int (*)(struct dmi_system_id const * ))0, (char const *)0, {{(unsigned char)0,
1023 {(char)0,
1024 (char)0,
1025 (char)0,
1026 (char)0,
1027 (char)0,
1028 (char)0,
1029 (char)0,
1030 (char)0,
1031 (char)0,
1032 (char)0,
1033 (char)0,
1034 (char)0,
1035 (char)0,
1036 (char)0,
1037 (char)0,
1038 (char)0,
1039 (char)0,
1040 (char)0,
1041 (char)0,
1042 (char)0,
1043 (char)0,
1044 (char)0,
1045 (char)0,
1046 (char)0,
1047 (char)0,
1048 (char)0,
1049 (char)0,
1050 (char)0,
1051 (char)0,
1052 (char)0,
1053 (char)0,
1054 (char)0,
1055 (char)0,
1056 (char)0,
1057 (char)0,
1058 (char)0,
1059 (char)0,
1060 (char)0,
1061 (char)0,
1062 (char)0,
1063 (char)0,
1064 (char)0,
1065 (char)0,
1066 (char)0,
1067 (char)0,
1068 (char)0,
1069 (char)0,
1070 (char)0,
1071 (char)0,
1072 (char)0,
1073 (char)0,
1074 (char)0,
1075 (char)0,
1076 (char)0,
1077 (char)0,
1078 (char)0,
1079 (char)0,
1080 (char)0,
1081 (char)0,
1082 (char)0,
1083 (char)0,
1084 (char)0,
1085 (char)0,
1086 (char)0,
1087 (char)0,
1088 (char)0,
1089 (char)0,
1090 (char)0,
1091 (char)0,
1092 (char)0,
1093 (char)0,
1094 (char)0,
1095 (char)0,
1096 (char)0,
1097 (char)0,
1098 (char)0,
1099 (char)0,
1100 (char)0,
1101 (char)0}},
1102 {(unsigned char)0,
1103 {(char)0,
1104 (char)0,
1105 (char)0,
1106 (char)0,
1107 (char)0,
1108 (char)0,
1109 (char)0,
1110 (char)0,
1111 (char)0,
1112 (char)0,
1113 (char)0,
1114 (char)0,
1115 (char)0,
1116 (char)0,
1117 (char)0,
1118 (char)0,
1119 (char)0,
1120 (char)0,
1121 (char)0,
1122 (char)0,
1123 (char)0,
1124 (char)0,
1125 (char)0,
1126 (char)0,
1127 (char)0,
1128 (char)0,
1129 (char)0,
1130 (char)0,
1131 (char)0,
1132 (char)0,
1133 (char)0,
1134 (char)0,
1135 (char)0,
1136 (char)0,
1137 (char)0,
1138 (char)0,
1139 (char)0,
1140 (char)0,
1141 (char)0,
1142 (char)0,
1143 (char)0,
1144 (char)0,
1145 (char)0,
1146 (char)0,
1147 (char)0,
1148 (char)0,
1149 (char)0,
1150 (char)0,
1151 (char)0,
1152 (char)0,
1153 (char)0,
1154 (char)0,
1155 (char)0,
1156 (char)0,
1157 (char)0,
1158 (char)0,
1159 (char)0,
1160 (char)0,
1161 (char)0,
1162 (char)0,
1163 (char)0,
1164 (char)0,
1165 (char)0,
1166 (char)0,
1167 (char)0,
1168 (char)0,
1169 (char)0,
1170 (char)0,
1171 (char)0,
1172 (char)0,
1173 (char)0,
1174 (char)0,
1175 (char)0,
1176 (char)0,
1177 (char)0,
1178 (char)0,
1179 (char)0,
1180 (char)0,
1181 (char)0}},
1182 {(unsigned char)0,
1183 {(char)0,
1184 (char)0,
1185 (char)0,
1186 (char)0,
1187 (char)0,
1188 (char)0,
1189 (char)0,
1190 (char)0,
1191 (char)0,
1192 (char)0,
1193 (char)0,
1194 (char)0,
1195 (char)0,
1196 (char)0,
1197 (char)0,
1198 (char)0,
1199 (char)0,
1200 (char)0,
1201 (char)0,
1202 (char)0,
1203 (char)0,
1204 (char)0,
1205 (char)0,
1206 (char)0,
1207 (char)0,
1208 (char)0,
1209 (char)0,
1210 (char)0,
1211 (char)0,
1212 (char)0,
1213 (char)0,
1214 (char)0,
1215 (char)0,
1216 (char)0,
1217 (char)0,
1218 (char)0,
1219 (char)0,
1220 (char)0,
1221 (char)0,
1222 (char)0,
1223 (char)0,
1224 (char)0,
1225 (char)0,
1226 (char)0,
1227 (char)0,
1228 (char)0,
1229 (char)0,
1230 (char)0,
1231 (char)0,
1232 (char)0,
1233 (char)0,
1234 (char)0,
1235 (char)0,
1236 (char)0,
1237 (char)0,
1238 (char)0,
1239 (char)0,
1240 (char)0,
1241 (char)0,
1242 (char)0,
1243 (char)0,
1244 (char)0,
1245 (char)0,
1246 (char)0,
1247 (char)0,
1248 (char)0,
1249 (char)0,
1250 (char)0,
1251 (char)0,
1252 (char)0,
1253 (char)0,
1254 (char)0,
1255 (char)0,
1256 (char)0,
1257 (char)0,
1258 (char)0,
1259 (char)0,
1260 (char)0,
1261 (char)0}},
1262 {(unsigned char)0,
1263 {(char)0,
1264 (char)0,
1265 (char)0,
1266 (char)0,
1267 (char)0,
1268 (char)0,
1269 (char)0,
1270 (char)0,
1271 (char)0,
1272 (char)0,
1273 (char)0,
1274 (char)0,
1275 (char)0,
1276 (char)0,
1277 (char)0,
1278 (char)0,
1279 (char)0,
1280 (char)0,
1281 (char)0,
1282 (char)0,
1283 (char)0,
1284 (char)0,
1285 (char)0,
1286 (char)0,
1287 (char)0,
1288 (char)0,
1289 (char)0,
1290 (char)0,
1291 (char)0,
1292 (char)0,
1293 (char)0,
1294 (char)0,
1295 (char)0,
1296 (char)0,
1297 (char)0,
1298 (char)0,
1299 (char)0,
1300 (char)0,
1301 (char)0,
1302 (char)0,
1303 (char)0,
1304 (char)0,
1305 (char)0,
1306 (char)0,
1307 (char)0,
1308 (char)0,
1309 (char)0,
1310 (char)0,
1311 (char)0,
1312 (char)0,
1313 (char)0,
1314 (char)0,
1315 (char)0,
1316 (char)0,
1317 (char)0,
1318 (char)0,
1319 (char)0,
1320 (char)0,
1321 (char)0,
1322 (char)0,
1323 (char)0,
1324 (char)0,
1325 (char)0,
1326 (char)0,
1327 (char)0,
1328 (char)0,
1329 (char)0,
1330 (char)0,
1331 (char)0,
1332 (char)0,
1333 (char)0,
1334 (char)0,
1335 (char)0,
1336 (char)0,
1337 (char)0,
1338 (char)0,
1339 (char)0,
1340 (char)0,
1341 (char)0}}},
1342 (void *)0}};
1343#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4503/dscv_tempdir/dscv/ri/43_1a/drivers/firmware/google/memconsole.c.p"
1344struct dmi_system_id const __mod_dmi_device_table ;
1345#line 155 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4503/dscv_tempdir/dscv/ri/43_1a/drivers/firmware/google/memconsole.c.p"
1346static int memconsole_init(void)
1347{ int ret ;
1348 int tmp ;
1349 bool tmp___0 ;
1350 int tmp___1 ;
1351 struct dmi_system_id const *__cil_tmp5 ;
1352 unsigned long __cil_tmp6 ;
1353 struct bin_attribute const *__cil_tmp7 ;
1354
1355 {
1356 {
1357#line 159
1358 __cil_tmp5 = (struct dmi_system_id const *)(& memconsole_dmi_table);
1359#line 159
1360 tmp = dmi_check_system(__cil_tmp5);
1361 }
1362#line 159
1363 if (tmp == 0) {
1364#line 160
1365 return (-19);
1366 } else {
1367
1368 }
1369 {
1370#line 162
1371 tmp___0 = found_memconsole();
1372 }
1373#line 162
1374 if (tmp___0) {
1375#line 162
1376 tmp___1 = 0;
1377 } else {
1378#line 162
1379 tmp___1 = 1;
1380 }
1381#line 162
1382 if (tmp___1) {
1383#line 163
1384 return (-19);
1385 } else {
1386
1387 }
1388 {
1389#line 165
1390 __cil_tmp6 = (unsigned long )(& memconsole_bin_attr) + 32;
1391#line 165
1392 *((size_t *)__cil_tmp6) = memconsole_length;
1393#line 167
1394 __cil_tmp7 = (struct bin_attribute const *)(& memconsole_bin_attr);
1395#line 167
1396 ret = sysfs_create_bin_file(firmware_kobj, __cil_tmp7);
1397 }
1398#line 169
1399 return (ret);
1400}
1401}
1402#line 172 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4503/dscv_tempdir/dscv/ri/43_1a/drivers/firmware/google/memconsole.c.p"
1403static void memconsole_exit(void)
1404{ struct bin_attribute const *__cil_tmp1 ;
1405
1406 {
1407 {
1408#line 174
1409 __cil_tmp1 = (struct bin_attribute const *)(& memconsole_bin_attr);
1410#line 174
1411 sysfs_remove_bin_file(firmware_kobj, __cil_tmp1);
1412 }
1413#line 175
1414 return;
1415}
1416}
1417#line 199
1418extern void ldv_check_final_state(void) ;
1419#line 205
1420extern void ldv_initialize(void) ;
1421#line 208
1422extern int __VERIFIER_nondet_int(void) ;
1423#line 211 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4503/dscv_tempdir/dscv/ri/43_1a/drivers/firmware/google/memconsole.c.p"
1424int LDV_IN_INTERRUPT ;
1425#line 214 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4503/dscv_tempdir/dscv/ri/43_1a/drivers/firmware/google/memconsole.c.p"
1426void main(void)
1427{ struct file *var_group1 ;
1428 struct kobject *var_group2 ;
1429 struct bin_attribute *var_memconsole_read_0_p2 ;
1430 char *var_memconsole_read_0_p3 ;
1431 loff_t var_memconsole_read_0_p4 ;
1432 size_t var_memconsole_read_0_p5 ;
1433 int tmp ;
1434 int tmp___0 ;
1435 int tmp___1 ;
1436
1437 {
1438 {
1439#line 245
1440 LDV_IN_INTERRUPT = 1;
1441#line 254
1442 ldv_initialize();
1443#line 263
1444 tmp = memconsole_init();
1445 }
1446#line 263
1447 if (tmp != 0) {
1448#line 264
1449 goto ldv_final;
1450 } else {
1451
1452 }
1453#line 268
1454 goto ldv_14573;
1455 ldv_14572:
1456 {
1457#line 271
1458 tmp___0 = __VERIFIER_nondet_int();
1459 }
1460#line 273
1461 if (tmp___0 == 0) {
1462#line 273
1463 goto case_0;
1464 } else {
1465 {
1466#line 292
1467 goto switch_default;
1468#line 271
1469 if (0) {
1470 case_0:
1471 {
1472#line 284
1473 memconsole_read(var_group1, var_group2, var_memconsole_read_0_p2, var_memconsole_read_0_p3,
1474 var_memconsole_read_0_p4, var_memconsole_read_0_p5);
1475 }
1476#line 291
1477 goto ldv_14570;
1478 switch_default: ;
1479#line 292
1480 goto ldv_14570;
1481 } else {
1482 switch_break: ;
1483 }
1484 }
1485 }
1486 ldv_14570: ;
1487 ldv_14573:
1488 {
1489#line 268
1490 tmp___1 = __VERIFIER_nondet_int();
1491 }
1492#line 268
1493 if (tmp___1 != 0) {
1494#line 269
1495 goto ldv_14572;
1496 } else {
1497#line 271
1498 goto ldv_14574;
1499 }
1500 ldv_14574: ;
1501 {
1502#line 307
1503 memconsole_exit();
1504 }
1505 ldv_final:
1506 {
1507#line 310
1508 ldv_check_final_state();
1509 }
1510#line 313
1511 return;
1512}
1513}
1514#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4503/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
1515void ldv_blast_assert(void)
1516{
1517
1518 {
1519 ERROR: ;
1520#line 6
1521 goto ERROR;
1522}
1523}
1524#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4503/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
1525extern int __VERIFIER_nondet_int(void) ;
1526#line 334 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4503/dscv_tempdir/dscv/ri/43_1a/drivers/firmware/google/memconsole.c.p"
1527int ldv_spin = 0;
1528#line 338 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4503/dscv_tempdir/dscv/ri/43_1a/drivers/firmware/google/memconsole.c.p"
1529void ldv_check_alloc_flags(gfp_t flags )
1530{
1531
1532 {
1533#line 341
1534 if (ldv_spin != 0) {
1535#line 341
1536 if (flags != 32U) {
1537 {
1538#line 341
1539 ldv_blast_assert();
1540 }
1541 } else {
1542
1543 }
1544 } else {
1545
1546 }
1547#line 344
1548 return;
1549}
1550}
1551#line 344
1552extern struct page *ldv_some_page(void) ;
1553#line 347 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4503/dscv_tempdir/dscv/ri/43_1a/drivers/firmware/google/memconsole.c.p"
1554struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags )
1555{ struct page *tmp ;
1556
1557 {
1558#line 350
1559 if (ldv_spin != 0) {
1560#line 350
1561 if (flags != 32U) {
1562 {
1563#line 350
1564 ldv_blast_assert();
1565 }
1566 } else {
1567
1568 }
1569 } else {
1570
1571 }
1572 {
1573#line 352
1574 tmp = ldv_some_page();
1575 }
1576#line 352
1577 return (tmp);
1578}
1579}
1580#line 356 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4503/dscv_tempdir/dscv/ri/43_1a/drivers/firmware/google/memconsole.c.p"
1581void ldv_check_alloc_nonatomic(void)
1582{
1583
1584 {
1585#line 359
1586 if (ldv_spin != 0) {
1587 {
1588#line 359
1589 ldv_blast_assert();
1590 }
1591 } else {
1592
1593 }
1594#line 362
1595 return;
1596}
1597}
1598#line 363 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4503/dscv_tempdir/dscv/ri/43_1a/drivers/firmware/google/memconsole.c.p"
1599void ldv_spin_lock(void)
1600{
1601
1602 {
1603#line 366
1604 ldv_spin = 1;
1605#line 367
1606 return;
1607}
1608}
1609#line 370 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4503/dscv_tempdir/dscv/ri/43_1a/drivers/firmware/google/memconsole.c.p"
1610void ldv_spin_unlock(void)
1611{
1612
1613 {
1614#line 373
1615 ldv_spin = 0;
1616#line 374
1617 return;
1618}
1619}
1620#line 377 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4503/dscv_tempdir/dscv/ri/43_1a/drivers/firmware/google/memconsole.c.p"
1621int ldv_spin_trylock(void)
1622{ int is_lock ;
1623
1624 {
1625 {
1626#line 382
1627 is_lock = __VERIFIER_nondet_int();
1628 }
1629#line 384
1630 if (is_lock != 0) {
1631#line 387
1632 return (0);
1633 } else {
1634#line 392
1635 ldv_spin = 1;
1636#line 394
1637 return (1);
1638 }
1639}
1640}
1641#line 561 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4503/dscv_tempdir/dscv/ri/43_1a/drivers/firmware/google/memconsole.c.p"
1642void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 )
1643{
1644
1645 {
1646 {
1647#line 567
1648 ldv_check_alloc_flags(ldv_func_arg2);
1649#line 569
1650 kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
1651 }
1652#line 570
1653 return ((void *)0);
1654}
1655}