Mark native methods java_method_typet with ID_is_native_method
#2888
Conversation
mgudemann
requested review from
NathanJPhillips,
cesaro,
cristina-david,
peterschrammel,
pkesseli,
smowton and
thk123
as code owners
allredj
left a comment
allredj
left a comment
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 69e389a).
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).
thk123
left a comment
thk123
left a comment
There was a problem hiding this comment.
Please add setter/getter to java_method_typet to avoid exposing underlying irept structure
Please add simple unit test as done with bridge.
mgudemann
force-pushed
the
feature/jbmc/mark_ACC_NATIVE_java_methods
branch
from
69e389a to
d10ba94
Compare
|
@thk123 added access methods and unit tests |
mgudemann
force-pushed
the
feature/jbmc/mark_ACC_NATIVE_java_methods
branch
2 times, most recently
from
88a0e34 to
449e515
Compare
| require_type::require_java_method(function_symbol.type); | ||
| THEN("The method symbol should be of java_method_typet") | ||
| { | ||
| REQUIRE(function_type.get_bool(ID_C_java_method_type)); |
There was a problem hiding this comment.
⛏️ I wouldn't bother with this
| GIVEN("A class with a native method") | ||
| { | ||
| const symbol_tablet symbol_table = load_java_class( | ||
| "ClassWithNativeMethod", "./java_bytecode/java_bytecode_convert_method"); |
There was a problem hiding this comment.
CI is failing as you've not checked the class file in I believe!
| /*******************************************************************\ | ||
| Module: Unit tests for converting constructors and static initializers | ||
| Module: Unit tests for classes with bridge methods and native methods |
There was a problem hiding this comment.
When this is rebased on develop, it will include tests for methods which are neither bridge, static, or native methods. Maybe find a more general formulation? Unit tests for converting methods?
mgudemann
force-pushed
the
feature/jbmc/mark_ACC_NATIVE_java_methods
branch
2 times, most recently
from
562d8b3 to
aeea8ec
Compare
allredj
left a comment
allredj
left a comment
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 562d8b3).
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).
allredj
left a comment
allredj
left a comment
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: aeea8ec).
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).
mgudemann
force-pushed
the
feature/jbmc/mark_ACC_NATIVE_java_methods
branch
from
aeea8ec to
856902c
Compare
allredj
left a comment
allredj
left a comment
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 856902c).
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).
mgudemann
force-pushed
the
feature/jbmc/mark_ACC_NATIVE_java_methods
branch
from
856902c to
dd00225
Compare
allredj
left a comment
allredj
left a comment
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: dd00225).
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).
No description provided.