greg@unrelenting.technology has posted comments on this change. ( https://review.coreboot.org/c/libgfxinit/+/35869 )
Change subject: dp_info: read eDP 1.4+ DPCD link rates ......................................................................
Patch Set 2:
(9 comments)
Now using early returns with the success thing.
As for SPARK, the 'full' make target with spark-discovery-gpl-2017 spews a ton of warnings from all around the project. For new code, it says
hw-gfx-dp_info.adb:147:58: medium: range check might fail, in instantiation at hw-gfx-gma-dp_info.ads:19 hw-gfx-dp_info.adb:147:58: medium: overflow check might fail, in instantiation at hw-gfx-gma-dp_info.ads:19 hw-gfx-dp_info.adb:163:28: medium: range check might fail, in instantiation at hw-gfx-gma-dp_info.ads:19 hw-gfx-dp_info.adb:163:28: medium: overflow check might fail, in instantiation at hw-gfx-gma-dp_info.ads:19
which seems silly, it can't prove that the constants from the 0..7 range multiplied by 2 fit into the Aux_Payload_Index.
https://review.coreboot.org/c/libgfxinit/+/35869/1/common/hw-gfx-dp_info.adb File common/hw-gfx-dp_info.adb:
https://review.coreboot.org/c/libgfxinit/+/35869/1/common/hw-gfx-dp_info.adb... PS1, Line 106: Max_Rate : Word32;
An Integer type, e.g. `Natural`, would be preferred. GNATprove could check […]
Done
https://review.coreboot.org/c/libgfxinit/+/35869/1/common/hw-gfx-dp_info.adb... PS1, Line 109: Rates_Size : constant := 8;
oh.. I misread the Linux code, sorry. […]
Done
https://review.coreboot.org/c/libgfxinit/+/35869/1/common/hw-gfx-dp_info.adb... PS1, Line 120: Success := Success and Length = Caps_Size;
Yeah, I thought it's `in out`, I was looking at the wrong parameter (and didn't know how out paramet […]
Done
https://review.coreboot.org/c/libgfxinit/+/35869/1/common/hw-gfx-dp_info.adb... PS1, Line 122: 16#03#
We might want to give this a name, e.g. `eDP_Rev_1_4 : constant := 3;`, it's […]
Done
https://review.coreboot.org/c/libgfxinit/+/35869/1/common/hw-gfx-dp_info.adb... PS1, Line 122: Length = Caps_Size
Better check `Success` here instead of repeating `Length = Caps_Size`.
Done
https://review.coreboot.org/c/libgfxinit/+/35869/1/common/hw-gfx-dp_info.adb... PS1, Line 132: Length = Rates_Size
Same here, better check `Success`.
Done
https://review.coreboot.org/c/libgfxinit/+/35869/1/common/hw-gfx-dp_info.adb... PS1, Line 142: end if;
Something like this might do: […]
Done
https://review.coreboot.org/c/libgfxinit/+/35869/1/common/hw-gfx-dp_info.adb... PS1, Line 146: 540000
Nit, numbers could be written as `540_000` etc. […]
Done
https://review.coreboot.org/c/libgfxinit/+/35869/1/common/hw-gfx-dp_info.adb... PS1, Line 152: end if;
Please leave a comment here, that this actually needs support for individual […]
Done