asserting in expressions
#660
Closed
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
expandPredicates can handle unfolding and quantifier exprs properly removeFoldUnfold no longer produces extraneous statements
(Flatten a Seq[Set[String]] into a Set[String])
I'll also try to separate out retrieving the prePred/postPredIds.
For the life of me I cannot figure out how to do this functionally with the Strategys
…erly permissive causeing issue for tests that had "file" in there name
… the base carbon test suite with inlining on
…r includes an inline pred
# Conflicts: # src/main/scala/viper/silver/plugin/standard/inline/InlineRewrite.scala
Fixed Transformer
# Conflicts: # src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala # src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala # src/main/scala/viper/silver/frontend/SilFrontend.scala # src/main/scala/viper/silver/parser/FastParser.scala # src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala # src/test/scala/PluginTests.scala
alexanderjsummers
requested changes
Mar 16, 2023
There was a problem hiding this comment.
I'm not sure this is needed for the asserting in feature?
There was a problem hiding this comment.
I reverted the PredicateInline changes, I'm not sure how to fix the history without redoing all the merging again,
There was a problem hiding this comment.
Thanks, I see. Since the final diff is relatively few lines, in the worst case you could replay it by hand. But I think there is likely a better git way to do this and not leave the plugin changes out of sync or in the master history of silver. Maybe that's the cherry-pick route?
|
see #663 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Adds
asserting inexpressions to also for assertions in expression position.