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-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,a691dc29968966aa X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2003-03-21 03:31:30 PST Path: archiver1.google.com!news1.google.com!newsfeed.stanford.edu!logbridge.uoregon.edu!news-FFM2.ecrc.net!news.iks-jena.de!not-for-mail From: Lutz Donnerhacke Newsgroups: comp.lang.ada Subject: Re: pragma Import with 'Address clause Date: Fri, 21 Mar 2003 11:31:29 +0000 (UTC) Organization: IKS GmbH Jena Message-ID: References: NNTP-Posting-Host: taranis.iks-jena.de X-Trace: branwen.iks-jena.de 1048246289 7067 217.17.192.37 (21 Mar 2003 11:31:29 GMT) X-Complaints-To: usenet@iks-jena.de NNTP-Posting-Date: Fri, 21 Mar 2003 11:31:29 +0000 (UTC) User-Agent: slrn/0.9.7.4 (Linux) Xref: archiver1.google.com comp.lang.ada:35594 Date: 2003-03-21T11:31:29+00:00 List-Id: * Rod Chapman wrote: > Lutz Donnerhacke wrote in message news:... >> A common technique to reinterpret data is: >> a : AT; >> [...] >> b : BT; >> for b'Address use a'Address; >> pragma Import(Ada, b); > > This is really bad style, especially in SPARK. It's efficient. > You are deliberately creating an aliasing that the Examiner can't detect, > so this will cause great confusion for the information-flow analysis of > your program. That's why I hide it. > A better way might be to use a hidden, in-lined instantiation of > Unchecked_Conversion, thus: > > function AT_To_BT (A : in AT) return BT > is > --# hide AT_To_BT; > function C is new Unchecked_Conversion (AT, BT); > begin > return C(A); > end AT_To_BT; > pragma Inline (AT_To_BT); Given that AT'Size is large (and possibly indetermined), the possible temporary copy has to be avoided in any case. > If A and B are both library level objects, and the address of A is static, > then you can create two views onto the same area of memory, and use SPARK's > data refinement mechanism to pretend to the outside world that it's > only 1 object really. Known, but not applicable here. > You still have to think hard here about which object gets initialized and > when. That's the purpose of my question. > Oh - there's one other case where we've done this trick - for I/O > devices that overload a single address port with both a write-only control > register and a read-only status register. For those things, we simply > declare 2 library level variables which have an identical address > clause, since in this case, we really would prefer to treat them > as distinct objects anyway... :-) Known and already used. Current code excerpt: procedure getdents_read(dents : in out Dir_State; node : out INode; name : out Filename; name_last : out Filename_Length; valid : out Boolean) is e_node : long; e_reclen : ushort; new_offset : Positive; procedure Init --# global out name, e_node, e_reclen; in dents; --# derives name, e_node, e_reclen from dents; is --# hide Init; type getdent is record d_ino : long; d_off : Offset_T; d_reclen : ushort; d_name : Filename; end record; pragma Convention(C, getdent); e : getdent; for e'Address use dents.buffer(dents.offset)'Address; pragma Import(Ada, e); begin e_node := e.d_ino; e_reclen := e.d_reclen; name := e.d_name; end Init; pragma Inline (Init); begin Init; new_offset := dents.offset + Natural(e_reclen); if e_node not in long(INode'First) .. long(INode'Last) or else new_offset > dents.length or else name(name'First) = ASCII.NUL then valid := false; node := 0; name_last := name'First; else valid := true; node := INode(e_node); dents.offset := new_offset; name_last := name'First; for i in Filename_Length range name'First + 1 .. name'Last --# assert i in name'First + 1 .. name'Last; loop if name(i) = ASCII.NUL then name_last := i - 1; exit; end if; end loop; end if; if node = 0 then dents.length := 0; -- signaling end of data end if; end getdents_read; File /var/home/lutz/work/ada/src/kernel/kernel_/io/getdents_read.vcg procedure IO.getdents_read VCs generated 21-MAR-2003 12:21:16 VCs simplified 21-MAR-2003 12:24:23 VCs for procedure_getdents_read : ---------------------------------------------------------------------------- | | | ---------Proved In--------- | | # | From | To | vcg | siv | plg | prv | TO DO | ---------------------------------------------------------------------------- 1 | start | rtc check @ 185 | | YES | | | | 2 | start | rtc check @ 186 | | YES | | | | 3 | start | rtc check @ 190 | | YES | | | | 4 | start | rtc check @ 191 | | YES | | | | 5 | start | rtc check @ 194 | | YES | | | | 6 | start | rtc check @ 195 | | YES | | | | 7 | start | rtc check @ 196 | | YES | | | | 8 | start | rtc check @ 197 | | YES | | | | 9 | start | rtc check @ 197 | | YES | | | | 10 | start | assert @ 197 | | YES | | | | 11 | 197 | assert @ 197 | | YES | | | | 12 | 197 | rtc check @ 200 | | YES | | | | 13 | 197 | rtc check @ 201 | | YES | | | | 14 | start | rtc check @ 208 | | YES | | | | 15 | start | rtc check @ 208 | | YES | | | | 16 | 197 | rtc check @ 208 | | YES | | | | 17 | 197 | rtc check @ 208 | | YES | | | | 18 | start | assert @ finish | YES | | | | | 19 | start | assert @ finish | YES | | | | | 20 | start | assert @ finish | YES | | | | | 21 | start | assert @ finish | YES | | | | | 22 | 197 | assert @ finish | YES | | | | | 23 | 197 | assert @ finish | YES | | | | | 24 | 197 | assert @ finish | YES | | | | | 25 | 197 | assert @ finish | YES | | | | | ----------------------------------------------------------------------------