Challenge 7 – Initialization, array checks and range checks
Ever found yourself not knowing what to put in this backpack your little one is carrying to school? This helper program does it for you, or your kid, or your kid’s teacher. Because not everyone has the same priorities.
Have a look at the following code and see if you can spot the errors. Once you think you’ve got them all, click on the “Go CodePeer” button to see how well you matched up to CodePeer’s comprehensive and rapid analysis of the same code.
Error line 65: “medium: array index check might fail: requires Res in 1..100”
Here’s how CodePeer helps you coming to this conclusion: Res is the result of calling Find_More_Useful, which returns 0 if no useful item was found. Hence, the code should test that Res is not null before accessing array B at index Res.
Error line 81: “medium: validity check: Res might be uninitialized”
Here’s how CodePeer helps you coming to this conclusion: Res is a local variable which is only assigned to in the loop if some fun item is found. Therefore it might be uninitialized when returning it on line 81. Instead, it should be default initialized to 0 on line 72.
Error line 102: “medium: array index check might fail: requires Best in 1..100”
Here’s how CodePeer helps you coming to this conclusion: Same as the error on line 65.
Error line 119: “low: range check might fail: requires (Total_Weight + Stuff(Best).Something.W) in 0..10_000”
Here’s how CodePeer helps you coming to this conclusion: Summing the weights of the selected items might well overcome the 10 kg limit that a variable of type Weight should respect. Instead, this addition should be protected against overflow, for example by calling Weight’Min appropriately before assigning to Total_Weight.
package Backpack is Useless : constant := 0; Mandatory : constant := 5; type Utility is range Useless .. Mandatory; Boring : constant := 0; So_Cooool : constant := 5; type Fun is range Boring .. So_Cooool; subtype Weight is Natural range 0 .. 10_000; -- in grams Scoliosis_Limit : constant := 6_000; type Item is record U : Utility; F : Fun; W : Weight; end record; -- content of the backpack type Content is array (Positive range <>) of Item; type Belonging is record Something : Item; Available : Boolean; end record; type Extended is range 0 .. 100; subtype Index is Extended range 1 .. 100; -- set of stuff to choose from to populate the backpack type Belongings is array (Index) of Belonging; type Strategy is (Teacher, -- maximize utility Mom_And_Pop, -- maximize utility and minimize weight Kiddo); -- maximize fun and avoid punishment -- Choose items from Stuff to populate Choice according to Strat procedure Back_To_School (Strat : Strategy; Stuff : in out Belongings; Choice : in out Content; Num : out Natural); end Backpack; package body Backpack is function Find_More_Useful (B : Belongings) return Extended is Res : Extended := 0; U : Utility := Useless; begin for I in Index loop if B(I).Something.U > U then Res := I; U := B(I).Something.U; end if; end loop; return Res; end Find_More_Useful; function Find_Mandatory (B : Belongings) return Extended is Res : Extended; begin Res := Find_More_Useful (B); if B (Res).Something.U /= Mandatory then Res := 0; end if; return Res; end Find_Mandatory; function Find_More_Fun (B : Belongings) return Extended is Res : Extended; F : Fun := Boring; begin for I in Index loop if B(I).Something.F > F then Res := I; F := B(I).Something.F; end if; end loop; return Res; end Find_More_Fun; procedure Back_To_School (Strat : Strategy; Stuff : in out Belongings; Choice : in out Content; Num : out Natural) is Best : Extended := 1; Total_Weight : Weight := 0; begin Num := 0; for Next in Positive range Choice'Range loop exit when Best = 0; -- no more stuff to pack, exit. case Strat is when Teacher | Mom_And_Pop => Best := Find_More_Useful (Stuff); -- take only useful stuff if Strat = Mom_And_Pop and then Stuff (Best).Something.U /= Mandatory and then Total_Weight + Stuff (Best).Something.W >= Scoliosis_Limit then -- Stop piling non-mandatory stuff before the scoliosis. Best := 0; end if; when Kiddo => Best := Find_Mandatory (Stuff); -- start with mandatory stuff if Best = 0 then Best := Find_More_Fun (Stuff); -- then pile fun stuff end if; end case; -- Found something useful/fun to bring in class? Put it in backpack. if Best /= 0 then Stuff (Best).Available := False; Choice (Next) := Stuff (Best).Something; Total_Weight := Total_Weight + Stuff (Best).Something.W; Num := Num + 1; end if; end loop; end Back_To_School; end Backpack;