Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Instrumentation for interval loop invariants #1603

Merged
merged 2 commits into from Jan 26, 2024

Conversation

rafaelsamenezes
Copy link
Contributor

@rafaelsamenezes rafaelsamenezes commented Jan 19, 2024

This PR adds:

  1. Multiple instrumentation modes for the interval analysis
  2. A new instrumentation mode which will add only restrictions for loop variables.

This is mostly so I can start running more experiments. I will avoid adding explicit flags for now

Copy link
Contributor

@lucasccordeiro lucasccordeiro left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@rafaelsamenezes: could you please run this PR over the SV-COMP benchmarks?

@rafaelsamenezes
Copy link
Contributor Author

Master

Statistics:          23805 Files
  correct:           15091
    correct true:     8534
    correct false:    6557
  incorrect:            45
    incorrect true:     17
    incorrect false:    28
  unknown:            8669
  Score:             22633 (max: 38482)

This PR:

Statistics:          23805 Files
  correct:           15105
    correct true:     8545
    correct false:    6560
  incorrect:            45
    incorrect true:     17
    incorrect false:    28
  unknown:            8655
  Score:             22658 (max: 38482)

@rafaelsamenezes rafaelsamenezes marked this pull request as ready for review January 26, 2024 09:49
Copy link
Contributor

@lucasccordeiro lucasccordeiro left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM.

@rafaelsamenezes
Copy link
Contributor Author

I will merge this for now. @fbrausse let me know if you have any comments.

@rafaelsamenezes rafaelsamenezes merged commit f8d55da into master Jan 26, 2024
14 checks passed
@rafaelsamenezes rafaelsamenezes deleted the interval-loop-instrumentation branch January 26, 2024 12:20
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants