[eacsl] Fix debug compilation

See merge request frama-c/frama-c!2893

[annotations] iter/fold_assigns filter out spurious WriteAnys

See merge request frama-c/frama-c!2884

Resolve "[wp] Corner cases with bitwise mask"

Closes #963

See merge request frama-c/frama-c!2877

Metavariables in Aorai

See merge request frama-c/frama-c!2098

Resolve "[nix] missing package zmq"

Closes #851

See merge request frama-c/frama-c!2889

[Ptests] show EXECNOW command when -show is set

See merge request frama-c/frama-c!2891

Actions are sequential, which means that `$x=foo; $y = $x;` must be specified
as `ensures aorai_y == aorai_x;`, not `\old(aorai_x)`.

it turns out that meta-variables can be modified through several transitions,
possibly with distinct end states. It is thus not possible to mention that
they are unchanged in behaviors that are grouped by the state at the end of
the call to the transition function.

This commit creates specific behaviors for indicating in which case an
auxiliary variable is unchanged.

Determistic C translation is now a series of `if ... else if ... else ...`
This avoids the need for auxiliary variables and inadvertently updating an
auxiliary variable that is used in a subsequent test.

Additionally, we have a marginally better ordering of tests wrt state numbering

Valentin Perrelle authored 4 years ago and Virgile Prevosto committed 4 years ago

- Use the same field "actions" for parsed and typed transitions
- Rename confusing types in Promelaast
- Reorganized Promelaoutput to mirror the naming convention