<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>