Bug: Using Dafny.dll to build an AST fails if no compiler specified.

[MikaelMayer]

Since #1894 , ModuleExportDecl.FullCompileName used in the constructor of ModuleExportDecl can throw a null pointer exception because TopLevelDecl.FullCompileName now depends on DafnyOptions.O.Compiler, which does not have a default value.

[cpitclaudel]

Can you give a repro for this issue? The option-parsing code does Compiler ??= new CsharpCompiler();; when is it not called?

[cpitclaudel]

In other words, it's intended that FullCompileName depends on the compiler; the bug is that Compiler is null, and that's what we should fix.

[MikaelMayer]

The method ApplyDefaultOptions() is never called if one builds a DafnyOptions using the constructor.
Previously, it was only depending on whether the compiler target was C# or not, not the full compiler.

[cpitclaudel]

Previously, it was only depending on whether the compiler target was C# or not, not the full compiler.

Initializing a compiler instance doesn't really do that much, so it would be fine to initialize the compiler to be the C# one. But isn't it good that you get an error? It tells you that your code may depend on the internals of the compiler, which is good to know?

[keyboardDrummer]

When this does bug occur? It seems like it occurs if DafnyOptions.O are not properly initialised, like you might forget to do in a test. Isn't initialising them properly the fix then?

[MikaelMayer]

Yes indeed. However, previously, parsing would succeed even though DafnyOptions.O is not properly initialized. Users setting themselves the options without depending on our custom initialization faced the problem of having a field that is uninitialized (Compiler), which break their code.