search

ftsrg / theta

Generic, modular and configurable formal verification framework supporting various formalisms and algorithms
http://theta.inf.mit.bme.hu/
Apache License 2.0
49 stars 43 forks source link

Bounded analysis improvements, CLI bindings for CFA,STS,XSTS #286

Closed mondokm closed 3 months ago

mondokm commented 3 months ago

This PR adds the following:

sonarcloud[bot] commented 3 months ago

Quality Gate Failed Quality Gate failed

Failed conditions
4.2% Coverage on New Code (required ≥ 60%)
5.0% Duplication on New Code (required ≤ 5%)

See analysis details on SonarCloud

github-actions[bot] commented 3 months ago

Benchexec test report for a selection of SV-Benchmarks (correct / incorrect / all):

:white_check_mark: ConcurrencySafety-Main (3 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/monolithic/BenchexecResults-ConcurrencySafety-Main/theta.2024-07-31_11-48-51.results.SV-COMP24_unreach-call.ConcurrencySafety-Main.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/monolithic/BenchexecResults-ConcurrencySafety-Main/theta.2024-07-31_11-48-51.results.SV-COMP24_unreach-call.ConcurrencySafety-Main.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ConcurrencySafety-Main, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Wed, 2024-07-31 11:48:51 UTC tool: Theta 6.3.0 tool executable: Theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az1427-249 os: Linux-6.5.0-1024-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3243.222 MHz ram: 16757.342208000002 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ConcurrencySafety-Main Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ----------------------------------------------------------------------------------------------------------- pthread-ext/18_read_write_lock-pthread.yml Parsing OK 10.13 5.03 None pthread-atomic/read_write_lock-1.yml true 11.19 4.23 None pthread-wmm/rfi003_tso.yml TIMEOUT 120.79 88.89 None pthread/lazy01.yml false(unreach-call) 8.11 3.43 None pthread-wmm/mix000.oepc.yml false(unreach-call) 19.95 7.53 None ----------------------------------------------------------------------------------------------------------- Run set 1 done 49.47 109.85 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 5 Files correct: 3 correct true: 1 correct false: 2 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 2 Score: 4 (max: 8) ```
:white_check_mark: ConcurrencySafety-MemSafety (4 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/monolithic/BenchexecResults-ConcurrencySafety-MemSafety/theta.2024-07-31_11-48-37.results.SV-COMP24_valid-memsafety.ConcurrencySafety-MemSafety.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/monolithic/BenchexecResults-ConcurrencySafety-MemSafety/theta.2024-07-31_11-48-37.results.SV-COMP24_valid-memsafety.ConcurrencySafety-MemSafety.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety.ConcurrencySafety-MemSafety date: Wed, 2024-07-31 11:48:37 UTC tool: Theta 6.3.0 tool executable: Theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az573-810 os: Linux-6.5.0-1024-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3243.3 MHz ram: 16757.342208000002 MB ------------------------------------------------------------ SV-COMP24_unreach-call Run set 1 of 4: skipped because it has no files SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety.ConcurrencySafety-MemSafety Run set 4 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ----------------------------------------------------------------------------------------------------------- pthread-ext/18_read_write_lock-pthread.yml Parsing OK 10.09 5.01 None pthread-atomic/read_write_lock-1.yml true 8.47 3.39 None pthread-wmm/rfi003_tso.yml true 14.90 6.04 None pthread/lazy01.yml true 7.16 3.07 None pthread-wmm/mix000.oepc.yml true 13.58 5.64 None ----------------------------------------------------------------------------------------------------------- Run set 4 done 54.18 23.68 - Statistics: 5 Files correct: 4 correct true: 4 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 1 Score: 8 (max: 10) ```
:white_check_mark: ConcurrencySafety-NoOverflows (4 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/monolithic/BenchexecResults-ConcurrencySafety-NoOverflows/theta.2024-07-31_11-48-39.results.SV-COMP24_no-overflow.ConcurrencySafety-NoOverflows.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/monolithic/BenchexecResults-ConcurrencySafety-NoOverflows/theta.2024-07-31_11-48-39.results.SV-COMP24_no-overflow.ConcurrencySafety-NoOverflows.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call, SV-COMP24_no-data-race, SV-COMP24_no-overflow.ConcurrencySafety-NoOverflows, SV-COMP24_valid-memsafety date: Wed, 2024-07-31 11:48:39 UTC tool: Theta 6.3.0 tool executable: Theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az1382-274 os: Linux-6.5.0-1024-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3242.193 MHz ram: 16757.338112 MB ------------------------------------------------------------ SV-COMP24_unreach-call Run set 1 of 4: skipped because it has no files SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow.ConcurrencySafety-NoOverflows Run set 3 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ----------------------------------------------------------------------------------------------------------- pthread-ext/18_read_write_lock-pthread.yml Parsing OK 11.62 5.43 None pthread-atomic/read_write_lock-1.yml true 9.19 3.64 None pthread-wmm/rfi003_tso.yml true 15.06 6.42 None pthread/lazy01.yml true 7.97 3.32 None pthread-wmm/mix000.oepc.yml true 14.95 6.14 None ----------------------------------------------------------------------------------------------------------- Run set 3 done 58.76 25.47 - SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 5 Files correct: 4 correct true: 4 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 1 Score: 8 (max: 10) ```
:white_check_mark: NoDataRace-Main (4 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/monolithic/BenchexecResults-NoDataRace-Main/theta.2024-07-31_11-48-55.results.SV-COMP24_no-data-race.NoDataRace-Main.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/monolithic/BenchexecResults-NoDataRace-Main/theta.2024-07-31_11-48-55.results.SV-COMP24_no-data-race.NoDataRace-Main.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call, SV-COMP24_no-data-race.NoDataRace-Main, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Wed, 2024-07-31 11:48:55 UTC tool: Theta 6.3.0 tool executable: Theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az801-433 os: Linux-6.5.0-1024-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3239.951 MHz ram: 16757.342208000002 MB ------------------------------------------------------------ SV-COMP24_unreach-call Run set 1 of 4: skipped because it has no files SV-COMP24_no-data-race.NoDataRace-Main Run set 2 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ----------------------------------------------------------------------------------------------------------- pthread-ext/18_read_write_lock-pthread.yml Parsing OK 10.28 5.10 None pthread-atomic/read_write_lock-1.yml true 11.69 4.38 None pthread-wmm/rfi003_tso.yml true 18.34 7.05 None pthread/lazy01.yml true 7.97 3.30 None pthread-wmm/mix000.oepc.yml true 17.80 7.01 None ----------------------------------------------------------------------------------------------------------- Run set 2 done 66.04 27.37 - SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 5 Files correct: 4 correct true: 4 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 1 Score: 8 (max: 10) ```
:white_check_mark: ReachSafety-Arrays (1 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/monolithic/BenchexecResults-ReachSafety-Arrays/theta.2024-07-31_11-47-10.results.SV-COMP24_unreach-call.ReachSafety-Arrays.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/monolithic/BenchexecResults-ReachSafety-Arrays/theta.2024-07-31_11-47-10.results.SV-COMP24_unreach-call.ReachSafety-Arrays.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-Arrays, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Wed, 2024-07-31 11:47:10 UTC tool: Theta 6.3.0 tool executable: Theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az661-193 os: Linux-6.5.0-1024-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3197.272 MHz ram: 16757.342208000002 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-Arrays Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host --------------------------------------------------------------------------------------------------------------- array-examples/standard_partition_ground-2.yml TIMEOUT 76.32 161.00 None array-crafted/mapavg4.yml TIMEOUT 76.77 161.02 None array-programs/copysome2-1.yml TIMEOUT 78.15 161.02 None array-examples/sanfoundry_24-1.yml true 11.96 103.28 None array-multidimensional/max-2-u.yml ERROR (frontend failed) 1.88 0.80 None --------------------------------------------------------------------------------------------------------------- Run set 1 done 14.18 588.36 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 5 Files correct: 1 correct true: 1 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 4 Score: 2 (max: 10) ```
:white_check_mark: ReachSafety-BitVectors (3 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/monolithic/BenchexecResults-ReachSafety-BitVectors/theta.2024-07-31_11-46-11.results.SV-COMP24_unreach-call.ReachSafety-BitVectors.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/monolithic/BenchexecResults-ReachSafety-BitVectors/theta.2024-07-31_11-46-11.results.SV-COMP24_unreach-call.ReachSafety-BitVectors.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-BitVectors, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Wed, 2024-07-31 11:46:11 UTC tool: Theta 6.3.0 tool executable: Theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az564-73 os: Linux-6.5.0-1024-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3243.016 MHz ram: 16757.342208000002 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-BitVectors Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ------------------------------------------------------------------------------------------------------------ bitvector/gcd_4.yml true 6.60 2.87 None bitvector/soft_float_1-3a.c.cil.yml false(unreach-call) 31.90 17.48 None bitvector-regression/integerpromotion-3.yml false(unreach-call) 4.99 2.85 None bitvector/sum02-1.yml Parsing OK 35.70 18.25 None bitvector-loops/diamond_2-1.yml TIMEOUT 120.49 106.07 None ------------------------------------------------------------------------------------------------------------ Run set 1 done 74.22 148.14 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 5 Files correct: 3 correct true: 1 correct false: 2 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 2 Score: 4 (max: 6) ```
:question: ReachSafety-Combinations (0 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/monolithic/BenchexecResults-ReachSafety-Combinations/theta.2024-07-31_11-47-49.results.SV-COMP24_unreach-call.ReachSafety-Combinations.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/monolithic/BenchexecResults-ReachSafety-Combinations/theta.2024-07-31_11-47-49.results.SV-COMP24_unreach-call.ReachSafety-Combinations.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-Combinations, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Wed, 2024-07-31 11:47:49 UTC tool: Theta 6.3.0 tool executable: Theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az665-750 os: Linux-6.5.0-1024-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3206.797 MHz ram: 16757.342208000002 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-Combinations Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ---------------------------------------------------------------------------------------------------------------------- pc_sfifo_3.cil+token_ring.02.cil-2.yml TIMEOUT 120.74 72.64 None Problem05_label47+token_ring.02.cil-1.yml TIMEOUT 120.31 95.63 None pc_sfifo_3.cil+token_ring.11.cil-1.yml TIMEOUT 121.06 109.16 None Problem05_label45+token_ring.01.cil-2.yml TIMEOUT 120.36 95.46 None pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label04.yml TIMEOUT 120.25 68.14 None ---------------------------------------------------------------------------------------------------------------------- Run set 1 done 0.61 442.05 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 5 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 5 Score: 0 (max: 5) ```
:white_check_mark: ReachSafety-ControlFlow (1 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/monolithic/BenchexecResults-ReachSafety-ControlFlow/theta.2024-07-31_11-46-19.results.SV-COMP24_unreach-call.ReachSafety-ControlFlow.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/monolithic/BenchexecResults-ReachSafety-ControlFlow/theta.2024-07-31_11-46-19.results.SV-COMP24_unreach-call.ReachSafety-ControlFlow.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-ControlFlow, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Wed, 2024-07-31 11:46:19 UTC tool: Theta 6.3.0 tool executable: Theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az1108-493 os: Linux-6.5.0-1024-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3166.66 MHz ram: 16757.342208000002 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-ControlFlow Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host -------------------------------------------------------------------------------------------------------------------- longjmp/68-longjmp_18-simple-else_unknown_1_pos.yml ERROR (frontend failed) 3.21 1.14 None locks/test_locks_11.yml TIMEOUT 122.86 102.99 None locks/test_locks_5.yml true 14.69 5.63 None longjmp/68-longjmp_18-simple-else_unknown_2_pos.yml ERROR (frontend failed) 3.63 1.32 None longjmp/68-longjmp_11-counting-return_true.yml ERROR (frontend failed) 2.03 0.86 None -------------------------------------------------------------------------------------------------------------------- Run set 1 done 23.03 112.97 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 5 Files correct: 1 correct true: 1 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 4 Score: 2 (max: 8) ```
:question: ReachSafety-ECA (0 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/monolithic/BenchexecResults-ReachSafety-ECA/theta.2024-07-31_11-49-24.results.SV-COMP24_unreach-call.ReachSafety-ECA.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/monolithic/BenchexecResults-ReachSafety-ECA/theta.2024-07-31_11-49-24.results.SV-COMP24_unreach-call.ReachSafety-ECA.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-ECA, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Wed, 2024-07-31 11:49:24 UTC tool: Theta 6.3.0 tool executable: Theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az1153-711 os: Linux-6.5.0-1024-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3037.227 MHz ram: 16757.342208000002 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-ECA Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ---------------------------------------------------------------------------------------------------- eca-rers2012/Problem06_label18.yml TIMEOUT 120.54 78.19 None eca-rers2012/Problem06_label11.yml TIMEOUT 120.73 75.02 None eca-programs/Problem101_label07.yml TIMEOUT 120.82 73.30 None eca-rers2012/Problem05_label44.yml TIMEOUT 121.04 73.86 None eca-rers2012/Problem04_label05.yml TIMEOUT 121.11 76.08 None ---------------------------------------------------------------------------------------------------- Run set 1 done 0.60 378.98 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 5 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 5 Score: 0 (max: 7) ```
:white_check_mark: ReachSafety-Floats (4 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/monolithic/BenchexecResults-ReachSafety-Floats/theta.2024-07-31_11-49-06.results.SV-COMP24_unreach-call.ReachSafety-Floats.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/monolithic/BenchexecResults-ReachSafety-Floats/theta.2024-07-31_11-49-06.results.SV-COMP24_unreach-call.ReachSafety-Floats.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-Floats, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Wed, 2024-07-31 11:49:06 UTC tool: Theta 6.3.0 tool executable: Theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az1269-474 os: Linux-6.5.0-1024-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3243.911 MHz ram: 16757.342208000002 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-Floats Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ---------------------------------------------------------------------------------------------------------------- float-benchs/float_double.yml true 6.02 2.90 None float-benchs/zonotope_loose.c.v+cfa-reducer.yml TIMEOUT 120.49 111.79 None float-benchs/float_int_inv_square.yml false(unreach-call) 6.80 3.34 None floats-cdfpl/square_3.yml false(unreach-call) 88.93 85.01 None floats-cbmc-regression/float11.yml true 5.58 3.06 None ---------------------------------------------------------------------------------------------------------------- Run set 1 done 25.66 207.13 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 5 Files correct: 4 correct true: 2 correct false: 2 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 1 Score: 6 (max: 8) ```
:question: ReachSafety-Hardware (0 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/monolithic/BenchexecResults-ReachSafety-Hardware/theta.2024-07-31_11-49-30.results.SV-COMP24_unreach-call.ReachSafety-Hardware.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/monolithic/BenchexecResults-ReachSafety-Hardware/theta.2024-07-31_11-49-30.results.SV-COMP24_unreach-call.ReachSafety-Hardware.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-Hardware, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Wed, 2024-07-31 11:49:30 UTC tool: Theta 6.3.0 tool executable: Theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az1385-208 os: Linux-6.5.0-1024-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2873.973 MHz ram: 16757.342208000002 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-Hardware Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ------------------------------------------------------------------------------------------------------------------ btor2c-lazyMod.arbitrated_top_n4_w16_d32_e0.yml TIMEOUT 120.67 111.47 None btor2c-lazyMod.cambridge.5.prop1-back-serstep.yml TIMEOUT 120.44 99.00 None btor2c-lazyMod.extinction.4.prop1-func-interl.yml TIMEOUT 120.47 94.47 None btor2c-lazyMod.lup.2.prop1-func-interl.yml TIMEOUT 120.47 95.36 None btor2c-lazyMod.train-gate.6.prop1-func-interl.yml TIMEOUT 120.85 82.20 None ------------------------------------------------------------------------------------------------------------------ Run set 1 done 0.60 485.15 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 5 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 5 Score: 0 (max: 9) ```
:white_check_mark: ReachSafety-Heap (5 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/monolithic/BenchexecResults-ReachSafety-Heap/theta.2024-07-31_11-46-46.results.SV-COMP24_unreach-call.ReachSafety-Heap.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/monolithic/BenchexecResults-ReachSafety-Heap/theta.2024-07-31_11-46-46.results.SV-COMP24_unreach-call.ReachSafety-Heap.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-Heap, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Wed, 2024-07-31 11:46:46 UTC tool: Theta 6.3.0 tool executable: Theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az1456-958 os: Linux-6.5.0-1024-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3190.383 MHz ram: 16757.342208000002 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-Heap Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host --------------------------------------------------------------------------------------- test09.yml true 9.76 4.76 None test15.yml true 8.79 4.41 None just_assert.yml true 5.55 2.87 None volatile_alias.yml true 8.06 4.23 None mutex_lock_int.c_1.yml true 9.21 4.54 None --------------------------------------------------------------------------------------- Run set 1 done 41.34 21.35 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 5 Files correct: 5 correct true: 5 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 0 Score: 10 (max: 10) ```
:white_check_mark: ReachSafety-Loops (1 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/monolithic/BenchexecResults-ReachSafety-Loops/theta.2024-07-31_11-48-26.results.SV-COMP24_unreach-call.ReachSafety-Loops.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/monolithic/BenchexecResults-ReachSafety-Loops/theta.2024-07-31_11-48-26.results.SV-COMP24_unreach-call.ReachSafety-Loops.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-Loops, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Wed, 2024-07-31 11:48:26 UTC tool: Theta 6.3.0 tool executable: Theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az1245-111 os: Linux-6.5.0-1024-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3255.362 MHz ram: 16757.342208000002 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-Loops Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ---------------------------------------------------------------------------------------------------------------- nla-digbench/ps3-ll.yml TIMEOUT 120.50 106.95 None loop-crafted/simple_vardep_2.yml TIMEOUT 120.82 109.79 None nla-digbench-scaling/divbin_valuebound100.yml TIMEOUT 120.66 107.61 None nla-digbench-scaling/mannadiv_valuebound50.yml true 23.00 10.38 None nla-digbench-scaling/mannadiv_unwindbound10.yml Parsing OK 29.35 12.80 None ---------------------------------------------------------------------------------------------------------------- Run set 1 done 52.58 349.17 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 5 Files correct: 1 correct true: 1 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 4 Score: 2 (max: 9) ```
:white_check_mark: ReachSafety-Recursive (1 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/monolithic/BenchexecResults-ReachSafety-Recursive/theta.2024-07-31_11-46-33.results.SV-COMP24_unreach-call.ReachSafety-Recursive.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/monolithic/BenchexecResults-ReachSafety-Recursive/theta.2024-07-31_11-46-33.results.SV-COMP24_unreach-call.ReachSafety-Recursive.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-Recursive, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Wed, 2024-07-31 11:46:33 UTC tool: Theta 6.3.0 tool executable: Theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az735-305 os: Linux-6.5.0-1024-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3235.906 MHz ram: 16757.338112 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-Recursive Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ----------------------------------------------------------------------------------------------------------------- recursive-simple/id_o100.yml Parsing OK 17.65 7.38 None recursive-simple/id2_i5_o5-2.yml true 13.79 5.33 None recursified_nla-digbench/recursified_geo2-ll.yml TIMEOUT 33.42 161.02 None recursive/recHanoi03-2.yml TIMEOUT 120.35 91.95 None recursified_nla-digbench/recursified_lcm2.yml TIMEOUT 120.37 114.01 None ----------------------------------------------------------------------------------------------------------------- Run set 1 done 31.76 381.47 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 5 Files correct: 1 correct true: 1 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 4 Score: 2 (max: 9) ```
:white_check_mark: ReachSafety-Sequentialized (1 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/monolithic/BenchexecResults-ReachSafety-Sequentialized/theta.2024-07-31_11-47-33.results.SV-COMP24_unreach-call.ReachSafety-Sequentialized.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/monolithic/BenchexecResults-ReachSafety-Sequentialized/theta.2024-07-31_11-47-33.results.SV-COMP24_unreach-call.ReachSafety-Sequentialized.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-Sequentialized, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Wed, 2024-07-31 11:47:33 UTC tool: Theta 6.3.0 tool executable: Theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az837-459 os: Linux-6.5.0-1024-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3243.904 MHz ram: 16757.342208000002 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-Sequentialized Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ------------------------------------------------------------------------------------------------------------------------------- systemc/transmitter.12.cil.yml TIMEOUT 120.25 108.78 None seq-mthreaded/pals_opt-floodmax.3.1.ufo.UNBOUNDED.pals.yml TIMEOUT 120.33 94.50 None systemc/pipeline.cil-1.yml TIMEOUT 120.22 104.98 None seq-mthreaded/pals_lcr-var-start-time.3.ufo.UNBOUNDED.pals.yml TIMEOUT 120.53 93.84 None seq-mthreaded/pals_floodmax.3.2.ufo.BOUNDED-6.pals.yml false(unreach-call) 107.11 68.44 None ------------------------------------------------------------------------------------------------------------------------------- Run set 1 done 105.75 471.97 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 5 Files correct: 1 correct true: 0 correct false: 1 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 4 Score: 1 (max: 6) ```
:question: ReachSafety-XCSP (0 / 0 / 5) `table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/monolithic/BenchexecResults-ReachSafety-XCSP/theta.2024-07-31_11-46-19.results.SV-COMP24_unreach-call.ReachSafety-XCSP.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/monolithic/BenchexecResults-ReachSafety-XCSP/theta.2024-07-31_11-46-19.results.SV-COMP24_unreach-call.ReachSafety-XCSP.csv) ``` BENCHMARK INFORMATION benchmark definition: xml/theta.xml name: theta run sets: SV-COMP24_unreach-call.ReachSafety-XCSP, SV-COMP24_no-data-race, SV-COMP24_no-overflow, SV-COMP24_valid-memsafety date: Wed, 2024-07-31 11:46:19 UTC tool: Theta 6.3.0 tool executable: Theta/theta-start.sh options: --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO resource limits: - time: 120 s hardware requirements: ------------------------------------------------------------ SYSTEM INFORMATION host: fv-az840-758 os: Linux-6.5.0-1024-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3242.505 MHz ram: 16757.334016 MB ------------------------------------------------------------ SV-COMP24_unreach-call.ReachSafety-XCSP Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None' inputfile status cpu time wall time host ---------------------------------------------------------------------------------------- CostasArray-14.yml TIMEOUT 120.37 105.42 None Dubois-025.yml TIMEOUT 120.28 108.20 None aim-100-2-0-unsat-4.yml TIMEOUT 120.23 107.73 None AllInterval-014.yml TIMEOUT 120.11 107.42 None AllInterval-005.yml TIMEOUT 120.91 109.18 None ---------------------------------------------------------------------------------------- Run set 1 done 0.60 538.98 - SV-COMP24_no-data-race Run set 2 of 4: skipped because it has no files SV-COMP24_no-overflow Run set 3 of 4: skipped because it has no files SV-COMP24_valid-memsafety Run set 4 of 4: skipped because it has no files Statistics: 5 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 5 Score: 0 (max: 7) ```