const margin_getterinfo: JSJitInfo;