Use IcfgBuilder instead of RCFGBuilder as default#770
Open
schuessf wants to merge 7 commits into
Open
Conversation
schuessf
commented
Jan 27, 2026
| @@ -1,18 +1,15 @@ | |||
| [L3] int a = 5; | |||
| [L4] int x = 0; | |||
| VAL [a=5, x=0] | |||
Contributor
Author
There was a problem hiding this comment.
@Heizmann IcfgBuilder seems to behave slightly different than RCFGBuilder on these states in the error path. Is this expected?
| VAL [a=0, c=0, d=0, e=0, f=2] | ||
| [L23] COND FALSE !(d>0) | ||
| VAL [a=0, c=0, e=0, f=2] | ||
| [L29] COND TRUE f>0 |
Contributor
Author
There was a problem hiding this comment.
@Heizmann IcfgBuilder seems to behave slightly different than RCFGBuilder on these states in the error path. Is this expected?
This includes moving several classes from RCFGBuilder to IcfgBuilder (that were either used by IcfgBuilder or other plugins).
…ings files" This reverts commit 9c0a010.
UnstructureCode is now disabled by default.
schuessf
force-pushed
the
wip/fs/use-icfgbuilder
branch
from
2b9b84a to
df77478
Compare
schuessf
changed the title
IcfgBuilder and remove RCFGBuilderIcfgBuilder instead of RCFGBuilder as default
Contributor
Author
|
After some discussion with @Heizmann we agreed to the following:
Therefore, I just adapted the PR to reflect these changes. |
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Currently, Ultimate still offers two ways to build control-flow graphs:
RCFGBuilder: the legacy implementation, which only works for programs withoutwhile/ifand therefore requiresUnstructureCodeIcfgBuilder: the newer implementation, which supports arbitrary programs and fixed existing bugsMaintaining both implementations is undesirable because any change requires keeping multiple (partly duplicated) files in sync. For SV-COMP 2026 we already used
IcfgBuilderand observed almost identical results as withRCFGBuilder. However, this was achieved via changes in the settings and toolchains as the quickest solution. This PR applies the switch properlyand removes. Therefore, the following changes were performed:RCFGBuilderentirelyRCFGBuildertoIcfgBuilder(incl. those used for regression tests)Remove theand move required files intoRCFGBuilderpluginIcfgBuilderUnstructureCodeby default (globally, not just via settings)