-
Notifications
You must be signed in to change notification settings - Fork 112
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
Refactored the define attribute on functions #236
Merged
Merged
Changes from 22 commits
Commits
Show all changes
31 commits
Select commit
Hold shift + click to select a range
ab5df04
fixup! Add support for function definitions
f29eedd
Add support for function definitions
f321806
fixup! Add support for function definitions
d746ece
fixup! Add support for function definitions
8b416f9
fixup! Add support for function definitions
18e18ab
fixup! Add support for function definitions
a4aed19
fixup! Add support for function definitions
778d897
Refactored support for function definitions
zvonimir e61b35a
Minor fix, no need to pass false as immutable to forall constructor
zvonimir d9be498
Fixed indentation in parser
zvonimir 2cbc782
Moved data type processing into a separate function
zvonimir 32d5c3d
Moved processing of function definitions into a separate file
zvonimir 5fabe6f
Prevent function arguments from being declared in SMT queries
zvonimir d6820fe
Cleaned up the code and added some comments
zvonimir c45d561
Fixed a problem with missing function definition dependencies
zvonimir 770b21b
Renamed DefBody into DefinitionBody
zvonimir 6fae2eb
Function cannot have both inline and define enabled
zvonimir 2978973
Added assertions and more comments
zvonimir 2dbc8c3
Added more complex regressions that use function definitions
zvonimir a3f14e4
Added more regressions
zvonimir 11d834f
Minor fix since I messed up expected output for a regression
zvonimir c3c56bf
Merge branch 'master' into define-func
zvonimir 440921e
Fixed expected regression results based on updates to CIVL
zvonimir c3a1f48
Merge branch 'master' into define-func
zvonimir b90bb21
Added useArrayTheory to SMACK regression that uses function definitions
zvonimir 7795d0f
Function definitions work only with monomorphic functions
zvonimir 719c84f
Added checking and error reporting for polymorphic functions
zvonimir 723f921
Minor fix to wording of error messages
zvonimir 83bbd83
Added regression that checks for recursion in function definitions
zvonimir 6728ce2
Minor fix
zvonimir 5260c33
Check for function monomorphism before creating definition body
zvonimir File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
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
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
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
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
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
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
Oops, something went wrong.
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.
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 concede that this makes the code clearer, but it does require you to duplicate code - wherever Body was used before, there are now two cases. I did not attempt to check that you caught every such case, so I have to trust you did.
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.
Yes, you are absolutely right, and this is a valid point. I made sure I checked off all such occurrences and I don't think I missed any.
The original plan I discussed with Shaz was not to duplicate code, but to use
Body
for both. However,Body
is being leveraged in rarely used codes (AbstractHoudini and FixedPointVC) that we do not quite understand. Hence, I was hesitant to reuse it until someone either cleans up AbstractHoudini and FixedPointVC or completely removes them. My time was running out and I did not get to that.