search

AdaCore / spark2014

SPARK 2014 is the new version of SPARK, a software development technology specifically designed for engineering high-reliability applications.
GNU General Public License v3.0
249 stars 33 forks source link

gnatprove fails with gnatcoll as dependency in alire #48

Closed vbramselaar closed 2 months ago

vbramselaar commented 2 months ago

When creating a basic project with gnatcoll as dependency gnatprove fails. The error comes from gpr-err-scanner.adb it looks like. I reported the issue here because that was said here: https://github.com/AdaCore/gprbuild/issues/150.

Issue

Phase 1 of 3: generation of data representation information ...
Phase 2 of 3: generation of Global contracts ...

gpr-err-scanner.adb:2421:15: error: choice given in case statement is not static
 2421 |         when Name_Abort =>
      |              ^~~~~~~~~~

gpr-err-scanner.adb:2421:15: error: "Name_Abort" is not a static constant (RM 4.9(5))
 2421 |         when Name_Abort =>
      |              ^~~~~~~~~~

gpr-err-scanner.adb:2423:15: error: choice given in case statement is not static
 2423 |         when Name_Abs =>
      |              ^~~~~~~~

gpr-err-scanner.adb:2423:15: error: "Name_Abs" is not a static constant (RM 4.9(5))
 2423 |         when Name_Abs =>
      |              ^~~~~~~~

gpr-err-scanner.adb:2425:15: error: choice given in case statement is not static
 2425 |         when Name_Accept =>
      |              ^~~~~~~~~~~

gpr-err-scanner.adb:2425:15: error: "Name_Accept" is not a static constant (RM 4.9(5))
 2425 |         when Name_Accept =>
      |              ^~~~~~~~~~~

gpr-err-scanner.adb:2427:15: error: choice given in case statement is not static
 2427 |         when Name_And =>
      |              ^~~~~~~~

gpr-err-scanner.adb:2427:15: error: "Name_And" is not a static constant (RM 4.9(5))
 2427 |         when Name_And =>
      |              ^~~~~~~~

gpr-err-scanner.adb:2429:15: error: choice given in case statement is not static
 2429 |         when Name_All =>
      |              ^~~~~~~~

gpr-err-scanner.adb:2429:15: error: "Name_All" is not a static constant (RM 4.9(5))
 2429 |         when Name_All =>
      |              ^~~~~~~~

gpr-err-scanner.adb:2431:15: error: choice given in case statement is not static
 2431 |         when Name_Array =>
      |              ^~~~~~~~~~

gpr-err-scanner.adb:2431:15: error: "Name_Array" is not a static constant (RM 4.9(5))
 2431 |         when Name_Array =>
      |              ^~~~~~~~~~

gpr-err-scanner.adb:2433:15: error: choice given in case statement is not static
 2433 |         when Name_At =>
      |              ^~~~~~~

gpr-err-scanner.adb:2433:15: error: "Name_At" is not a static constant (RM 4.9(5))
 2433 |         when Name_At =>
      |              ^~~~~~~

gpr-err-scanner.adb:2435:15: error: choice given in case statement is not static
 2435 |         when Name_Begin =>
      |              ^~~~~~~~~~

gpr-err-scanner.adb:2435:15: error: "Name_Begin" is not a static constant (RM 4.9(5))
 2435 |         when Name_Begin =>
      |              ^~~~~~~~~~

gpr-err-scanner.adb:2437:15: error: choice given in case statement is not static
 2437 |         when Name_Body =>
      |              ^~~~~~~~~

gpr-err-scanner.adb:2437:15: error: "Name_Body" is not a static constant (RM 4.9(5))
 2437 |         when Name_Body =>
      |              ^~~~~~~~~

gpr-err-scanner.adb:2439:15: error: choice given in case statement is not static
 2439 |         when Name_Case =>
      |              ^~~~~~~~~

gpr-err-scanner.adb:2439:15: error: "Name_Case" is not a static constant (RM 4.9(5))
 2439 |         when Name_Case =>
      |              ^~~~~~~~~

gpr-err-scanner.adb:2441:15: error: choice given in case statement is not static
 2441 |         when Name_Constant =>
      |              ^~~~~~~~~~~~~

gpr-err-scanner.adb:2441:15: error: "Name_Constant" is not a static constant (RM 4.9(5))
 2441 |         when Name_Constant =>
      |              ^~~~~~~~~~~~~

gpr-err-scanner.adb:2443:15: error: choice given in case statement is not static
 2443 |         when Name_Declare =>
      |              ^~~~~~~~~~~~

gpr-err-scanner.adb:2443:15: error: "Name_Declare" is not a static constant (RM 4.9(5))
 2443 |         when Name_Declare =>
      |              ^~~~~~~~~~~~

gpr-err-scanner.adb:2445:15: error: choice given in case statement is not static
 2445 |         when Name_Delay =>
      |              ^~~~~~~~~~

gpr-err-scanner.adb:2445:15: error: "Name_Delay" is not a static constant (RM 4.9(5))
 2445 |         when Name_Delay =>
      |              ^~~~~~~~~~

gpr-err-scanner.adb:2447:15: error: choice given in case statement is not static
 2447 |         when Name_Do =>
      |              ^~~~~~~

gpr-err-scanner.adb:2447:15: error: "Name_Do" is not a static constant (RM 4.9(5))
 2447 |         when Name_Do =>
      |              ^~~~~~~

gpr-err-scanner.adb:2449:15: error: choice given in case statement is not static
 2449 |         when Name_Else =>
      |              ^~~~~~~~~

gpr-err-scanner.adb:2449:15: error: "Name_Else" is not a static constant (RM 4.9(5))
 2449 |         when Name_Else =>
      |              ^~~~~~~~~

gpr-err-scanner.adb:2451:15: error: choice given in case statement is not static
 2451 |         when Name_Elsif =>
      |              ^~~~~~~~~~

gpr-err-scanner.adb:2451:15: error: "Name_Elsif" is not a static constant (RM 4.9(5))
 2451 |         when Name_Elsif =>
      |              ^~~~~~~~~~

gpr-err-scanner.adb:2453:15: error: choice given in case statement is not static
 2453 |         when Name_End =>
      |              ^~~~~~~~

gpr-err-scanner.adb:2453:15: error: "Name_End" is not a static constant (RM 4.9(5))
 2453 |         when Name_End =>
      |              ^~~~~~~~

gpr-err-scanner.adb:2455:15: error: choice given in case statement is not static
 2455 |         when Name_Entry =>
      |              ^~~~~~~~~~

gpr-err-scanner.adb:2455:15: error: "Name_Entry" is not a static constant (RM 4.9(5))
 2455 |         when Name_Entry =>
      |              ^~~~~~~~~~

gpr-err-scanner.adb:2457:15: error: choice given in case statement is not static
 2457 |         when Name_Exception =>
      |              ^~~~~~~~~~~~~~

gpr-err-scanner.adb:2457:15: error: "Name_Exception" is not a static constant (RM 4.9(5))
 2457 |         when Name_Exception =>
      |              ^~~~~~~~~~~~~~

gpr-err-scanner.adb:2459:15: error: choice given in case statement is not static
 2459 |         when Name_Exit =>
      |              ^~~~~~~~~

gpr-err-scanner.adb:2459:15: error: "Name_Exit" is not a static constant (RM 4.9(5))
 2459 |         when Name_Exit =>
      |              ^~~~~~~~~

gpr-err-scanner.adb:2461:15: error: choice given in case statement is not static
 2461 |         when Name_For =>
      |              ^~~~~~~~

gpr-err-scanner.adb:2461:15: error: "Name_For" is not a static constant (RM 4.9(5))
 2461 |         when Name_For =>
      |              ^~~~~~~~

gpr-err-scanner.adb:2463:15: error: choice given in case statement is not static
 2463 |         when Name_Function =>
      |              ^~~~~~~~~~~~~

gpr-err-scanner.adb:2463:15: error: "Name_Function" is not a static constant (RM 4.9(5))
 2463 |         when Name_Function =>
      |              ^~~~~~~~~~~~~

gpr-err-scanner.adb:2465:15: error: choice given in case statement is not static
 2465 |         when Name_Generic =>
      |              ^~~~~~~~~~~~

gpr-err-scanner.adb:2465:15: error: "Name_Generic" is not a static constant (RM 4.9(5))
 2465 |         when Name_Generic =>
      |              ^~~~~~~~~~~~

gpr-err-scanner.adb:2467:15: error: choice given in case statement is not static
 2467 |         when Name_Goto =>
      |              ^~~~~~~~~

gpr-err-scanner.adb:2467:15: error: "Name_Goto" is not a static constant (RM 4.9(5))
 2467 |         when Name_Goto =>
      |              ^~~~~~~~~

gpr-err-scanner.adb:2469:15: error: choice given in case statement is not static
 2469 |         when Name_If =>
      |              ^~~~~~~

gpr-err-scanner.adb:2469:15: error: "Name_If" is not a static constant (RM 4.9(5))
 2469 |         when Name_If =>
      |              ^~~~~~~

gpr-err-scanner.adb:2471:15: error: choice given in case statement is not static
 2471 |         when Name_In =>
      |              ^~~~~~~

gpr-err-scanner.adb:2471:15: error: "Name_In" is not a static constant (RM 4.9(5))
 2471 |         when Name_In =>
      |              ^~~~~~~

gpr-err-scanner.adb:2473:15: error: choice given in case statement is not static
 2473 |         when Name_Is =>
      |              ^~~~~~~

gpr-err-scanner.adb:2473:15: error: "Name_Is" is not a static constant (RM 4.9(5))
 2473 |         when Name_Is =>
      |              ^~~~~~~

gpr-err-scanner.adb:2475:15: error: choice given in case statement is not static
 2475 |         when Name_Limited =>
      |              ^~~~~~~~~~~~

gpr-err-scanner.adb:2475:15: error: "Name_Limited" is not a static constant (RM 4.9(5))
 2475 |         when Name_Limited =>
      |              ^~~~~~~~~~~~

gpr-err-scanner.adb:2477:15: error: choice given in case statement is not static
 2477 |         when Name_Loop =>
      |              ^~~~~~~~~

gpr-err-scanner.adb:2477:15: error: "Name_Loop" is not a static constant (RM 4.9(5))
 2477 |         when Name_Loop =>
      |              ^~~~~~~~~

gpr-err-scanner.adb:2479:15: error: choice given in case statement is not static
 2479 |         when Name_New =>
      |              ^~~~~~~~

gpr-err-scanner.adb:2479:15: error: "Name_New" is not a static constant (RM 4.9(5))
 2479 |         when Name_New =>
      |              ^~~~~~~~

gpr-err-scanner.adb:2481:15: error: choice given in case statement is not static
 2481 |         when Name_Not =>
      |              ^~~~~~~~

gpr-err-scanner.adb:2481:15: error: "Name_Not" is not a static constant (RM 4.9(5))
 2481 |         when Name_Not =>
      |              ^~~~~~~~

gpr-err-scanner.adb:2483:15: error: choice given in case statement is not static
 2483 |         when Name_Null =>
      |              ^~~~~~~~~

gpr-err-scanner.adb:2483:15: error: "Name_Null" is not a static constant (RM 4.9(5))
 2483 |         when Name_Null =>
      |              ^~~~~~~~~

gpr-err-scanner.adb:2485:15: error: choice given in case statement is not static
 2485 |         when Name_Of =>
      |              ^~~~~~~

gpr-err-scanner.adb:2485:15: error: "Name_Of" is not a static constant (RM 4.9(5))
 2485 |         when Name_Of =>
      |              ^~~~~~~

gpr-err-scanner.adb:2487:15: error: choice given in case statement is not static
 2487 |         when Name_Or =>
      |              ^~~~~~~

gpr-err-scanner.adb:2487:15: error: "Name_Or" is not a static constant (RM 4.9(5))
 2487 |         when Name_Or =>
      |              ^~~~~~~

gpr-err-scanner.adb:2489:15: error: choice given in case statement is not static
 2489 |         when Name_Others =>
      |              ^~~~~~~~~~~

gpr-err-scanner.adb:2489:15: error: "Name_Others" is not a static constant (RM 4.9(5))
 2489 |         when Name_Others =>
      |              ^~~~~~~~~~~

gpr-err-scanner.adb:2491:15: error: choice given in case statement is not static
 2491 |         when Name_Out =>
      |              ^~~~~~~~

gpr-err-scanner.adb:2491:15: error: "Name_Out" is not a static constant (RM 4.9(5))
 2491 |         when Name_Out =>
      |              ^~~~~~~~

gpr-err-scanner.adb:2493:15: error: choice given in case statement is not static
 2493 |         when Name_Package =>
      |              ^~~~~~~~~~~~

gpr-err-scanner.adb:2493:15: error: "Name_Package" is not a static constant (RM 4.9(5))
 2493 |         when Name_Package =>
      |              ^~~~~~~~~~~~

gpr-err-scanner.adb:2495:15: error: choice given in case statement is not static
 2495 |         when Name_Pragma =>
      |              ^~~~~~~~~~~

gpr-err-scanner.adb:2495:15: error: "Name_Pragma" is not a static constant (RM 4.9(5))
 2495 |         when Name_Pragma =>
      |              ^~~~~~~~~~~

gpr-err-scanner.adb:2497:15: error: choice given in case statement is not static
 2497 |         when Name_Private =>
      |              ^~~~~~~~~~~~

gpr-err-scanner.adb:2497:15: error: "Name_Private" is not a static constant (RM 4.9(5))
 2497 |         when Name_Private =>
      |              ^~~~~~~~~~~~

gpr-err-scanner.adb:2499:15: error: choice given in case statement is not static
 2499 |         when Name_Procedure =>
      |              ^~~~~~~~~~~~~~

gpr-err-scanner.adb:2499:15: error: "Name_Procedure" is not a static constant (RM 4.9(5))
 2499 |         when Name_Procedure =>
      |              ^~~~~~~~~~~~~~

gpr-err-scanner.adb:2501:15: error: choice given in case statement is not static
 2501 |         when Name_Raise =>
      |              ^~~~~~~~~~

gpr-err-scanner.adb:2501:15: error: "Name_Raise" is not a static constant (RM 4.9(5))
 2501 |         when Name_Raise =>
      |              ^~~~~~~~~~

gpr-err-scanner.adb:2503:15: error: choice given in case statement is not static
 2503 |         when Name_Record =>
      |              ^~~~~~~~~~~

gpr-err-scanner.adb:2503:15: error: "Name_Record" is not a static constant (RM 4.9(5))
 2503 |         when Name_Record =>
      |              ^~~~~~~~~~~

gpr-err-scanner.adb:2505:15: error: choice given in case statement is not static
 2505 |         when Name_Rem =>
      |              ^~~~~~~~

gpr-err-scanner.adb:2505:15: error: "Name_Rem" is not a static constant (RM 4.9(5))
 2505 |         when Name_Rem =>
      |              ^~~~~~~~

gpr-err-scanner.adb:2507:15: error: choice given in case statement is not static
 2507 |         when Name_Renames =>
      |              ^~~~~~~~~~~~

gpr-err-scanner.adb:2507:15: error: "Name_Renames" is not a static constant (RM 4.9(5))
 2507 |         when Name_Renames =>
      |              ^~~~~~~~~~~~

gpr-err-scanner.adb:2509:15: error: choice given in case statement is not static
 2509 |         when Name_Return =>
      |              ^~~~~~~~~~~

gpr-err-scanner.adb:2509:15: error: "Name_Return" is not a static constant (RM 4.9(5))
 2509 |         when Name_Return =>
      |              ^~~~~~~~~~~

gpr-err-scanner.adb:2511:15: error: choice given in case statement is not static
 2511 |         when Name_Reverse =>
      |              ^~~~~~~~~~~~

gpr-err-scanner.adb:2511:15: error: "Name_Reverse" is not a static constant (RM 4.9(5))
 2511 |         when Name_Reverse =>
      |              ^~~~~~~~~~~~

gpr-err-scanner.adb:2513:15: error: choice given in case statement is not static
 2513 |         when Name_Select =>
      |              ^~~~~~~~~~~

gpr-err-scanner.adb:2513:15: error: "Name_Select" is not a static constant (RM 4.9(5))
 2513 |         when Name_Select =>
      |              ^~~~~~~~~~~

gpr-err-scanner.adb:2515:15: error: choice given in case statement is not static
 2515 |         when Name_Separate =>
      |              ^~~~~~~~~~~~~

gpr-err-scanner.adb:2515:15: error: "Name_Separate" is not a static constant (RM 4.9(5))
 2515 |         when Name_Separate =>
      |              ^~~~~~~~~~~~~

gpr-err-scanner.adb:2517:15: error: choice given in case statement is not static
 2517 |         when Name_Subtype =>
      |              ^~~~~~~~~~~~

gpr-err-scanner.adb:2517:15: error: "Name_Subtype" is not a static constant (RM 4.9(5))
 2517 |         when Name_Subtype =>
      |              ^~~~~~~~~~~~

gpr-err-scanner.adb:2519:15: error: choice given in case statement is not static
 2519 |         when Name_Task =>
      |              ^~~~~~~~~

gpr-err-scanner.adb:2519:15: error: "Name_Task" is not a static constant (RM 4.9(5))
 2519 |         when Name_Task =>
      |              ^~~~~~~~~

gpr-err-scanner.adb:2521:15: error: choice given in case statement is not static
 2521 |         when Name_Terminate =>
      |              ^~~~~~~~~~~~~~

gpr-err-scanner.adb:2521:15: error: "Name_Terminate" is not a static constant (RM 4.9(5))
 2521 |         when Name_Terminate =>
      |              ^~~~~~~~~~~~~~

gpr-err-scanner.adb:2523:15: error: choice given in case statement is not static
 2523 |         when Name_Then =>
      |              ^~~~~~~~~

gpr-err-scanner.adb:2523:15: error: "Name_Then" is not a static constant (RM 4.9(5))
 2523 |         when Name_Then =>
      |              ^~~~~~~~~

gpr-err-scanner.adb:2525:15: error: choice given in case statement is not static
 2525 |         when Name_Type =>
      |              ^~~~~~~~~

gpr-err-scanner.adb:2525:15: error: "Name_Type" is not a static constant (RM 4.9(5))
 2525 |         when Name_Type =>
      |              ^~~~~~~~~

gpr-err-scanner.adb:2527:15: error: choice given in case statement is not static
 2527 |         when Name_Use =>
      |              ^~~~~~~~

gpr-err-scanner.adb:2527:15: error: "Name_Use" is not a static constant (RM 4.9(5))
 2527 |         when Name_Use =>
      |              ^~~~~~~~

gpr-err-scanner.adb:2529:15: error: choice given in case statement is not static
 2529 |         when Name_When =>
      |              ^~~~~~~~~

gpr-err-scanner.adb:2529:15: error: "Name_When" is not a static constant (RM 4.9(5))
 2529 |         when Name_When =>
      |              ^~~~~~~~~

gpr-err-scanner.adb:2531:15: error: choice given in case statement is not static
 2531 |         when Name_With =>
      |              ^~~~~~~~~

gpr-err-scanner.adb:2531:15: error: "Name_With" is not a static constant (RM 4.9(5))
 2531 |         when Name_With =>
      |              ^~~~~~~~~

gpr-err-scanner.adb:2533:15: error: choice given in case statement is not static
 2533 |         when Name_Xor =>
      |              ^~~~~~~~

gpr-err-scanner.adb:2533:15: error: "Name_Xor" is not a static constant (RM 4.9(5))
 2533 |         when Name_Xor =>
      |              ^~~~~~~~

gpr-err-scanner.adb:2535:15: error: choice given in case statement is not static
 2535 |         when Name_Access =>
      |              ^~~~~~~~~~~

gpr-err-scanner.adb:2535:15: error: "Name_Access" is not a static constant (RM 4.9(5))
 2535 |         when Name_Access =>
      |              ^~~~~~~~~~~

gpr-err-scanner.adb:2537:15: error: choice given in case statement is not static
 2537 |         when Name_Delta =>
      |              ^~~~~~~~~~

gpr-err-scanner.adb:2537:15: error: "Name_Delta" is not a static constant (RM 4.9(5))
 2537 |         when Name_Delta =>
      |              ^~~~~~~~~~

gpr-err-scanner.adb:2539:15: error: choice given in case statement is not static
 2539 |         when Name_Digits =>
      |              ^~~~~~~~~~~

gpr-err-scanner.adb:2539:15: error: "Name_Digits" is not a static constant (RM 4.9(5))
 2539 |         when Name_Digits =>
      |              ^~~~~~~~~~~

gpr-err-scanner.adb:2541:15: error: choice given in case statement is not static
 2541 |         when Name_Mod =>
      |              ^~~~~~~~

gpr-err-scanner.adb:2541:15: error: "Name_Mod" is not a static constant (RM 4.9(5))
 2541 |         when Name_Mod =>
      |              ^~~~~~~~

gpr-err-scanner.adb:2543:15: error: choice given in case statement is not static
 2543 |         when Name_Range =>
      |              ^~~~~~~~~~

gpr-err-scanner.adb:2543:15: error: "Name_Range" is not a static constant (RM 4.9(5))
 2543 |         when Name_Range =>
      |              ^~~~~~~~~~

gpr-err-scanner.adb:2545:15: error: choice given in case statement is not static
 2545 |         when Name_Abstract =>
      |              ^~~~~~~~~~~~~

gpr-err-scanner.adb:2545:15: error: "Name_Abstract" is not a static constant (RM 4.9(5))
 2545 |         when Name_Abstract =>
      |              ^~~~~~~~~~~~~

gpr-err-scanner.adb:2547:15: error: choice given in case statement is not static
 2547 |         when Name_Aliased =>
      |              ^~~~~~~~~~~~

gpr-err-scanner.adb:2547:15: error: "Name_Aliased" is not a static constant (RM 4.9(5))
 2547 |         when Name_Aliased =>
      |              ^~~~~~~~~~~~

gpr-err-scanner.adb:2549:15: error: choice given in case statement is not static
 2549 |         when Name_Protected =>
      |              ^~~~~~~~~~~~~~

gpr-err-scanner.adb:2549:15: error: "Name_Protected" is not a static constant (RM 4.9(5))
 2549 |         when Name_Protected =>
      |              ^~~~~~~~~~~~~~

gpr-err-scanner.adb:2551:15: error: choice given in case statement is not static
 2551 |         when Name_Until =>
      |              ^~~~~~~~~~

gpr-err-scanner.adb:2551:15: error: "Name_Until" is not a static constant (RM 4.9(5))
 2551 |         when Name_Until =>
      |              ^~~~~~~~~~

gpr-err-scanner.adb:2553:15: error: choice given in case statement is not static
 2553 |         when Name_Requeue =>
      |              ^~~~~~~~~~~~

gpr-err-scanner.adb:2553:15: error: "Name_Requeue" is not a static constant (RM 4.9(5))
 2553 |         when Name_Requeue =>
      |              ^~~~~~~~~~~~

gpr-err-scanner.adb:2555:15: error: choice given in case statement is not static
 2555 |         when Name_Tagged =>
      |              ^~~~~~~~~~~

gpr-err-scanner.adb:2555:15: error: "Name_Tagged" is not a static constant (RM 4.9(5))
 2555 |         when Name_Tagged =>
      |              ^~~~~~~~~~~

gpr-err-scanner.adb:2557:15: error: choice given in case statement is not static
 2557 |         when Name_Project =>
      |              ^~~~~~~~~~~~

gpr-err-scanner.adb:2557:15: error: "Name_Project" is not a static constant (RM 4.9(5))
 2557 |         when Name_Project =>
      |              ^~~~~~~~~~~~

gpr-err-scanner.adb:2559:15: error: choice given in case statement is not static
 2559 |         when Name_Extends =>
      |              ^~~~~~~~~~~~

gpr-err-scanner.adb:2559:15: error: "Name_Extends" is not a static constant (RM 4.9(5))
 2559 |         when Name_Extends =>
      |              ^~~~~~~~~~~~

gpr-err-scanner.adb:2561:15: error: choice given in case statement is not static
 2561 |         when Name_External =>
      |              ^~~~~~~~~~~~~

gpr-err-scanner.adb:2561:15: error: "Name_External" is not a static constant (RM 4.9(5))
 2561 |         when Name_External =>
      |              ^~~~~~~~~~~~~

gpr-err-scanner.adb:2563:15: error: choice given in case statement is not static
 2563 |         when Name_External_As_List =>
      |              ^~~~~~~~~~~~~~~~~~~~~

gpr-err-scanner.adb:2563:15: error: "Name_External_As_List" is not a static constant (RM 4.9(5))
 2563 |         when Name_External_As_List =>
      |              ^~~~~~~~~~~~~~~~~~~~~

gpr-err-scanner.adb:2565:15: error: choice given in case statement is not static
 2565 |         when Name_Interface =>
      |              ^~~~~~~~~~~~~~

gpr-err-scanner.adb:2565:15: error: "Name_Interface" is not a static constant (RM 4.9(5))
 2565 |         when Name_Interface =>
      |              ^~~~~~~~~~~~~~

gpr-err-scanner.adb:2567:15: error: choice given in case statement is not static
 2567 |         when Name_Overriding =>
      |              ^~~~~~~~~~~~~~~

gpr-err-scanner.adb:2567:15: error: "Name_Overriding" is not a static constant (RM 4.9(5))
 2567 |         when Name_Overriding =>
      |              ^~~~~~~~~~~~~~~

gpr-err-scanner.adb:2569:15: error: choice given in case statement is not static
 2569 |         when Name_Synchronized =>
      |              ^~~~~~~~~~~~~~~~~

gpr-err-scanner.adb:2569:15: error: "Name_Synchronized" is not a static constant (RM 4.9(5))
 2569 |         when Name_Synchronized =>
      |              ^~~~~~~~~~~~~~~~~

gpr-err-scanner.adb:2571:15: error: choice given in case statement is not static
 2571 |         when Name_Some =>
      |              ^~~~~~~~~

gpr-err-scanner.adb:2571:15: error: "Name_Some" is not a static constant (RM 4.9(5))
 2571 |         when Name_Some =>
      |              ^~~~~~~~~
gnatprove: error during generation of Global contracts
error: Command ["gnatprove", "-P", "testcol.gpr"] exited with code 1

Steps to reproduce

alr init --bin test cd test alr with gnatcoll alr with gnatprove alr build alr gnatprove

kanigsson commented 2 months ago

Thanks for reporting the issue here, we are looking into it.

kanigsson commented 2 months ago

Hello,

This seems to be a consequence of how alr and gnatprove are designed. Alire likes to make the entire source tree available, including dependencies, but this means SPARK will analyze it. There is currently no way to avoid this.

Note that the error you saw is a bug and has been fixed in the compiler. It will be available in next year's FSF compiler release.

vbramselaar commented 1 month ago

Alire likes to make the entire source tree available, including dependencies, but this means SPARK will analyze it. There is currently no way to avoid this.

I kinda have one workaround. Where I created another .gpr file which only mentioned the sources of SPARK code I want to verify (it would not really compile or anything). So the main file was from alire and another just for mentioning the spark code and run gnatprove on it.

kanigsson commented 1 month ago

Yes, creating a separate project for analysis is a solution to avoid this issue. Another solution is to use scenario variables in your project to avoid code duplication.