I propose to add to the BenchExec results XML file a column (or attribute) that links the run to its results files and the log file.
Like in a database, an object in a table should have a foreign key that points to another object in a different table if it depends on this.
From the <result> tag, it is not clear how to identify the results or log files:
<result benchmarkname="jbmc" date="2026-02-24 19:45:08 CET" starttime="2026-02-24T19:46:23.869863+01:00" tool="JBMC" version="6.8.0 (cbmc-6.8.0-10-g4767cf5d65)" toolmodule="benchexec.tools.jbmc" generator="BenchExec 3.35-dev" displayName="JBMC" memlimit="3000000000B" timelimit="900s" cpuCores="1" options="--graphml-witness witness.graphml" block="Java.no-runtime-exception.Main" name="SV-COMP27_no-runtime-exception.Java.no-runtime-exception.Main" endtime="2026-02-24T20:39:49.605286+01:00">
For example, consider the following <run>:
<run name="../sv-benchmarks/java/jayhorn-recursive/SatFibonacci02.yml" files="[../sv-benchmarks/java/common, ../sv-benchmarks/java/jayhorn-recursive/SatFibonacci02]" properties="no-runtime-exception" propertyFile="../sv-benchmarks/java/properties/no-runtime-exception.prp" expectedVerdict="true">
<column title="cputime" value="0.972704s"/>
<column title="host" value="apollon030"/>
<column title="memory" value="47448064B"/>
<column title="status" value="true"/>
The result files are stored in the folder
./jbmc.2026-02-24_19-45-08.files/SV-COMP27_no-runtime-exception/SatFibonacci02.yml/
I propose to add a column:
<column title="result_files" value="./jbmc.2026-02-24_19-45-08.files/SV-COMP27_no-runtime-exception/SatFibonacci02.yml/" hidden="true"/>
Alternatively, this could be an attribute for the <run> tag instead of a child <column>.
Similar for the log file.
Currently, the missing information requires complicated post-processing, composing the path in a hard-coded manner
as the concatenation by delimiter . of the following attributes of <result>:
- the
benchmarkname
- the
date="2026-02-24 19:45:08 CET", after removing CET and replacing : and
- the constant
files
- then a subdirectory consisting of
- the
name of the result
- then a subdirectory of
- the
name of the <run> tag, by removing directory prefix from it (because name is a file path)
An alternative way is to use the name of the XML file jbmc.2026-02-24_19-45-08.results.SV-COMP27_no-runtime-exception.Java.no-runtime-exception.Main.xml.bz2:
- extract the prefix until the constant
results
- then replace
results by files,
- then a subdirectory consisting of
- the
name of the result
- then a subdirectory of
- the
name of the <run> tag, by removing directory prefix from it (because name is a file path)
This can be avoided by adding to the the explicit knowledge of where its results (and log file) are located.
I propose to add to the BenchExec results XML file a column (or attribute) that links the run to its results files and the log file.
Like in a database, an object in a table should have a foreign key that points to another object in a different table if it depends on this.
From the
<result>tag, it is not clear how to identify the results or log files:For example, consider the following
<run>:The result files are stored in the folder
./jbmc.2026-02-24_19-45-08.files/SV-COMP27_no-runtime-exception/SatFibonacci02.yml/I propose to add a column:
Alternatively, this could be an attribute for the
<run>tag instead of a child<column>.Similar for the log file.
Currently, the missing information requires complicated post-processing, composing the path in a hard-coded manner
as the concatenation by delimiter
.of the following attributes of<result>:benchmarknamedate="2026-02-24 19:45:08 CET", after removing CET and replacing:andfilesnameof the resultnameof the<run>tag, by removing directory prefix from it (becausenameis a file path)An alternative way is to use the name of the XML file
jbmc.2026-02-24_19-45-08.results.SV-COMP27_no-runtime-exception.Java.no-runtime-exception.Main.xml.bz2:resultsresultsbyfiles,nameof the resultnameof the<run>tag, by removing directory prefix from it (becausenameis a file path)This can be avoided by adding to the the explicit knowledge of where its results (and log file) are located.