[configure] fix landmarks and document it

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

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}

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"