From 86b6fa5cc2694b83c9b38154cd967da19b630cd7 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 12 Sep 2022 18:16:59 +0200
Subject: [PATCH] [Doc] document -ast-diff in manpage, userman, analysis.mk
---
doc/userman/user-changes.tex | 1 +
doc/userman/user-sources.tex | 19 +++++++++++++++++++
man/frama-c.1.md | 5 +++++
share/analysis-scripts/analysis.mk | 7 +++++++
4 files changed, 32 insertions(+)
diff --git a/doc/userman/user-changes.tex b/doc/userman/user-changes.tex
index 60d058461dc..ee078baa1ad 100644
--- a/doc/userman/user-changes.tex
+++ b/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)}
diff --git a/doc/userman/user-sources.tex b/doc/userman/user-sources.tex
index f104502d342..63269b7f62c 100644
--- a/doc/userman/user-sources.tex
+++ b/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
diff --git a/man/frama-c.1.md b/man/frama-c.1.md
index 30fa54a0ea4..73b505a0074 100644
--- a/man/frama-c.1.md
+++ b/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.
diff --git a/share/analysis-scripts/analysis.mk b/share/analysis-scripts/analysis.mk
index 301f0647287..1d5d87e03b5 100644
--- a/share/analysis-scripts/analysis.mk
+++ b/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)))
--
GitLab