From b63f725c70cd82c9d561caf3a345066f6e341f8d Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Thu, 20 Jan 2022 18:11:20 +0100
Subject: [PATCH] [devel-tools] Add a helper to invoke frama-c within
 valgrind/callgrind

---
 devel_tools/frama-c-callgrind | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)
 create mode 100755 devel_tools/frama-c-callgrind

diff --git a/devel_tools/frama-c-callgrind b/devel_tools/frama-c-callgrind
new file mode 100755
index 00000000000..3e23c01dbd8
--- /dev/null
+++ b/devel_tools/frama-c-callgrind
@@ -0,0 +1,31 @@
+#!/bin/bash
+
+# Script for profiling Frama-C with callgrind (a valgrind tool).
+# Note: execution time with valgrind is about 15x-20x slower.
+#
+# Use this script at the root of the repository, so local_export.sh can be found
+# in bin.
+# For more focused results, you can activate the profiling only after entering
+# a specific function. For instance, to only profile Eva, add
+#
+#   --toggle-collect='*Eva__Analysis__force_compute*'
+#
+# to the command line below.
+#
+# Example of invocation :
+#
+#   devel_tools/frama-c-callgrind tests/idct/*.c -eva -float-normal -no-warn-signed-overflow
+#
+# This creates a 'callgrind.out' file (Callgrind format), which can be viewed
+# with a tool such as kcachegrind:
+#
+#   kcachegrind callgrind.out
+
+BASH_ARGV0="bin/frama-c" # hackish way to tell local_export that its dir is bin
+
+. bin/local_export.sh
+
+valgrind \
+  --tool=callgrind --callgrind-out-file=callgrind.out --dump-instr=yes \
+  --separate-callers=2 --collect-jumps=yes --fn-skip='caml_*' \
+  $BINDIR/toplevel.opt "$@"
-- 
GitLab