Challenge 3 – Discriminant record and null pointer

This package defines the configuration of a player in an adventure computer game. Type Gameplay defines the various modes that the player can adopt. Depending on this mode, various features are defined, which determine the hourly energy consumption of the player.

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 73: “warning: dead code because Current.all.Mode >= Travel_Fast”

Here’s how CodePeer helps you coming to this conclusion: Looking at the preconditions generated by CodePeer for procedure Hourly_Energy_Consumption, we see that it generated the precondition (Current.Mode >= Travel_Fast), which is the reason for the dead code warning. Now look at the code and imagine what would happen with Current.Mode equal to Save_On_Energy, and you will see that there is a problem on line 63 when accessing Current.Max_Velocity, which is not defined when Current.Mode is equal to Save_On_Energy.

Error line 82: “high: validity check: Current.all.Fallback.all.Mode is uninitialized here”

Here’s how CodePeer helps you coming to this conclusion: Execution reaches this line only when the test on line 81 fails, which means that Current.Fallback is null! Then, of course, CodePeer considers that Current.Fallback.Mode is uninitialized. The correct code has an ‘and then’ instead of an ‘or else’ operator on line 81.

package Configs is

   type Gameplay is
     (Save_On_Energy, --  "green" mode
      Travel_Fast,    --  running program
      Invisible,      --  hide-and-seek
      Kill_Them_All); --  self explanatory

   subtype Energy is Natural range 0 .. 10_000;

   type Features (Mode : Gameplay := Save_On_Energy) is record
      Fallback : access Features; --  fallback features if current features
                                  --  require too much energy
      case Mode is
         when Save_On_Energy =>
         when Travel_Fast | Invisible =>
            Max_Velocity       : Positive range 1 .. 60;
            case Mode is
               when Invisible =>
                  Transparency : Float range 0.0 .. 0.1;
               when others =>
            end case;
         when Kill_Them_All =>
            Strength           : Natural range 0 .. 140;
            Protection         : Natural range 0 .. 25;
      end case;
   end record;

   Max_Hourly_Consumption : constant := 500;

   --  Compute an hourly energy consumption with the current features.
   --  Start from an initial energy consumption Consumed dependent on external
   --  factors and consumption history, and update it.
   --  If the current features do not sustain survival beyond current hour
   --  (Available would become less than Consumed) then adopt lower profile
   --  with fallback features if possible.
   procedure Hourly_Energy_Consumption
     (Current   : in out Features;
      Consumed  : in out Energy;
      Available : in Energy);

end Configs;

package body Configs is

   procedure Hourly_Energy_Consumption
     (Current   : in out Features;
      Consumed  : in out Energy;
      Available : in Energy)
      Lower_Body_Movements : Natural := 0;
      Upper_Body_Movements : Natural := 0;
      Raw_Total            : Energy;
      --  Depending on mode, energy is consumed in lower body movements or
      --  in upper body movements
      case Current.Mode is
         when Kill_Them_All =>
            Upper_Body_Movements := 5 * Current.Strength;
         when others =>
            Lower_Body_Movements := 5 * Current.Max_Velocity;
      end case;

      --  Spending of energy is topped by Max_Hourly_Consumption
      Raw_Total :=
        Natural'Min(Consumed + Lower_Body_Movements + Upper_Body_Movements,

      --  Recuperation operates twice as fast in "green" mode
      if Current.Mode = Save_On_Energy then
         Raw_Total := Raw_Total / 2;
      end if;

      --  If current features do not sustain life, switch to fallback features.
      --  Do not switch to "green" mode automatically, as this may rather
      --  endanger the player. Instead, he has the opportunity to switch to
      --  "green" mode manually in this case.
      if Raw_Total > Available then
         if Current.Fallback /= null or else
           Current.Fallback.Mode /= Save_On_Energy then
            --  Update features for caller
            Current := Current.Fallback.all;
            --  Recompute hourly energy consumption with the updated features
            Hourly_Energy_Consumption (Current, Consumed, Available);
            Consumed := Raw_Total;
         end if;
         Consumed := Raw_Total;
      end if;

   end Hourly_Energy_Consumption;

end Configs;