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.
-
Nico Huber (Code Review)