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
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 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.