docs: require Java 8 as the active JDK

[tomatotomata]

Description

Fixes #9111.

Clarify that JBMC requires Java 8 to be the active default JDK, not merely installed alongside a newer JDK. The Linux instructions now show runtime/compiler verification and the appropriate alternatives commands for Debian-like and Red Hat/Fedora systems. The FreeBSD instructions now explain how to activate OpenJDK 8 through JAVA_HOME and PATH.

Validation

• git diff --check

This documentation-only change does not require a compiled CBMC/JBMC test run.

[kroening]

Fixes #9111.

Clarify that JBMC requires Java 8 to be the active default JDK, not merely installed alongside a newer JDK. The Linux instructions now show runtime/compiler verification and the appropriate alternatives commands for Debian-like and Red Hat/Fedora systems. The FreeBSD instructions now explain how to activate OpenJDK 8 through JAVA_HOME and PATH.

Can we instead not require Java 8 to be the default JDK?

[tomatotomata]

Yes. The build uses the Java toolchain available in its shell, so requiring Java 8 as the system-wide default was unnecessarily invasive. c526747 now instructs users to select Java 8 only for the build via JAVA_HOME and PATH, then verify java and javac report 1.8.

[kroening]

Yes. The build uses the Java toolchain available in its shell, so requiring Java 8 as the system-wide default was unnecessarily invasive. c526747 now instructs users to select Java 8 only for the build via JAVA_HOME and PATH, then verify java and javac report 1.8.

Sorry, I wasn't clear: can we support versions other than Java 8, so this requirement is no longer necessary?

[tomatotomata]

I checked the build inputs before answering this. The regression POM targets Java 8 bytecode, but the pinned java-models-library submodule still configures maven-compiler-plugin with ${java.home}/lib/rt.jar; that path only exists on JDK 8. So a newer JDK is not currently just a documentation choice. Supporting newer versions would need a separate migration of that submodule/compiler setup, plus JBMC regression validation. I kept this PR scoped to documenting the current requirement and selecting Java 8 in the build shell rather than changing that build system.

[peterschrammel]

Yes, supporting JDKs above 8 requires considerable work.

Step one has been done in this series of PRs (that @tautschnig gladly pushed to merge) to make the regression test system compile benchmarks from source instead of committing class files. That's the basis to add additional regression test CI jobs that compile with newer, yet unsupported JDK versions to understand what breaks and fix both, JBMC as well as the models library, step by step.