From 89bb646167bf80ef789e44e8d08ef65349dd7ba5 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Fri, 24 Jun 2016 12:56:30 +0200
Subject: [PATCH] Fine-grained asserion generation for e-acsl-gcc

---
 src/plugins/e-acsl/scripts/e-acsl-gcc.sh | 89 +++++++++++++++++++-----
 1 file changed, 70 insertions(+), 19 deletions(-)

diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
index e2a4a854fcf..eae3b80c4d7 100755
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
@@ -52,6 +52,57 @@ check_tool() {
    { has_tool "$1" || test -e "$1"; } || error "No executable $1 found";
 }
 
+# build and output option string for RTE plugin based on a comma-delimited
+# option string
+rte_options() {
+  local optstring="$1"
+  local start="-rte -rte-warn"
+  local opts="-rte-no-all"
+  # RTE integer overflow options coming from Frama-C, presently
+  # they are enabled by default, so they should be negated
+  local intopts="-no-warn-signed-overflow -no-warn-unsigned-overflow"
+  local vopts="mem,int,float,div,ret,precond,shift,all"
+  local all=""
+
+  for opt in $(echo $optstring | tr ',' ' '); do
+    case $opt in
+      mem) # valid pointer or array access
+        opts="$opts -rte-mem"
+      ;;
+      int) # integer overflows
+        intopts=""
+      ;;
+      float) # casts from floating-point to integer
+        opts="$opts -rte-float-to-int"
+      ;;
+      div) # division by zero
+        opts="$opts -rte-div"
+      ;;
+      ret) # return
+      ;;
+      precond) # function calls based on contracts
+        opts="$opts -rte-precond"
+      ;;
+      shift) # left and right shifts by a value out of bounds
+        opts="$opts -rte-shift"
+      ;;
+      all) # all assertions
+        all=1
+      ;;
+      *)
+        return 1;
+      ;;
+    esac
+  done
+
+  if [ -n "$all" ]; then
+    echo $start -rte-all -then
+  else
+    echo $start $opts $intopts -then
+  fi
+  return 0;
+}
+
 # Check if getopt is GNU
 required_tool getopt "util-linux"
 required_tool readlink "GNU coreutils"
@@ -60,8 +111,8 @@ required_tool readlink "GNU coreutils"
 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:,instrumented-only,rte,oexec-e-acsl:"
-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,a"
+  debug-log:,frama-c:,gcc:,e-acsl-share:,instrumented-only,rte:,oexec-e-acsl:"
+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,a:"
 # Prefix for an error message due to wrong arguments
 ERROR="ERROR parsing arguments:"
 
@@ -80,7 +131,7 @@ OPTION_COMPILE=                          # Compile instrumented program
 OPTION_OUTPUT_CODE="a.out.frama.c"       # Name of the translated file
 OPTION_OUTPUT_EXEC="a.out"               # Generated executable name
 OPTION_EACSL_OUTPUT_EXEC=""              # Name of E-ACSL executable
-OPTION_EACSL="-e-acsl -then-last"        # Specifies E-ACSL run
+OPTION_EACSL="-e-acsl"                   # Specifies E-ACSL run
 OPTION_FRAMA_STDLIB="-no-frama-c-stdlib" # Use Frama-C stdlib
 OPTION_FULL_MMODEL=                      # Instrument as much as possible
 OPTION_GMP=                              # Use GMP integers everywhere
@@ -127,14 +178,6 @@ BASEDIR="$(readlink -f `dirname $0`)"
 # Directory with contrib libraries of E-ACSL
 LIBDIR="$BASEDIR/../lib"
 
-# See if pygmentize if available for color highlighting and default to plain
-# cat command otherwise
-if has_tool 'pygmentize'; then
-  CAT="pygmentize -g -O style=colorful,linenos=1"
-else
-  CAT="cat"
-fi
-
 # Run getopt
 ARGS=`getopt -n "$ERROR" -l "$LONGOPTIONS" -o "$SHORTOPTIONS" -- "$@"`
 
@@ -310,9 +353,10 @@ do
       shift;
     ;;
     --rte|-a)
-      shift
-      OPTION_RTE="-rte -rte-mem -rte-no-float-to-int
-        -no-warn-signed-overflow -no-warn-unsigned-overflow -then"
+      shift;
+      OPTION_RTE=`rte_options $1`
+      error "Invalid argument $1 to --rte|-a option" $?
+      shift;
     ;;
     # A memory model  (or models) to link against
     -m|--memory-model)
@@ -467,6 +511,15 @@ else
     EACSL_OUTPUT_EXEC="$OPTION_EACSL_OUTPUT_EXEC"
 fi
 
+# Build E-ACSL plugin argument string
+if [ -n "$OPTION_EACSL" ]; then
+  OPTION_EACSL="
+    $OPTION_EACSL
+    $OPTION_GMP
+    $OPTION_FULL_MMODEL
+    -then-last"
+fi
+
 # Instrument
 if [ -n "$OPTION_INSTRUMENT" ]; then
   ($OPTION_ECHO; \
@@ -475,19 +528,17 @@ if [ -n "$OPTION_INSTRUMENT" ]; then
     $MACHDEP \
     -cpp-extra-args="$OPTION_FRAMAC_CPP_EXTRA" \
     -e-acsl-share=$EACSL_SHARE \
+    $OPTION_FRAMA_STDLIB \
     $OPTION_VERBOSE \
     $OPTION_DEBUG \
-    $OPTION_FRAMA_STDLIB \
-    $OPTION_FULL_MMODEL \
-    $OPTION_GMP \
     "$@" \
     $OPTION_RTE \
-    $OPTION_EACSL -then-last \
+    $OPTION_EACSL \
     -print -ocode "$OPTION_OUTPUT_CODE");
     error "aborted by Frama-C" $?;
   # Print translated code
   if [ -n "$OPTION_PRINT" ]; then
-    $CAT $OPTION_OUTPUT_CODE
+    cat $OPTION_OUTPUT_CODE
   fi
 fi
 
-- 
GitLab