David Bühler authored 3 years ago and Virgile Prevosto committed 3 years ago

Removes unused declarations in plugins registration files.

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

David Bühler authored 6 years ago and Virgile Prevosto committed 6 years ago

Asserts are both evaluated and used as hypotheses afterwards.
Checks are only evaluated, but are not used as hypotheses: they must not affect
the analyses.

(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).

[Ptests] preserve LOG after STDOPT directive

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

This is absolutely not a sneaky attempt to relaunch a build (now that OCI seems
in better shape) pushing a nearly empty commit.