Skip to content

Add abortUnless analysis#875

Merged
michael-schwarz merged 9 commits intomasterfrom
issue_873
Nov 3, 2022
Merged

Add abortUnless analysis#875
michael-schwarz merged 9 commits intomasterfrom
issue_873

Conversation

@michael-schwarz
Copy link
Copy Markdown
Member

@michael-schwarz michael-schwarz commented Oct 31, 2022 •
edited
Loading

Adds an analysis that detects if control flow only returns if the argument is non-zero, and issues a corresponding assert event.

TODO:

  • Exploit in more analyses
  • Test

Closes #873

@michael-schwarz michael-schwarz added this to the SV-COMP 2023 milestone Oct 31, 2022
@michael-schwarz
Copy link
Copy Markdown
Member Author

michael-schwarz commented Oct 31, 2022

There are no other analysis where adding it would make sense (except maybe vareq, but that doesn't even exploit branch at all currently).
Adding this analysis to the set of default analyses does not cause any regressions.

@michael-schwarz
Copy link
Copy Markdown
Member Author

michael-schwarz commented Oct 31, 2022

Unless anyone opposes, I would propose we do a joint sv-comp run of this & #869 to reduce the number of needed runs, as we currently have a lot of things we would need server time for.

@michael-schwarz michael-schwarz marked this pull request as ready for review October 31, 2022 08:14
@michael-schwarz michael-schwarz mentioned this pull request Oct 31, 2022
Closed
sim642
sim642 reviewed Oct 31, 2022
View reviewed changes
Comment thread src/analyses/apron/apronAnalysis.apron.ml Outdated
Comment thread src/analyses/base.ml Outdated
Comment thread src/analyses/abortUnless.ml Outdated
Comment thread src/analyses/abortUnless.ml
Comment thread src/analyses/abortUnless.ml
@michael-schwarz
Copy link
Copy Markdown
Member Author

michael-schwarz commented Nov 3, 2022

For sv-comp this analysis currently does not seem to pay off, so I would not include it in the config this year (unless I can come up with a more powerful analysis where we would benefit).
I would still propose to merge it, it does not add much code and might be handy.

@michael-schwarz michael-schwarz merged commit 1bfc9cd into master Nov 3, 2022
@michael-schwarz michael-schwarz deleted the issue_873 branch November 3, 2022 15:40
This was referenced May 10, 2024
Closed
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@sim642 sim642 sim642 approved these changes

Assignees

No one assigned

Labels

feature precision

Projects

None yet

Milestone

SV-COMP 2023

Development

Successfully merging this pull request may close these issues.

Support for void assume_abort_if_not(int cond) { if(!cond) {abort();} }

2 participants

@michael-schwarz @sim642