- always remove FC's internal attribute everywhere before deciding whether
  a cast is needed.
- ACSL and C decisions to cast are similar
- only unroll type for checking equality. If a cast is needed, keep
  typedef (if any) as target

Clang 13 emits warnings related to uninitialized variables:

variable 'r' is used uninitialized whenever 'if'
condition is false [-Wsometimes-uninitialized]

This is due to the fact that the assert(0) macro, when using Frama-C's libc,
is expanded to __FC_assert. Since it is not known by the compiler, it cannot
consider it as "noreturn" when the condition is zero. Note that adding
'__attribute__ ((__noreturn__))' will not work: Frama-C will assume it
never returns, even when the condition is true.
Initializing the 'r' variables with a default value will not change the
actual behavior, and will avoid the warnings.

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.

it's pointless to be accurate for the ERANGE case while our current
modelization can't tell whether we will succeed in opening the
corresponding file in /proc.