Cleanup options

[vogler]

There are 32 'experimental' options. Maybe those could be better classified or cleaned up.
The number of experimental options should be kept at a minimum.
Todo:

• Introduce additional categories:
  • witness
  • solver
  • context
  • incremental
  • output
• Sort experimental options into the categories
• Rename defaults.ml to options.ml
• Finalize options, so that they cannot be mutated after the solver started
• ana.warnings is used
• warnstyle only refers to race warnings

Related #192

[michael-schwarz]

@sim642: What is the state of dbg.test.domain? Right now it fails right away with

domain testing analysis...: PathSensitive2(MCP2 context hashconsed) lifted hashconsed
About to crash! (:-1)
Fatal error: exception Failure("HConsed lifted PathSensitive (Set ([expRelation:(Unit), mallocWrapper:(lifted proglines), base:(value domain * array partitioning deps * P), threadid:(Thread), threadflag:(MT mode), escape:(top or Set (variables)), mutex:(Reversed (top or Set (Normal Lvals * booleans)))])): no arbitrary")

Do we want this option to do domain testing when running on a single program? If yes we should aim to fix it?
Or is this superfluous since we introduced the make domaintest target?

[sim642]

dbg.test.domain is separate from domaintest. The latter is testing the single small "leaf" domains that are explicitly listed for direct testing. The former is for testing Spec.D itself, which cannot be reasonably assembled in the separate domaintest executable without all the options and valid CIL values around (because some domains actually use them, but writing an Arbitrary instance for varinfo etc is problematic, if I remember correctly).

Since I never implemented arbitrary for every single domain in Goblint, dbg.test.domain has never tested the complete extent of the domains. Although when it initially was added, it at least didn't crash but just used trivial arbitrary implementations for some things.

So I'd keep it because it should allow testing the actual domain of the analysis, which depends on all the options, not just a handful we can test separately, for example all the domain functors. I'll have to see what the failing piece is right now.

[michael-schwarz]

Closed in favor of #653.