From dee0778ab39b4b864de74e3a314bec392b71a34c Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Thu, 15 Jun 2017 10:53:20 +0200
Subject: [PATCH] E-ACSL variables for floating point types
---
.../bittree_model/e_acsl_bittree_mmodel.c | 1 +
.../share/e-acsl/e_acsl_floating_point.h | 68 +++++++++++++++++++
.../e-acsl/share/e-acsl/e_acsl_mmodel_api.h | 22 ++++++
src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c | 1 +
.../segment_model/e_acsl_segment_mmodel.c | 1 +
5 files changed, 93 insertions(+)
create mode 100644 src/plugins/e-acsl/share/e-acsl/e_acsl_floating_point.h
diff --git a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
index ea0f5a8d451..8bdf605326c 100644
--- a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
+++ b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
@@ -597,6 +597,7 @@ void memory_init(int *argc_ref, char ***argv_ref, size_t ptr_size) {
if (safe_locations[i].is_initialized)
initialize(addr, len);
}
+ init_infinity_values();
}
/* }}} */
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_floating_point.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_floating_point.h
new file mode 100644
index 00000000000..b34817af827
--- /dev/null
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_floating_point.h
@@ -0,0 +1,68 @@
+/**************************************************************************/
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2017 */
+/* 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 e_acsl_floating_point.h
+ * \brief Functionality related to processing of floating point values
+***************************************************************************/
+
+#ifndef E_ACSL_FLOATING_POINT_H
+#define E_ACSL_FLOATING_POINT_H
+
+#include "e_acsl_mmodel_api.h"
+#include <math.h>
+#include <float.h>
+
+/* Below variables hold infinity values for floaing points defined in math.h.
+ Most of them are defined as macros that expand to built-in function calls.
+ As such, they cannot be used in E-ACSL specifications directly. To solve
+ the issue this header provides alternative definitions prefixed
+ __e_acsl_math_. For instance, if a call to `pow` overflows it
+ returns `HUGE_VAL`. To make sure that the result of pow does not overflow
+ one can use the following assertion
+
+ extern double __e_acsl_math_HUGE_VAL;
+ ...
+ double x = 500000000.0;
+ double y = 500000000.0;
+ double z = pow(x,y);
+ //@assert z != 0.0 && z != __e_acsl_math_HUGE_VAL;
+*/
+
+/** \brief Positive infinity for doubles: same as HUGE_VAL */
+double math_HUGE_VAL = 0.0;
+/** \brief Positive infinity for floats: same as HUGE_VALF */
+float math_HUGE_VALF = 0.0;
+/** \brief Positive infinity for long doubles: same as HUGE_VALL */
+long double math_HUGE_VALL = 0.0;
+/** \brief Representation of infinity value for doubles: same as INFINITY */
+double math_INFINITY = 0.0;
+
+/* Initialize E-ACSL infinity values */
+static void init_infinity_values() {
+ math_HUGE_VAL = HUGE_VAL;
+ math_HUGE_VALF = HUGE_VALF;
+ math_HUGE_VALL = HUGE_VALL;
+ math_INFINITY = INFINITY;
+}
+
+#endif
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
index 649e522b701..b31b8d4bdcf 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
@@ -75,6 +75,11 @@
#define temporal_reset_return export_alias(temporal_reset_return)
#define temporal_memcpy export_alias(temporal_memcpy)
#define temporal_memset export_alias(temporal_memset)
+/* Infinity values for floating point types */
+#define math_HUGE_VAL export_alias(math_HUGE_VAL)
+#define math_HUGE_VALF export_alias(math_HUGE_VALF)
+#define math_HUGE_VALL export_alias(math_HUGE_VALL)
+#define math_INFINITY export_alias(math_INFINITY)
/******************************/
/* Dedicated E-ACSL assertion */
@@ -295,6 +300,23 @@ extern size_t heap_allocation_size;
\at(heap_allocation_size, L1)
- \at(heap_allocation_size, L2) == i; */
+/************************************************************************/
+/************ Machine-dependent infinity values for flating points ******/
+/************************************************************************/
+
+/* Positive infinity for doubles: same as HUGE_VAL */
+extern double math_HUGE_VAL
+ __attribute__((FC_BUILTIN));
+/* Positive infinity for floats: same as HUGE_VALF */
+extern float math_HUGE_VALF
+ __attribute__((FC_BUILTIN));
+/* Positive infinity for long doubles: same as HUGE_VALL */
+extern long double math_HUGE_VALL
+ __attribute__((FC_BUILTIN));
+/* Representation of infinity value for doubles: same as INFINITY */
+extern double math_INFINITY
+ __attribute__((FC_BUILTIN));
+
/***********************************************/
/************ Temporal analysis API ************/
/***********************************************/
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c b/src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c
index 68fef6584c6..740c9da96ca 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c
@@ -39,6 +39,7 @@
#include "e_acsl_shexec.h"
#include "e_acsl_trace.h"
#include "e_acsl_assert.h"
+#include "e_acsl_floating_point.h"
#include "e_acsl_safe_locations.h"
#include "e_acsl_temporal_timestamp.h"
#include "e_acsl_mmodel_api.h"
diff --git a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c
index 0f98f6cca72..3ca4e0ecfeb 100644
--- a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c
+++ b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c
@@ -229,6 +229,7 @@ void memory_init(int *argc_ref, char *** argv_ref, size_t ptr_size) {
if (safe_locations[i].is_initialized)
initialize(addr, len);
}
+ init_infinity_values();
}
void memory_clean(void) {
--
GitLab