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:
if (str == null)
str2 = ".dfy";
str2 = str;
Note that "str" is uninitialized. It should have been initialized to the left-hand operand of ??.