From a3eb75e335b46cd6b9085f80a40addb51424f8f8 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu, 18 Nov 2021 17:40:46 +0100
Subject: [PATCH] [Libc] avoid spurious uninitialized warnings from the
 compiler

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.
---
 share/libc/stdatomic.c                 | 12 ++++++------
 tests/libc/oracle/fc_libc.0.res.oracle |  4 ++--
 tests/libc/oracle/fc_libc.1.res.oracle | 12 ++++++------
 3 files changed, 14 insertions(+), 14 deletions(-)

diff --git a/share/libc/stdatomic.c b/share/libc/stdatomic.c
index caaeb092968..5121379c4eb 100644
--- a/share/libc/stdatomic.c
+++ b/share/libc/stdatomic.c
@@ -60,7 +60,7 @@ unsigned long long __fc_atomic_load_explicit(void *object,
 unsigned long long __fc_atomic_exchange(void *obj,
                                         unsigned long long desired,
                                         size_t obj_size) {
-  unsigned long long r;
+  unsigned long long r = 0;
   if (obj_size == sizeof(char)) {
     r = *((volatile atomic_uchar *)obj);
     *((volatile atomic_uchar *)obj) = desired;
@@ -120,7 +120,7 @@ _Bool __fc_atomic_compare_exchange_weak_explicit(void *object, void *expected,
 
 unsigned long long __fc_atomic_fetch_add(void *obj, unsigned long long operand,
                                          size_t obj_size) {
-  unsigned long long r;
+  unsigned long long r = 0;
   if (obj_size == sizeof(char)) {
     r = *((volatile atomic_uchar *)obj);
     *((volatile atomic_uchar *)obj) += operand;
@@ -149,7 +149,7 @@ unsigned long long __fc_atomic_fetch_add_explicit(void *obj,
 
 unsigned long long __fc_atomic_fetch_sub(void *obj, unsigned long long operand,
                                          size_t obj_size) {
-  unsigned long long r;
+  unsigned long long r = 0;
   if (obj_size == sizeof(char)) { r = *((volatile atomic_uchar *)obj);
     *((volatile atomic_uchar *)obj) -= operand; }
   else if (obj_size == sizeof(short)) { r =  *((volatile atomic_ushort *)obj);
@@ -173,7 +173,7 @@ unsigned long long __fc_atomic_fetch_sub_explicit(void *obj,
 
 unsigned long long __fc_atomic_fetch_or(void *obj, unsigned long long operand,
                                         size_t obj_size) {
-  unsigned long long r;
+  unsigned long long r = 0;
   if (obj_size == sizeof(char)) { r = *((volatile atomic_uchar *)obj);
     *((volatile atomic_uchar *)obj) |= operand; }
   else if (obj_size == sizeof(short)) { r =  *((volatile atomic_ushort *)obj);
@@ -197,7 +197,7 @@ unsigned long long __fc_atomic_fetch_or_explicit(void *obj,
 
 unsigned long long __fc_atomic_fetch_xor(void *obj, unsigned long long operand,
                                          size_t obj_size) {
-  unsigned long long r;
+  unsigned long long r = 0;
   if (obj_size == sizeof(char)) {
     r = *((volatile atomic_uchar *)obj);
     *((volatile atomic_uchar *)obj) ^= operand;
@@ -228,7 +228,7 @@ unsigned long long __fc_atomic_fetch_xor_explicit(void *obj,
 unsigned long long __fc_atomic_fetch_and(void *obj,
                                          unsigned long long operand,
                                          size_t obj_size) {
-  unsigned long long r;
+  unsigned long long r = 0;
   if (obj_size == sizeof(char)) {
     r = *((volatile atomic_uchar *)obj);
     *((volatile atomic_uchar *)obj) &= operand;
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 297a5e0531d..cd64f335d70 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -213,13 +213,13 @@
   
   Global metrics
   ============== 
-  Sloc = 1641
+  Sloc = 1647
   Decision point = 307
   Global variables = 86
   If = 292
   Loop = 55
   Goto = 118
-  Assignment = 711
+  Assignment = 717
   Exit point = 128
   Function = 556
   Function call = 165
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 7053e853eee..36845c92b12 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -5865,7 +5865,7 @@ unsigned long long __fc_atomic_exchange(void *obj,
                                         unsigned long long desired,
                                         size_t obj_size)
 {
-  unsigned long long r;
+  unsigned long long r = (unsigned long long)0;
   if (obj_size == sizeof(char)) {
     r = (unsigned long long)*((atomic_uchar volatile *)obj);
     *((atomic_uchar volatile *)obj) = (unsigned char)desired;
@@ -5953,7 +5953,7 @@ unsigned long long __fc_atomic_fetch_add(void *obj,
                                          unsigned long long operand,
                                          size_t obj_size)
 {
-  unsigned long long r;
+  unsigned long long r = (unsigned long long)0;
   if (obj_size == sizeof(char)) {
     r = (unsigned long long)*((atomic_uchar volatile *)obj);
     *((atomic_uchar volatile *)obj) = (unsigned char)((unsigned long long)*((atomic_uchar volatile *)obj) + operand);
@@ -5996,7 +5996,7 @@ unsigned long long __fc_atomic_fetch_sub(void *obj,
                                          unsigned long long operand,
                                          size_t obj_size)
 {
-  unsigned long long r;
+  unsigned long long r = (unsigned long long)0;
   if (obj_size == sizeof(char)) {
     r = (unsigned long long)*((atomic_uchar volatile *)obj);
     *((atomic_uchar volatile *)obj) = (unsigned char)((unsigned long long)*((atomic_uchar volatile *)obj) - operand);
@@ -6039,7 +6039,7 @@ unsigned long long __fc_atomic_fetch_or(void *obj,
                                         unsigned long long operand,
                                         size_t obj_size)
 {
-  unsigned long long r;
+  unsigned long long r = (unsigned long long)0;
   if (obj_size == sizeof(char)) {
     r = (unsigned long long)*((atomic_uchar volatile *)obj);
     *((atomic_uchar volatile *)obj) = (unsigned char)((unsigned long long)*((atomic_uchar volatile *)obj) | operand);
@@ -6082,7 +6082,7 @@ unsigned long long __fc_atomic_fetch_xor(void *obj,
                                          unsigned long long operand,
                                          size_t obj_size)
 {
-  unsigned long long r;
+  unsigned long long r = (unsigned long long)0;
   if (obj_size == sizeof(char)) {
     r = (unsigned long long)*((atomic_uchar volatile *)obj);
     *((atomic_uchar volatile *)obj) = (unsigned char)((unsigned long long)*((atomic_uchar volatile *)obj) ^ operand);
@@ -6125,7 +6125,7 @@ unsigned long long __fc_atomic_fetch_and(void *obj,
                                          unsigned long long operand,
                                          size_t obj_size)
 {
-  unsigned long long r;
+  unsigned long long r = (unsigned long long)0;
   if (obj_size == sizeof(char)) {
     r = (unsigned long long)*((atomic_uchar volatile *)obj);
     *((atomic_uchar volatile *)obj) = (unsigned char)((unsigned long long)*((atomic_uchar volatile *)obj) & operand);
-- 
GitLab