From 192b9538fcbe46649dccd44b499a0d52d17cf283 Mon Sep 17 00:00:00 2001 From: Jedidiah Barber Date: Thu, 10 Apr 2025 19:38:53 +1200 Subject: Added preconditions on FLTK.Draw image subprograms --- doc/fl_draw.html | 22 ++++++++++++++-------- 1 file changed, 14 insertions(+), 8 deletions(-) (limited to 'doc/fl_draw.html') diff --git a/doc/fl_draw.html b/doc/fl_draw.html index d987920..55b08bd 100644 --- a/doc/fl_draw.html +++ b/doc/fl_draw.html @@ -415,9 +415,12 @@ procedure Draw_Image (X, Y, W, H : in Integer; Data : in Color_Component_Array; Depth : in Positive := 3; - Line_Data : in Natural := 0; + Line_Size : in Natural := 0; Flip_Horizontal : in Boolean := False; - Flip_Vertical : in Boolean := False); + Flip_Vertical : in Boolean := False) +with Pre => (if Line_Size = 0 + then Data'Length >= W * H * Depth + else Data'Length >= Line_Size * H); @@ -444,9 +447,12 @@ procedure Draw_Image_Mono (X, Y, W, H : in Integer; Data : in Color_Component_Array; Depth : in Positive := 1; - Line_Data : in Natural := 0; + Line_Size : in Natural := 0; Flip_Horizontal : Boolean := False; - Flip_Vertical : Boolean := False); + Flip_Vertical : Boolean := False) +with Pre => (if Line_Size = 0 + then Data'Length >= W * H * Depth + else Data'Length >= Line_Size * H); @@ -477,7 +483,7 @@ procedure Draw_Pixmap Colors : in FLTK.Images.Pixmaps.Color_Definition_Array; Pixels : in FLTK.Images.Pixmaps.Pixmap_Data; X, Y : in Integer; - Hue : in Color := Grey0_Color) + Tone : in Color := Grey0_Color) with Pre => Colors'Length = Values.Colors and Pixels'Length (1) = Values.Height and @@ -909,9 +915,9 @@ function Read_Image Alpha : in Integer := 0) return Color_Component_Array with Post => - (if Alpha = 0 - then Read_Image'Result'Length = W * H * 3 - else Read_Image'Result'Length = W * H * 4); + (if Alpha = 0 + then Read_Image'Result'Length = W * H * 3 + else Read_Image'Result'Length = W * H * 4); -- cgit