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

Java synchronized blocks don't throw NullPointerException #1236

Open
reuk opened this issue Aug 14, 2017 · 1 comment
Open

Java synchronized blocks don't throw NullPointerException #1236

reuk opened this issue Aug 14, 2017 · 1 comment
Labels
bug Java Front End

Comments

@reuk
Copy link
Contributor

reuk commented Aug 14, 2017

The docs for the Java monitorenter instruction say that NullPointerException should be thrown if the argument to the synchronized block is null.

It seems like the current behaviour is to ignore monitorenter and monitorexit (according to #186), which leads to inaccurate results. I suggest that the exception-throwing behaviour is modelled, even if the thread-synchronization itself is not.
@reuk reuk mentioned this issue Aug 14, 2017
Merged
peterschrammel added a commit to peterschrammel/cbmc that referenced this issue Nov 14, 2018
@peterschrammel
Update jbmc/lib/java-models-library to #11 (enable-monitor-exceptions)
bc9256a 
Allows to detect errors related to synchronization on null references,
for example.

Fixes diffblue#1236.
@peterschrammel peterschrammel self-assigned this Nov 14, 2018
peterschrammel added a commit to peterschrammel/cbmc that referenced this issue Nov 16, 2018
@peterschrammel
Update jbmc/lib/java-models-library to #11 (enable-monitor-exceptions)
e1b39c6 
Allows to detect errors related to synchronization on null references,
for example.

Fixes diffblue#1236.
peterschrammel added a commit to peterschrammel/cbmc that referenced this issue Nov 17, 2018
@peterschrammel
Update jbmc/lib/java-models-library to #11 (enable-monitor-exceptions)
50f62ac 
Allows to detect errors related to synchronization on null references,
for example.

Fixes diffblue#1236.
@peterschrammel peterschrammel removed their assignment Nov 17, 2018
@peterschrammel
Copy link
Member

The monitor entry exception is fixed in #3423.

The Monitor exit exceptions require additional attention: Enabling these exceptions makes jbmc-regression/synchronized-blocks/test_sync.desc run into an infinite loop during symex (which I don't have time to investigate now).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug Java Front End
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@tautschnig @reuk @peterschrammel