'Indeterminate' alarms are alarms about uninitialized memory, escaping pointers
and special floating-point values (infinite and NaN).

These alarms are emitted for functions specified by -eva-warn-copy-indeterminate
option, which is @all by default. These alarms can be disabled for some function
by -eva-warn-copy-indeterminate=-f, in which case they are also disabled for
the argument expressions of calls to [f].

However:
- the @all default value did not include functions without definition
  (for which a specification or a builtin is used).
- 'indeterminate' alarms were emitted anyway for the arguments of calls to
  functions without definition, except for builtins.
So no indeterminate alarms were emitted for the argument expressions of calls
to builtins (unless their definitions were included).

This commit fixes this behavior:
the @all default of -eva-warn-copy-indeterminate option include all functions
and special case for functions without definition or builtins are removed.

It still avoids to emit surch alarms on Eva directives such as Frama_C_show_each.

[Libc] add specs for tan* functions

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

The preconditions generated in place of behaviors leading to NaN or infinite
floating-point values are now named.

Andre Maroneze authored 3 years ago and David Bühler committed 3 years ago

The Linux manpage for tan states that only a floating-point exception
(FE_OVERFLOW) occurs in case of result overflow, but the POSIX manpage mentions
that errno can be set to ERANGE.

[Kernel] improve error message related to GCC/MSVC machdeps

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

Renames the function [allowed_machdep].

Feature/andre/z to int opt

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

Removes exception ParseIntError.
Restores the previous behavior of parseInt that aborts Frama-C in case of
failure.
Renames parseInt_opt into parseIntRes that returns [Error message] in
case of failure.

Creates missing .mli interface files

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

[wp] Add axioms about bitwise operator idempotence

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

[Cabs2cil] warn about local typedefs

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