3. Understanding Messages

3.1. Checks

In the location view, click in the tree on the + sign (or triangle) at the left of tokens.adb. Click on the message reported at line 26. This opens the file tokens.adb at line 26.

The message gives 3 different pieces of information:

  • Ranking

    Can be high, medium or low. It is an indication of the severity and certainty of the associated message. The higher the ranking, the more interesting the message, and the greater the likelihood the indicated line of code would fail when executed.

    Here, it is a medium message.

  • Check

    A short description of the problem.

    Here, it says that the array index check might fail.

  • Explanation

    Some messages have a more detailed explanation to help you understand the problem.

    Here, it says that it requires the first index in Input.Next_Word to be less than its last index, which is the same as saying Input.Next_Word should not be empty.

Indeed, the expression at line 26 is accessing at the first index in local variable Word, which happens to be initialized at line 18 with a call to Input.Next_Word. So it will raise a Constraint_Error if Input.Next_Word returns the empty string.

Now go to the definition of function Input.Next_Word. This can be achieved either by clicking on the right mouse button on Next_Word on line 18 and selecting Goto body of Next_Word or by clicking on the middle mouse button while holding Control key and moving the mouse over Next_Word on line 18. To do so, you first need to go to Scenario and in the Build Mode, select gnatsas from the drop down list.

The annotations generated by GNAT SAS’ Inspector are displayed before the definition of function Next_Word on line 184. You can hide these annotations by clicking on the right mouse button and selecting GNATSAS ‣ Hide annotations. Re-display these annotations by clicking on the right mouse button and selecting GNATSAS ‣ Show annotations.

In the postconditions generated by GNAT SAS’ Inspector, you can see that Inspector computed a possible range of 1..1_024 for the application of attribute First to the result of calling Next_Word, which is displayed as input.next_word’Result’First, and a possible range of 0..1_023 for the application of attribute Last to the same value. This includes the case where Result’First is 1 and Result’Last is 0, so the result may be an empty string.

Looking at the body of function Next_Word, it appears that an empty string is indeed returned when the first character read on line 191 is not in the range of Printable_Character.

To protect against this error, return to file tokens.adb at line 26, and insert the following code before the case-statement:

if Word = "" then
   raise Except.User_Error;
end if;

Re-run GNAT SAS by selecting the menu GNATSAS ‣ Analyze All. Notice that the error on tokens.adb has disappeared.

3.2. Warnings

This refers to messages reported by GNAT SAS that do not correspond to checks, but rather to potential logic errors: dead code, test or condition predetermined, unused assignment, etc. Like checks, these messages have an associated ranking, they are introduced by the keyword warning which is appended after the high, medium or low markers, e.g medium warning.

In the Locations View, click on the message reported at line 41 of stack.adb. It says that the precondition computed by GNAT SAS’ Inspector for variable Last is suspicious, because it is not a continuous range of values.

Indeed, looking at the preconditions generated by Inspector, we see the following lines:

--  Preconditions:
--    Last in (2..199, 201)

It is indeed the case that the range of values allowed for variable Last has a ‘hole’, because value 200 is not allowed while values 199 and 201 are allowed.

Since 200 is the value of Tab’Last, having Last equal to 200 means that the stack is full. So it is expected that we should not call Push on a stack when Last equals 200.

What’s surprising is that Last can be equal to 201 in the precondition computed by Inspector. This means that we could call Push on a stack which is more than full!

Let’s simulate what happens when we call Push with Last being equal to 201. The test on line 43 is false, so execution continues on line 47, then on line 49 Last is assigned the value 200 (201 - 1) and finally on line 50 we replace the last item in array Tab with the value V.

What’s wrong here?

The problem is on line 49: instead of decrementing the value of Last, it should be incremented. This bug is also found by debugging during the GNAT Studio tutorial.

Notice that it also causes the message at line 11 in file values.adb, because function Stack.Push is called in function Values.Process, so the precondition generated for Stack.Push causes a similar precondition to be generated for Values.Process.

This kind of logic error typically results in a precondition with a ‘hole’ like the one reported here. This is why GNAT SAS reports warnings when it encounters such preconditions.

After correcting line 49, re-run GNAT SAS. The two messages in files stack.adb and values.adb are no longer present.

3.3. False Positive

Some messages reported by GNAT SAS are not actual errors. These messages which are called false positive are a necessary evil when performing static analysis of complex properties of code.

First, allow low messages to be displayed by checking the box low in Message ranking.

In the location view, click on the message reported on the code you were asked to insert before line 26 of tokens.adb. It says that an exception might be raised, which is precisely the intention of the inserted code when Input.Next_Word returns an empty string.

Likewise, click on the message reported at line 191 of input.adb. It says that First_Char might be greater than Line_Size (1024).

This cannot happen, as the call to Input.Skip_Spaces ensures that First_Char points within the bounds of Line to a printable character, and the loop between lines 191 and 193 cannot increase First_Char beyond Line_Size because the procedure Input.Read_New_Line which updates Line ensures that the line is terminated by a character ASCII.CR which is not printable. So the loop will exit at most when First_Char is the index of this last character.

You can choose to ignore such false positive, or else mark them as reviewed so that they do not show up in future runs of GNAT SAS. To do that, click on the Edit icon displayed in front of GNAT SAS messages in the Locations View. This opens a window where you can enter a manual analysis of the message and e.g. change its New status to Not a bug.

Notice that the reasoning above, for the value of First_Char, depends on subtle invariants maintained by the code on the Line data structure. This may reveal brittle code which would deserve refactoring. A good way to realize this is to try to understand how Input.Skip_Spaces ensures that First_Char points within the bounds of Line. This is not as easy as it seems!