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,FREEMAIL_FROM autolearn=unavailable autolearn_force=no version=3.4.4 X-Received: by 10.66.145.103 with SMTP id st7mr7615964pab.0.1472658115349; Wed, 31 Aug 2016 08:41:55 -0700 (PDT) X-Received: by 10.157.26.54 with SMTP id a51mr1004522ote.0.1472658115302; Wed, 31 Aug 2016 08:41:55 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!news.glorb.com!e124no85309ith.0!news-out.google.com!n186ni1285ith.0!nntp.google.com!i184no86516itf.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Wed, 31 Aug 2016 08:41:55 -0700 (PDT) In-Reply-To: Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=174.28.146.45; posting-account=lJ3JNwoAAAAQfH3VV9vttJLkThaxtTfC NNTP-Posting-Host: 174.28.146.45 References: <2a104643-59b9-4a46-b543-5c124984bf43@googlegroups.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <7b6e2997-fea8-4840-8829-8f975b4eed4a@googlegroups.com> Subject: Re: SPARK 2014 and protected objects From: Shark8 Injection-Date: Wed, 31 Aug 2016 15:41:55 +0000 Content-Type: text/plain; charset=UTF-8 Xref: news.eternal-september.org comp.lang.ada:31660 Date: 2016-08-31T08:41:55-07:00 List-Id: On Wednesday, August 31, 2016 at 1:42:51 AM UTC-6, Simon Wright wrote: > > We seem to have come up with (almost) the same solution, which gives me > confidence it's the right one. Thanks. You're quite welcome. > I had Protected_Value outside the PO because it's standing in for a > number of I/O registers communicating with devices on a shared SPI bus > via their /Chip Select lines. Not sure how to deal with the concept of > "a number of machine registers"! Well, if they're memory-mapped registers you could use something like: Regester_A : Word with Address => Location; If they aren't, you may have to be a bit more complex. Perhaps something like: Type Register is (AX, BX, CX, PC, Flags); Subtype GP_Register is Register range AX..Register'Pred(PC); -- Implemented w/ Machine_Code. Procedure Read ( Item : GP_Register; Value : out Value_Type ); Procedure Write( Item : GP_Register; Value : in Value_Type );