Skip to content

java: do not use void reference #4057

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

Closed
wants to merge 1 commit into from
Closed

java: do not use void reference #4057

wants to merge 1 commit into from

Conversation

kroening
Copy link
Member

@kroening kroening commented Feb 3, 2019

The concept of void * is borrowed from C. This commit changes void * to
a reference to java.lang.object.

The benefit is that we will be able to establish that all references in Java
are references to an object.

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@smowton
Copy link
Contributor

smowton commented Feb 4, 2019

Before this works we might need to ensure that array types are based on Object

@thk123
Copy link
Contributor

thk123 commented Feb 4, 2019

When I tried this before in #3992, it definitely broke things...

It broke because somehow a dynamically sized array got down to symex.

@kroening kroening mentioned this pull request Apr 6, 2019
4 tasks
@thk123
Copy link
Contributor

thk123 commented Apr 9, 2019

@smowton

that array types are based on Object

I'm not sure if this is what your question is referning to, but:

Object[] arr = new Object[4];
Object ao = arr;

Is valid Java

@smowton
Copy link
Contributor

smowton commented Apr 9, 2019

Sure, I meant that our representation should reflect that inheritance. Looks like we do though; once upon a time array[int] (for example) had a @class_identifier member; now it has a @java.lang.Object.

The concept of 'void *' is borrowed from C.  This commit changes 'void *' to
a reference to java.lang.object.

The benefit is that we will be able to establish that all references in Java
are references to an object.
@TGWDB
Copy link
Contributor

TGWDB commented Sep 15, 2021

Closing this as it appears to be very old and failing (ancient) CI. Please reopen if you believe this is erroneous and will rebase/update.

@TGWDB TGWDB closed this Sep 15, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants