<p>Nico Huber has uploaded this change for <strong>review</strong>.</p><p><a href="https://review.coreboot.org/27152">View Change</a></p><pre style="font-family: monospace,monospace; white-space: pre-wrap;">gma pipe setup: Refactor calculation to ease proof<br><br>Somehow GNATprove stumbles here when code changes elsewhere. Let's make<br>him focus on the linear-offset calculation.<br><br>Change-Id: Id5def319993b34144473984ca25c71d92c957180<br>Signed-off-by: Nico Huber <nico.h@gmx.de><br>---<br>M common/hw-gfx-gma-pipe_setup.adb<br>1 file changed, 10 insertions(+), 5 deletions(-)<br><br></pre><pre style="font-family: monospace,monospace; white-space: pre-wrap;">git pull ssh://review.coreboot.org:29418/libgfxinit refs/changes/52/27152/1</pre><pre style="font-family: monospace,monospace; white-space: pre-wrap;"><span>diff --git a/common/hw-gfx-gma-pipe_setup.adb b/common/hw-gfx-gma-pipe_setup.adb</span><br><span>index 10afbfd..647ba35 100644</span><br><span>--- a/common/hw-gfx-gma-pipe_setup.adb</span><br><span>+++ b/common/hw-gfx-gma-pipe_setup.adb</span><br><span>@@ -259,11 +259,16 @@</span><br><span>          Registers.Write</span><br><span>            (Controller.DSPSTRIDE, Word32 (Pixel_To_Bytes (FB.Stride, FB)));</span><br><span>          if Config.Has_DSP_Linoff and then FB.Tiling = Linear then</span><br><span style="color: hsl(0, 100%, 40%);">-            Registers.Write</span><br><span style="color: hsl(0, 100%, 40%);">-              (Register => Controller.DSPLINOFF,</span><br><span style="color: hsl(0, 100%, 40%);">-               Value    => Word32 (Pixel_To_Bytes</span><br><span style="color: hsl(0, 100%, 40%);">-                             (FB.Start_Y * FB.Stride + FB.Start_X, FB)));</span><br><span style="color: hsl(0, 100%, 40%);">-            Registers.Write (Controller.DSPTILEOFF, 0);</span><br><span style="color: hsl(120, 100%, 40%);">+            pragma Assert_And_Cut (True);</span><br><span style="color: hsl(120, 100%, 40%);">+            declare</span><br><span style="color: hsl(120, 100%, 40%);">+               Linear_Offset : constant Pixel_Type :=</span><br><span style="color: hsl(120, 100%, 40%);">+                  FB.Start_Y * FB.Stride + FB.Start_X;</span><br><span style="color: hsl(120, 100%, 40%);">+            begin</span><br><span style="color: hsl(120, 100%, 40%);">+               Registers.Write</span><br><span style="color: hsl(120, 100%, 40%);">+                 (Register => Controller.DSPLINOFF,</span><br><span style="color: hsl(120, 100%, 40%);">+                  Value    => Word32 (Pixel_To_Bytes (Linear_Offset, FB)));</span><br><span style="color: hsl(120, 100%, 40%);">+               Registers.Write (Controller.DSPTILEOFF, 0);</span><br><span style="color: hsl(120, 100%, 40%);">+            end;</span><br><span>          else</span><br><span>             if Config.Has_DSP_Linoff then</span><br><span>                Registers.Write (Controller.DSPLINOFF, 0);</span><br><span></span><br></pre><p>To view, visit <a href="https://review.coreboot.org/27152">change 27152</a>. To unsubscribe, or for help writing mail filters, 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/27152"/><meta itemprop="name" content="View Change"/></div></div>

<div style="display:none"> Gerrit-Project: libgfxinit </div>
<div style="display:none"> Gerrit-Branch: master </div>
<div style="display:none"> Gerrit-MessageType: newchange </div>
<div style="display:none"> Gerrit-Change-Id: Id5def319993b34144473984ca25c71d92c957180 </div>
<div style="display:none"> Gerrit-Change-Number: 27152 </div>
<div style="display:none"> Gerrit-PatchSet: 1 </div>
<div style="display:none"> Gerrit-Owner: Nico Huber <nico.h@gmx.de> </div>