[e-acsl-gcc.sh] Functionality specify several models via -m option

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

@@ -74,7 +74,8 @@ OPTION_GMP=                              # Use GMP integers everywhere
 OPTION_DEBUG_MACRO="-DE_ACSL_DEBUG"      # Debug macro
 OPTION_DEBUG_LOG_MACRO=""                # Specification of debug log file
 OPTION_FRAMAC_CPP_EXTRA=""               # Extra CPP flags for Frama-C
-OPTION_EACSL_MMODEL="bittree"            # Memory model used
+OPTION_EACSL_MMODELS="bittree"           # Memory model used
+OPTION_EACSL_SHARE=                      # Custom E-ACSL share directory
 # The following option controls whether to use gcc builtins
 # (e.g., __builtin_strlen) in RTL or fall back to custom implementations
 # of standard functions.
@@ -280,12 +281,11 @@ do
       OPTION_EACSL_SHARE="$1"
       shift;
     ;;
-    # A memory model to link against
+    # A memory model  (or models) to link against
     -m|--memory-model)
       shift;
-      echo $1 | grep "\(tree\|bittree\|splaytree\|list\|segment\)"
-      error "no such memory model: $1" $?
-      OPTION_EACSL_MMODEL="$1"
+      # Convert comma-separated string into white-space separated string
+      OPTION_EACSL_MMODELS="`echo $1 | sed -s 's/,/ /g'`"
       shift;
     ;;
   esac
@@ -345,6 +345,38 @@ else
   fi
 fi
 
+# Check if the E-ACSL share directory is indeed an E-ACSL share directory that
+# contains required C code. The check involves looking up
+# $EACSL_SHARE/e_acsl_mmodel_api.h - one of the headers required by the Frama-C
+# invocation. This is a week check but it is better than nothing.
+error "Cannot find required $EACSL_SHARE/e_acsl_mmodel_api.h header" \
+  `test -f $EACSL_SHARE/e_acsl_mmodel_api.h; echo $?`
+
+# Echo the name of the source file corresponding to the name of a memory model
+# or report an error of the given model does not exist.
+mmodel_sources() {
+  model=""
+  case "$1" in
+    bittree) model="adt_models/e_acsl_bittree_mmodel.c" ;;
+    splaytree) model="adt_models/e_acsl_splaytree_mmodel.c" ;;
+    tree) model="adt_models/e_acsl_tree_mmodel.c" ;;
+    list) model="adt_models/e_acsl_list_mmodel.c" ;;
+    foo) model="adt_models/e_acsl_foo_mmodel.c" ;;
+    *) error "Memory model '$1' does not exist" ;;
+  esac
+  model="$EACSL_SHARE/$model"
+  if ! [ -f "$model" ]; then
+    error "Memory model '$1' exists but not available in this distribution"
+  else
+    echo "$model"
+  fi
+}
+
+# Once EACSL_SHARE is defined check the memory models provided at inputs
+for mod in $OPTION_EACSL_MMODELS; do
+  mmodel_sources $mod > /dev/null
+done
+
 # Macro that identifies E-ACSL compilation. Passed to Frama-C
 # and GCC runs but not to the original compilation
 EACSL_MACRO_ID="__E_ACSL__"
@@ -352,7 +384,7 @@ EACSL_MACRO_ID="__E_ACSL__"
 # Gcc and related flags
 CC="$OPTION_CC"
 CFLAGS="$OPTION_CFLAGS
-  -std=c99 $GCCMACHDEP -g3 -O2 -pedantic -fno-builtin -w
+  -std=c99 $GCCMACHDEP -g3 -O2 -pedantic -fno-builtin
   -Wall \
   -Wno-long-long \
   -Wno-attributes \
@@ -365,7 +397,6 @@ CFLAGS="$OPTION_CFLAGS
   -Wno-unused-variable \
   -Wno-unused-but-set-variable \
   -Wno-implicit-function-declaration \
-  -Wno-extra-semi \
   -Wno-empty-body"
 
 # Disable extra warning for clang
@@ -388,13 +419,6 @@ EACSL_CPPFLAGS="
   -D__FC_errno=(*__errno_location())"
 EACSL_LDFLAGS="-lgmp -lm"
 
-# Memory model sources
-if [ $OPTION_EACSL_MMODEL = "segment" ]; then
-  error "Segment model not available in this distribution"
-else
-  EACSL_RTL="$EACSL_SHARE/adt_models/e_acsl_"$OPTION_EACSL_MMODEL"_mmodel.c"
-fi
-
 # Output file names
 OUTPUT_CODE="$OPTION_OUTPUT_CODE" # E-ACSL instrumented source
 OUTPUT_EXEC="$OPTION_OUTPUT_EXEC" # Output name of the original executable
@@ -435,18 +459,30 @@ if [ -n "$OPTION_COMPILE" ]; then
   else
     OUTPUT_CODE="$@"
   fi
-  # Compile and link E-ACSL-instrumented file
-  ($OPTION_ECHO;
-   $CC \
-     $CFLAGS $CPPFLAGS \
-     $EACSL_CFLAGS $EACSL_CPPFLAGS \
-     $EACSL_RTL \
-     $OPTION_DEBUG_MACRO \
-     $OPTION_DEBUG_LOG_MACRO \
-     $OPTION_BUILTINS \
-     -o "$EACSL_OUTPUT_EXEC" \
-     "$OUTPUT_CODE" \
-     $LDFLAGS $EACSL_LDFLAGS)
-  error "fail to compile/link instrumented code: $@" $?;
+  # Compile and link E-ACSL-instrumented file with all models specified
+  for mod in $OPTION_EACSL_MMODELS; do
+    # If multiple models are specified then the generated executable
+    # is appended a '-MODEL' suffix, where MODEL is the name of the memory
+    # model used
+    if ! [ "`echo $OPTION_EACSL_MMODELS | wc -w`" = 1 ]; then
+      OUTPUT_EXEC="$EACSL_OUTPUT_EXEC-$mod"
+    else
+      OUTPUT_EXEC="$EACSL_OUTPUT_EXEC"
+    fi
+    # Sources of the selected memory model
+    EACSL_RTL=`mmodel_sources "$mod"`
+    ($OPTION_ECHO;
+     $CC \
+       $CFLAGS $CPPFLAGS \
+       $EACSL_CFLAGS $EACSL_CPPFLAGS \
+       $EACSL_RTL \
+       $OPTION_DEBUG_MACRO \
+       $OPTION_DEBUG_LOG_MACRO \
+       $OPTION_BUILTINS \
+       -o "$OUTPUT_EXEC" \
+       "$OUTPUT_CODE" \
+       $LDFLAGS $EACSL_LDFLAGS)
+    error "fail to compile/link instrumented code: $@" $?;
+  done
 fi
 exit 0;