Merge branch 'feature/kostyantyn/e-acsl-gcc' into 'master'

An e-acsl-gcc.sh option to skip compilation of original source files and generate an instrumented executable only



See merge request !40

src/plugins/e-acsl/doc/Changelog

@@ -24,6 +24,8 @@
 Plugin E-ACSL 0.6 Magnesium
 ###########################
 
+-* E-ACSL       [2016/01/22] Added an e-acsl-gcc.sh option allowing to skip
+	        compilation of original sources.
 -* E-ACSL       [2016/01/15] Fix installation with custom --prefix.
 -* E-ACSL       [2016/01/05] Fix bug in the memory model that caused the
 	        tracked size of heap memory be computed incorrectly.

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

@@ -45,6 +45,10 @@ show a help page.
 compile the generated and the original (supplied) sources.
 By default no compilation is performed.
 .TP
+.B -X, --instrumented-only
+Do not compile original code. Has effect only in the presence of the \fI-c\fP
+flag.
+.TP
 .B -C, --compile-only
 compile the input files as if they were generated by \fBE-ACSL\fP.
 .TP

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

@@ -48,8 +48,8 @@ check_tool() {
 LONGOPTIONS="help,compile,compile-only,print,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:,production,no-stdlib,
-  debug-log:,frama-c:,gcc:,e-acsl-share:"
-SHORTOPTIONS="h,c,C,p,d:,o:,O:,v:,f,E:,L,M,l:,e:,g,q,s:,F:,m:,P,N,D:I:G:"
+  debug-log:,frama-c:,gcc:,e-acsl-share:,instrumented-only"
+SHORTOPTIONS="h,c,C,p,d:,o:,O:,v:,f,E:,L,M,l:,e:,g,q,s:,F:,m:,P,N,D:,I:,G:,X"
 # Prefix for an error message due to wrong arguments
 ERROR="ERROR parsing arguments:"
 
@@ -76,6 +76,7 @@ OPTION_DEBUG_LOG_MACRO=""                # Specification of debug log file
 OPTION_FRAMAC_CPP_EXTRA=""               # Extra CPP flags for Frama-C
 OPTION_EACSL_MMODELS="bittree"           # Memory model used
 OPTION_EACSL_SHARE=                      # Custom E-ACSL share directory
+OPTION_INSTRUMENTED_ONLY=                # Do not compile original code
 # The following option controls whether to use gcc builtins
 # (e.g., __builtin_strlen) in RTL or fall back to custom implementations
 # of standard functions.
@@ -234,6 +235,11 @@ do
       shift;
       OPTION_EACSL=
     ;;
+    # Do not compile original source file
+    --instrumented-only|-X)
+      shift;
+      OPTION_INSTRUMENTED_ONLY=1
+    ;;
     # Do use Frama-C stdlib, which is the default behaviour of Frama-C
     --frama-c-stdlib|-L)
       shift;
@@ -449,7 +455,7 @@ fi
 if [ -n "$OPTION_COMPILE" ]; then
   # Compile the original files only if the instrumentation option is given,
   # otherwise the provided sources are assumed to be E-ACSL instrumented files
-  if [ -n "$OPTION_INSTRUMENT" ]; then
+  if [ -n "$OPTION_INSTRUMENT" ] && [ -z "$OPTION_INSTRUMENTED_ONLY" ]; then
     ($OPTION_ECHO; $CC $CPPFLAGS $CFLAGS "$@" -o "$OUTPUT_EXEC" $LDFLAGS);
     error "fail to compile/link un-instrumented code: $@" $?;
   else