diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog index 983c1997b76c402a2a1d853195e0453e6ec2a2a8..8fed599b80e26fcb87b3f3cf7fc0e4475e1f9975 100644 --- a/src/plugins/e-acsl/doc/Changelog +++ b/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 diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh index 45d8ddb1222d13c2d6dddff5eca2ba1201ecdda5..d0cbd0bb70852e85ca6c150ce75e16275a6495ff 100755 --- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh +++ b/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 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 7fbaa53abc297c342d9687ada805a2e20df1d3b7..cad865b1e71e191097478ce3cbb751f3ff758765 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; }