Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
F
frama-c
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Container Registry
Model registry
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
pub
frama-c
Commits
a24e600c
Commit
a24e600c
authored
9 years ago
by
Kostyantyn Vorobyov
Browse files
Options
Downloads
Patches
Plain Diff
[testrun.sh] Improved reporting during test failures
parent
1baf1ac8
No related branches found
No related tags found
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
src/plugins/e-acsl/scripts/testrun.sh
+45
-23
45 additions, 23 deletions
src/plugins/e-acsl/scripts/testrun.sh
with
45 additions
and
23 deletions
src/plugins/e-acsl/scripts/testrun.sh
+
45
−
23
View file @
a24e600c
...
...
@@ -39,7 +39,7 @@
# $3 - if specified this script re-runs test sequence generating using
# -e-acsl-gmp-only option
# $4 - extra flags for e-acsl-gcc.sh
# $5 - debug flag
# $5 - debug flag
- pring extra messages and retain log files
set
-e
...
...
@@ -50,38 +50,61 @@ EXTRA="$4" # Extra flags for e-acsl-gcc.sh
DEBUG
=
"
$5
"
# Debug flag
ROOTDIR
=
"
`
readlink
-f
$(
dirname
$0
)
/../
`
"
# Root directory of the repository
TESTDIR
=
"
$ROOTDIR
/tests/
$PREFIX
"
RESDIR
=
$TESTDIR
/result
#
r
esult directory within the test suite
TESTDIR
=
"
$ROOTDIR
/tests/
$PREFIX
"
# Test suite directory
RESDIR
=
$TESTDIR
/result
#
R
esult directory within the test suite
TESTFILE
=
`
ls
$TESTDIR
/
$TEST
.[ic]
`
# Source test file
MODEL
=
"bittree"
# Memory model to link against
.
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
RUNS
=
1
# Nth run of `run_test` function
# Print a message if the DEBUG flag is set
debug
()
{
if
[
-n
"
$DEBUG
"
]
;
then
echo
"
$1
"
1>&2
echo
" ** DEBUG:
$1
"
1>&2
fi
}
# Clean up log/output files unless the DEBUG flag is set
clean
()
{
if
[
-z
"
$DEBUG
"
]
;
then
rm
-f
$LOG
.
*
$OUT
.
*
fi
}
# Error reporting
# $1 - error message
# $2 - log file. If supplied the contents of the log file are dumpmed to
# STDERR with each line prefixed by ' > '.
error
()
{
echo
"Error:
$1
"
1>&2
debug
"See
$2
for details"
if
[
-n
"
$2
"
]
;
then
cat
$2
2>&1 |
sed
's/^/ > /'
1>&2
debug
"See
$2
for details"
fi
exit
1
}
# Clean up log/output files unless the DEBUG flag is set
clean
()
{
if
[
-z
"
$DEBUG
"
]
;
then
rm
-f
$LOG
.
*
$OUT
.
*
fi
}
# Do clean up on exit
trap
"clean"
EXIT HUP INT QUIT TERM
# Run executable and report results
# $1 - path to an executable
# $2 - file for logging the outputs of the command
# $3 - the type of the executable (e.g., original executable
# or an executable generated from the instrumented sources)
run_executable
()
{
local
executable
=
"
$1
"
local
log
=
"
$2
"
local type
=
"
$3
"
debug
"Run and log
$executable
"
if
!
`
$executable
>
$log
2>&1
`
;
then
error
"[
$3
run]: Runtime failure in test case
$TEST
:"
$log
fi
}
# Instrument the given test using e-acsl-gcc.sh and compare outputs of the
# executables generated from instrumented and non-instrumented sources
run_test
()
{
...
...
@@ -93,27 +116,26 @@ run_test() {
# Command for instrumenting the source file and compiling the original
# and the instrumented code
EACSL_GCC
=
"./scripts/e-acsl-gcc.sh
--compile
$TESTFILE
--ocode=
$ocode
--logfile=
$logfile
EACSL_GCC
=
"./scripts/e-acsl-gcc.sh
\
--compile
$TESTFILE
--ocode=
$ocode
--logfile=
$logfile
\
--memory-model=
$MODEL
--oexec=
$oexec
$extra
"
debug
"Run
$EACSL_GCC
"
$EACSL_GCC
||
error
"Command
$EACSL_GCC
failed"
"
$logfile
"
# Log outputs of the generated executables
debug
"Run and log native execution to
$oexeclog
.native"
$oexec
>
$oexeclog
.native 2>&1
debug
"Run and log E-ACSL execution to
$oexeclog
.e-acsl"
$oexec
.e-acsl
>
$oexeclog
.e-acsl 2>&1
run_executable
$oexec
$oexeclog
.native
"Native"
run_executable
$oexec
.e-acsl
$oexeclog
.e-acsl
"Instrumented"
## Make sure that instrumented and uninstrumented programs have same outputs
d
iff
$oexeclog
.native
$oexec
log
.e-acsl
||
error
"Output of programs before and after instrumentation differ"
\
"
o
utput of
$oexec
and
$oexec
.e-acsl"
d
ebug
"Compare outputs of
$oexec
and
$oexec
.e-acsl
"
diff
-ur
-N
$oexeclog
.native
$oexeclog
.e-acsl
>
$oexeclog
.diff 2>&1
||
\
error
"
O
utput of
instrumented and original programs differ"
$oexeclog
.diff
RUNS
=
$((
RUNS+1
))
}
# Run GMP tests if specified
run_test
"
$EXTRA
"
if
test
-n
"
$GMP
"
;
then
run_test
"--gmp
$EXTRA
"
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment