add Java monitorenter/exit symbols #2286
Conversation
kroening
requested review from
mgudemann,
peterschrammel,
smowton and
thk123
as code owners
| code_typet type; | ||
| type.return_type() = void_typet(); | ||
| type.parameters().resize(1); | ||
| type.parameters()[0].type() = java_reference_type(void_typet()); |
There was a problem hiding this comment.
Perhaps an Object *, since that defines the @lock field they are expected to use?
|
Marking do-not-merge as per #2280 (comment). |
| code_typet type; | ||
| type.return_type() = void_typet(); | ||
| type.parameters().resize(1); | ||
| type.parameters()[0].type() = java_reference_type(void_typet()); |
There was a problem hiding this comment.
Once the other concerns are addressed, please use the new code_typet constructor that takes two arguments.
kroening
force-pushed
the
monitorenter-exit
branch
from
d03cf29 to
657d744
Compare
|
Both done |
|
@kroening I don't think this is needed. The critical section is implemented as part of the java-model library (https://github.com/diffblue/java-models-library) in two methods: |
|
Hi @tautschnig, would it be possible for this to be rebased on top of current |
I guess it's up to @kroening for this one - based on earlier comments it's not clear to me whether this is needed at all. |
|
I think this can be closed as obsolete. |
|
I am going forward with closing this as previous comments indicate this is now obsolete. |
These are needed for any "synchronized" methods.