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 51 "include/asm-generic/int-ll64.h"
21typedef long long s64;
22#line 52 "include/asm-generic/int-ll64.h"
23typedef unsigned long long u64;
24#line 14 "include/asm-generic/posix_types.h"
25typedef long __kernel_long_t;
26#line 15 "include/asm-generic/posix_types.h"
27typedef unsigned long __kernel_ulong_t;
28#line 75 "include/asm-generic/posix_types.h"
29typedef __kernel_ulong_t __kernel_size_t;
30#line 76 "include/asm-generic/posix_types.h"
31typedef __kernel_long_t __kernel_ssize_t;
32#line 91 "include/asm-generic/posix_types.h"
33typedef long long __kernel_loff_t;
34#line 21 "include/linux/types.h"
35typedef __u32 __kernel_dev_t;
36#line 24 "include/linux/types.h"
37typedef __kernel_dev_t dev_t;
38#line 27 "include/linux/types.h"
39typedef unsigned short umode_t;
40#line 38 "include/linux/types.h"
41typedef _Bool bool;
42#line 54 "include/linux/types.h"
43typedef __kernel_loff_t loff_t;
44#line 63 "include/linux/types.h"
45typedef __kernel_size_t size_t;
46#line 68 "include/linux/types.h"
47typedef __kernel_ssize_t ssize_t;
48#line 219 "include/linux/types.h"
49struct __anonstruct_atomic_t_7 {
50 int counter ;
51};
52#line 219 "include/linux/types.h"
53typedef struct __anonstruct_atomic_t_7 atomic_t;
54#line 224 "include/linux/types.h"
55struct __anonstruct_atomic64_t_8 {
56 long counter ;
57};
58#line 224 "include/linux/types.h"
59typedef struct __anonstruct_atomic64_t_8 atomic64_t;
60#line 229 "include/linux/types.h"
61struct list_head {
62 struct list_head *next ;
63 struct list_head *prev ;
64};
65#line 12 "include/linux/lockdep.h"
66struct task_struct;
67#line 12
68struct task_struct;
69#line 20 "include/linux/kobject_ns.h"
70struct sock;
71#line 20
72struct sock;
73#line 21
74struct kobject;
75#line 21
76struct kobject;
77#line 27
78enum kobj_ns_type {
79 KOBJ_NS_TYPE_NONE = 0,
80 KOBJ_NS_TYPE_NET = 1,
81 KOBJ_NS_TYPES = 2
82} ;
83#line 40 "include/linux/kobject_ns.h"
84struct kobj_ns_type_operations {
85 enum kobj_ns_type type ;
86 void *(*grab_current_ns)(void) ;
87 void const *(*netlink_ns)(struct sock *sk ) ;
88 void const *(*initial_ns)(void) ;
89 void (*drop_ns)(void * ) ;
90};
91#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
92struct task_struct;
93#line 146 "include/linux/init.h"
94typedef void (*ctor_fn_t)(void);
95#line 295 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
96struct file;
97#line 295
98struct file;
99#line 52 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
100struct task_struct;
101#line 329
102struct arch_spinlock;
103#line 329
104struct arch_spinlock;
105#line 138 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
106struct cpuinfo_x86;
107#line 138
108struct cpuinfo_x86;
109#line 139
110struct task_struct;
111#line 56 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
112struct module;
113#line 56
114struct module;
115#line 47 "include/linux/dynamic_debug.h"
116struct device;
117#line 47
118struct device;
119#line 135 "include/linux/kernel.h"
120struct completion;
121#line 135
122struct completion;
123#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
124struct task_struct;
125#line 10 "include/asm-generic/bug.h"
126struct bug_entry {
127 int bug_addr_disp ;
128 int file_disp ;
129 unsigned short line ;
130 unsigned short flags ;
131};
132#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
133struct static_key;
134#line 234
135struct static_key;
136#line 70 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
137struct cpuinfo_x86 {
138 __u8 x86 ;
139 __u8 x86_vendor ;
140 __u8 x86_model ;
141 __u8 x86_mask ;
142 int x86_tlbsize ;
143 __u8 x86_virt_bits ;
144 __u8 x86_phys_bits ;
145 __u8 x86_coreid_bits ;
146 __u32 extended_cpuid_level ;
147 int cpuid_level ;
148 __u32 x86_capability[10] ;
149 char x86_vendor_id[16] ;
150 char x86_model_id[64] ;
151 int x86_cache_size ;
152 int x86_cache_alignment ;
153 int x86_power ;
154 unsigned long loops_per_jiffy ;
155 u16 x86_max_cores ;
156 u16 apicid ;
157 u16 initial_apicid ;
158 u16 x86_clflush_size ;
159 u16 booted_cores ;
160 u16 phys_proc_id ;
161 u16 cpu_core_id ;
162 u8 compute_unit_id ;
163 u16 cpu_index ;
164 u32 microcode ;
165} __attribute__((__aligned__((1) << (6) ))) ;
166#line 23 "include/asm-generic/atomic-long.h"
167typedef atomic64_t atomic_long_t;
168#line 22 "include/linux/sysfs.h"
169struct kobject;
170#line 23
171struct module;
172#line 24
173enum kobj_ns_type;
174#line 26 "include/linux/sysfs.h"
175struct attribute {
176 char const *name ;
177 umode_t mode ;
178};
179#line 56 "include/linux/sysfs.h"
180struct attribute_group {
181 char const *name ;
182 umode_t (*is_visible)(struct kobject * , struct attribute * , int ) ;
183 struct attribute **attrs ;
184};
185#line 85
186struct file;
187#line 86
188struct vm_area_struct;
189#line 86
190struct vm_area_struct;
191#line 88 "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 *attr , struct vm_area_struct *vma ) ;
201};
202#line 112 "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 118
209struct sysfs_dirent;
210#line 118
211struct sysfs_dirent;
212#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
213struct task_struct;
214#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
215typedef u16 __ticket_t;
216#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
217typedef u32 __ticketpair_t;
218#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
219struct __raw_tickets {
220 __ticket_t head ;
221 __ticket_t tail ;
222};
223#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
224union __anonunion____missing_field_name_36 {
225 __ticketpair_t head_tail ;
226 struct __raw_tickets tickets ;
227};
228#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
229struct arch_spinlock {
230 union __anonunion____missing_field_name_36 __annonCompField17 ;
231};
232#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
233typedef struct arch_spinlock arch_spinlock_t;
234#line 20 "include/linux/spinlock_types.h"
235struct raw_spinlock {
236 arch_spinlock_t raw_lock ;
237 unsigned int magic ;
238 unsigned int owner_cpu ;
239 void *owner ;
240};
241#line 64 "include/linux/spinlock_types.h"
242union __anonunion____missing_field_name_39 {
243 struct raw_spinlock rlock ;
244};
245#line 64 "include/linux/spinlock_types.h"
246struct spinlock {
247 union __anonunion____missing_field_name_39 __annonCompField19 ;
248};
249#line 64 "include/linux/spinlock_types.h"
250typedef struct spinlock spinlock_t;
251#line 22 "include/linux/kref.h"
252struct kref {
253 atomic_t refcount ;
254};
255#line 49 "include/linux/wait.h"
256struct __wait_queue_head {
257 spinlock_t lock ;
258 struct list_head task_list ;
259};
260#line 53 "include/linux/wait.h"
261typedef struct __wait_queue_head wait_queue_head_t;
262#line 55
263struct task_struct;
264#line 60 "include/linux/kobject.h"
265struct kset;
266#line 60
267struct kobj_type;
268#line 60 "include/linux/kobject.h"
269struct kobject {
270 char const *name ;
271 struct list_head entry ;
272 struct kobject *parent ;
273 struct kset *kset ;
274 struct kobj_type *ktype ;
275 struct sysfs_dirent *sd ;
276 struct kref kref ;
277 unsigned int state_initialized : 1 ;
278 unsigned int state_in_sysfs : 1 ;
279 unsigned int state_add_uevent_sent : 1 ;
280 unsigned int state_remove_uevent_sent : 1 ;
281 unsigned int uevent_suppress : 1 ;
282};
283#line 108 "include/linux/kobject.h"
284struct kobj_type {
285 void (*release)(struct kobject *kobj ) ;
286 struct sysfs_ops const *sysfs_ops ;
287 struct attribute **default_attrs ;
288 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject *kobj ) ;
289 void const *(*namespace)(struct kobject *kobj ) ;
290};
291#line 116 "include/linux/kobject.h"
292struct kobj_uevent_env {
293 char *envp[32] ;
294 int envp_idx ;
295 char buf[2048] ;
296 int buflen ;
297};
298#line 123 "include/linux/kobject.h"
299struct kset_uevent_ops {
300 int (* const filter)(struct kset *kset , struct kobject *kobj ) ;
301 char const *(* const name)(struct kset *kset , struct kobject *kobj ) ;
302 int (* const uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
303};
304#line 140
305struct sock;
306#line 159 "include/linux/kobject.h"
307struct kset {
308 struct list_head list ;
309 spinlock_t list_lock ;
310 struct kobject kobj ;
311 struct kset_uevent_ops const *uevent_ops ;
312};
313#line 202 "include/linux/ioport.h"
314struct device;
315#line 19 "include/linux/klist.h"
316struct klist_node;
317#line 19
318struct klist_node;
319#line 39 "include/linux/klist.h"
320struct klist_node {
321 void *n_klist ;
322 struct list_head n_node ;
323 struct kref n_ref ;
324};
325#line 48 "include/linux/mutex.h"
326struct mutex {
327 atomic_t count ;
328 spinlock_t wait_lock ;
329 struct list_head wait_list ;
330 struct task_struct *owner ;
331 char const *name ;
332 void *magic ;
333};
334#line 46 "include/linux/ktime.h"
335union ktime {
336 s64 tv64 ;
337};
338#line 59 "include/linux/ktime.h"
339typedef union ktime ktime_t;
340#line 10 "include/linux/timer.h"
341struct tvec_base;
342#line 10
343struct tvec_base;
344#line 12 "include/linux/timer.h"
345struct timer_list {
346 struct list_head entry ;
347 unsigned long expires ;
348 struct tvec_base *base ;
349 void (*function)(unsigned long ) ;
350 unsigned long data ;
351 int slack ;
352 int start_pid ;
353 void *start_site ;
354 char start_comm[16] ;
355};
356#line 17 "include/linux/workqueue.h"
357struct work_struct;
358#line 17
359struct work_struct;
360#line 79 "include/linux/workqueue.h"
361struct work_struct {
362 atomic_long_t data ;
363 struct list_head entry ;
364 void (*func)(struct work_struct *work ) ;
365};
366#line 25 "include/linux/completion.h"
367struct completion {
368 unsigned int done ;
369 wait_queue_head_t wait ;
370};
371#line 42 "include/linux/pm.h"
372struct device;
373#line 50 "include/linux/pm.h"
374struct pm_message {
375 int event ;
376};
377#line 50 "include/linux/pm.h"
378typedef struct pm_message pm_message_t;
379#line 264 "include/linux/pm.h"
380struct dev_pm_ops {
381 int (*prepare)(struct device *dev ) ;
382 void (*complete)(struct device *dev ) ;
383 int (*suspend)(struct device *dev ) ;
384 int (*resume)(struct device *dev ) ;
385 int (*freeze)(struct device *dev ) ;
386 int (*thaw)(struct device *dev ) ;
387 int (*poweroff)(struct device *dev ) ;
388 int (*restore)(struct device *dev ) ;
389 int (*suspend_late)(struct device *dev ) ;
390 int (*resume_early)(struct device *dev ) ;
391 int (*freeze_late)(struct device *dev ) ;
392 int (*thaw_early)(struct device *dev ) ;
393 int (*poweroff_late)(struct device *dev ) ;
394 int (*restore_early)(struct device *dev ) ;
395 int (*suspend_noirq)(struct device *dev ) ;
396 int (*resume_noirq)(struct device *dev ) ;
397 int (*freeze_noirq)(struct device *dev ) ;
398 int (*thaw_noirq)(struct device *dev ) ;
399 int (*poweroff_noirq)(struct device *dev ) ;
400 int (*restore_noirq)(struct device *dev ) ;
401 int (*runtime_suspend)(struct device *dev ) ;
402 int (*runtime_resume)(struct device *dev ) ;
403 int (*runtime_idle)(struct device *dev ) ;
404};
405#line 458
406enum rpm_status {
407 RPM_ACTIVE = 0,
408 RPM_RESUMING = 1,
409 RPM_SUSPENDED = 2,
410 RPM_SUSPENDING = 3
411} ;
412#line 480
413enum rpm_request {
414 RPM_REQ_NONE = 0,
415 RPM_REQ_IDLE = 1,
416 RPM_REQ_SUSPEND = 2,
417 RPM_REQ_AUTOSUSPEND = 3,
418 RPM_REQ_RESUME = 4
419} ;
420#line 488
421struct wakeup_source;
422#line 488
423struct wakeup_source;
424#line 495 "include/linux/pm.h"
425struct pm_subsys_data {
426 spinlock_t lock ;
427 unsigned int refcount ;
428};
429#line 506
430struct dev_pm_qos_request;
431#line 506
432struct pm_qos_constraints;
433#line 506 "include/linux/pm.h"
434struct dev_pm_info {
435 pm_message_t power_state ;
436 unsigned int can_wakeup : 1 ;
437 unsigned int async_suspend : 1 ;
438 bool is_prepared : 1 ;
439 bool is_suspended : 1 ;
440 bool ignore_children : 1 ;
441 spinlock_t lock ;
442 struct list_head entry ;
443 struct completion completion ;
444 struct wakeup_source *wakeup ;
445 bool wakeup_path : 1 ;
446 struct timer_list suspend_timer ;
447 unsigned long timer_expires ;
448 struct work_struct work ;
449 wait_queue_head_t wait_queue ;
450 atomic_t usage_count ;
451 atomic_t child_count ;
452 unsigned int disable_depth : 3 ;
453 unsigned int idle_notification : 1 ;
454 unsigned int request_pending : 1 ;
455 unsigned int deferred_resume : 1 ;
456 unsigned int run_wake : 1 ;
457 unsigned int runtime_auto : 1 ;
458 unsigned int no_callbacks : 1 ;
459 unsigned int irq_safe : 1 ;
460 unsigned int use_autosuspend : 1 ;
461 unsigned int timer_autosuspends : 1 ;
462 enum rpm_request request ;
463 enum rpm_status runtime_status ;
464 int runtime_error ;
465 int autosuspend_delay ;
466 unsigned long last_busy ;
467 unsigned long active_jiffies ;
468 unsigned long suspended_jiffies ;
469 unsigned long accounting_timestamp ;
470 ktime_t suspend_time ;
471 s64 max_time_suspended_ns ;
472 struct dev_pm_qos_request *pq_req ;
473 struct pm_subsys_data *subsys_data ;
474 struct pm_qos_constraints *constraints ;
475};
476#line 564 "include/linux/pm.h"
477struct dev_pm_domain {
478 struct dev_pm_ops ops ;
479};
480#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
481struct dma_map_ops;
482#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
483struct dev_archdata {
484 void *acpi_handle ;
485 struct dma_map_ops *dma_ops ;
486 void *iommu ;
487};
488#line 28 "include/linux/device.h"
489struct device;
490#line 29
491struct device_private;
492#line 29
493struct device_private;
494#line 30
495struct device_driver;
496#line 30
497struct device_driver;
498#line 31
499struct driver_private;
500#line 31
501struct driver_private;
502#line 32
503struct module;
504#line 33
505struct class;
506#line 33
507struct class;
508#line 34
509struct subsys_private;
510#line 34
511struct subsys_private;
512#line 35
513struct bus_type;
514#line 35
515struct bus_type;
516#line 36
517struct device_node;
518#line 36
519struct device_node;
520#line 37
521struct iommu_ops;
522#line 37
523struct iommu_ops;
524#line 39 "include/linux/device.h"
525struct bus_attribute {
526 struct attribute attr ;
527 ssize_t (*show)(struct bus_type *bus , char *buf ) ;
528 ssize_t (*store)(struct bus_type *bus , char const *buf , size_t count ) ;
529};
530#line 89
531struct device_attribute;
532#line 89
533struct driver_attribute;
534#line 89 "include/linux/device.h"
535struct bus_type {
536 char const *name ;
537 char const *dev_name ;
538 struct device *dev_root ;
539 struct bus_attribute *bus_attrs ;
540 struct device_attribute *dev_attrs ;
541 struct driver_attribute *drv_attrs ;
542 int (*match)(struct device *dev , struct device_driver *drv ) ;
543 int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
544 int (*probe)(struct device *dev ) ;
545 int (*remove)(struct device *dev ) ;
546 void (*shutdown)(struct device *dev ) ;
547 int (*suspend)(struct device *dev , pm_message_t state ) ;
548 int (*resume)(struct device *dev ) ;
549 struct dev_pm_ops const *pm ;
550 struct iommu_ops *iommu_ops ;
551 struct subsys_private *p ;
552};
553#line 127
554struct device_type;
555#line 159
556struct notifier_block;
557#line 159
558struct notifier_block;
559#line 214
560struct of_device_id;
561#line 214 "include/linux/device.h"
562struct device_driver {
563 char const *name ;
564 struct bus_type *bus ;
565 struct module *owner ;
566 char const *mod_name ;
567 bool suppress_bind_attrs ;
568 struct of_device_id const *of_match_table ;
569 int (*probe)(struct device *dev ) ;
570 int (*remove)(struct device *dev ) ;
571 void (*shutdown)(struct device *dev ) ;
572 int (*suspend)(struct device *dev , pm_message_t state ) ;
573 int (*resume)(struct device *dev ) ;
574 struct attribute_group const **groups ;
575 struct dev_pm_ops const *pm ;
576 struct driver_private *p ;
577};
578#line 249 "include/linux/device.h"
579struct driver_attribute {
580 struct attribute attr ;
581 ssize_t (*show)(struct device_driver *driver , char *buf ) ;
582 ssize_t (*store)(struct device_driver *driver , char const *buf , size_t count ) ;
583};
584#line 330
585struct class_attribute;
586#line 330 "include/linux/device.h"
587struct class {
588 char const *name ;
589 struct module *owner ;
590 struct class_attribute *class_attrs ;
591 struct device_attribute *dev_attrs ;
592 struct bin_attribute *dev_bin_attrs ;
593 struct kobject *dev_kobj ;
594 int (*dev_uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
595 char *(*devnode)(struct device *dev , umode_t *mode ) ;
596 void (*class_release)(struct class *class ) ;
597 void (*dev_release)(struct device *dev ) ;
598 int (*suspend)(struct device *dev , pm_message_t state ) ;
599 int (*resume)(struct device *dev ) ;
600 struct kobj_ns_type_operations const *ns_type ;
601 void const *(*namespace)(struct device *dev ) ;
602 struct dev_pm_ops const *pm ;
603 struct subsys_private *p ;
604};
605#line 397 "include/linux/device.h"
606struct class_attribute {
607 struct attribute attr ;
608 ssize_t (*show)(struct class *class , struct class_attribute *attr , char *buf ) ;
609 ssize_t (*store)(struct class *class , struct class_attribute *attr , char const *buf ,
610 size_t count ) ;
611 void const *(*namespace)(struct class *class , struct class_attribute const *attr ) ;
612};
613#line 465 "include/linux/device.h"
614struct device_type {
615 char const *name ;
616 struct attribute_group const **groups ;
617 int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
618 char *(*devnode)(struct device *dev , umode_t *mode ) ;
619 void (*release)(struct device *dev ) ;
620 struct dev_pm_ops const *pm ;
621};
622#line 476 "include/linux/device.h"
623struct device_attribute {
624 struct attribute attr ;
625 ssize_t (*show)(struct device *dev , struct device_attribute *attr , char *buf ) ;
626 ssize_t (*store)(struct device *dev , struct device_attribute *attr , char const *buf ,
627 size_t count ) ;
628};
629#line 559 "include/linux/device.h"
630struct device_dma_parameters {
631 unsigned int max_segment_size ;
632 unsigned long segment_boundary_mask ;
633};
634#line 627
635struct dma_coherent_mem;
636#line 627 "include/linux/device.h"
637struct device {
638 struct device *parent ;
639 struct device_private *p ;
640 struct kobject kobj ;
641 char const *init_name ;
642 struct device_type const *type ;
643 struct mutex mutex ;
644 struct bus_type *bus ;
645 struct device_driver *driver ;
646 void *platform_data ;
647 struct dev_pm_info power ;
648 struct dev_pm_domain *pm_domain ;
649 int numa_node ;
650 u64 *dma_mask ;
651 u64 coherent_dma_mask ;
652 struct device_dma_parameters *dma_parms ;
653 struct list_head dma_pools ;
654 struct dma_coherent_mem *dma_mem ;
655 struct dev_archdata archdata ;
656 struct device_node *of_node ;
657 dev_t devt ;
658 u32 id ;
659 spinlock_t devres_lock ;
660 struct list_head devres_head ;
661 struct klist_node knode_class ;
662 struct class *class ;
663 struct attribute_group const **groups ;
664 void (*release)(struct device *dev ) ;
665};
666#line 43 "include/linux/pm_wakeup.h"
667struct wakeup_source {
668 char const *name ;
669 struct list_head entry ;
670 spinlock_t lock ;
671 struct timer_list timer ;
672 unsigned long timer_expires ;
673 ktime_t total_time ;
674 ktime_t max_time ;
675 ktime_t last_time ;
676 unsigned long event_count ;
677 unsigned long active_count ;
678 unsigned long relax_count ;
679 unsigned long hit_count ;
680 unsigned int active : 1 ;
681};
682#line 20 "include/linux/edac.h"
683struct device;
684#line 188 "include/linux/rcupdate.h"
685struct notifier_block;
686#line 50 "include/linux/notifier.h"
687struct notifier_block {
688 int (*notifier_call)(struct notifier_block * , unsigned long , void * ) ;
689 struct notifier_block *next ;
690 int priority ;
691};
692#line 10 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/x86_init.h"
693struct cpuinfo_x86;
694#line 103 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mpspec.h"
695struct device;
696#line 8 "include/linux/vmalloc.h"
697struct vm_area_struct;
698#line 10 "include/linux/gfp.h"
699struct vm_area_struct;
700#line 29 "include/linux/sysctl.h"
701struct completion;
702#line 49 "include/linux/kmod.h"
703struct file;
704#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
705struct task_struct;
706#line 18 "include/linux/elf.h"
707typedef __u64 Elf64_Addr;
708#line 19 "include/linux/elf.h"
709typedef __u16 Elf64_Half;
710#line 23 "include/linux/elf.h"
711typedef __u32 Elf64_Word;
712#line 24 "include/linux/elf.h"
713typedef __u64 Elf64_Xword;
714#line 194 "include/linux/elf.h"
715struct elf64_sym {
716 Elf64_Word st_name ;
717 unsigned char st_info ;
718 unsigned char st_other ;
719 Elf64_Half st_shndx ;
720 Elf64_Addr st_value ;
721 Elf64_Xword st_size ;
722};
723#line 194 "include/linux/elf.h"
724typedef struct elf64_sym Elf64_Sym;
725#line 438
726struct file;
727#line 39 "include/linux/moduleparam.h"
728struct kernel_param;
729#line 39
730struct kernel_param;
731#line 41 "include/linux/moduleparam.h"
732struct kernel_param_ops {
733 int (*set)(char const *val , struct kernel_param const *kp ) ;
734 int (*get)(char *buffer , struct kernel_param const *kp ) ;
735 void (*free)(void *arg ) ;
736};
737#line 50
738struct kparam_string;
739#line 50
740struct kparam_array;
741#line 50 "include/linux/moduleparam.h"
742union __anonunion____missing_field_name_199 {
743 void *arg ;
744 struct kparam_string const *str ;
745 struct kparam_array const *arr ;
746};
747#line 50 "include/linux/moduleparam.h"
748struct kernel_param {
749 char const *name ;
750 struct kernel_param_ops const *ops ;
751 u16 perm ;
752 s16 level ;
753 union __anonunion____missing_field_name_199 __annonCompField32 ;
754};
755#line 63 "include/linux/moduleparam.h"
756struct kparam_string {
757 unsigned int maxlen ;
758 char *string ;
759};
760#line 69 "include/linux/moduleparam.h"
761struct kparam_array {
762 unsigned int max ;
763 unsigned int elemsize ;
764 unsigned int *num ;
765 struct kernel_param_ops const *ops ;
766 void *elem ;
767};
768#line 445
769struct module;
770#line 80 "include/linux/jump_label.h"
771struct module;
772#line 143 "include/linux/jump_label.h"
773struct static_key {
774 atomic_t enabled ;
775};
776#line 22 "include/linux/tracepoint.h"
777struct module;
778#line 23
779struct tracepoint;
780#line 23
781struct tracepoint;
782#line 25 "include/linux/tracepoint.h"
783struct tracepoint_func {
784 void *func ;
785 void *data ;
786};
787#line 30 "include/linux/tracepoint.h"
788struct tracepoint {
789 char const *name ;
790 struct static_key key ;
791 void (*regfunc)(void) ;
792 void (*unregfunc)(void) ;
793 struct tracepoint_func *funcs ;
794};
795#line 19 "include/linux/export.h"
796struct kernel_symbol {
797 unsigned long value ;
798 char const *name ;
799};
800#line 8 "include/asm-generic/module.h"
801struct mod_arch_specific {
802
803};
804#line 35 "include/linux/module.h"
805struct module;
806#line 37
807struct module_param_attrs;
808#line 37 "include/linux/module.h"
809struct module_kobject {
810 struct kobject kobj ;
811 struct module *mod ;
812 struct kobject *drivers_dir ;
813 struct module_param_attrs *mp ;
814};
815#line 44 "include/linux/module.h"
816struct module_attribute {
817 struct attribute attr ;
818 ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
819 ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const * ,
820 size_t count ) ;
821 void (*setup)(struct module * , char const * ) ;
822 int (*test)(struct module * ) ;
823 void (*free)(struct module * ) ;
824};
825#line 71
826struct exception_table_entry;
827#line 71
828struct exception_table_entry;
829#line 182
830struct notifier_block;
831#line 199
832enum module_state {
833 MODULE_STATE_LIVE = 0,
834 MODULE_STATE_COMING = 1,
835 MODULE_STATE_GOING = 2
836} ;
837#line 215 "include/linux/module.h"
838struct module_ref {
839 unsigned long incs ;
840 unsigned long decs ;
841} __attribute__((__aligned__((2) * (sizeof(unsigned long )) ))) ;
842#line 220
843struct module_sect_attrs;
844#line 220
845struct module_notes_attrs;
846#line 220
847struct ftrace_event_call;
848#line 220 "include/linux/module.h"
849struct module {
850 enum module_state state ;
851 struct list_head list ;
852 char name[64UL - sizeof(unsigned long )] ;
853 struct module_kobject mkobj ;
854 struct module_attribute *modinfo_attrs ;
855 char const *version ;
856 char const *srcversion ;
857 struct kobject *holders_dir ;
858 struct kernel_symbol const *syms ;
859 unsigned long const *crcs ;
860 unsigned int num_syms ;
861 struct kernel_param *kp ;
862 unsigned int num_kp ;
863 unsigned int num_gpl_syms ;
864 struct kernel_symbol const *gpl_syms ;
865 unsigned long const *gpl_crcs ;
866 struct kernel_symbol const *unused_syms ;
867 unsigned long const *unused_crcs ;
868 unsigned int num_unused_syms ;
869 unsigned int num_unused_gpl_syms ;
870 struct kernel_symbol const *unused_gpl_syms ;
871 unsigned long const *unused_gpl_crcs ;
872 struct kernel_symbol const *gpl_future_syms ;
873 unsigned long const *gpl_future_crcs ;
874 unsigned int num_gpl_future_syms ;
875 unsigned int num_exentries ;
876 struct exception_table_entry *extable ;
877 int (*init)(void) ;
878 void *module_init ;
879 void *module_core ;
880 unsigned int init_size ;
881 unsigned int core_size ;
882 unsigned int init_text_size ;
883 unsigned int core_text_size ;
884 unsigned int init_ro_size ;
885 unsigned int core_ro_size ;
886 struct mod_arch_specific arch ;
887 unsigned int taints ;
888 unsigned int num_bugs ;
889 struct list_head bug_list ;
890 struct bug_entry *bug_table ;
891 Elf64_Sym *symtab ;
892 Elf64_Sym *core_symtab ;
893 unsigned int num_symtab ;
894 unsigned int core_num_syms ;
895 char *strtab ;
896 char *core_strtab ;
897 struct module_sect_attrs *sect_attrs ;
898 struct module_notes_attrs *notes_attrs ;
899 char *args ;
900 void *percpu ;
901 unsigned int percpu_size ;
902 unsigned int num_tracepoints ;
903 struct tracepoint * const *tracepoints_ptrs ;
904 unsigned int num_trace_bprintk_fmt ;
905 char const **trace_bprintk_fmt_start ;
906 struct ftrace_event_call **trace_events ;
907 unsigned int num_trace_events ;
908 struct list_head source_list ;
909 struct list_head target_list ;
910 struct task_struct *waiter ;
911 void (*exit)(void) ;
912 struct module_ref *refptr ;
913 ctor_fn_t *ctors ;
914 unsigned int num_ctors ;
915};
916#line 60 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mce.h"
917struct mce {
918 __u64 status ;
919 __u64 misc ;
920 __u64 addr ;
921 __u64 mcgstatus ;
922 __u64 ip ;
923 __u64 tsc ;
924 __u64 time ;
925 __u8 cpuvendor ;
926 __u8 inject_flags ;
927 __u16 pad ;
928 __u32 cpuid ;
929 __u8 cs ;
930 __u8 bank ;
931 __u8 cpu ;
932 __u8 finished ;
933 __u32 extcpu ;
934 __u32 socketid ;
935 __u32 apicid ;
936 __u64 mcgcap ;
937};
938#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/drivers/edac/mce_amd_inj.c.common.c"
939struct edac_mce_attr {
940 struct attribute attr ;
941 ssize_t (*show)(struct kobject *kobj , struct edac_mce_attr *attr , char *buf ) ;
942 ssize_t (*store)(struct kobject *kobj , struct edac_mce_attr *attr , char const *buf ,
943 size_t count ) ;
944};
945#line 134 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/drivers/edac/mce_amd_inj.c.common.c"
946struct __anonstruct_201 {
947 int : 0 ;
948};
949#line 160 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/drivers/edac/mce_amd_inj.c.common.c"
950struct __anonstruct_202 {
951 int : 0 ;
952};
953#line 1 "<compiler builtins>"
954long __builtin_expect(long val , long res ) ;
955#line 100 "include/linux/printk.h"
956extern int ( printk)(char const *fmt , ...) ;
957#line 215 "include/linux/kernel.h"
958extern int __attribute__((__warn_unused_result__)) _kstrtoul(char const *s , unsigned int base ,
959 unsigned long *res ) ;
960#line 218
961extern int __attribute__((__warn_unused_result__)) kstrtoull(char const *s , unsigned int base ,
962 unsigned long long *res ) ;
963#line 220
964__inline static int __attribute__((__warn_unused_result__)) kstrtoul(char const *s ,
965 unsigned int base ,
966 unsigned long *res ) __attribute__((__no_instrument_function__)) ;
967#line 220 "include/linux/kernel.h"
968__inline static int __attribute__((__warn_unused_result__)) kstrtoul(char const *s ,
969 unsigned int base ,
970 unsigned long *res )
971{ int tmp ;
972 int tmp___0 ;
973 unsigned long long *__cil_tmp6 ;
974
975 {
976#line 226
977 if (8UL == 8UL) {
978#line 226
979 if (8UL == 8UL) {
980 {
981#line 228
982 __cil_tmp6 = (unsigned long long *)res;
983#line 228
984 tmp = (int )kstrtoull(s, base, __cil_tmp6);
985 }
986#line 228
987 return (tmp);
988 } else {
989 {
990#line 230
991 tmp___0 = (int )_kstrtoul(s, base, res);
992 }
993#line 230
994 return (tmp___0);
995 }
996 } else {
997 {
998#line 230
999 tmp___0 = (int )_kstrtoul(s, base, res);
1000 }
1001#line 230
1002 return (tmp___0);
1003 }
1004}
1005}
1006#line 320
1007extern int ( sprintf)(char *buf , char const *fmt , ...) ;
1008#line 138 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
1009extern struct cpuinfo_x86 boot_cpu_data ;
1010#line 131 "include/linux/sysfs.h"
1011extern int __attribute__((__warn_unused_result__)) sysfs_create_file(struct kobject *kobj ,
1012 struct attribute const *attr ) ;
1013#line 137
1014extern void sysfs_remove_file(struct kobject *kobj , struct attribute const *attr ) ;
1015#line 94 "include/linux/kobject.h"
1016extern void kobject_del(struct kobject *kobj ) ;
1017#line 97
1018extern struct kobject * __attribute__((__warn_unused_result__)) kobject_create_and_add(char const *name ,
1019 struct kobject *parent ) ;
1020#line 152 "include/linux/mutex.h"
1021void mutex_lock(struct mutex *lock ) ;
1022#line 153
1023int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock ) ;
1024#line 154
1025int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock ) ;
1026#line 168
1027int mutex_trylock(struct mutex *lock ) ;
1028#line 169
1029void mutex_unlock(struct mutex *lock ) ;
1030#line 170
1031int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
1032#line 34 "include/linux/edac.h"
1033extern struct bus_type *edac_get_sysfs_subsys(void) ;
1034#line 35
1035extern void edac_put_sysfs_subsys(void) ;
1036#line 67 "include/linux/module.h"
1037int init_module(void) ;
1038#line 68
1039void cleanup_module(void) ;
1040#line 91 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/edac/mce_amd.h"
1041extern int amd_decode_mce(struct notifier_block *nb , unsigned long val , void *data ) ;
1042#line 32 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/drivers/edac/mce_amd_inj.c.common.c"
1043static struct kobject *mce_kobj ;
1044#line 37 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/drivers/edac/mce_amd_inj.c.common.c"
1045static struct mce i_mce ;
1046#line 56 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/drivers/edac/mce_amd_inj.c.common.c"
1047static ssize_t edac_inject_status_store(struct kobject *kobj , struct edac_mce_attr *attr ,
1048 char const *data , size_t count )
1049{ int ret ;
1050 unsigned long value ;
1051 struct mce *__cil_tmp7 ;
1052 unsigned long *__cil_tmp8 ;
1053 unsigned long __cil_tmp9 ;
1054
1055 {
1056 {
1057#line 56
1058 ret = 0;
1059#line 56
1060 ret = (int )kstrtoul(data, 16U, & value);
1061 }
1062#line 56
1063 if (ret < 0) {
1064 {
1065#line 56
1066 printk("<3>Error writing MCE status field.\n");
1067 }
1068 } else {
1069
1070 }
1071#line 56
1072 __cil_tmp7 = & i_mce;
1073#line 56
1074 __cil_tmp8 = & value;
1075#line 56
1076 __cil_tmp9 = *__cil_tmp8;
1077#line 56
1078 *((__u64 *)__cil_tmp7) = (__u64 )__cil_tmp9;
1079#line 56
1080 return ((ssize_t )count);
1081}
1082}
1083#line 57 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/drivers/edac/mce_amd_inj.c.common.c"
1084static ssize_t edac_inject_misc_store(struct kobject *kobj , struct edac_mce_attr *attr ,
1085 char const *data , size_t count )
1086{ int ret ;
1087 unsigned long value ;
1088 unsigned long __cil_tmp7 ;
1089 unsigned long *__cil_tmp8 ;
1090 unsigned long __cil_tmp9 ;
1091
1092 {
1093 {
1094#line 57
1095 ret = 0;
1096#line 57
1097 ret = (int )kstrtoul(data, 16U, & value);
1098 }
1099#line 57
1100 if (ret < 0) {
1101 {
1102#line 57
1103 printk("<3>Error writing MCE misc field.\n");
1104 }
1105 } else {
1106
1107 }
1108#line 57
1109 __cil_tmp7 = (unsigned long )(& i_mce) + 8;
1110#line 57
1111 __cil_tmp8 = & value;
1112#line 57
1113 __cil_tmp9 = *__cil_tmp8;
1114#line 57
1115 *((__u64 *)__cil_tmp7) = (__u64 )__cil_tmp9;
1116#line 57
1117 return ((ssize_t )count);
1118}
1119}
1120#line 58 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/drivers/edac/mce_amd_inj.c.common.c"
1121static ssize_t edac_inject_addr_store(struct kobject *kobj , struct edac_mce_attr *attr ,
1122 char const *data , size_t count )
1123{ int ret ;
1124 unsigned long value ;
1125 unsigned long __cil_tmp7 ;
1126 unsigned long *__cil_tmp8 ;
1127 unsigned long __cil_tmp9 ;
1128
1129 {
1130 {
1131#line 58
1132 ret = 0;
1133#line 58
1134 ret = (int )kstrtoul(data, 16U, & value);
1135 }
1136#line 58
1137 if (ret < 0) {
1138 {
1139#line 58
1140 printk("<3>Error writing MCE addr field.\n");
1141 }
1142 } else {
1143
1144 }
1145#line 58
1146 __cil_tmp7 = (unsigned long )(& i_mce) + 16;
1147#line 58
1148 __cil_tmp8 = & value;
1149#line 58
1150 __cil_tmp9 = *__cil_tmp8;
1151#line 58
1152 *((__u64 *)__cil_tmp7) = (__u64 )__cil_tmp9;
1153#line 58
1154 return ((ssize_t )count);
1155}
1156}
1157#line 68 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/drivers/edac/mce_amd_inj.c.common.c"
1158static ssize_t edac_inject_status_show(struct kobject *kobj , struct edac_mce_attr *attr ,
1159 char *buf )
1160{ int tmp ;
1161 struct mce *__cil_tmp5 ;
1162 __u64 __cil_tmp6 ;
1163
1164 {
1165 {
1166#line 68
1167 __cil_tmp5 = & i_mce;
1168#line 68
1169 __cil_tmp6 = *((__u64 *)__cil_tmp5);
1170#line 68
1171 tmp = sprintf(buf, "0x%016llx\n", __cil_tmp6);
1172 }
1173#line 68
1174 return ((ssize_t )tmp);
1175}
1176}
1177#line 69 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/drivers/edac/mce_amd_inj.c.common.c"
1178static ssize_t edac_inject_misc_show(struct kobject *kobj , struct edac_mce_attr *attr ,
1179 char *buf )
1180{ int tmp ;
1181 unsigned long __cil_tmp5 ;
1182 __u64 __cil_tmp6 ;
1183
1184 {
1185 {
1186#line 69
1187 __cil_tmp5 = (unsigned long )(& i_mce) + 8;
1188#line 69
1189 __cil_tmp6 = *((__u64 *)__cil_tmp5);
1190#line 69
1191 tmp = sprintf(buf, "0x%016llx\n", __cil_tmp6);
1192 }
1193#line 69
1194 return ((ssize_t )tmp);
1195}
1196}
1197#line 70 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/drivers/edac/mce_amd_inj.c.common.c"
1198static ssize_t edac_inject_addr_show(struct kobject *kobj , struct edac_mce_attr *attr ,
1199 char *buf )
1200{ int tmp ;
1201 unsigned long __cil_tmp5 ;
1202 __u64 __cil_tmp6 ;
1203
1204 {
1205 {
1206#line 70
1207 __cil_tmp5 = (unsigned long )(& i_mce) + 16;
1208#line 70
1209 __cil_tmp6 = *((__u64 *)__cil_tmp5);
1210#line 70
1211 tmp = sprintf(buf, "0x%016llx\n", __cil_tmp6);
1212 }
1213#line 70
1214 return ((ssize_t )tmp);
1215}
1216}
1217#line 72 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/drivers/edac/mce_amd_inj.c.common.c"
1218static struct edac_mce_attr mce_attr_status = {{"status", (umode_t )420}, & edac_inject_status_show, & edac_inject_status_store};
1219#line 73 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/drivers/edac/mce_amd_inj.c.common.c"
1220static struct edac_mce_attr mce_attr_misc = {{"misc", (umode_t )420}, & edac_inject_misc_show, & edac_inject_misc_store};
1221#line 74 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/drivers/edac/mce_amd_inj.c.common.c"
1222static struct edac_mce_attr mce_attr_addr = {{"addr", (umode_t )420}, & edac_inject_addr_show, & edac_inject_addr_store};
1223#line 80 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/drivers/edac/mce_amd_inj.c.common.c"
1224static ssize_t edac_inject_bank_store(struct kobject *kobj , struct edac_mce_attr *attr ,
1225 char const *data , size_t count )
1226{ int ret ;
1227 unsigned long value ;
1228 unsigned long *__cil_tmp7 ;
1229 unsigned long __cil_tmp8 ;
1230 struct cpuinfo_x86 *__cil_tmp9 ;
1231 __u8 __cil_tmp10 ;
1232 int __cil_tmp11 ;
1233 unsigned long *__cil_tmp12 ;
1234 unsigned long __cil_tmp13 ;
1235 unsigned long *__cil_tmp14 ;
1236 unsigned long __cil_tmp15 ;
1237 unsigned long *__cil_tmp16 ;
1238 unsigned long __cil_tmp17 ;
1239 unsigned long __cil_tmp18 ;
1240 unsigned long *__cil_tmp19 ;
1241 unsigned long __cil_tmp20 ;
1242 void *__cil_tmp21 ;
1243 struct notifier_block *__cil_tmp22 ;
1244 void *__cil_tmp23 ;
1245
1246 {
1247 {
1248#line 84
1249 ret = 0;
1250#line 87
1251 ret = (int )kstrtoul(data, 10U, & value);
1252 }
1253#line 88
1254 if (ret < 0) {
1255 {
1256#line 89
1257 printk("<3>Invalid bank value!\n");
1258 }
1259#line 90
1260 return ((ssize_t )-22);
1261 } else {
1262
1263 }
1264 {
1265#line 93
1266 __cil_tmp7 = & value;
1267#line 93
1268 __cil_tmp8 = *__cil_tmp7;
1269#line 93
1270 if (__cil_tmp8 > 5UL) {
1271 {
1272#line 94
1273 __cil_tmp9 = & boot_cpu_data;
1274#line 94
1275 __cil_tmp10 = *((__u8 *)__cil_tmp9);
1276#line 94
1277 __cil_tmp11 = (int )__cil_tmp10;
1278#line 94
1279 if (__cil_tmp11 != 21) {
1280 {
1281#line 95
1282 __cil_tmp12 = & value;
1283#line 95
1284 __cil_tmp13 = *__cil_tmp12;
1285#line 95
1286 printk("<3>Non-existent MCE bank: %lu\n", __cil_tmp13);
1287 }
1288#line 96
1289 return ((ssize_t )-22);
1290 } else {
1291 {
1292#line 94
1293 __cil_tmp14 = & value;
1294#line 94
1295 __cil_tmp15 = *__cil_tmp14;
1296#line 94
1297 if (__cil_tmp15 > 6UL) {
1298 {
1299#line 95
1300 __cil_tmp16 = & value;
1301#line 95
1302 __cil_tmp17 = *__cil_tmp16;
1303#line 95
1304 printk("<3>Non-existent MCE bank: %lu\n", __cil_tmp17);
1305 }
1306#line 96
1307 return ((ssize_t )-22);
1308 } else {
1309
1310 }
1311 }
1312 }
1313 }
1314 } else {
1315
1316 }
1317 }
1318 {
1319#line 99
1320 __cil_tmp18 = (unsigned long )(& i_mce) + 65;
1321#line 99
1322 __cil_tmp19 = & value;
1323#line 99
1324 __cil_tmp20 = *__cil_tmp19;
1325#line 99
1326 *((__u8 *)__cil_tmp18) = (__u8 )__cil_tmp20;
1327#line 101
1328 __cil_tmp21 = (void *)0;
1329#line 101
1330 __cil_tmp22 = (struct notifier_block *)__cil_tmp21;
1331#line 101
1332 __cil_tmp23 = (void *)(& i_mce);
1333#line 101
1334 amd_decode_mce(__cil_tmp22, 0UL, __cil_tmp23);
1335 }
1336#line 103
1337 return ((ssize_t )count);
1338}
1339}
1340#line 106 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/drivers/edac/mce_amd_inj.c.common.c"
1341static ssize_t edac_inject_bank_show(struct kobject *kobj , struct edac_mce_attr *attr ,
1342 char *buf )
1343{ int tmp ;
1344 unsigned long __cil_tmp5 ;
1345 __u8 __cil_tmp6 ;
1346 int __cil_tmp7 ;
1347
1348 {
1349 {
1350#line 109
1351 __cil_tmp5 = (unsigned long )(& i_mce) + 65;
1352#line 109
1353 __cil_tmp6 = *((__u8 *)__cil_tmp5);
1354#line 109
1355 __cil_tmp7 = (int )__cil_tmp6;
1356#line 109
1357 tmp = sprintf(buf, "%d\n", __cil_tmp7);
1358 }
1359#line 109
1360 return ((ssize_t )tmp);
1361}
1362}
1363#line 112 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/drivers/edac/mce_amd_inj.c.common.c"
1364static struct edac_mce_attr mce_attr_bank = {{"bank", (umode_t )420}, & edac_inject_bank_show, & edac_inject_bank_store};
1365#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/drivers/edac/mce_amd_inj.c.common.c"
1366static struct edac_mce_attr *sysfs_attrs[4] = { & mce_attr_status, & mce_attr_misc, & mce_attr_addr, & mce_attr_bank};
1367#line 118
1368static int edac_init_mce_inject(void) __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
1369#line 118 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/drivers/edac/mce_amd_inj.c.common.c"
1370static int edac_init_mce_inject(void)
1371{ struct bus_type *edac_subsys___0 ;
1372 int i ;
1373 int err ;
1374 void *__cil_tmp4 ;
1375 unsigned long __cil_tmp5 ;
1376 unsigned long __cil_tmp6 ;
1377 struct device *__cil_tmp7 ;
1378 unsigned long __cil_tmp8 ;
1379 unsigned long __cil_tmp9 ;
1380 struct kobject *__cil_tmp10 ;
1381 unsigned long __cil_tmp11 ;
1382 unsigned long __cil_tmp12 ;
1383 unsigned long __cil_tmp13 ;
1384 unsigned long __cil_tmp14 ;
1385 unsigned long __cil_tmp15 ;
1386 struct edac_mce_attr *__cil_tmp16 ;
1387 struct attribute *__cil_tmp17 ;
1388 struct attribute const *__cil_tmp18 ;
1389 unsigned long __cil_tmp19 ;
1390 unsigned long __cil_tmp20 ;
1391 struct edac_mce_attr *__cil_tmp21 ;
1392 char const *__cil_tmp22 ;
1393 unsigned long __cil_tmp23 ;
1394 unsigned long __cil_tmp24 ;
1395 struct edac_mce_attr *__cil_tmp25 ;
1396 struct attribute *__cil_tmp26 ;
1397 struct attribute const *__cil_tmp27 ;
1398
1399 {
1400 {
1401#line 120
1402 __cil_tmp4 = (void *)0;
1403#line 120
1404 edac_subsys___0 = (struct bus_type *)__cil_tmp4;
1405#line 121
1406 err = 0;
1407#line 123
1408 edac_subsys___0 = edac_get_sysfs_subsys();
1409 }
1410#line 124
1411 if (! edac_subsys___0) {
1412#line 125
1413 return (-22);
1414 } else {
1415
1416 }
1417 {
1418#line 127
1419 __cil_tmp5 = (unsigned long )edac_subsys___0;
1420#line 127
1421 __cil_tmp6 = __cil_tmp5 + 16;
1422#line 127
1423 __cil_tmp7 = *((struct device **)__cil_tmp6);
1424#line 127
1425 __cil_tmp8 = (unsigned long )__cil_tmp7;
1426#line 127
1427 __cil_tmp9 = __cil_tmp8 + 16;
1428#line 127
1429 __cil_tmp10 = (struct kobject *)__cil_tmp9;
1430#line 127
1431 mce_kobj = (struct kobject *)kobject_create_and_add("mce", __cil_tmp10);
1432 }
1433#line 128
1434 if (! mce_kobj) {
1435 {
1436#line 129
1437 printk("<3>Error creating a mce kset.\n");
1438#line 130
1439 err = -12;
1440 }
1441#line 131
1442 goto err_mce_kobj;
1443 } else {
1444
1445 }
1446#line 134
1447 i = 0;
1448 {
1449#line 134
1450 while (1) {
1451 while_continue: ;
1452 {
1453#line 134
1454 __cil_tmp11 = 32UL / 8UL;
1455#line 134
1456 __cil_tmp12 = __cil_tmp11 + 0UL;
1457#line 134
1458 __cil_tmp13 = (unsigned long )i;
1459#line 134
1460 if (__cil_tmp13 < __cil_tmp12) {
1461
1462 } else {
1463#line 134
1464 goto while_break;
1465 }
1466 }
1467 {
1468#line 135
1469 __cil_tmp14 = i * 8UL;
1470#line 135
1471 __cil_tmp15 = (unsigned long )(sysfs_attrs) + __cil_tmp14;
1472#line 135
1473 __cil_tmp16 = *((struct edac_mce_attr **)__cil_tmp15);
1474#line 135
1475 __cil_tmp17 = (struct attribute *)__cil_tmp16;
1476#line 135
1477 __cil_tmp18 = (struct attribute const *)__cil_tmp17;
1478#line 135
1479 err = (int )sysfs_create_file(mce_kobj, __cil_tmp18);
1480 }
1481#line 136
1482 if (err) {
1483 {
1484#line 137
1485 __cil_tmp19 = i * 8UL;
1486#line 137
1487 __cil_tmp20 = (unsigned long )(sysfs_attrs) + __cil_tmp19;
1488#line 137
1489 __cil_tmp21 = *((struct edac_mce_attr **)__cil_tmp20);
1490#line 137
1491 __cil_tmp22 = *((char const **)__cil_tmp21);
1492#line 137
1493 printk("<3>Error creating %s in sysfs.\n", __cil_tmp22);
1494 }
1495#line 139
1496 goto err_sysfs_create;
1497 } else {
1498
1499 }
1500#line 134
1501 i = i + 1;
1502 }
1503 while_break: ;
1504 }
1505#line 142
1506 return (0);
1507 err_sysfs_create:
1508 {
1509#line 145
1510 while (1) {
1511 while_continue___0: ;
1512#line 145
1513 i = i - 1;
1514#line 145
1515 if (i >= 0) {
1516
1517 } else {
1518#line 145
1519 goto while_break___0;
1520 }
1521 {
1522#line 146
1523 __cil_tmp23 = i * 8UL;
1524#line 146
1525 __cil_tmp24 = (unsigned long )(sysfs_attrs) + __cil_tmp23;
1526#line 146
1527 __cil_tmp25 = *((struct edac_mce_attr **)__cil_tmp24);
1528#line 146
1529 __cil_tmp26 = (struct attribute *)__cil_tmp25;
1530#line 146
1531 __cil_tmp27 = (struct attribute const *)__cil_tmp26;
1532#line 146
1533 sysfs_remove_file(mce_kobj, __cil_tmp27);
1534 }
1535 }
1536 while_break___0: ;
1537 }
1538 {
1539#line 148
1540 kobject_del(mce_kobj);
1541 }
1542 err_mce_kobj:
1543 {
1544#line 151
1545 edac_put_sysfs_subsys();
1546 }
1547#line 153
1548 return (err);
1549}
1550}
1551#line 156
1552static void edac_exit_mce_inject(void) __attribute__((__section__(".exit.text"),
1553__no_instrument_function__)) ;
1554#line 156 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/drivers/edac/mce_amd_inj.c.common.c"
1555static void edac_exit_mce_inject(void)
1556{ int i ;
1557 unsigned long __cil_tmp2 ;
1558 unsigned long __cil_tmp3 ;
1559 unsigned long __cil_tmp4 ;
1560 unsigned long __cil_tmp5 ;
1561 unsigned long __cil_tmp6 ;
1562 struct edac_mce_attr *__cil_tmp7 ;
1563 struct attribute *__cil_tmp8 ;
1564 struct attribute const *__cil_tmp9 ;
1565
1566 {
1567#line 160
1568 i = 0;
1569 {
1570#line 160
1571 while (1) {
1572 while_continue: ;
1573 {
1574#line 160
1575 __cil_tmp2 = 32UL / 8UL;
1576#line 160
1577 __cil_tmp3 = __cil_tmp2 + 0UL;
1578#line 160
1579 __cil_tmp4 = (unsigned long )i;
1580#line 160
1581 if (__cil_tmp4 < __cil_tmp3) {
1582
1583 } else {
1584#line 160
1585 goto while_break;
1586 }
1587 }
1588 {
1589#line 161
1590 __cil_tmp5 = i * 8UL;
1591#line 161
1592 __cil_tmp6 = (unsigned long )(sysfs_attrs) + __cil_tmp5;
1593#line 161
1594 __cil_tmp7 = *((struct edac_mce_attr **)__cil_tmp6);
1595#line 161
1596 __cil_tmp8 = (struct attribute *)__cil_tmp7;
1597#line 161
1598 __cil_tmp9 = (struct attribute const *)__cil_tmp8;
1599#line 161
1600 sysfs_remove_file(mce_kobj, __cil_tmp9);
1601#line 160
1602 i = i + 1;
1603 }
1604 }
1605 while_break: ;
1606 }
1607 {
1608#line 163
1609 kobject_del(mce_kobj);
1610#line 165
1611 edac_put_sysfs_subsys();
1612 }
1613#line 166
1614 return;
1615}
1616}
1617#line 168 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/drivers/edac/mce_amd_inj.c.common.c"
1618int init_module(void)
1619{ int tmp ;
1620
1621 {
1622 {
1623#line 168
1624 tmp = edac_init_mce_inject();
1625 }
1626#line 168
1627 return (tmp);
1628}
1629}
1630#line 169 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/drivers/edac/mce_amd_inj.c.common.c"
1631void cleanup_module(void)
1632{
1633
1634 {
1635 {
1636#line 169
1637 edac_exit_mce_inject();
1638 }
1639#line 169
1640 return;
1641}
1642}
1643#line 171 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/drivers/edac/mce_amd_inj.c.common.c"
1644static char const __mod_license171[12] __attribute__((__used__, __unused__, __section__(".modinfo"),
1645__aligned__(1))) =
1646#line 171
1647 { (char const )'l', (char const )'i', (char const )'c', (char const )'e',
1648 (char const )'n', (char const )'s', (char const )'e', (char const )'=',
1649 (char const )'G', (char const )'P', (char const )'L', (char const )'\000'};
1650#line 172 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/drivers/edac/mce_amd_inj.c.common.c"
1651static char const __mod_author172[49] __attribute__((__used__, __unused__, __section__(".modinfo"),
1652__aligned__(1))) =
1653#line 172
1654 { (char const )'a', (char const )'u', (char const )'t', (char const )'h',
1655 (char const )'o', (char const )'r', (char const )'=', (char const )'B',
1656 (char const )'o', (char const )'r', (char const )'i', (char const )'s',
1657 (char const )'l', (char const )'a', (char const )'v', (char const )' ',
1658 (char const )'P', (char const )'e', (char const )'t', (char const )'k',
1659 (char const )'o', (char const )'v', (char const )' ', (char const )'<',
1660 (char const )'b', (char const )'o', (char const )'r', (char const )'i',
1661 (char const )'s', (char const )'l', (char const )'a', (char const )'v',
1662 (char const )'.', (char const )'p', (char const )'e', (char const )'t',
1663 (char const )'k', (char const )'o', (char const )'v', (char const )'@',
1664 (char const )'a', (char const )'m', (char const )'d', (char const )'.',
1665 (char const )'c', (char const )'o', (char const )'m', (char const )'>',
1666 (char const )'\000'};
1667#line 173 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/drivers/edac/mce_amd_inj.c.common.c"
1668static char const __mod_author173[16] __attribute__((__used__, __unused__, __section__(".modinfo"),
1669__aligned__(1))) =
1670#line 173
1671 { (char const )'a', (char const )'u', (char const )'t', (char const )'h',
1672 (char const )'o', (char const )'r', (char const )'=', (char const )'A',
1673 (char const )'M', (char const )'D', (char const )' ', (char const )'I',
1674 (char const )'n', (char const )'c', (char const )'.', (char const )'\000'};
1675#line 174 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/drivers/edac/mce_amd_inj.c.common.c"
1676static char const __mod_description174[60] __attribute__((__used__, __unused__,
1677__section__(".modinfo"), __aligned__(1))) =
1678#line 174
1679 { (char const )'d', (char const )'e', (char const )'s', (char const )'c',
1680 (char const )'r', (char const )'i', (char const )'p', (char const )'t',
1681 (char const )'i', (char const )'o', (char const )'n', (char const )'=',
1682 (char const )'M', (char const )'C', (char const )'E', (char const )' ',
1683 (char const )'i', (char const )'n', (char const )'j', (char const )'e',
1684 (char const )'c', (char const )'t', (char const )'i', (char const )'o',
1685 (char const )'n', (char const )' ', (char const )'f', (char const )'a',
1686 (char const )'c', (char const )'i', (char const )'l', (char const )'i',
1687 (char const )'t', (char const )'y', (char const )' ', (char const )'f',
1688 (char const )'o', (char const )'r', (char const )' ', (char const )'t',
1689 (char const )'e', (char const )'s', (char const )'t', (char const )'i',
1690 (char const )'n', (char const )'g', (char const )' ', (char const )'M',
1691 (char const )'C', (char const )'E', (char const )' ', (char const )'d',
1692 (char const )'e', (char const )'c', (char const )'o', (char const )'d',
1693 (char const )'i', (char const )'n', (char const )'g', (char const )'\000'};
1694#line 192
1695void ldv_check_final_state(void) ;
1696#line 198
1697extern void ldv_initialize(void) ;
1698#line 201
1699extern int __VERIFIER_nondet_int(void) ;
1700#line 204 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/drivers/edac/mce_amd_inj.c.common.c"
1701int LDV_IN_INTERRUPT ;
1702#line 207 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/drivers/edac/mce_amd_inj.c.common.c"
1703void main(void)
1704{ int tmp ;
1705 int tmp___0 ;
1706 int tmp___1 ;
1707
1708 {
1709 {
1710#line 219
1711 LDV_IN_INTERRUPT = 1;
1712#line 228
1713 ldv_initialize();
1714#line 260
1715 tmp = edac_init_mce_inject();
1716 }
1717#line 260
1718 if (tmp) {
1719#line 261
1720 goto ldv_final;
1721 } else {
1722
1723 }
1724 {
1725#line 263
1726 while (1) {
1727 while_continue: ;
1728 {
1729#line 263
1730 tmp___1 = __VERIFIER_nondet_int();
1731 }
1732#line 263
1733 if (tmp___1) {
1734
1735 } else {
1736#line 263
1737 goto while_break;
1738 }
1739 {
1740#line 266
1741 tmp___0 = __VERIFIER_nondet_int();
1742 }
1743 {
1744#line 268
1745 goto switch_default;
1746#line 266
1747 if (0) {
1748 switch_default:
1749#line 268
1750 goto switch_break;
1751 } else {
1752 switch_break: ;
1753 }
1754 }
1755 }
1756 while_break: ;
1757 }
1758 {
1759#line 306
1760 edac_exit_mce_inject();
1761 }
1762 ldv_final:
1763 {
1764#line 309
1765 ldv_check_final_state();
1766 }
1767#line 312
1768 return;
1769}
1770}
1771#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
1772void ldv_blast_assert(void)
1773{
1774
1775 {
1776 ERROR:
1777#line 6
1778 goto ERROR;
1779}
1780}
1781#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
1782extern int __VERIFIER_nondet_int(void) ;
1783#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1784int ldv_mutex = 1;
1785#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1786int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )
1787{ int nondetermined ;
1788
1789 {
1790#line 29
1791 if (ldv_mutex == 1) {
1792
1793 } else {
1794 {
1795#line 29
1796 ldv_blast_assert();
1797 }
1798 }
1799 {
1800#line 32
1801 nondetermined = __VERIFIER_nondet_int();
1802 }
1803#line 35
1804 if (nondetermined) {
1805#line 38
1806 ldv_mutex = 2;
1807#line 40
1808 return (0);
1809 } else {
1810#line 45
1811 return (-4);
1812 }
1813}
1814}
1815#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1816int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock )
1817{ int nondetermined ;
1818
1819 {
1820#line 57
1821 if (ldv_mutex == 1) {
1822
1823 } else {
1824 {
1825#line 57
1826 ldv_blast_assert();
1827 }
1828 }
1829 {
1830#line 60
1831 nondetermined = __VERIFIER_nondet_int();
1832 }
1833#line 63
1834 if (nondetermined) {
1835#line 66
1836 ldv_mutex = 2;
1837#line 68
1838 return (0);
1839 } else {
1840#line 73
1841 return (-4);
1842 }
1843}
1844}
1845#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1846int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock )
1847{ int atomic_value_after_dec ;
1848
1849 {
1850#line 83
1851 if (ldv_mutex == 1) {
1852
1853 } else {
1854 {
1855#line 83
1856 ldv_blast_assert();
1857 }
1858 }
1859 {
1860#line 86
1861 atomic_value_after_dec = __VERIFIER_nondet_int();
1862 }
1863#line 89
1864 if (atomic_value_after_dec == 0) {
1865#line 92
1866 ldv_mutex = 2;
1867#line 94
1868 return (1);
1869 } else {
1870
1871 }
1872#line 98
1873 return (0);
1874}
1875}
1876#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1877void mutex_lock(struct mutex *lock )
1878{
1879
1880 {
1881#line 108
1882 if (ldv_mutex == 1) {
1883
1884 } else {
1885 {
1886#line 108
1887 ldv_blast_assert();
1888 }
1889 }
1890#line 110
1891 ldv_mutex = 2;
1892#line 111
1893 return;
1894}
1895}
1896#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1897int mutex_trylock(struct mutex *lock )
1898{ int nondetermined ;
1899
1900 {
1901#line 121
1902 if (ldv_mutex == 1) {
1903
1904 } else {
1905 {
1906#line 121
1907 ldv_blast_assert();
1908 }
1909 }
1910 {
1911#line 124
1912 nondetermined = __VERIFIER_nondet_int();
1913 }
1914#line 127
1915 if (nondetermined) {
1916#line 130
1917 ldv_mutex = 2;
1918#line 132
1919 return (1);
1920 } else {
1921#line 137
1922 return (0);
1923 }
1924}
1925}
1926#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1927void mutex_unlock(struct mutex *lock )
1928{
1929
1930 {
1931#line 147
1932 if (ldv_mutex == 2) {
1933
1934 } else {
1935 {
1936#line 147
1937 ldv_blast_assert();
1938 }
1939 }
1940#line 149
1941 ldv_mutex = 1;
1942#line 150
1943 return;
1944}
1945}
1946#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1947void ldv_check_final_state(void)
1948{
1949
1950 {
1951#line 156
1952 if (ldv_mutex == 1) {
1953
1954 } else {
1955 {
1956#line 156
1957 ldv_blast_assert();
1958 }
1959 }
1960#line 157
1961 return;
1962}
1963}
1964#line 321 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/drivers/edac/mce_amd_inj.c.common.c"
1965long s__builtin_expect(long val , long res )
1966{
1967
1968 {
1969#line 322
1970 return (val);
1971}
1972}