Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Enable parser to accept
transient
as data location or identifier #15001base: catchSolUnimplementedFeatureErrors
Are you sure you want to change the base?
Enable parser to accept
transient
as data location or identifier #15001Changes from all commits
96760e4
e65fb17
d196c33
2e99c16
6a55279
7525a68
ce01cd3
6925866
947a802
f5024f9
4897478
22e3b5e
34d3d01
59a4566
d6289ff
9b325bb
211070b
f5076cc
File filter
Filter by extension
Conversations
Jump to
There are no files selected for viewing
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think that this check would fit better in
analyze()
(somewhere after theif (m_settings.engine.none())
check there).checkRequestedSourcesAndContracts()
looks more like it was meant for validating settings, not sources. It does look at the AST but only to validate the contract names supplied in settings. Rejecting unsupported transient variables on the other hand feels more like it should be a part of the analysis process.If you do it here, you're always checking it for all the sources. So you're making it impossible for the user to still use SMTChecker in presence of
transient
by just telling it to run on contracts that do not contain it. In fact, maybe it would even be better to move this check as far asCHC::visit(ContractDefinition)
andBMC::visit(ContractDefinition)
because otherwise we're still ignoring thecontracts
setting.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Since unimplemented errors are not ICEs, we should provide a clear message for the user in each one.