diff --git a/doc/userman/user-changes.tex b/doc/userman/user-changes.tex
index 60d058461dc268df9b646252cfbd1e0525314e8e..ee078baa1ad21322661cd39c3a6f4d4271738097 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 f104502d3423b2d9554110da8fae661c2b4109e9..42e1bb39238d7286e8be314a05ccea46d90dd647 100644
--- a/doc/userman/user-sources.tex
+++ b/doc/userman/user-sources.tex
@@ -332,6 +332,31 @@ 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. Note however that since \verb|-load| implies that
+files given on the command line are ignored, \verb|-load| and \verb|-ast-diff| with
+the list of C files to consider must be properly sequenced through the use of
+\verb|-then| or one of its variants (Section~\ref{sec:then}), as in:
+\begin{lstlisting}[language=shell]
+frama-c -load previous.sav -then -ast-diff file1.c file2.c [...]
+\end{lstlisting}
+
+{\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 30fa54a0ea410812b67aff5471f605b6c2ee2ee9..73b505a007498ebcd306bb1a5b051efec98349a6 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 027f5ebed9639ac2339f7282406c373fb258f44e..0970e1d96a2e80af1e591e319a039ce578082001 100644
--- a/share/analysis-scripts/analysis.mk
+++ b/share/analysis-scripts/analysis.mk
@@ -28,10 +28,12 @@
#
# FRAMAC frama-c binary
# FRAMAC_GUI frama-c gui binary
+# IVETTE ivette binary
# CPPFLAGS preprocessing flags
# MACHDEP machdep
# FCFLAGS general flags to use with frama-c
# FCGUIFLAGS flags to use with frama-c-gui
+# IVETTEFLAGS flags to use with Ivette
# EVAFLAGS flags to use with the Eva plugin
# EVABUILTINS Eva builtins to be set (via -eva-builtin)
# EVAUSESPECS Eva functions to be overridden by specs (-eva-use-spec)
@@ -40,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:
@@ -60,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)))
@@ -108,6 +117,7 @@ fc_list = $(subst $(space),$(comma),$(strip $1))
FRAMAC ?= frama-c
FRAMAC_SCRIPT = $(FRAMAC)-script
FRAMAC_GUI ?= frama-c-gui
+IVETTE ?= ivette
EVAFLAGS ?= \
-eva-no-print -eva-no-show-progress -eva-msg-key=-initial-state \
-eva-print-callstacks -eva-warn-key alarm=inactive \
@@ -119,6 +129,7 @@ EVAFLAGS ?= \
WPFLAGS ?=
FCFLAGS ?=
FCGUIFLAGS ?=
+IVETTEFLAGS ?=
export LIBOVERLAY_SCROLLBAR=0
@@ -134,7 +145,6 @@ clean-backups:
-regex '^.*_[0-9]{4}-[0-9]{2}-[0-9]{2}_[0-9]{2}-[0-9]{2}-[0-9]{2}\.eva(\.(log|stats|alarms|warnings|metrics))?' \
-delete
-
# --- Generic rules ---
HR_TIMESTAMP := $(shell date +"%H:%M:%S %d/%m/%Y")# Human readable
@@ -151,10 +161,20 @@ SHELL := $(shell which bash)
@#
%.parse: SOURCES = $(filter-out %/command,$^)
-%.parse: PARSE = $(FRAMAC) $(FCFLAGS) $(if $(value MACHDEP),-machdep $(MACHDEP),) -cpp-extra-args="$(CPPFLAGS)" $(SOURCES)
+%.parse: PARSE = $(FRAMAC) \
+ $(FCFLAGS) \
+ $(if $(value MACHDEP),-machdep $(MACHDEP),) \
+ -cpp-extra-args="$(CPPFLAGS)" $(SOURCES) \
+
%.parse: $$(if $$^,,.IMPOSSIBLE) $$(shell $(SHELL) $(DIR)cmd-dep.sh $$@/command $$(PARSE))
@$(call display_command,$(PARSE))
mkdir -p $@
+ $(if $(AST_DIFF),\
+ $(if $(wildcard $*.eva/framac.sav), \
+ mv $*.eva/framac.sav $@/framac.reparse,\
+ $(if $(wildcard $@/framac.sav), \
+ mv $@/framac.sav $@/framac.reparse,true)),\
+ true)
mv -f $@/{command,running}
{
$(call time_with_output,$@/stats.txt) \
@@ -164,7 +184,9 @@ SHELL := $(shell which bash)
-metrics -metrics-log a:$@/metrics.log \
-save $@/framac.sav \
-print -ocode $@/framac.ast -then -no-print \
- || ($(RM) $@/stats.txt && false) # Prevents having error code reporting in stats.txt
+ || (mv -f $@/{running,command} &&
+ $(RM) $@/stats.txt &&
+ false) # Prevents having error code reporting in stats.txt
} 2>&1 |
$(SED_UNBUFFERED) '/\[metrics\]/,999999d' |
tee $@/parse.log
@@ -176,7 +198,14 @@ SHELL := $(shell which bash)
mv $@/{running,command}
touch $@ # Update timestamp and prevent remake if nothing changes
-%.eva: EVA = $(FRAMAC) $(FCFLAGS) -eva $(EVAFLAGS)
+define incremental
+ $(if $(AST_DIFF),\
+ $(if $(wildcard $@/framac.sav),\
+ -eva-load $@/framac.sav,\
+ $(warning Cannot do incremental analysis: no previously saved state)))
+endef
+
+%.eva: EVA = $(FRAMAC) $(FCFLAGS) -eva $(call incremental,$1) $(EVAFLAGS)
%.eva: PARSE_RESULT = $(word 1,$(subst ., ,$*)).parse
%.eva: $$(PARSE_RESULT) $$(shell $(SHELL) $(DIR)cmd-dep.sh $$@/command $$(EVA)) $(if $(BENCHMARK),.FORCE,)
@$(call display_command,$(EVA))
@@ -185,7 +214,7 @@ SHELL := $(shell which bash)
{
$(call time_with_output,$@/stats.txt) \
$(EVA) \
- -load $(PARSE_RESULT)/framac.sav -save $@/framac.sav \
+ -load $(PARSE_RESULT)/framac.sav \
-eva-flamegraph $@/flamegraph.txt \
-kernel-log w:$@/warnings.log \
-from-log w:$@/warnings.log \
@@ -193,12 +222,16 @@ SHELL := $(shell which bash)
-scope-log w:$@/warnings.log \
-eva-log w:$@/warnings.log \
-then \
+ -remove-projects @all_but_current -save $@/framac.sav \
+ -then \
-report-csv $@/alarms.csv -report-no-proven \
-report-log w:$@/warnings.log \
-metrics-eva-cover \
-metrics-log a:$@/metrics.log \
-nonterm -nonterm-log a:$@/nonterm.log \
- || ($(RM) $@/stats.txt && false) # Prevents having error code reporting in stats.txt
+ || (mv -f $@/{running,command} &&
+ $(RM) $@/stats.txt &&
+ false) # Prevents having error code reporting in stats.txt
} 2>&1 |
$(SED_UNBUFFERED) '/\[eva\] Values at end of function/,999999d' |
tee $@/eva.log
@@ -231,7 +264,9 @@ SHELL := $(shell which bash)
-then \
-report-csv $@/alarms.csv -report-no-proven \
-report-log w:$@/warnings.log \
- || ($(RM) $@/stats.txt && false) # Prevents having error code reporting in stats.txt
+ || (mv -f $@/{running,command} &&
+ $(RM) $@/stats.txt &&
+ false) # Prevents having error code reporting in stats.txt
} 2>&1 |
tee $@/wp.log
{
@@ -247,6 +282,9 @@ SHELL := $(shell which bash)
%.gui: %
$(FRAMAC_GUI) $(FCGUIFLAGS) -load $^/framac.sav &
+%.ivette: %
+ $(IVETTE) $(IVETTEFLAGS) -load $^/framac.sav &
+
# Produce and open an SVG + HTML from raw flamegraph data produced by Eva
%/flamegraph: %/flamegraph.html
@