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

Improve loop bound detection for loop unrolling by handling casts in loop statements #1599

Merged
merged 2 commits into from
Oct 15, 2024

Conversation

karoliineh
Copy link
Member

Inspired by an unreach-call task num_conversion_1.c where we couldn't detect a bound for the following loop:

unsigned char c;
c = 0;
while (c < (unsigned char) 8) {
  ...
}

Unrolling the loop 8 times here helps us solve the task. In addition to the case in this program, where the loop statement is in the form CastE(TInt(int, ), Lval(Var(c, NoOffset))) < Const(Int(8,int,None)) I included all possible combinations of casting for both the left and right expressions in the loop comparison statement.

@karoliineh karoliineh added sv-comp SV-COMP (analyses, results), witnesses precision labels Oct 15, 2024
@karoliineh karoliineh added this to the SV-COMP 2025 milestone Oct 15, 2024
src/util/loopUnrolling.ml Outdated Show resolved Hide resolved
@sim642 sim642 merged commit d120e34 into master Oct 15, 2024
21 checks passed
@sim642 sim642 deleted the loopUnroll-casts-in-loopStatment branch October 15, 2024 17:47
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
precision sv-comp SV-COMP (analyses, results), witnesses
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants