Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Allow final fields to be written once in java_verify #152

Closed
atomb opened this issue Jun 29, 2016 · 1 comment
Closed

Allow final fields to be written once in java_verify #152

atomb opened this issue Jun 29, 2016 · 1 comment
Assignees
@atomb
Labels
obsolete Issues that involve/depend on deprecated code, such that they are not worth pursuing

Comments

@atomb
Copy link
Contributor

atomb commented Jun 29, 2016

Class initializers set final fields to their one, constant value. Currently, java_verify treats these initializations as disallowed, even though they are effectively constants. We should be able to simply ignore modifications to final fields, since the JVM ensures these modifications will happen only once.
@atomb atomb added the priority High-priority issues label Jun 29, 2016
@atomb atomb self-assigned this Jun 29, 2016
@atomb
Copy link
Contributor Author

atomb commented Oct 13, 2016

This issue is somewhat ameliorated by the introduction of java_requires_class, which can be used to ensure that a class initializer runs before execution of the method being verified.

@atomb atomb removed the priority High-priority issues label May 3, 2017
@atomb atomb added the obsolete Issues that involve/depend on deprecated code, such that they are not worth pursuing label Apr 2, 2019
brianhuffman pushed a commit that referenced this issue Apr 26, 2021
Merge pull request #152 from GaloisInc/issue151
0d1051d 
Adapt Conversion library to use `scGlobalDef` when building terms.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@atomb atomb

Labels
obsolete Issues that involve/depend on deprecated code, such that they are not worth pursuing
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@atomb @brianhuffman