)]}'
{"/PATCHSET_LEVEL":[{"author":{"_account_id":1000000,"name":"Nico Huber","email":"nico.h@gmx.de","username":"icon","avatars":[{"url":"https://www.gravatar.com/avatar/60d420b5d650d48b86d6921a9f683b64.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d32","height":32},{"url":"https://www.gravatar.com/avatar/60d420b5d650d48b86d6921a9f683b64.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d56","height":56},{"url":"https://www.gravatar.com/avatar/60d420b5d650d48b86d6921a9f683b64.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d100","height":100},{"url":"https://www.gravatar.com/avatar/60d420b5d650d48b86d6921a9f683b64.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d120","height":120}]},"change_message_id":"043c9bff7ac909c440007ce7a38752ac9760c86a","unresolved":false,"context_lines":[],"source_content_type":"","patch_set":1,"id":"dad66f76_56a5d635","updated":"2026-07-21 15:11:04.000000000","message":"Changing the `Mode` parameter to `in out` might break some proofs, let\u0027s see.\nIt\u0027s probably better to handle this in `Config_Helpers.Fill_Port_Config ()`.\nWe have something for HDMI there already.\n\nI also wonder if we shouldn\u0027t just always limit to 8 BPC. If displays can\ngenerally take it, there should be no loss. WDYT? I\u0027m not sure if I tested\nany 10BPC displays yet.","commit_id":"1dec9b2d32f93daf10a1f4ce06be16e9f4b13c95"},{"author":{"_account_id":1000031,"name":"Matt DeVillier","email":"mrchromebox@gmail.com","username":"mrchromebox","avatars":[{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d32","height":32},{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d56","height":56},{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d100","height":100},{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d120","height":120}]},"change_message_id":"53eeeaffad76900571444e23b1725abf42bda058","unresolved":false,"context_lines":[],"source_content_type":"","patch_set":1,"id":"43a43dea_1a4ed2b9","in_reply_to":"dad66f76_56a5d635","updated":"2026-07-21 15:52:03.000000000","message":"patch 2: switched to using Auto_BPC instead of EDID-provided color depth","commit_id":"1dec9b2d32f93daf10a1f4ce06be16e9f4b13c95"},{"author":{"_account_id":1000031,"name":"Matt DeVillier","email":"mrchromebox@gmail.com","username":"mrchromebox","avatars":[{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d32","height":32},{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d56","height":56},{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d100","height":100},{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d120","height":120}]},"change_message_id":"2e159c67da7e7b37e3e49d2e8c3dd06edb8437f6","unresolved":false,"context_lines":[],"source_content_type":"","patch_set":3,"id":"264e0ec5_c24e6e4d","updated":"2026-07-21 17:04:50.000000000","message":"rebasing since the gnatprove failure in PS2 was due to 3f37cce, not this patch","commit_id":"e7d3f56c9cace2b1c178004804bb6ea0f5346688"},{"author":{"_account_id":1000000,"name":"Nico Huber","email":"nico.h@gmx.de","username":"icon","avatars":[{"url":"https://www.gravatar.com/avatar/60d420b5d650d48b86d6921a9f683b64.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d32","height":32},{"url":"https://www.gravatar.com/avatar/60d420b5d650d48b86d6921a9f683b64.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d56","height":56},{"url":"https://www.gravatar.com/avatar/60d420b5d650d48b86d6921a9f683b64.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d100","height":100},{"url":"https://www.gravatar.com/avatar/60d420b5d650d48b86d6921a9f683b64.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d120","height":120}]},"change_message_id":"2b41495369bfd39c71b33c062cbb604103981e99","unresolved":false,"context_lines":[],"source_content_type":"","patch_set":3,"id":"b17fb9f5_9c673d89","in_reply_to":"264e0ec5_c24e6e4d","updated":"2026-07-22 07:51:41.000000000","message":"Don\u0027t worry about that. The bot is not 100% accurate yet, we\u0027ll override when necessary.","commit_id":"e7d3f56c9cace2b1c178004804bb6ea0f5346688"},{"author":{"_account_id":1000000,"name":"Nico Huber","email":"nico.h@gmx.de","username":"icon","avatars":[{"url":"https://www.gravatar.com/avatar/60d420b5d650d48b86d6921a9f683b64.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d32","height":32},{"url":"https://www.gravatar.com/avatar/60d420b5d650d48b86d6921a9f683b64.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d56","height":56},{"url":"https://www.gravatar.com/avatar/60d420b5d650d48b86d6921a9f683b64.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d100","height":100},{"url":"https://www.gravatar.com/avatar/60d420b5d650d48b86d6921a9f683b64.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d120","height":120}]},"change_message_id":"4e0da8f7bf2a229f2930bdfe4ae8f2244f5dbdfb","unresolved":false,"context_lines":[],"source_content_type":"","patch_set":5,"id":"1b547ad9_e96e2bd8","updated":"2026-07-24 15:27:28.000000000","message":"Found at least one 10-bit monitor (U3415W) but it doesn\u0027t advertise the 10 bits\nin its EDID 🤷","commit_id":"24902327df796c95e4b49fcf68d55374bd258722"}],"common/hw-gfx-edid.adb":[{"author":{"_account_id":1000000,"name":"Nico Huber","email":"nico.h@gmx.de","username":"icon","avatars":[{"url":"https://www.gravatar.com/avatar/60d420b5d650d48b86d6921a9f683b64.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d32","height":32},{"url":"https://www.gravatar.com/avatar/60d420b5d650d48b86d6921a9f683b64.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d56","height":56},{"url":"https://www.gravatar.com/avatar/60d420b5d650d48b86d6921a9f683b64.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d100","height":100},{"url":"https://www.gravatar.com/avatar/60d420b5d650d48b86d6921a9f683b64.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d120","height":120}]},"change_message_id":"2b41495369bfd39c71b33c062cbb604103981e99","unresolved":true,"context_lines":[{"line_number":155,"context_line":"            else"},{"line_number":156,"context_line":"               4 + 2 * Pos64 (Shift_Right"},{"line_number":157,"context_line":"                 (Raw_EDID (INPUT) and INPUT_DIGITAL_DEPTH_MASK,"},{"line_number":158,"context_line":"                  INPUT_DIGITAL_DEPTH_SHIFT))));"},{"line_number":159,"context_line":""},{"line_number":160,"context_line":"      -- Calculate absolute values from EDID relative values."},{"line_number":161,"context_line":"      Mode.H_Sync_Begin :\u003d Mode.H_Visible    + Mode.H_Sync_Begin;"}],"source_content_type":"application/octet-stream","patch_set":3,"id":"abe05c5e_fa2dc7ff","side":"PARENT","line":158,"updated":"2026-07-22 07:51:41.000000000","message":"I\u0027m afraid we\u0027re still going to need that code 😆 `Default_BPC ()` tries its best,\nbut it isn\u0027t always that simple. So with the EDID information, if present, we still\nhave higher chances to make things work (in case of LVDS, for instance, we can\u0027t be\nwrong, as it also affects the number of physical lanes to expect).\n\nBut this seems like a good spot, how about a\n```\nif Mode.BPC \u003e 8 then\n   Mode.BPC :\u003d 8;\n```\nwith a comment that we want to conserve bandwidth and expect such displays to accept\n8-bit colors? (and hopefully will be right)","commit_id":"7e08e5d2803914af4e46280b558ec1307ead9031"},{"author":{"_account_id":1000031,"name":"Matt DeVillier","email":"mrchromebox@gmail.com","username":"mrchromebox","avatars":[{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d32","height":32},{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d56","height":56},{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d100","height":100},{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d120","height":120}]},"change_message_id":"dc87eba7d0e5e051392545a6d945aedfbe95789b","unresolved":false,"context_lines":[{"line_number":155,"context_line":"            else"},{"line_number":156,"context_line":"               4 + 2 * Pos64 (Shift_Right"},{"line_number":157,"context_line":"                 (Raw_EDID (INPUT) and INPUT_DIGITAL_DEPTH_MASK,"},{"line_number":158,"context_line":"                  INPUT_DIGITAL_DEPTH_SHIFT))));"},{"line_number":159,"context_line":""},{"line_number":160,"context_line":"      -- Calculate absolute values from EDID relative values."},{"line_number":161,"context_line":"      Mode.H_Sync_Begin :\u003d Mode.H_Visible    + Mode.H_Sync_Begin;"}],"source_content_type":"application/octet-stream","patch_set":3,"id":"68d97a7d_f72ee21e","side":"PARENT","line":158,"in_reply_to":"abe05c5e_fa2dc7ff","updated":"2026-07-22 13:05:40.000000000","message":"Done","commit_id":"7e08e5d2803914af4e46280b558ec1307ead9031"},{"author":{"_account_id":1000000,"name":"Nico Huber","email":"nico.h@gmx.de","username":"icon","avatars":[{"url":"https://www.gravatar.com/avatar/60d420b5d650d48b86d6921a9f683b64.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d32","height":32},{"url":"https://www.gravatar.com/avatar/60d420b5d650d48b86d6921a9f683b64.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d56","height":56},{"url":"https://www.gravatar.com/avatar/60d420b5d650d48b86d6921a9f683b64.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d100","height":100},{"url":"https://www.gravatar.com/avatar/60d420b5d650d48b86d6921a9f683b64.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d120","height":120}]},"change_message_id":"68eb16d769fa84d12cec4e3e7bf708ca4ab1d4fd","unresolved":true,"context_lines":[{"line_number":159,"context_line":"         -- Clamp to 8-bit for compatibility and to conserve bandwidth"},{"line_number":160,"context_line":"         if Mode.BPC \u003e 8 then"},{"line_number":161,"context_line":"            Mode.BPC :\u003d 8;"},{"line_number":162,"context_line":"         end if;"},{"line_number":163,"context_line":""},{"line_number":164,"context_line":"      -- Calculate absolute values from EDID relative values."},{"line_number":165,"context_line":"      Mode.H_Sync_Begin :\u003d Mode.H_Visible    + Mode.H_Sync_Begin;"}],"source_content_type":"application/octet-stream","patch_set":4,"id":"3c10f89c_ec64734b","line":162,"updated":"2026-07-22 13:37:38.000000000","message":"The indentation is off, the new code should align with the code below. Sorry for\nthe ugly code up there.\n\nOtherwise the change looks good. I\u0027ll try to find some monitor to test as well.\nPretty sure I have some, just never actually looked at the BPC setting.","commit_id":"15e226c75d20ce0a1e70ef1a75d643c7ab7c3f98"},{"author":{"_account_id":1000031,"name":"Matt DeVillier","email":"mrchromebox@gmail.com","username":"mrchromebox","avatars":[{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d32","height":32},{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d56","height":56},{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d100","height":100},{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d120","height":120}]},"change_message_id":"1ee2e5f74ea12b7aad9017ca08014c9af519c34a","unresolved":false,"context_lines":[{"line_number":159,"context_line":"         -- Clamp to 8-bit for compatibility and to conserve bandwidth"},{"line_number":160,"context_line":"         if Mode.BPC \u003e 8 then"},{"line_number":161,"context_line":"            Mode.BPC :\u003d 8;"},{"line_number":162,"context_line":"         end if;"},{"line_number":163,"context_line":""},{"line_number":164,"context_line":"      -- Calculate absolute values from EDID relative values."},{"line_number":165,"context_line":"      Mode.H_Sync_Begin :\u003d Mode.H_Visible    + Mode.H_Sync_Begin;"}],"source_content_type":"application/octet-stream","patch_set":4,"id":"bc757816_d48ed07d","line":162,"in_reply_to":"3c10f89c_ec64734b","updated":"2026-07-22 13:43:21.000000000","message":"Done","commit_id":"15e226c75d20ce0a1e70ef1a75d643c7ab7c3f98"}],"common/hw-gfx-gma-config_helpers.adb":[{"author":{"_account_id":1000029,"name":"Ada SPARK","email":"gnatbot@sourcearcade.org","username":"gnatbot","avatars":[{"url":"https://www.gravatar.com/avatar/c244ab97f43ca382a72e76784b616a4b.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d32","height":32},{"url":"https://www.gravatar.com/avatar/c244ab97f43ca382a72e76784b616a4b.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d56","height":56},{"url":"https://www.gravatar.com/avatar/c244ab97f43ca382a72e76784b616a4b.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d100","height":100},{"url":"https://www.gravatar.com/avatar/c244ab97f43ca382a72e76784b616a4b.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d120","height":120}]},"change_message_id":"54d690330c60f00d02fabd50bd84bef8d2aec004","unresolved":false,"context_lines":[{"line_number":169,"context_line":"   with"},{"line_number":170,"context_line":"      Post \u003d\u003e"},{"line_number":171,"context_line":"         Port_Cfg.Mode.H_Visible \u003d Port_Cfg\u0027Old.Mode.H_Visible and"},{"line_number":172,"context_line":"         Port_Cfg.Mode.V_Visible \u003d Port_Cfg\u0027Old.Mode.V_Visible"},{"line_number":173,"context_line":"   is"},{"line_number":174,"context_line":"   begin"},{"line_number":175,"context_line":"      Port_Cfg.FDI.Receiver_Caps.Max_Link_Rate    :\u003d DP_Bandwidth_2_7;"}],"source_content_type":"application/octet-stream","patch_set":1,"id":"3f904241_6c1f3af5","line":172,"updated":"2026-07-21 15:14:10.000000000","message":"Config(s): alderlake haswell broxton g45 tigerlake i945 skylake\n```\nhw-gfx-gma-config_helpers.adb:172: medium: postcondition might fail, cannot prove Port_Cfg.Mode.V_Visible \u003d Port_Cfg\u0027Old.Mode.V_Visible\n  172 |         Port_Cfg.Mode.V_Visible \u003d Port_Cfg\u0027Old.Mode.V_Visible\n      |         ^ here\n  e.g. when Port_Cfg.Port \u003d DIGI_D\n        and Port_Cfg.Mode.V_Visible \u003d 2\n        and Port_Cfg.Mode.V_Sync_Begin \u003d 2\n        and Port_Cfg.Mode.V_Sync_End \u003d 2\n        and Port_Cfg.Mode.V_Total \u003d 2\n        and Port_Cfg\u0027Old.Port \u003d DIGI_D\n        and Port_Cfg\u0027Old.Mode.V_Visible \u003d 1\n        and Port_Cfg\u0027Old.Mode.V_Sync_Begin \u003d 2\n        and Port_Cfg\u0027Old.Mode.V_Sync_End \u003d 2\n        and Port_Cfg\u0027Old.Mode.V_Total \u003d 2\n  possible fix: call at line 180 should mention Mode (for argument Port_Cfg) in a postcondition\n  180 |      DP_Info.Preferred_Link_Setting (Port_Cfg.FDI, Port_Cfg.Mode, Success);\n      |             ^ here\n```","commit_id":"1dec9b2d32f93daf10a1f4ce06be16e9f4b13c95"}],"common/hw-gfx-gma-connector_info.ads":[{"author":{"_account_id":1000029,"name":"Ada SPARK","email":"gnatbot@sourcearcade.org","username":"gnatbot","avatars":[{"url":"https://www.gravatar.com/avatar/c244ab97f43ca382a72e76784b616a4b.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d32","height":32},{"url":"https://www.gravatar.com/avatar/c244ab97f43ca382a72e76784b616a4b.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d56","height":56},{"url":"https://www.gravatar.com/avatar/c244ab97f43ca382a72e76784b616a4b.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d100","height":100},{"url":"https://www.gravatar.com/avatar/c244ab97f43ca382a72e76784b616a4b.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d120","height":120}]},"change_message_id":"54d690330c60f00d02fabd50bd84bef8d2aec004","unresolved":false,"context_lines":[{"line_number":22,"context_line":"   with"},{"line_number":23,"context_line":"      Post \u003d\u003e"},{"line_number":24,"context_line":"         Port_Cfg.Port \u003d Port_Cfg.Port\u0027Old and"},{"line_number":25,"context_line":"         Port_Cfg.Mode \u003d Port_Cfg.Mode\u0027Old;"},{"line_number":26,"context_line":""},{"line_number":27,"context_line":"   procedure Next_Link_Setting"},{"line_number":28,"context_line":"     (Port_Cfg : in out Port_Config;"}],"source_content_type":"application/octet-stream","patch_set":1,"id":"4c9837f1_39f9c713","line":25,"updated":"2026-07-21 15:14:10.000000000","message":"Config(s): tigerlake g45 ironlake broxton i945 ironlake_edp skylake alderlake haswell\n```\nhw-gfx-gma-connector_info.ads:25: medium: postcondition might fail, cannot prove Port_Cfg.Mode \u003d Port_Cfg.Mode\u0027old\n   25 |         Port_Cfg.Mode \u003d Port_Cfg.Mode\u0027Old;\n      |         ^ here\n  e.g. when Port_Cfg.Display \u003d DP\n        and Port_Cfg.Mode.Dotclock \u003d Frequency_Type\u0027First+1\n        and Port_Cfg.Mode.H_Visible \u003d 1\n        and Port_Cfg.Mode.H_Sync_Begin \u003d 1\n        and Port_Cfg.Mode.H_Sync_End \u003d 1\n        and Port_Cfg\u0027Old.Display \u003d DP\n        and Port_Cfg\u0027Old.Mode.Dotclock \u003d Frequency_Type\u0027First\n        and Port_Cfg\u0027Old.Mode.H_Visible \u003d 1\n        and Port_Cfg\u0027Old.Mode.H_Sync_Begin \u003d 1\n        and Port_Cfg\u0027Old.Mode.H_Sync_End \u003d 1\n```","commit_id":"1dec9b2d32f93daf10a1f4ce06be16e9f4b13c95"}],"common/hw-gfx-gma-pipe_setup.adb":[{"author":{"_account_id":1000029,"name":"Ada SPARK","email":"gnatbot@sourcearcade.org","username":"gnatbot","avatars":[{"url":"https://www.gravatar.com/avatar/c244ab97f43ca382a72e76784b616a4b.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d32","height":32},{"url":"https://www.gravatar.com/avatar/c244ab97f43ca382a72e76784b616a4b.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d56","height":56},{"url":"https://www.gravatar.com/avatar/c244ab97f43ca382a72e76784b616a4b.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d100","height":100},{"url":"https://www.gravatar.com/avatar/c244ab97f43ca382a72e76784b616a4b.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d120","height":120}]},"change_message_id":"54d690330c60f00d02fabd50bd84bef8d2aec004","unresolved":false,"context_lines":[{"line_number":311,"context_line":""},{"line_number":312,"context_line":"         if Config.Has_DSP_Linoff and then FB.Tiling \u003d Linear then"},{"line_number":313,"context_line":"            pragma Assert_And_Cut"},{"line_number":314,"context_line":"              (FB.Start_Y * FB.Stride + FB.Start_X in Pixel_Type);"},{"line_number":315,"context_line":"            declare"},{"line_number":316,"context_line":"               Linear_Offset : constant Pixel_Type :\u003d"},{"line_number":317,"context_line":"                  FB.Start_Y * FB.Stride + FB.Start_X;"}],"source_content_type":"application/octet-stream","patch_set":1,"id":"11e8512e_121ca197","line":314,"updated":"2026-07-21 15:14:10.000000000","message":"Config(s): ironlake_edp i945 ironlake\n```\nhw-gfx-gma-pipe_setup.adb:314: medium: assertion might fail, cannot prove FB.Start_Y * FB.Stride + FB.Start_X in Pixel_Type\n  314 |              (FB.Start_Y * FB.Stride + FB.Start_X in Pixel_Type);\n      |               ^ here\n```","commit_id":"1dec9b2d32f93daf10a1f4ce06be16e9f4b13c95"},{"author":{"_account_id":1000029,"name":"Ada SPARK","email":"gnatbot@sourcearcade.org","username":"gnatbot","avatars":[{"url":"https://www.gravatar.com/avatar/c244ab97f43ca382a72e76784b616a4b.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d32","height":32},{"url":"https://www.gravatar.com/avatar/c244ab97f43ca382a72e76784b616a4b.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d56","height":56},{"url":"https://www.gravatar.com/avatar/c244ab97f43ca382a72e76784b616a4b.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d100","height":100},{"url":"https://www.gravatar.com/avatar/c244ab97f43ca382a72e76784b616a4b.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d120","height":120}]},"change_message_id":"290fcb3f62fe08fce6653e7a83bf4cbad4a5db36","unresolved":false,"context_lines":[{"line_number":311,"context_line":""},{"line_number":312,"context_line":"         if Config.Has_DSP_Linoff and then FB.Tiling \u003d Linear then"},{"line_number":313,"context_line":"            pragma Assert_And_Cut"},{"line_number":314,"context_line":"              (FB.Start_Y * FB.Stride + FB.Start_X in Pixel_Type);"},{"line_number":315,"context_line":"            declare"},{"line_number":316,"context_line":"               Linear_Offset : constant Pixel_Type :\u003d"},{"line_number":317,"context_line":"                  FB.Start_Y * FB.Stride + FB.Start_X;"}],"source_content_type":"application/octet-stream","patch_set":2,"id":"25970b8a_7a06b540","line":314,"updated":"2026-07-21 15:53:52.000000000","message":"Config(s): i945 ironlake_edp ironlake\n```\nhw-gfx-gma-pipe_setup.adb:314: medium: assertion might fail, cannot prove FB.Start_Y * FB.Stride + FB.Start_X in Pixel_Type\n  314 |              (FB.Start_Y * FB.Stride + FB.Start_X in Pixel_Type);\n      |               ^ here\n```","commit_id":"3ad2010b2ebfcc1106a99dd2fa4f6fd723121091"},{"author":{"_account_id":1000029,"name":"Ada SPARK","email":"gnatbot@sourcearcade.org","username":"gnatbot","avatars":[{"url":"https://www.gravatar.com/avatar/c244ab97f43ca382a72e76784b616a4b.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d32","height":32},{"url":"https://www.gravatar.com/avatar/c244ab97f43ca382a72e76784b616a4b.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d56","height":56},{"url":"https://www.gravatar.com/avatar/c244ab97f43ca382a72e76784b616a4b.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d100","height":100},{"url":"https://www.gravatar.com/avatar/c244ab97f43ca382a72e76784b616a4b.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d120","height":120}]},"change_message_id":"12a4ca3bdebe9a288e9f329127b00e9a2c5acb3b","unresolved":false,"context_lines":[{"line_number":311,"context_line":""},{"line_number":312,"context_line":"         if Config.Has_DSP_Linoff and then FB.Tiling \u003d Linear then"},{"line_number":313,"context_line":"            pragma Assert_And_Cut"},{"line_number":314,"context_line":"              (FB.Start_Y * FB.Stride + FB.Start_X in Pixel_Type);"},{"line_number":315,"context_line":"            declare"},{"line_number":316,"context_line":"               Linear_Offset : constant Pixel_Type :\u003d"},{"line_number":317,"context_line":"                  FB.Start_Y * FB.Stride + FB.Start_X;"}],"source_content_type":"application/octet-stream","patch_set":4,"id":"28049f8d_63f6b8c1","line":314,"updated":"2026-07-22 13:07:37.000000000","message":"Config(s): i945 ironlake_edp ironlake\n```\nhw-gfx-gma-pipe_setup.adb:314: medium: assertion might fail, cannot prove FB.Start_Y * FB.Stride + FB.Start_X in Pixel_Type\n  314 |              (FB.Start_Y * FB.Stride + FB.Start_X in Pixel_Type);\n      |               ^ here\n```","commit_id":"15e226c75d20ce0a1e70ef1a75d643c7ab7c3f98"},{"author":{"_account_id":1000029,"name":"Ada SPARK","email":"gnatbot@sourcearcade.org","username":"gnatbot","avatars":[{"url":"https://www.gravatar.com/avatar/c244ab97f43ca382a72e76784b616a4b.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d32","height":32},{"url":"https://www.gravatar.com/avatar/c244ab97f43ca382a72e76784b616a4b.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d56","height":56},{"url":"https://www.gravatar.com/avatar/c244ab97f43ca382a72e76784b616a4b.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d100","height":100},{"url":"https://www.gravatar.com/avatar/c244ab97f43ca382a72e76784b616a4b.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d120","height":120}]},"change_message_id":"d215769707dd35bd1604dce51732289d8a4d4896","unresolved":false,"context_lines":[{"line_number":311,"context_line":""},{"line_number":312,"context_line":"         if Config.Has_DSP_Linoff and then FB.Tiling \u003d Linear then"},{"line_number":313,"context_line":"            pragma Assert_And_Cut"},{"line_number":314,"context_line":"              (FB.Start_Y * FB.Stride + FB.Start_X in Pixel_Type);"},{"line_number":315,"context_line":"            declare"},{"line_number":316,"context_line":"               Linear_Offset : constant Pixel_Type :\u003d"},{"line_number":317,"context_line":"                  FB.Start_Y * FB.Stride + FB.Start_X;"}],"source_content_type":"application/octet-stream","patch_set":5,"id":"09351181_73b6b6de","line":314,"updated":"2026-07-22 13:45:28.000000000","message":"Config(s): ironlake i945 ironlake_edp\n```\nhw-gfx-gma-pipe_setup.adb:314: medium: assertion might fail, cannot prove FB.Start_Y * FB.Stride + FB.Start_X in Pixel_Type\n  314 |              (FB.Start_Y * FB.Stride + FB.Start_X in Pixel_Type);\n      |               ^ here\n```","commit_id":"24902327df796c95e4b49fcf68d55374bd258722"}],"common/ironlake/hw-gfx-gma-connectors.adb":[{"author":{"_account_id":1000029,"name":"Ada SPARK","email":"gnatbot@sourcearcade.org","username":"gnatbot","avatars":[{"url":"https://www.gravatar.com/avatar/c244ab97f43ca382a72e76784b616a4b.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d32","height":32},{"url":"https://www.gravatar.com/avatar/c244ab97f43ca382a72e76784b616a4b.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d56","height":56},{"url":"https://www.gravatar.com/avatar/c244ab97f43ca382a72e76784b616a4b.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d100","height":100},{"url":"https://www.gravatar.com/avatar/c244ab97f43ca382a72e76784b616a4b.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d120","height":120}]},"change_message_id":"54d690330c60f00d02fabd50bd84bef8d2aec004","unresolved":false,"context_lines":[{"line_number":44,"context_line":"      -- Override lane count for FDI_B if FDI_C is used"},{"line_number":45,"context_line":"      procedure Override_FDI_Link"},{"line_number":46,"context_line":"      with"},{"line_number":47,"context_line":"         Post \u003d\u003e Port_Cfg.Mode \u003d Port_Cfg\u0027Old.Mode"},{"line_number":48,"context_line":"      is"},{"line_number":49,"context_line":"         FDI_TX_CTL_FDI_TX_ENABLE      : constant :\u003d 1 * 2 ** 31;"},{"line_number":50,"context_line":"         FDI_TX_CTL_PORT_WIDTH_SEL_4   : constant :\u003d 3 * 2 ** 19;"}],"source_content_type":"application/octet-stream","patch_set":1,"id":"b2ed6633_189f4e00","line":47,"updated":"2026-07-21 15:14:10.000000000","message":"Config(s): ironlake_edp ironlake\n```\nhw-gfx-gma-connectors.adb:47: medium: postcondition might fail, cannot prove Port_Cfg.Mode \u003d Port_Cfg\u0027Old.Mode\n   47 |         Post \u003d\u003e Port_Cfg.Mode \u003d Port_Cfg\u0027Old.Mode\n      |                 ^ here\n  e.g. when Port_Cfg.Mode.Dotclock \u003d Frequency_Type\u0027First+1\n        and Port_Cfg.Mode.H_Visible \u003d 1\n        and Port_Cfg.Mode.H_Sync_Begin \u003d 1\n        and Port_Cfg.Mode.H_Sync_End \u003d 1\n        and Port_Cfg.Mode.H_Total \u003d 1\n        and Port_Cfg\u0027Old.Mode.Dotclock \u003d Frequency_Type\u0027First\n        and Port_Cfg\u0027Old.Mode.H_Visible \u003d 1\n        and Port_Cfg\u0027Old.Mode.H_Sync_Begin \u003d 1\n        and Port_Cfg\u0027Old.Mode.H_Sync_End \u003d 1\n        and Port_Cfg\u0027Old.Mode.H_Total \u003d 1\n  possible fix: call at line 77 should mention Mode (for argument Port_Cfg) in a postcondition\n   77 |         DP_Info.Preferred_Link_Setting (Port_Cfg.FDI, Port_Cfg.Mode, Success);\n      |                ^ here\n```","commit_id":"1dec9b2d32f93daf10a1f4ce06be16e9f4b13c95"}]}