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

[AutoPR] Reformatted code #269

Closed thetabotmaintainer[bot] closed 5 months ago

thetabotmaintainer[bot] commented 5 months ago

Automated changes by create-pull-request GitHub action

github-actions[bot] commented 5 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/code-reformat/BenchexecResults-ConcurrencySafety-Main/theta.2024-06-21_09-18-31.results.SV-COMP24_unreach-call.ConcurrencySafety-Main.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/code-reformat/BenchexecResults-ConcurrencySafety-Main/theta.2024-06-21_09-18-31.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: Fri, 2024-06-21 09:18:31 UTC tool: Theta 5.2.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-48 os: Linux-6.5.0-1022-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2832.476 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 11.00 5.20 None pthread-atomic/read_write_lock-1.yml true 11.86 4.34 None pthread-wmm/rfi003_tso.yml TIMEOUT 120.89 86.68 None pthread/lazy01.yml false(unreach-call) 8.26 3.46 None pthread-wmm/mix000.oepc.yml false(unreach-call) 21.08 7.83 None ----------------------------------------------------------------------------------------------------------- Run set 1 done 52.30 108.25 - 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/code-reformat/BenchexecResults-ConcurrencySafety-MemSafety/theta.2024-06-21_09-18-19.results.SV-COMP24_valid-memsafety.ConcurrencySafety-MemSafety.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/code-reformat/BenchexecResults-ConcurrencySafety-MemSafety/theta.2024-06-21_09-18-19.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: Fri, 2024-06-21 09:18:19 UTC tool: Theta 5.2.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-az651-661 os: Linux-6.5.0-1022-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3223.641 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 11.06 5.14 None pthread-atomic/read_write_lock-1.yml true 9.01 3.62 None pthread-wmm/rfi003_tso.yml true 13.60 5.66 None pthread/lazy01.yml true 7.64 3.25 None pthread-wmm/mix000.oepc.yml true 13.36 5.49 None ----------------------------------------------------------------------------------------------------------- Run set 4 done 54.65 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/code-reformat/BenchexecResults-ConcurrencySafety-NoOverflows/theta.2024-06-21_09-18-22.results.SV-COMP24_no-overflow.ConcurrencySafety-NoOverflows.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/code-reformat/BenchexecResults-ConcurrencySafety-NoOverflows/theta.2024-06-21_09-18-22.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: Fri, 2024-06-21 09:18:22 UTC tool: Theta 5.2.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-az732-226 os: Linux-6.5.0-1022-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3176.658 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.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.34 5.19 None pthread-atomic/read_write_lock-1.yml true 8.58 3.37 None pthread-wmm/rfi003_tso.yml true 15.83 6.36 None pthread/lazy01.yml true 7.47 3.16 None pthread-wmm/mix000.oepc.yml true 15.63 6.32 None ----------------------------------------------------------------------------------------------------------- Run set 3 done 58.83 24.92 - 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/code-reformat/BenchexecResults-NoDataRace-Main/theta.2024-06-21_09-18-35.results.SV-COMP24_no-data-race.NoDataRace-Main.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/code-reformat/BenchexecResults-NoDataRace-Main/theta.2024-06-21_09-18-35.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: Fri, 2024-06-21 09:18:35 UTC tool: Theta 5.2.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-az1020-671 os: Linux-6.5.0-1022-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3183.878 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.54 5.03 None pthread-atomic/read_write_lock-1.yml true 11.35 4.31 None pthread-wmm/rfi003_tso.yml true 18.22 7.03 None pthread/lazy01.yml true 7.91 3.30 None pthread-wmm/mix000.oepc.yml true 16.88 6.72 None ----------------------------------------------------------------------------------------------------------- Run set 2 done 64.86 26.92 - 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/code-reformat/BenchexecResults-ReachSafety-Arrays/theta.2024-06-21_09-16-54.results.SV-COMP24_unreach-call.ReachSafety-Arrays.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/code-reformat/BenchexecResults-ReachSafety-Arrays/theta.2024-06-21_09-16-54.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: Fri, 2024-06-21 09:16:54 UTC tool: Theta 5.2.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-az1493-135 os: Linux-6.5.0-1022-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2682.315 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 77.05 161.00 None array-crafted/mapavg4.yml TIMEOUT 77.08 161.03 None array-programs/copysome2-1.yml TIMEOUT 77.87 161.03 None array-examples/sanfoundry_24-1.yml true 12.14 103.29 None array-multidimensional/max-2-u.yml ERROR (frontend failed) 1.96 0.81 None --------------------------------------------------------------------------------------------------------------- Run set 1 done 14.45 587.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: 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/code-reformat/BenchexecResults-ReachSafety-BitVectors/theta.2024-06-21_09-15-46.results.SV-COMP24_unreach-call.ReachSafety-BitVectors.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/code-reformat/BenchexecResults-ReachSafety-BitVectors/theta.2024-06-21_09-15-46.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: Fri, 2024-06-21 09:15:46 UTC tool: Theta 5.2.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-az984-244 os: Linux-6.5.0-1022-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3232.464 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.86 None bitvector/soft_float_1-3a.c.cil.yml false(unreach-call) 30.09 16.73 None bitvector-regression/integerpromotion-3.yml false(unreach-call) 4.94 2.76 None bitvector/sum02-1.yml Parsing OK 34.84 17.98 None bitvector-loops/diamond_2-1.yml TIMEOUT 120.84 96.59 None ------------------------------------------------------------------------------------------------------------ Run set 1 done 70.77 137.55 - 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/code-reformat/BenchexecResults-ReachSafety-Combinations/theta.2024-06-21_09-17-31.results.SV-COMP24_unreach-call.ReachSafety-Combinations.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/code-reformat/BenchexecResults-ReachSafety-Combinations/theta.2024-06-21_09-17-31.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: Fri, 2024-06-21 09:17:31 UTC tool: Theta 5.2.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-az651-661 os: Linux-6.5.0-1022-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3238.889 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.71 72.67 None Problem05_label47+token_ring.02.cil-1.yml TIMEOUT 120.44 95.27 None pc_sfifo_3.cil+token_ring.11.cil-1.yml TIMEOUT 121.03 109.21 None Problem05_label45+token_ring.01.cil-2.yml TIMEOUT 120.23 96.75 None pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label04.yml TIMEOUT 122.67 69.67 None ---------------------------------------------------------------------------------------------------------------------- Run set 1 done 0.60 444.70 - 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/code-reformat/BenchexecResults-ReachSafety-ControlFlow/theta.2024-06-21_09-15-56.results.SV-COMP24_unreach-call.ReachSafety-ControlFlow.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/code-reformat/BenchexecResults-ReachSafety-ControlFlow/theta.2024-06-21_09-15-56.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: Fri, 2024-06-21 09:15:56 UTC tool: Theta 5.2.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-az570-320 os: Linux-6.5.0-1022-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2633.958 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.43 1.21 None locks/test_locks_11.yml TIMEOUT 122.53 103.53 None locks/test_locks_5.yml true 13.41 5.15 None longjmp/68-longjmp_18-simple-else_unknown_2_pos.yml ERROR (frontend failed) 4.13 1.47 None longjmp/68-longjmp_11-counting-return_true.yml ERROR (frontend failed) 2.17 0.85 None -------------------------------------------------------------------------------------------------------------------- Run set 1 done 22.63 112.83 - 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/code-reformat/BenchexecResults-ReachSafety-ECA/theta.2024-06-21_09-19-12.results.SV-COMP24_unreach-call.ReachSafety-ECA.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/code-reformat/BenchexecResults-ReachSafety-ECA/theta.2024-06-21_09-19-12.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: Fri, 2024-06-21 09:19:12 UTC tool: Theta 5.2.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-az2026-576 os: Linux-6.5.0-1022-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3215.887 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 121.20 80.15 None eca-rers2012/Problem06_label11.yml TIMEOUT 120.30 76.09 None eca-programs/Problem101_label07.yml TIMEOUT 121.25 73.13 None eca-rers2012/Problem05_label44.yml TIMEOUT 121.01 70.26 None eca-rers2012/Problem04_label05.yml TIMEOUT 120.85 75.93 None ---------------------------------------------------------------------------------------------------- Run set 1 done 0.59 378.60 - 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/code-reformat/BenchexecResults-ReachSafety-Floats/theta.2024-06-21_09-18-36.results.SV-COMP24_unreach-call.ReachSafety-Floats.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/code-reformat/BenchexecResults-ReachSafety-Floats/theta.2024-06-21_09-18-36.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: Fri, 2024-06-21 09:18:36 UTC tool: Theta 5.2.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-az2026-576 os: Linux-6.5.0-1022-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3248.248 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 5.51 2.76 None float-benchs/zonotope_loose.c.v+cfa-reducer.yml TIMEOUT 120.39 113.76 None float-benchs/float_int_inv_square.yml false(unreach-call) 6.28 2.99 None floats-cdfpl/square_3.yml false(unreach-call) 75.01 71.17 None floats-cbmc-regression/float11.yml true 5.35 2.76 None ---------------------------------------------------------------------------------------------------------------- Run set 1 done 23.75 194.45 - 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/code-reformat/BenchexecResults-ReachSafety-Hardware/theta.2024-06-21_09-19-07.results.SV-COMP24_unreach-call.ReachSafety-Hardware.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/code-reformat/BenchexecResults-ReachSafety-Hardware/theta.2024-06-21_09-19-07.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: Fri, 2024-06-21 09:19:07 UTC tool: Theta 5.2.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-az570-320 os: Linux-6.5.0-1022-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2620.071 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.26 None btor2c-lazyMod.cambridge.5.prop1-back-serstep.yml TIMEOUT 120.53 98.22 None btor2c-lazyMod.extinction.4.prop1-func-interl.yml TIMEOUT 120.41 95.45 None btor2c-lazyMod.lup.2.prop1-func-interl.yml TIMEOUT 120.13 95.26 None btor2c-lazyMod.train-gate.6.prop1-func-interl.yml TIMEOUT 120.50 87.81 None ------------------------------------------------------------------------------------------------------------------ Run set 1 done 0.59 490.62 - 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/code-reformat/BenchexecResults-ReachSafety-Heap/theta.2024-06-21_09-16-17.results.SV-COMP24_unreach-call.ReachSafety-Heap.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/code-reformat/BenchexecResults-ReachSafety-Heap/theta.2024-06-21_09-16-17.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: Fri, 2024-06-21 09:16:17 UTC tool: Theta 5.2.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-az1116-180 os: Linux-6.5.0-1022-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2590.001 MHz ram: 16757.338112 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.91 4.68 None test15.yml true 8.63 4.22 None just_assert.yml true 5.35 2.77 None volatile_alias.yml true 7.73 4.03 None mutex_lock_int.c_1.yml true 8.82 4.33 None --------------------------------------------------------------------------------------- Run set 1 done 40.40 20.56 - 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/code-reformat/BenchexecResults-ReachSafety-Loops/theta.2024-06-21_09-18-04.results.SV-COMP24_unreach-call.ReachSafety-Loops.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/code-reformat/BenchexecResults-ReachSafety-Loops/theta.2024-06-21_09-18-04.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: Fri, 2024-06-21 09:18:04 UTC tool: Theta 5.2.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-az1432-569 os: Linux-6.5.0-1022-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2944.621 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.33 107.27 None loop-crafted/simple_vardep_2.yml TIMEOUT 120.70 110.17 None nla-digbench-scaling/divbin_valuebound100.yml TIMEOUT 120.65 108.02 None nla-digbench-scaling/mannadiv_valuebound50.yml true 22.26 10.03 None nla-digbench-scaling/mannadiv_unwindbound10.yml Parsing OK 27.64 11.94 None ---------------------------------------------------------------------------------------------------------------- Run set 1 done 50.15 348.25 - 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/code-reformat/BenchexecResults-ReachSafety-Recursive/theta.2024-06-21_09-16-09.results.SV-COMP24_unreach-call.ReachSafety-Recursive.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/code-reformat/BenchexecResults-ReachSafety-Recursive/theta.2024-06-21_09-16-09.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: Fri, 2024-06-21 09:16:09 UTC tool: Theta 5.2.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-az1766-97 os: Linux-6.5.0-1022-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3242.5 MHz ram: 16757.342208000002 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.19 6.88 None recursive-simple/id2_i5_o5-2.yml true 13.61 4.85 None recursified_nla-digbench/recursified_geo2-ll.yml TIMEOUT 33.33 161.02 None recursive/recHanoi03-2.yml TIMEOUT 120.33 90.63 None recursified_nla-digbench/recursified_lcm2.yml TIMEOUT 120.36 114.32 None ----------------------------------------------------------------------------------------------------------------- Run set 1 done 31.16 379.48 - 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/code-reformat/BenchexecResults-ReachSafety-Sequentialized/theta.2024-06-21_09-17-16.results.SV-COMP24_unreach-call.ReachSafety-Sequentialized.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/code-reformat/BenchexecResults-ReachSafety-Sequentialized/theta.2024-06-21_09-17-16.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: Fri, 2024-06-21 09:17:16 UTC tool: Theta 5.2.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-az740-901 os: Linux-6.5.0-1022-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3243.219 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.15 108.54 None seq-mthreaded/pals_opt-floodmax.3.1.ufo.UNBOUNDED.pals.yml TIMEOUT 120.33 94.67 None systemc/pipeline.cil-1.yml TIMEOUT 120.51 103.66 None seq-mthreaded/pals_lcr-var-start-time.3.ufo.UNBOUNDED.pals.yml TIMEOUT 120.67 94.38 None seq-mthreaded/pals_floodmax.3.2.ufo.BOUNDED-6.pals.yml false(unreach-call) 104.28 67.71 None ------------------------------------------------------------------------------------------------------------------------------- Run set 1 done 103.00 470.39 - 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/code-reformat/BenchexecResults-ReachSafety-XCSP/theta.2024-06-21_09-15-54.results.SV-COMP24_unreach-call.ReachSafety-XCSP.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/code-reformat/BenchexecResults-ReachSafety-XCSP/theta.2024-06-21_09-15-54.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: Fri, 2024-06-21 09:15:54 UTC tool: Theta 5.2.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-184 os: Linux-6.5.0-1022-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2924.412 MHz ram: 16757.342208000002 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 121.09 105.33 None Dubois-025.yml TIMEOUT 120.68 107.61 None aim-100-2-0-unsat-4.yml TIMEOUT 121.00 107.35 None AllInterval-014.yml TIMEOUT 120.53 105.98 None AllInterval-005.yml TIMEOUT 120.36 105.37 None ---------------------------------------------------------------------------------------- Run set 1 done 0.58 532.66 - 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) ```