dafny
dafny copied to clipboard
Bad code generated for edge-case when using `generate-tests`
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)