Skip to content

test(StandardLibrary): Update Unicode tests to work around Dafny transpile bug #672

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

Merged
lucasmcdonald3 merged 3 commits into from
Sep 5, 2024
Merged

test(StandardLibrary): Update Unicode tests to work around Dafny transpile bug #672

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
79f0063
standardlibrary
lucasmcdonald3 Sep 5, 2024
1ea1e52
Update StandardLibrary/test/TestComputeSetToOrderedSequenceCharLess.dfy
lucasmcdonald3 Sep 5, 2024
0e6cd8c
Merge branch 'main' into no-high-unicode
lucasmcdonald3 Sep 5, 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
12 changes: 10 additions & 2 deletions StandardLibrary/test/TestComputeSetToOrderedSequenceCharLess.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -88,10 +88,18 @@ module TestComputeSetToOrderedSequenceCharLess {
}

method {:test} TestSetToOrderedComplexUnicode() {
var a := {"𐐷", "&", "Љ", "ᝀ", "🂡", "｡", "𐀂"};
// Due to https://github.com/dafny-lang/dafny/issues/5737,
// Unicode characters whose UTF-16 encodings lie outside the BMP
// should not be used in Dafny source code,
// as the Dafny-Python compiler does not correctly convert these characters
// into UTF-16 when translating the Dafny source code to Python.
// var a := {"𐐷", "&", "Љ", "ᝀ", "🂡", "｡", "𐀂"};
Comment thread
lucasmcdonald3 marked this conversation as resolved.
// TODO: After #5737 is fixed, use the commented-out expression.
var a := {"\ud801\udc37", "&", "Љ", "ᝀ", "\ud83c\udca1", "｡", "\ud800\udc02"};
var output := ComputeSetToOrderedSequence(a, CharLess);
var output2 := ComputeSetToOrderedSequence2(a, CharLess);
var expected := ["&", "Љ", "ᝀ", "𐀂", "𐐷", "🂡", "｡"];
// var expected := ["&", "Љ", "ᝀ", "𐀂", "𐐷", "🂡", "｡"];
var expected := ["&", "Љ", "ᝀ", "\ud800\udc02", "\ud801\udc37", "\ud83c\udca1", "｡"];
// This is the pure logographic order,
// however this function is used in the DB-ESDK
// to canonicalize sets, and needs to remain the same.
Expand Down