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 206 "include/linux/types.h"
33typedef u64 phys_addr_t;
34#line 219 "include/linux/types.h"
35struct __anonstruct_atomic_t_7 {
36 int counter ;
37};
38#line 219 "include/linux/types.h"
39typedef struct __anonstruct_atomic_t_7 atomic_t;
40#line 229 "include/linux/types.h"
41struct list_head {
42 struct list_head *next ;
43 struct list_head *prev ;
44};
45#line 12 "include/linux/lockdep.h"
46struct task_struct;
47#line 12
48struct task_struct;
49#line 20 "include/linux/kobject_ns.h"
50struct sock;
51#line 20
52struct sock;
53#line 21
54struct kobject;
55#line 21
56struct kobject;
57#line 27
58enum kobj_ns_type {
59 KOBJ_NS_TYPE_NONE = 0,
60 KOBJ_NS_TYPE_NET = 1,
61 KOBJ_NS_TYPES = 2
62} ;
63#line 40 "include/linux/kobject_ns.h"
64struct kobj_ns_type_operations {
65 enum kobj_ns_type type ;
66 void *(*grab_current_ns)(void) ;
67 void const *(*netlink_ns)(struct sock *sk ) ;
68 void const *(*initial_ns)(void) ;
69 void (*drop_ns)(void * ) ;
70};
71#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
72struct task_struct;
73#line 295 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
74struct file;
75#line 295
76struct file;
77#line 52 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
78struct task_struct;
79#line 329
80struct arch_spinlock;
81#line 329
82struct arch_spinlock;
83#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
84struct task_struct;
85#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
86struct task_struct;
87#line 22 "include/linux/sysfs.h"
88struct kobject;
89#line 24
90enum kobj_ns_type;
91#line 26 "include/linux/sysfs.h"
92struct attribute {
93 char const *name ;
94 umode_t mode ;
95};
96#line 85
97struct file;
98#line 86
99struct vm_area_struct;
100#line 86
101struct vm_area_struct;
102#line 88 "include/linux/sysfs.h"
103struct bin_attribute {
104 struct attribute attr ;
105 size_t size ;
106 void *private ;
107 ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
108 loff_t , size_t ) ;
109 ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
110 loff_t , size_t ) ;
111 int (*mmap)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ) ;
112};
113#line 112 "include/linux/sysfs.h"
114struct sysfs_ops {
115 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
116 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
117 void const *(*namespace)(struct kobject * , struct attribute const * ) ;
118};
119#line 118
120struct sysfs_dirent;
121#line 118
122struct sysfs_dirent;
123#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
124struct task_struct;
125#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
126typedef u16 __ticket_t;
127#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
128typedef u32 __ticketpair_t;
129#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
130struct __raw_tickets {
131 __ticket_t head ;
132 __ticket_t tail ;
133};
134#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
135union __anonunion____missing_field_name_36 {
136 __ticketpair_t head_tail ;
137 struct __raw_tickets tickets ;
138};
139#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
140struct arch_spinlock {
141 union __anonunion____missing_field_name_36 __annonCompField17 ;
142};
143#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
144typedef struct arch_spinlock arch_spinlock_t;
145#line 20 "include/linux/spinlock_types.h"
146struct raw_spinlock {
147 arch_spinlock_t raw_lock ;
148 unsigned int magic ;
149 unsigned int owner_cpu ;
150 void *owner ;
151};
152#line 64 "include/linux/spinlock_types.h"
153union __anonunion____missing_field_name_39 {
154 struct raw_spinlock rlock ;
155};
156#line 64 "include/linux/spinlock_types.h"
157struct spinlock {
158 union __anonunion____missing_field_name_39 __annonCompField19 ;
159};
160#line 64 "include/linux/spinlock_types.h"
161typedef struct spinlock spinlock_t;
162#line 22 "include/linux/kref.h"
163struct kref {
164 atomic_t refcount ;
165};
166#line 55 "include/linux/wait.h"
167struct task_struct;
168#line 60 "include/linux/kobject.h"
169struct kset;
170#line 60
171struct kobj_type;
172#line 60 "include/linux/kobject.h"
173struct kobject {
174 char const *name ;
175 struct list_head entry ;
176 struct kobject *parent ;
177 struct kset *kset ;
178 struct kobj_type *ktype ;
179 struct sysfs_dirent *sd ;
180 struct kref kref ;
181 unsigned int state_initialized : 1 ;
182 unsigned int state_in_sysfs : 1 ;
183 unsigned int state_add_uevent_sent : 1 ;
184 unsigned int state_remove_uevent_sent : 1 ;
185 unsigned int uevent_suppress : 1 ;
186};
187#line 108 "include/linux/kobject.h"
188struct kobj_type {
189 void (*release)(struct kobject *kobj ) ;
190 struct sysfs_ops const *sysfs_ops ;
191 struct attribute **default_attrs ;
192 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject *kobj ) ;
193 void const *(*namespace)(struct kobject *kobj ) ;
194};
195#line 116 "include/linux/kobject.h"
196struct kobj_uevent_env {
197 char *envp[32] ;
198 int envp_idx ;
199 char buf[2048] ;
200 int buflen ;
201};
202#line 123 "include/linux/kobject.h"
203struct kset_uevent_ops {
204 int (* const filter)(struct kset *kset , struct kobject *kobj ) ;
205 char const *(* const name)(struct kset *kset , struct kobject *kobj ) ;
206 int (* const uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
207};
208#line 140
209struct sock;
210#line 159 "include/linux/kobject.h"
211struct kset {
212 struct list_head list ;
213 spinlock_t list_lock ;
214 struct kobject kobj ;
215 struct kset_uevent_ops const *uevent_ops ;
216};
217#line 48 "include/linux/mutex.h"
218struct mutex {
219 atomic_t count ;
220 spinlock_t wait_lock ;
221 struct list_head wait_list ;
222 struct task_struct *owner ;
223 char const *name ;
224 void *magic ;
225};
226#line 8 "include/linux/vmalloc.h"
227struct vm_area_struct;
228#line 10 "include/linux/gfp.h"
229struct vm_area_struct;
230#line 49 "include/linux/kmod.h"
231struct file;
232#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
233struct task_struct;
234#line 438 "include/linux/elf.h"
235struct file;
236#line 472 "include/linux/mod_devicetable.h"
237struct dmi_strmatch {
238 unsigned char slot ;
239 char substr[79] ;
240};
241#line 486 "include/linux/mod_devicetable.h"
242struct dmi_system_id {
243 int (*callback)(struct dmi_system_id const * ) ;
244 char const *ident ;
245 struct dmi_strmatch matches[4] ;
246 void *driver_data ;
247};
248#line 24 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/drivers/firmware/google/memconsole.c.common.c"
249struct __anonstruct_v1_203 {
250 u8 enabled ;
251 u32 buffer_addr ;
252 u16 start ;
253 u16 end ;
254 u16 num_chars ;
255 u8 wrapped ;
256} __attribute__((__packed__)) ;
257#line 24 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/drivers/firmware/google/memconsole.c.common.c"
258struct __anonstruct_v2_204 {
259 u32 buffer_addr ;
260 u16 num_bytes ;
261 u16 start ;
262 u16 end ;
263} __attribute__((__packed__)) ;
264#line 24 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/drivers/firmware/google/memconsole.c.common.c"
265union __anonunion____missing_field_name_202 {
266 struct __anonstruct_v1_203 v1 ;
267 struct __anonstruct_v2_204 v2 ;
268};
269#line 24 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/drivers/firmware/google/memconsole.c.common.c"
270struct biosmemcon_ebda {
271 u32 signature ;
272 union __anonunion____missing_field_name_202 __annonCompField33 ;
273} __attribute__((__packed__)) ;
274#line 1 "<compiler builtins>"
275long __builtin_expect(long val , long res ) ;
276#line 100 "include/linux/printk.h"
277extern int ( printk)(char const *fmt , ...) ;
278#line 135 "include/linux/string.h"
279extern ssize_t memory_read_from_buffer(void *to , size_t count , loff_t *ppos , void const *from ,
280 size_t available ) ;
281#line 140 "include/linux/sysfs.h"
282extern int __attribute__((__warn_unused_result__)) sysfs_create_bin_file(struct kobject *kobj ,
283 struct bin_attribute const *attr ) ;
284#line 142
285extern void sysfs_remove_bin_file(struct kobject *kobj , struct bin_attribute const *attr ) ;
286#line 204 "include/linux/kobject.h"
287extern struct kobject *firmware_kobj ;
288#line 152 "include/linux/mutex.h"
289void mutex_lock(struct mutex *lock ) ;
290#line 153
291int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock ) ;
292#line 154
293int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock ) ;
294#line 168
295int mutex_trylock(struct mutex *lock ) ;
296#line 169
297void mutex_unlock(struct mutex *lock ) ;
298#line 170
299int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
300#line 129 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
301__inline static void *phys_to_virt(phys_addr_t address ) __attribute__((__no_instrument_function__)) ;
302#line 129 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
303__inline static void *phys_to_virt(phys_addr_t address )
304{ unsigned long __cil_tmp2 ;
305 unsigned long __cil_tmp3 ;
306
307 {
308 {
309#line 131
310 __cil_tmp2 = (unsigned long )address;
311#line 131
312 __cil_tmp3 = __cil_tmp2 + 0xffff880000000000UL;
313#line 131
314 return ((void *)__cil_tmp3);
315 }
316}
317}
318#line 67 "include/linux/module.h"
319int init_module(void) ;
320#line 68
321void cleanup_module(void) ;
322#line 96 "include/linux/dmi.h"
323extern int dmi_check_system(struct dmi_system_id const *list ) ;
324#line 9 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/bios_ebda.h"
325__inline static unsigned int get_bios_ebda(void) __attribute__((__no_instrument_function__)) ;
326#line 9 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/bios_ebda.h"
327__inline static unsigned int get_bios_ebda(void)
328{ unsigned int address ;
329 void *tmp ;
330 phys_addr_t __cil_tmp3 ;
331 unsigned short *__cil_tmp4 ;
332 unsigned short __cil_tmp5 ;
333
334 {
335 {
336#line 15
337 __cil_tmp3 = (phys_addr_t )1038;
338#line 15
339 tmp = phys_to_virt(__cil_tmp3);
340#line 15
341 __cil_tmp4 = (unsigned short *)tmp;
342#line 15
343 __cil_tmp5 = *__cil_tmp4;
344#line 15
345 address = (unsigned int )__cil_tmp5;
346#line 16
347 address = address << 4;
348 }
349#line 17
350 return (address);
351}
352}
353#line 45 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/drivers/firmware/google/memconsole.c.common.c"
354static char *memconsole_baseaddr ;
355#line 46 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/drivers/firmware/google/memconsole.c.common.c"
356static size_t memconsole_length ;
357#line 48 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/drivers/firmware/google/memconsole.c.common.c"
358static ssize_t memconsole_read(struct file *filp , struct kobject *kobp , struct bin_attribute *bin_attr ,
359 char *buf , loff_t pos , size_t count )
360{ ssize_t tmp ;
361 void *__cil_tmp8 ;
362 void const *__cil_tmp9 ;
363
364 {
365 {
366#line 52
367 __cil_tmp8 = (void *)buf;
368#line 52
369 __cil_tmp9 = (void const *)memconsole_baseaddr;
370#line 52
371 tmp = memory_read_from_buffer(__cil_tmp8, count, & pos, __cil_tmp9, memconsole_length);
372 }
373#line 52
374 return (tmp);
375}
376}
377#line 56 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/drivers/firmware/google/memconsole.c.common.c"
378static struct bin_attribute memconsole_bin_attr = {{"log", (umode_t )292}, 0UL, (void *)0, & memconsole_read, (ssize_t (*)(struct file * ,
379 struct kobject * ,
380 struct bin_attribute * ,
381 char * ,
382 loff_t ,
383 size_t ))0,
384 (int (*)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ))0};
385#line 62 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/drivers/firmware/google/memconsole.c.common.c"
386static void found_v1_header(struct biosmemcon_ebda *hdr )
387{ void *tmp ;
388 unsigned long __cil_tmp3 ;
389 unsigned long __cil_tmp4 ;
390 unsigned long __cil_tmp5 ;
391 unsigned long __cil_tmp6 ;
392 u32 __cil_tmp7 ;
393 unsigned long __cil_tmp8 ;
394 unsigned long __cil_tmp9 ;
395 unsigned long __cil_tmp10 ;
396 unsigned long __cil_tmp11 ;
397 u16 __cil_tmp12 ;
398 int __cil_tmp13 ;
399 unsigned long __cil_tmp14 ;
400 unsigned long __cil_tmp15 ;
401 unsigned long __cil_tmp16 ;
402 unsigned long __cil_tmp17 ;
403 u16 __cil_tmp18 ;
404 int __cil_tmp19 ;
405 unsigned long __cil_tmp20 ;
406 unsigned long __cil_tmp21 ;
407 unsigned long __cil_tmp22 ;
408 unsigned long __cil_tmp23 ;
409 u16 __cil_tmp24 ;
410 int __cil_tmp25 ;
411 unsigned long __cil_tmp26 ;
412 unsigned long __cil_tmp27 ;
413 unsigned long __cil_tmp28 ;
414 unsigned long __cil_tmp29 ;
415 u16 __cil_tmp30 ;
416 unsigned long __cil_tmp31 ;
417 unsigned long __cil_tmp32 ;
418 unsigned long __cil_tmp33 ;
419 unsigned long __cil_tmp34 ;
420 u32 __cil_tmp35 ;
421 phys_addr_t __cil_tmp36 ;
422
423 {
424 {
425#line 64
426 printk("<6>BIOS console v1 EBDA structure found at %p\n", hdr);
427#line 65
428 __cil_tmp3 = 0 + 1;
429#line 65
430 __cil_tmp4 = 4 + __cil_tmp3;
431#line 65
432 __cil_tmp5 = (unsigned long )hdr;
433#line 65
434 __cil_tmp6 = __cil_tmp5 + __cil_tmp4;
435#line 65
436 __cil_tmp7 = *((u32 *)__cil_tmp6);
437#line 65
438 __cil_tmp8 = 0 + 5;
439#line 65
440 __cil_tmp9 = 4 + __cil_tmp8;
441#line 65
442 __cil_tmp10 = (unsigned long )hdr;
443#line 65
444 __cil_tmp11 = __cil_tmp10 + __cil_tmp9;
445#line 65
446 __cil_tmp12 = *((u16 *)__cil_tmp11);
447#line 65
448 __cil_tmp13 = (int )__cil_tmp12;
449#line 65
450 __cil_tmp14 = 0 + 7;
451#line 65
452 __cil_tmp15 = 4 + __cil_tmp14;
453#line 65
454 __cil_tmp16 = (unsigned long )hdr;
455#line 65
456 __cil_tmp17 = __cil_tmp16 + __cil_tmp15;
457#line 65
458 __cil_tmp18 = *((u16 *)__cil_tmp17);
459#line 65
460 __cil_tmp19 = (int )__cil_tmp18;
461#line 65
462 __cil_tmp20 = 0 + 9;
463#line 65
464 __cil_tmp21 = 4 + __cil_tmp20;
465#line 65
466 __cil_tmp22 = (unsigned long )hdr;
467#line 65
468 __cil_tmp23 = __cil_tmp22 + __cil_tmp21;
469#line 65
470 __cil_tmp24 = *((u16 *)__cil_tmp23);
471#line 65
472 __cil_tmp25 = (int )__cil_tmp24;
473#line 65
474 printk("<6>BIOS console buffer at 0x%.8x, start = %d, end = %d, num = %d\n", __cil_tmp7,
475 __cil_tmp13, __cil_tmp19, __cil_tmp25);
476#line 70
477 __cil_tmp26 = 0 + 9;
478#line 70
479 __cil_tmp27 = 4 + __cil_tmp26;
480#line 70
481 __cil_tmp28 = (unsigned long )hdr;
482#line 70
483 __cil_tmp29 = __cil_tmp28 + __cil_tmp27;
484#line 70
485 __cil_tmp30 = *((u16 *)__cil_tmp29);
486#line 70
487 memconsole_length = (size_t )__cil_tmp30;
488#line 71
489 __cil_tmp31 = 0 + 1;
490#line 71
491 __cil_tmp32 = 4 + __cil_tmp31;
492#line 71
493 __cil_tmp33 = (unsigned long )hdr;
494#line 71
495 __cil_tmp34 = __cil_tmp33 + __cil_tmp32;
496#line 71
497 __cil_tmp35 = *((u32 *)__cil_tmp34);
498#line 71
499 __cil_tmp36 = (phys_addr_t )__cil_tmp35;
500#line 71
501 tmp = phys_to_virt(__cil_tmp36);
502#line 71
503 memconsole_baseaddr = (char *)tmp;
504 }
505#line 72
506 return;
507}
508}
509#line 74 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/drivers/firmware/google/memconsole.c.common.c"
510static void found_v2_header(struct biosmemcon_ebda *hdr )
511{ void *tmp ;
512 unsigned long __cil_tmp3 ;
513 unsigned long __cil_tmp4 ;
514 u32 __cil_tmp5 ;
515 unsigned long __cil_tmp6 ;
516 unsigned long __cil_tmp7 ;
517 unsigned long __cil_tmp8 ;
518 unsigned long __cil_tmp9 ;
519 u16 __cil_tmp10 ;
520 int __cil_tmp11 ;
521 unsigned long __cil_tmp12 ;
522 unsigned long __cil_tmp13 ;
523 unsigned long __cil_tmp14 ;
524 unsigned long __cil_tmp15 ;
525 u16 __cil_tmp16 ;
526 int __cil_tmp17 ;
527 unsigned long __cil_tmp18 ;
528 unsigned long __cil_tmp19 ;
529 unsigned long __cil_tmp20 ;
530 unsigned long __cil_tmp21 ;
531 u16 __cil_tmp22 ;
532 int __cil_tmp23 ;
533 unsigned long __cil_tmp24 ;
534 unsigned long __cil_tmp25 ;
535 unsigned long __cil_tmp26 ;
536 unsigned long __cil_tmp27 ;
537 u16 __cil_tmp28 ;
538 int __cil_tmp29 ;
539 unsigned long __cil_tmp30 ;
540 unsigned long __cil_tmp31 ;
541 unsigned long __cil_tmp32 ;
542 unsigned long __cil_tmp33 ;
543 u16 __cil_tmp34 ;
544 int __cil_tmp35 ;
545 int __cil_tmp36 ;
546 unsigned long __cil_tmp37 ;
547 unsigned long __cil_tmp38 ;
548 unsigned long __cil_tmp39 ;
549 unsigned long __cil_tmp40 ;
550 u16 __cil_tmp41 ;
551 u32 __cil_tmp42 ;
552 unsigned long __cil_tmp43 ;
553 unsigned long __cil_tmp44 ;
554 u32 __cil_tmp45 ;
555 u32 __cil_tmp46 ;
556 phys_addr_t __cil_tmp47 ;
557
558 {
559 {
560#line 76
561 printk("<6>BIOS console v2 EBDA structure found at %p\n", hdr);
562#line 77
563 __cil_tmp3 = (unsigned long )hdr;
564#line 77
565 __cil_tmp4 = __cil_tmp3 + 4;
566#line 77
567 __cil_tmp5 = *((u32 *)__cil_tmp4);
568#line 77
569 __cil_tmp6 = 0 + 6;
570#line 77
571 __cil_tmp7 = 4 + __cil_tmp6;
572#line 77
573 __cil_tmp8 = (unsigned long )hdr;
574#line 77
575 __cil_tmp9 = __cil_tmp8 + __cil_tmp7;
576#line 77
577 __cil_tmp10 = *((u16 *)__cil_tmp9);
578#line 77
579 __cil_tmp11 = (int )__cil_tmp10;
580#line 77
581 __cil_tmp12 = 0 + 8;
582#line 77
583 __cil_tmp13 = 4 + __cil_tmp12;
584#line 77
585 __cil_tmp14 = (unsigned long )hdr;
586#line 77
587 __cil_tmp15 = __cil_tmp14 + __cil_tmp13;
588#line 77
589 __cil_tmp16 = *((u16 *)__cil_tmp15);
590#line 77
591 __cil_tmp17 = (int )__cil_tmp16;
592#line 77
593 __cil_tmp18 = 0 + 4;
594#line 77
595 __cil_tmp19 = 4 + __cil_tmp18;
596#line 77
597 __cil_tmp20 = (unsigned long )hdr;
598#line 77
599 __cil_tmp21 = __cil_tmp20 + __cil_tmp19;
600#line 77
601 __cil_tmp22 = *((u16 *)__cil_tmp21);
602#line 77
603 __cil_tmp23 = (int )__cil_tmp22;
604#line 77
605 printk("<6>BIOS console buffer at 0x%.8x, start = %d, end = %d, num_bytes = %d\n",
606 __cil_tmp5, __cil_tmp11, __cil_tmp17, __cil_tmp23);
607#line 82
608 __cil_tmp24 = 0 + 6;
609#line 82
610 __cil_tmp25 = 4 + __cil_tmp24;
611#line 82
612 __cil_tmp26 = (unsigned long )hdr;
613#line 82
614 __cil_tmp27 = __cil_tmp26 + __cil_tmp25;
615#line 82
616 __cil_tmp28 = *((u16 *)__cil_tmp27);
617#line 82
618 __cil_tmp29 = (int )__cil_tmp28;
619#line 82
620 __cil_tmp30 = 0 + 8;
621#line 82
622 __cil_tmp31 = 4 + __cil_tmp30;
623#line 82
624 __cil_tmp32 = (unsigned long )hdr;
625#line 82
626 __cil_tmp33 = __cil_tmp32 + __cil_tmp31;
627#line 82
628 __cil_tmp34 = *((u16 *)__cil_tmp33);
629#line 82
630 __cil_tmp35 = (int )__cil_tmp34;
631#line 82
632 __cil_tmp36 = __cil_tmp35 - __cil_tmp29;
633#line 82
634 memconsole_length = (size_t )__cil_tmp36;
635#line 83
636 __cil_tmp37 = 0 + 6;
637#line 83
638 __cil_tmp38 = 4 + __cil_tmp37;
639#line 83
640 __cil_tmp39 = (unsigned long )hdr;
641#line 83
642 __cil_tmp40 = __cil_tmp39 + __cil_tmp38;
643#line 83
644 __cil_tmp41 = *((u16 *)__cil_tmp40);
645#line 83
646 __cil_tmp42 = (u32 )__cil_tmp41;
647#line 83
648 __cil_tmp43 = (unsigned long )hdr;
649#line 83
650 __cil_tmp44 = __cil_tmp43 + 4;
651#line 83
652 __cil_tmp45 = *((u32 *)__cil_tmp44);
653#line 83
654 __cil_tmp46 = __cil_tmp45 + __cil_tmp42;
655#line 83
656 __cil_tmp47 = (phys_addr_t )__cil_tmp46;
657#line 83
658 tmp = phys_to_virt(__cil_tmp47);
659#line 83
660 memconsole_baseaddr = (char *)tmp;
661 }
662#line 85
663 return;
664}
665}
666#line 91 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/drivers/firmware/google/memconsole.c.common.c"
667static bool found_memconsole(void)
668{ unsigned int address ;
669 size_t length ;
670 size_t cur ;
671 void *tmp ;
672 struct biosmemcon_ebda *hdr ;
673 void *tmp___0 ;
674 phys_addr_t __cil_tmp7 ;
675 u8 *__cil_tmp8 ;
676 u8 __cil_tmp9 ;
677 size_t __cil_tmp10 ;
678 size_t __cil_tmp11 ;
679 phys_addr_t __cil_tmp12 ;
680 u32 __cil_tmp13 ;
681 int __cil_tmp14 ;
682 int __cil_tmp15 ;
683 int __cil_tmp16 ;
684 int __cil_tmp17 ;
685 int __cil_tmp18 ;
686 int __cil_tmp19 ;
687 u32 __cil_tmp20 ;
688 u32 __cil_tmp21 ;
689
690 {
691 {
692#line 96
693 address = get_bios_ebda();
694 }
695#line 97
696 if (! address) {
697 {
698#line 98
699 printk("<6>BIOS EBDA non-existent.\n");
700 }
701#line 99
702 return ((bool )0);
703 } else {
704
705 }
706 {
707#line 103
708 __cil_tmp7 = (phys_addr_t )address;
709#line 103
710 tmp = phys_to_virt(__cil_tmp7);
711#line 103
712 __cil_tmp8 = (u8 *)tmp;
713#line 103
714 __cil_tmp9 = *__cil_tmp8;
715#line 103
716 length = (size_t )__cil_tmp9;
717#line 104
718 length = length << 10;
719#line 110
720 cur = (size_t )0;
721 }
722 {
723#line 110
724 while (1) {
725 while_continue: ;
726#line 110
727 if (cur < length) {
728
729 } else {
730#line 110
731 goto while_break;
732 }
733 {
734#line 111
735 __cil_tmp10 = (size_t )address;
736#line 111
737 __cil_tmp11 = __cil_tmp10 + cur;
738#line 111
739 __cil_tmp12 = (phys_addr_t )__cil_tmp11;
740#line 111
741 tmp___0 = phys_to_virt(__cil_tmp12);
742#line 111
743 hdr = (struct biosmemcon_ebda *)tmp___0;
744 }
745 {
746#line 114
747 __cil_tmp13 = *((u32 *)hdr);
748#line 114
749 if (__cil_tmp13 == 3735927486U) {
750 {
751#line 115
752 found_v1_header(hdr);
753 }
754#line 116
755 return ((bool )1);
756 } else {
757
758 }
759 }
760 {
761#line 120
762 __cil_tmp14 = 78 << 24;
763#line 120
764 __cil_tmp15 = 79 << 16;
765#line 120
766 __cil_tmp16 = 67 << 8;
767#line 120
768 __cil_tmp17 = 77 | __cil_tmp16;
769#line 120
770 __cil_tmp18 = __cil_tmp17 | __cil_tmp15;
771#line 120
772 __cil_tmp19 = __cil_tmp18 | __cil_tmp14;
773#line 120
774 __cil_tmp20 = (u32 )__cil_tmp19;
775#line 120
776 __cil_tmp21 = *((u32 *)hdr);
777#line 120
778 if (__cil_tmp21 == __cil_tmp20) {
779 {
780#line 121
781 found_v2_header(hdr);
782 }
783#line 122
784 return ((bool )1);
785 } else {
786
787 }
788 }
789#line 110
790 cur = cur + 1UL;
791 }
792 while_break: ;
793 }
794 {
795#line 126
796 printk("<6>BIOS console EBDA structure not found!\n");
797 }
798#line 127
799 return ((bool )0);
800}
801}
802#line 130 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/drivers/firmware/google/memconsole.c.common.c"
803static struct dmi_system_id memconsole_dmi_table[1] __attribute__((__section__(".init.data"))) = { {(int (*)(struct dmi_system_id const * ))0,
804 "Google Board", {{(unsigned char)9, {(char )'G', (char )'o', (char )'o', (char )'g',
805 (char )'l', (char )'e', (char )',', (char )' ',
806 (char )'I', (char )'n', (char )'c', (char )'.',
807 (char )'\000'}}, {(unsigned char)0, {(char)0,
808 (char)0,
809 (char)0,
810 (char)0,
811 (char)0,
812 (char)0,
813 (char)0,
814 (char)0,
815 (char)0,
816 (char)0,
817 (char)0,
818 (char)0,
819 (char)0,
820 (char)0,
821 (char)0,
822 (char)0,
823 (char)0,
824 (char)0,
825 (char)0,
826 (char)0,
827 (char)0,
828 (char)0,
829 (char)0,
830 (char)0,
831 (char)0,
832 (char)0,
833 (char)0,
834 (char)0,
835 (char)0,
836 (char)0,
837 (char)0,
838 (char)0,
839 (char)0,
840 (char)0,
841 (char)0,
842 (char)0,
843 (char)0,
844 (char)0,
845 (char)0,
846 (char)0,
847 (char)0,
848 (char)0,
849 (char)0,
850 (char)0,
851 (char)0,
852 (char)0,
853 (char)0,
854 (char)0,
855 (char)0,
856 (char)0,
857 (char)0,
858 (char)0,
859 (char)0,
860 (char)0,
861 (char)0,
862 (char)0,
863 (char)0,
864 (char)0,
865 (char)0,
866 (char)0,
867 (char)0,
868 (char)0,
869 (char)0,
870 (char)0,
871 (char)0,
872 (char)0,
873 (char)0,
874 (char)0,
875 (char)0,
876 (char)0,
877 (char)0,
878 (char)0,
879 (char)0,
880 (char)0,
881 (char)0,
882 (char)0,
883 (char)0,
884 (char)0,
885 (char)0}},
886 {(unsigned char)0, {(char)0, (char)0, (char)0, (char)0, (char)0,
887 (char)0, (char)0, (char)0, (char)0, (char)0,
888 (char)0, (char)0, (char)0, (char)0, (char)0,
889 (char)0, (char)0, (char)0, (char)0, (char)0,
890 (char)0, (char)0, (char)0, (char)0, (char)0,
891 (char)0, (char)0, (char)0, (char)0, (char)0,
892 (char)0, (char)0, (char)0, (char)0, (char)0,
893 (char)0, (char)0, (char)0, (char)0, (char)0,
894 (char)0, (char)0, (char)0, (char)0, (char)0,
895 (char)0, (char)0, (char)0, (char)0, (char)0,
896 (char)0, (char)0, (char)0, (char)0, (char)0,
897 (char)0, (char)0, (char)0, (char)0, (char)0,
898 (char)0, (char)0, (char)0, (char)0, (char)0,
899 (char)0, (char)0, (char)0, (char)0, (char)0,
900 (char)0, (char)0, (char)0, (char)0, (char)0,
901 (char)0, (char)0, (char)0, (char)0}}, {(unsigned 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 (char)0}}},
981 (void *)0}};
982#line 139
983extern struct dmi_system_id const __mod_dmi_device_table __attribute__((__unused__,
984__alias__("memconsole_dmi_table"))) ;
985#line 141
986static int memconsole_init(void) __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
987#line 141 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/drivers/firmware/google/memconsole.c.common.c"
988static int memconsole_init(void)
989{ int ret ;
990 int tmp ;
991 bool tmp___0 ;
992 unsigned long __cil_tmp4 ;
993 unsigned long __cil_tmp5 ;
994 struct dmi_system_id *__cil_tmp6 ;
995 struct dmi_system_id const *__cil_tmp7 ;
996 unsigned long __cil_tmp8 ;
997 struct bin_attribute const *__cil_tmp9 ;
998
999 {
1000 {
1001#line 145
1002 __cil_tmp4 = 0 * 344UL;
1003#line 145
1004 __cil_tmp5 = (unsigned long )(memconsole_dmi_table) + __cil_tmp4;
1005#line 145
1006 __cil_tmp6 = (struct dmi_system_id *)__cil_tmp5;
1007#line 145
1008 __cil_tmp7 = (struct dmi_system_id const *)__cil_tmp6;
1009#line 145
1010 tmp = dmi_check_system(__cil_tmp7);
1011 }
1012#line 145
1013 if (tmp) {
1014
1015 } else {
1016#line 146
1017 return (-19);
1018 }
1019 {
1020#line 148
1021 tmp___0 = found_memconsole();
1022 }
1023#line 148
1024 if (tmp___0) {
1025
1026 } else {
1027#line 149
1028 return (-19);
1029 }
1030 {
1031#line 151
1032 __cil_tmp8 = (unsigned long )(& memconsole_bin_attr) + 16;
1033#line 151
1034 *((size_t *)__cil_tmp8) = memconsole_length;
1035#line 153
1036 __cil_tmp9 = (struct bin_attribute const *)(& memconsole_bin_attr);
1037#line 153
1038 ret = (int )sysfs_create_bin_file(firmware_kobj, __cil_tmp9);
1039 }
1040#line 155
1041 return (ret);
1042}
1043}
1044#line 158
1045static void memconsole_exit(void) __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
1046#line 158 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/drivers/firmware/google/memconsole.c.common.c"
1047static void memconsole_exit(void)
1048{ struct bin_attribute const *__cil_tmp1 ;
1049
1050 {
1051 {
1052#line 160
1053 __cil_tmp1 = (struct bin_attribute const *)(& memconsole_bin_attr);
1054#line 160
1055 sysfs_remove_bin_file(firmware_kobj, __cil_tmp1);
1056 }
1057#line 161
1058 return;
1059}
1060}
1061#line 163 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/drivers/firmware/google/memconsole.c.common.c"
1062int init_module(void)
1063{ int tmp ;
1064
1065 {
1066 {
1067#line 163
1068 tmp = memconsole_init();
1069 }
1070#line 163
1071 return (tmp);
1072}
1073}
1074#line 164 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/drivers/firmware/google/memconsole.c.common.c"
1075void cleanup_module(void)
1076{
1077
1078 {
1079 {
1080#line 164
1081 memconsole_exit();
1082 }
1083#line 164
1084 return;
1085}
1086}
1087#line 166 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/drivers/firmware/google/memconsole.c.common.c"
1088static char const __mod_author166[20] __attribute__((__used__, __unused__, __section__(".modinfo"),
1089__aligned__(1))) =
1090#line 166
1091 { (char const )'a', (char const )'u', (char const )'t', (char const )'h',
1092 (char const )'o', (char const )'r', (char const )'=', (char const )'G',
1093 (char const )'o', (char const )'o', (char const )'g', (char const )'l',
1094 (char const )'e', (char const )',', (char const )' ', (char const )'I',
1095 (char const )'n', (char const )'c', (char const )'.', (char const )'\000'};
1096#line 167 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/drivers/firmware/google/memconsole.c.common.c"
1097static char const __mod_license167[12] __attribute__((__used__, __unused__, __section__(".modinfo"),
1098__aligned__(1))) =
1099#line 167
1100 { (char const )'l', (char const )'i', (char const )'c', (char const )'e',
1101 (char const )'n', (char const )'s', (char const )'e', (char const )'=',
1102 (char const )'G', (char const )'P', (char const )'L', (char const )'\000'};
1103#line 185
1104void ldv_check_final_state(void) ;
1105#line 191
1106extern void ldv_initialize(void) ;
1107#line 194
1108extern int __VERIFIER_nondet_int(void) ;
1109#line 197 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/drivers/firmware/google/memconsole.c.common.c"
1110int LDV_IN_INTERRUPT ;
1111#line 200 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/drivers/firmware/google/memconsole.c.common.c"
1112void main(void)
1113{ struct file *var_group1 ;
1114 struct kobject *var_group2 ;
1115 struct bin_attribute *var_memconsole_read_0_p2 ;
1116 char *var_memconsole_read_0_p3 ;
1117 loff_t var_memconsole_read_0_p4 ;
1118 size_t var_memconsole_read_0_p5 ;
1119 int tmp ;
1120 int tmp___0 ;
1121 int tmp___1 ;
1122
1123 {
1124 {
1125#line 231
1126 LDV_IN_INTERRUPT = 1;
1127#line 240
1128 ldv_initialize();
1129#line 249
1130 tmp = memconsole_init();
1131 }
1132#line 249
1133 if (tmp) {
1134#line 250
1135 goto ldv_final;
1136 } else {
1137
1138 }
1139 {
1140#line 254
1141 while (1) {
1142 while_continue: ;
1143 {
1144#line 254
1145 tmp___1 = __VERIFIER_nondet_int();
1146 }
1147#line 254
1148 if (tmp___1) {
1149
1150 } else {
1151#line 254
1152 goto while_break;
1153 }
1154 {
1155#line 257
1156 tmp___0 = __VERIFIER_nondet_int();
1157 }
1158#line 259
1159 if (tmp___0 == 0) {
1160#line 259
1161 goto case_0;
1162 } else {
1163 {
1164#line 278
1165 goto switch_default;
1166#line 257
1167 if (0) {
1168 case_0:
1169 {
1170#line 270
1171 memconsole_read(var_group1, var_group2, var_memconsole_read_0_p2, var_memconsole_read_0_p3,
1172 var_memconsole_read_0_p4, var_memconsole_read_0_p5);
1173 }
1174#line 277
1175 goto switch_break;
1176 switch_default:
1177#line 278
1178 goto switch_break;
1179 } else {
1180 switch_break: ;
1181 }
1182 }
1183 }
1184 }
1185 while_break: ;
1186 }
1187 {
1188#line 293
1189 memconsole_exit();
1190 }
1191 ldv_final:
1192 {
1193#line 296
1194 ldv_check_final_state();
1195 }
1196#line 299
1197 return;
1198}
1199}
1200#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
1201void ldv_blast_assert(void)
1202{
1203
1204 {
1205 ERROR:
1206#line 6
1207 goto ERROR;
1208}
1209}
1210#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
1211extern int __VERIFIER_nondet_int(void) ;
1212#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1213int ldv_mutex = 1;
1214#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1215int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )
1216{ int nondetermined ;
1217
1218 {
1219#line 29
1220 if (ldv_mutex == 1) {
1221
1222 } else {
1223 {
1224#line 29
1225 ldv_blast_assert();
1226 }
1227 }
1228 {
1229#line 32
1230 nondetermined = __VERIFIER_nondet_int();
1231 }
1232#line 35
1233 if (nondetermined) {
1234#line 38
1235 ldv_mutex = 2;
1236#line 40
1237 return (0);
1238 } else {
1239#line 45
1240 return (-4);
1241 }
1242}
1243}
1244#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1245int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock )
1246{ int nondetermined ;
1247
1248 {
1249#line 57
1250 if (ldv_mutex == 1) {
1251
1252 } else {
1253 {
1254#line 57
1255 ldv_blast_assert();
1256 }
1257 }
1258 {
1259#line 60
1260 nondetermined = __VERIFIER_nondet_int();
1261 }
1262#line 63
1263 if (nondetermined) {
1264#line 66
1265 ldv_mutex = 2;
1266#line 68
1267 return (0);
1268 } else {
1269#line 73
1270 return (-4);
1271 }
1272}
1273}
1274#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1275int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock )
1276{ int atomic_value_after_dec ;
1277
1278 {
1279#line 83
1280 if (ldv_mutex == 1) {
1281
1282 } else {
1283 {
1284#line 83
1285 ldv_blast_assert();
1286 }
1287 }
1288 {
1289#line 86
1290 atomic_value_after_dec = __VERIFIER_nondet_int();
1291 }
1292#line 89
1293 if (atomic_value_after_dec == 0) {
1294#line 92
1295 ldv_mutex = 2;
1296#line 94
1297 return (1);
1298 } else {
1299
1300 }
1301#line 98
1302 return (0);
1303}
1304}
1305#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1306void mutex_lock(struct mutex *lock )
1307{
1308
1309 {
1310#line 108
1311 if (ldv_mutex == 1) {
1312
1313 } else {
1314 {
1315#line 108
1316 ldv_blast_assert();
1317 }
1318 }
1319#line 110
1320 ldv_mutex = 2;
1321#line 111
1322 return;
1323}
1324}
1325#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1326int mutex_trylock(struct mutex *lock )
1327{ int nondetermined ;
1328
1329 {
1330#line 121
1331 if (ldv_mutex == 1) {
1332
1333 } else {
1334 {
1335#line 121
1336 ldv_blast_assert();
1337 }
1338 }
1339 {
1340#line 124
1341 nondetermined = __VERIFIER_nondet_int();
1342 }
1343#line 127
1344 if (nondetermined) {
1345#line 130
1346 ldv_mutex = 2;
1347#line 132
1348 return (1);
1349 } else {
1350#line 137
1351 return (0);
1352 }
1353}
1354}
1355#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1356void mutex_unlock(struct mutex *lock )
1357{
1358
1359 {
1360#line 147
1361 if (ldv_mutex == 2) {
1362
1363 } else {
1364 {
1365#line 147
1366 ldv_blast_assert();
1367 }
1368 }
1369#line 149
1370 ldv_mutex = 1;
1371#line 150
1372 return;
1373}
1374}
1375#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1376void ldv_check_final_state(void)
1377{
1378
1379 {
1380#line 156
1381 if (ldv_mutex == 1) {
1382
1383 } else {
1384 {
1385#line 156
1386 ldv_blast_assert();
1387 }
1388 }
1389#line 157
1390 return;
1391}
1392}
1393#line 308 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6153/dscv_tempdir/dscv/ri/32_1/drivers/firmware/google/memconsole.c.common.c"
1394long s__builtin_expect(long val , long res )
1395{
1396
1397 {
1398#line 309
1399 return (val);
1400}
1401}