Ada/Spark: Where is the "platinum" mode in gnatprove?...

SPARK Functional-Correctness Proof...