4. Understanding Inspector’s Annotations

In addition to messages, GNAT SAS’ Inspector analysis also generates annotations on your source code. Annotations express properties and assumptions of the code, and can be used to help reviewing the code manually and spot inconsistencies, and also to help understand messages generated by Inspector.

4.1. Basic Annotations

Open file stack.adb and look at the annotations for procedure Push.

The preconditions of Push correspond to constraints that should be respected prior to calling Push in order to avoid errors. The third precondition states that Last should be less than 200, so that the stack is not full. The other preconditions state that parameter V should not be null and V.E should be initialized:

--  Preconditions:
--    Last <= 199
--    V /= null
--    V.E'Initialized

While some preconditions can be traced to checks inside the current procedure, others originate in functions or procedures directly or indirectly (through a chain of other functions or procedures) called by the current procedure. Here, the last precondition can be traced to the increment on Last at line 49 and the access to Tab (Last) that follows on line 50, while the preconditions on V are propagated from the precondition of function Values.To_String called on line 47.

The postconditions of Push correspond to constraints that will be satisfied after calling Push. The first postcondition states that the output value for Last will be its input value plus one. Notice the use of Ada 2012 attribute ‘Old to denote the input value of Last. The second postcondition states that the output value of Last will be in the range 1..200:

--  Postconditions:
--    Last = Last'Old + 1
--    Last in 1..200
--    Tab(1..200) = One-of{V, Tab(1..200)'Old}

We will explain the last postcondition in the next section.

4.2. More Complex Annotations

Open file tokens.adb and look at the preconditions generated for procedure Process:

--  Preconditions:
--    T.Kind /= Op or Stack'Body.Last in 2..200
--    T.Kind /= Op or Stack'Body.Tab(Stack'Body.Last - 1) /= null
--    T.Kind /= Op or Stack'Body.Tab(Stack'Body.Last) /= null
--    T.Kind /= Op or Stack'Body.Tab(1..200).E'Initialized
--    T.Kind /= Op or T.Op'Initialized
--    T.Kind <= Op or Stack'Body.Last <= 200 or T.Instr /= Print
--    T.Kind <= Op or Stack'Body.Last = 0 or T.Instr /= Print or Stack'Body.Tab(Stack'Body.Last) /= null
--    T.Kind <= Op or Stack'Body.Last = 0 or T.Instr /= Print or Stack'Body.Tab(1..200).E'Initialized
--    T.Kind <= Op or T.Instr <= Print
--    T.Kind >= Op or Stack'Body.Last <= 199
--    T.Kind >= Op or T.Val /= null
--    T.Kind >= Op or T.Val.E'Initialized

Some preconditions are disjunctions of cases, like T.Kind /= Op or Last in 2..200. This conditional precondition states that, either T.Kind is different from Op, or Last must be in the range 2..200. This is because the constraint on Last comes from a path in Process that is only executed when T.Kind = Op, so it does not apply when T.Kind /= Op.

Look now at the postconditions generated for procedure Process:

--  Postconditions:
--    Stack'Body.Last = One-of{Stack'Body.Last'Old + 1, Stack'Body.Last'Old - 2, Stack'Body.Last'Old - 1, 0, Stack'Body.Last'Old}
--    Stack'Body.Last <= 200
--    Stack'Body.Tab(1..200) = One-of{T.Val, Stack'Body.Tab(1..200)'Old, new Value_Info(in values.operations.process)#1'Address}
--    new Value_Info(in values.operations.process)#1.<num objects> in 0..1
--    new Value_Info(in values.operations.process)#1.E'Initialized

Some postconditions of Process are of the form Variable = One-of{Value1, Value2, …}. This indicates that the output value of Variable is either Value1 or Value2 or … Look in particular at the postcondition of this form for Last. Inspector computed that the possible output value for Last is either zero, input value of Last, input value of Last plus one, input value of Last minus one or input value of Last minus two. This postcondition effectively summarizes all the possible modifications occuring to Last in various procedures and functions called from Process.

Be aware that, although annotations are displayed in an Ada-friendly syntax, they may not be legal Ada, or they may designate something different than in Ada. For example, there is no way in Ada to specify that a value should be initialized like suggested by the pseudo-Ada attribute ‘Initialized. Likewise, it is not valid in Ada to refer to the value of ‘any element of an array’ like done in Inspector annotations using the syntax of an array slice.