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

Add support for float_to_int_unchecked #3660

Merged
merged 12 commits into from
Nov 6, 2024
Merged

Add support for float_to_int_unchecked #3660

Changes from 1 commit
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
88a0af4
Add support for float_to_int_unchecked
zhassan-aws Oct 30, 2024
293b748
Add one more test
zhassan-aws Oct 30, 2024
56ea3f3
Add more tests
zhassan-aws Oct 31, 2024
d49291c
Update documentation
zhassan-aws Oct 31, 2024
3aa243e
Merge branch 'main' into float-to-int-intrinsic
zhassan-aws Oct 31, 2024
08531f6
Clean-up
zhassan-aws Oct 31, 2024
f6a4d28
Clarify comment
zhassan-aws Oct 31, 2024
5dbd3bc
Include a check that u128::MAX does not need a bound
zhassan-aws Oct 31, 2024
df44869
Merge branch 'main' into float-to-int-intrinsic
zhassan-aws Nov 5, 2024
9a32883
Move code that computes in-range expression to a new module
zhassan-aws Nov 6, 2024
9dbeb98
Merge branch 'main' into float-to-int-intrinsic
zhassan-aws Nov 6, 2024
7cce2a3
Clippy fix
zhassan-aws Nov 6, 2024
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
Prev Previous commit
Next Next commit
Clarify comment
  • Loading branch information
@zhassan-aws
zhassan-aws committed Oct 31, 2024
commit f6a4d285320dca50b695ebd28f102f87e08288d4
2 changes: 1 addition & 1 deletion kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1929,7 +1929,7 @@ impl GotocCtx<'_> {

/// Checks that the floating-point value is:
/// 1. Finite (i.e. neither infinite nor NaN)
/// 2. Is in range of the target integer
/// 2. Its truncated value is in range of the target integer
/// then performs the cast to the target type
pub fn codegen_float_to_int_unchecked(
&mut self,
Expand Down
Loading