From: Lutz Donnerhacke <lutz@iks-jena.de>
Subject: Re: [Spark] Converting Arrays
Date: Tue, 11 Mar 2003 10:52:12 +0000 (UTC)
Date: 2003-03-11T10:52:12+00:00 [thread overview]
Message-ID: <slrnb6rfur.nq.lutz@taranis.iks-jena.de> (raw)
In-Reply-To: cf2c6063.0303110214.5c978575@posting.google.com
* Rod Chapman wrote:
> A common trick in this case is to use a local,
> hidden procedure to initialise the out parameter:
Cool idea. I read the book yesterday evening till midnight and came to the
conclusion, that I have to replace Fullpath by a large constraint array.
This was obviosly wrong. You can always switch off Spark checkings when
running into trouble. :-/
But how can I write the required pre conditions?
*******************************************************
Listing of SPARK Text
SPARK95 Examiner with VC and RTC Generator Release 6.3 / 11.02
Demonstration Version
*******************************************************
DATE : 11-MAR-2003 11:49:13.68
Line
1 with Kernel.Linux_i86;
2 --# inherit Kernel, Kernel.Linux_i86;
3
4 package Kernel.IO is
5 pragma Pure;
6
7 subtype long is Linux_i86.long;
8
9 type Fullpath is array(Positive range <>) of Character;
10 procedure To_Fullpath (s : String; path : out Fullpath);
11 --# derives path from s;
12 --# pre s'Length < path'Length;
^1
*** ( 1) Semantic Error:322: Only imports may be referenced in pre-conditions
or return expressions.
13 pragma Inline (To_Fullpath);
14 pragma Inline_Always (To_Fullpath);
[...]
5 summarised warning(s), comprising:
5 pragma(s)*
(*Note: the above warnings may affect the validity of the analysis.)
next prev parent reply other threads:[~2003-03-11 10:52 UTC|newest]
Thread overview: 18+ messages / expand[flat|nested] mbox.gz Atom feed top
2003-03-10 17:06 [Spark] Converting Arrays Lutz Donnerhacke
2003-03-10 20:03 ` James S. Rogers
2003-03-10 22:33 ` Lutz Donnerhacke
2003-03-11 10:14 ` Rod Chapman
2003-03-11 10:51 ` Lutz Donnerhacke
2003-03-11 10:52 ` Lutz Donnerhacke [this message]
2003-03-11 20:46 ` JP Thornley
2003-03-12 8:43 ` Phil Thornley
2003-03-12 11:57 ` Lutz Donnerhacke
2003-03-12 18:46 ` JP Thornley
2003-03-13 10:14 ` Lutz Donnerhacke
2003-03-12 9:43 ` Rod Chapman
2003-03-12 10:15 ` Lutz Donnerhacke
-- strict thread matches above, loose matches on Subject: below --
2003-03-13 5:55 Grein, Christoph
2003-03-13 9:47 ` Peter Amey
2003-03-13 10:15 ` Lutz Donnerhacke
2003-03-21 15:05 ` Peter Amey
2003-03-21 15:17 ` Lutz Donnerhacke
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox