Eva relies on the inout plugin to ensure that a function call has not modified
the values of its concrete arguments, meaning that at the end of the call, the
values of formal parameters can be backward propagated to the corresponding
concrete arguments. This is useful when the values of some parameters have been
reduced by the call, for instance by some preconditions.

To this end, Eva uses the Inout callback Record_Inout_Callbacks from Db, but
this callback was only applied by Inout for functions whose body is analyzed.

This commit modifies Inout to also record its result through this callback
on functions interpreted by a builtin or a specification, thus allowing a
precise backward propagation of the values of formal parameters to concrete
arguments in all cases.

For the functions [use_spec_instead_of_definition] and [no_results].

- lints some files

Removes optional argument [access] from [as_zone].

Adds function [as_zone_result] that returns a zone result, without converting
error cases.

Changes the Inout plugin accordingly.

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

Removes unused declarations in plugins registration files.

Type [cacheable] is now defined in Eval.
Type [call_result] is defined in Builtins.
Changes the type of callbacks Db.Call_Type_Value_Callbacks.

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

  and also some libraries

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

Handles \exit_status exactly as \result.

Fixes a performance issue.

- shares and moves the functions [reduce_offset_by_validity] of Locations and
  Precise_locs into base.ml.
- replaces the boolean argument ~for_writing into the new type access, that
  represents Read, Write or No_access. Without any access, offsets must point
  into or just beyond the base validity.
- fixes the support of accesses of size 0: they are now invalid:
  + in bases with Invalid validity;
  + one past a base validity unless the base ends with an empty struct.

Initialized const variables should be included as outputs of the function.