Warning and error messages
==========================

Syntax error messages
---------------------

Error: foobar at line 17 column 42.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

The Bison front-end has detected a syntax error at the given location.
The error message is usually unusable, so let us hope the location is
enough for you to find what the problem is.

.. code-block:: gappa

   f(x) = x + 1;

::

   Error: syntax error, unexpected '(', expecting FUNID or '=' at line 1 column 2

Error: unrecognized option 'bar'.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Gappa was invoked with an unknown option.

Variant: ``unrecognized option 'bar' at line 42``. This error is displayed
for options embedded in the script.

Error: redefinition of identifier 'foo'...
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

A symbol cannot be defined more than once, even if the right hand sides
of every definitions are equivalent.

.. code-block:: gappa

   a = 1;
   a = 1;

Nor can it be defined after being used as an unbound variable.

.. code-block:: gappa

   b = a * 2;
   a = 1;

Error: invalid parameters for 'foo'...
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

A function template has been instantiated with an incorrect number of
parameters or with parameters of the wrong type.

.. code-block:: gappa

   x = float<ieee_32,0>(y);

::

   Error: invalid parameters for 'float' at line 1 column 20

Error: incorrect number of arguments for 'foo'...
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

There are either less or more expressions between parentheses than
expected by the function.

.. code-block:: gappa

   x = int<zr>(y, z);

::

   Error: incorrect number of arguments for 'fixed<0,zr>' at line 1 column 17

Other error messages during parsing
-----------------------------------

Error: undefined intervals are restricted to conclusions.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

You are not allowed to use an interrogation mark for an interval that
appears in negative position in the logical formula.

.. code-block:: gappa

   { x in ? -> x + 1 in [0,1] }

Error: the range of foo is an empty interval.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

An interval has been interpreted as having reverted bounds.

.. code-block:: gappa

   { x in [2,1] }

::

   Error: the range of x is an empty interval.

Interval bounds are replaced by binary floating-point numbers. As a
consequence, Gappa can encounter an empty interval when it tightens a
range appearing in a goal. For example, the empty set is the biggest
representable interval that is a subset of the singleton {1.3}. So Gappa
fails to prove the following property.

.. code-block:: gappa

   { 1.3 in [1.3,1.3] }

::

   Error: the range of 13e-1 is an empty interval.

Error: zero appears as a denominator in a rewriting rule.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Gappa has a detected that a divisor is trivially equal to zero in an
expression that appears in a rewriting rule. This is most certainly an
error.

.. code-block:: gappa

   { 1 in ? }
   y -> y * (x - x) / (x - x);

Proof failures
--------------

Error: no contradiction was found.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

The logical formula had no property in negative position or Gappa has
discharged all of them, yet this was not sufficient to prove the
formula.

.. code-block:: gappa

   { x in [1,2] -> not x + 1 in [2,3] }

Error: some enclosures were not satisfied.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Only part of a conjunction of goals was proved to be true. Gappa was
unable to prove some other expressions or formulas, which are displayed
after the message.

.. code-block:: gappa

   { x in [1,2] -> x + 1 in ? /\ x + 2 in [2,3] }

::

   Warning: case split on x + 2 has not produced any interesting new result.
   Results:
     x + 1 in [2, 3]
   Error: some properties were not satisfied:
     BND(x + 2), best: [3, 4]

.. _warning-messages1:

Warning messages during parsing
-------------------------------

Warning: renaming identifier 'foo' as 'bar'...
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

When a definition ``foo = expr`` is given to Gappa, the name ``foo`` is
associated to the expression ``expr``. This name is then used whenever
Gappa outputs ``expr``. If another definition ``bar = expr`` is later
provided, the new name supersedes the name given previously.

.. code-block:: gappa

   a = 42;
   b = 42;
   { a - b in ? }

::

   Warning: renaming identifier 'a' as 'b' at line 2 column 7
   b - b in [0, 0]

Warning: the expression foo has been assumed to be nonzero when checking a rewriting rule.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

When Gappa verifies that both sides of a user rewriting rule are
equivalent, it does not generate additional constraints to verify that
denominators appearing in the expressions are not zero. For example, the
rule ``1 / (1 / x) -> x`` only applies when ``x`` is not zero; yet Gappa
does not test for it.

No warning messages are displayed when constraints are added to the
rewriting rule (whether these constraints are sufficient or not). E.g.
``1 / (1/ x) -> x { x <> 0 }``.

This warning is controlled by options :option:`-Wnull-denominator`
and :option:`-Wno-null-denominator`.

Warning: foo and bar are not trivially equal.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

When Gappa verifies the rule ``foo -> bar``, it first performs the
subtraction of both sides. Then it normalizes this expression in the
field of polynomial fractions with integer coefficients. If this result
is not zero, Gappa warns about it.

As the normalization only deals with polynomials and integers, false
positive may appear when the expressions involve numerical values or
square roots or absolute values.

.. code-block:: gappa

   { 1 in ? }
   x * (y - 2) -> x * y - x;  # not equal
   1b-2 -> 0.2 + 0.05;        # equal, but needs numerical computations
   sqrt(x * x) -> |x|;        # equal, but involves square root and absolute value

::

   Warning: x * (y - 2) and x * y - x are not trivially equal.
            Difference: -(x)
   Warning: 1b-2 and 2e-1 + 5e-2 are not trivially equal.
            Difference: -(2e-1) - (5e-2) + (1b-2)
   Warning: sqrt(x * x) and |x| are not trivially equal.
            Difference: (sqrt(x * x)) - (|x|)
   Results:
     1 in [1, 1]

This warning is controlled by options :option:`-Whint-difference`
and :option:`-Wno-hint-difference`.

Warning: bar is a variable without definition, yet it is unbound.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Identifier ``bar`` neither represents an expression nor is it a sub-term
of any of the bounded expressions of the logical property. This may mean
an identifier was mistyped.

.. code-block:: gappa

   { x - x in ? }

::

   Warning: x is a variable without definition, yet it is unbound.


This warning is controlled by options :option:`-Wunbound-variable`
and :option:`-Wno-unbound-variable`.

Warning: no path was found for foo.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

The expression ``foo`` appears in one of the goals, yet Gappa does not
have any theorem that could be used to compute this expression or one of
its sub-terms.

.. _warning-messages2:

Warning messages during proof computation
-----------------------------------------

Warning: when foo is in i1, bar cannot be proved.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

When Gappa applies a case splitting ``bar $ foo``, it splits the
interval of ``foo`` until the property about ``bar`` holds for any
sub-interval. If the maximal dichotomy depth has been reached yet the
property still does not hold, the warning message displays the failing
sub-interval (the leftmost one).

.. code-block:: gappa

   { x in [-2,1] -> x / x in [1,1] }
   x / x $ x;

::

   Warning: when x is in [-1b-99 {-1.57772e-30, -2^(-99)}, 1b-100 {7.88861e-31, 2^(-100)}], BND(x / x, [1, 1]) cannot be proved.
   Error: some properties were not satisfied:
     BND(x / x)

This warning is controlled by options :option:`-Wdichotomy-failure`
and :option:`-Wno-dichotomy-failure`.

Warning: case split on foo has not produced any interesting new result.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

This warning is displayed when Gappa is successful in finding a case
split that satisfies the goals, yet the results obtained on the
sub-intervals are not interesting: they have already been proved through
a simpler analysis.

.. code-block:: gappa

   { x in [1,2] -> x + 1 in ? }
   $ x;

::

   Warning: case split on x has not produced any interesting new result.
   Results:
     x + 1 in [2, 3]


This warning is controlled by options :option:`-Wdichotomy-failure`
and :option:`-Wno-dichotomy-failure`.

Warning: case split on foo has no range to split.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

This warning is displayed when Gappa is unable to find the initial range
on which to split cases.

.. code-block:: gappa

   { x in [-1,1] -> 1 in ? }
   $ 1 / x;

::

   Warning: case split on 1 / x has no range to split.
   Results:
     1 in [1, 1]


This warning is controlled by options :option:`-Wdichotomy-failure`
and :option:`-Wno-dichotomy-failure`.

Warning: case split on foo is not goal-driven anymore.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

This warning is displayed when Gappa is supposed to find the best case
split for proving a property, yet it does not know the range for this
property or it has already proved it.

.. code-block:: gappa

   { x in [-1,1] -> x + 1 in ? }
   x + 1 $ x;

::

   Warning: case split on x is not goal-driven anymore.
   Results:
     x + 1 in [0, 2]

This warning is controlled by options :option:`-Wdichotomy-failure`
and :option:`-Wno-dichotomy-failure`.