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.

Go CodePeer!

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;