Skip to content

Improve position information for CIF invariants

From the output of !582 (merged):

WARNING:   --------------------------------------------------------
WARNING:   (2/2) Requirement invariant will be explored as a plant.
WARNING:   --------------------------------------------------------
WARNING:    * In the top-level scope of the specification:
WARNING:      - requirement invariant r1.x + r2.x >= 0;
WARNING:                                          ^
WARNING:    * In automaton "r1":
WARNING:      - requirement invariant x >= 0;
WARNING:                                ^
WARNING:      - requirement invariant x >= 0;
WARNING:                                ^
WARNING:    * In automaton "r2":
WARNING:      - requirement invariant x >= 0;
WARNING:                                ^
WARNING:    * In location "r2.loc":
WARNING:      - requirement invariant x >= 0;
WARNING:                                ^
WARNING:      - requirement invariant x <= 1 div x;
WARNING:                                ^

The position information for invariants should not be on the predicate, but on one of the keywords.