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
a2e67b9b
Commit
a2e67b9b
authored
2 years ago
by
Andre Maroneze
Committed by
David Bühler
2 years ago
Browse files
Options
Downloads
Patches
Plain Diff
[Doc] add flame graph section to Eva user manual
parent
7bef4502
No related branches found
Branches containing commit
No related tags found
Tags containing commit
No related merge requests found
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
doc/eva/flamegraph.png
+0
-0
0 additions, 0 deletions
doc/eva/flamegraph.png
doc/eva/main.tex
+37
-0
37 additions, 0 deletions
doc/eva/main.tex
with
37 additions
and
0 deletions
doc/eva/flamegraph.png
0 → 100644
NaN GiB (NaN%)
View file @
a2e67b9b
File suppressed by a .gitattributes entry or the file's encoding is unsupported.
This diff is collapsed.
Click to expand it.
doc/eva/main.tex
+
37
−
0
View file @
a2e67b9b
...
...
@@ -2067,6 +2067,43 @@ In these three cases, the function \lstinline|f| is reached by the analysis
(and thus counted in the
\textsf
{
Metrics
}
coverage), but not analyzed
(and thus not counted in the
\Eva
{}
coverage).
\subsection
{
Profiling via
{
\em
Flame graphs
}}
When running long analyses with
\Eva
{}
, you can use option
\texttt
{
-eva-flamegraph <file>
}
to obtain profiling information about which
functions are taking time. This option outputs textual data to the specified
\texttt
{
<file>
}
, which can then be read by the
\texttt
{
flamegraph.pl
}
script
developed by Brendan Egg
\footnote
{
\url
{
https://www.brendangregg.com/flamegraphs.html
}}
.
This script is available as a package in some Linux distributions, and it is
also included in Frama-C's shared files. The version shipped with Frama-C can
be run with the following command:
\begin{listing}
{
1
}
frama-c-script flamegraph <file> [<dir>]
\end{listing}
The
\texttt
{
<file>
}
argument must be the same given to option
\texttt
{
-eva-flamegraph
}
. The
\texttt
{
<dir>
}
argument is optional, but when
specified, it stores the produced flame graph (in SVG and HTML versions)
in that directory.
Figure~
\ref
{
fig:flamegraph
}
presents an example of a flame graph.
\begin{figure}
[hbt]
\centering
\includegraphics
[width=0.95\textwidth]
{
flamegraph.png
}
\caption
{
Flame graph for an analysis with Eva
}
\label
{
fig:flamegraph
}
\end{figure}
These flame graphs are interactive SVGs, which can be wrapped in an HTML page.
It is possible to zoom and filter by name. The length of a bar is proportional
to the time spent in that function. Note that if a function
\texttt
{
f
}
contains several callsites for
\texttt
{
g
}
, only the total aggregated time is
displayed as a single bar
\texttt
{
g
}
below
\texttt
{
f
}
.
Finally, note that
\texttt
{
-eva-flamegraph
}
has a negligible cost in terms of
execution time for the analysis.
\subsection
{
Audit messages (
{
\em
experimental
}
)
}
Using options
\lstinline
|-audit-prepare| and
\lstinline
|-audit-check|, the
...
...
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