Moved floating point rounding mode into Program#1019
Moved floating point rounding mode into Program#1019ThomasHaas wants to merge 4 commits intodevelopmentfrom
Conversation
| // We only show the condition if this is the reason of the failure | ||
| String condition = ""; | ||
| final boolean ignoreFilter = task.getConfig().hasProperty(IGNORE_FILTER_SPECIFICATION) && task.getConfig().getProperty(IGNORE_FILTER_SPECIFICATION).equals("true"); | ||
| final boolean ignoreFilter = Objects.equals(task.getConfig().getProperty(IGNORE_FILTER_SPECIFICATION), "true"); |
There was a problem hiding this comment.
Does this now handle the case where we do not have the property?
There was a problem hiding this comment.
Yeah, it seems getProperty just returns NULL in that case.
| this.witness = checkNotNull(witness); | ||
| this.config = checkNotNull(config); | ||
|
|
||
| // TODO: Is it a good idea to inject configs into the program here? |
There was a problem hiding this comment.
What would be the alternative?
There was a problem hiding this comment.
Inject it right after parsing the program.
There was a problem hiding this comment.
Code-wise that would be bad, because we have different "places" where program is parsed (CLI, UI, unit tests) and we would have to inject it in all of them.
One could claim that we do not care the rounding mode unless we are doing the verification (and thus having the inject the VerificationTask is ok), but then this raises the question if the rounding mode should then indeed be part of the Program.
There was a problem hiding this comment.
Well, we have a central ProgramParser that is always used to parse the program. If that class was configurable via a Configuration, we could inject the settings there. Generally, making the parsers configurable would be a good idea and allow us to give options like ignore inline assembly or throw on unknown inline assembly etc.
If the rounding mode was part of the verification task, we would need to lift all program passes to verification task passes (at least in principle) for otherwise the rounding mode was inaccessible.
But for now, I think having the injection in VerificationTask is okayish.
2 participants
This is basically the less controversial half of #978 :)
I kept the
Program.SemanticConfigclass even though it contains only a single option right now.The biggest question is where to best inject the
Configurationinto theProgram. For simplicity, I do this when constructing theVerificationTask, but it is a bit sketchy.