Skip to content

Commit 0196cb2

Browse files
committed
do_SRPM: Rebase to newer upstream release
* Update csexec-symbiotic.sh
1 parent 8a39b9a commit 0196cb2

File tree

2 files changed

+26
-45
lines changed

2 files changed

+26
-45
lines changed

csexec-symbiotic.sh

Lines changed: 23 additions & 44 deletions
Original file line numberDiff line numberDiff line change
@@ -2,59 +2,38 @@
22

33
usage() {
44
cat << EOF
5-
USAGE:
5+
USAGE: $0 -s SYMBIOTIC_ARGS ARGV
66
1) Build the source with gllvm and CFLAGS internally used by Symbiotic and
77
LDFLAGS='-Wl,--dynamic-linker=/usr/bin/csexec-loader'.
8-
2) CSEXEC_WRAP_CMD=$'csexec-symbiotic.sh\a--prp=memsafety' make check
8+
2) CSEXEC_WRAP_CMD=$'--skip-ld-linux\acsexec-symbiotic\a-s\a--prp=memsafety' make check
99
3) Wait for some time.
1010
4) ...
1111
5) Profit!
1212
EOF
1313
}
1414

15-
if [ $# -eq 0 ]; then
16-
usage
17-
exit 1
18-
fi
19-
20-
if [ ! -x /usr/bin/get-bc ]; then
21-
echo "gllvm is not installed!" > /dev/tty
22-
exit 42
23-
fi
24-
25-
i=1
26-
while [ ! -e ${!i} ]; do
27-
SYMBIOTIC_ARGS[$i - 1]="${!i}"
28-
((i++))
15+
[[ $# -eq 0 ]] && usage && exit 1
16+
17+
while getopts "s:h" opt; do
18+
case "$opt" in
19+
s)
20+
SYMBIOTIC=($OPTARG)
21+
;;
22+
h)
23+
usage && exit 0
24+
;;
25+
*)
26+
usage && exit 1
27+
;;
28+
esac
2929
done
3030

31-
# Skip LD_LINUX_SO
32-
((i++))
33-
34-
# Skip --argv0
35-
if [ ${!i} = "--argv0" ]; then
36-
((i += 2))
37-
fi
38-
39-
BINARY="${!i}"
40-
((i++))
41-
42-
BINARY_ARGV="${!i}"
43-
((i++))
31+
shift $((OPTIND - 1))
32+
ARGV=("$@")
4433

45-
while [ $i -le $# ]; do
46-
BINARY_ARGV="$BINARY_ARGV,${!i}"
47-
((i++))
48-
done
49-
50-
get-bc "$BINARY" 1> /dev/tty 2>&1
51-
echo "Executing 'symbiotic${SYMBIOTIC_ARGS[*]} --argv='$BINARY_ARGV' $BINARY.bc'" 1> /dev/tty 2>&1
52-
symbiotic "${SYMBIOTIC_ARGS[@]}" --argv="'$BINARY_ARGV'" "$BINARY.bc" 1> /dev/tty 2>&1
53-
54-
i=1
55-
while [[ ! "${!i}" =~ "ld-linux" ]]; do
56-
((i++))
57-
done
34+
# Run!
35+
get-bc "${ARGV[0]}" 1> /dev/tty 2>&1
36+
symbiotic "${SYMBIOTIC[@]}" --argv="'${ARGV[*]}'" "${ARGV[0]}.bc" 1> /dev/tty 2>&1
5837

59-
ARGS=( "$@" )
60-
exec "${ARGS[@]:i-1}"
38+
# Continue
39+
exec $(csexec --print-ld-exec-cmd) "${ARGV[@]}"

do_SRPM.sh

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
set -e
44

55
# upstream revision to checkout
6-
SYMBIOTIC_REV="svcomp19-715-gad622b5"
6+
SYMBIOTIC_REV="svcomp19-718-g6c18930"
77

88
rm -rf srpm
99
mkdir srpm
@@ -81,6 +81,7 @@ BuildRequires: glibc-devel
8181
BuildRequires: glibc-devel(x86-32)
8282
BuildRequires: jsoncpp-devel
8383
BuildRequires: llvm-devel
84+
BuildRequires: make
8485
BuildRequires: ncurses-devel
8586
BuildRequires: python3
8687
BuildRequires: sqlite-devel
@@ -89,6 +90,7 @@ BuildRequires: zlib-devel
8990
9091
Requires: clang
9192
Requires: llvm
93+
Requires: python3
9294
9395
%description
9496
Symbiotic is a tool for analysis of sequential computer programs written in the programming language C. It can check all common safety properties like assertion violations, invalid pointer dereference, double free, memory leaks, etc.

0 commit comments

Comments
 (0)