const margin_right_getterinfo: JSJitInfo;