Newer
Older
#!/bin/bash
##########################################################################
# #
# This file is part of Frama-C. #
# #
# 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 licenses/LGPLv2.1). #
# #
##########################################################################
# Accept '-check' to avoid issues with ptests
while [ $# -ge 1 -a "$1" = "-check" ]; do
shift
done
echo "usage: $0 cmd [args]"
echo ""
echo " where cmd is:"
echo ""
echo " - help"
echo " Display this help message and exit."
echo ""
echo " - make-template [dir]"
echo " Interactively prepares a template for analyses,"
echo " writing it to dir/GNUmakefile [default: .frama-c]."
echo ""
echo " - list-files [path/to/compile_commands.json]"
echo " Lists all sources in the given compile_commands.json"
echo " [default: ./compile_commands.json]."
echo " Also lists files defining a 'main' function"
echo " (heuristics-based; neither correct nor complete)."
echo ""
echo " - flamegraph flamegraph.txt [dir]"
echo " Generates flamegraph.svg and flamegraph.html in dir"
echo " [default: FRAMAC_SESSION]."
echo " Also opens it in a browser, unless variable NOGUI is set."
Andre Maroneze
committed
echo ""
echo " - find-fun function-name [dir...]"
echo " Lists files in dir... declaring or defining function-name"
echo " [default: PWD /usr/include]."
Andre Maroneze
committed
echo " Heuristics-based: neither correct nor complete."
echo ""
echo " - summary [options]"
echo " Monitors and summarizes multiple analyses dispatched by a Makefile"
echo " in the current PWD."
echo " Use $0 summary --help for more informations."
echo " Runs an existing configure script to only consider files"
echo " in Frama-C's libc; this will hopefully disable non-essential"
echo " and non-POSIX external libraries."
echo " (run 'frama-c -machdep help' to get the list of machdeps)."
echo ""
echo " - make-wrapper target arg..."
echo " Runs 'make target arg...', parsing the output to suggest"
echo " useful commands in case of failure."
echo ""
echo " - normalize-jcdb [path/to/compile_commands.json]"
echo " Applies some transformations to an existing compile_commands.json"
echo " (such as relativizing paths) to improve portability."
echo " [default: ./compile_commands.json]"
exit $1
}
if [ $# -lt 1 ]; then
usage 1
fi
DIR="$( cd "$( dirname "$0" )" && pwd )"
Andre Maroneze
committed
# All scripts called by frama-c-script may rely on FRAMAC_BIN pointing to the
# directory containing frama-c, frama-c-config and frama-c-script.
export FRAMAC_BIN="$DIR"
FRAMAC_SHARE=$("${DIR}/frama-c-config" -print-share-path)
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
if [ -z ${FRAMAC_SESSION+x} ]; then
FRAMAC_SESSION="./.frama-c";
fi
command="$1"
# [check_path_exists path]: if [path] exists,
# ask if it should be overwritten
check_path_exists() {
if [ -e "$1" ]; then
read -p "warning: '$1' already exists. Overwrite? [y/N] " yn
case $yn in
[Yy]) ;;
*)
echo "Exiting without overwriting."
exit 0;;
esac
fi
}
# [open file]
open_file() {
case "$OSTYPE" in
cygwin*)
cmd /c start "$1"
;;
linux*)
xdg-open "$1"
;;
darwin*)
open "$1"
;;
esac
}
flamegraph() {
if [ "$#" -eq 0 ]; then
echo "error: 'flamegraph' command requires a path";
exit 1
fi
if [ ! -e "$1" ]; then
echo "error: '$1' not found"
exit 1
else
path="$1"
fi
if [ "$#" -ge 2 ]; then
dir="${2%/}"
else
dir="$FRAMAC_SESSION"
fi
if [ ! -d "$dir" ]; then
mkdir "$dir"
if [ $? -ne 0 ]; then
echo "error: could not create '$dir'"
exit 1
fi
fi
out_svg="$dir/flamegraph.svg"
"${FRAMAC_SHARE}/analysis-scripts/flamegraph.pl" \
--title "Eva Flamegraph" --inverted --hash "$path" \
--width 1400 --fontsize 11 > "$out_svg.tmp"
if [ ! $? -eq 0 ]; then
echo "Error creating flamegraph, aborting."
exit 1
fi
mv "$out_svg.tmp" "$out_svg"
out_html="$dir/flamegraph.html"
cat <<EOF > "$out_html"
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8">
<title>Eva Flamegraph</title>
</head>
<body>
<embed src="flamegraph.svg" style="max-width:100%;width:1400px;min-width:1000px">
</body>
</html>
EOF
if [ -z "$NOGUI" ]; then
open_file "$out_html"
fi
}
configure_for_frama_c() {
if [ "$#" -eq 0 ]; then
echo "error: 'configure' command requires a machdep";
exit 1
fi
MACHDEP="$(echo $1 | tr a-z A-Z)"
shift
CPP="gcc -E -nostdinc -fno-builtin -I${FRAMAC_SHARE}/libc -D__FC_MACHDEP_${MACHDEP}" ./configure "$@"
}
case "$command" in
"help" | "-help" | "--help" | "-h")
usage 0;
;;
"make-template")
shift;
${FRAMAC_SHARE}/analysis-scripts/make_template.py "$@";
;;
"list-files")
shift;
${FRAMAC_SHARE}/analysis-scripts/list_files.py "$@";
;;
Andre Maroneze
committed
"find-fun")
shift;
${FRAMAC_SHARE}/analysis-scripts/find_fun.py "$@";
;;
"flamegraph")
shift;
flamegraph "$@";
;;
"summary")
shift;
${FRAMAC_SHARE}/analysis-scripts/summary.py "$@";
;;
"configure")
shift;
configure_for_frama_c "$@";
;;
"make-wrapper")
shift;
${FRAMAC_SHARE}/analysis-scripts/make_wrapper.py "$0" "$@";
;;
"normalize-jcdb")
shift;
${FRAMAC_SHARE}/analysis-scripts/normalize_jcdb.py "$@";
;;
echo "error: unrecognized command: $command";
exit 1