SPARK and Interfaces.C

SPARK and Interfaces.C

[ich_bin_elvis]

Hi,

Im trying to spark a program that uses Interfaces.C and
Ada.Numerics.Elementary_Functions; I read in John Barnes book that
there is a method callded shadowing that allows you to use these
packages. I understand that you create a dummy package and uses this
with the spark examiner. But i get an error when i try to examin the
dummy package. Does anybody have any good examples how this is done??
any article regarding multilanguage development and spark would be
apriciated.

Regrads
Ronny

Re: SPARK and Interfaces.C

[JP Thornley]

In article <1116005688.002279.128010@g43g2000cwa.googlegroups.com>,
ich_bin_elvis@hotmail.com writes
>Hi,
>
>Im trying to spark a program that uses Interfaces.C and
>Ada.Numerics.Elementary_Functions; I read in John Barnes book that
>there is a method callded shadowing that allows you to use these
>packages. I understand that you create a dummy package and uses this
>with the spark examiner. But i get an error when i try to examin the
>dummy package. Does anybody have any good examples how this is done??
>any article regarding multilanguage development and spark would be
>apriciated.
>
>Regrads
>Ronny
>

What errors are you getting? The following packages (based on the
examples in John's book) go through the Examiner without any errors.

(You have to add a couple of parent packages that aren't there at
present.)

Cheers,

Phil Thornley

-------------------------------------------------
package Interfaces is

end Interfaces;


package Interfaces.C is

   UCHAR_MAX : constant := 255;

   type unsigned_char is mod (UCHAR_MAX+1);

end Interfaces.C;






package Ada.Numerics is

end Ada.Numerics;



package Ada.Numerics.Elementary_Functions is

   function Sqrt(X : Float) return Float;
   function Log(X : Float) return Float;
   function Cos(X : Float) return Float;

end Ada.Numerics.Elementary_Functions;

-----------------------------------------------------



-- 
JP Thornley

Re: SPARK and Interfaces.C

[Rod Chapman]

You'll also need to supply entries for these units in your Examiner
Index file, of course.  For example:

Interfaces specification is in interfaces.ads
Interfaces.C specification is in interfaces-c.ads
Ada.Numerics specification is in ada-numerics.ads
Ada.Numerics.Elementary_Functions specification is in
ada-numerics-elementary_functions.ads

assuming you're using the GNAT file-naming convention.

You _don't_ need to supply an index file entry for package Ada, since
this
is internally synthesized by the Examiner.
 - Rod Chapman, SPARK Team

Re: SPARK and Interfaces.C

[Martin Dowie]

Rod Chapman wrote:
> You'll also need to supply entries for these units in your Examiner
> Index file, of course.  For example:
> 
> Interfaces specification is in interfaces.ads
> Interfaces.C specification is in interfaces-c.ads
> Ada.Numerics specification is in ada-numerics.ads
> Ada.Numerics.Elementary_Functions specification is in
> ada-numerics-elementary_functions.ads
> 
> assuming you're using the GNAT file-naming convention.
> 
> You _don't_ need to supply an index file entry for package Ada, since
> this is internally synthesized by the Examiner.

Don't know if the SPARK Examiner cares but the GNAT file-naming 
convention is slightly different for the predefined units, e.g.

Interfaces                        => interfac.ads
Interfaces.C                      => i-c.ads
Ada.Numerics                      => a-numeri.ads
Ada.Numerics.Elementary_Functions => a-nuelfu.ads

Just in case... presumably they still need to support 'old fashioned' 
8.3 filenames on some environments.

Cheers

-- Martin

Re: SPARK and Interfaces.C

[Rod Chapman]

Yes...but the whole point of shadows in SPARK is that you _don't_
want the Examiner to read in the compiler's standard specifications
of these packages, since they aren't legal SPARK!
 - Rod

Re: SPARK and Interfaces.C

[ich_bin_elvis]

Now I've made the index file as described above. I also made all the
files interfaces.ads, interfaces-c.ads etc and made empty package
spesifications on the parent packages. I run the spark command

spark /i=adadll.idx
adadll.ads,interfaces.ads,interfaces-c.ads,ada-numerics.ads,ada-numerics-elementary_functions.ads


and I get the message.

                       DATE : 17-MAY-2005 12:48:54.31


   3  WITH Interfaces.C;
      ^
***        Syntax Error      : No complete DOTTED_SIMPLE_NAME can be
followe
           by ANNOTATION_END here.

           Generating listing file ADADLL.LST ...

           Examining the specification of package Interfaces ...

           Generating listing file INTERFACES.LST ...

           Examining the specification of package C ...

           Generating listing file INTERFACES-C.LST ...

           Examining the specification of package Numerics ...

           Generating listing file ADA-NUMERICS.LST ...

           Examining the specification of package Elementary_Functions
...

           Generating listing file
ADA-NUMERICS-ELEMENTARY_FUNCTIONS.LST ...

           Generating report file ...


-----------End of SPARK Examination--------------------------------

The start of the Adadll.ads file looks like this:

with Ada.Numerics.Elementary_Functions;
with Interfaces.C;
with Win32;
use type Win32.Bool;

package body Adadll is
...

What am I doing wrong??

Re: SPARK and Interfaces.C

[Rod Chapman]

1) When you give an indedx file you shouldn't have to specify all the
other files on the command-line - that's the whole idea!  just try
   spark /i=adadll adadll.ads
and let the Examiner sort out all the dependencies for you.

2) Why do you have a package body in a file ending in ".ads" - this
looks wrong.

3) Does this package have an "inherit" annotation?  If so, then it must
be a package specification not a body!

4) Are you seriously planning on shadowing the Win32 package for use
within SPARK? This could be very hard indeed.

- Rod, SPARK Team

Re: SPARK and Interfaces.C

[ich_bin_elvis]

Thanx, Sorry I posted in the adb fil heading.
Isn'nt there always the possibility to just shadow the things you use
from the win32 package? or I can hide the Dllmain function in the adb
file??? The only thing I use from the Win32 package is use type
Win32.Bool;

Re: SPARK and Interfaces.C

[ich_bin_elvis]

I've come a little further  all the packages is examined except the
system package.

type Address is private;

gives the error
           Examining the specification of package System ...

  16  end System;
          ^
***        Semantic Error    : 27: The private type Address does not
have an
           associated full definition.
          ^
---        Warning           :394: Variables of type Address cannot be
initialized
           using the facilities of this package.

How can one declare this one??

regards
Ronny

Re: SPARK and Interfaces.C

[Rod Chapman]

Either
a) Supply a hidden private part in your shadow.  e.g.
  ...
  private
      -# hide System;
  end System;

or

b) Give the specifications of packages Standardm and System in the
Examiner's configuration file. This is the preferred method - see page
196-7 of the SPARK book.

As for Win32 - yes - you only have to shadow the delcarations that you
actually need - in this case just type Bool.

 - Rod

Re: SPARK and Interfaces.C

[ich_bin_elvis]

Thanks got the sytem shadow to work when i used the hide an, with
configuration file i still got an error.

   4  type double is new Standard.Long_Float;
                                            ^
***        Syntax Error      : reserved word "WITH" expected.

   6  type int is new Integer;
                             ^
***        Syntax Error      : reserved word "WITH" expected.

           Examining the specification of package Adadll ...

The spesification file looks like this

package interfaces.C is

type double is new Standard.Long_Float;
type unsigned_long  is mod 2 ** long'Size;
type int is new Integer;

end interfaces.C;

and the Adadll.ads file looks like this, this one gets several errors
like this
  11     subtype BOOL      is Interfaces.C.int;
                              ^
***        Semantic Error    :754: The identifier Interfaces is either
undeclared
           or not visible at this point. This package must be both
inherited
           and withed to be visible here.


----
with System;
WITH Interfaces.C;
--#inherit System,Interfaces.C;

package Adadll is

   ------------------------------
   --  Win32 Type Definitions  --
   ------------------------------

   subtype BOOL      is Interfaces.C.int;
   subtype ULONG     is Interfaces.C.unsigned_long;
   subtype LPVOID    is System.Address;
   subtype HINSTANCE is System.Address;

   --------------------------
   --  DLL Initialization  --
   --------------------------

   function DllMain (hInst    : HINSTANCE;
                     Reason   : ULONG;
                     Reserved : LPVOID) return BOOL;
   --  DLL management

   -------------------
   --  Subprograms  --
   -------------------

   procedure Check_Buffer(Vrtemp,Vltemp : in out Interfaces.C.Double );
   procedure Calcnewposandcourse (T,Vr,Vl,Oldfi, width : in
Interfaces.C.Double;
      X,Y,Fi    : in out Interfaces.C.Double  );
    procedure Stopdrone(vr,vl : in out Interfaces.C.Double);

   function Angle(X1, Y1, X2, Y2 : in Interfaces.C.Double) return
Interfaces.C.Double;
   function Distance(X1, Y1, X2, Y2 : in Interfaces.C.Double) return
Interfaces.C.Double;



private

   -----------------
   --  Constants  --
   -----------------

   True_BOOL : constant BOOL := 1;
   --  win32 BOOL 'True' value

   DLL_PROCESS_DETACH : constant ULONG := 0;
   DLL_PROCESS_ATTACH : constant ULONG := 1;
   --  reasons for calling DllMain

   ---------------------------
   --  Export Declarations  --
   ---------------------------

   pragma Export (StdCall, DllMain, "DllMain");
   --DllMain always uses the StdCall convention
   --pragma Export(C, Distance, "Distance");
   pragma Export (Convention => C, Entity => Distance, External_Name =>
"Distance");

   --pragma Export(C, Angle, "Angle");
   pragma Export (Convention => C, Entity => Angle, External_Name =>
"Angle");

   --pragma Export (C, Checkbuffer,    "CheckBuffer");
   pragma Export (Convention => C, Entity => Check_Buffer,
External_Name => "CheckBuffer");

--pragma Export (C, Calcnewposandcourse,    "Calcnewposandcourse");
   pragma Export (Convention => C, Entity => Calcnewposandcourse,
External_Name => "Calcnewposandcourse");

   --pragma Export (C, Stopdrone,    "Stopdrone");
   pragma Export (Convention => C, Entity => Stopdrone, External_Name
=> "Stopdrone");

    ---------------------------
   --  Import Declarations  --
   ---------------------------

   procedure AdaInit;
   pragma Import (C, AdaInit, "adainit");
   --  initialize Ada runtime library

   procedure AdaFinal;
   pragma Import (C, AdaFinal, "adafinal");
   --  finalize Ada runtime library

end Adadll;

Re: SPARK and Interfaces.C

[JP Thornley]

In article <1116498302.651121.297610@g49g2000cwa.googlegroups.com>,
ich_bin_elvis@hotmail.com writes
>Thanks got the sytem shadow to work when i used the hide an, with
>configuration file i still got an error.
>
>   4  type double is new Standard.Long_Float;
>                                            ^
>***        Syntax Error      : reserved word "WITH" expected.
>
>   6  type int is new Integer;
>                             ^
>***        Syntax Error      : reserved word "WITH" expected.
>
>           Examining the specification of package Adadll ...

That's because non-tagged derived types aren't in SPARK.

The obvious change is to change them to renaming subtype definitions:

   subtype double is Standard.Long_Float;

   subtype int is Integer;

which might trigger some "unnecessary type conversion" warnings, but you
can ignore these.

>
>The spesification file looks like this
>
>package interfaces.C is
>
>type double is new Standard.Long_Float;
>type unsigned_long  is mod 2 ** long'Size;
>type int is new Integer;
>
>end interfaces.C;
>
>and the Adadll.ads file looks like this, this one gets several errors
>like this
>  11     subtype BOOL      is Interfaces.C.int;
>                              ^
>***        Semantic Error    :754: The identifier Interfaces is either
>undeclared
>           or not visible at this point. This package must be both
>inherited
>           and withed to be visible here.
This is probably a result of the semantic errors in the specification.
Once you've got rid of those then this one will probably go away as
well.

Cheers,

Phil
-- 
JP Thornley

Re: SPARK and Interfaces.C

[ich_bin_elvis]

Now I have sparked the adadll.ads spesifcation file with the use of
interfaces.C.
Ada have moved on to Adadll.adb  this one uses the elementary
functions. and I have added. ada.numerics.elementary_functions; on the
inherit clause in the ads file. when I try to spark then I get an error
when I try to spark the ads file again.


           Examining the specification of package Elementary_Functions
...

   1  package Ada.Numerics.Elementary_Functions is
                  ^
***        Semantic Error    :  1: The identifier Numerics is either
undeclared
or
           not visible at this point.

           Examining the specification of package Adadll ...

   4  --#inherit System, Interfaces.C,
Ada.Numerics.Elementary_Functions;
                                           ^
***        Semantic Error    :  1: The identifier Numerics is either
undeclared
or
           not visible at this point.

 130  end Adadll;

---        Warning           : 10: The private part of package Adadll
is hidden
-
           hidden text is ignored by the SPARK Examiner.

           Generating listing file ADADLL.LST ...

           Generating report file ...

Ive added

Ada.Numerics specification is in ada-numerics.ads
Ada.Numerics.Elementary_Functions specification is in
ada-numerics-elementary_functions.ads

in my Index file where ada-numerics.ads is an empty

package ada.numerics is
end package;

Ada.numerics.elementarty_functions contains all the functions I use
like Cos,Sin and Atan.

could some one help me please?

Re: SPARK and Interfaces.C

[JP Thornley]

In article <1116841716.694148.260010@g43g2000cwa.googlegroups.com>, 
ich_bin_elvis@hotmail.com writes
>           Examining the specification of package Elementary_Functions
>...
>
>   1  package Ada.Numerics.Elementary_Functions is
>                  ^
>***        Semantic Error    :  1: The identifier Numerics is either
>undeclared
>or
>           not visible at this point.

One of the more unexpected rules in SPARK is that a child package has to 
explicitly inherit its parent (although no with clause is required).

Add
--# inherit Ada.Numerics;
to the Elementary_Functions child and you should be OK.

Cheers,

Phil

-- 
JP Thornley

Re: SPARK and Interfaces.C

[JP Thornley]

In article <jzj4YsA$rdkCJw85@diphi.demon.co.uk>, JP Thornley 
<jpt@diphi.demon.co.uk> writes
>One of the more unexpected rules in SPARK is that a child package has 
>to explicitly inherit its parent (although no with clause is required).
>
>Add
>--# inherit Ada.Numerics;
>to the Elementary_Functions child and you should be OK.
(Sorry about following up my own post...) but I've just realised that if 
both specifications are in the same file then that will pass the 
Examiner without an inherit clause.

I don't know whether this is intended behaviour, or an undocumented 
feature ;-)

Cheers,

Phil
-- 
JP Thornley

Re: SPARK and Interfaces.C

[ich_bin_elvis]

Got all the shadows to work now, I hided the DLLmain in procedure since
this one had some types that I had difficulties to get thru the
examiner. but now im left with an proofing annaion I don't know how to
work around.
Ads file:

function Distance (
         X1,
         Y1,
         X2,
      Y2 : in     Float)
      return Float;
      --# return Ada.Numerics.Elementary_Functions.Sqrt(((X2 - X1)
**2),((Y2-Y1)**2));

If i understand the error right it only wan't to parameters an now i
have to many paranteces, but how do I make an temporary value I can use
insead of the expressions I have.

Regards
Ronny

Re: SPARK and Interfaces.C

[JP Thornley]

In article <1116925072.146066.235050@g49g2000cwa.googlegroups.com>, 
ich_bin_elvis@hotmail.com writes
>      --# return Ada.Numerics.Elementary_Functions.Sqrt(((X2 - X1)
>**2),((Y2-Y1)**2));
>
>If i understand the error right it only wan't to parameters an now i
>have to many paranteces, but how do I make an temporary value I can use
>insead of the expressions I have.
Well, you've put two parameters in for a function that usually only has 
one.

Perhaps that comma should be a '+'?

Cheers

Phil
-- 
JP Thornley

Re: SPARK and Interfaces.C

[ich_bin_elvis]

You were corret about the above my fault so thanks for seeing that. One
more question and I hope this is the last for my concern for awhile.
Pragma Import is it okay to use that or is it best to use --#hide

procedure AdaInit;
   pragma Import (C, AdaInit, "adainit");
   --  initialize Ada runtime library

   procedure AdaFinal;
   pragma Import (C, AdaFinal, "adafinal");
   --  finalize Ada runtime library

adainit and adafinal is not in the adb file since those are imported so
I get an error. what is done in the real world concerning pragma
imports?? pragma export is ingored by the examiner but this is not the
case for ada import

Ronny

Re: SPARK and Interfaces.C

[JP Thornley]

In article <1116966852.991519.250200@g43g2000cwa.googlegroups.com>, 
ich_bin_elvis@hotmail.com writes
>You were corret about the above my fault so thanks for seeing that. One
>more question and I hope this is the last for my concern for awhile.
>Pragma Import is it okay to use that or is it best to use --#hide
>
>procedure AdaInit;
>   pragma Import (C, AdaInit, "adainit");
>   --  initialize Ada runtime library
>
>   procedure AdaFinal;
>   pragma Import (C, AdaFinal, "adafinal");
>   --  finalize Ada runtime library
>
>adainit and adafinal is not in the adb file since those are imported so
>I get an error. what is done in the real world concerning pragma
>imports?? pragma export is ingored by the examiner but this is not the
>case for ada import
I don't think that there is a universal best answer for this sort of 
question - it all depends on what level of confidence you require for 
the software and how you can get that confidence at minimum cost.

Clearly you are developing a system with some non-SPARK components, and 
so you need to think about how you are going to get the same level of 
confidence in that software as you are getting with the SPARK 
components. You need to identify the SPARK boundary - i.e. what parts of 
the system will be SPARK, and analysable by the tools and what parts 
will be non-SPARK and so require analysis by other means.

You should define the SPARK boundary so that you get the maximum 
confidence in the complete system for the effort that you have available 
(which isn't always achieved by getting as much as possible into SPARK.)

So the answer is to look at the options and pick the one that suits your 
situation.

Cheers,

Phil
-- 
JP Thornley