static inline void mthca_write_db_rec(u32 val[2], u32 *db) 
static inline void mthca_write_db_rec(__be32 val[2], __be32 *db) 
static inline void mthca_write_db_rec(u32 val[2], u32 *db){	db[0] = val[0];	wmb();	db[1] = val[1];}
10457	/local/tlutelli/issta_data/temp/c/2005_temp/2005/10457/97f52eb438be7caebe026421545619d8a0c1398a/mthca_doorbell.h/buggy/drivers/infiniband/hw/mthca/mthca_doorbell.h