.. _Understanding_Messages: ********************** Understanding Messages ********************** Checks ====== In the location view, click in the tree on the `+` sign (or triangle) at the left of :file:`tokens.adb`. Click on the message reported at line 26. This opens the file :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 :kbd:`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 :menuselection:`GNATSAS --> Hide annotations`. Re-display these annotations by clicking on the right mouse button and selecting :menuselection:`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`. .. highlight:: ada To protect against this error, return to file :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 :menuselection:`GNATSAS --> Analyze All`. Notice that the error on :file:`tokens.adb` has disappeared. 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 :file:`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 :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 :file:`stack.adb` and :file:`values.adb` are no longer present. .. _False_Positive: 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 :file:`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 :file:`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!