.. highlight:: ada

.. _Understanding_Annotations:

*************************************
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.

.. _Basic_Annotations:

Basic Annotations
=================

Open file :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.

.. _More_Complex_Annotations:

More Complex Annotations
========================

Open file :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.