[eacsl] Move assertion data to a separate C file

src/plugins/e-acsl/headers/header_spec.txt

@@ -14,6 +14,7 @@ man/e-acsl-gcc.sh.1: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 scripts/e-acsl-gcc.sh: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 share/e-acsl/instrumentation_model/e_acsl_assert.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 share/e-acsl/instrumentation_model/e_acsl_assert.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+share/e-acsl/instrumentation_model/e_acsl_assert_data.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 share/e-acsl/instrumentation_model/e_acsl_contract.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 share/e-acsl/instrumentation_model/e_acsl_contract.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 share/e-acsl/instrumentation_model/e_acsl_temporal.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL

src/plugins/e-acsl/share/e-acsl/e_acsl.h

@@ -81,6 +81,7 @@
 /************************************************************************/
 
 #include "instrumentation_model/e_acsl_assert.h"
+#include "instrumentation_model/e_acsl_assert_data.h"
 #include "observation_model/e_acsl_heap.h"
 
 /* }}} */

src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.h

@@ -29,9 +29,9 @@
 #define E_ACSL_ASSERT_H
 
 #include "../internals/e_acsl_alias.h"
+#include "e_acsl_assert_data.h"
 
 #define eacsl_runtime_sound_verdict export_alias(sound_verdict)
-#define eacsl_assert_data_t         export_alias(assert_data_t)
 #define eacsl_runtime_assert        export_alias(assert)
 
 /*! E-ACSL instrumentation automatically sets this global to 0 if its verdict
@@ -40,24 +40,6 @@
     For arithmetic properties, the verdict is always sound (?). */
 extern int __attribute__((FC_BUILTIN)) eacsl_runtime_sound_verdict;
 
-/*! Data holding context information for E-ACSL assertions. */
-typedef struct eacsl_assert_data_t {
-  /*! integer representing if the assertion is blocking or not */
-  int blocking;
-  /*! C string representing a kind of annotation (e.g., "Assertion") */
-  const char *kind;
-  /*! stringified predicate */
-  const char *pred_txt;
-  /*! un-instrumented file of predicate placement */
-  const char *file;
-  /*! function of predicate placement in the un-instrumented file */
-  const char *fct;
-  /*! line of predicate placement in the un-instrumented file */
-  int line;
-  /*! values contributing to the predicate */
-  void *values;
-} __attribute__((__FC_BUILTIN__)) eacsl_assert_data_t;
-
 /*! \brief Runtime assertion verifying a given predicate
  *  \param predicate integer code of a predicate
  *  \param data context data for the predicate. */

src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert_data.h

+/**************************************************************************/
+/*                                                                        */
+/*  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 E-ACSL data for assertions.
+ **************************************************************************/
+
+#ifndef E_ACSL_ASSERT_DATA_H
+#define E_ACSL_ASSERT_DATA_H
+
+#include "../internals/e_acsl_alias.h"
+
+#define eacsl_assert_data_t export_alias(assert_data_t)
+
+/*! Data holding context information for E-ACSL assertions. */
+typedef struct eacsl_assert_data_t {
+  /*! integer representing if the assertion is blocking or not */
+  int blocking;
+  /*! C string representing a kind of annotation (e.g., "Assertion") */
+  const char *kind;
+  /*! stringified predicate */
+  const char *pred_txt;
+  /*! un-instrumented file of predicate placement */
+  const char *file;
+  /*! function of predicate placement in the un-instrumented file */
+  const char *fct;
+  /*! line of predicate placement in the un-instrumented file */
+  int line;
+  /*! values contributing to the predicate */
+  void *values;
+} __attribute__((FC_BUILTIN)) eacsl_assert_data_t;
+
+#endif // E_ACSL_ASSERT_DATA_H