Java front-end: rule out multiple parallel instances of java_bytecode_languaget #4434
Conversation
…_languaget The front-end, unlike the C front-end, is not designed to be run on a partially populated symbol table. Ensure we don't do that using an invariant in java_bytecode_languaget::typecheck, and forestall hitting that invariant with a friendlier error message in the Java frontend programs. Note jdiff did not require any change as it already insists on exactly two arguments.
smowton
requested review from
cesaro,
cristina-david,
NathanJPhillips,
peterschrammel,
pkesseli and
thk123
as code owners
|
Would you mind also changing the |
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 32be85e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/105821593
|
@tautschnig do you approve now that #4437 is in? |
Sure, but my approval doesn't really count for Java stuff... |
| if(cmdline.args.empty()) | ||
| { | ||
| error() << "Please provide a program to verify" << eom; | ||
| return 6; |
There was a problem hiding this comment.
I'd use CPROVER_EXIT_USAGE_ERROR here
| "'--lazy-methods-extra-entry-point somepackage.SomeClass.method' along " | ||
| "with '--classpath'" | ||
| << messaget::eom; | ||
| return 6; |
There was a problem hiding this comment.
I'd use CPROVER_EXIT_USAGE_ERROR here
|
Nothing else in |
The front-end, unlike the C front-end, is not designed to be run on a partially populated symbol table.
Ensure we don't do that using an invariant in java_bytecode_languaget::typecheck, and forestall hitting
that invariant with a friendlier error message in the Java frontend programs.
Note jdiff did not require any change as it already insists on exactly two arguments.
@tautschnig I suggest this as an alternative to #4390