Warning and Error in GNATprove

[mgudemann]

When I open the project in GPS 5.1.1 I get the following warning:

default.gpr:1:9 warning: object directory "obj/" not found

when trying to execute "Prove All" or "Prove Root Project" I get the following error message with gnatprove (version "2012 (20120509)")

gnatprove -P/users/gudemann.home/tmp/model/tmp/model/GNATprove-MERCE/default.gpr --mode=prove --ide-progress-bar
Phase 1 of 3: frame condition computation ...
Phase 2 of 3: translation to intermediate language ...
+===========================GNAT BUG DETECTED==============================+
| GPL 2012 (20120509) (i686-pc-linux-gnu) Program_Error gnat2why-decls.adb:626 explicit raise|
| Error detected at a-chtgbk.adb:30:1 [a-cfhama.adb:83:4 [com_map.ads:31:4]]|
| Please submit a bug report by email to report@adacore.com.               |
| GAP members can alternatively use GNAT Tracker:                          |
| http://www.adacore.com/ section 'send a report'.                         |
| See gnatinfo.txt for full info on procedure for submitting bugs.         |
| 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 gcc or gnatmake command that you entered.              |
| Also include sources listed below in gnatchop format                     |
| (concatenated together with no headers between files).                   |
| Use plain ASCII or MIME attachment.                                      |
+==========================================================================+

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).

/users/gudemann.home/tmp/model/tmp/model/GNATprove-MERCE/src/com_map.ads
/users/gudemann.home/tmp/model/tmp/model/GNATprove-MERCE/obj/gnatprove/GNAT-TEMP-000001.TMP
/users/gudemann.home/tmp/model/tmp/model/GNATprove-MERCE/src/data_types.ads

compilation abandoned

   compilation of com_map.ads failed

gprbuild: *** compilation phase failed
gnatprove: error during translation to intermediate language, aborting.

How can I proceed? Dows the error depend on the first warning?

[MERCEmentre]

Hello Matthias,

Thanks for the report.

I am using the same release of gnat tools. I can reproduce the issue (and I have the same warning). In fact, it is the proof of com_map.ads that fails.

If I am correct, Ada.Containers.Formal_HashedMaps is badly supported in current GPL release of GNATprove. That should improve in next release with official support of all Containers.Formal*.

You can try "Prove File" on all other files except com_map.ads.

Sorry for the poor current state of the model, it badly needs some attention.

Regards, d.

[MERCEmentre]

As a follow-up, Yannick Moy proposed a modification of the model that uses array instead of hash map, that should solve the issue. I need to work on it.

[mgudemann]

Hi David,

thank you for your quick answer. Using gnatprove on the individual files works without problems.

best regards Matthias

[MERCEmentre]

The issue will be fixed in next release of the model.