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

- Remove unused Output_Spec
- Add GenerateAnnotations and GenerateDeterministicLemmas
  true by default to preserve default behavior
- Move change_formals and change_result classes higher in the
  file to apply them as soon as possible in the pre/post generation
  phase
- This last step ensures that add_pre_post_from_buch actually only deals
  with specification, it is not responsible for remapping formals and
  return value anymore
- Now add_pre_post_from_buch can safely be disabled when
  GenerateAnnotations is false

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

- use more Cil smart constructors
- use an optional parameter for global variable initial values
- factorisation of common code

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

- add an "observables" option at the begining of ya files
- multiple "observables" options merges together (union of symbols)
- check that every function referred to is inside the observable list
- remove the initial curOperation and curOpStatus : the main function is
  not necessarily observable and the pre/post function will set those
  variables anyway
- ignore unobservables functions inside the relevant visitors

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

when an action is required for a transition in non-deterministic mode, it was
done before the test for updating the boolean variables representing active
state, leading to a possibly incorrect decision when said test depends on the
value of the variable modified by the action

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

(blind make headers from specifications)

- Fix Value/Value#5
- Fix Value/Value#14

Some case studies (e.g. dyad) use some ugly casts from fd_set_t which lead
to the analysis stopping too early.
Changing the representation of fd_set_t should also help it better conform to
the standard (since a fd_set_t should be able to hold FD_SETSIZE elements).