From c87f79337ea7526dd302c11854f22ca8d4f8ec79 Mon Sep 17 00:00:00 2001 From: Mamatha1718 Date: Sun, 12 Jan 2025 19:08:57 +0530 Subject: [PATCH] Error counts in generated table summary tab --- .../src/components/StatisticsTable.js | 31 ++++++++++--------- .../react-table/src/utils/stats.js | 2 +- 2 files changed, 17 insertions(+), 16 deletions(-) diff --git a/benchexec/tablegenerator/react-table/src/components/StatisticsTable.js b/benchexec/tablegenerator/react-table/src/components/StatisticsTable.js index 586fa4590..1db378315 100644 --- a/benchexec/tablegenerator/react-table/src/components/StatisticsTable.js +++ b/benchexec/tablegenerator/react-table/src/components/StatisticsTable.js @@ -88,8 +88,7 @@ const StatisticsTable = ({ header.className || "" }`, }) - } > - { header.render("Header") } + } > { header.render("Header") } { (!header.className || @@ -120,8 +119,7 @@ const StatisticsTable = ({ div {...cell.getCellProps({ className: "td " + (cell.column.className || ""), }) - } > - { cell.render("Cell") } < + } > { cell.render("Cell") } < /div> )) } < @@ -149,10 +147,10 @@ const StatisticsTable = ({ div className = "table-content" > < div className = "table-container" {...getTableProps() } > { renderTableHeaders(headerGroups) } { renderTableData(rows) } < - /div> < - /div> < - /div> < - /div> + /div> < / + div > < + /div> < / + div > ); }; @@ -168,7 +166,8 @@ const StatisticsTable = ({ className = "header-data clickable" title = "Show Quantile Plot of this column" onClick = { - (e) => switchToQuantile(column) } + (e) => switchToQuantile(column) + } /> ), hidden: hiddenCols[runSetIdx].includes(column.colIdx) || @@ -212,7 +211,8 @@ const StatisticsTable = ({ title = { column.type !== "status" ? renderTooltip(cell.value) : undefined } > - < /div> + < + /div> ) : ( < div className = "cell" > - < /div> ); @@ -231,9 +231,10 @@ const StatisticsTable = ({ type = "checkbox" checked = { isTitleColSticky } onChange = { - ({ target }) => setTitleColSticky(target.checked) } - /> < - /label> < + ({ target }) => setTitleColSticky(target.checked) + } + /> < / + label > < /form> ), id: "row-title", @@ -312,8 +313,8 @@ const StatisticsTable = ({ return ( < div id = "statistics" > < - h2 > Statistics < /h2> { renderTable(headerGroups, rows) } < - /div> + h2 > Statistics < /h2> { renderTable(headerGroups, rows) } < / + div > ); }; diff --git a/benchexec/tablegenerator/react-table/src/utils/stats.js b/benchexec/tablegenerator/react-table/src/utils/stats.js index c05f51366..6ab72ad95 100644 --- a/benchexec/tablegenerator/react-table/src/utils/stats.js +++ b/benchexec/tablegenerator/react-table/src/utils/stats.js @@ -114,7 +114,7 @@ export const computeStats = async({ tools, tableData, stats }) => { // The result of our stat calculation only contains relevant columns. // The stat table however requires a strict ordering of columns that also // includes columns that are not even rendered. - // + // In order to ensure a consistent layout we iterate through all columns // of the runset and append dummy objects until we reach a column that we // have calculated data for