Found a bug with GNATProve/Spark when using protected objects

General
1

I was able to us AI to get a reproducible version of it, you can check it out here: GitHub - ValorZard/spark_po_pointer_repro · GitHub

full crash:


PS C:\ada-stuff\spark_po_pointer_repro> alr exec -- gnatprove -P spark_po_pointer_repro.gpr --mode=check_all
Phase 1 of 3: generation of data representation information ...
Phase 2 of 3: generation of Global contracts ...
+===========================GNAT BUG DETECTED==============================+
| 1.0 (spark) Program_Error spark_util-types.adb:2188 explicit raise       |
| Error detected at po.ads:18:26                                           |
| Compiling C:\ada-stuff\spark_po_pointer_repro\src\spark_po_pointer_repro.adb|
| Please submit a bug report; see 
 .              |
| Use a subject line meaningful to you and us to track the bug.            |
| Include the entire contents of this bug box in the report.               |
| Include the exact command that you entered.                              |
| Also include sources listed below.                                       |
+==========================================================================+

Please include these source files with error report
Note that list may not be accurate in some cases,
so please double check that the problem can still
be reproduced with the set of files listed.
Consider also -gnatd.n switch (see debug.adb).

C:\ada-stuff\spark_po_pointer_repro\src\spark_po_pointer_repro.adb
C:\ada-stuff\spark_po_pointer_repro\src\po.ads

compilation abandoned
gnatprove: error during generation of Global contracts
ERROR: Command ["gnatprove", "-P", "spark_po_pointer_repro.gpr", "--mode=check_all"] exited with code 1
2

This would be the place to report it, assuming it’s not fixed upstream: GitHub - AdaCore/spark2014: SPARK 2014 is the new version of SPARK, a software development technology specifically designed for engineering high-reliability applications. · GitHub

As an aside, I can’t understand how anyone can tolerate using Anthropic models and/or Claude Code when they write so much useless garbage in every comment and the readme.

3

I have just tested it with v16 (I just changed the version in alire.toml) and it does work

alr gnatprove
ⓘ Synchronizing workspace...
Dependencies automatically updated as follows:                           

   ⭧📦 gnatprove 16.1.0 (upgraded from 15.1.0,binary)
ⓘ Deploying gnatprove=16.1.0...
################################################################################################################################################################ 100.0%
                                                                                      
Phase 1 of 3: generation of data representation information ...
Phase 2 of 3: generation of Global contracts ...
Phase 3 of 3: flow analysis and proof ...
 warning: "X" is set by "Take" but not used after the call
--> spark_po_pointer_repro.adb:10:20
   10 |       Po.Buffer.Take (X);
      |                       ^
 medium: pointer dereference check might fail
--> po.adb:7:23
    7 |             V     := Head.Value;
      |                      ~~~~^
      + provers gave up before completing the proof

 medium: resource or memory leak might occur
--> po.adb:8:16
    8 |             Head  := Head.Next;
      |             ~~~~~~^~~~~~~~~~~~
      + provers gave up before completing the proof

 medium: pointer dereference check might fail
--> po.adb:8:23
    8 |             Head  := Head.Next;
      |                      ~~~~^
      + provers gave up before completing the proof
Summary logged in /home/fernando/Dirt/spark_po_pointer_repro/obj/development/gnatprove/gnatprove.out

I hope this helps. Best regards,
Fer

4

Yeah I agree the README is pretty much junk. I just felt lazy and didn’t feel like cleaning it up and rewriting it.

Thats a failure on my part though, thanks for reminding me I should have higher standards for myself

5

Huh, I wonder what changed in 16 that let it work