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

Enhance PR messaging for checks #259

Closed

leventeBajczi wants to merge 23 commits into master from enhance-pr

Contributor

leventeBajczi commented Mar 19, 2024

No description provided.

leventeBajczi added 2 commits

March 19, 2024 12:42


          Added suggestion for check-version

d84f2d2


          Fixed version

9f103b0

leventeBajczi marked this pull request as ready for review

March 19, 2024 11:44

leventeBajczi added 21 commits

March 19, 2024 12:46


          Update check-version.yml

5eb176e


          Fixed bash function

c3eba05


          Instead of proper gradle command, using grep

472ea5c


          Fixed reviewdog

b73825e


          Fixed reviewdog

3cc0343


          Adding comment

3430f51


          Trying with app token

befc6c0


          Fixed reviewdog

8850e8e


          Added diagnostic log

bd080f3


          Retrying with github token

84576ab


          added debug logging

0c11a5d


          fail-on-error

406b518


          Trying ' -f.diff.strip=0'

f633b26


          Trying suggested pattern

f9ea339


          Trying non-failing check

8ab036f


          trying nofilter

9fc050b


          fail-on-error


          -level=warning

14f93fa


          debug

0d86ee3


          Trial commit

ae6c4e6

fix

c98355a

github-actions bot reviewed

View reviewed changes

.github/workflows/check-version.yml

+                        IFS='.' read -r -a array <<< "${{ steps.new_version.outputs.version }}"
+                        new_version="${array[0]}.${array[1]}.$((array[2]+1))"
+                        #sed -i "s/version = \".*\"/version = \"$new_version\"/" build.gradle.kts
+                        sed -i "s/proba/proba2/g" .github/workflows/check-version.yml

github-actions bot Mar 19, 2024

[diff] _{reported by reviewdog 🐶}

Suggested change

      
                      sed -i "s/proba/proba2/g" .github/workflows/check-version.yml
          
                      sed -i "s/proba2/proba22/g" .github/workflows/check-version.yml

leventeBajczi closed this

leventeBajczi deleted the enhance-pr branch

March 19, 2024 13:12

github-actions bot commented Mar 19, 2024

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:                    Tue, 2024-03-19 13:25:57 UTC
tool:                    Theta 5.0.4
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az1206-875
os:                      Linux-6.5.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         2415.991 MHz
ram:                     16757.3504 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                       6.00        2.74        None
pthread-atomic/read_write_lock-1.yml          true                            12.40        4.50        None
pthread-wmm/rfi003_tso.yml                    TIMEOUT (Parsing OK)           120.26       90.36        None
pthread/lazy01.yml                            false(unreach-call)              8.71        3.62        None
pthread-wmm/mix000.oepc.yml                   false(unreach-call)             12.88        4.64        None
-----------------------------------------------------------------------------------------------------------
Run set 1                                     done                            40.09      106.50           -


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:                    Tue, 2024-03-19 13:25:33 UTC
tool:                    Theta 5.0.4
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-az1208-527
os:                      Linux-6.5.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3242.329 MHz
ram:                     16757.3504 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                       5.09        2.41        None
pthread-atomic/read_write_lock-1.yml          true                             9.16        3.66        None
pthread-wmm/rfi003_tso.yml                    true                            10.77        4.07        None
pthread/lazy01.yml                            true                             6.84        3.02        None
pthread-wmm/mix000.oepc.yml                   true                             9.89        3.83        None
-----------------------------------------------------------------------------------------------------------
Run set 4                                     done                            41.73       17.51           -

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:                    Tue, 2024-03-19 13:25:26 UTC
tool:                    Theta 5.0.4
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-az891-499
os:                      Linux-6.5.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3298.635 MHz
ram:                     16757.3504 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                       5.70        2.59        None
pthread-atomic/read_write_lock-1.yml          true                             9.50        3.74        None
pthread-wmm/rfi003_tso.yml                    true                            11.19        4.18        None
pthread/lazy01.yml                            true                             7.39        3.13        None
pthread-wmm/mix000.oepc.yml                   true                            10.83        4.06        None
-----------------------------------------------------------------------------------------------------------
Run set 3                                     done                            44.59       18.23           -


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:                    Tue, 2024-03-19 13:25:50 UTC
tool:                    Theta 5.0.4
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-az1240-768
os:                      Linux-6.5.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3189.794 MHz
ram:                     16757.3504 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                       5.93        2.70        None
pthread-atomic/read_write_lock-1.yml          true                            12.72        4.71        None
pthread-wmm/rfi003_tso.yml                    true                            15.07        5.36        None
pthread/lazy01.yml                            true                             7.02        3.06        None
pthread-wmm/mix000.oepc.yml                   true                            13.50        4.91        None
-----------------------------------------------------------------------------------------------------------
Run set 2                                     done                            54.23       21.26           -


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 (0 / 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:                    Tue, 2024-03-19 13:24:11 UTC
tool:                    Theta 5.0.4
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-az1146-613
os:                      Linux-6.5.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         2894.692 MHz
ram:                     16757.3504 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    Parsing OK                     113.04      101.16        None
array-crafted/mapavg4.yml                         Parsing OK                     114.44      101.26        None
array-programs/copysome2-1.yml                    Parsing OK                     113.43      101.17        None
array-examples/sanfoundry_24-1.yml                Parsing OK                       8.88        3.85        None
array-multidimensional/max-2-u.yml                Parsing OK                     118.57      101.32        None
---------------------------------------------------------------------------------------------------------------
Run set 1                                         done                            21.75      409.28           -


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: 10)

✅ ReachSafety-BitVectors (2 / 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:                    Tue, 2024-03-19 13:23:14 UTC
tool:                    Theta 5.0.4
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-az1240-768
os:                      Linux-6.5.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3244.177 MHz
ram:                     16757.3504 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                             9.32        3.76        None
bitvector/soft_float_1-3a.c.cil.yml            Parsing OK                      13.23        4.87        None
bitvector-regression/integerpromotion-3.yml    false(unreach-call)              6.53        3.15        None
bitvector/sum02-1.yml                          Parsing OK                       7.14        3.14        None
bitvector-loops/diamond_2-1.yml                Parsing OK                       8.47        3.48        None
------------------------------------------------------------------------------------------------------------
Run set 1                                      done                            44.66       18.92           -


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:               2
    correct true:        1
    correct false:       1
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               3
  Score:                 3 (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:                    Tue, 2024-03-19 13:24:47 UTC
tool:                    Theta 5.0.4
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-az1146-613
os:                      Linux-6.5.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3242.571 MHz
ram:                     16757.346304 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                   Parsing OK                      47.04       26.01        None
Problem05_label47+token_ring.02.cil-1.yml                TIMEOUT (Parsing OK)           122.00       80.19        None
pc_sfifo_3.cil+token_ring.11.cil-1.yml                   TIMEOUT (Parsing OK)           120.10       93.86        None
Problem05_label45+token_ring.01.cil-2.yml                TIMEOUT (Parsing OK)           122.41       75.33        None
pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label04.yml    Parsing OK                      63.28       32.27        None
----------------------------------------------------------------------------------------------------------------------
Run set 1                                                done                           104.30      309.68           -


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


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


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

Statistics:              5 Files
  correct:               0
    correct true:        0
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               5
  Score:                 0 (max: 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:                    Tue, 2024-03-19 13:23:19 UTC
tool:                    Theta 5.0.4
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-826
os:                      Linux-6.5.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3243.186 MHz
ram:                     16757.346304 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    Parsing OK                       8.09        3.51        None
locks/test_locks_11.yml                                Parsing OK                     116.70      101.36        None
locks/test_locks_5.yml                                 true                            13.78        5.28        None
longjmp/68-longjmp_18-simple-else_unknown_2_pos.yml    Parsing OK                       8.49        3.73        None
longjmp/68-longjmp_11-counting-return_true.yml         Parsing OK                       6.58        2.90        None
--------------------------------------------------------------------------------------------------------------------
Run set 1                                              done                            40.23      117.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: 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:                    Tue, 2024-03-19 13:26:29 UTC
tool:                    Theta 5.0.4
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-az575-265
os:                      Linux-6.5.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         2945.079 MHz
ram:                     16757.3504 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)           120.41       78.62        None
eca-rers2012/Problem06_label11.yml     TIMEOUT (Parsing OK)           120.84       74.00        None
eca-programs/Problem101_label07.yml    TIMEOUT                        120.40       66.94        None
eca-rers2012/Problem05_label44.yml     TIMEOUT (Parsing OK)           120.77       71.62        None
eca-rers2012/Problem04_label05.yml     TIMEOUT (Parsing OK)           120.57       78.11        None
----------------------------------------------------------------------------------------------------
Run set 1                              done                             0.60      372.23           -


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 (3 / 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:                    Tue, 2024-03-19 13:25:56 UTC
tool:                    Theta 5.0.4
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-az1118-649
os:                      Linux-6.5.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3187.904 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.92        2.85        None
float-benchs/zonotope_loose.c.v+cfa-reducer.yml    Parsing OK                       8.60        4.34        None
float-benchs/float_int_inv_square.yml              false(unreach-call)             10.10        5.95        None
floats-cdfpl/square_3.yml                          TIMEOUT (false(unreach-call))      120.33      115.94        None
floats-cbmc-regression/float11.yml                 true                             6.03        3.05        None
----------------------------------------------------------------------------------------------------------------
Run set 1                                          done                            29.27      133.15           -


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:        2
    correct false:       1
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               2
  Score:                 5 (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:                    Tue, 2024-03-19 13:26:39 UTC
tool:                    Theta 5.0.4
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-az1055-417
os:                      Linux-6.5.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3243.015 MHz
ram:                     16757.3504 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.33      115.34        None
btor2c-lazyMod.cambridge.5.prop1-back-serstep.yml    TIMEOUT (Parsing OK)           120.35       98.01        None
btor2c-lazyMod.extinction.4.prop1-func-interl.yml    TIMEOUT (Parsing OK)           120.41       94.84        None
btor2c-lazyMod.lup.2.prop1-func-interl.yml           TIMEOUT (Parsing OK)           120.56       94.88        None
btor2c-lazyMod.train-gate.6.prop1-func-interl.yml    Parsing OK                      86.05       62.44        None
------------------------------------------------------------------------------------------------------------------
Run set 1                                            done                            74.24      467.64           -


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 (1 / 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:                    Tue, 2024-03-19 13:23:52 UTC
tool:                    Theta 5.0.4
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-az1148-51
os:                      Linux-6.5.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3243.344 MHz
ram:                     16757.3504 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                Parsing OK                       4.93        2.30        None
test15.yml                Parsing OK                       5.12        2.48        None
just_assert.yml           true                             5.62        2.67        None
volatile_alias.yml        Parsing OK                       3.97        2.14        None
mutex_lock_int.c_1.yml    Parsing OK                       5.10        2.36        None
---------------------------------------------------------------------------------------
Run set 1                 done                            24.72       12.46           -


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-Loops (0 / 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:                    Tue, 2024-03-19 13:25:30 UTC
tool:                    Theta 5.0.4
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-az1148-51
os:                      Linux-6.5.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3218.059 MHz
ram:                     16757.3504 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                            Parsing OK                     110.08      101.26        None
loop-crafted/simple_vardep_2.yml                   Parsing OK                     107.23      101.17        None
nla-digbench-scaling/divbin_valuebound100.yml      Parsing OK                      82.52       76.88        None
nla-digbench-scaling/mannadiv_valuebound50.yml     Parsing OK                       6.20        2.77        None
nla-digbench-scaling/mannadiv_unwindbound10.yml    Parsing OK                       6.37        2.82        None
----------------------------------------------------------------------------------------------------------------
Run set 1                                          done                           100.99      285.44           -


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-Recursive (0 / 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:                    Tue, 2024-03-19 13:23:35 UTC
tool:                    Theta 5.0.4
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-az1456-72
os:                      Linux-6.5.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3243.009 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                        TIMEOUT (Parsing OK)           120.05      100.60        None
recursive-simple/id2_i5_o5-2.yml                    TIMEOUT (Parsing OK)           120.24      100.77        None
recursified_nla-digbench/recursified_geo2-ll.yml    ERROR (frontend failed)          1.64        0.69        None
recursive/recHanoi03-2.yml                          TIMEOUT (Parsing OK)           120.32       99.82        None
recursified_nla-digbench/recursified_lcm2.yml       ERROR (frontend failed)          1.64        0.70        None
-----------------------------------------------------------------------------------------------------------------
Run set 1                                           done                             3.62      304.33           -


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-Sequentialized (0 / 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:                    Tue, 2024-03-19 13:25:04 UTC
tool:                    Theta 5.0.4
tool executable:         Theta/theta-start.sh
options:                 --disable-xcfa-serialization --disable-c-serialization --disable-arg-generation --backend PORTFOLIO --portfolio COMPLEX --loglevel INFO
resource limits:
- time:                  120 s
hardware requirements:
------------------------------------------------------------

   SYSTEM INFORMATION
host:                    fv-az1206-875
os:                      Linux-6.5.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         3208.0 MHz
ram:                     16757.3504 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 (Parsing OK)           120.38       92.65        None
seq-mthreaded/pals_opt-floodmax.3.1.ufo.UNBOUNDED.pals.yml        Parsing OK                      14.65        5.22        None
systemc/pipeline.cil-1.yml                                        TIMEOUT (Parsing OK)           120.05       99.13        None
seq-mthreaded/pals_lcr-var-start-time.3.ufo.UNBOUNDED.pals.yml    Parsing OK                      17.46        6.40        None
seq-mthreaded/pals_floodmax.3.2.ufo.BOUNDED-6.pals.yml            Parsing OK                      28.53       10.85        None
-------------------------------------------------------------------------------------------------------------------------------
Run set 1                                                         done                            58.55      215.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:               0
    correct true:        0
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:               5
  Score:                 0 (max: 6)

✅ ReachSafety-XCSP (1 / 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:                    Tue, 2024-03-19 13:23:21 UTC
tool:                    Theta 5.0.4
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-az730-722
os:                      Linux-6.5.0-1016-azure-x86_64-with-glibc2.35
cpu:                     AMD EPYC 7763 64-Core Processor
- cores:                 4
- max frequency:         2839.997 MHz
ram:                     16757.3504 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 (false(unreach-call))      120.27       92.48        None
Dubois-025.yml             Parsing OK                      26.68       11.45        None
aim-100-2-0-unsat-4.yml    Parsing OK                      36.94       19.00        None
AllInterval-014.yml        Parsing OK                     114.26      102.06        None
AllInterval-005.yml        false(unreach-call)             12.66        4.63        None
----------------------------------------------------------------------------------------
Run set 1                  done                            70.40      230.64           -


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: 7)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet