Re: Problems with SPARK 2015 and XMLAda

[Serge Robyns <serge.robyns@gmail.com>]

Hi Simon,

Manually editing the grp file as suggested did the trick.

Sadly I quickly abandoned SPARK as it barked on me for using bounded strings.  I intend to use a DB with my application and bounded strings seems to be the way to go, even if I do find them a pain to use.  For every type of string I've to instantiate the generic package as I want to have strong typing on the usage of these strings throughout the program and this is one of my drivers to use Ada.

And I know many other things SPARK doesn't like, like exceptions (not used (yet)) or access types.  So I guess it must dislike the standard containers too.

I guess I'll uninstall SPARK, as so far it hasn't been so helpful for me.
For example in another small toy (a little game) I'm using the following construct.

      Count1      : Natural range 0 .. Number_Of_Columns;
      Count2      : Natural range 0 .. Number_Of_Columns;
      The_Score   : Integer := 0;
      J           : Columns;

      --  To speed up, the value is calculated as a delta
      --  from the previous value.
      --  This is the less good code of this game (I'm not proud).
   begin
      --
      --  Horizontal
      --
      Count1 := 0;
      if Column > Columns'First then
         for J in reverse Columns'First .. Columns'Pred (Column)
         loop
            exit when The_Board.Board (Row, J) /= Player;
            Count1 := Count1 + 1;
            pragma Loop_Invariant ( Count1 <= Number_Of_Columns - Integer (Columns'First - Columns'Pred (Column)));
            pragma Loop_Variant ( Increases => Count1 );
            pragma Loop_Variant ( Decreases => J );
         end loop;
      end if;
      Count2 := 0;
      if Column < Columns'Last then
      for J in Columns'Succ (Column) .. Columns'Last
      loop
         exit when The_Board.Board (Row, J) /= Player;
         Count2 := Count2 + 1;
         pragma Loop_Invariant ( Count2 < Number_Of_Columns );
         pragma Loop_Variant ( Increases => Count2 );
         pragma Loop_Variant ( Increases => J );
      end loop;
   end if;

SPARK warns about potential range errors on Count1 and Count2 while I've put a lot of safeguards and tried two different Loop_Invariant constructs to tell SPARK to be happy.  For every construct attempt I get a different error.

I'm not going to waste my time fighting SPARK and put my trust in the standard ADA features and testing.  To bad not being able to proof.

Serge