New option allowing to exit instead of fail on assertion violation

src/plugins/e-acsl/doc/Changelog

@@ -19,6 +19,7 @@
 Plugin E-ACSL Phosphorus-20170515
 #################################
 
+-! E-ACSL       [2017/05/29] Add --fail-with-code option to e-acsl.gcc.sh
 -! E-ACSL       [2017/05/19] Add --temporal option to e-acsl.gcc.sh
 -! E-ACSL       [2017/05/19] Enable analysis for temporal errors in E-ACSL
 -! E-ACSL       [2017/03/26] Add --weak-validity option to e-acsl.gcc.sh

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

@@ -159,6 +159,10 @@ Set the size (in MB) of the heap shadow space
 .B -k, --keep-going
 Continue execution after an assertion failure
 .TP
+.B --fail-with-code=\fI<NUMBER>
+On assertion failure exit with the given integer code intead of raising an abort
+signal
+.TP
 .B -m, --memory-model=\fI<model>
 memory model (i.e., a runtime library for checking memory related annotations)
 to be linked against the instrumented file.

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

@@ -233,6 +233,10 @@ mmodel_features() {
     flags="$flags -DE_ACSL_VERBOSE -DE_ACSL_DEBUG_VERBOSE"
   fi
 
+  if [ -n "$OPTION_FAIL_WITH_CODE" ]; then
+    flags="$flags -DE_ACSL_FAIL_EXITCODE=$OPTION_FAIL_WITH_CODE "
+  fi
+
   if [ -n "$OPTION_WEAK_VALIDITY" ]; then
     flags="$flags -DE_ACSL_WEAK_VALIDITY"
   fi
@@ -246,8 +250,8 @@ check_getopt;
 LONGOPTIONS="help,compile,compile-only,debug:,ocode:,oexec:,verbose:,
   frama-c-only,extra-cpp-args:,frama-c-stdlib,full-mmodel,gmp,quiet,logfile:,
   ld-flags:,cpp-flags:,frama-c-extra:,memory-model:,keep-going,
-  frama-c:,gcc:,e-acsl-share:,instrumented-only,rte:,oexec-e-acsl:
-  print-mmodels,rt-debug,rte-select:,then,e-acsl-extra:,check,
+  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"
 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
@@ -279,6 +283,7 @@ OPTION_INSTRUMENTED_ONLY=                # Do not compile original code
 OPTION_TEMPORAL=                         # Enable temporal analysis
 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_FRAMAC_CPP_EXTRA=""               # Extra CPP flags for Frama-C
 OPTION_RTE_SELECT=       # Generate assertions for these functions only
@@ -541,6 +546,16 @@ do
       shift;
       OPTION_KEEP_GOING=1
     ;;
+    # Exit with a given code on assertion failure instead of raising abort
+    --fail-with-code)
+      shift;
+      if [ "$1" -eq "$1" ] 2>/dev/null; then
+        OPTION_FAIL_WITH_CODE="$1"
+      else
+        error "--fail-with-code option requires integer argument"
+      fi
+      shift;
+    ;;
     # Use notion of weak validity
     --weak-validity)
       shift;

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

@@ -94,8 +94,12 @@ void runtime_assert(int predicate, char *kind, char *fct, char *pred_txt, int li
   if (!predicate) {
       STDERR("%s failed at line %d in function %s.\n"
         "The failing predicate is:\n%s.\n", kind, line, fct, pred_txt);
-#ifndef E_ACSL_NO_ASSERT_FAIL
-    runtime_abort();
+#ifndef E_ACSL_NO_ASSERT_FAIL /* Do fail on assertions */
+#ifdef E_ACSL_FAIL_EXITCODE /* Fail by exit with a given code */
+    exit(E_ACSL_FAIL_EXITCODE);
+#else
+    runtime_abort(); /* Raise abort signal */
+#endif
 #endif
   }
 }

src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c

@@ -68,6 +68,8 @@
  *    Assertions:
  *      E_ACSL_NO_ASSERT_FAIL - do not issue abort signal of E-ACSL
  *        assertion failure
+ *      E_ACSL_FAIL_EXITCODE - do not issue abort signal but exit with a
+ *        given code
  *    Shadow spaces (only for segment model):
  *      E_ACSL_STACK_SIZE - size (in MB) of the tracked program stack
  *      E_ACSL_HEAP_SIZE - size (in MB) of the tracked program heap