Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Allow $ in xsts variable names #287

Merged
merged 2 commits into from
Jul 31, 2024
Merged

Allow $ in xsts variable names #287

merged 2 commits into from
Jul 31, 2024

Conversation

mondokm
Copy link
Contributor

@mondokm mondokm commented Jul 31, 2024

This PR allows $ in XSTS variable names, closing #265

@mondokm mondokm linked an issue Jul 31, 2024 that may be closed by this pull request
Allow "$" in XSTS variable names #265
Closed
@mondokm mondokm added the Ready to test This will run the final sonar check in PRs. label Jul 31, 2024
@sonarcloud SonarCloud
Copy link

sonarcloud bot commented Jul 31, 2024

Quality Gate Passed Quality Gate passed

Issues
0 New issues
0 Accepted issues

Measures
0 Security Hotspots
0.0% Coverage on New Code
0.0% Duplication on New Code

See analysis details on SonarCloud

@github-actions GitHub Actions
Copy link

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:                    Wed, 2024-07-31 10:35:25 UTC
tool:                    Theta 6.2.3
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-az1536-525
os:                      Linux-6.5.0-1024-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         2592.775 MHz
ram:                     16757.338112 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.81        5.19        None
pthread-atomic/read_write_lock-1.yml          true                            10.93        4.12        None
pthread-wmm/rfi003_tso.yml                    TIMEOUT                        120.81       89.13        None
pthread/lazy01.yml                            false(unreach-call)              7.08        3.07        None
pthread-wmm/mix000.oepc.yml                   false(unreach-call)             18.39        6.95        None
-----------------------------------------------------------------------------------------------------------
Run set 1                                     done                            47.30      109.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:               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:                    Wed, 2024-07-31 10:35:18 UTC
tool:                    Theta 6.2.3
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-az849-821
os:                      Linux-6.5.0-1024-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3010.912 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.73        5.22        None
pthread-atomic/read_write_lock-1.yml          true                             8.64        3.41        None
pthread-wmm/rfi003_tso.yml                    true                            13.82        5.75        None
pthread/lazy01.yml                            true                             6.97        3.04        None
pthread-wmm/mix000.oepc.yml                   true                            14.27        5.84        None
-----------------------------------------------------------------------------------------------------------
Run set 4                                     done                            54.41       23.78           -

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:                    Wed, 2024-07-31 10:35:25 UTC
tool:                    Theta 6.2.3
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-az525-159
os:                      Linux-6.5.0-1024-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3149.845 MHz
ram:                     16757.342208000002 MB
------------------------------------------------------------



SV-COMP24_unreach-call
Run set 1 of 4: skipped because it has no files


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow.ConcurrencySafety-NoOverflows
Run set 3 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                                     status                       cpu time   wall time        host
-----------------------------------------------------------------------------------------------------------
pthread-ext/18_read_write_lock-pthread.yml    Parsing OK                      12.01        5.47        None
pthread-atomic/read_write_lock-1.yml          true                             9.54        3.72        None
pthread-wmm/rfi003_tso.yml                    true                            16.17        6.51        None
pthread/lazy01.yml                            true                             7.84        3.32        None
pthread-wmm/mix000.oepc.yml                   true                            15.08        6.18        None
-----------------------------------------------------------------------------------------------------------
Run set 3                                     done                            60.61       25.74           -


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:                    Wed, 2024-07-31 10:35:30 UTC
tool:                    Theta 6.2.3
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-az849-821
os:                      Linux-6.5.0-1024-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         2813.461 MHz
ram:                     16757.342208000002 MB
------------------------------------------------------------



SV-COMP24_unreach-call
Run set 1 of 4: skipped because it has no files


SV-COMP24_no-data-race.NoDataRace-Main
Run set 2 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                                     status                       cpu time   wall time        host
-----------------------------------------------------------------------------------------------------------
pthread-ext/18_read_write_lock-pthread.yml    Parsing OK                      10.58        5.13        None
pthread-atomic/read_write_lock-1.yml          true                            11.50        4.31        None
pthread-wmm/rfi003_tso.yml                    true                            17.95        7.02        None
pthread/lazy01.yml                            true                             7.87        3.24        None
pthread-wmm/mix000.oepc.yml                   true                            17.73        6.91        None
-----------------------------------------------------------------------------------------------------------
Run set 2                                     done                            65.61       27.14           -


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:                    Wed, 2024-07-31 10:33:54 UTC
tool:                    Theta 6.2.3
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-az1144-461
os:                      Linux-6.5.0-1024-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3193.482 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.46      161.00        None
array-crafted/mapavg4.yml                         TIMEOUT                         77.56      161.02        None
array-programs/copysome2-1.yml                    TIMEOUT                         78.15      161.02        None
array-examples/sanfoundry_24-1.yml                true                            12.01      103.28        None
array-multidimensional/max-2-u.yml                ERROR (frontend failed)          1.79        0.76        None
---------------------------------------------------------------------------------------------------------------
Run set 1                                         done                            14.15      588.31           -


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:                    Wed, 2024-07-31 10:32:51 UTC
tool:                    Theta 6.2.3
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-az1014-921
os:                      Linux-6.5.0-1024-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3084.605 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.40        3.11        None
bitvector/soft_float_1-3a.c.cil.yml            false(unreach-call)             34.85       18.62        None
bitvector-regression/integerpromotion-3.yml    false(unreach-call)              5.34        3.01        None
bitvector/sum02-1.yml                          Parsing OK                      38.05       19.28        None
bitvector-loops/diamond_2-1.yml                TIMEOUT                        121.04      109.51        None
------------------------------------------------------------------------------------------------------------
Run set 1                                      done                            80.14      154.16           -


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:                    Wed, 2024-07-31 10:34:32 UTC
tool:                    Theta 6.2.3
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-az1424-702
os:                      Linux-6.5.0-1024-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3219.234 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.77       71.87        None
Problem05_label47+token_ring.02.cil-1.yml                TIMEOUT                        120.36       94.79        None
pc_sfifo_3.cil+token_ring.11.cil-1.yml                   TIMEOUT                        120.29      107.25        None
Problem05_label45+token_ring.01.cil-2.yml                TIMEOUT                        120.39       94.75        None
pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label04.yml    TIMEOUT                        120.62       67.85        None
----------------------------------------------------------------------------------------------------------------------
Run set 1                                                done                             0.61      437.63           -


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:                    Wed, 2024-07-31 10:33:00 UTC
tool:                    Theta 6.2.3
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-az881-897
os:                      Linux-6.5.0-1024-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         2941.616 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)          4.34        1.55        None
locks/test_locks_11.yml                                TIMEOUT                        123.45      103.36        None
locks/test_locks_5.yml                                 true                            14.56        5.50        None
longjmp/68-longjmp_18-simple-else_unknown_2_pos.yml    ERROR (frontend failed)          4.81        1.73        None
longjmp/68-longjmp_11-counting-return_true.yml         ERROR (frontend failed)          2.08        0.86        None
--------------------------------------------------------------------------------------------------------------------
Run set 1                                              done                            25.87      113.62           -


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


SV-COMP24_valid-memsafety
Run set 4 of 4: skipped because it has no files

Statistics:              5 Files
  correct:               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:                    Wed, 2024-07-31 10:36:11 UTC
tool:                    Theta 6.2.3
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-az1110-82
os:                      Linux-6.5.0-1024-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3227.835 MHz
ram:                     16757.342208000002 MB
------------------------------------------------------------



SV-COMP24_unreach-call.ReachSafety-ECA
Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                              status                       cpu time   wall time        host
----------------------------------------------------------------------------------------------------
eca-rers2012/Problem06_label18.yml     TIMEOUT                        122.24       77.87        None
eca-rers2012/Problem06_label11.yml     TIMEOUT                        120.16       75.27        None
eca-programs/Problem101_label07.yml    TIMEOUT                        121.07       74.44        None
eca-rers2012/Problem05_label44.yml     TIMEOUT                        120.27       72.84        None
eca-rers2012/Problem04_label05.yml     TIMEOUT                        120.94       75.25        None
----------------------------------------------------------------------------------------------------
Run set 1                              done                             0.59      378.60           -


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


SV-COMP24_valid-memsafety
Run set 4 of 4: skipped because it has no files

Statistics:              5 Files
  correct:               0
    correct true:        0
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               5
  Score:                 0 (max: 7)
✅ 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:                    Wed, 2024-07-31 10:35:36 UTC
tool:                    Theta 6.2.3
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-az1391-55
os:                      Linux-6.5.0-1024-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3183.503 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.76        2.93        None
float-benchs/zonotope_loose.c.v+cfa-reducer.yml    TIMEOUT                        120.45      112.56        None
float-benchs/float_int_inv_square.yml              false(unreach-call)              6.47        3.13        None
floats-cdfpl/square_3.yml                          false(unreach-call)             74.76       71.19        None
floats-cbmc-regression/float11.yml                 true                             5.17        2.91        None
----------------------------------------------------------------------------------------------------------------
Run set 1                                          done                            24.18      193.75           -


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:                    Wed, 2024-07-31 10:36:09 UTC
tool:                    Theta 6.2.3
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-az1380-767
os:                      Linux-6.5.0-1024-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         2991.517 MHz
ram:                     16757.342208000002 MB
------------------------------------------------------------



SV-COMP24_unreach-call.ReachSafety-Hardware
Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                                            status                       cpu time   wall time        host
------------------------------------------------------------------------------------------------------------------
btor2c-lazyMod.arbitrated_top_n4_w16_d32_e0.yml      TIMEOUT                        120.62      111.91        None
btor2c-lazyMod.cambridge.5.prop1-back-serstep.yml    TIMEOUT                        120.45       99.09        None
btor2c-lazyMod.extinction.4.prop1-func-interl.yml    TIMEOUT                        120.45       94.82        None
btor2c-lazyMod.lup.2.prop1-func-interl.yml           TIMEOUT                        120.46       94.47        None
btor2c-lazyMod.train-gate.6.prop1-func-interl.yml    TIMEOUT                        120.56       83.42        None
------------------------------------------------------------------------------------------------------------------
Run set 1                                            done                             0.62      485.93           -


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:                    Wed, 2024-07-31 10:33:21 UTC
tool:                    Theta 6.2.3
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az1108-493
os:                      Linux-6.5.0-1024-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3243.254 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.77        4.81        None
test15.yml                true                             8.73        4.59        None
just_assert.yml           true                             5.65        2.72        None
volatile_alias.yml        true                             7.99        4.17        None
mutex_lock_int.c_1.yml    true                             8.82        4.49        None
---------------------------------------------------------------------------------------
Run set 1                 done                            40.92       21.31           -


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:                    Wed, 2024-07-31 10:35:04 UTC
tool:                    Theta 6.2.3
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az735-305
os:                      Linux-6.5.0-1024-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         2730.568 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.46      106.93        None
loop-crafted/simple_vardep_2.yml                   TIMEOUT                        120.75      109.99        None
nla-digbench-scaling/divbin_valuebound100.yml      TIMEOUT                        120.67      107.38        None
nla-digbench-scaling/mannadiv_valuebound50.yml     true                            22.60        9.97        None
nla-digbench-scaling/mannadiv_unwindbound10.yml    Parsing OK                      28.69       12.59        None
----------------------------------------------------------------------------------------------------------------
Run set 1                                          done                            51.52      347.69           -


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:                    Wed, 2024-07-31 10:33:12 UTC
tool:                    Theta 6.2.3
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-az2021-574
os:                      Linux-6.5.0-1024-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3197.488 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.94        7.18        None
recursive-simple/id2_i5_o5-2.yml                    true                            13.07        5.07        None
recursified_nla-digbench/recursified_geo2-ll.yml    TIMEOUT                         33.37      161.03        None
recursive/recHanoi03-2.yml                          TIMEOUT                        120.16       92.90        None
recursified_nla-digbench/recursified_lcm2.yml       TIMEOUT                        120.37      113.95        None
-----------------------------------------------------------------------------------------------------------------
Run set 1                                           done                            30.32      381.51           -


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:                    Wed, 2024-07-31 10:34:16 UTC
tool:                    Theta 6.2.3
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-816
os:                      Linux-6.5.0-1024-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3249.728 MHz
ram:                     16757.342208000002 MB
------------------------------------------------------------



SV-COMP24_unreach-call.ReachSafety-Sequentialized
Run set 1 of 4 with options '--disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO' and propertyfile 'None'

inputfile                                                         status                       cpu time   wall time        host
-------------------------------------------------------------------------------------------------------------------------------
systemc/transmitter.12.cil.yml                                    TIMEOUT                        120.22      107.88        None
seq-mthreaded/pals_opt-floodmax.3.1.ufo.UNBOUNDED.pals.yml        TIMEOUT                        120.41       93.41        None
systemc/pipeline.cil-1.yml                                        TIMEOUT                        120.59      103.95        None
seq-mthreaded/pals_lcr-var-start-time.3.ufo.UNBOUNDED.pals.yml    TIMEOUT                        120.56       93.74        None
seq-mthreaded/pals_floodmax.3.2.ufo.BOUNDED-6.pals.yml            false(unreach-call)            103.36       66.99        None
-------------------------------------------------------------------------------------------------------------------------------
Run set 1                                                         done                           102.07      467.39           -


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


SV-COMP24_valid-memsafety
Run set 4 of 4: skipped because it has no files

Statistics:              5 Files
  correct:               1
    correct true:        0
    correct false:       1
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               4
  Score:                 1 (max: 6)
❓ 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:                    Wed, 2024-07-31 10:32:55 UTC
tool:                    Theta 6.2.3
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-az885-996
os:                      Linux-6.5.0-1024-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         2964.501 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.06      107.61        None
Dubois-025.yml             TIMEOUT                        120.20      107.84        None
aim-100-2-0-unsat-4.yml    TIMEOUT                        120.43      105.65        None
AllInterval-014.yml        TIMEOUT                        120.85      109.35        None
AllInterval-005.yml        TIMEOUT                        120.37      105.57        None
----------------------------------------------------------------------------------------
Run set 1                  done                             0.60      537.05           -


SV-COMP24_no-data-race
Run set 2 of 4: skipped because it has no files


SV-COMP24_no-overflow
Run set 3 of 4: skipped because it has no files


SV-COMP24_valid-memsafety
Run set 4 of 4: skipped because it has no files

Statistics:              5 Files
  correct:               0
    correct true:        0
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               5
  Score:                 0 (max: 7)

@mondokm mondokm merged commit 1dba638 into master Jul 31, 2024
83 checks passed
@mondokm mondokm deleted the xstsvarname branch July 31, 2024 11:28
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
Ready to test This will run the final sonar check in PRs.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Allow "$" in XSTS variable names
1 participant
@mondokm