Merge branch 'bugfix/basile/eacsl-151-backtrace' into 'master'

[eacsl] Fix runtime backtraces

Closes e-acsl#151

See merge request frama-c/frama-c!3133

src/plugins/e-acsl/doc/Changelog

@@ -27,6 +27,10 @@ Plugin E-ACSL <next-release>
 
 -  E-ACSL       [2021-04-07] Add support for multiple binders in guarded
                 quantifications (frama-c/e-acsl#127).
+-* runtime      [2021-04-08] Fix backtrace output on failed assertion
+                (frama-c/e-acsl#151).
+-* runtime      [2021-04-08] Fix incorrect check on program arguments when the
+                main function takes no arguments (frama-c/e-acsl#151).
 -* runtime      [2021-03-30] Fix the end address of the memory segments in the
                 RTL layouts.
 -  E-ACSL       [2021-03-25] Add support for `check` and `admit` annotations

src/plugins/e-acsl/scripts/e-acsl-gcc.sh

@@ -803,8 +803,10 @@ fi
 # compilation
 if [ -n "$OPTION_RT_DEBUG" ]; then
   OPT_CFLAGS="-g3 -O0 -fno-omit-frame-pointer"
+  OPT_LDFLAGS="-no-pie"
 else
   OPT_CFLAGS="-g -O2"
+  OPT_LDFLAGS=""
 fi
 
 # Gcc and related flags
@@ -837,7 +839,8 @@ if [ "`basename $CC`" = 'clang' ]; then
 fi
 
 CPPFLAGS="$OPTION_CPPFLAGS"
-LDFLAGS="$OPTION_LDFLAGS"
+LDFLAGS="$OPTION_LDFLAGS
+  $OPT_LDFLAGS"
 
 # Dlmalloc
 if [ -n "$OPTION_WITH_DLMALLOC" ]; then

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;
 }