From 7f67a87725e4a3290d07237239772ff1c2701c32 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 26 Oct 2020 17:56:05 +0100
Subject: [PATCH] [eacsl] Add internal C defines to discriminate between OSes
---
src/plugins/e-acsl/headers/header_spec.txt | 1 +
.../share/e-acsl/internals/e_acsl_config.h | 66 +++++++++++++++++++
.../share/e-acsl/internals/e_acsl_trace.c | 5 +-
3 files changed, 70 insertions(+), 2 deletions(-)
create mode 100644 src/plugins/e-acsl/share/e-acsl/internals/e_acsl_config.h
diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
index cf2b2a13c0e..b7f88f446f5 100644
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ b/src/plugins/e-acsl/headers/header_spec.txt
@@ -21,6 +21,7 @@ share/e-acsl/instrumentation_model/e_acsl_temporal_timestamp.h: CEA_LGPL_OR_PROP
share/e-acsl/internals/e_acsl_alias.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/internals/e_acsl_bits.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/internals/e_acsl_bits.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+share/e-acsl/internals/e_acsl_config.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/internals/e_acsl_debug.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/internals/e_acsl_debug.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/internals/e_acsl_malloc.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_config.h b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_config.h
new file mode 100644
index 00000000000..7ab971cc8b2
--- /dev/null
+++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_config.h
@@ -0,0 +1,66 @@
+/**************************************************************************/
+/* */
+/* This file is part of the Frama-C's E-ACSL plug-in. */
+/* */
+/* Copyright (C) 2012-2020 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/**************************************************************************/
+
+/*! ***********************************************************************
+ * \file
+ * \brief Internal defines for E-ACSL set according to the current environment.
+ *
+ * Instead of using complicated logic with predefined macros in the RTL, the
+ * logic should be done in this file and an E-ACSL specific define set to record
+ * the result of the logic.
+ */
+
+#ifndef E_ACSL_CONFIG_H
+#define E_ACSL_CONFIG_H
+
+// OS detection
+// - Assign values to specific OSes
+#define E_ACSL_OS_LINUX_VALUE 1
+#define E_ACSL_OS_WINDOWS_VALUE 2
+#define E_ACSL_OS_OTHER_VALUE 999
+// - Declare defines to test for a specific OS
+/*!
+ * \brief True if the target OS is linux, false otherwise
+ */
+#define E_ACSL_OS_IS_LINUX E_ACSL_OS == E_ACSL_OS_LINUX_VALUE
+/*!
+ * \brief True if the target OS is windows, false otherwise
+ */
+#define E_ACSL_OS_IS_WINDOWS E_ACSL_OS == E_ACSL_OS_WINDOWS_VALUE
+/*!
+ * \brief True if the target OS is unknown, false otherwise
+ */
+#define E_ACSL_OS_IS_OTHER E_ACSL_OS == E_ACSL_OS_OTHER_VALUE
+// - Check current OS
+#ifdef __linux__
+// Linux compilation
+# define E_ACSL_OS E_ACSL_OS_LINUX_VALUE
+#elif defined(WIN32) || defined(_WIN32) || defined(__WIN32)
+// Windows compilation
+# define E_ACSL_OS E_ACSL_OS_WINDOWS_VALUE
+#else
+// Other
+# define E_ACSL_OS E_ACSL_OS_OTHER_VALUE
+# error "Unsupported OS for E-ACSL RTL"
+#endif
+
+#endif // E_ACSL_CONFIG_H
diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.c b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.c
index 892f53f5c20..486c9458cac 100644
--- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.c
+++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.c
@@ -28,6 +28,7 @@
#include <limits.h>
#include <stddef.h>
+#include "e_acsl_config.h"
#include "e_acsl_malloc.h"
#include "e_acsl_rtl_io.h"
#include "e_acsl_rtl_string.h"
@@ -71,7 +72,7 @@ static int native_backtrace (void **array, int size) {
}
void trace() {
-# ifdef __linux__
+# if E_ACSL_OS_IS_LINUX
int size = 24;
void **bb = private_malloc(sizeof(void*)*size);
@@ -107,5 +108,5 @@ void trace() {
counter++;
}
STDOUT("/***************************************/\n");
-# endif /* __linux__ */
+# endif /* E_ACSL_OS_IS_LINUX */
}
--
GitLab