as proposed in [MR](https://git.frama-c.com/frama-c/frama-c/-/merge_requests/2817#note_95099)

this is a generalization of `check` vs. `assert` to other annotations. Not all
annotations are relevant though. Currently, there are more annotation nodes in
the AST that can have a flag `{ tp_only_check }` than was deemed useful in
pub/frama-c#25, but said flag can in fact safely be ignored. Moreover, this
commit only add this flag in the AST, but provides no further mean to set it to
true except for the original `check` keyword (i.e. on `AAssert`). The parser
and the behavior of the plugins that can handle the flag will be updated in
subsequent commits

These aliases will not be printed in the help message of Eva, and will emit
a warning when used.

This is required to automatically unroll loops with conditions such as
`nondet && x < 100`, as this is converted by the Frama-C kernel as two
nested conditional statements, where only the second one can be used to
unroll the loop.

If the variable used in the exit condition of the loop is not incremented within
the loop, but is assigned to the value of another lvalue, the heuristic uses
this second lvalue instead.
This is especially useful to deal with some temporary variables introduced
by Frama-C to translate condition such as (i++ < l).

The exit condition of a loop can refer to a temporary variable that is not in
scope at the beginning of the loop. In this case, the exit condition cannot be
properly evaluated in the entry state of the loop, unless the variable is
introduced into the state.