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

Clarify usage of history variables in error messages #8456

Open
wants to merge 1 commit into
base: develop
Choose a base branch
from
Open

Clarify usage of history variables in error messages #8456

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 12 additions & 0 deletions src/solvers/smt2/smt2_conv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2476,6 +2476,18 @@
out << ')';
}
}
else if(expr.id() == ID_old)

Check warning on line 2479 in src/solvers/smt2/smt2_conv.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/smt2/smt2_conv.cpp#L2479 

Added line #L2479 was not covered by tests
Copy link
Collaborator

Choose a reason for hiding this comment

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

Can't we detect this much earlier, e.g., in the C front-end during type checking? We actually already do some such checking, I think we just need to do more of it.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

We can't detect this during type checking as we can't distinguish expressions in loop invariants and in __CPROVER_assert at that stage.

CBMC warned that it would ignore __CPROVER_loop_entry in assertions during prop_conv when using SAT backend. However, when using SMT backend, CBMC would throw exception without notifying that the cause is invalid usage of loop_entry.

This PR patches the case of using SMT backend and clarify the correct usage of loop_entry when exception thrown.

{
UNEXPECTEDCASE(

Check warning on line 2481 in src/solvers/smt2/smt2_conv.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/smt2/smt2_conv.cpp#L2481 

Added line #L2481 was not covered by tests
"Invalid usage of old expressions detected. old expressions must be "
"used in function contracts.");

Check warning on line 2483 in src/solvers/smt2/smt2_conv.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/smt2/smt2_conv.cpp#L2483 

Added line #L2483 was not covered by tests
}
else if(expr.id() == ID_loop_entry)

Check warning on line 2485 in src/solvers/smt2/smt2_conv.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/smt2/smt2_conv.cpp#L2485 

Added line #L2485 was not covered by tests
{
UNEXPECTEDCASE(
"Invalid usage of loop_entry expressions detected. loop_entry "
"expressions must be used in loop invariants.");

Check warning on line 2489 in src/solvers/smt2/smt2_conv.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/smt2/smt2_conv.cpp#L2487-L2489 

Added lines #L2487 - L2489 were not covered by tests
}
else
INVARIANT_WITH_DIAGNOSTICS(
false,
Expand Down
Loading