search

dafny-lang / dafny

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

Havocs allow null arrays #5599

Open anymeyer opened 2 weeks ago

anymeyer commented 2 weeks ago

Dafny version

4.7.0

Code to produce this issue

method Havoc()
{
   var a:array<int> := *;
   assert a != null;
}

Command to run and resulting output

dafny verify prog.dfy

What happened?

Linux's Dafny 3.7.1, 4.6.0 and 4.7.0 all work correctly and generate a warning that the array cannot be null in the assert statement. But 4.7 now also incorrectly generates an assertion violation.

The program works correctly on the mac's 4.7.0, curiously.

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

Linux

anymeyer commented 2 weeks ago

My comment on the last line of "What happened?" is incorrect. The program also fails on mac 4.7.0.

anymeyer commented 6 days ago

The code
var b:nat := *; assert b>=0; also causes an assertion violation on Linux and the Mac. It appears to be the verify option on the command line that is causing the problem.

whonore commented 6 days ago

This looks like the same problem as #3742.