There are still many missing specifications, but at least parsing should
succeed for strictly POSIX-compliant code.

Frama-C does not yet support _Alignof and _Alignas, but this header helps
parsing code and emitting a proper error message.

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.

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.