Open rami3l opened 2 years ago
I just tried the change you proposed locally, and I got the same error as in the figure you attached. I used SPARK Community 2021, which is the version that is currently being used on the learn website:
SPARK Community 2021 (20210519)
Why3 for gnatprove version 1.4.0+git
/opt/Ada/gpl/x86_64-linux/gnat-gpl-2021-x86_64-linux-bin/libexec/spark/bin/alt-ergo: Alt-Ergo version 2.3.0+
/opt/Ada/gpl/x86_64-linux/gnat-gpl-2021-x86_64-linux-bin/libexec/spark/bin/colibri: Colibri 2020.9
/opt/Ada/gpl/x86_64-linux/gnat-gpl-2021-x86_64-linux-bin/libexec/spark/bin/cvc4: This is CVC4 version 1.8
/opt/Ada/gpl/x86_64-linux/gnat-gpl-2021-x86_64-linux-bin/libexec/spark/bin/z3: Z3 version 4.8.10 - 64 bit
Your prover version is more recent. Maybe this plays a role here?
Also, this was the associated main.adc
:
pragma Profile(GNAT_Extended_Ravenscar);
pragma Partition_Elaboration_Policy(Sequential);
pragma SPARK_Mode (On);
pragma Warnings (Off, "no Global contract available");
pragma Warnings (Off, "subprogram * has no effect");
pragma Warnings (Off, "file name does not match");
In
Courses.Intro_To_Spark.Proof_of_Functional_Correctness.Example_08
:I tried moving L7-L8 in
array_util.adb
to the end ofif-else
which should be an obvious semantic error to be fixed.However, the online playground complains:
Local execution, on the other hand, completes without any problem: