From db20590247f7d55c970e879e2e5c21374352938f Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Mon, 6 Mar 2017 10:19:46 +0100
Subject: [PATCH] Refactor valid and valid_read using allocated
---
.../segment_model/e_acsl_segment_mmodel.c | 33 +++++--------------
1 file changed, 8 insertions(+), 25 deletions(-)
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 8ef1e350f1e..06de2ff3008 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
@@ -77,31 +77,6 @@ static void mark_readonly(void * ptr) {
/* E-ACSL annotations */
/* ****************** */
-static int valid(void * ptr, size_t size, void *ptr_base, void *addr_of_base) {
- uintptr_t addr = (uintptr_t)ptr;
- uintptr_t base = (uintptr_t)ptr_base;
- if (IS_ON_HEAP(addr))
- return heap_allocated(addr, size, base);
- else if (IS_ON_STACK(addr) || IS_ON_TLS(addr))
- return static_allocated(addr, size, base);
- else if (IS_ON_GLOBAL(addr))
- return static_allocated(addr, size, base) && !global_readonly(addr);
- else if (!IS_ON_VALID(addr))
- return 0;
- return 0;
-}
-
-static int valid_read(void * ptr, size_t size, void *ptr_base, void *addr_of_base) {
- uintptr_t addr = (uintptr_t)ptr;
- uintptr_t base = (uintptr_t)ptr_base;
- TRY_SEGMENT_WEAK(addr,
- return heap_allocated(addr, size, base),
- return static_allocated(addr, size, base));
- if (!IS_ON_VALID(addr))
- return 0;
- return 0;
-}
-
/** \brief Return 1 if a given memory location is read-only and 0 otherwise */
static int readonly (void *ptr) {
uintptr_t addr = (uintptr_t)ptr;
@@ -109,6 +84,14 @@ static int readonly (void *ptr) {
return IS_ON_GLOBAL(addr) && global_readonly(addr) ? 1 : 0;
}
+static int valid(void * ptr, size_t size, void *ptr_base, void *addr_of_base) {
+ return allocated((uintptr_t)ptr, size, (uintptr_t)ptr_base) && !readonly(ptr);
+}
+
+static int valid_read(void * ptr, size_t size, void *ptr_base, void *addr_of_base) {
+ return allocated((uintptr_t)ptr, size, (uintptr_t)ptr_base);
+}
+
/*! NB: The implementation for this function can also be specified via
* \p base_addr macro that will eventually call ::TRY_SEGMENT. The following
* implementation is preferred for performance reasons. */
--
GitLab