Nico Huber merged this change.

View Change

gma pipe setup: Refactor calculation to ease proof

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

Change-Id: Id5def319993b34144473984ca25c71d92c957180
Signed-off-by: Nico Huber <nico.h@gmx.de>
Reviewed-on: https://review.coreboot.org/c/libgfxinit/+/27152
Reviewed-by: Angel Pons <th3fanbus@gmail.com>
---
M common/hw-gfx-gma-pipe_setup.adb
1 file changed, 10 insertions(+), 5 deletions(-)

diff --git a/common/hw-gfx-gma-pipe_setup.adb b/common/hw-gfx-gma-pipe_setup.adb
index 0a2cbcf..bb7b989 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);

To view, visit change 27152. To unsubscribe, or for help writing mail filters, visit settings.