* SPARK and Interfaces.C @ 2005-05-13 17:34 ich_bin_elvis 2005-05-13 19:40 ` JP Thornley 0 siblings, 1 reply; 19+ messages in thread From: ich_bin_elvis @ 2005-05-13 17:34 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: SPARK and Interfaces.C 2005-05-13 17:34 SPARK and Interfaces.C ich_bin_elvis @ 2005-05-13 19:40 ` JP Thornley 2005-05-14 12:15 ` Rod Chapman 0 siblings, 1 reply; 19+ messages in thread From: JP Thornley @ 2005-05-13 19:40 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: SPARK and Interfaces.C 2005-05-13 19:40 ` JP Thornley @ 2005-05-14 12:15 ` Rod Chapman 2005-05-14 13:31 ` Martin Dowie 2005-05-17 10:55 ` ich_bin_elvis 0 siblings, 2 replies; 19+ messages in thread From: Rod Chapman @ 2005-05-14 12:15 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: SPARK and Interfaces.C 2005-05-14 12:15 ` Rod Chapman @ 2005-05-14 13:31 ` Martin Dowie 2005-05-14 15:41 ` Rod Chapman 2005-05-17 10:55 ` ich_bin_elvis 1 sibling, 1 reply; 19+ messages in thread From: Martin Dowie @ 2005-05-14 13:31 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: SPARK and Interfaces.C 2005-05-14 13:31 ` Martin Dowie @ 2005-05-14 15:41 ` Rod Chapman 0 siblings, 0 replies; 19+ messages in thread From: Rod Chapman @ 2005-05-14 15:41 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: SPARK and Interfaces.C 2005-05-14 12:15 ` Rod Chapman 2005-05-14 13:31 ` Martin Dowie @ 2005-05-17 10:55 ` ich_bin_elvis 2005-05-17 14:40 ` Rod Chapman 1 sibling, 1 reply; 19+ messages in thread From: ich_bin_elvis @ 2005-05-17 10:55 UTC (permalink / raw) 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?? ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: SPARK and Interfaces.C 2005-05-17 10:55 ` ich_bin_elvis @ 2005-05-17 14:40 ` Rod Chapman 2005-05-19 8:12 ` ich_bin_elvis 2005-05-19 8:46 ` ich_bin_elvis 0 siblings, 2 replies; 19+ messages in thread From: Rod Chapman @ 2005-05-17 14:40 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: SPARK and Interfaces.C 2005-05-17 14:40 ` Rod Chapman @ 2005-05-19 8:12 ` ich_bin_elvis 2005-05-19 8:46 ` ich_bin_elvis 1 sibling, 0 replies; 19+ messages in thread From: ich_bin_elvis @ 2005-05-19 8:12 UTC (permalink / raw) 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; ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: SPARK and Interfaces.C 2005-05-17 14:40 ` Rod Chapman 2005-05-19 8:12 ` ich_bin_elvis @ 2005-05-19 8:46 ` ich_bin_elvis 2005-05-19 9:01 ` Rod Chapman 1 sibling, 1 reply; 19+ messages in thread From: ich_bin_elvis @ 2005-05-19 8:46 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: SPARK and Interfaces.C 2005-05-19 8:46 ` ich_bin_elvis @ 2005-05-19 9:01 ` Rod Chapman 2005-05-19 10:25 ` ich_bin_elvis 0 siblings, 1 reply; 19+ messages in thread From: Rod Chapman @ 2005-05-19 9:01 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: SPARK and Interfaces.C 2005-05-19 9:01 ` Rod Chapman @ 2005-05-19 10:25 ` ich_bin_elvis 2005-05-21 22:52 ` JP Thornley 0 siblings, 1 reply; 19+ messages in thread From: ich_bin_elvis @ 2005-05-19 10:25 UTC (permalink / raw) 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; ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: SPARK and Interfaces.C 2005-05-19 10:25 ` ich_bin_elvis @ 2005-05-21 22:52 ` JP Thornley 2005-05-23 9:48 ` ich_bin_elvis 0 siblings, 1 reply; 19+ messages in thread From: JP Thornley @ 2005-05-21 22:52 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: SPARK and Interfaces.C 2005-05-21 22:52 ` JP Thornley @ 2005-05-23 9:48 ` ich_bin_elvis 2005-05-23 13:30 ` JP Thornley 0 siblings, 1 reply; 19+ messages in thread From: ich_bin_elvis @ 2005-05-23 9:48 UTC (permalink / raw) 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? ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: SPARK and Interfaces.C 2005-05-23 9:48 ` ich_bin_elvis @ 2005-05-23 13:30 ` JP Thornley 2005-05-23 15:10 ` JP Thornley 0 siblings, 1 reply; 19+ messages in thread From: JP Thornley @ 2005-05-23 13:30 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: SPARK and Interfaces.C 2005-05-23 13:30 ` JP Thornley @ 2005-05-23 15:10 ` JP Thornley 2005-05-24 8:57 ` ich_bin_elvis 0 siblings, 1 reply; 19+ messages in thread From: JP Thornley @ 2005-05-23 15:10 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: SPARK and Interfaces.C 2005-05-23 15:10 ` JP Thornley @ 2005-05-24 8:57 ` ich_bin_elvis 2005-05-24 10:36 ` JP Thornley 0 siblings, 1 reply; 19+ messages in thread From: ich_bin_elvis @ 2005-05-24 8:57 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: SPARK and Interfaces.C 2005-05-24 8:57 ` ich_bin_elvis @ 2005-05-24 10:36 ` JP Thornley 2005-05-24 20:34 ` ich_bin_elvis 0 siblings, 1 reply; 19+ messages in thread From: JP Thornley @ 2005-05-24 10:36 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: SPARK and Interfaces.C 2005-05-24 10:36 ` JP Thornley @ 2005-05-24 20:34 ` ich_bin_elvis 2005-05-25 7:54 ` JP Thornley 0 siblings, 1 reply; 19+ messages in thread From: ich_bin_elvis @ 2005-05-24 20:34 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: SPARK and Interfaces.C 2005-05-24 20:34 ` ich_bin_elvis @ 2005-05-25 7:54 ` JP Thornley 0 siblings, 0 replies; 19+ messages in thread From: JP Thornley @ 2005-05-25 7:54 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 19+ messages in thread
end of thread, other threads:[~2005-05-25 7:54 UTC | newest] Thread overview: 19+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2005-05-13 17:34 SPARK and Interfaces.C ich_bin_elvis 2005-05-13 19:40 ` JP Thornley 2005-05-14 12:15 ` Rod Chapman 2005-05-14 13:31 ` Martin Dowie 2005-05-14 15:41 ` Rod Chapman 2005-05-17 10:55 ` ich_bin_elvis 2005-05-17 14:40 ` Rod Chapman 2005-05-19 8:12 ` ich_bin_elvis 2005-05-19 8:46 ` ich_bin_elvis 2005-05-19 9:01 ` Rod Chapman 2005-05-19 10:25 ` ich_bin_elvis 2005-05-21 22:52 ` JP Thornley 2005-05-23 9:48 ` ich_bin_elvis 2005-05-23 13:30 ` JP Thornley 2005-05-23 15:10 ` JP Thornley 2005-05-24 8:57 ` ich_bin_elvis 2005-05-24 10:36 ` JP Thornley 2005-05-24 20:34 ` ich_bin_elvis 2005-05-25 7:54 ` JP Thornley
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox