Error counts in generated table summary tab

sosy-lab · Jan 12, 2025 · c87f793 · c87f793
1 parent b8d6cc8
commit c87f793
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 16 deletions.
diff --git 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
@@ -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