C frontend fix #252

leventeBajczi · 2024-02-28T12:01:19Z

Fixes around our C frontend, including:

__PRETTY_FUNC__ ignored
sleep() ignored
pthread_* implemented
pointer support merged (successor of Pointer support #239)
Added --enable-output flag to globally enable/disable file outputs
Fixed a problem with the portfolio where it exited after the first error

…o xcfa-oc

sonarqubecloud · 2024-06-15T19:05:26Z

Quality Gate failed

Failed conditions
31.3% Coverage on New Code (required ≥ 60%)

See analysis details on SonarCloud

github-actions · 2024-06-15T19:21:01Z

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

✅ ConcurrencySafety-Main (3 / 0 / 5)

table-generator output: HTML/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)

✅ ConcurrencySafety-MemSafety (4 / 0 / 5)

table-generator output: HTML/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)

✅ ConcurrencySafety-NoOverflows (4 / 0 / 5)

table-generator output: HTML/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)

✅ NoDataRace-Main (4 / 0 / 5)

table-generator output: HTML/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)

✅ ReachSafety-Arrays (1 / 0 / 5)

table-generator output: HTML/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)

✅ ReachSafety-BitVectors (3 / 0 / 5)

table-generator output: HTML/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)

❓ ReachSafety-Combinations (0 / 0 / 5)

table-generator output: HTML/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)

✅ ReachSafety-ControlFlow (1 / 0 / 5)

table-generator output: HTML/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)

❓ ReachSafety-ECA (0 / 0 / 5)

table-generator output: HTML/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)

✅ ReachSafety-Floats (4 / 0 / 5)

table-generator output: HTML/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)

❓ ReachSafety-Hardware (0 / 0 / 5)

table-generator output: HTML/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)

✅ ReachSafety-Heap (5 / 0 / 5)

table-generator output: HTML/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)

✅ ReachSafety-Loops (1 / 0 / 5)

table-generator output: HTML/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)

✅ ReachSafety-Recursive (1 / 0 / 5)

table-generator output: HTML/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)

✅ ReachSafety-Sequentialized (1 / 0 / 5)

table-generator output: HTML/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)

❓ ReachSafety-XCSP (0 / 0 / 5)

table-generator output: HTML/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)

leventeBajczi added the Ready to test This will run the final sonar check in PRs. label Feb 28, 2024

csanadtelbisz and others added 29 commits March 3, 2024 22:35

immediate version

7f7a23b

basic working version

db60b68

retrieving trace

d2fd28e

oc checker no ssa

c25860c

general params in prec vars

ae3efd4

mutextovarpass

4c94fff

intermediate commit

18a41fa

basic oc solver

b751542

atomic support

37185bf

same procedure fix

6660a3c

guard thread var fix

1e6d3cd

atomic block global var read-write access limitations

ebfd0ce

atomic fix

1d7cfc5

oc config, derive fix

63248be

violation guard fix

aeca14e

global declaration fix

1204710

Added javasmt-solver as new subproject

a28479d

Added CVC5 libraries, fixed some bugs

ac9b50e

Fixed interpolation, and tests

d93deef

Fixed JavaSMTTransformerTest

1c6abba

Implemented some missing exprs

bb0fa05

Added lots more tests, aiming for 100% coverage

718673b

Updated tests and implementation

a9784bf

Reformatted code

922dbd0

version bump

da0ad6e

Fixed errors

c575e51

Limited max memory for tests on the jvm

e1757ad

Added --max-workers 2 --no-daemon to CI

cfc6c0f

Added flags to sonar as well

26d2cb1

leventeBajczi and others added 17 commits May 3, 2024 11:31

Moved counters to companion object

3fed4e0

added enabling switch to FEW pass

46c83f9

Merge remote-tracking branch 'refs/remotes/origin/c-frontend-fix' int…

39f831c

…o xcfa-oc

Fix FEW

a38b6b8

Merge remote-tracking branch 'refs/remotes/origin/c-frontend-fix' int…

ef0845b

…o xcfa-oc

por mutex fence var empty name fix

ac5ef13

simplify exprs constant propagation

474667b

spor+coi

6d1cad9

When ERR+multithread, use DFS

c2a4de4

Fixed multi-type derefs

f3f2cf2

Various frontend fixes regarding dereferences

95a5e58

Fixes to allow javasmt:mathsat to work with pointers

49de255

Fixed compile errors in tests

35dce04

added missing function decl

6316582

Removed array task from IMC/kind

0dc10ec

Fixed expected witness edge info

61fbbf4

Removed map from state

1d1914f

leventeBajczi force-pushed the c-frontend-fix branch from 0da0240 to 1d1914f Compare May 21, 2024 16:00

thetabotmaintainer bot and others added 8 commits May 22, 2024 14:47

Reformatted code

d2eb799

Reapplied copyright

09539f1

Fixed test outcome

5b28139

Removed M1 mac from ci

94cb88d

Fixed cast

4ef4cee

Fixed float problem, added error for PRED_SPLIT

9afa6dd

Fixed compilation error

0f35b6b

Fixed test

9f48fe6

leventeBajczi merged commit b42b297 into master Jun 15, 2024
83 of 84 checks passed

leventeBajczi deleted the c-frontend-fix branch June 15, 2024 19:22

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

C frontend fix #252

C frontend fix #252

leventeBajczi commented Feb 28, 2024 •

edited

Loading

sonarqubecloud bot commented Jun 15, 2024

github-actions bot commented Jun 15, 2024

C frontend fix #252

C frontend fix #252

Conversation

leventeBajczi commented Feb 28, 2024 • edited Loading

sonarqubecloud bot commented Jun 15, 2024

Quality Gate failed

github-actions bot commented Jun 15, 2024

leventeBajczi commented Feb 28, 2024 •

edited

Loading