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

MDD-based analysis #278

Closed mondokm closed 4 months ago

mondokm commented 4 months ago

This PR contains the following:

leventeBajczi commented 4 months ago

I don't know if it's feasible to address the testing and duplication requirements, but otherwise, I can approve this PR, and I think it's mergeable.

sonarcloud[bot] commented 4 months ago

Quality Gate Failed Quality Gate failed

Failed conditions
39.5% Coverage on New Code (required ≥ 60%)
13.6% Duplication on New Code (required ≤ 5%)

See analysis details on SonarCloud

github-actions[bot] commented 4 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/zeta-merge-clean/BenchexecResults-ConcurrencySafety-Main/theta.2024-07-12_14-22-57.results.SV-COMP24_unreach-call.ConcurrencySafety-Main.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/zeta-merge-clean/BenchexecResults-ConcurrencySafety-Main/theta.2024-07-12_14-22-57.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-07-12 14:22:57 UTC tool: Theta 6.0.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-az566-865 os: Linux-6.5.0-1023-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3213.391 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.34 4.99 None pthread-atomic/read_write_lock-1.yml true 11.18 4.09 None pthread-wmm/rfi003_tso.yml TIMEOUT 120.82 88.79 None pthread/lazy01.yml false(unreach-call) 7.80 3.30 None pthread-wmm/mix000.oepc.yml false(unreach-call) 19.89 7.56 None ----------------------------------------------------------------------------------------------------------- Run set 1 done 49.31 109.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: 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/zeta-merge-clean/BenchexecResults-ConcurrencySafety-MemSafety/theta.2024-07-12_14-23-02.results.SV-COMP24_valid-memsafety.ConcurrencySafety-MemSafety.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/zeta-merge-clean/BenchexecResults-ConcurrencySafety-MemSafety/theta.2024-07-12_14-23-02.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-07-12 14:23:02 UTC tool: Theta 6.0.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-az1016-580 os: Linux-6.5.0-1023-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2694.298 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.92 5.25 None pthread-atomic/read_write_lock-1.yml true 8.54 3.37 None pthread-wmm/rfi003_tso.yml true 14.64 5.95 None pthread/lazy01.yml true 7.62 3.24 None pthread-wmm/mix000.oepc.yml true 13.99 5.79 None ----------------------------------------------------------------------------------------------------------- Run set 4 done 55.67 24.13 - 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/zeta-merge-clean/BenchexecResults-ConcurrencySafety-NoOverflows/theta.2024-07-12_14-23-21.results.SV-COMP24_no-overflow.ConcurrencySafety-NoOverflows.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/zeta-merge-clean/BenchexecResults-ConcurrencySafety-NoOverflows/theta.2024-07-12_14-23-21.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-07-12 14:23:21 UTC tool: Theta 6.0.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-az1149-710 os: Linux-6.5.0-1023-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2840.371 MHz ram: 16757.334016 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.73 5.41 None pthread-atomic/read_write_lock-1.yml true 8.64 3.42 None pthread-wmm/rfi003_tso.yml true 15.42 6.26 None pthread/lazy01.yml true 7.09 3.01 None pthread-wmm/mix000.oepc.yml true 15.90 6.36 None ----------------------------------------------------------------------------------------------------------- Run set 3 done 58.75 24.98 - 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/zeta-merge-clean/BenchexecResults-NoDataRace-Main/theta.2024-07-12_14-22-58.results.SV-COMP24_no-data-race.NoDataRace-Main.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/zeta-merge-clean/BenchexecResults-NoDataRace-Main/theta.2024-07-12_14-22-58.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-07-12 14:22:58 UTC tool: Theta 6.0.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-az883-738 os: Linux-6.5.0-1023-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2801.879 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.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.92 5.21 None pthread-atomic/read_write_lock-1.yml true 11.74 4.41 None pthread-wmm/rfi003_tso.yml true 17.98 7.00 None pthread/lazy01.yml true 7.82 3.27 None pthread-wmm/mix000.oepc.yml true 17.23 6.89 None ----------------------------------------------------------------------------------------------------------- Run set 2 done 65.67 27.30 - 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/zeta-merge-clean/BenchexecResults-ReachSafety-Arrays/theta.2024-07-12_14-21-39.results.SV-COMP24_unreach-call.ReachSafety-Arrays.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/zeta-merge-clean/BenchexecResults-ReachSafety-Arrays/theta.2024-07-12_14-21-39.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-07-12 14:21:39 UTC tool: Theta 6.0.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-701 os: Linux-6.5.0-1023-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3051.021 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.34 161.00 None array-crafted/mapavg4.yml TIMEOUT 77.11 161.02 None array-programs/copysome2-1.yml TIMEOUT 78.36 161.02 None array-examples/sanfoundry_24-1.yml true 12.29 103.34 None array-multidimensional/max-2-u.yml ERROR (frontend failed) 1.88 0.78 None --------------------------------------------------------------------------------------------------------------- Run set 1 done 14.51 588.00 - 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/zeta-merge-clean/BenchexecResults-ReachSafety-BitVectors/theta.2024-07-12_14-25-43.results.SV-COMP24_unreach-call.ReachSafety-BitVectors.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/zeta-merge-clean/BenchexecResults-ReachSafety-BitVectors/theta.2024-07-12_14-25-43.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-07-12 14:25:43 UTC tool: Theta 6.0.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-az1535-465 os: Linux-6.5.0-1023-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3154.843 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 7.16 3.04 None bitvector/soft_float_1-3a.c.cil.yml false(unreach-call) 34.15 18.39 None bitvector-regression/integerpromotion-3.yml false(unreach-call) 5.30 2.94 None bitvector/sum02-1.yml Parsing OK 36.85 18.88 None bitvector-loops/diamond_2-1.yml TIMEOUT 120.10 107.70 None ------------------------------------------------------------------------------------------------------------ Run set 1 done 78.21 151.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: 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/zeta-merge-clean/BenchexecResults-ReachSafety-Combinations/theta.2024-07-12_14-22-15.results.SV-COMP24_unreach-call.ReachSafety-Combinations.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/zeta-merge-clean/BenchexecResults-ReachSafety-Combinations/theta.2024-07-12_14-22-15.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-07-12 14:22:15 UTC tool: Theta 6.0.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-az1052-228 os: Linux-6.5.0-1023-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3103.439 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.41 74.44 None Problem05_label47+token_ring.02.cil-1.yml TIMEOUT 120.47 94.86 None pc_sfifo_3.cil+token_ring.11.cil-1.yml TIMEOUT 120.35 108.01 None Problem05_label45+token_ring.01.cil-2.yml TIMEOUT 120.57 94.17 None pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label04.yml TIMEOUT 122.04 70.42 None ---------------------------------------------------------------------------------------------------------------------- Run set 1 done 0.59 443.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: 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/zeta-merge-clean/BenchexecResults-ReachSafety-ControlFlow/theta.2024-07-12_14-20-29.results.SV-COMP24_unreach-call.ReachSafety-ControlFlow.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/zeta-merge-clean/BenchexecResults-ReachSafety-ControlFlow/theta.2024-07-12_14-20-29.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-07-12 14:20:29 UTC tool: Theta 6.0.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-az1206-191 os: Linux-6.5.0-1023-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3232.699 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.63 1.28 None locks/test_locks_11.yml TIMEOUT 121.82 102.53 None locks/test_locks_5.yml true 14.93 5.47 None longjmp/68-longjmp_18-simple-else_unknown_2_pos.yml ERROR (frontend failed) 3.23 1.16 None longjmp/68-longjmp_11-counting-return_true.yml ERROR (frontend failed) 1.95 0.77 None -------------------------------------------------------------------------------------------------------------------- Run set 1 done 23.85 111.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/zeta-merge-clean/BenchexecResults-ReachSafety-ECA/theta.2024-07-12_14-23-53.results.SV-COMP24_unreach-call.ReachSafety-ECA.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/zeta-merge-clean/BenchexecResults-ReachSafety-ECA/theta.2024-07-12_14-23-53.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-07-12 14:23:53 UTC tool: Theta 6.0.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-az585-42 os: Linux-6.5.0-1023-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2685.231 MHz ram: 16757.338112 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 122.63 78.64 None eca-rers2012/Problem06_label11.yml TIMEOUT 122.08 74.58 None eca-programs/Problem101_label07.yml TIMEOUT 121.19 73.21 None eca-rers2012/Problem05_label44.yml TIMEOUT 120.12 72.83 None eca-rers2012/Problem04_label05.yml TIMEOUT 120.99 75.38 None ---------------------------------------------------------------------------------------------------- Run set 1 done 0.59 377.68 - 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/zeta-merge-clean/BenchexecResults-ReachSafety-Floats/theta.2024-07-12_14-23-21.results.SV-COMP24_unreach-call.ReachSafety-Floats.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/zeta-merge-clean/BenchexecResults-ReachSafety-Floats/theta.2024-07-12_14-23-21.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-07-12 14:23:21 UTC tool: Theta 6.0.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-az1498-957 os: Linux-6.5.0-1023-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3244.126 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.70 2.84 None float-benchs/zonotope_loose.c.v+cfa-reducer.yml TIMEOUT 120.44 112.72 None float-benchs/float_int_inv_square.yml false(unreach-call) 6.44 2.98 None floats-cdfpl/square_3.yml false(unreach-call) 76.23 72.48 None floats-cbmc-regression/float11.yml true 5.39 2.75 None ---------------------------------------------------------------------------------------------------------------- Run set 1 done 93.83 194.80 - 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/zeta-merge-clean/BenchexecResults-ReachSafety-Hardware/theta.2024-07-12_14-23-34.results.SV-COMP24_unreach-call.ReachSafety-Hardware.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/zeta-merge-clean/BenchexecResults-ReachSafety-Hardware/theta.2024-07-12_14-23-34.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-07-12 14:23:34 UTC tool: Theta 6.0.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-az1442-24 os: Linux-6.5.0-1023-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3243.451 MHz ram: 16757.338112 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.65 111.59 None btor2c-lazyMod.cambridge.5.prop1-back-serstep.yml TIMEOUT 120.52 98.58 None btor2c-lazyMod.extinction.4.prop1-func-interl.yml TIMEOUT 120.48 94.27 None btor2c-lazyMod.lup.2.prop1-func-interl.yml TIMEOUT 123.11 95.70 None btor2c-lazyMod.train-gate.6.prop1-func-interl.yml TIMEOUT 121.05 85.21 None ------------------------------------------------------------------------------------------------------------------ Run set 1 done 0.60 487.57 - 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/zeta-merge-clean/BenchexecResults-ReachSafety-Heap/theta.2024-07-12_14-20-47.results.SV-COMP24_unreach-call.ReachSafety-Heap.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/zeta-merge-clean/BenchexecResults-ReachSafety-Heap/theta.2024-07-12_14-20-47.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-07-12 14:20:47 UTC tool: Theta 6.0.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-az1106-48 os: Linux-6.5.0-1023-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3244.583 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.84 4.77 None test15.yml true 8.67 4.37 None just_assert.yml true 5.51 2.80 None volatile_alias.yml true 8.01 4.19 None mutex_lock_int.c_1.yml true 8.84 4.44 None --------------------------------------------------------------------------------------- Run set 1 done 40.84 21.10 - 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/zeta-merge-clean/BenchexecResults-ReachSafety-Loops/theta.2024-07-12_14-22-47.results.SV-COMP24_unreach-call.ReachSafety-Loops.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/zeta-merge-clean/BenchexecResults-ReachSafety-Loops/theta.2024-07-12_14-22-47.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-07-12 14:22:47 UTC tool: Theta 6.0.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-927 os: Linux-6.5.0-1023-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3243.649 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.57 107.32 None loop-crafted/simple_vardep_2.yml TIMEOUT 120.75 110.05 None nla-digbench-scaling/divbin_valuebound100.yml TIMEOUT 120.68 107.25 None nla-digbench-scaling/mannadiv_valuebound50.yml true 22.59 10.31 None nla-digbench-scaling/mannadiv_unwindbound10.yml Parsing OK 28.88 12.50 None ---------------------------------------------------------------------------------------------------------------- Run set 1 done 51.71 348.65 - 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/zeta-merge-clean/BenchexecResults-ReachSafety-Recursive/theta.2024-07-12_14-20-35.results.SV-COMP24_unreach-call.ReachSafety-Recursive.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/zeta-merge-clean/BenchexecResults-ReachSafety-Recursive/theta.2024-07-12_14-20-35.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-07-12 14:20:35 UTC tool: Theta 6.0.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-az2036-51 os: Linux-6.5.0-1023-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3242.647 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 16.72 7.13 None recursive-simple/id2_i5_o5-2.yml true 13.17 5.23 None recursified_nla-digbench/recursified_geo2-ll.yml TIMEOUT 33.80 161.03 None recursive/recHanoi03-2.yml TIMEOUT 120.39 92.27 None recursified_nla-digbench/recursified_lcm2.yml TIMEOUT 120.36 114.16 None ----------------------------------------------------------------------------------------------------------------- Run set 1 done 30.14 381.20 - 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/zeta-merge-clean/BenchexecResults-ReachSafety-Sequentialized/theta.2024-07-12_14-21-44.results.SV-COMP24_unreach-call.ReachSafety-Sequentialized.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/zeta-merge-clean/BenchexecResults-ReachSafety-Sequentialized/theta.2024-07-12_14-21-44.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-07-12 14:21:44 UTC tool: Theta 6.0.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-az1442-24 os: Linux-6.5.0-1023-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3243.094 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 121.06 109.23 None seq-mthreaded/pals_opt-floodmax.3.1.ufo.UNBOUNDED.pals.yml TIMEOUT 120.37 93.86 None systemc/pipeline.cil-1.yml TIMEOUT 120.68 103.42 None seq-mthreaded/pals_lcr-var-start-time.3.ufo.UNBOUNDED.pals.yml TIMEOUT 120.58 93.20 None seq-mthreaded/pals_floodmax.3.2.ufo.BOUNDED-6.pals.yml false(unreach-call) 105.84 67.71 None ------------------------------------------------------------------------------------------------------------------------------- Run set 1 done 105.91 469.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: 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/zeta-merge-clean/BenchexecResults-ReachSafety-XCSP/theta.2024-07-12_14-20-23.results.SV-COMP24_unreach-call.ReachSafety-XCSP.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/zeta-merge-clean/BenchexecResults-ReachSafety-XCSP/theta.2024-07-12_14-20-23.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-07-12 14:20:23 UTC tool: Theta 6.0.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-az975-252 os: Linux-6.5.0-1023-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2841.101 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 120.20 106.22 None Dubois-025.yml TIMEOUT 120.30 108.13 None aim-100-2-0-unsat-4.yml TIMEOUT 120.22 108.52 None AllInterval-014.yml TIMEOUT 120.77 110.28 None AllInterval-005.yml TIMEOUT 120.19 106.97 None ---------------------------------------------------------------------------------------- Run set 1 done 0.62 540.95 - 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) ```