From 1721f7d23bfdab0127d70ddddb6292bf8ee64f6b Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Tue, 16 Jul 2024 16:02:23 +1000 Subject: [PATCH] mark Int2Bytes(Int,Endianness,Signedness) rules as preserving definedness (#4522) Without the annotation, `booster` won't use these rules. The `/Int` division is partial but harmless in these rules. --- k-distribution/include/kframework/builtin/domains.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index 717639a083a..9dd803c9de9 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -2211,12 +2211,12 @@ module BYTES imports private INT rule Int2Bytes(I::Int, E::Endianness, Unsigned) => Int2Bytes((log2Int(I) +Int 8) /Int 8, I, E) - requires I >Int 0 + requires I >Int 0 [preserves-definedness] rule Int2Bytes(0, _::Endianness, _) => .Bytes rule Int2Bytes(I::Int, E::Endianness, Signed) => Int2Bytes((log2Int(I) +Int 9) /Int 8, I, E) - requires I >Int 0 + 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 Int2Bytes(1, -1, E) endmodule ```