From bad771600a81f16d954b29568e0d89604d0617f0 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Tue, 21 Jun 2016 10:10:22 +0200
Subject: [PATCH] Fixed ordering of plugins
---
src/plugins/e-acsl/scripts/e-acsl-gcc.sh | 10 +++++-----
1 file changed, 5 insertions(+), 5 deletions(-)
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
index 93dcf2ceeda..e2a4a854fcf 100755
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
@@ -311,7 +311,8 @@ do
;;
--rte|-a)
shift
- OPTION_RTE="-rte -rte-mem -rte-no-float-to-int -no-warn-signed-overflow -no-warn-unsigned-overflow"
+ OPTION_RTE="-rte -rte-mem -rte-no-float-to-int
+ -no-warn-signed-overflow -no-warn-unsigned-overflow -then"
;;
# A memory model (or models) to link against
-m|--memory-model)
@@ -479,11 +480,10 @@ if [ -n "$OPTION_INSTRUMENT" ]; then
$OPTION_FRAMA_STDLIB \
$OPTION_FULL_MMODEL \
$OPTION_GMP \
- $OPTION_RTE \
"$@" \
- $OPTION_EACSL \
- -print \
- -ocode "$OPTION_OUTPUT_CODE");
+ $OPTION_RTE \
+ $OPTION_EACSL -then-last \
+ -print -ocode "$OPTION_OUTPUT_CODE");
error "aborted by Frama-C" $?;
# Print translated code
if [ -n "$OPTION_PRINT" ]; then
--
GitLab