CodePeer : Find the Bug Challenge
« Back to Index

Challenge 9 – Checking User-Specified Contracts

Ever wondered how a drowsy pilot might react to wings having bad vibrations on a diverging plane? Well, let’s explore the possibilities in this small automaton with 3^5 states.

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 74: “high: postcondition failure on wings.decrease_stress: requires Current_State <= Under_Stress”

Here’s how CodePeer helps you coming to this conclusion: Decrease_Stress is annotated with a contract expressed as a pair of aspects “Pre” and “Post” in Ada 2012 syntax. CodePeer detects that the postcondition of this contract is violated. Indeed, Decrease_Stress starts in a state where Current_State is not minimal, then it is incremented, so it cannot end with Normal_Condition or Under_Stress, which is required by its postcondition. The problem is that the increment on line 73 should really be a decrement.

Error line 111: “medium: precondition might fail on plane.transition: requires (soft) New_State = In_Distress”

Here’s how CodePeer helps you coming to this conclusion: Procedure Plane. Transition has a precondition expressed in Ada 2012 syntax, with a “Pre” aspect. It says that argument New_State should be equal to In_Distress whenever the Current_State is so. Here, it might be the case, so the caller should not be allowed to call Plane.Transition with New_State = On_Trajectory.

Error line 122: “high: precondition failure on wings.transition: requires New_State = Under_Stress or Current_State = Under_Stress”

Here’s how CodePeer helps you coming to this conclusion: CodePeer computes the precondition that either one of parameter New_State or global Current_State must be equal to Under_Stress when calling Wings.Transition. This precondition directly originates in a user assertion in Wings.Transition. On line 122, neither is true: Current_State is equal to Bad_Vibration according to the test on line 121, and the parameter New_State is equal to Normal_Condition.

Error line 144: “warning: dead code because New_State >= Drowsy”

Here’s how CodePeer helps you coming to this conclusion: CodePeer detects that New_State cannot be equal to Awake at this point. Assume that Transition is called with New_State = Awake. It returns on line 133 if Current_State = Awake. Otherwise, Current_State /= Awake and Transition calls Treat_Emergency on line 138, which requires in precondition that Current_State = Awake (through a pragma Precondition). This is impossible, which CodePeer correctly detects and transforms into a precondition on Transition, requiring that Current_State <= New_State.

Error line 146: “medium: precondition might fail on plane.transition: requires (soft) New_State = In_Distress”

Here’s how CodePeer helps you coming to this conclusion: This is the same error as on line 111.


package Engines is

   type State is (Excessive_Speed, Normal_Speed, Halted);

   Current_State : State;

   procedure Transition (New_State : State);

end Engines;

package Plane is

   type State is (On_Trajectory, Diverging, In_Distress);

   Current_State : State;

   procedure Transition (New_State : State) with
     Pre => (if Current_State = In_Distress then New_State = In_Distress);
             --  State 'In_Distress' is sticky, no action should change it

end Plane;

package body Plane is

   procedure Transition (New_State : State) is
   begin
      Current_State := New_State;
   end Transition;

end Plane;

package Tank is

   type State is (Full, Half_Full, Empty);

   Current_State : State;

   procedure Transition (New_State : State);

end Tank;

package Wings is

   type State is (Normal_Condition, Under_Stress, Bad_Vibration);

   Current_State : State;

   function Stress_Is_Minimal return Boolean is
      (Current_State = Normal_Condition);
   function Stress_Is_Maximal return Boolean is
      (Current_State = Bad_Vibration);

   procedure Increase_Stress with
      Pre  => not Stress_Is_Maximal,
      Post => not Stress_Is_Minimal;
   procedure Decrease_Stress with
      Pre  => not Stress_Is_Minimal,
      Post => not Stress_Is_Maximal;

   procedure Transition (New_State : State);

end Wings;

package body Wings is

   procedure Increase_Stress is
   begin
      Current_State := State'Val (State'Pos (Current_State) + 1);
   end Increase_Stress;

   procedure Decrease_Stress is
   begin
      Current_State := State'Val (State'Pos (Current_State) + 1);
   end Decrease_Stress;

   procedure Transition (New_State : State) is
   begin
      pragma Assert
        (New_State = Under_Stress or else Current_State = Under_Stress);
      --  No abrupt transition should be observed from 'Normal_Condition' to
      --  'Bad_Vibration' directly, or the opposite way

      Current_State := New_State;
   end Transition;

end Wings;

package Pilot is

   type State is (Awake, Drowsy, Asleep);

   Current_State : State;

   procedure Transition (New_State : State);

end Pilot;

with Engines; use type Engines.State;
with Plane;   use type Plane.State;
with Tank;    use type Tank.State;
with Wings;   use type Wings.State;

package body Pilot is

   procedure Recover_Trajectory is
   begin
      if Engines.Current_State = Engines.Normal_Speed and then
        Tank.Current_State /= Tank.Empty and then
        Wings.Current_State = Wings.Normal_Condition then
         --  Eventually recover the planned trajectory, if not currently
         Plane.Transition (Plane.On_Trajectory);
      end if;
   end Recover_Trajectory;

   procedure Treat_Emergency is
      pragma Precondition (Current_State = Awake);
   begin
      if Engines.Current_State /= Engines.Normal_Speed and then
        Tank.Current_State /= Tank.Empty then
         --  Get back to normal state when possible
         if Wings.Current_State = Wings.Bad_Vibration then
            Wings.Transition (Wings.Normal_Condition);
         end if;
         if Engines.Current_State = Engines.Excessive_Speed then
            Engines.Transition (Engines.Normal_Speed);
         end if;
      end if;
   end Treat_Emergency;

   procedure Transition (New_State : State) is
   begin
      if New_State = Current_State then
         return;
      end if;

      --  If not asleep, then the pilot can recover from an emergency
      if New_State /= Asleep then
         Treat_Emergency;
      end if;

      --  It requires the pilot to be fully awake to recover the trajectory,
      --  otherwise the plane just drifts away
      if New_State = Awake then
         Recover_Trajectory;
      else
         Plane.Transition (Plane.Diverging);
      end if;

      Current_State := New_State;
   end Transition;

end Pilot;

See CodePeer in Action!

In this video, AdaCore engineer Yannick Moy walks you through this month’s challenge using CodePeer and GNAT Programming Studio, GNAT Pro IDE.