Re: SPARK - runtime checks question

[Maciej Sobczak <see.my.homepage@gmail.com>]

On 19 Cze, 18:04, Rod Chapman <roderick.chap...@googlemail.com> wrote:

> The Examiner, by default, doesn't know the values of Natural'First
> and Natural'Last, since these are implementation-defined.
>
> You can supply these values with a configuration file - see
> the Examiner User Manual.  Run the Examiner
> with the -conf switch to re-generate the VCs, then re-simplify.
> I then get 100% of the VCs proved.

Done, it works - thank you. I have used the confgen program form lib/
spark.

Is it considered to be a good practice to always provide the config
file that was generated for the target platform?

BTW - when the config file is provided, spark always reports this:

           Reading target configuration file ...

  10     type Address is private;

---        Note              :  3: The deferred constant Null_Address
has been
           implicitly defined here.

  21     subtype Priority is Any_Priority range  0 ..  62;

---        Note              :  4: The constant Default_Priority, of
type Priority,
           has been implicitly defined here.

[...]

    2 errors or warnings, comprising:
         2 warnings

Is this normal?

--
Maciej Sobczak * www.msobczak.com * www.inspirel.com

Database Access Library for Ada: www.inspirel.com/soci-ada