Support for an external lazy methods driver to control when the INITIALIZE_FUNCTION is generated
#5156
Conversation
thomasspriggs
requested review from
cesaro,
cristina-david,
peterschrammel,
pkesseli,
smowton and
thk123
as code owners
| @@ -58,4 +74,6 @@ void java_internal_additions(symbol_table_baset &dest) | |||
| symbol.is_static_lifetime = true; | |||
| dest.add(symbol); | |||
| } | |||
|
|
|||
| create_java_initialize(dest); | |||
There was a problem hiding this comment.
I wouldn't hide this inside internal_additions, just explicitly call it where needed
| @@ -942,6 +944,8 @@ bool java_bytecode_languaget::typecheck( | |||
| convert_single_method( | |||
| method_sig.first, journalling_symbol_table, class_to_declared_symbols); | |||
| } | |||
| convert_single_method( | |||
| INITIALIZE_FUNCTION, journalling_symbol_table, class_to_declared_symbols); | |||
There was a problem hiding this comment.
What about old ci-lazy-methods?
There was a problem hiding this comment.
That is already indirectly tested via the regression tests. I chose to add a unit test of the new functionality in this PR, because it would otherwise be untested within this repository.
There was a problem hiding this comment.
I guess I could add a unit test of that...
This allows for an external lazy methods driver to control when the `INITIALIZE_FUNCTION` is generated.
thomasspriggs
force-pushed
the
tas/lazy_initialize
branch
from
3f8c646 to
6423c08
Compare
This tests that an empty bodied initialize function is generated by `typecheck` and that the body is then populated by `convert_lazy_method`
thomasspriggs
force-pushed
the
tas/lazy_initialize
branch
from
6423c08 to
3989689
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 3989689).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/131119343
To describe what the tests are doing.
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 082b368).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/131147875
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.
Codecov Report
@@ Coverage Diff @@
## develop #5156 +/- ##
===========================================
- Coverage 67.12% 67.08% -0.05%
===========================================
Files 1149 1149
Lines 94194 94037 -157
===========================================
- Hits 63229 63082 -147
+ Misses 30965 30955 -10
Continue to review full report at Codecov.
|
Support for an external lazy methods driver to control when the
INITIALIZE_FUNCTIONis generated. TheINITIALIZE_FUNCTIONneeds to be generated after all needed string literals have been added to the symbol table. The existing implementation tied the generation of theINITIALIZE_FUNCTION, to the point wheregenerate_support_functionsis called. This PR frees an external loading driver to generate theINITIALIZE_FUNCTIONseparately.The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/- N/AMy commit message includes data points confirming performance improvements (if claimed).Non claimed