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.31.170.82 with SMTP id t79mr13631720vke.2.1472760453992;
        Thu, 01 Sep 2016 13:07:33 -0700 (PDT)
X-Received: by 10.157.38.178 with SMTP id l47mr1784449otb.13.1472760453952;
 Thu, 01 Sep 2016 13:07:33 -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!j37no12241912qta.0!news-out.google.com!w143ni953itb.0!nntp.google.com!i184no417155itf.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Thu, 1 Sep 2016 13:07:33 -0700 (PDT)
In-Reply-To: <lyzinshd4i.fsf@pushface.org>
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: <ly1t16k0kk.fsf@pushface.org>
 <2a104643-59b9-4a46-b543-5c124984bf43@googlegroups.com>
 <ly8tvdidty.fsf@pushface.org>
 <7b6e2997-fea8-4840-8829-8f975b4eed4a@googlegroups.com>
 <lyzinshd4i.fsf@pushface.org>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <ff262b9f-a0d4-41c6-aec9-31bab4667de6@googlegroups.com>
Subject: Re: SPARK 2014 and protected objects
From: Shark8 <onewingedshark@gmail.com>
Injection-Date: Thu, 01 Sep 2016 20:07:33 +0000
Content-Type: text/plain; charset=UTF-8
Xref: news.eternal-september.org comp.lang.ada:31684
Date: 2016-09-01T13:07:33-07:00
List-Id: <comp.lang.ada>

On Wednesday, August 31, 2016 at 2:55:42 PM UTC-6, Simon Wright wrote:
> Shark8 writes:
> 
> >> 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;
> 
> I meant rather how I was to get SPARK to handle them. I suppose one
> could detail each individual register or even bit field, but as far as I
> can see most folk just turn SPARK_Mode off.

Well, Randy just pointed out that specifying the address was/is meant for registers -- https://groups.google.com/forum/#!topic/comp.lang.ada/gPJh0r2XxcA -- so I guess it just depends on how far you want to use SPARK on them.