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

Add support for JVM globals (i.e. static fields) #908

Closed
brianhuffman opened this issue Nov 17, 2020 · 2 comments · Fixed by #981
Closed

Add support for JVM globals (i.e. static fields) #908

brianhuffman opened this issue Nov 17, 2020 · 2 comments · Fixed by #981
Assignees
@brianhuffman
Labels
subsystem: crucible-jvm Issues related to Java verification with crucible-jvm
Milestone
0.8

Comments

@brianhuffman
Copy link
Contributor

Currently SAW has no way to specify the contents of a static field in the pre- or post-state section of a JVMSetup block. We need to add support for this.
@brianhuffman brianhuffman added the subsystem: crucible-jvm Issues related to Java verification with crucible-jvm label Nov 17, 2020
@brianhuffman brianhuffman self-assigned this Nov 17, 2020
@brianhuffman brianhuffman mentioned this issue Nov 18, 2020
Open
@brianhuffman
Copy link
Contributor Author

Currently there is a jvm_global function in saw-script that doesn't work and should probably be removed.

brianhuffman pushed a commit that referenced this issue Dec 2, 2020
Remove non-functional saw-script function jvm_global.
6a62999 
Support for static fields is planned using a different mechanism.
(See #908.)
brianhuffman pushed a commit that referenced this issue Dec 3, 2020
Remove non-functional saw-script function jvm_global.
191a0e9 
Support for static fields is planned using a different mechanism.
(See #908.)
brianhuffman pushed a commit that referenced this issue Dec 4, 2020
Remove non-functional saw-script function jvm_global.
45928e0 
Support for static fields is planned using a different mechanism.
(See #908.)
brianhuffman pushed a commit that referenced this issue Dec 4, 2020
Remove non-functional saw-script function jvm_global.
db75c2b 
Support for static fields is planned using a different mechanism.
(See #908.)
@atomb atomb added this to the 0.8 milestone Dec 11, 2020
@brianhuffman
Copy link
Contributor Author

I have implemented this in a branch, but it's not really useful until we have a way to specify class initialization status (#916).

@brianhuffman brianhuffman mentioned this issue Dec 16, 2020
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@brianhuffman brianhuffman

Labels
subsystem: crucible-jvm Issues related to Java verification with crucible-jvm
Projects
None yet
Milestone
0.8
Development

Successfully merging a pull request may close this issue.

Add jvm_static_field_is command for specifying static fields in JVM. GaloisInc/saw-script
2 participants
@atomb @brianhuffman