C frontend fix - Githubissues

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/c-frontend-fix/BenchexecResults-ConcurrencySafety-Main/theta.2024-06-15_19-10-06.results.SV-COMP24_unreach-call.ConcurrencySafety-Main.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/c-frontend-fix/BenchexecResults-ConcurrencySafety-Main/theta.2024-06-15_19-10-06.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: Sat, 2024-06-15 19:10:06 UTC tool: Theta 5.1.1 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-298 os: Linux-6.5.0-1021-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3277.539 MHz ram: 16757.354496 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.91 5.06 None pthread-atomic/read_write_lock-1.yml true 11.19 4.23 None pthread-wmm/rfi003_tso.yml TIMEOUT (Parsing OK) 120.71 88.69 None pthread/lazy01.yml false(unreach-call) 7.13 3.10 None pthread-wmm/mix000.oepc.yml false(unreach-call) 20.80 7.85 None ----------------------------------------------------------------------------------------------------------- Run set 1 done 50.13 109.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: 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/c-frontend-fix/BenchexecResults-ConcurrencySafety-MemSafety/theta.2024-06-15_19-09-55.results.SV-COMP24_valid-memsafety.ConcurrencySafety-MemSafety.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/c-frontend-fix/BenchexecResults-ConcurrencySafety-MemSafety/theta.2024-06-15_19-09-55.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: Sat, 2024-06-15 19:09:55 UTC tool: Theta 5.1.1 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-az1501-79 os: Linux-6.5.0-1021-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3240.542 MHz ram: 16757.354496 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.54 4.87 None pthread-atomic/read_write_lock-1.yml true 9.12 3.68 None pthread-wmm/rfi003_tso.yml true 14.64 5.97 None pthread/lazy01.yml true 7.70 3.28 None pthread-wmm/mix000.oepc.yml true 14.01 5.76 None ----------------------------------------------------------------------------------------------------------- Run set 4 done 55.98 24.07 - 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/c-frontend-fix/BenchexecResults-ConcurrencySafety-NoOverflows/theta.2024-06-15_19-09-54.results.SV-COMP24_no-overflow.ConcurrencySafety-NoOverflows.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/c-frontend-fix/BenchexecResults-ConcurrencySafety-NoOverflows/theta.2024-06-15_19-09-54.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: Sat, 2024-06-15 19:09:54 UTC tool: Theta 5.1.1 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-az1501-79 os: Linux-6.5.0-1021-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3145.669 MHz ram: 16757.354496 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.35 5.20 None pthread-atomic/read_write_lock-1.yml true 8.66 3.44 None pthread-wmm/rfi003_tso.yml true 15.75 6.28 None pthread/lazy01.yml true 7.74 3.27 None pthread-wmm/mix000.oepc.yml true 15.49 6.31 None ----------------------------------------------------------------------------------------------------------- Run set 3 done 58.97 25.02 - 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/c-frontend-fix/BenchexecResults-NoDataRace-Main/theta.2024-06-15_19-10-08.results.SV-COMP24_no-data-race.NoDataRace-Main.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/c-frontend-fix/BenchexecResults-NoDataRace-Main/theta.2024-06-15_19-10-08.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: Sat, 2024-06-15 19:10:08 UTC tool: Theta 5.1.1 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-az888-802 os: Linux-6.5.0-1021-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3241.363 MHz ram: 16757.354496 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.91 5.10 None pthread-atomic/read_write_lock-1.yml true 10.94 4.14 None pthread-wmm/rfi003_tso.yml true 18.53 7.15 None pthread/lazy01.yml true 8.04 3.35 None pthread-wmm/mix000.oepc.yml true 16.67 6.68 None ----------------------------------------------------------------------------------------------------------- Run set 2 done 65.06 26.94 - 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/c-frontend-fix/BenchexecResults-ReachSafety-Arrays/theta.2024-06-15_19-08-31.results.SV-COMP24_unreach-call.ReachSafety-Arrays.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/c-frontend-fix/BenchexecResults-ReachSafety-Arrays/theta.2024-06-15_19-08-31.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: Sat, 2024-06-15 19:08:31 UTC tool: Theta 5.1.1 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-298 os: Linux-6.5.0-1021-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3262.006 MHz ram: 16757.354496 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 (Parsing OK) 75.61 161.00 None array-crafted/mapavg4.yml TIMEOUT (Parsing OK) 76.26 161.02 None array-programs/copysome2-1.yml TIMEOUT (Parsing OK) 78.00 161.02 None array-examples/sanfoundry_24-1.yml true 11.14 103.14 None array-multidimensional/max-2-u.yml ERROR (frontend failed) 1.80 0.75 None --------------------------------------------------------------------------------------------------------------- Run set 1 done 13.26 587.77 - 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/c-frontend-fix/BenchexecResults-ReachSafety-BitVectors/theta.2024-06-15_19-07-25.results.SV-COMP24_unreach-call.ReachSafety-BitVectors.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/c-frontend-fix/BenchexecResults-ReachSafety-BitVectors/theta.2024-06-15_19-07-25.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: Sat, 2024-06-15 19:07:25 UTC tool: Theta 5.1.1 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-457 os: Linux-6.5.0-1021-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3242.394 MHz ram: 16757.354496 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.53 2.83 None bitvector/soft_float_1-3a.c.cil.yml false(unreach-call) 30.73 16.75 None bitvector-regression/integerpromotion-3.yml false(unreach-call) 4.87 2.70 None bitvector/sum02-1.yml Parsing OK 35.90 18.14 None bitvector-loops/diamond_2-1.yml TIMEOUT 120.36 79.56 None ------------------------------------------------------------------------------------------------------------ Run set 1 done 77.24 120.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: 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/c-frontend-fix/BenchexecResults-ReachSafety-Combinations/theta.2024-06-15_19-09-04.results.SV-COMP24_unreach-call.ReachSafety-Combinations.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/c-frontend-fix/BenchexecResults-ReachSafety-Combinations/theta.2024-06-15_19-09-04.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: Sat, 2024-06-15 19:09:04 UTC tool: Theta 5.1.1 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-az887-100 os: Linux-6.5.0-1021-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3241.484 MHz ram: 16757.3504 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 (Parsing OK) 120.48 73.71 None Problem05_label47+token_ring.02.cil-1.yml TIMEOUT 120.22 97.29 None pc_sfifo_3.cil+token_ring.11.cil-1.yml TIMEOUT 120.04 107.20 None Problem05_label45+token_ring.01.cil-2.yml TIMEOUT 120.58 93.45 None pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label04.yml TIMEOUT (Parsing OK) 120.19 69.24 None ---------------------------------------------------------------------------------------------------------------------- Run set 1 done 0.60 442.02 - 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/c-frontend-fix/BenchexecResults-ReachSafety-ControlFlow/theta.2024-06-15_19-07-35.results.SV-COMP24_unreach-call.ReachSafety-ControlFlow.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/c-frontend-fix/BenchexecResults-ReachSafety-ControlFlow/theta.2024-06-15_19-07-35.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: Sat, 2024-06-15 19:07:35 UTC tool: Theta 5.1.1 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-az1778-489 os: Linux-6.5.0-1021-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3191.516 MHz ram: 16757.354496 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) 4.17 1.46 None locks/test_locks_11.yml TIMEOUT (Parsing OK) 122.91 103.00 None locks/test_locks_5.yml true 13.70 5.31 None longjmp/68-longjmp_18-simple-else_unknown_2_pos.yml ERROR (frontend failed) 4.43 1.58 None longjmp/68-longjmp_11-counting-return_true.yml ERROR (frontend failed) 1.93 0.80 None -------------------------------------------------------------------------------------------------------------------- Run set 1 done 23.71 113.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: 8) ```

:question: ReachSafety-ECA (0 / 0 / 5)

`table-generator` output: [HTML](https://theta.mit.bme.hu/benchmark-results/c-frontend-fix/BenchexecResults-ReachSafety-ECA/theta.2024-06-15_19-10-51.results.SV-COMP24_unreach-call.ReachSafety-ECA.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/c-frontend-fix/BenchexecResults-ReachSafety-ECA/theta.2024-06-15_19-10-51.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: Sat, 2024-06-15 19:10:51 UTC tool: Theta 5.1.1 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-az654-952 os: Linux-6.5.0-1021-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3243.517 MHz ram: 16757.354496 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 (Parsing OK) 121.29 79.09 None eca-rers2012/Problem06_label11.yml TIMEOUT (Parsing OK) 120.55 72.92 None eca-programs/Problem101_label07.yml TIMEOUT 121.16 73.60 None eca-rers2012/Problem05_label44.yml TIMEOUT (Parsing OK) 121.20 73.22 None eca-rers2012/Problem04_label05.yml TIMEOUT (Parsing OK) 120.94 74.43 None ---------------------------------------------------------------------------------------------------- Run set 1 done 0.60 376.19 - 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/c-frontend-fix/BenchexecResults-ReachSafety-Floats/theta.2024-06-15_19-10-20.results.SV-COMP24_unreach-call.ReachSafety-Floats.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/c-frontend-fix/BenchexecResults-ReachSafety-Floats/theta.2024-06-15_19-10-20.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: Sat, 2024-06-15 19:10:20 UTC tool: Theta 5.1.1 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-963 os: Linux-6.5.0-1021-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3244.178 MHz ram: 16757.3504 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.56 2.85 None float-benchs/zonotope_loose.c.v+cfa-reducer.yml TIMEOUT (Parsing OK) 120.41 113.37 None float-benchs/float_int_inv_square.yml false(unreach-call) 6.78 3.21 None floats-cdfpl/square_3.yml false(unreach-call) 78.50 74.54 None floats-cbmc-regression/float11.yml true 5.35 2.83 None ---------------------------------------------------------------------------------------------------------------- Run set 1 done 24.41 197.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: 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/c-frontend-fix/BenchexecResults-ReachSafety-Hardware/theta.2024-06-15_19-10-40.results.SV-COMP24_unreach-call.ReachSafety-Hardware.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/c-frontend-fix/BenchexecResults-ReachSafety-Hardware/theta.2024-06-15_19-10-40.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: Sat, 2024-06-15 19:10:40 UTC tool: Theta 5.1.1 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-963 os: Linux-6.5.0-1021-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2760.51 MHz ram: 16757.354496 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.62 111.75 None btor2c-lazyMod.cambridge.5.prop1-back-serstep.yml TIMEOUT (Parsing OK) 120.50 98.62 None btor2c-lazyMod.extinction.4.prop1-func-interl.yml TIMEOUT (Parsing OK) 120.44 94.46 None btor2c-lazyMod.lup.2.prop1-func-interl.yml TIMEOUT (Parsing OK) 121.89 94.39 None btor2c-lazyMod.train-gate.6.prop1-func-interl.yml TIMEOUT (Parsing OK) 120.15 84.88 None ------------------------------------------------------------------------------------------------------------------ Run set 1 done 0.58 486.73 - 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/c-frontend-fix/BenchexecResults-ReachSafety-Heap/theta.2024-06-15_19-07-58.results.SV-COMP24_unreach-call.ReachSafety-Heap.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/c-frontend-fix/BenchexecResults-ReachSafety-Heap/theta.2024-06-15_19-07-58.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: Sat, 2024-06-15 19:07:58 UTC tool: Theta 5.1.1 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-207 os: Linux-6.5.0-1021-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2807.122 MHz ram: 16757.354496 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.58 4.58 None test15.yml true 8.41 4.20 None just_assert.yml true 5.41 2.77 None volatile_alias.yml true 7.72 4.07 None mutex_lock_int.c_1.yml true 8.64 4.25 None --------------------------------------------------------------------------------------- Run set 1 done 39.73 20.40 - 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/c-frontend-fix/BenchexecResults-ReachSafety-Loops/theta.2024-06-15_19-09-40.results.SV-COMP24_unreach-call.ReachSafety-Loops.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/c-frontend-fix/BenchexecResults-ReachSafety-Loops/theta.2024-06-15_19-09-40.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: Sat, 2024-06-15 19:09:40 UTC tool: Theta 5.1.1 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-481 os: Linux-6.5.0-1021-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3220.253 MHz ram: 16757.354496 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 (Parsing OK) 120.43 107.03 None loop-crafted/simple_vardep_2.yml TIMEOUT (Parsing OK) 120.80 109.87 None nla-digbench-scaling/divbin_valuebound100.yml TIMEOUT (Parsing OK) 120.65 107.92 None nla-digbench-scaling/mannadiv_valuebound50.yml true 21.98 9.76 None nla-digbench-scaling/mannadiv_unwindbound10.yml Parsing OK 28.28 11.61 None ---------------------------------------------------------------------------------------------------------------- Run set 1 done 50.56 347.02 - 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/c-frontend-fix/BenchexecResults-ReachSafety-Recursive/theta.2024-06-15_19-07-43.results.SV-COMP24_unreach-call.ReachSafety-Recursive.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/c-frontend-fix/BenchexecResults-ReachSafety-Recursive/theta.2024-06-15_19-07-43.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: Sat, 2024-06-15 19:07:43 UTC tool: Theta 5.1.1 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-az887-100 os: Linux-6.5.0-1021-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3186.165 MHz ram: 16757.3504 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.96 7.00 None recursive-simple/id2_i5_o5-2.yml true 12.78 4.60 None recursified_nla-digbench/recursified_geo2-ll.yml TIMEOUT (Parsing OK) 33.21 161.02 None recursive/recHanoi03-2.yml TIMEOUT (Parsing OK) 120.31 91.53 None recursified_nla-digbench/recursified_lcm2.yml TIMEOUT (Parsing OK) 120.34 114.51 None ----------------------------------------------------------------------------------------------------------------- Run set 1 done 30.05 380.12 - 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/c-frontend-fix/BenchexecResults-ReachSafety-Sequentialized/theta.2024-06-15_19-08-50.results.SV-COMP24_unreach-call.ReachSafety-Sequentialized.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/c-frontend-fix/BenchexecResults-ReachSafety-Sequentialized/theta.2024-06-15_19-08-50.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: Sat, 2024-06-15 19:08:50 UTC tool: Theta 5.1.1 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-az1759-424 os: Linux-6.5.0-1021-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 2756.789 MHz ram: 16757.354496 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.48 108.43 None seq-mthreaded/pals_opt-floodmax.3.1.ufo.UNBOUNDED.pals.yml TIMEOUT (Parsing OK) 120.32 94.91 None systemc/pipeline.cil-1.yml TIMEOUT 120.65 104.14 None seq-mthreaded/pals_lcr-var-start-time.3.ufo.UNBOUNDED.pals.yml TIMEOUT (Parsing OK) 120.69 94.33 None seq-mthreaded/pals_floodmax.3.2.ufo.BOUNDED-6.pals.yml false(unreach-call) 102.21 66.94 None ------------------------------------------------------------------------------------------------------------------------------- Run set 1 done 100.93 470.18 - 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/c-frontend-fix/BenchexecResults-ReachSafety-XCSP/theta.2024-06-15_19-07-31.results.SV-COMP24_unreach-call.ReachSafety-XCSP.html)/[CSV](https://theta.mit.bme.hu/benchmark-results/c-frontend-fix/BenchexecResults-ReachSafety-XCSP/theta.2024-06-15_19-07-31.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: Sat, 2024-06-15 19:07:31 UTC tool: Theta 5.1.1 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-az1759-424 os: Linux-6.5.0-1021-azure-x86_64-with-glibc2.35 cpu: AMD EPYC 7763 64-Core Processor - cores: 4 - max frequency: 3240.339 MHz ram: 16757.354496 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.30 None Dubois-025.yml TIMEOUT 120.62 105.25 None aim-100-2-0-unsat-4.yml TIMEOUT 120.31 107.96 None AllInterval-014.yml TIMEOUT 120.36 105.75 None AllInterval-005.yml TIMEOUT 120.34 105.09 None ---------------------------------------------------------------------------------------- Run set 1 done 0.59 530.38 - 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) ```

ftsrg / theta

C frontend fix #252

Quality Gate failed