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

    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.

    a = 1;
    a = 1;

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

    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.

    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.

    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.

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

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

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

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

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

### Error: some properties 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.

    { 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 messages during parsing

### 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 `-Wnull-denominator` and `-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.

    { 1 in ? }
    x * (y - 2) -> x * y - x;  # not equal
    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: sqrt(x * x) and |x| are not trivially equal.
             Difference: -(|x|) + (sqrt(x * x))
    Results:
      1 in [1, 1]

This warning is controlled by options `-Whint-difference` and `-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.

    { x - x in ? }

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

This warning is controlled by options `-Wunbound-variable` and `-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 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).

    { 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 `-Wdichotomy-failure` and `-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.

    { 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 `-Wdichotomy-failure` and `-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.

    { 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 `-Wdichotomy-failure` and `-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 to prove a property, yet it does not know the range for this property or it has already proved it.

    { 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 `-Wdichotomy-failure` and `-Wno-dichotomy-failure`.