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

Jump to bottom

Standard Library fails to build to target:lib (doo) #4964

Closed
ShubhamChaturvedi7 opened this issue Jan 9, 2024 · 1 comment · Fixed by #5329 · May be fixed by #4979
Closed

Standard Library fails to build to target:lib (doo) #4964

ShubhamChaturvedi7 opened this issue Jan 9, 2024 · 1 comment · Fixed by #5329 · May be fixed by #4979
Labels
during 2: compilation of correct program Dafny rejects a valid program during compilation kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label priority: now Will work on this now

Comments

@ShubhamChaturvedi7
Copy link
Collaborator

Dafny version

4.4

Code to produce this issue

Line 25, UTF8.dfy in Standard Library

function method {:extern "Encode"} Encode(s: string): (res: Result<ValidUTF8Bytes, string>)
   // US-ASCII only needs a single UTF-8 byte per character
   ensures IsASCIIString(s) ==> res.Success? && |res.value| == |s|
   // The following MUST be true for any correct implementation of Encode
   // If it weren't, then data would be lost.
   ensures res.Success? ==> Decode(res.value).Success? && Decode(res.value).value == s

Command to run and resulting output

Command:

build
--target:lib
--function-syntax:3
--quantifier-syntax:3

Output:

Error: Function with [{:extern}] attribute.
   |
25 |   function method {:extern "Encode"} Encode(s: string): (res: Result<ValidUTF8Bytes, string>)
   |                                      ^^^^^^

What happened?

Got the below error. Same code builds with target:go.

Error: Function with [{:extern}] attribute.
   |
25 |   function method {:extern "Encode"} Encode(s: string): (res: Result<ValidUTF8Bytes, string>)
   |                                      ^^^^^^

What type of operating system are you experiencing the problem on?

Mac
@ShubhamChaturvedi7 ShubhamChaturvedi7 added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label Jan 9, 2024
@keyboardDrummer
Copy link
Member

I'm changing the checks that are done when building a doo file, which should resolve this problem.

Step 1: track whether a doo file was built with warnings: #4971
Step 2: add additional warnings related to axioms in verification: #3553
Step 3: stop looking at the auditor results when building doo files, and add options for warning on particular constructs such as functions with {:extern}

@robin-aws robin-aws mentioned this issue Jan 12, 2024
Open
@keyboardDrummer keyboardDrummer added the during 2: compilation of correct program Dafny rejects a valid program during compilation label Apr 24, 2024
@keyboardDrummer keyboardDrummer mentioned this issue Apr 24, 2024
Merged
@keyboardDrummer keyboardDrummer added the priority: now Will work on this now label Apr 24, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
during 2: compilation of correct program Dafny rejects a valid program during compilation kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label priority: now Will work on this now
Projects
None yet
Milestone
No milestone
2 participants
@keyboardDrummer @ShubhamChaturvedi7