[coreboot-gerrit] Change in libgfxinit[master]: gma pipe setup: Refactor calculation to ease proof

[Nico Huber (Code Review)]

Nico Huber has uploaded this change for review. ( https://review.coreboot.org/27152

Change subject: gma pipe setup: Refactor calculation to ease proof
......................................................................

gma pipe setup: Refactor calculation to ease proof

Somehow GNATprove stumbles here when code changes elsewhere. Let's make
him focus on the linear-offset calculation.

Change-Id: Id5def319993b34144473984ca25c71d92c957180
Signed-off-by: Nico Huber 
---
M common/hw-gfx-gma-pipe_setup.adb
1 file changed, 10 insertions(+), 5 deletions(-)

git pull ssh://review.coreboot.org:29418/libgfxinit refs/changes/52/27152/1

diff --git a/common/hw-gfx-gma-pipe_setup.adb b/common/hw-gfx-gma-pipe_setup.adb
index 10afbfd..647ba35 100644
--- a/common/hw-gfx-gma-pipe_setup.adb
+++ b/common/hw-gfx-gma-pipe_setup.adb
@@ -259,11 +259,16 @@
          Registers.Write
            (Controller.DSPSTRIDE, Word32 (Pixel_To_Bytes (FB.Stride, FB)));
          if Config.Has_DSP_Linoff and then FB.Tiling = Linear then
-            Registers.Write
-              (Register => Controller.DSPLINOFF,
-               Value    => Word32 (Pixel_To_Bytes
-                             (FB.Start_Y * FB.Stride + FB.Start_X, FB)));
-            Registers.Write (Controller.DSPTILEOFF, 0);
+            pragma Assert_And_Cut (True);
+            declare
+               Linear_Offset : constant Pixel_Type :=
+                  FB.Start_Y * FB.Stride + FB.Start_X;
+            begin
+               Registers.Write
+                 (Register => Controller.DSPLINOFF,
+                  Value    => Word32 (Pixel_To_Bytes (Linear_Offset, FB)));
+               Registers.Write (Controller.DSPTILEOFF, 0);
+            end;
          else
             if Config.Has_DSP_Linoff then
                Registers.Write (Controller.DSPLINOFF, 0);