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

Support multi-dimensional Java arrays #44

Closed
atomb opened this issue Jul 31, 2015 · 3 comments
Closed

Support multi-dimensional Java arrays #44

atomb opened this issue Jul 31, 2015 · 3 comments
Assignees
@atomb
Labels
type: enhancement Issues describing an improvement to an existing feature or capability
Milestone
0.4

Comments

@atomb
Copy link
Contributor

atomb commented Jul 31, 2015

The current set of commands in the JavaSetup context does not support declaring or stating properties about multi-dimensional arrays.
@atomb atomb added the type: enhancement Issues describing an improvement to an existing feature or capability label Aug 5, 2015
@robdockins robdockins self-assigned this Aug 7, 2015
@atomb atomb assigned atomb and unassigned robdockins Mar 9, 2016
@atomb atomb added the priority High-priority issues label Mar 9, 2016
@atomb atomb removed the priority High-priority issues label May 3, 2017
@atomb
Copy link
Contributor Author

atomb commented Apr 2, 2019

We should ensure that we can do this with the Crucible-based interface to Java verification.

@brianhuffman
Copy link
Contributor

The new Crucible-JVM interface can describe multi-dimensional arrays, but not concisely. Basically, you have to describe things as explicit arrays of arrays, with a points_to constraint for each element at every level.

We need to design some higher-level commands for declaring multi-dimensional arrays without all the repetition. It also might help to extend the Crucible-JVM memory model/object representation to support multi-dimensional arrays directly (so we can avoid the overhead of all the object references at intermediate levels).

@atomb atomb added this to the 1.0 milestone Jun 4, 2019
@atomb atomb modified the milestones: 1.0, 0.4 Oct 1, 2019
@atomb
Copy link
Contributor Author

atomb commented Oct 8, 2019

I think the remaining work on this is encompassed in #422, so this issue can be closed.

@atomb atomb closed this as completed Oct 8, 2019
brianhuffman pushed a commit that referenced this issue Apr 26, 2021
Switch Lambda and Pi constructors to use Text instead of String.
9b3dc10 
We introduce a type synonym `LocalName = Text` for this purpose.

This is a step toward removing all uses of `String` in saw-core
(#44).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@atomb atomb

Labels
type: enhancement Issues describing an improvement to an existing feature or capability
Projects
None yet
Milestone
0.4
Development

No branches or pull requests
3 participants
@atomb @brianhuffman @robdockins