search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.91k stars 262 forks source link

Java doesn't like nested array of chars #5741

Open kbuaaaaaa opened 2 months ago

kbuaaaaaa commented 2 months ago

Dafny version

4.7.0 (but also in older versions)

Code to produce this issue

method Main() {
  var v2 := new char[1];
  var v3 := new array<char>[1][v2];
}

Command to run and resulting output

dafny run -t java main.dfy

Dafny program verifier finished with 1 verified, 0 errors
Exception in thread "main" java.lang.ClassCastException: class [[C cannot be cast to class [[I ([[C and [[I are in module java.base of loader 'bootstrap')
    at _System.__default.Main(__default.java:16)
    at _System.__default.__Main(__default.java:21)
    at main.lambda$main$0(main.java:8)
    at dafny.Helpers.withHaltHandling(Helpers.java:350)
    at main.main(main.java:8)

What happened?

Might be related to #3055 ?

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

Linux, Mac

robin-aws commented 1 month ago

Almost certainly a subset of #3055 but will need to confirm.

kbuaaaaaa commented 1 week ago

I am convinced that these two issues are different.

This code compiled successfully at the time issue #3055 was reported. The problem here was actually introduced later by commit 5758205aae4ae4099aa6a110b0ec29dabe12dcee.

Also, for nested char arrays as in issue #3055, Dafny outputs broken Java that cannot be compiled. The translated Java here compiles correctly but causes a runtime exception.