Adds summary for remove_exceptions [DOC-84] #2794
Conversation
jeannielynnmoulton
requested review from
cesaro,
cristina-david,
mgudemann,
NathanJPhillips,
peterschrammel,
pkesseli,
smowton and
thk123
as code owners
jeannielynnmoulton
force-pushed
the
jeannie/DocumentRemoveExceptions
branch
from
3bd5e1a to
1c83024
Compare
jbmc/src/java_bytecode/README.md
Outdated
|
|
||
| To be documented. | ||
| When `remove_exceptions` is called on the goto model, the goto model contains |
There was a problem hiding this comment.
There should be a link to the file/class.
jbmc/src/java_bytecode/README.md
Outdated
|
|
||
| To be documented. | ||
| When `remove_exceptions` is called on the goto model, the goto model contains | ||
| complex instructions such as `CATCH-POP`, `CATCH-PUSH` and `THROW`. In order to |
There was a problem hiding this comment.
Make instructions a link
jbmc/src/java_bytecode/README.md
Outdated
| and replacing irrelevant parts with `...`) is: | ||
|
|
||
| ``` | ||
| com.diffblue.regression.TestExceptions.testException(int) /* java::com.diffblue.regression.TestExceptions.testException:(I)V */ |
There was a problem hiding this comment.
there is no package in the example above. I suggest to remove it here.
There was a problem hiding this comment.
The package is used below, so I will leave it.
There was a problem hiding this comment.
The maybe complete the example by wrapping it into a class TestExceptions and adding a package statement in the beginning.
There was a problem hiding this comment.
I've removed the package and included a copy-pasteable test.
jbmc/src/java_bytecode/README.md
Outdated
|
|
||
| ``` | ||
| where now instead of the instruction `THROW`, the global variable | ||
| `@inflight_exception` holds the thrown exception in ia separate goto statement. |
There was a problem hiding this comment.
I think the words don't quite match up with the examples, you talk about removing a CATCH instruction, but it seems there are three different instructions CATCH-PUSH, CATCH-POP and LANDING-PAD? It'd be good to summarise what they get translated to at the top.
Otherwise LGTM
jbmc/src/java_bytecode/README.md
Outdated
| instructions - this is called "lowering". This class lowers the `CATCH` and | ||
| `THROW` instructions. | ||
|
|
||
| Exceptions that have been thrown, but not yet caught are stored the global |
There was a problem hiding this comment.
perhaps reword to be clearer
THROW instructions are replaced by assigning to @inflight_exception and a goto to end of the function.
CATCH instructions are replaced by a check of the @inflight_exception and setting it to null
There was a problem hiding this comment.
If the bit about the goto statement is right? In your below example it doesn't seem to introduce a GOTO so perhaps that is already present.
There was a problem hiding this comment.
Actually it'd be good to split out CATCH into CATCH-PUSH CATCH-POP and EXCEPTION LANDING PAD into roughly what they get translated into
There was a problem hiding this comment.
It introduces THEN GOTO 4
|
|
||
| ... | ||
|
|
||
| CATCH-PUSH ->2 |
There was a problem hiding this comment.
This needs some context I think?
There was a problem hiding this comment.
There is not much context to give, I'm afraid, but I've added some description to what this signifies.
thk123
changed the title
thk123
changed the title
jeannielynnmoulton
force-pushed
the
jeannie/DocumentRemoveExceptions
branch
from
1c83024 to
9d8422a
Compare
jeannielynnmoulton
requested review from
chrisr-diffblue,
forejtv,
kroening,
martin-cs and
tautschnig
as code owners
jeannielynnmoulton
force-pushed
the
jeannie/DocumentRemoveExceptions
branch
from
9d8422a to
5b5a77e
Compare
jeannielynnmoulton
force-pushed
the
jeannie/DocumentRemoveExceptions
branch
from
5b5a77e to
00ede79
Compare
There was a problem hiding this comment.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: 9d8422a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/91230518
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.
There was a problem hiding this comment.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: 5b5a77e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/91230843
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 00ede79).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/91233551
No description provided.