[coreboot-gerrit] Change in libgfxinit[master]: gma pipe setup: Refactor calculation to ease proof
Nico Huber (Code Review)
gerrit at coreboot.org
Mon Jun 18 17:22:56 CEST 2018
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 <nico.h at gmx.de>
---
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);
--
To view, visit https://review.coreboot.org/27152
To unsubscribe, or for help writing mail filters, visit https://review.coreboot.org/settings
Gerrit-Project: libgfxinit
Gerrit-Branch: master
Gerrit-MessageType: newchange
Gerrit-Change-Id: Id5def319993b34144473984ca25c71d92c957180
Gerrit-Change-Number: 27152
Gerrit-PatchSet: 1
Gerrit-Owner: Nico Huber <nico.h at gmx.de>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.coreboot.org/pipermail/coreboot-gerrit/attachments/20180618/edf3e64c/attachment-0001.html>
More information about the coreboot-gerrit
mailing list