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;