From efcc3964395f8157aaef47725e247ce926934831 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Mon, 15 Apr 2019 16:44:47 +0200
Subject: [PATCH] [configure] fix landmarks and document it
---
configure.in | 2 +-
doc/developer/changes.tex | 1 +
doc/developer/refman.tex | 38 ++++++++++++++++++++++++++++++++++++++
3 files changed, 40 insertions(+), 1 deletion(-)
diff --git a/configure.in b/configure.in
index e5bd40a6513..cf7e595c785 100644
--- a/configure.in
+++ b/configure.in
@@ -400,7 +400,7 @@ if test "$ENABLE_LANDMARKS" = yes ; then
AC_MSG_CHECKING(for Landmarks)
LANDMARKS_PATH=$($OCAMLFIND query landmarks 2>/dev/null | tr -d '\r\n')
LANDMARKS_PPX_PATH=$($OCAMLFIND query landmarks.ppx 2>/dev/null | tr -d '\r\n')
- if test -f "$LANDMARKS_PATH/landmarks.$DYN_SUFFIX" -a -f "$LANDMARKS_PPX_PATH/ppx_landmarks"; then
+ if test -f "$LANDMARKS_PATH/landmark.$DYN_SUFFIX" -a -f "$LANDMARKS_PPX_PATH/ppx_landmarks.$DYN_SUFFIX"; then
HAS_LANDMARKS="yes";
AC_MSG_RESULT(found)
else
diff --git a/doc/developer/changes.tex b/doc/developer/changes.tex
index 41a4ee2c9fc..7e8eb0d889f 100644
--- a/doc/developer/changes.tex
+++ b/doc/developer/changes.tex
@@ -9,6 +9,7 @@ This chapter summarizes the major changes in this documentation between each
\begin{itemize}
\item \textbf{ACSL Extension}: Document new \texttt{status} flag for registration functions
\item \textbf{Testing}: Document of usage \texttt{@@} in a directive
+\item \textbf{Profiling with Landmarks}: New section
\end{itemize}
\section*{18.0 Argon}
diff --git a/doc/developer/refman.tex b/doc/developer/refman.tex
index 6eaa39440e1..2b6313b3054 100644
--- a/doc/developer/refman.tex
+++ b/doc/developer/refman.tex
@@ -868,6 +868,44 @@ one for regular tests (if more than one \verb|OPT|).\\
\caption{Predefined macros for ptests}\label{fig:ptests-macros}
\end{figure}
+\section{Profiling with Landmarks} \label{refman:landmarks}\codeidxdef{Landmarks}
+
+{\em Landmarks}\footnote{\url{https://github.com/LexiFi/landmarks}} is a
+library for ``quick and dirty'' profiling of OCaml programs. It allows the
+insertion of annotations in the code to enable profiling of specific parts of
+it, but also an automatic mode, in which every function call is instrumented.
+The Frama-C \texttt{configure} file is setup to enable usage of this library
+when it is available (the usual way to install it is via the \texttt{landmarks}
+opam package).
+
+For quick usage of the library:
+\begin{itemize}
+\item ensure that the \texttt{configure} script detected it
+ (there should be a line \texttt{checking for Landmarks... found});
+\item enable instrumentation {\em when compiling Frama-C's files}, that is,
+ when running \texttt{make}, by setting the environment variable
+ \verb+OCAML_LANDMARKS+. For instance, to enable automatic instrumentation
+ of every Frama-C function (note: this increases compilation time of Frama-C),
+ run:
+
+\begin{lstlisting}
+ OCAML_LANDMARKS=auto make
+\end{lstlisting}
+
+\item enable instrumentation {\em during execution} of Frama-C, again using
+ \verb+OCAML_LANDMARKS+. Note that the \texttt{auto} parameter here is
+ implicit if you enabled it on the previous step.
+ For instance, run:
+
+ \begin{lstlisting}
+ OCAML_LANDMARKS= bin/frama-c [files] [options]
+ \end{lstlisting}
+\end{itemize}
+
+Commonly used options include \verb+output=landmarks.log+ to output the result
+to a file instead of \texttt{stderr}.
+Check \url{https://github.com/LexiFi/landmarks} for its documentation.
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Local Variables:
%%% TeX-master: "developer.tex"
--
GitLab