From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,b2df4819ac8b566a X-Google-Attributes: gid103376,public X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!news4.google.com!news.glorb.com!newsfeed.stueberl.de!newsfeed.vmunix.org!peer-uk.news.demon.net!kibo.news.demon.net!news.demon.co.uk!demon!diphi.demon.co.uk!jpt From: JP Thornley Newsgroups: comp.lang.ada Subject: Re: SPARK and Interfaces.C Date: Wed, 25 May 2005 08:54:22 +0100 Message-ID: References: <1116005688.002279.128010@g43g2000cwa.googlegroups.com> <1116072937.506109.246460@g47g2000cwa.googlegroups.com> <1116327342.680775.205190@o13g2000cwo.googlegroups.com> <1116340818.264418.117280@g14g2000cwa.googlegroups.com> <1116492378.074823.321470@g43g2000cwa.googlegroups.com> <1116493274.004505.67590@g49g2000cwa.googlegroups.com> <1116498302.651121.297610@g49g2000cwa.googlegroups.com> <4lZe9SBIv7jCJwn3@diphi.demon.co.uk> <1116841716.694148.260010@g43g2000cwa.googlegroups.com> <1116925072.146066.235050@g49g2000cwa.googlegroups.com> <1116966852.991519.250200@g43g2000cwa.googlegroups.com> NNTP-Posting-Host: diphi.demon.co.uk Mime-Version: 1.0 Content-Type: text/plain;charset=us-ascii;format=flowed X-Trace: news.demon.co.uk 1117007895 10086 80.177.171.182 (25 May 2005 07:58:15 GMT) X-Complaints-To: abuse@demon.net NNTP-Posting-Date: Wed, 25 May 2005 07:58:15 +0000 (UTC) User-Agent: Turnpike/6.04-S () Xref: g2news1.google.com comp.lang.ada:11144 Date: 2005-05-25T08:54:22+01:00 List-Id: 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