This project is read-only.
1
Vote

Dependence of libraries on CommandLineOptions.Clo should be removed

description

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

comments