Class SymbolicAnalysis

java.lang.Object
org.ek9lang.compiler.CompilerPhase
org.ek9lang.compiler.symbolic.SymbolicAnalysis
All Implemented Interfaces:
BiFunction<Workspace, CompilerFlags, CompilationPhaseResult>
public class SymbolicAnalysis extends CompilerPhase
SINGLE THREADED The Layer-2 symbolic/contract verification pass (docs/tooling/EK9_SYMBOLIC_SCANNER_IMPLEMENTATION_SPEC.md §4.4). It runs SymbolicEngine over every user callable and squirrels the ConstructVerdict — the SYMBOLIC_VERIFIED flag and the SYMBOLIC_COUNTEREXAMPLES witness list — so the @Verified/@Counterexample directive listeners (compiler self-tests) and the Contract roundel can read it, exactly as the M1 census squirrels OBLIGATIONS_* at PRE_IR_CHECKS.

Off by default. The bounded-model solver is expensive relative to a normal build and is not wanted on every compile, so the whole phase is a no-op unless -Xverify (CompilerFlags.isVerifyEnabled()) is set — used by the directive-test harness and the on-demand / report paths. It sits after PLUGIN_RESOLUTION and before IR_GENERATION (the first middle-end phase) so every symbol is fully resolved and the census is already squirrelled; it never runs during bootstrap (which uses only the front-end supplier).

Advisory only. A counterexample is not a compile error — it is squirrelled data a directive or the report surfaces. The phase therefore always reports success; it adds nothing to any source's error listener.