The ?? operator, inherited from C# and with the meaning "return the left-hand operand unless it is null; if it is null, return the right-hand operator", is not compiled correctly by the Spec# compiler. In particular, I found that (s.Tok.filename ?? ".dfy") compiles the str2 in:

    string str;
    string str2;
    if (str == null)
    {
        str2 = ".dfy";
    }
    else
    {
        str2 = str;
    }

Note that "str" is uninitialized. It should have been initialized to the left-hand operand of ??.