Repository navigation
Conversation
- Restore compilation and flow analysis with `--report=all` using the default toolchain. - Expect the termination diagnostic for the original loop. Co-Authored-By: Codex <noreply@openai.com>
- Qualify the comparison with `Element_Array` so GNAT and GNATprove report ordinary errors for using abstract state as a value. - Restore compilation and flow analysis with the default toolchain. Co-Authored-By: Codex <noreply@openai.com>
Add a short note after the semicolon example to explain the loop termination diagnostic and the `Loop_Variant` that resolves it. Validated with GNATprove 16: the original loop reports an unproved `Always_Terminates` check. Adding `pragma Loop_Variant (Decreases => 1)` proves the check. Co-Authored-By: Codex <noreply@openai.com>
| not Is_Empty and | ||
| (if Is_Full'Old then The_Stack = The_Stack'Old else Peek = E); | ||
| (if Is_Full'Old then | ||
| Element_Array'(The_Stack) = Element_Array'(The_Stack)'Old |
There was a problem hiding this comment.
why do you need to change that?
There was a problem hiding this comment.
Short answer: because of a compiler crash. Here's the full report:
GNAT 16 and the state abstraction example
Without the change, both GNAT 16 and GNATprove 16 crashed on the original postcondition. They failed with internal errors instead of reporting the intended error in the example.
The original expression was:
The_Stack = The_Stack'OldThat is deliberately invalid: The_Stack is a state abstraction and cannot be used as a value in an expression. With the original source and version 16.1.0-1, the saved tests produced:
-
GNAT: an internal compiler error:
GNAT BUG DETECTED GCC error: in gnat_to_gnu_entity, at ada/gcc-interface/decl.cc:4492 -
GNATprove: an internal exception during generation of Global contracts:
GNAT BUG DETECTED Program_Error spark_util-types.adb:2367 explicit raise
The change in the PR adds explicit type qualifications:
Element_Array'(The_Stack) = Element_Array'(The_Stack)'OldThis avoids the crashes. Both tools then report ordinary errors at the two uses of The_Stack:
error: expected type "Element_Array" defined at line 8
error: found package or procedure name
So the change is a workaround for a compiler bug that preserves the example's intentional error. It allows us to use GNAT 16 while retaining the lesson described in the surrounding text.
We also checked qualifying only one operand: that avoided the crashes too, but introduced additional, distracting errors about incompatible types in the conditional expression. Qualifying both operands keeps the diagnostics focused on the invalid uses of The_Stack.
There was a problem hiding this comment.
Did you report the bug?
Add `pragma Loop_Variant (Decreases => 1)` to the loop and remove `ada-expect-prove-error` now that GNATprove proves termination. Explain in one sentence that a constant variant rules out a second iteration. Validated all 10 code blocks in the syntactic guarantees chapter with GNAT/GNATprove 16 and the course's 80-column limit. Co-Authored-By: Codex <noreply@openai.com>
Enable compilation and flow analysis with the default toolchain for
the semicolon and abstract-state examples.
Qualify the invalid abstract-state operands with
Element_ArraysoGNAT and GNATprove report the intended errors instead of crashing.
Keep the semicolon source unchanged and add a short note explaining
its unproved termination check and the
Loop_Variantthat resolves it.Remove unused GNAT 12 and 14 and GNATprove 12 from the installation
list. Retain GNAT/GNATprove 15 and GPRbuild 25 for the two unchanged
ring-buffer examples: version 16 misses the ghost-use errors they
demonstrate.
Validation:
explicit content pin is covered by the configured versions.
Co-Authored-By: Codex noreply@openai.com