[Doc] document -ast-diff in manpage, userman, analysis.mk

doc/userman/user-changes.tex

@@ -6,6 +6,7 @@ release. First we list changes of the last release.
 \section*{Frama-C+dev}
 \begin{itemize}
 \item Removed Journalisation
+\item \textbf{Preparing the Sources:} added option \texttt{-ast-diff}.
 \end{itemize}
 
 \section*{24.0 (Chromium)}

doc/userman/user-sources.tex

@@ -332,6 +332,25 @@ in case of \texttt{UNROLL} pragma.
 supported are typedefs redefinition.
 \end{description}
 
+\section{Incremental parsing} (experimental)\label{sec:incremental-parsing}
+
+Parsing large code bases takes a non-negligible amount of time.
+More importantly, non-modular analyses need to be recomputed in their entirety
+even for minuscule AST changes.
+
+In order to help deal with these issues, and to help support for future
+incremental analyses (which recompute results only for the modified AST parts
+and their dependencies), you can use option \optiondef{-}{ast-diff}.
+It enables computing the difference between a previous AST (loaded via
+option \verb|-load| (Section~\ref{sec:saveload}) and the AST computed from the
+current sources. This difference is stored by the \FramaC kernel and can be
+used by plug-ins which support it.
+
+{\em Note: currently, parsing and type-checking are systematically performed
+  even with this option, and \verb|-ast-diff| compares the normalized ASTs.
+  In the future, though, these steps should be refactored to allow saving
+  further time.}
+
 \section{Predefined macros}\label{sec:predefined-macros}
 
 \FramaC, like several compilers and code analysis tools, predefines and uses

man/frama-c.1.md

@@ -119,6 +119,11 @@ with non-trivial control flow are never duplicated. Defaults to yes.
 : reads ACSL annotations. This is the default. Annotations are pre-processed
 by default. Use -no-pp-annot if you don't want to expand macros in annotations.
 
+[-no]-ast-diff
+: computes AST differences between a loaded session (loaded with **-load**)
+and the current sources. These can then be used by plug-ins supporting
+incremental analyses.
+
 -autocomplete *p1,...,pn*
 : lists the options of plugins *p1,...,pn* in a format suitable for
 autocompletion scripts.

share/analysis-scripts/analysis.mk

@@ -42,6 +42,8 @@
 # FLAMEGRAPH    If set (to any value), running an analysis will produce an
 #               SVG + HTML flamegraph at the end.
 #
+# AST_DIFF      If set (to any value), enables usage of -ast-diff during parse.
+#
 # There are several ways to define or change these variables.
 #
 # With an environment variable:
@@ -62,6 +64,11 @@
 #
 # target.parse: file1.c file2.c file3.c...
 #
+# NOTE ABOUT AST_DIFF:
+# - If AST_DIFF is set to a non-empty value (e.g. `fcmake AST_DIFF=y`), then
+#   during parsing (rule %.parse), we check if there already exists a framac.sav
+#   file. If so, we rename it framac.reparse and, instead of parsing from zero,
+#   we reload this file and apply -ast-diff before reparsing the sources.
 
 # Test if Makefile is > 4.0
 ifneq (4.0,$(firstword $(sort $(MAKE_VERSION) 4.0)))