diff options
| author | Jedidiah Barber <contact@jedbarber.id.au> | 2025-04-10 19:38:53 +1200 |
|---|---|---|
| committer | Jedidiah Barber <contact@jedbarber.id.au> | 2025-04-10 19:38:53 +1200 |
| commit | 192b9538fcbe46649dccd44b499a0d52d17cf283 (patch) | |
| tree | 0f32f064468eafa84aa8370b093ed5567a798eb0 /spec | |
| parent | 97df98beefa9cc088a5b68899dd90baf67d175c5 (diff) | |
Added preconditions on FLTK.Draw image subprograms
Diffstat (limited to 'spec')
| -rw-r--r-- | spec/fltk-draw.ads | 22 |
1 files changed, 14 insertions, 8 deletions
diff --git a/spec/fltk-draw.ads b/spec/fltk-draw.ads index 950a247..8346112 100644 --- a/spec/fltk-draw.ads +++ b/spec/fltk-draw.ads @@ -252,9 +252,12 @@ package FLTK.Draw is (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); procedure Draw_Image (X, Y, W, H : in Integer; @@ -265,9 +268,12 @@ package FLTK.Draw is (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); procedure Draw_Image_Mono (X, Y, W, H : in Integer; @@ -279,7 +285,7 @@ package FLTK.Draw is 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 @@ -292,9 +298,9 @@ package FLTK.Draw is 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); |