Challenge 1 – Uninitialized variables and fields

This code defines a library Contacts of helper functions (Complete, Get_By_Name, Get_By_Phone) that access a database of contacts stored in an array. A contact is a record gathering the name, address and phone number of a person.

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 70: “precondition failure on contacts.complete: requires C.Phone to be initialized”

Here’s how CodePeer helps you coming to this conclusion: On line 63, Result is declared without being initialized. In particular, Result.Phone is not initialized. Then, on line 70, procedure Complete is called with Result for parameter C. This causes Result.Phone to be read on line 47.

Error line 70: “contacts.complete.Done might be uninitialized”

Here’s how CodePeer helps you coming to this conclusion: On line 64, Found is declared without being initialized. On line 70, procedure Complete is called with Found for out parameter Done. Inside Complete, Done is only initialized on line 56 if a matching contact is found. Thus, the loop might exit with Done uninitialized. In this case, Found is uninitialized on line 72 when it is read.

Error line 86: “precondition failure on contacts.complete: requires C.Name_Length to be initialized”

Here’s how CodePeer helps you coming to this conclusion: On line 80, Result is declared without being initialized. In particular, Result.Name_Length is not initialized. Then, on line 86, procedure Complete is called with Result for parameter C. This causes Result.Name_Length to be read on line 50.

Error line 86: “validity check: contacts.complete.Done might be uninitialized”

Here’s how CodePeer helps you coming to this conclusion: On line 81, Found is declared without being initialized. On line 86, procedure Complete is called with Found for out parameter Done. Inside Complete, Done is only initialized on line 56 if a matching contact is found. Thus, the loop might exit with Done uninitialized. In this case, Found is uninitialized on line 88 when it is read.

package Contacts is

 type Phone_Number is range 0 .. 2**32-1;
 type String_Access is access String;
 subtype String_Length is Natural range 0 .. 20;

 type Contact is record
    Name_Length : String_Length;
    Name        : String (1 .. String_Length'Last);
    Address     : String_Access;
    Phone       : Phone_Number;
 end record;

 Null_Contact : constant Contact :=
   (Name_Length => 0, Name => "####################", Address => null,
    Phone => 0);

 type Database is array (Integer range 1 .. 100) of Contact;

 procedure Complete (DB : Database; C : in out Contact; Done : out Boolean);
 --  Given a partial contact C, complete it to an existing contact in
 --  the database DB if possible, in which case Done is set to True

 function Get_By_Name (DB : Database; N : String) return Contact;
 --  Get an existing contact in the database DB by its name N.
 --  If no such contact exists, return a Null_Contact.

 function Get_By_Phone (DB : Database; P : Phone_Number) return Contact;
 --  Get an existing contact in the database DB by its phone number P.
 --  If no such contact exists, return a Null_Contact.

end Contacts;

package body Contacts is

 procedure Complete (DB : Database; C : in out Contact; Done : out Boolean) is
 begin
    --  Looping over database DB to find contact C
    for D in DB'Range loop
       pragma Assert (DB (D).Address /= null);
       --  For C to match DB (D), one of 3 cases must apply:
       --  (1) both have the same phone number
       --  (2) both have the same (non-null) address
       --  (3) both have the same name, which implies that their field
       --      Name_Length are equal, and their field Name are equal
       --      between indices 1 and Name_Length
       if C.Phone = DB (D).Phone or
         (C.Address /= null and then
            C.Address.all = DB (D).Address.all) or
         (C.Name_Length = DB (D).Name_Length and then
            C.Name (1 .. C.Name_Length) =
            DB (D).Name (1 .. DB (D).Name_Length))
       then
          --  A matching contact has been found. Update C and Done.
          C := DB (D);
          Done := True;
          exit;
       end if;
    end loop;
 end Complete;

 function Get_By_Name (DB : Database; N : String) return Contact is
    Result : Contact;
    Found  : Boolean;
 begin
    --  Initialize Result with name N
    Result.Name_Length := N'Last;
    Result.Name (1 .. N'Last) := N;
    --  Look for a matching contact in database DB
    Complete (DB, Result, Found);
    --  If a complete contact has been found, return it
    if Found then
       return Result;
    else
       return Null_Contact;
    end if;
 end Get_By_Name;

 function Get_By_Phone (DB : Database; P : Phone_Number) return Contact is
    Result : Contact;
    Found  : Boolean;
 begin
    --  Initialize Result with phone P
    Result.Phone := P;
    --  Look for a matching contact in database DB
    Complete (DB, Result, Found);
    --  If a complete contact has been found, return it
    if Found then
       return Result;
    else
       return Null_Contact;
    end if;
 end Get_By_Phone;

end Contacts;