ftsrg
Nontermination witnesses
Quality Gate failed
Failed conditions
15.3% Coverage on New Code (required ≥ 60%)
See analysis details on SonarQube Cloud
![sonarqubecloud[bot] avatar](https://avatars.githubusercontent.com/in/12526?v=4 "Published by a pub.dev verified publisher"){kind=small}
Quality Gate failed
Failed conditions
58.1% Coverage on New Code (required ≥ 60%)
See analysis details on SonarQube Cloud
@csanadtelbisz I had to solve quite a few merge issues after your PR was merged today. Could you take a quick look if I messed up anything? Especially related to error properties (verified/input), and the portfolio utils.
(windows builds are not working RN because the gateway GitHub actions can use for install vcredist is down.)
Quality Gate failed
Failed conditions
6.8% Duplication on New Code (required ≤ 5%)
See analysis details on SonarQube Cloud
Benchexec test report for a selection of SV-Benchmarks (correct / incorrect / all):
| Rundefinition | BOUNDED | CEGAR | HORN |
|---|---|---|---|
| SV-COMP25_no-data-race | :white_check_mark: (13 / 0 / 49) HTML/CSV | :white_check_mark: (33 / 0 / 48) HTML/CSV | :white_check_mark: (13 / 0 / 49) HTML/CSV |
| SV-COMP25_no-overflow | :question: (0 / 0 / 1003) HTML/CSV | :white_check_mark: (44 / 0 / 971) HTML/CSV | :question: (0 / 0 / 76) HTML/CSV |
| SV-COMP25_termination | :exclamation: (6 / 2 / 283) HTML/CSV | :question: (0 / 0 / 616) HTML/CSV | :white_check_mark: (5 / 0 / 283) HTML/CSV |
| SV-COMP25_unreach-call | :exclamation: (16 / 1 / 600) HTML/CSV | :exclamation: (84 / 1 / 431) HTML/CSV | :exclamation: (62 / 1 / 601) HTML/CSV |
| SV-COMP25_valid-memcleanup | :question: (0 / 0 / 65) HTML/CSV | :question: (0 / 0 / 65) HTML/CSV | :question: (0 / 0 / 65) HTML/CSV |
| SV-COMP25_valid-memsafety | :white_check_mark: (1 / 0 / 1467) HTML/CSV | :exclamation: (30 / 2 / 985) HTML/CSV | :white_check_mark: (50 / 0 / 1513) HTML/CSV |
![github-actions[bot] avatar](https://avatars.githubusercontent.com/in/15368?v=4 "Published by a pub.dev verified publisher"){kind=small}
Some wrong results (@mondokm, @AdamZsofi):
theta26-termseparate.2025-10-29_23-54-24.results.SV-COMP25_termination.html
theta26-termseparate.2025-10-29_23-54-24.logfiles.zip
ASG:
- loops/for_infinite_loop_1.yml
- loops/for_infinite_loop_2.yml
- loops/while_infinite_loop_1.yml
- loops/while_infinite_loop_2.yml
BMC:
I looked at count_up_down-2 locally, simply with --backend BOUNDED.
- On the
trace-generationbranch it just seemed to not be solved even after quite a while (I'll run it again in a sec for longer and keep an eye on it), - On this branch, yes, I could reproduce the issue - but because it is likely solved on the other branch, I did not start to look into it more. I will also check a few more wrong bounded ones on the other branch.
@mondokm fyi, might be worth to check the wrong liveness CEGAR examples on the trace-generation branch as well, as to not re-discover and re-fix something that was already fixed once.
update: Ok, so there have been more changes here, I am merging them into trace-generation and checking again, please wait :D
update 2: I merged a lot of changes into trace-generation, including this branch. Now I see the false positive there as well. Working on it. Feel free now to try the other wrong results on that branch as well.
Solution to bounded issues:
We found the cause of the bounded false positives: there was a synthetic loop added to the error location, so bmc finds the shorter error paths with a larger bound as well.
I think this rather might be a BMC implementation issue?
Anyhow, removed the loop in case of termination, and now it seems okay. Added the fix on trace-generation: https://github.com/ftsrg/theta/pull/401/commits/d279c81e3a7acfaf348b34eb4104d186f8c9bd48
Why do we have an error location at all for verifying termination? If we do not need it (and only use the prop of XCFA which we discussed at the meeting to be potentially refactored), then we could remove all edges going to the error location. Or at least the error location is properly updated by some specification transformation passes. Maybe only I am confused and the error location is kept as it is if we simply have a different (verified) property, but it seems a bit weird to me that we need a check in the XcfaToMonolithicAdapter whether we verify termination.
Perhaps, all of this is resolved if prop is refactored from XCFA to be part of XcfaProperty, and then we do not need a specific check for termination.
Yes, the example has a reach_error() call, thus we have an error location in the xcfa.
Which, in the termination case, should be regarded simply as a program exit.
So yes, maybe we could add an early xcfa pass, which makes final locations out of error locations in case of termination and I also agree that this check is a bandaid. For now, I just linked your comment to the prop issue.
What I am still not sure about is how much is this error location loop is a bandaid in the case of reachability, and if something in BMC should be changed instead.
Some wrong results (@mondokm, @AdamZsofi):
ASG:
Unfortunately these still persist, also on trace-generation.
ASG wrong true issue solution: RemoveDeadEnds works too well and removes the infinite loop (pass was implemented with reachability in mind). Will remove it from pass list in case of termination in a sec.
Additions from this PR were merged into and will be merged to master in https://github.com/ftsrg/theta/pull/401