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 =>
null;
when Travel_Fast | Invisible =>
Max_Velocity : Positive range 1 .. 60;
case Mode is
when Invisible =>
Transparency : Float range 0.0 .. 0.1;
when others =>
null;
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)
is
Lower_Body_Movements : Natural := 0;
Upper_Body_Movements : Natural := 0;
Raw_Total : Energy;
begin
-- 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,
Max_Hourly_Consumption);
-- 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);
else
Consumed := Raw_Total;
end if;
else
Consumed := Raw_Total;
end if;
end Hourly_Energy_Consumption;
end Configs;