dafny icon indicating copy to clipboard operation
dafny copied to clipboard

Bad code generated for edge-case when using `generate-tests`

Open keyboardDrummer opened this issue 1 year ago • 0 comments

Input

Code:

module M {
  method {:testEntry} Main() {
  }
}
module A {
  function UnsafeSetToSeq<T>(s: set<T>): seq<T>
    requires false
    ensures forall x <- s :: x in s <==> x in UnsafeSetToSeq(s)
  {
    if s == {} then []
    else
      var x :| x in s;
      [x] + UnsafeSetToSeq(s - {x})
  }
}

module B {
  function {:axiom} mapToString<A>(toStr: A -> string, m: map<string, A>): string {
    if |m| == 0 then ""
    else var k :| k in m;
      assume {:axiom} false;
      k + " -> " + toStr(m[k]) + "\n" + mapToString(toStr, m - {k})
  }
}

Cli: dafny generate-tests InlinedBlock <file> --length-limit:50

Bad output

include "..."
module ....UnitTests {
(1972,622): Error: invalid type for argument 1 in application of $let#0$canCall: Map (expected: Set)
(1974,649): Error: invalid type for argument 1 in application of $let#0$canCall: Map (expected: Set)
(1976,659): Error: invalid type for argument 1 in application of $let#0$canCall: Map (expected: Set)
(1994,152): Error: invalid type for argument 1 in application of $let#0$canCall: Map (expected: Set)
(2071,57): Error: invalid type for argument 1 in application of $let#0$canCall: Map (expected: Set)
(1811,622): Error: invalid type for argument 1 in application of $let#0$canCall: Map (expected: Set)
(1812,649): Error: invalid type for argument 1 in application of $let#0$canCall: Map (expected: Set)
(1813,659): Error: invalid type for argument 1 in application of $let#0$canCall: Map (expected: Set)
(1828,152): Error: invalid type for argument 1 in application of $let#0$canCall: Map (expected: Set)
(1897,57): Error: invalid type for argument 1 in application of $let#0$canCall: Map (expected: Set)
(1817,622): Error: invalid type for argument 1 in application of $let#0$canCall: Map (expected: Set)
(1818,649): Error: invalid type for argument 1 in application of $let#0$canCall: Map (expected: Set)
(1819,659): Error: invalid type for argument 1 in application of $let#0$canCall: Map (expected: Set)
(1834,152): Error: invalid type for argument 1 in application of $let#0$canCall: Map (expected: Set)
(1905,57): Error: invalid type for argument 1 in application of $let#0$canCall: Map (expected: Set)

keyboardDrummer avatar Jul 31 '24 11:07 keyboardDrummer