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.

Sign up for GitHub

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

Jump to bottom

Added sscanf OM #1519

Merged
merged 5 commits into from Nov 28, 2023
Merged

Added sscanf OM #1519

merged 5 commits into from Nov 28, 2023

Conversation

rafaelsamenezes
Copy link
Contributor

No description provided.

fbrausse
fbrausse approved these changes Nov 22, 2023
View reviewed changes
Copy link
Member

@fbrausse fbrausse left a comment

Choose a reason for hiding this comment

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

Nice, fixes all 3 sv-comp tasks reorder_[25]-2 and twostage_3-2!

@fbrausse fbrausse mentioned this pull request Nov 22, 2023
Closed
47 tasks
lucasccordeiro
lucasccordeiro approved these changes Nov 22, 2023
View reviewed changes
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.

Thanks for submitting this PR, @rafaelsamenezes.

@lucasccordeiro
Copy link
Contributor

@rafaelsamenezes: could you please fix the CI?

@fbrausse
Copy link
Member

The CI doesn't really say much, just

2023-11-23T08:49:03.6656622Z ##[error]The runner has received a shutdown signal. This can happen when the runner service is stopped, or a manually started runner is canceled.
2023-11-23T08:49:03.6661614Z ##[error]Process completed with exit code 143.

My guess would be memory usage, possibly due to variables initialized with sscanf now having unbounded values in some regression tests.

@rafaelsamenezes
Copy link
Contributor Author

@fbrausse yeah, most of then is because some loops are "symbolically bounded" now. I am running locally and setting a timeout on ctest to identify the ones that are affected. Most of time is just a matter of adding a strategy.

rafaelsamenezes and others added 5 commits November 28, 2023 11:28
@rafaelsamenezes @lucasccordeiro
[sscanf] added sscanf OM
b8003e5
@rafaelsamenezes @lucasccordeiro
[sscanf] added strategy to previous sscanf test
9436400
@rafaelsamenezes @lucasccordeiro
[sscanf] more test fixes
609fe88
@rafaelsamenezes @lucasccordeiro
[sscanf] fixed test-cases
27af2f8 
Mainly three fixes:

1. Added a strategy when needed i.e. --incremental-bmc.
2. Added --force-malloc-success when needed. There are tests that fail
with it although it is not the test goal.
3. Added an include to assert.h when needed.
@rafaelsamenezes @lucasccordeiro
clang-format
43440c5
@lucasccordeiro
Copy link
Contributor

@rafaelsamenezes: Thanks for submitting this PR.

@lucasccordeiro lucasccordeiro merged commit 1b596ec into master Nov 28, 2023
9 checks passed
@lucasccordeiro lucasccordeiro deleted the sscanf branch November 28, 2023 11:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@fbrausse fbrausse fbrausse approved these changes

@lucasccordeiro lucasccordeiro lucasccordeiro approved these changes

Assignees
No one assigned
Labels
SV-COMP
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@rafaelsamenezes @lucasccordeiro @fbrausse