Skip to content

Commit

Permalink
HOTFIX define Int2Bytes for -1 again
Browse files Browse the repository at this point in the history
Fixing an oversight in the previous change.
The value of `I` in the formula for negative `I` is actually
_bitwise-negated_ instead of just taking its negative. Therefore,
we would be calling log2Int(0) for `I ==Int -1`.
  • Loading branch information
jberthold committed Jul 26, 2024
1 parent 1e8c9b6 commit 21fe3cc
Showing 1 changed file with 3 additions and 1 deletion.
4 changes: 3 additions & 1 deletion k-distribution/include/kframework/builtin/domains.md
Original file line number Diff line number Diff line change
Expand Up @@ -2217,7 +2217,9 @@ module BYTES
rule Int2Bytes(I::Int, E::Endianness, Signed ) => Int2Bytes((log2Int(I) +Int 9) /Int 8, I, E)
requires I >Int 0 [preserves-definedness]
rule Int2Bytes(I::Int, E::Endianness, Signed ) => Int2Bytes((log2Int(~Int I) +Int 9) /Int 8, I, E)
requires I <Int 0 [preserves-definedness]
requires I <Int -1 [preserves-definedness]
rule Int2Bytes(I::Int, E::Endianness, Signed ) => Int2Bytes(1, -1, E)
requires I ==Int -1 [preserves-definedness]
endmodule
```

Expand Down

0 comments on commit 21fe3cc

Please sign in to comment.