const margin_right_setterinfo: JSJitInfo;