CodePeer Find the Bug Challenge
Challenge 1 – Uninitialized variables and fields
Abstract:
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.
Error Line 70: “precondition failure on contacts.complete: requires C.Phone to be initialized”
Here’s how CodePeer came 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 came 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 came 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 came 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;
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.
(Note: for best viewing results make sure that the player is set to 720p)
Alexis Paluel-Marmont said:
Hi!
I don’t want to be nitpicking, and maybe I am a complete moron. But you tell me.
For me, the most obvious problem with Get_By_Name is that it assumes being called with String which first index is 1. This could happen if, for example, the name is a slice extracted from another String.
If anybody calls it with a String which first index is not one, the Name_Length will be wrong (it should be N’Length and not N’Last) and the assignment [ Result.Name (1 .. N'Last) := N ] will automatically raise a Constraint_Error, because the lengthes of the strings do not match, no sliding helping here…
Would CodePeer not signal a potential problem here?
Alexis Paluel-Marmont said:
Sorry – I meant:
‘For me, the most obvious problem with Get_By_Name is that it assumes being called with String which first index is 1. This does not necessarily happen, for example, when the name is a slice extracted from another String.’
Bad editing…
Arnaud Charlet said:
You are right, there is a potential bug here, and a better coding would be to use ‘Length instead of ‘Last, good catch!
CodePeer does detect this and will generate a precondition that requires every caller to obey this strict rule (‘First = 1), so no message is generated directly, but any call that does not follow this rule would then be flagged by CodePeer.