Dependence of libraries on CommandLineOptions.Clo should be removed

[delcypher]

I'm currently using Boogie as a library and there is an issue that makes it incredibly painful to use. The issue is lots of the code refers to CommandLineOptions.Clo which is the global command line object which causes lots of problems

• Lots of code simply crashes if CommandLineOptions.Clo is not initialised. There should not be a requirement to use this because clients may not want to use the Boogie command line parser. In my case I really don't want to use it but in order to prevent Boogie's libraries from crashing I have to create an instance of Microsoft.Boogie.CommandLineOptions.
• Using Microsoft.Boogie.CommandLineOptions brings in an implicit dependency on SMTLib.dll the Command line parser tries to do something disgusting and reads this dll to determine some command line arguments. This is really bad because if you want to use only the Core library you cannot because the SMTLib library has to be built as well.

I'd like to propose the following

• All stable features controlled by Command line flags should be made part of Boogie's API and the BoogieDriver should be responsible for using Boogie command line flags and using them to control Boogie's API
• Using Command line flags can be beneficial if working on an experimental feature because it allows you to reach deep inside Boogie's code without changing any of its API. For these experimental features controlling them via command line options should be allowed but the code should be written such that if the CommandLineOptions.Clo is not set then the code does not crash and the experiment feature is switched off.

[RustanLeino]

Would a simple solution be to declare the static Clo field with an initializer that creates, essentially, an empty object? By "empty" I mean an object where the options are set to default values.

[delcypher]

@RustanLeino
This would fix the crashes but it still leaves the problem of

• Some features being only accessible via the CommandLineOptions.Clo object instead of a proper API
• The implicit dependency on SMTLib.dll. This could probably be fixed though.

There is also a far worse problem that I forgot to mention is that the CommandLineOptions.Clo object is not thread safe!

For example I have method in my program to print a Boogie program to a file. It has an option to control whether the structured, unstructured or both is emitted. This can only be controlled via the CommandLineOptions.Clo object (which is what I have to do). If another thread changes the CommandlineOptions.Clo object during printing then the emitted program could be corrupted.

Global state is evil!

[shazqadeer]

@delcypher : I am revisiting this issue after a long time. In the above, you refer to a "Boogie API". What do you mean by that?

[shazqadeer]

The global static for tracking options has been eliminated.