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.

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

Java sequence prefix < fail compilation when combined with if ... then ... else #3952

Open
Dilan-s opened this issue May 5, 2023 · 0 comments
Labels
during 2: compilation of correct program Dafny rejects a valid program during compilation invalid translated code The compiler generates invalid code, making the the target language infrastructure crash kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: java Dafny's Java transpiler and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag priority: next Will consider working on this after in progress work is done

Comments

@Dilan-s
Copy link

Dilan-s commented May 5, 2023

Dafny version

4.1.0

Code to produce this issue

method Main() returns ()
{
    var v_seq_9: seq<int> := [];
    print [] < (if false then v_seq_9 else []);
}

Command to run and resulting output

$ dafny /compile:4 /compileTarget:java test.dfy 

_System/__default.java:14: error: method isProperPrefixOf in class DafnySequence<T> cannot be applied to given types;
    System.out.print(java.lang.String.valueOf((dafny.DafnySequence.<java.math.BigInteger> empty(dafny.TypeDescriptor.BIG_INTEGER)).isProperPrefixOf(((false) ? (_0_v__seq__9) : (dafny.DafnySequence.<java.math.BigInteger> empty(dafny.TypeDescriptor.BIG_INTEGER))))));
                                                                                                                                  ^
  required: DafnySequence<U>
  found: (false) ? [...]GER))
  reason: inference variable U has incompatible equality constraints BigInteger,CAP#1
  where U,T are type-variables:
    U extends Object declared in method <U>isProperPrefixOf(DafnySequence<U>)
    T extends Object declared in class DafnySequence
  where CAP#1 is a fresh type-variable:
    CAP#1 extends BigInteger from capture of ? extends BigInteger
1 error
Error while compiling Java files. Process exited with exit code 1

What happened?

Introducing the if then else condition as the second argument to the '<' operator for sequences causes compilation to Java to crash due to an incompatible type error.

Note that removing the if then else condition and replacing with just '[]' does not cause a crash

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

Linux

@Dilan-s Dilan-s added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label May 5, 2023
@fabiomadge fabiomadge added lang: java Dafny's Java transpiler and its runtime invalid translated code The compiler generates invalid code, making the the target language infrastructure crash part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag labels May 8, 2023
@keyboardDrummer keyboardDrummer added the during 2: compilation of correct program Dafny rejects a valid program during compilation label Feb 7, 2024
@keyboardDrummer keyboardDrummer added the priority: next Will consider working on this after in progress work is done label Apr 25, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
during 2: compilation of correct program Dafny rejects a valid program during compilation invalid translated code The compiler generates invalid code, making the the target language infrastructure crash kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: java Dafny's Java transpiler and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag priority: next Will consider working on this after in progress work is done
Projects
None yet
Development

No branches or pull requests

3 participants