Skip to content

Conversation

@celinval
Copy link
Contributor

@celinval celinval commented Sep 14, 2023

Description of changes:

This is to avoid missing out-of-bounds access errors when dereferencing the vector with an index that is greater or equal to length.

Resolved issues:

Resolves #2759

Related RFC:

Call-outs:

I added some extra tests for exact_vec too since it is a public API.

Testing:

  • How is this change tested? New tests

  • Is this a refactor change?

Checklist

  • Each commit message has a non-empty body, explaining why the change was made
  • Methods or procedures are documented
  • Regression or unit tests are included, or existing tests cover the modified code
  • My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

This is to avoid missing out-of-bounds access errors when dereferencing
the vector with an index that is greater or equal to length.
@celinval celinval requested a review from a team as a code owner September 14, 2023 21:39
Copy link
Contributor

@zhassan-aws zhassan-aws left a comment

Choose a reason for hiding this comment

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

Thanks!

@celinval celinval enabled auto-merge (squash) September 14, 2023 23:24
@celinval celinval disabled auto-merge September 14, 2023 23:24
@celinval celinval added the Z-EndToEndBenchCI Tag a PR to run benchmark CI label Sep 14, 2023
@tautschnig tautschnig merged commit eb62ad8 into model-checking:main Sep 15, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Z-EndToEndBenchCI Tag a PR to run benchmark CI

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Kani does not flag out-of-bounds dereference with kani::vec::any_vec

3 participants