Skip to content
Snippets Groups Projects
Commit 7a408d9b authored by Kostyantyn Vorobyov's avatar Kostyantyn Vorobyov Committed by Julien Signoles
Browse files

Brought forward changes from the segment-model remote: 

    - structural changes to e-acsl wrapper script
    - --memory-model option in the e-acsl wrapper script that allows
        switching between different memory models
    - added script to facilitate runs of e-acsl during
    testing (scripts/testrun.sh)
parent 814e52d1
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+ 129
− 39
View file @ 7a408d9b
......@@ -46,18 +46,25 @@ check_tool() {
# Getopt options
LONGOPTIONS="help,compile,compile-only,print,debug:,ocode:,oexec:,verbose:, \
frama-c-only,extra-cpp-args,rtl,frama-c-stdlib,full-mmodel,gmp,quiet,logfile:,
ld-flags:,cpp-flags:,frama-c-extra:"
SHORTOPTIONS="h,c,C,p,d:,o:,O:,v:,f,E:,R,L,M,l:,e:,g,q,s:,F:"
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:"
SHORTOPTIONS="h,c,C,p,d:,o:,O:,v:,f,E:,L,M,l:,e:,g,q,s:,F:,m:,P,N,D:"
# Prefix for an error message due to wrong arguments
ERROR="ERROR parsing arguments:"
# Frama-C
FRAMAC="`check_tool 'frama-c'`"
FRAMAC_CONGIG="`check_tool 'frama-c-config'`"
FRAMAC_FLAGS=""
FRAMA_C_SHARE="`$FRAMAC_CONGIG -print-share-path`"
# Architecture-dependent flags. Since by default Frama-C uses 32-bit
# architecture we need to make sure that same architecture is used for
# instrumentation and for compilation.
MACHDEPFLAGS="`getconf LONG_BIT`"
# Check if getconf gives out the value accepted by Frama-C/GCC
echo "$MACHDEPFLAGS" | grep '16\|32\|64' \
echo "$MACHDEPFLAGS" | grep '16\|32\|64' 2>&1 >/dev/null \
|| error "$MACHDEPFLAGS-bit architecture not supported"
# -machdep option sent to frama-c
MACHDEP="-machdep gcc_x86_$MACHDEPFLAGS"
......@@ -66,39 +73,58 @@ CPPMACHDEP="-D__FC_MACHDEP_X86_$MACHDEPFLAGS"
# GCC machine option
GCCMACHDEP="-m$MACHDEPFLAGS"
# Macro that identifies E-ACSL compilation. Passed to Framac and GCC runs
# but not to the original compilation
EACSL_MACRO_ID="__E_ACSL__"
# Gcc
CC="`check_tool 'gcc'`"
CFLAGS="-std=c99 $GCCMACHDEP -g3 -O2 -pedantic -fno-builtin -Wall \
-Wno-long-long \
-Wno-attributes \
-Wno-unused \
-Wno-unused-function \
-Wno-unused-result \
-Wno-unused-value \
-Wno-unused-function \
-Wno-unused-variable \
-Wno-unused-but-set-variable \
-Wno-implicit-function-declaration \
-Wno-attributes"
-Wno-implicit-function-declaration"
CPPFLAGS=""
LDFLAGS=""
# Frama-C
FRAMAC="`check_tool 'frama-c'`"
FRAMAC_CONGIG="`check_tool 'frama-c-config'`"
FRAMAC_FLAGS="-implicit-function-declaration ignore"
# E-ACSL source that needed for compilation
FRAMA_C_SHARE="`$FRAMAC_CONGIG -print-share-path`"
EACSL_SHARE="$FRAMA_C_SHARE/e-acsl"
RTL="$EACSL_SHARE/e_acsl.c \
$EACSL_SHARE/memory_model/e_acsl_mmodel.c \
$EACSL_SHARE/memory_model/e_acsl_bittree.c \
RTL_BITTREE="\
$EACSL_SHARE/e_acsl.c \
$EACSL_SHARE/memory_model/e_acsl_mmodel.c \
$EACSL_SHARE/memory_model/e_acsl_bittree.c \
"
RTL_SPLAYTREE="\
$EACSL_SHARE/e_acsl.c \
$EACSL_SHARE/memory_model/e_acsl_splay_tree.c \
$EACSL_SHARE/memory_model/e_acsl_mmodel.c \
"
RTL_TREE="\
$EACSL_SHARE/e_acsl.c \
$EACSL_SHARE/memory_model/e_acsl_tree.c \
$EACSL_SHARE/memory_model/e_acsl_mmodel.c \
"
RTL_LIST="\
$EACSL_SHARE/e_acsl.c \
$EACSL_SHARE/memory_model/e_acsl_list.c \
$EACSL_SHARE/memory_model/e_acsl_mmodel.c \
"
# CPP and LD flags for compilation of E-ACSL-generated sources
EACSL_CPP_FLAGS="
-D__FC_errno=(*__errno_location())
-D__builtin_printf=printf
-D__builtin_memcpy=memcpy"
EACSL_LD_FLAGS="-lgmp -lm"
RTL="$RTL_BITTREE"
# C, CPP and LD flags for compilation of E-ACSL-generated sources
EACSL_CFLAGS=""
EACSL_CPPFLAGS="
-I$EACSL_SHARE
-D$EACSL_MACRO_ID
-D__FC_errno=(*__errno_location())"
EACSL_LDFLAGS="-lgmp -lm"
# Variables holding getopt options
OPTION_FRAMAC_EXTRA= # Extra Frama-C options
......@@ -114,7 +140,14 @@ OPTION_EACSL="-e-acsl -then-last" # 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
OPTION_EXTRA_CPP="-I$FRAMA_C_SHARE/libc $CPPMACHDEP" # Extra CPP flags
OPTION_DEBUG_MACRO="-DE_ACSL_DEBUG" # Debug macro
OPTION_DEBUG_LOG_MACRO="" # Specification of debug log file
# The following option controls whether to use gcc builtins
# (e.g., __builtin_strlen) in RTL or fall back to custom implementations
# of standard functions.
OPTION_BUILTINS="-DE_ACSL_BUILTINS"
# Extra CPP flags for frama-c
OPTION_EXTRA_CPP="-D$EACSL_MACRO_ID -I$FRAMA_C_SHARE/libc $CPPMACHDEP"
manpage() {
echo "NAME"
......@@ -134,38 +167,56 @@ manpage() {
echo " compile input files as if they were generated by E-ACSL"
echo " -p, --print"
echo " output the code generated by E-ACSL to STDOUT"
echo " -d, --debug <N>"
echo " -d, --debug=<N>"
echo " pass a value to Frama-C -debug option"
echo " -o, --ocode <FILENAME>"
echo " -o, --ocode=<FILENAME>"
echo " name of the output source file, defaults to a.out.frama.c"
echo " -O, --oexec <FILENAME>"
echo " -O, --oexec=<FILENAME>"
echo " name of the executable generated from the un-instrumented code."
echo " Executable compiled from the E-ACSL instrumented sources is"
echo " appended .e.acsl suffix. Defaults to a.out and a.out.e-acsl"
echo " -v, --verbose <N>"
echo " -v, --verbose=<N>"
echo " pass a value to Frama-C -verbose option"
echo " -f, --frama-c-only"
echo " run input source files through Frama-C without E-ACSL"
echo " -E, --extra-cpp-args <FLAGS>"
echo " -E, --extra-cpp-args=<FLAGS>"
echo " pass additional arguments to the Frama-C pre-processor"
echo " -R, --rtl"
echo " output E_ACSL runtime libraries to STDOUT"
echo " -L, --frama-c-stdlib"
echo " use Frama-C standard library"
echo " -M, --full-mmodel"
echo " maximise memory-related instrumentation"
echo " -g, --gmp"
echo " always use GMP integers instead of C integral types"
echo " -l, --ld-flags <FLAGS>"
echo " -l, --ld-flags=<FLAGS>"
echo " pass the specified flags to the linker"
echo " -e, --cpp-flags <FLAGS>"
echo " -e, --cpp-flags=<FLAGS>"
echo " pass the specified flags to the pre-processor (compile-time)"
echo " -q, --quiet"
echo " suppress any output except for errors and warnings"
echo " -s, --logfile <FILE>"
echo " -s, --logfile=<FILE>"
echo " redirect all output to a given log file"
echo " -F, --frama-c-extra <OPTION>"
echo " pass an extra option to frama-c invocation"
echo " -m, --memory-model=<bittree|tree|list|splaytree>"
echo " memory model (i.e., runtime library) to be used at compile time."
echo " Valid arguments are:"
echo " bittree - memory modelling using a Patricie trie ADT"
echo " splaytree - memory modelling using a splay tree ADT"
echo " list - memory modelling using a linked-list ADT"
echo " tree - memory modelling using a binary tree ADT"
echo " -P, --production"
echo " Compile optimized executatle without debug features"
echo " -N, --no-stdlib"
echo " If specified the E-ACSL run-time library uses custom "
echo " implementations of standard library functions (such as memset)."
echo " By default GCC builtins are used (e.g., __builtin_memset)."
echo " -D, --debug-log=<FILE>"
echo " Specify the name of the file for logging of debugging output of"
echo " modified modified executables. If '-' is specified then the"
echo " output is redirected to the standard error stream. By default "
echo " /tmp/e-acsl.log file is used. Note that this option is meaningful"
echo " in the absence of the -P flag, which diables debug logging for "
echo " performance reasons."
echo ""
echo "EXAMPLES:"
echo " # Instrument foo.c and output the instrumented code to a.out.frama.c"
......@@ -275,7 +326,7 @@ do
# Additional CPP arguments
--extra-cpp-args|-E)
shift;
OPTION_EXTRA_CPP="$OPTION_EXTRA_CPP$1"
OPTION_EXTRA_CPP="$OPTION_EXTRA_CPP $1"
shift;
;;
# Additional flags passed to the linker
......@@ -303,11 +354,6 @@ do
shift;
OPTION_EACSL=
;;
# Output the RTL files
--rtl|-R)
echo $RTL
exit 0;
;;
# Do use Frama-C stdlib, which is the default behaviour of Frama-C
--frama-c-stdlib|-L)
shift;
......@@ -323,6 +369,41 @@ do
shift;
OPTION_GMP="-e-acsl-gmp-only"
;;
-P|--production)
shift;
OPTION_DEBUG_MACRO=""
;;
-N|--no-stdlib)
shift;
OPTION_BUILTINS=""
;;
-D|--debug-log)
shift;
OPTION_DEBUG_LOG_MACRO="-DE_ACSL_DEBUG_LOG=$1"
shift;
;;
-m|--memory-model)
shift;
mmodel="$1"
shift;
case $mmodel in
bittree)
RTL="$RTL_BITTREE"
;;
splaytree)
RTL="$RTL_SPLAYTREE"
;;
tree)
RTL="$RTL_TREE"
;;
list)
RTL="$RTL_LIST"
;;
*)
error "Unknown model memory model: '$mmodel'"
;;
esac
;;
esac
done
shift;
......@@ -368,8 +449,17 @@ if test -n "$OPTION_COMPILE" ; then
OPTION_OCODE="$@"
fi
# Compile and link E-ACSL-instrumented file
($OPTION_ECHO; $CC $CPPFLAGS $CFLAGS $EACSL_CPP_FLAGS $RTL \
"$OPTION_OCODE" -o "$OPTION_OEXEC.e-acsl" $LDFLAGS $EACSL_LD_FLAGS)
($OPTION_ECHO; \
$CC \
$CFLAGS $CPPFLAGS \
$EACSL_CFLAGS $EACSL_CPPFLAGS \
$RTL \
$OPTION_DEBUG_MACRO \
$OPTION_DEBUG_LOG_MACRO \
$OPTION_BUILTINS \
-o "$OPTION_OEXEC.e-acsl" \
"$OPTION_OCODE" \
$LDFLAGS $EACSL_LDFLAGS)
error "fail to compile/link instrumented code: $@" $?;
fi
exit 0;
src/plugins/e-acsl/scripts/testrun.sh 0 → 100755
+ 97
− 0
View file @ 7a408d9b
##########################################################################
# #
# This file is part of the Frama-C's E-ACSL plug-in. #
# #
# Copyright (C) 2012-2015 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
# you can redistribute it and/or modify it under the terms of the GNU #
# Lesser General Public License as published by the Free Software #
# Foundation, version 2.1. #
# #
# It is distributed in the hope that it will be useful, #
# but WITHOUT ANY WARRANTY; without even the implied warranty of #
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
# GNU Lesser General Public License for more details. #
# #
# See the GNU Lesser General Public License version 2.1 #
# for more details (enclosed in the file license/LGPLv2.1). #
# #
##########################################################################
#!/bin/sh -e
# Convenience script for running tests with E-ACSL. Given a source file the
# sequence is as follows:
# 1. Perform E-ACSL instrumentation
# 2. Compile instrumented and original files
# 3. Compare outputs of the above
# Arguments:
# $1 - base name of the source file to use (e.g., addrOf)
# $2 - base name of the test suite directory the test file is located in.
# (for instance e-acsl-runtime). Provided that ROOT is the directory
# holding the E-ACSL repository there should be either:
# $ROOT/test/e-acsl-runtime/addrOf.i or
# $ROOT/test/e-acsl-runtime/addrOf.c
# $3 - if specified this script re-runs test sequence generating using
# -e-acsl-gmp-only option
PREFIX="$1" # Prefix (test suite) directory, e.g., bts, e-acsl-runtime
TEST="$2" # Based name of the test file with extension stripped
GMP="$3" # Whether to use a subsequent run with -e-acsl-gmp-only
ROOTDIR="`readlink -f $(dirname $0)/../`" # Root directory of the repository
TESTDIR="$ROOTDIR/tests/$PREFIX"
RESDIR=$TESTDIR/result # result directory within the test suite
TESTFILE=`ls $TESTDIR/$TEST.[ic]` # Source test file
MODEL="bittree" # Memory model to link against.
LOG="$RESDIR/$TEST.testrun" # Base name for log files
OUT="$RESDIR/gen_$TEST" # Base name for output
RUNS=1
# Remove all old logs and executables before running new tests
rm -f $LOG.* $OUT.*
# Error reporting
error() {
echo "Error: $1" 1>&2
echo "See $2 for details" 1>&2
exit 1
}
# Instrument the given test using e-acsl-gcc.sh and compare outputs of the
# executables generated from instrumented and non-instrumented sources
run_test() {
local ocode=$OUT.$RUNS.c # Generated source file
local logfile=$LOG.$RUNS.elog # Log file for e-acsl-gcc.sh output
local oexec=$OUT.$RUNS.out # Generated executable name
local oexeclog=$LOG.$RUNS.rlog # Log for executable output
local extra="$1" # Additional arguments to e-acsl-gcc.sh
# Command for instrumenting the source file and compiling the original
# and the instrumented code
EACSL_GCC="e-acsl-gcc.sh
--compile $TESTFILE --ocode=$ocode --logfile=$logfile
--memory-model=$MODEL --oexec=$oexec $extra"
$EACSL_GCC || error "Command $EACSL_GCC failed" "$logfile"
# Log outputs of the generated executables
$oexec 2>&1 > $oexeclog.native
$oexec.e-acsl 2>&1 > $oexeclog.e-acsl
## Make sure that instrumented and uninstrumented programs have same outputs
diff $oexeclog.native $oexeclog.e-acsl ||
error "Output of programs before and after instrumentation differ" \
"output of $oexec and $oexec.e-acsl"
RUNS=$((RUNS+1))
}
run_test
if test -n "$GMP"; then
run_test "--gmp"
fi
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment