Showing error 777

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-linux-3.4/43_1a_cilled_safe_ok_nondet_linux-43_1a-drivers--edac--mce_amd_inj.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 1714
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

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