const margin_top_setterinfo: JSJitInfo;