Skip to content

Conversation

jaisnan
Copy link
Contributor

@jaisnan jaisnan commented Jun 28, 2024

Adds support for f16 and f128, i.e

  1. adding translation to irep .
  2. generating arbitrary values for the new types
  3. generating basic invariants (checking if safe) for new types
  4. Adds sanity testing for arbitrary on the new types.

Resolves #3303

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

@jaisnan jaisnan requested a review from a team as a code owner June 28, 2024 16:22
@github-actions github-actions bot added the Z-EndToEndBenchCI Tag a PR to run benchmark CI label Jun 28, 2024
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. Should the title say "upgrade to 6/28" instead of 6/26?

@jaisnan jaisnan changed the title Add support for f16 and f128 for toolchain upgrade to 6/26 Add support for f16 and f128 for toolchain upgrade to 6/28 Jun 28, 2024
@jaisnan jaisnan requested a review from zhassan-aws June 28, 2024 18:09
Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

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

Can you please add some tests?

@zhassan-aws
Copy link
Contributor

Can you please add some tests?

I was going to mention this in my overall comment, but completely forgot 🙈

Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

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

Can you at least extend this test to include the new floating points?

https://github.com/model-checking/kani/blob/main/tests/kani/FloatingPoint/main.rs

@jaisnan jaisnan requested a review from celinval June 28, 2024 22:06
@tautschnig tautschnig dismissed celinval’s stale review July 1, 2024 18:28

Review is stale as tests have been added.

@adpaco-aws adpaco-aws enabled auto-merge (squash) July 1, 2024 19:09
@adpaco-aws adpaco-aws merged commit d55f25b into model-checking:main Jul 1, 2024
@jaisnan jaisnan deleted the toolchain-upgrade-3303 branch July 1, 2024 19:21
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.

Toolchain upgrade to nightly-2024-06-28 failed
5 participants