[coreboot-gerrit] Change in libhwbase[master]: linux pci: Add dummy PCI access for shared contracts

[Nico Huber (Code Review)]

Nico Huber has posted comments on this change. ( https://review.coreboot.org/21206 )

Change subject: linux pci: Add dummy PCI access for shared contracts
......................................................................


Patch Set 1:

(1 comment)

> (1 comment)
> 
> Instead of faking an access on Linux another potential approach
> could be to explicitly specify the global contracts and accept/
> justify the warning in the Linux implementation using pragma
> Annotate (GNATprove).

This only just became feasible since GNATprove's flow analysis
doesn't seem to explode any more when you give explicit contracts
in generic packages. A first test seems to work with SPARK GPL
2017.

> 
> Have not tested it and will result in more code due to contracts.
> On the other hand one would avoid the automatic contract
> generation...

I'm planning to use more explicit contracts once I've tested newer
GNATprove versions more thoroughly. Especially such cases with a
contract shared among different implementations deserve an explicit
contract (i.e. lesson learned). Though, I'm not fond of warning
justifications and try to avoid them where possible. Maybe that
changes once GNAT developers stop rewording the warnings ;)

https://review.coreboot.org/#/c/21206/1/common/linux/hw-pci-dev.adb
File common/linux/hw-pci-dev.adb:

https://review.coreboot.org/#/c/21206/1/common/linux/hw-pci-dev.adb@44
PS1, Line 44:    package Dummy is
> Wrapping the procedure in a Dummy package is not necessary. Is there a part
Hmmm, IIRC, I was forced to this pattern by some upstream GNAT
version once and applied it ever since. I'll retest with coreboot's
current reference toolchain (GCC 6.3). Maybe it's not needed any
more.



-- 
To view, visit https://review.coreboot.org/21206
To unsubscribe, visit https://review.coreboot.org/settings

Gerrit-Project: libhwbase
Gerrit-Branch: master
Gerrit-MessageType: comment
Gerrit-Change-Id: If994db22d91eb3707e555871d854c3a25a13678b
Gerrit-Change-Number: 21206
Gerrit-PatchSet: 1
Gerrit-Owner: Nico Huber <nico.h at gmx.de>
Gerrit-Reviewer: Adrian-Ken Rueegsegger <ken at codelabs.ch>
Gerrit-Reviewer: Nico Huber <nico.h at gmx.de>
Gerrit-Comment-Date: Mon, 28 Aug 2017 10:24:23 +0000
Gerrit-HasComments: Yes
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.coreboot.org/pipermail/coreboot-gerrit/attachments/20170828/e4833a2a/attachment.html>