const margin_top_getterinfo: JSJitInfo;