From ec5918f54073c5b5342310984d75384a1718c07c Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 7 Apr 2021 11:53:22 +0200
Subject: [PATCH] [eacsl] Support main function without arguments
Add guards so that the addresses of `argc` and `argv` are only cheched
if `main()` has those arguments.
---
.../segment_model/e_acsl_shadow_layout.c | 26 ++++++++++++-------
1 file changed, 16 insertions(+), 10 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 7fbaa53abc2..cad865b1e71 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
@@ -97,16 +97,22 @@ static uintptr_t get_stack_start(int *argc_ref, char *** argv_ref) {
// 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);
+ if (argc_ref) {
+ 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\n",
+ stack_start, stack_end, argc_ref);
+ }
+ if (argv_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&argv: %a\n",
+ stack_start, stack_end, argv_ref);
+ }
return stack_start;
}
--
GitLab