options for warnings/post-processing

[vogler]

There's some weirdness with the options and code for warnings:

• Goblintutil.may_narrow is only used to decide whether warnings/post-processing should be done and misused for it in the case of dbg.earlywarn (solver runs with may_narrow = false).
  

  analyzer/src/util/goblintutil.ml

  Lines 61 to 63 in adeb01f

  	(** Tells the spec that result may still get smaller (on narrowing).
  	If this is false we can output messages and collect accesses. *)
  	let may_narrow = ref true

  
  

  analyzer/src/framework/control.ml

  Lines 342 to 344 in adeb01f

  	let do_analyze_using_solver () =
  	if get_bool "dbg.earlywarn" then Goblintutil.may_narrow := false;
  	let lh, gh = Stats.time "solving" (Slvr.solve entrystates []) startvars' in

• Warnings/post-processing are done during the verification phase. With --enable noverify there are no warnings. This should be decoupled.
• --enable noverify is weird (we have some no-... options for contexts, but those are actively changing something instead of not doing something).
• The code in messages.ml could use some cleanup/comments.

[michael-schwarz]

The refactoring of messages.ml is part of #201