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=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,e646052dc594401f X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!postnews.google.com!c10g2000yqi.googlegroups.com!not-for-mail From: Alexandre K Newsgroups: comp.lang.ada Subject: Re: Strategies with SPARK which does not support exceptions Date: Mon, 21 Jun 2010 07:10:34 -0700 (PDT) Organization: http://groups.google.com Message-ID: <6236693f-0658-498d-a3c9-b8f3aea7a856@c10g2000yqi.googlegroups.com> References: NNTP-Posting-Host: 82.229.198.39 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 X-Trace: posting.google.com 1277129435 30319 127.0.0.1 (21 Jun 2010 14:10:35 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Mon, 21 Jun 2010 14:10:35 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: c10g2000yqi.googlegroups.com; posting-host=82.229.198.39; posting-account=TcezFQoAAAAjIIx-1YP3Hv74ICh_b8qk User-Agent: G2/1.0 X-HTTP-UserAgent: Opera/9.80 (Macintosh; Intel Mac OS X; U; fr) Presto/2.2.15 Version/10.10,gzip(gfe) Xref: g2news1.google.com comp.lang.ada:11851 Date: 2010-06-21T07:10:34-07:00 List-Id: > Does SPARK even permit exceptions? I'm too lazy to > look it up. > > Warren Hi Warren, Spark doesn't permit exception. The program that checks your code will complain about it. We can "use" exception in a package that is hidden for Spark (so not parsed by the Examiner), but as it is hidden, we can't proove this body part. It is the case when you need to call an existing program that is not a Spark one (Ada.Text_IO ...). Alex