Constant USER_MARSHAL_FC_DOUBLE 

pub const USER_MARSHAL_FC_DOUBLE: u32 = 12u32;