Skip to content

Fix relation analysis ignoring extern inits#1444

Merged
sim642 merged 2 commits intomasterfrom
relation-extern
May 7, 2024
Merged

Fix relation analysis ignoring extern inits#1444
sim642 merged 2 commits intomasterfrom
relation-extern

Conversation

@sim642
Copy link
Copy Markdown
Member

@sim642 sim642 commented May 6, 2024

Fixes two instances from #1440.

For some reason the relation analysis simply ignored extern initializers, which meant that those variables evaluated to bottom in conditionals.

@sim642 sim642 added bug unsound sv-comp SV-COMP (analyses, results), witnesses relational Relational analyses (Apron, affeq, lin2var) labels May 6, 2024
@sim642 sim642 added this to the SV-COMP 2025 milestone May 6, 2024
@michael-schwarz michael-schwarz self-requested a review May 6, 2024 08:19
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

bug relational Relational analyses (Apron, affeq, lin2var) sv-comp SV-COMP (analyses, results), witnesses unsound

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants