const margin_setterinfo: JSJitInfo;