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 4 years ago and David Bühler committed 3 years ago

Due to the absence of a long double version of the pow() logic function,
and due to likely little demand for ldexpl, this function has not been
specified.

David Bühler authored 4 years ago and Loïc Correnson committed 4 years ago

The behaviors leading to forbidden floating-point values are now removed, and
the negation of their assumes are added as preconditions.

Fixes #877.

Nowadays, Metrics has option -metrics-no-libc to exclude definitions from
the Frama-C standard library, which was the purpose of the __FRAMA_C_MODEL__.
Also, several libc variables were lacking the attribute, leading to
inconsistent results.