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

Initialize all Java fields to fresh values unless otherwise specified in java_verify #69

Closed
atomb opened this issue Oct 13, 2015 · 1 comment
Closed

Initialize all Java fields to fresh values unless otherwise specified in java_verify #69

atomb opened this issue Oct 13, 2015 · 1 comment
Labels
obsolete Issues that involve/depend on deprecated code, such that they are not worth pursuing type: enhancement Issues describing an improvement to an existing feature or capability

Comments

@atomb
Copy link
Contributor

atomb commented Oct 13, 2015

When using java_verify, ensure that each field of a newly created object has a fresh value, rather than the default zero value. Using the proposed java_assert_eq, (#68) the user could overwrite this fresh value with a different value if desired, or constrain its value with the current java_assert command.
@atomb atomb added the type: enhancement Issues describing an improvement to an existing feature or capability label May 2, 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
Copy link
Contributor

The java_verify command is set to be removed as part of #1005, so I'm closing.

brianhuffman pushed a commit that referenced this issue Apr 26, 2021
Merge pull request #69 from GaloisInc/typed-extcns
bd853c8 
Additions to Verifier.SAW.TypedTerm library
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
obsolete Issues that involve/depend on deprecated code, such that they are not worth pursuing type: enhancement Issues describing an improvement to an existing feature or capability
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@atomb @brianhuffman