Error message when entry function body cannot be produced [TG-8299]

[peterschrammel]

Previously crashed on a failed map.at

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[allredj]

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: b590a06).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/120286881
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-io]

Codecov Report

Merging #4943 into develop will decrease coverage by <.01%.
The diff coverage is 100%.

@@             Coverage Diff             @@
##           develop    #4943      +/-   ##
===========================================
- Coverage    69.26%   69.26%   -0.01%     
===========================================
  Files         1307     1307              
  Lines       108102   108092      -10     
===========================================
- Hits         74881    74871      -10     
  Misses       33221    33221

Impacted Files	Coverage Δ
jbmc/src/java_bytecode/java_bytecode_language.cpp	93.33% <100%> (+0.04%)	⬆️
src/util/ssa_expr.cpp	87.5% <0%> (-0.31%)	⬇️
unit/util/ssa_expr.cpp	100% <0%> (ø)	⬆️
src/util/ssa_expr.h	100% <0%> (ø)	⬆️

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 3ad2a27...18fa5da. Read the comment docs.

[smowton]

Not sure most readers would comprehend "in the analysis context". How about "Specify an entry-point function defined on the classpath"? If they're using "--context-exclude" and so on they presumably understand the hole they're making in the realm of loaded classes?

[peterschrammel]

That would be misleading. The case that it is not on the classpath is already covered elsewhere. This only happens with context restrictions.

[smowton]

Hmm. Perhaps name-check the offending --context-exclude argument?

[peterschrammel]

I don't understand

[smowton]

For example, "The specified entry-point was not in the analysis context; check that it is included by your --context-include or --context-exclude options"

[smowton]

Or even just "was not available"; I'm trying to avoid saying "the analysis context" and hoping they know what that means

[peterschrammel]

Ok, changed.

[smowton]

Side-note, and not for this PR (I should have talked about this back when --context-in/exclude went in): why are we calling this "context" anyway? It's a pretty broad term that refers to a lot of different things, but I don't see any relationship between "the set of methods we don't stub" and "context"?

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: 18fa5da).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/120460442