New --no-trace option in e-acsl-gcc.sh

src/plugins/e-acsl/man/e-acsl-gcc.sh.1

@@ -49,6 +49,9 @@ By default no compilation is performed.
 Enable runtime debug features, i.e., compile unoptimized executable
 with assertions and extra checks.
 .TP
+.B --no-trace
+Disable stack trace reporting in debug mode
+.TP
 .B -V, --rt-verbose
 Output extra messages when executing generated code
 .TP

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

@@ -247,6 +247,11 @@ mmodel_features() {
   if [ -n "$OPTION_EXTERNAL_ASSERT" ]; then
     flags="$flags -DE_ACSL_EXTERNAL_ASSERT"
   fi
+
+  if [ -n "$OPTION_NO_TRACE" ]; then
+    flags="$flags -DE_ACSL_NO_TRACE"
+  fi
+
   echo $flags
 }
 
@@ -260,7 +265,7 @@ LONGOPTIONS="help,compile,compile-only,debug:,ocode:,oexec:,verbose:,
   frama-c:,gcc:,e-acsl-share:,instrumented-only,rte:,oexec-e-acsl:,
   print-mmodels,rt-debug,rte-select:,then,e-acsl-extra:,check,fail-with-code:,
   temporal,weak-validity,stack-size:,heap-size:,rt-verbose,free-valid-address,
-  external-assert:"
+  external-assert:,no-trace"
 SHORTOPTIONS="h,c,C,d:,D,o:,O:,v:,f,E:,L,M,l:,e:,g,q,s:,F:,m:,I:,G:,X,a:,T,k,V"
 # Prefix for an error message due to wrong arguments
 ERROR="ERROR parsing arguments:"
@@ -293,6 +298,7 @@ OPTION_WEAK_VALIDITY=                    # Use notion of weak validity
 OPTION_RTE=                              # Enable assertion generation
 OPTION_FAIL_WITH_CODE=                   # Exit status code for failures
 OPTION_CHECK=                            # Check AST integrity
+OPTION_NO_TRACE=                         # Disable trace in debug mode
 OPTION_FRAMAC_CPP_EXTRA=""               # Extra CPP flags for Frama-C
 OPTION_FREE_VALID_ADDRESS="" # Fail if NULL is used as input to free function
 OPTION_RTE_SELECT=       # Generate assertions for these functions only
@@ -605,6 +611,11 @@ do
       OPTION_EXTERNAL_ASSERT="$1"
       shift;
     ;;
+    # Disable trace in debug mode
+    --no-trace)
+      shift
+      OPTION_NO_TRACE=1
+    ;;
   esac
 done
 shift;

src/plugins/e-acsl/share/e-acsl/e_acsl_assert.h

@@ -54,7 +54,9 @@ static void vabort(char *fmt, ...);
 /* This ::exec_abort replaces `abort` via a macro at the top of this file */
 static void exec_abort(int line, const char *file) {
 #ifdef E_ACSL_DEBUG
+#ifndef E_ACSL_NO_TRACE
   trace();
+#endif
 #endif
   kill(getpid(), SIGABRT);
 }