From 3f781f5018cc2eedb6669e84cfaa3c3f81b29b3f Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Thu, 3 Dec 2020 15:25:42 +0100
Subject: [PATCH] [eacsl] Check assumption in get_stack_start
---
.../segment_model/e_acsl_shadow_layout.c | 18 ++++++++++++++++--
1 file changed, 16 insertions(+), 2 deletions(-)
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c
index fa02c208e9d..5ddb496007a 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c
@@ -79,8 +79,8 @@ extern char ** environ;
/*! \brief Return the greatest (known) address on a program's stack.
* This function presently determines the address using the address of the
* last string in `environ`. That is, it assumes that argc and argv are
- * stored below environ, which holds for GCC/Glibc but is not necessarily
- * true for some other compilers/libraries. */
+ * stored below environ, which holds for GCC or Clang and Glibc but is not
+ * necessarily true for some other compilers/libraries. */
static uintptr_t get_stack_start(int *argc_ref, char *** argv_ref) {
char **env = environ;
while (env[1])
@@ -94,6 +94,20 @@ static uintptr_t get_stack_start(int *argc_ref, char *** argv_ref) {
* ::argv_alloca. */
uintptr_t stack_end = addr + ULONG_BITS;
uintptr_t stack_start = stack_end - get_stack_size();
+
+ // Check that the assumption that argc and argv are stored below environ in
+ // the stack holds
+ DVASSERT(stack_start <= (uintptr_t)argc_ref
+ && (uintptr_t)argc_ref <= stack_end,
+ "Assumption that argc is stored below environ is not verified.\n\
+ \tStack: [%a - %a]\n\t&argc: %a",
+ stack_start, stack_end, argc_ref);
+ DVASSERT(stack_start <= (uintptr_t)argv_ref
+ && (uintptr_t)argv_ref <= stack_end,
+ "Assumption that argv is stored below environ is not verified.\n\
+ \tStack: [%a - %a]\n\t&argc: %a",
+ stack_start, stack_end, argc_ref);
+
return stack_start;
}
/* }}} */
--
GitLab