Debugging timed out programs

Oct 29, 2012 at 4:32 AM


Here is a program with out-of-bound array access but passed the verification phase of Dafny.

I have no idea what went wrong. I appreciate your help.


Oct 31, 2012 at 10:05 PM

Perhaps you're worried about the use of ret[i] in the loop, where there is neither any information about ret being non-null nor any information about i being within range of the array ret?  But note this this loop is never entered, because your program says:

    var current : CachePage := null;
    while (current != null)
    { ... }


Oct 31, 2012 at 11:19 PM

Thanks! I keep making silly mistakes :-(

After fixing it, Dafny timed out on the following program.

It seems that Dafny stucks at a particular VC, as a z3 process runs more than 30 minutes.

Here are the stack traces:

Unhandled Exception:System.IO.IOException: Write fault on path /Users/mai4/work/vm-shared/dafny/[Unknown]

  at System.IO.FileStream.WriteInternal (System.Byte[] src, Int32 offset, Int32 count) [0x00000] in <filename unknown>:0
  at System.IO.FileStream.Write (System.Byte[] array, Int32 offset, Int32 count) [0x00000] in <filename unknown>:0
  at System.IO.StreamWriter.FlushBytes () [0x00000] in <filename unknown>:0   at System.IO.StreamWriter.Flush () [0x00000] in <filename unknown>:0   at System.IO.StreamWriter.Write (System.String value) [0x00000] in <filename unknown>:0
   at System.IO.TextWriter.WriteLine (System.String value) [0x00000] in <filename unknown>:0   at Microsoft.Boogie.SMTLib.SMTLibProcess.Send (System.String cmd) [0x00000] in <filename unknown>:0
   at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.Send (System.String s, Boolean isCommon) [0x00000] in <filename unknown>:0   at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.SendThisVC (System.String s) [0x00000] in <filename unknown>:0
   at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.CheckOutcome (Microsoft.Boogie.ErrorHandler handler) [0x00000] in <filename unknown>:0
   at Microsoft.Boogie.Checker.WaitForOutput (System.Object dummy) [0x00000] in <filename unknown>:0 

Is there a way to pinpoint the problem and to fix it?