-
Notifications
You must be signed in to change notification settings - Fork 43
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Deploying to gh-pages from @ 8c971b8 🚀
- Loading branch information
0 parents
commit 478cce0
Showing
2,774 changed files
with
799,184 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1 @@ | ||
| theta.mit.bme.hu |
8 changes: 8 additions & 0 deletions
8
...Safety-Main/theta.2023-11-12_17-50-43.logfiles/SV-COMP24_unreach-call.fib_safe-11.yml.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,8 @@ | ||
| theta/theta-start.sh sv-benchmarks/c/pthread/fib_safe-11.i --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/unreach-call.prp | ||
|
|
||
|
|
||
| -------------------------------------------------------------------------------- | ||
|
|
||
|
|
||
| LD_LIBRARY_PATH=/home/runner/work/theta/theta/theta/lib /usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss120m -Xmx14210m -jar /home/runner/work/theta/theta/theta/theta.jar --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/unreach-call.prp --input sv-benchmarks/c/pthread/fib_safe-11.i --smt-home /home/runner/work/theta/theta/theta/solvers | ||
| Arithmetic: integer |
8 changes: 8 additions & 0 deletions
8
...rencySafety-Main/theta.2023-11-12_17-50-43.logfiles/SV-COMP24_unreach-call.lazy01.yml.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,8 @@ | ||
| theta/theta-start.sh sv-benchmarks/c/pthread/lazy01.i --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/unreach-call.prp | ||
|
|
||
|
|
||
| -------------------------------------------------------------------------------- | ||
|
|
||
|
|
||
| LD_LIBRARY_PATH=/home/runner/work/theta/theta/theta/lib /usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss120m -Xmx14210m -jar /home/runner/work/theta/theta/theta/theta.jar --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/unreach-call.prp --input sv-benchmarks/c/pthread/lazy01.i --smt-home /home/runner/work/theta/theta/theta/solvers | ||
| Arithmetic: integer |
8 changes: 8 additions & 0 deletions
8
...Safety-Main/theta.2023-11-12_17-50-43.logfiles/SV-COMP24_unreach-call.mix000.oepc.yml.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,8 @@ | ||
| theta/theta-start.sh sv-benchmarks/c/pthread-wmm/mix000.oepc.i --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/unreach-call.prp | ||
|
|
||
|
|
||
| -------------------------------------------------------------------------------- | ||
|
|
||
|
|
||
| LD_LIBRARY_PATH=/home/runner/work/theta/theta/theta/lib /usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss120m -Xmx14210m -jar /home/runner/work/theta/theta/theta/theta.jar --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/unreach-call.prp --input sv-benchmarks/c/pthread-wmm/mix000.oepc.i --smt-home /home/runner/work/theta/theta/theta/solvers | ||
| Arithmetic: integer |
8 changes: 8 additions & 0 deletions
8
...-Main/theta.2023-11-12_17-50-43.logfiles/SV-COMP24_unreach-call.read_write_lock-1.yml.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,8 @@ | ||
| theta/theta-start.sh sv-benchmarks/c/pthread-atomic/read_write_lock-1.i --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/unreach-call.prp | ||
|
|
||
|
|
||
| -------------------------------------------------------------------------------- | ||
|
|
||
|
|
||
| LD_LIBRARY_PATH=/home/runner/work/theta/theta/theta/lib /usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss120m -Xmx14210m -jar /home/runner/work/theta/theta/theta/theta.jar --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/unreach-call.prp --input sv-benchmarks/c/pthread-atomic/read_write_lock-1.i --smt-home /home/runner/work/theta/theta/theta/solvers | ||
| Arithmetic: integer |
8 changes: 8 additions & 0 deletions
8
...ySafety-Main/theta.2023-11-12_17-50-43.logfiles/SV-COMP24_unreach-call.rfi003_tso.yml.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,8 @@ | ||
| theta/theta-start.sh sv-benchmarks/c/pthread-wmm/rfi003_tso.i --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/unreach-call.prp | ||
|
|
||
|
|
||
| -------------------------------------------------------------------------------- | ||
|
|
||
|
|
||
| LD_LIBRARY_PATH=/home/runner/work/theta/theta/theta/lib /usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss120m -Xmx14210m -jar /home/runner/work/theta/theta/theta/theta.jar --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/unreach-call.prp --input sv-benchmarks/c/pthread-wmm/rfi003_tso.i --smt-home /home/runner/work/theta/theta/theta/solvers | ||
| Arithmetic: integer |
8 changes: 8 additions & 0 deletions
8
...-Main/theta.2023-11-12_17-50-43.logfiles/SV-COMP24_unreach-call.safe018_power.opt.yml.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,8 @@ | ||
| theta/theta-start.sh sv-benchmarks/c/pthread-wmm/safe018_power.opt.i --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/unreach-call.prp | ||
|
|
||
|
|
||
| -------------------------------------------------------------------------------- | ||
|
|
||
|
|
||
| LD_LIBRARY_PATH=/home/runner/work/theta/theta/theta/lib /usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss120m -Xmx14210m -jar /home/runner/work/theta/theta/theta/theta.jar --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/unreach-call.prp --input sv-benchmarks/c/pthread-wmm/safe018_power.opt.i --smt-home /home/runner/work/theta/theta/theta/solvers | ||
| Arithmetic: integer |
8 changes: 8 additions & 0 deletions
8
...Safety-Main/theta.2023-11-12_17-50-43.logfiles/SV-COMP24_unreach-call.safe024_tso.yml.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,8 @@ | ||
| theta/theta-start.sh sv-benchmarks/c/pthread-wmm/safe024_tso.i --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/unreach-call.prp | ||
|
|
||
|
|
||
| -------------------------------------------------------------------------------- | ||
|
|
||
|
|
||
| LD_LIBRARY_PATH=/home/runner/work/theta/theta/theta/lib /usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss120m -Xmx14210m -jar /home/runner/work/theta/theta/theta/theta.jar --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/unreach-call.prp --input sv-benchmarks/c/pthread-wmm/safe024_tso.i --smt-home /home/runner/work/theta/theta/theta/solvers | ||
| Arithmetic: integer |
8 changes: 8 additions & 0 deletions
8
...Safety-Main/theta.2023-11-12_17-50-43.logfiles/SV-COMP24_unreach-call.safe026_tso.yml.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,8 @@ | ||
| theta/theta-start.sh sv-benchmarks/c/pthread-wmm/safe026_tso.i --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/unreach-call.prp | ||
|
|
||
|
|
||
| -------------------------------------------------------------------------------- | ||
|
|
||
|
|
||
| LD_LIBRARY_PATH=/home/runner/work/theta/theta/theta/lib /usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss120m -Xmx14210m -jar /home/runner/work/theta/theta/theta/theta.jar --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/unreach-call.prp --input sv-benchmarks/c/pthread-wmm/safe026_tso.i --smt-home /home/runner/work/theta/theta/theta/solvers | ||
| Arithmetic: integer |
8 changes: 8 additions & 0 deletions
8
...Safety-Main/theta.2023-11-12_17-50-43.logfiles/SV-COMP24_unreach-call.safe030_tso.yml.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,8 @@ | ||
| theta/theta-start.sh sv-benchmarks/c/pthread-wmm/safe030_tso.i --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/unreach-call.prp | ||
|
|
||
|
|
||
| -------------------------------------------------------------------------------- | ||
|
|
||
|
|
||
| LD_LIBRARY_PATH=/home/runner/work/theta/theta/theta/lib /usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss120m -Xmx14210m -jar /home/runner/work/theta/theta/theta/theta.jar --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/unreach-call.prp --input sv-benchmarks/c/pthread-wmm/safe030_tso.i --smt-home /home/runner/work/theta/theta/theta/solvers | ||
| Arithmetic: integer |
8 changes: 8 additions & 0 deletions
8
...Safety-Main/theta.2023-11-12_17-50-43.logfiles/SV-COMP24_unreach-call.safe032_tso.yml.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,8 @@ | ||
| theta/theta-start.sh sv-benchmarks/c/pthread-wmm/safe032_tso.i --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/unreach-call.prp | ||
|
|
||
|
|
||
| -------------------------------------------------------------------------------- | ||
|
|
||
|
|
||
| LD_LIBRARY_PATH=/home/runner/work/theta/theta/theta/lib /usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss120m -Xmx14210m -jar /home/runner/work/theta/theta/theta/theta.jar --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/unreach-call.prp --input sv-benchmarks/c/pthread-wmm/safe032_tso.i --smt-home /home/runner/work/theta/theta/theta/solvers | ||
| Arithmetic: integer |
13 changes: 13 additions & 0 deletions
13
...-Main/theta.2023-11-12_17-50-43.results.SV-COMP24_unreach-call.ConcurrencySafety-Main.csv
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,13 @@ | ||
| tool Theta 5.0.0 Theta 5.0.0 Theta 5.0.0 Theta 5.0.0 | ||
| run set SV-COMP24_unreach-call.ConcurrencySafety-Main SV-COMP24_unreach-call.ConcurrencySafety-Main SV-COMP24_unreach-call.ConcurrencySafety-Main SV-COMP24_unreach-call.ConcurrencySafety-Main | ||
| ../sv-benchmarks/c/ status cputime (s) walltime (s) memory (MB) | ||
| pthread-atomic/read_write_lock-1.yml true ERROR (server error) 3.943731 1.4177350630000092 250.474496 | ||
| pthread-wmm/rfi003_tso.yml true ERROR (server error) 4.506863 1.6077008799999817 256.634880 | ||
| pthread/lazy01.yml false ERROR (server error) 3.836386 1.4339034249999827 266.461184 | ||
| pthread-wmm/mix000.oepc.yml false ERROR (server error) 4.365972 1.565908798999999 262.889472 | ||
| pthread-wmm/safe032_tso.yml true ERROR (server error) 3.362911 1.2581821470000136 238.686208 | ||
| pthread-wmm/safe030_tso.yml true ERROR (server error) 4.193322 1.5252179600000204 253.833216 | ||
| pthread-wmm/safe018_power.opt.yml false ERROR (server error) 4.384561 1.5719564300000002 248.582144 | ||
| pthread-wmm/safe026_tso.yml true ERROR (server error) 3.910786 1.4363257679999606 255.365120 | ||
| pthread/fib_safe-11.yml true ERROR (server error) 4.015042 1.4429220310000233 254.738432 | ||
| pthread-wmm/safe024_tso.yml true ERROR (server error) 4.33857 1.5934931150000011 251.219968 |
62 changes: 62 additions & 0 deletions
62
...Main/theta.2023-11-12_17-50-43.results.SV-COMP24_unreach-call.ConcurrencySafety-Main.html
Large diffs are not rendered by default.
Oops, something went wrong.
Binary file added
BIN
+5.83 KB
...n/theta.2023-11-12_17-50-43.results.SV-COMP24_unreach-call.ConcurrencySafety-Main.xml.bz2
Binary file not shown.
64 changes: 64 additions & 0 deletions
64
...chexec-test/BenchexecResults-ConcurrencySafety-Main/theta.2023-11-12_17-50-43.results.txt
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,64 @@ | ||
| 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: Sun, 2023-11-12 17:50:43 UTC | ||
| tool: Theta 5.0.0 | ||
| tool executable: theta/theta-start.sh | ||
| options: --witness-only --portfolio COMPLEX --loglevel RESULT | ||
| resource limits: | ||
| - time: 120 s | ||
| hardware requirements: | ||
| - cpu model: Intel Xeon E3-1230 v5 @ 3.40 GHz | ||
| ------------------------------------------------------------ | ||
|
|
||
| SYSTEM INFORMATION | ||
| host: fv-az1456-892 | ||
| os: Linux-6.2.0-1015-azure-x86_64-with-glibc2.35 | ||
| cpu: AMD EPYC 7763 64-Core Processor | ||
| - cores: 4 | ||
| - max frequency: 3242.787 MHz | ||
| ram: 16757.796864 MB | ||
| ------------------------------------------------------------ | ||
|
|
||
|
|
||
|
|
||
| SV-COMP24_unreach-call.ConcurrencySafety-Main | ||
| Run set 1 of 4 with options '--witness-only --portfolio COMPLEX --loglevel RESULT' and propertyfile 'None' | ||
|
|
||
| inputfile status cpu time wall time host | ||
| ----------------------------------------------------------------------------------------------------- | ||
| pthread-atomic/read_write_lock-1.yml ERROR (server error) 3.94 1.42 None | ||
| pthread-wmm/rfi003_tso.yml ERROR (server error) 4.51 1.61 None | ||
| pthread/lazy01.yml ERROR (server error) 3.84 1.43 None | ||
| pthread-wmm/mix000.oepc.yml ERROR (server error) 4.37 1.57 None | ||
| pthread-wmm/safe032_tso.yml ERROR (server error) 3.36 1.26 None | ||
| pthread-wmm/safe030_tso.yml ERROR (server error) 4.19 1.53 None | ||
| pthread-wmm/safe018_power.opt.yml ERROR (server error) 4.38 1.57 None | ||
| pthread-wmm/safe026_tso.yml ERROR (server error) 3.91 1.44 None | ||
| pthread/fib_safe-11.yml ERROR (server error) 4.02 1.44 None | ||
| pthread-wmm/safe024_tso.yml ERROR (server error) 4.34 1.59 None | ||
| ----------------------------------------------------------------------------------------------------- | ||
| Run set 1 done 40.86 15.90 - | ||
|
|
||
|
|
||
| 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: 10 Files | ||
| correct: 0 | ||
| correct true: 0 | ||
| correct false: 0 | ||
| incorrect: 0 | ||
| incorrect true: 0 | ||
| incorrect false: 0 | ||
| unknown: 10 | ||
| Score: 0 (max: 17) |
8 changes: 8 additions & 0 deletions
8
...emSafety/theta.2023-11-12_17-50-36.logfiles/SV-COMP24_valid-memsafety.fib_safe-11.yml.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,8 @@ | ||
| theta/theta-start.sh sv-benchmarks/c/pthread/fib_safe-11.i --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/valid-memsafety.prp | ||
|
|
||
|
|
||
| -------------------------------------------------------------------------------- | ||
|
|
||
|
|
||
| LD_LIBRARY_PATH=/home/runner/work/theta/theta/theta/lib /usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss120m -Xmx14210m -jar /home/runner/work/theta/theta/theta/theta.jar --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/valid-memsafety.prp --input sv-benchmarks/c/pthread/fib_safe-11.i --smt-home /home/runner/work/theta/theta/theta/solvers | ||
| Arithmetic: integer |
8 changes: 8 additions & 0 deletions
8
...ety-MemSafety/theta.2023-11-12_17-50-36.logfiles/SV-COMP24_valid-memsafety.lazy01.yml.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,8 @@ | ||
| theta/theta-start.sh sv-benchmarks/c/pthread/lazy01.i --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/valid-memsafety.prp | ||
|
|
||
|
|
||
| -------------------------------------------------------------------------------- | ||
|
|
||
|
|
||
| LD_LIBRARY_PATH=/home/runner/work/theta/theta/theta/lib /usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss120m -Xmx14210m -jar /home/runner/work/theta/theta/theta/theta.jar --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/valid-memsafety.prp --input sv-benchmarks/c/pthread/lazy01.i --smt-home /home/runner/work/theta/theta/theta/solvers | ||
| Arithmetic: integer |
8 changes: 8 additions & 0 deletions
8
...emSafety/theta.2023-11-12_17-50-36.logfiles/SV-COMP24_valid-memsafety.mix000.oepc.yml.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,8 @@ | ||
| theta/theta-start.sh sv-benchmarks/c/pthread-wmm/mix000.oepc.i --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/valid-memsafety.prp | ||
|
|
||
|
|
||
| -------------------------------------------------------------------------------- | ||
|
|
||
|
|
||
| LD_LIBRARY_PATH=/home/runner/work/theta/theta/theta/lib /usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss120m -Xmx14210m -jar /home/runner/work/theta/theta/theta/theta.jar --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/valid-memsafety.prp --input sv-benchmarks/c/pthread-wmm/mix000.oepc.i --smt-home /home/runner/work/theta/theta/theta/solvers | ||
| Arithmetic: integer |
8 changes: 8 additions & 0 deletions
8
...ty/theta.2023-11-12_17-50-36.logfiles/SV-COMP24_valid-memsafety.read_write_lock-1.yml.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,8 @@ | ||
| theta/theta-start.sh sv-benchmarks/c/pthread-atomic/read_write_lock-1.i --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/valid-memsafety.prp | ||
|
|
||
|
|
||
| -------------------------------------------------------------------------------- | ||
|
|
||
|
|
||
| LD_LIBRARY_PATH=/home/runner/work/theta/theta/theta/lib /usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss120m -Xmx14210m -jar /home/runner/work/theta/theta/theta/theta.jar --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/valid-memsafety.prp --input sv-benchmarks/c/pthread-atomic/read_write_lock-1.i --smt-home /home/runner/work/theta/theta/theta/solvers | ||
| Arithmetic: integer |
8 changes: 8 additions & 0 deletions
8
...MemSafety/theta.2023-11-12_17-50-36.logfiles/SV-COMP24_valid-memsafety.rfi003_tso.yml.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,8 @@ | ||
| theta/theta-start.sh sv-benchmarks/c/pthread-wmm/rfi003_tso.i --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/valid-memsafety.prp | ||
|
|
||
|
|
||
| -------------------------------------------------------------------------------- | ||
|
|
||
|
|
||
| LD_LIBRARY_PATH=/home/runner/work/theta/theta/theta/lib /usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss120m -Xmx14210m -jar /home/runner/work/theta/theta/theta/theta.jar --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/valid-memsafety.prp --input sv-benchmarks/c/pthread-wmm/rfi003_tso.i --smt-home /home/runner/work/theta/theta/theta/solvers | ||
| Arithmetic: integer |
8 changes: 8 additions & 0 deletions
8
...ty/theta.2023-11-12_17-50-36.logfiles/SV-COMP24_valid-memsafety.safe018_power.opt.yml.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,8 @@ | ||
| theta/theta-start.sh sv-benchmarks/c/pthread-wmm/safe018_power.opt.i --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/valid-memsafety.prp | ||
|
|
||
|
|
||
| -------------------------------------------------------------------------------- | ||
|
|
||
|
|
||
| LD_LIBRARY_PATH=/home/runner/work/theta/theta/theta/lib /usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss120m -Xmx14210m -jar /home/runner/work/theta/theta/theta/theta.jar --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/valid-memsafety.prp --input sv-benchmarks/c/pthread-wmm/safe018_power.opt.i --smt-home /home/runner/work/theta/theta/theta/solvers | ||
| Arithmetic: integer |
8 changes: 8 additions & 0 deletions
8
...emSafety/theta.2023-11-12_17-50-36.logfiles/SV-COMP24_valid-memsafety.safe024_tso.yml.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,8 @@ | ||
| theta/theta-start.sh sv-benchmarks/c/pthread-wmm/safe024_tso.i --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/valid-memsafety.prp | ||
|
|
||
|
|
||
| -------------------------------------------------------------------------------- | ||
|
|
||
|
|
||
| LD_LIBRARY_PATH=/home/runner/work/theta/theta/theta/lib /usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss120m -Xmx14210m -jar /home/runner/work/theta/theta/theta/theta.jar --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/valid-memsafety.prp --input sv-benchmarks/c/pthread-wmm/safe024_tso.i --smt-home /home/runner/work/theta/theta/theta/solvers | ||
| Arithmetic: integer |
8 changes: 8 additions & 0 deletions
8
...emSafety/theta.2023-11-12_17-50-36.logfiles/SV-COMP24_valid-memsafety.safe026_tso.yml.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,8 @@ | ||
| theta/theta-start.sh sv-benchmarks/c/pthread-wmm/safe026_tso.i --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/valid-memsafety.prp | ||
|
|
||
|
|
||
| -------------------------------------------------------------------------------- | ||
|
|
||
|
|
||
| LD_LIBRARY_PATH=/home/runner/work/theta/theta/theta/lib /usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss120m -Xmx14210m -jar /home/runner/work/theta/theta/theta/theta.jar --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/valid-memsafety.prp --input sv-benchmarks/c/pthread-wmm/safe026_tso.i --smt-home /home/runner/work/theta/theta/theta/solvers | ||
| Arithmetic: integer |
8 changes: 8 additions & 0 deletions
8
...emSafety/theta.2023-11-12_17-50-36.logfiles/SV-COMP24_valid-memsafety.safe030_tso.yml.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,8 @@ | ||
| theta/theta-start.sh sv-benchmarks/c/pthread-wmm/safe030_tso.i --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/valid-memsafety.prp | ||
|
|
||
|
|
||
| -------------------------------------------------------------------------------- | ||
|
|
||
|
|
||
| LD_LIBRARY_PATH=/home/runner/work/theta/theta/theta/lib /usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss120m -Xmx14210m -jar /home/runner/work/theta/theta/theta/theta.jar --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/valid-memsafety.prp --input sv-benchmarks/c/pthread-wmm/safe030_tso.i --smt-home /home/runner/work/theta/theta/theta/solvers | ||
| Arithmetic: integer |
8 changes: 8 additions & 0 deletions
8
...emSafety/theta.2023-11-12_17-50-36.logfiles/SV-COMP24_valid-memsafety.safe032_tso.yml.log
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,8 @@ | ||
| theta/theta-start.sh sv-benchmarks/c/pthread-wmm/safe032_tso.i --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/valid-memsafety.prp | ||
|
|
||
|
|
||
| -------------------------------------------------------------------------------- | ||
|
|
||
|
|
||
| LD_LIBRARY_PATH=/home/runner/work/theta/theta/theta/lib /usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss120m -Xmx14210m -jar /home/runner/work/theta/theta/theta/theta.jar --witness-only --portfolio COMPLEX --loglevel RESULT --property sv-benchmarks/c/properties/valid-memsafety.prp --input sv-benchmarks/c/pthread-wmm/safe032_tso.i --smt-home /home/runner/work/theta/theta/theta/solvers | ||
| Arithmetic: integer |
13 changes: 13 additions & 0 deletions
13
...eta.2023-11-12_17-50-36.results.SV-COMP24_valid-memsafety.ConcurrencySafety-MemSafety.csv
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,13 @@ | ||
| tool Theta 5.0.0 Theta 5.0.0 Theta 5.0.0 Theta 5.0.0 | ||
| run set SV-COMP24_valid-memsafety.ConcurrencySafety-MemSafety SV-COMP24_valid-memsafety.ConcurrencySafety-MemSafety SV-COMP24_valid-memsafety.ConcurrencySafety-MemSafety SV-COMP24_valid-memsafety.ConcurrencySafety-MemSafety | ||
| ../sv-benchmarks/c/ status cputime (s) walltime (s) memory (MB) | ||
| pthread-atomic/read_write_lock-1.yml ERROR (server error) 4.10696 1.525479240999971 246.988800 | ||
| pthread-wmm/rfi003_tso.yml ERROR (server error) 3.779929 1.3621680640000022 247.427072 | ||
| pthread/lazy01.yml ERROR (server error) 3.891631 1.4485685869999543 263.618560 | ||
| pthread-wmm/mix000.oepc.yml ERROR (server error) 4.398683 1.5823550669999804 265.146368 | ||
| pthread-wmm/safe032_tso.yml ERROR (server error) 3.328471 1.2315741400000206 246.603776 | ||
| pthread-wmm/safe030_tso.yml ERROR (server error) 4.128106 1.5115364649999492 240.832512 | ||
| pthread-wmm/safe018_power.opt.yml ERROR (server error) 4.463395 1.6066658449999522 256.577536 | ||
| pthread-wmm/safe026_tso.yml ERROR (server error) 4.057112 1.4982898959999602 254.660608 | ||
| pthread/fib_safe-11.yml ERROR (server error) 4.136054 1.517930008999997 269.627392 | ||
| pthread-wmm/safe024_tso.yml ERROR (server error) 4.189061 1.5356821719999516 264.880128 |
Oops, something went wrong.