<p>Nico Huber <strong>posted comments</strong> on this change.</p><p><a href="https://review.coreboot.org/21206">View Change</a></p><p>Patch set 1:</p><blockquote style="border-left: 1px solid #aaa; margin: 10px 0; padding: 0 10px;"><p style="white-space: pre-wrap; word-wrap: break-word;">(1 comment)</p><p style="white-space: pre-wrap; word-wrap: break-word;">Instead of faking an access on Linux another potential approach<br>could be to explicitly specify the global contracts and accept/<br>justify the warning in the Linux implementation using pragma<br>Annotate (GNATprove).</p></blockquote><p style="white-space: pre-wrap; word-wrap: break-word;">This only just became feasible since GNATprove's flow analysis<br>doesn't seem to explode any more when you give explicit contracts<br>in generic packages. A first test seems to work with SPARK GPL<br>2017.</p><blockquote style="border-left: 1px solid #aaa; margin: 10px 0; padding: 0 10px;"><p style="white-space: pre-wrap; word-wrap: break-word;"><br>Have not tested it and will result in more code due to contracts.<br>On the other hand one would avoid the automatic contract<br>generation...</p></blockquote><p style="white-space: pre-wrap; word-wrap: break-word;">I'm planning to use more explicit contracts once I've tested newer<br>GNATprove versions more thoroughly. Especially such cases with a<br>contract shared among different implementations deserve an explicit<br>contract (i.e. lesson learned). Though, I'm not fond of warning<br>justifications and try to avoid them where possible. Maybe that<br>changes once GNAT developers stop rewording the warnings ;)</p><p>(1 comment)</p><ul style="list-style: none; padding-left: 20px;"><li><p><a href="https://review.coreboot.org/#/c/21206/1/common/linux/hw-pci-dev.adb">File common/linux/hw-pci-dev.adb:</a></p><ul style="list-style: none; padding-left: 20px;"><li><p style="margin-bottom: 4px;"><a href="https://review.coreboot.org/#/c/21206/1/common/linux/hw-pci-dev.adb@44">Patch Set #1, Line 44:</a> <code style="font-family:monospace,monospace">   package Dummy is</code></p><p><blockquote style="border-left: 1px solid #aaa; margin: 10px 0; padding: 0 10px;">Wrapping the procedure in a Dummy package is not necessary. Is there a part</blockquote></p><p style="white-space: pre-wrap; word-wrap: break-word;">Hmmm, IIRC, I was forced to this pattern by some upstream GNAT<br>version once and applied it ever since. I'll retest with coreboot's<br>current reference toolchain (GCC 6.3). Maybe it's not needed any<br>more.</p></li></ul></li></ul><p>To view, visit <a href="https://review.coreboot.org/21206">change 21206</a>. To unsubscribe, visit <a href="https://review.coreboot.org/settings">settings</a>.</p><div itemscope itemtype="http://schema.org/EmailMessage"><div itemscope itemprop="action" itemtype="http://schema.org/ViewAction"><link itemprop="url" href="https://review.coreboot.org/21206"/><meta itemprop="name" content="View Change"/></div></div>

<div style="display:none"> Gerrit-Project: libhwbase </div>
<div style="display:none"> Gerrit-Branch: master </div>
<div style="display:none"> Gerrit-MessageType: comment </div>
<div style="display:none"> Gerrit-Change-Id: If994db22d91eb3707e555871d854c3a25a13678b </div>
<div style="display:none"> Gerrit-Change-Number: 21206 </div>
<div style="display:none"> Gerrit-PatchSet: 1 </div>
<div style="display:none"> Gerrit-Owner: Nico Huber <nico.h@gmx.de> </div>
<div style="display:none"> Gerrit-Reviewer: Adrian-Ken Rueegsegger <ken@codelabs.ch> </div>
<div style="display:none"> Gerrit-Reviewer: Nico Huber <nico.h@gmx.de> </div>
<div style="display:none"> Gerrit-Comment-Date: Mon, 28 Aug 2017 10:24:23 +0000 </div>
<div style="display:none"> Gerrit-HasComments: Yes </div>