goblint
Freeze Configuration to Avoid Timing Errors for Configurations
To prevent issues where the autotuner is run too late etc (c.f. #1265), we should devide the modification of the config into two phase: Config building and analysis:
- Functions during building (
get_build,set_build: The implementer needs to ensure correct order) -
freeze - Functions during analysis (
get_analysis)
If a call happens in the wrong phase, the analyzer should crash, making it easier to hunt-down such issues instead of having to deal with cases where settings seemingly are not applied.
This duplicates #944, which already introduced such mechanism. Unless that has been broken since.
It seems #944 does not cover all usecases (it is only concerned with not changing things while the solver runs). One can already get values before freezing and use them for the analysis. An example of this are the privatization modules which are constructed before the autotuner runs. The stricter mechanism proposed here should prevent this type of bug, by separating looking up options to potentially change other options from lookups that will be used during analysis.
The freezing point would just have to be moved earlier then. Maybe immediately before AfterConfig runs because those callbacks are supposed to run after configuration has been loaded and should be used.