diff --git a/ALL_VERSIONS b/ALL_VERSIONS
index 127fa685225b133394702ffd2819c5d442a72a21..d9447f7b7d320386cd109d9acaaefc53da5ca3c8 100644
--- a/ALL_VERSIONS
+++ b/ALL_VERSIONS
@@ -1,5 +1,6 @@
Version number Date of release Notes
============== =============== =====
+18.0 (Argon) 2018, November 29
Chlorine-20180502 2018, July 06 Bug fixed
Chlorine-20180501 2018, June 01
Sulfur-20171101 2017, November 28
diff --git a/Changelog b/Changelog
index d97c6803349ab92c574e12009d63afb771bb8aa3..141ced448ff11999cd6e3c9571ffaa1b38f307ea 100644
--- a/Changelog
+++ b/Changelog
@@ -13,11 +13,6 @@
# '#?nnn' : OLD-BTS entry #nnn #
###############################################################################
-##################################
-Open Source Release <next-release>
-##################################
-
-
################################
Open Source Release 18.0 (Argon)
################################
diff --git a/Makefile b/Makefile
index 6b117ec57cc620dae99d5829e1c410bffe79ecbc..70092c7cb3418f552d685b555464635837b4c83a 100644
--- a/Makefile
+++ b/Makefile
@@ -252,10 +252,13 @@ DISTRIB_FILES:=\
VERSION VERSION_CODENAME $(wildcard licenses/*) \
$(LIBC_FILES) \
share/analysis-scripts/cmd-dep.sh \
+ share/analysis-scripts/concat-csv.sh \
+ $(wildcard share/analysis-scripts/examples/*) \
share/analysis-scripts/flamegraph.pl \
share/analysis-scripts/frama-c.mk \
share/analysis-scripts/list_files.py \
share/analysis-scripts/parse-coverage.sh \
+ share/analysis-scripts/summary.sh \
share/analysis-scripts/README.md \
share/analysis-scripts/template.mk \
$(wildcard share/emacs/*.el) share/autocomplete_frama-c \
@@ -1800,13 +1803,18 @@ install:: install-lib
$(FRAMAC_DATADIR)
$(MKDIR) $(FRAMAC_DATADIR)/analysis-scripts
$(CP) share/analysis-scripts/cmd-dep.sh \
+ share/analysis-scripts/concat-csv.sh \
share/analysis-scripts/flamegraph.pl \
share/analysis-scripts/frama-c.mk \
share/analysis-scripts/parse-coverage.sh \
share/analysis-scripts/README.md \
share/analysis-scripts/list_files.py \
+ share/analysis-scripts/summary.sh \
share/analysis-scripts/template.mk \
$(FRAMAC_DATADIR)/analysis-scripts
+ $(MKDIR) $(FRAMAC_DATADIR)/analysis-scripts/examples
+ $(CP) share/analysis-scripts/examples/* \
+ $(FRAMAC_DATADIR)/analysis-scripts/examples
$(MKDIR) $(FRAMAC_DATADIR)/emacs
$(CP) $(wildcard share/emacs/*.el) $(FRAMAC_DATADIR)/emacs
$(CP) share/frama-c.rc $(ICONS) $(FRAMAC_DATADIR)
diff --git a/VERSION b/VERSION
index 3a48ff126f4f03ea3b2eb133fb1b2de6bb40e772..fc004cb52c7a3c23ed19e8b19149b832f492ca2b 100644
--- a/VERSION
+++ b/VERSION
@@ -1 +1 @@
-18.0+dev
\ No newline at end of file
+18.0
\ No newline at end of file
diff --git a/bin/build-src-distrib.sh b/bin/build-src-distrib.sh
index 67607a2e0835e5c71cbab3d6a56359f17830a6a4..111947be0a557a8aa3cd5d74275fc4987f32c2b5 100755
--- a/bin/build-src-distrib.sh
+++ b/bin/build-src-distrib.sh
@@ -36,7 +36,7 @@ FRAMAC_VERSION_CODENAME=$(cat VERSION_CODENAME)
FRAMAC_VERSION_AND_CODENAME="${FRAMAC_VERSION}-${FRAMAC_VERSION_CODENAME}"
TARGZ_FILENAME=frama-c-${FRAMAC_VERSION_AND_CODENAME}.tar.gz
-VERSION_MODIFIER=$(cat VERSION | sed -e s/[A-Za-z]*-[0-9]*\\\(.*\\\)/\\1/)
+VERSION_MODIFIER=$(cat VERSION | sed -e s/[0-9.]*\\\(.*\\\)/\\1/)
if test -n "$VERSION_MODIFIER"; then FINAL_RELEASE=no; else FINAL_RELEASE=yes; fi
@@ -313,7 +313,7 @@ case "${STEP}" in
echo " - [$TARGZ_FILENAME](downloads/$TARGZ_FILENAME)" >> $WIKI_PAGE
echo "" >> $WIKI_PAGE
echo "## Manuals" >> $WIKI_PAGE
- for f in "user-manual" "acsl-implementation" "value-analysis" "plugin-development-guide" "rte-manual" "wp-manual" "metrics-manual" "aorai-manual"; do
+ for f in "user-manual" "acsl-implementation" "eva-manual" "plugin-development-guide" "rte-manual" "wp-manual" "metrics-manual" "aorai-manual"; do
echo "- [$f](manuals/$f-${FRAMAC_VERSION_AND_CODENAME}.pdf)" >> $WIKI_PAGE
run "cp $MANUALS_DIR/$f.pdf $GITHUB_WIKI/manuals/$f-${FRAMAC_VERSION_AND_CODENAME}.pdf"
run "git -C $GITHUB_WIKI add manuals/$f-${FRAMAC_VERSION_AND_CODENAME}.pdf"
diff --git a/doc/Makefile b/doc/Makefile
index de074ba66b8d858ba6ce46003caf5ed7d5b448be..e45e252c0f47f8df338ed88a1f0431ad2a4b9f5c 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -55,7 +55,7 @@ MANUALS=acsl
#MANUALS that depend on the frama-c version
VERSIONED_MANUALS=acsl-implementation aorai-manual rte-manual \
wp-manual metrics-manual user-manual \
- plugin-development-guide value-analysis
+ plugin-development-guide eva-manual
FILES= $(addprefix manuals/, \
$(addsuffix -$(VERSION).pdf, $(VERSIONED_MANUALS)) \
diff --git a/doc/developer/developer.bib b/doc/developer/developer.bib
index 69d4aa57560e3129b6e730607fce0edd325f2387..7f4c8c58ecdc729975a21be0a0379d7799336ce8 100644
--- a/doc/developer/developer.bib
+++ b/doc/developer/developer.bib
@@ -35,7 +35,7 @@
title = {{Frama-C}'s value analysis plug-in},
year = 2015,
month = feb,
- note = {\mbox{\url{http://frama-c.com/download/frama-c-value-analysis.pdf}}},
+ note = {\mbox{\url{http://frama-c.com/download/frama-c-eva-manual.pdf}}},
}
@misc{slicing,
diff --git a/doc/rte/biblio.bib b/doc/rte/biblio.bib
index 12f5a2484516bc23f15dc83d1b406a3304890270..0bb03befc467bd8b9dfa10a17be6d55dd555205e 100644
--- a/doc/rte/biblio.bib
+++ b/doc/rte/biblio.bib
@@ -21,7 +21,7 @@ howpublished={\url{http://manju.cs.berkeley.edu/cil/}}
title = {Frama-C's value analysis plug-in},
author={Pascal Cuoq and Boris Yakobowski and Virgile Prevosto},
organization = {CEA List, Software Reliability Laboratory},
- note = {\url{http://frama-c.com/download/frama-c-value-analysis.pdf}}
+ note = {\url{http://frama-c.com/download/frama-c-eva-manual.pdf}}
}
@MANUAL{framacwp,
diff --git a/doc/userman/userman.bib b/doc/userman/userman.bib
index 0237983740a880d86e59ceeeb8992efc446a8f44..a8abde0581e886288dc4526765a1013c7ad2d742 100644
--- a/doc/userman/userman.bib
+++ b/doc/userman/userman.bib
@@ -4,7 +4,7 @@
title = {{Frama-C Plug-in Development Guide}},
year = 2015,
month = feb,
- note = {\newline \url{http://frama-c.cea.fr/download/plugin-developer.pdf}},
+ note = {\newline \url{http://frama-c.com/download/frama-c-plugin-development-guide.pdf}},
}
@manual{value,
@@ -12,7 +12,7 @@
title = {{Frama-C}'s value analysis plug-in},
year = 2015,
month = feb,
- note = {\mbox{\url{http://frama-c.cea.fr/download/value-analysis.pdf}}},
+ note = {\mbox{\url{http://frama-c.com/download/frama-c-eva-manual.pdf}}},
}
@manual{acsl,
@@ -109,5 +109,5 @@ note={Extended version of \cite{sefm12}},
author = {Julien Signoles},
year = {2015},
month = feb,
- note = {\url{http://frama-c.com/eacsl}},
+ note = {\url{http://frama-c.com/eacsl.html}},
}
diff --git a/doc/value/main.tex b/doc/value/main.tex
index e881bac4e14cb6cde8800c6bb82278310795d6c8..2d5124ad23a4639fa25509a1de053eaf6842253f 100644
--- a/doc/value/main.tex
+++ b/doc/value/main.tex
@@ -2205,7 +2205,7 @@ Besides, the source code of some of the functions used by
the application may not be available (library functions for instance).
The plug-in can be used, usually with more work, in all these circumstances.
The options for specifying the entry point of the analysis are detailed
-in this manual, section \ref{trait_fonctions}.
+in this manual, section \ref{val-use-spec}.
\subsection{Entry point of a complete application}
@@ -2564,7 +2564,7 @@ the following program does not terminate:
If this program is analyzed
with the default options of \Eva{}, the analysis finds
that every time execution reaches the end of \lstinline|main|, the value
-of \lstinline|x| is in $\bropen 100..127\brclose$. This does
+of \lstinline|x| is $\geq 100$. This does
not mean that the function always terminates or even that it may
sometimes terminate (it does neither). When \Eva{}
proposes an interval for \lstinline|x| at a point P,
@@ -2591,7 +2591,7 @@ int x, y, z;
main(int c){
...
...
-/* At this point \Eva{} guarantees:
+/* At this point Eva guarantees:
x IN {0; 1}
y IN {0; 1}; */
z = 10 / (x - y);
@@ -2634,7 +2634,27 @@ Just in case.}
\vspace{2cm}
+Parameterization of \Eva{} involves two main kinds of options:
+{\em correctness options} and {\em performance tuning options}.
+The former require understanding of their meaning and of the extra hypotheses
+they entail; used incorrectly, they can lead to a wrong analysis.
+The latter control the tradeoff between the quality of the results and the
+resources taken by the analyzer to provide them (CPU time and memory usage).
+These options cannot be used wrongly, in the sense that they do not affect the
+correctness of the results. However, using them efficiently is essential for
+scalability of the analysis.
+
+Section \ref{command-line} presents the general usage options of \Eva{} in the
+command-line.
+The options described in section \ref{context} are correctness options,
+while the remaining sections (\ref{boucles-traitement},
+\ref{controlling-approximations} and \ref{sec:eva}) deal with performance
+tuning options. Finally, \ref{nonterm} presents a derived analysis to
+obtain information about non-termination.
+
+
\section{Command line}
+\label{command-line}
The parameters that determine Frama-C's behavior can be
set through the command line.
@@ -3151,24 +3171,58 @@ informed assumptions. However, no guarantee is made that those assumptions
over-approximate the real behavior of the function. The inferred
contract should be verified carefully by the user.
+\subsection{Using the specification of a function instead of its body}
+\label{val-use-spec}
+In some cases, one can estimate that the analysis of a given function \verb+f+
+takes too much time. This can be caused by a very complex
+function, or because \verb+f+ is called many times during the analysis.
+Another situation is when a function already has a functional specification,
+proved for instance with the \textsf{WP} plug-in, and we do not want/need
+to analyze it with \Eva{}.
-\section{Controlling approximations}
+In the cases above, a somewhat radical
+approach consists in replacing the entire body of the function
+by an ACSL contract that describes its behavior. See for example
+section~\ref{annot_assigns} for how to specify which values the function
+reads and writes.
-Unlike options of section \ref{context}, which used wrongly may cause
-\Eva{} to produce incorrect results, all the options
-in this section give the user control over the tradeoff between the
-quality of the results and the resources taken by the analyzer to
-provide them. The options described in this section can, so to speak,
-not be used wrongly. They may cause Frama-C to exhaust the available
-memory, to take a nearly infinite time, or, in the other direction,
-to produce results so imprecise that they are useless, but {\bf never}
-to produce incorrect results.
-
-\subsection{Treatment of loops}
-\label{boucles-traitement}
+Alternatively, one can leave the body of the function untouched, but
+still write a contract. Then it is possible to use the option
+\verb+-eva-use-spec f+. This instructs \Eva{} to use the
+specification of \verb+f+ instead of its body each time a call to
+\verb+f+ is encountered. This is equivalent\footnote{Except for a few
+ properties, as described in the next paragraph.} to deleting the body
+of \verb+f+ for \Eva{}, but not for the other plug-ins of \FramaC,
+that may study the body of \verb+f+ on their own.
-\subsubsection{Default treatment of loops}
+Notice that option \verb+-eva-use-spec f+ loses some guarantees. In particular,
+the body of \verb+f+ is not studied at all by \Eva{}. Neither
+are the functions that \verb+f+ calls, unless they are used by some other
+functions than \verb+f+. Moreover, \Eva{} does not attempt
+to check that \verb+f+ conforms to its specification. In particular,
+postconditions are marked as {\em unknown} with \verb+-eva-use-spec+,
+while they are {\em considered valid} for functions without body.
+It is the responsibility
+of the user to verify those facts, for example by studying \verb+f+
+on its own in a generic context.
+
+
+
+%\section{Controlling approximations}
+%
+%Unlike options of section \ref{context}, which used wrongly may cause
+%\Eva{} to produce incorrect results, all the options
+%in this section give the user control over the tradeoff between the
+%quality of the results and the resources taken by the analyzer to
+%provide them. The options described in this section can, so to speak,
+%not be used wrongly. They may cause Frama-C to exhaust the available
+%memory, to take a nearly infinite time, or, in the other direction,
+%to produce results so imprecise that they are useless, but {\bf never}
+%to produce incorrect results.
+
+\section{Improving precision in loops}
+\label{boucles-traitement}
The default treatment of loops by the analyzer may produce
results that are too approximate. Tuning
@@ -3181,8 +3235,181 @@ entering the loop. This englobing state may be too imprecise
by construction: typically, if the analyzed loop is initializing
an array, the user does not expect to see the initial values of
the array appear in the state computed by the analyzer.
-The solution in this case is to use one of the two unrolling options,
-as described in this section.
+The solution in this case is to either unroll loops, using one of several
+available methods, or to add annotations (widening hints or loop invariants)
+that enable the analyzer to maintain precision while ensuring the analysis
+time remains bounded.
+
+\subsection{Loop unrolling}
+
+Loop unrolling is often easier to apply, since it does not require much
+knowledge about the loop, other than an estimate of the number of iterations.
+This estimate may not improve precision if too low
+or lead to unnecessary work if too high,
+but will never affect its correctness.
+
+\subsubsection{Loop unroll annotations}
+
+Whenever a loop has a fixed number of iterations (or a known upper bound),
+an easy and precise way to handle it is to include a
+\lstinline|loop unroll <n>| annotation, where
+\lstinline|<n>| is the number of iterations of the loop.
+It will indicate \Eva{} to analyze the loop by semantically unrolling each
+iteration, avoiding merging states from different iterations.
+This leads to increased cost in terms of analysis, but usually the cost
+increase is worth the improvement in precision.
+
+Such annotations must be placed before just before the loop (i.e. before the
+\lstinline|while|, \lstinline|for| or \lstinline|do| introducing the loop),
+and one annotation is required per loop, including nested ones. For instance:
+
+\begin{lstlisting}
+#define NROWS 10
+void main() {
+ int a[NROWS][20] = {0};
+ //@ loop unroll NROWS;
+ for (int i = 0; i < 10; i++) {
+ //@ loop unroll (10+10);
+ for (int j = 0; j < 20; j++) {
+ a[i][j] += i + j;
+ }
+ }
+}
+\end{lstlisting}
+
+Note that constants obtained via \lstinline|#define| macros can be used in
+annotations, as well as constant expressions. The annotations above will ensure
+that \Eva{} will unroll the loops and keep the analysis precise; otherwise,
+the array access \lstinline|a[i][j]| might generate alarms due to imprecisions.
+
+The unrolling mechanism is independent of \lstinline|-eva-slevel|
+(see next subsection): annotated loops are always unrolled at least the specified
+number of times. If the loop has not been entirely unrolled, however,
+remaining \lstinline|-eva-slevel| may be used to unroll more iterations.
+
+While it is sometimes useful to unroll only the first iterations, the usual
+objective is full unrolling; the user can enable option
+\lstinline|-value-msg-key=loop-unrolling| to be informed whenever the specified
+unrolling value is insufficient to unroll the loop entirely:
+
+\begin{lstlisting}
+void main() {
+ //@ loop unroll 20; // should be 21
+ for (int i = 0 ; i <= 20 ; i ++) {
+ }
+}
+\end{lstlisting}
+
+\begin{lstlisting}
+[eva:loop-unrolling] insuf-loop.c:3: loop not completely unrolled
+\end{lstlisting}
+
+Note that using an unrolling parameter which is higher than the actual number
+of iterations of a loop doesn't generally have an effect on the analysis.
+The analyzer will usually detect that further iterations are not useful.
+
+If all loops in a program need to be unrolled, one way to do it quickly
+consists in using option \lstinline|-eva-min-loop-unroll <n>|,
+where \lstinline|<n>| is the number of iterations to unroll in each loop.
+This option has lower precedence than \lstinline|loop unroll| annotations:
+\Eva{} will always consider the latter if it is present in a loop.
+This allows, for instance, to prevent unrolling of an infinite loop by
+adding \lstinline|loop unroll 0| before it, while unrolling the remaining
+loops by the specified amount in \lstinline|-eva-min-loop-unroll|.
+
+\subsubsection{Unrolling via option {\em -eva-slevel}}
+\label{slevel}
+
+The option \lstinline|-eva-slevel n| indicates that the analyzer is allowed
+to separate, in each point of the analyzed code,
+up to \lstinline|n| states from different execution paths before starting
+to compute the unions of said states. An effect of this option
+is that the states corresponding to the first, second,\ldots
+iterations in a loop remain separated, as if the loop had been unrolled.
+
+Unlike with \lstinline|loop unroll| annotations, the number \lstinline|n|
+to use with \lstinline|-eva-slevel| depends on the nature of the control flow
+graph of the function to analyze.
+If the only control structure is a loop of \lstinline|m| iterations,
+then \texttt{-eva-slevel \textsf{m+1}} allows to unroll the loop completely.
+The presence of other loops or of \lstinline|if-then-else| constructs
+multiplies the number of paths a state may correspond to,
+and thus the number of states it is necessary to keep separated
+in order to unroll a loop completely.
+For instance, the
+nested simple loops in the following example require the
+option \lstinline|-eva-slevel 55| in order to be completely unrolled:
+\lstinputlisting[numbers=left]
+ {examples/parametrizing/slevel.c}
+
+When the loops are sufficiently unrolled, the result obtained for the
+contents of array \lstinline|t| are the optimally precise:
+\lstinputlisting[linerange={14-14}]
+ {examples/parametrizing/slevel.1.log}
+
+The number to pass the option \lstinline|-eva-slevel| is of the magnitude of
+the number of values for \lstinline|i| (the 6 integers between 0 and 5)
+times the number of possible values for \lstinline|j| (the 11
+integers comprised between 0 and 10). If a value much lower than
+this is passed, the result of the initialization of array \lstinline|t|
+will only be precise for the first cells. The option \lstinline|-eva-slevel 28|
+gives for instance the following result for array \lstinline|t|:
+\lstinputlisting[linerange={15-16}]
+ {examples/parametrizing/slevel.2.log}
+
+In this result, the effects of the first iterations of the loops
+(for the whole of \lstinline|t[0]|, the whole of \lstinline|t[1]| and the first
+half of \lstinline|t[2]|) have been computed precisely. The
+effects on the rest of \lstinline|t| were computed with
+approximations. Because of these approximations, the analyzer can not
+tell whether each of those cells contains 1 or its original value 0.
+The value proposed for the cells \lstinline|t[2][5]| and following
+is imprecise but correct. The set \lstinline|{0; 1}| does
+contain the actual value \lstinline|1| of the cells.
+
+The option \lstinline|-eva-slevel-function f:n| tells the analyzer to apply
+semantic unrolling level \lstinline|n| to function \lstinline|f|.
+This fine-tuning option allows to
+force the analyzer to invest time precisely analyzing functions that matter,
+for instance \lstinline|-eva-slevel-function crucial_initialization:2000|.
+Oppositely, options \lstinline|-eva-slevel 100 -eva-slevel-function trifle:0|
+can be used together to avoid squandering resources over irrelevant parts of
+the analyzed application. The \lstinline|-eva-slevel-function| option can be used
+several times to set the semantic unrolling level of several functions.
+
+Overall, \lstinline|-eva-slevel| has the advantage of being quick to setup.
+However, it does not allow fine grained control as loop unrolling annotations,
+it is context-dependent (e.g. for nested loops), unstable (minor changes in
+control flow may affect the usage of slevel) and hard to estimate in presence
+of complex control flows.
+
+\subsubsection{Syntactic unrolling}
+
+Syntactic unrolling (option \lstinline|-ulevel n|, provided by the \FramaC
+kernel), while not recommended when using \Eva{}, is another way to unroll
+loops for a more precise analysis. The only advantage of syntactic unrolling
+is that the GUI will show separate statements, allowing
+the user to see the values of variables at each iteration.
+However, this method is slower and leads to code which may become less
+readable, due to the introduction of extra variables, labels and statements.
+
+The value \lstinline$n$ is the number of times to unroll the loop before starting
+any analysis (if larger than the number of loop iterations, the extra code will
+still be generated, but it may end up being considered unreachable by \Eva{}).
+In any case, a large value for \lstinline|n| makes the analyzed code larger,
+especially for nested loops. This may cause the analyzer to use more time and
+memory.
+
+It is possible to control syntactic unrolling for each loop in the analyzed code
+with the annotation \lstinline|//@loop pragma UNROLL n;|, placed before the loop.
+
+
+\subsection{Widening hints and loop invariants}
+
+Besides loop unrolling, another technique to improve precision in loops
+consists in using the standard computation by accumulation mechanism present in
+tools based on abstract interpretation. This mechanism requires a more involved
+setup, but can lead to more efficient analyses.
As compared to loop unrolling, the advantage of the computation
by accumulation is that it generally requires less iterations
@@ -3199,7 +3426,7 @@ parameters in the widening process, it may (rarely) be appropriate
to help it by providing it with the bounds that are likely to
be reached, for a given variable modified inside a loop.
-\subsubsection{Stipulating bounds}
+\subsubsection{Widening hints}
\label{subsub:widen-hints}
The user may place an annotation \lstinline|//@ widen_hints $v$, $e_1,\ldots,e_m$ ;|
@@ -3271,103 +3498,10 @@ Example:
\lstinputlisting[numbers=left]
{examples/parametrizing/pragma-widen-hints.c}
-\subsubsection{Loop unrolling}\label{deroulage}
-
-There are two different options for forcing \Eva{}
-to unroll the effects of the body of the loop, as many times as
-specified, in order to obtain a precise representation of the effects
-of the loop itself. If the number of iterations is sufficient,
-the analyzer is thus able to determine that each cell in the array
-is initialized, as opposed to the approximation techniques
-from the previous section.
-
-\paragraph{Syntactic unrolling}
-
-The option \lstinline|-ulevel n| indicates that Frama-C should unroll
-the loops syntactically \lstinline$n$ times before starting any analysis.
-If the provided number \lstinline|n| is larger than the number of iterations
-of the loop, then the loop is completely unrolled and the analysis will
-not observe any loop in that part of the code.
-
-Providing a large value for \lstinline|n| makes the analyzed code bigger:
-this may cause the analyzer to use more time and memory. This option
-can also make the code notably bigger in presence of
-nested loops (polynomially bigger in the depth of nested loops). A large value
-should therefore not be used in this case.
-
-It is possible to control the syntactic unrolling for each
-loop in the analyzed code with the annotation
-\lstinline|//@ loop pragma UNROLL n;|. The user should place
-this annotation in the source code, just before
-the loop. This annotation causes Frama-C's front-end to unroll
-the loop \lstinline|n| times.
-
-\paragraph{Semantic unrolling}
-\label{slevel}
-
-The option \lstinline|-eva-slevel n| indicates that the analyzer is allowed
-to separate, in each point of the analyzed code,
-up to \lstinline|n| states from different execution paths before starting
-to compute the unions of said states. An effect of this option
-is that the states corresponding to the first, second,\ldots
-iterations in the loop remain separated, as if the loop had been
-unrolled.
-
-The number \lstinline|n| to use depends on the
-nature of the control flow graph of the function to analyze.
-If the only control structure is a loop of \lstinline|m| iterations,
-then \texttt{-eva-slevel \textsf{m+1}} allows to unroll the loop completely.
-The presence of other loops or of \lstinline|if-then-else| constructs
-multiplies the number of paths a state may correspond to,
-and thus the number of states it is necessary to keep separated
-in order to unroll a loop completely.
-For instance, the
-nested simple loops in the following example require the
-option \lstinline|-eva-slevel 55| in order to be completely unrolled:
-\lstinputlisting[numbers=left]
- {examples/parametrizing/slevel.c}
-
-When the loops are sufficiently unrolled, the result obtained for the
-contents of array \lstinline|t| are the optimally precise:
-\lstinputlisting[linerange={14-14}]
- {examples/parametrizing/slevel.1.log}
-
-The number to pass the option \lstinline|-eva-slevel| is of the magnitude of
-the number of values for \lstinline|i| (the 6 integers between 0 and 5)
-times the number of possible values for \lstinline|j| (the 11
-integers comprised between 0 and 10). If a value much lower than
-this is passed, the result of the initialization of array \lstinline|t|
-will only be precise for the first cells. The option \lstinline|-eva-slevel 28|
-gives for instance the following result for array \lstinline|t|:
-\lstinputlisting[linerange={15-16}]
- {examples/parametrizing/slevel.2.log}
-
-In this result, the effects of the first iterations of the loops
-(for the whole of \lstinline|t[0]|, the whole of \lstinline|t[1]| and the first
-half of \lstinline|t[2]|) have been computed precisely. The
-effects on the rest of \lstinline|t| were computed with
-approximations. Because of these approximations, the analyzer can not
-tell whether each of those cells contains 1 or its original value 0.
-The value proposed for the cells \lstinline|t[2][5]| and following
-is imprecise but correct. The set \lstinline|{0; 1}| does
-contain the actual value \lstinline|1| of the cells.
-
-The option \lstinline|-eva-slevel-function f:n| tells the analyzer to apply
-semantic unrolling level \lstinline|n| to function \lstinline|f|.
-This fine-tuning option allows to
-force the analyzer to invest time precisely analyzing functions that matter,
-for instance \lstinline|-eva-slevel-function crucial_initialization:2000|.
-Oppositely, options \lstinline|-eva-slevel 100 -eva-slevel-function trifle:0|
-can be used together to avoid squandering resources over irrelevant parts of
-the analyzed application. The \lstinline|-eva-slevel-function| option can be used
-several times to set the semantic unrolling level of several functions.
-
-
\subsubsection{Loop invariants}
-A last technique, complementary to the unrolling ones above,
-consists in using the loop invariant construct of ACSL. Loop invariants
-describe some
+A last technique consists in using the loop invariant construct of ACSL.
+Loop invariants describe some
properties that hold at the beginning of each execution of a loop,
as explained in the ACSL specification, \S2.4.2.
%\url{http://frama-c.com/download/acsl.pdf}
@@ -3430,127 +3564,99 @@ We have effectively replaced an alarm, the possible out-of-bounds access at
line~7, by an invariant, that remains to be proven.
-\subsection{Treatment of functions}
-\label{trait_fonctions}
-
-\subsubsection{Skipping the recording of the results of a function}
-\label{noresults}
-
-When a function \lstinline|f|
-is called many times, or, in presence of semantic unrolling,
-if \lstinline|f| contains large/nested loops, significant
-time may be spent recording the values taken by the program's variables
-at each of \lstinline|f|'s statements.
-If the user knows that these values will not be useful later,
-ey can instruct \Eva{} not to record these with the
-\lstinline|-eva-no-results-function f| option.
-The \lstinline|-eva-no-results-function| option
-can be used several times, to omit the results of several functions.
-The option \lstinline|-eva-no-results| can be used to omit all
-results.
-It can result in a significant saving of time, as in the following example.
-
-\lstinputlisting[numbers=left]
- {examples/parametrizing/nor.c}
-
-\begin{shell}
-time frama-c -eva nor.c -eva-slevel 2001
-\end{shell}
-
-\lstinputlisting[linerange={30-33},numbers=left,firstnumber=36]
- {examples/parametrizing/nor.1.log}
-\lstinputlisting[linerange={2032-2035},numbers=left,firstnumber=2036]
- {examples/parametrizing/nor.1.log}
-\lstinputlisting[linerange={4032-4036},numbers=left,firstnumber=4038]
- {examples/parametrizing/nor.1.log}
-
-Launched with option \lstinline|-eva-slevel 2001| so that the value returned
-by \lstinline|main| can be computed precisely, the analysis takes more than
-half a second.
- Contrast with:
-
-\begin{shell}
-time frama-c -eva nor.c -eva-slevel 2001 -eva-no-results-function irrelevant_function
-\end{shell}
-
-\lstinputlisting[linerange={30-34},numbers=left,firstnumber=36]
- {examples/parametrizing/nor.2.log}
-\lstinputlisting[linerange={2031-2035},numbers=left,firstnumber=2037]
- {examples/parametrizing/nor.2.log}
-
-When instructed, with
-option \lstinline|-eva-no-results-function irrelevant_function|,
-that the values for the function
-\lstinline|irrelevant_function| do not need to be kept, \Eva{}
-takes less than half the time to produce its results. This shows
-that in the earlier analysis, most of the time was not spent in the
-analysis itself but in recording the values
-of \lstinline|irrelevant_function|.
-
-Note that the function \lstinline|irrelevant_function| was analyzed with
-as much precision as before, and that the result for \lstinline|main| is
-as precise as before. The recording of some results
-is omitted, but this does not cause any loss of precision {\em during}
-the analysis\footnote{The emission of run-time error alarms and the evaluation
-of user-provided ACSL properties are done during the analysis and are
-not influenced by the {\tt -eva-no-results*} options. If you make use
-of only these functionalities, then you can speed up the analysis
-with option {\tt -eva-no-results} without detrimental effects.}.
-The results for \verb|irrelevant_function| are, as expected, unavailable.
-The ``outputs'' of \verb|main| (the ``outputs'' computation is
-described in chapter \ref{inoutdeps}) cannot be computed, because
-they depend on the outputs of \lstinline|irrelevant_function|, which
-require the values of that function to be computed.
-These outputs would automatically be used for
-displaying only the relevant variables if they were available.
-Instead, all the program's variables are displayed.
-
-The meaning of option \lstinline|-eva-no-results-function irrelevant_function|
-is different from that of option
-\lstinline|-eva-slevel-function irrelevant_function:0|. In the case of the latter,
-values
-are computed with less precision for \verb|irrelevant_function|
-but the computed values are kept in memory as usual.
-All derived analyses (such as outputs)
-are available, but the values predicted by the analysis are
-less precise, because \verb|irrelevant_function| has been analyzed
-less precisely.
-
-\subsubsection{Using the specification of a function instead of its body}
-\label{val-use-spec}
-
-In some cases, one can estimate that the analysis of a given function \verb+f+
-takes too much time. This can be caused by a very complex
-function, or because \verb+f+ is called many times during the analysis.
-If the solutions of the previous section are not sufficient, a radical
-approach consists in replacing the entire body of the function
-by an ACSL contract, that describes its behavior. See for example
-section~\ref{annot_assigns} for how to specify which values the function
-reads and writes.
-
-Alternatively, one can leave the body of the function untouched, but
-still write a contract. Then it is possible to use the option
-\verb+-eva-use-spec f+. This instructs \Eva{} to use the
-specification of \verb+f+ instead of its body each time a call to
-\verb+f+ is encountered. This is equivalent\footnote{Except for a few
- properties, as described in the next paragraph.} to deleting the body
-of \verb+f+ for \Eva{}, but not for the other plug-ins of \FramaC,
-that may study the body of \verb+f+ on their own.
-
-Notice that option \verb+-eva-use-spec f+ loses some guarantees. In particular,
-the body of \verb+f+ is not studied at all by \Eva{}. Neither
-are the functions that \verb+f+ calls, unless they are used by some other
-functions than \verb+f+. Moreover, \Eva{} does not attempt
-to check that \verb+f+ conforms to its specification. In particular,
-postconditions are marked as {\em unknown} with \verb+-eva-use-spec+,
-while they are {\em considered valid} for functions without body.
-It is the responsibility
-of the user to verify those facts, for example by studying \verb+f+
-on its own in a generic context.
-
+%% \section{Treatment of functions}
+%% \label{trait_fonctions}
+
+%% Some \Eva{} options can be used to handle certain functions in a special
+%% way, to improve the efficiency of the analysis.
+
+
+%% \subsubsection{Skipping the recording of the results of a function}
+%% \label{noresults}
+
+%% When a function \lstinline|f|
+%% is called many times, or, in presence of semantic unrolling,
+%% if \lstinline|f| contains large/nested loops, significant
+%% time may be spent recording the values taken by the program's variables
+%% at each of \lstinline|f|'s statements.
+%% If the user knows that these values will not be useful later,
+%% ey can instruct \Eva{} not to record these with the
+%% \lstinline|-eva-no-results-function f| option.
+%% The \lstinline|-eva-no-results-function| option
+%% can be used several times, to omit the results of several functions.
+%% The option \lstinline|-eva-no-results| can be used to omit all
+%% results.
+%% It can result in a significant saving of time, as in the following example.
+
+%% \lstinputlisting[numbers=left]
+%% {examples/parametrizing/nor.c}
+
+%% \begin{shell}
+%% time frama-c -eva nor.c -eva-slevel 2001
+%% \end{shell}
+
+%% \lstinputlisting[linerange={30-33},numbers=left,firstnumber=36]
+%% {examples/parametrizing/nor.1.log}
+%% \lstinputlisting[linerange={2032-2035},numbers=left,firstnumber=2036]
+%% {examples/parametrizing/nor.1.log}
+%% \lstinputlisting[linerange={4032-4036},numbers=left,firstnumber=4038]
+%% {examples/parametrizing/nor.1.log}
+
+%% Launched with option \lstinline|-eva-slevel 2001| so that the value returned
+%% by \lstinline|main| can be computed precisely, the analysis takes more than
+%% half a second.
+%% Contrast with:
+
+%% \begin{shell}
+%% time frama-c -eva nor.c -eva-slevel 2001 -eva-no-results-function irrelevant_function
+%% \end{shell}
+
+%% \lstinputlisting[linerange={30-34},numbers=left,firstnumber=36]
+%% {examples/parametrizing/nor.2.log}
+%% \lstinputlisting[linerange={2031-2035},numbers=left,firstnumber=2037]
+%% {examples/parametrizing/nor.2.log}
+
+%% When instructed, with
+%% option \lstinline|-eva-no-results-function irrelevant_function|,
+%% that the values for the function
+%% \lstinline|irrelevant_function| do not need to be kept, \Eva{}
+%% takes less than half the time to produce its results. This shows
+%% that in the earlier analysis, most of the time was not spent in the
+%% analysis itself but in recording the values
+%% of \lstinline|irrelevant_function|.
+
+%% Note that the function \lstinline|irrelevant_function| was analyzed with
+%% as much precision as before, and that the result for \lstinline|main| is
+%% as precise as before. The recording of some results
+%% is omitted, but this does not cause any loss of precision {\em during}
+%% the analysis\footnote{The emission of run-time error alarms and the evaluation
+%% of user-provided ACSL properties are done during the analysis and are
+%% not influenced by the {\tt -eva-no-results*} options. If you make use
+%% of only these functionalities, then you can speed up the analysis
+%% with option {\tt -eva-no-results} without detrimental effects.}.
+%% The results for \verb|irrelevant_function| are, as expected, unavailable.
+%% The ``outputs'' of \verb|main| (the ``outputs'' computation is
+%% described in chapter \ref{inoutdeps}) cannot be computed, because
+%% they depend on the outputs of \lstinline|irrelevant_function|, which
+%% require the values of that function to be computed.
+%% These outputs would automatically be used for
+%% displaying only the relevant variables if they were available.
+%% Instead, all the program's variables are displayed.
+
+%% The meaning of option \lstinline|-eva-no-results-function irrelevant_function|
+%% is different from that of option
+%% \lstinline|-eva-slevel-function irrelevant_function:0|. In the case of the latter,
+%% values
+%% are computed with less precision for \verb|irrelevant_function|
+%% but the computed values are kept in memory as usual.
+%% All derived analyses (such as outputs)
+%% are available, but the values predicted by the analysis are
+%% less precise, because \verb|irrelevant_function| has been analyzed
+%% less precisely.
-\section{Analysis cutoff values}
+\section{Controlling approximations}
+\label{controlling-approximations}
\subsection{Cutoff between integer sets and integer intervals}
@@ -3576,6 +3682,36 @@ analysis result then becomes:
\lstinputlisting[linerange={23-23}]
{examples/parametrizing/ilevel.2.log}
+\subsection{Maximum number of precise items in arrays}
+
+Option \verb|-eva-plevel <n>| is used to limit the number of elements
+in an array that can be considered precisely during assignments.
+When assigning a value to an array element, if the index is imprecise,
+it may be very costly to update each array element individually.
+Instead, if the range of indices to be accessed is larger than {\em plevel},
+some approximations are made and a message is emitted:
+
+\begin{lstlisting}
+[kernel] arrays.c:32:
+ more than 200(300) elements to enumerate. Approximating.
+\end{lstlisting}
+
+This message means that the array to be updated had 300 elements, and
+\verb|-eva-plevel| was set to 200 (the default value). In this case, it
+might be reasonable to increase the plevel to 300, especially if some alarms
+could be caused by the imprecision. In other cases, however, there is little
+hope of obtaining a reasonable bound:
+
+\begin{lstlisting}
+more than 200(0x20000000) elements to enumerate. Approximating.
+\end{lstlisting}
+
+In some cases, lowering the plevel can improve performance, but it is rarely
+a significant factor. Most of the time, this option has little impact in the
+analysis, both in terms of precision and performance. However, when dealing
+with large arrays and matrices, it is worth considering its usage.
+
+
\section{Advanced analyses}
\label{sec:eva}
@@ -3835,7 +3971,7 @@ interpreted as leading to any possible value.
Moreover, the domain only infers error values for scalar variables. Structure
and union fields, as well as arrays, are ignored.
-\section{Non-termination}
+\section{Non-termination}\label{nonterm}
The parameterization of \Eva{} can lead to situations where the
analysis stops abruptly due to the absence of valid states. For instance,
@@ -4138,7 +4274,7 @@ to prove is therefore the assertion at line 8.
\subsubsection{Case analysis}
-When using {\em semantic unrolling} (section \ref{deroulage}), if an
+When using {\em slevel-based unrolling} (section \ref{slevel}), if an
assertion is a disjunction, then the reduction of the state by the
assertion may be computed independently for each disjunct. This
multiplies the number of states to propagate in the same way that
diff --git a/doc/value/makefile b/doc/value/makefile
index 63e44b450e00db4cbfd4306b1ad75eefdb415c50..01b7f9053b1dda140a0973bba93923607f0745c6 100644
--- a/doc/value/makefile
+++ b/doc/value/makefile
@@ -23,5 +23,5 @@ clean:
rm -f $(GENERATED)
install:
- rm -f ../manuals/value-analysis.pdf
- cp main.pdf ../manuals/value-analysis.pdf
+ rm -f ../manuals/eva-manual.pdf
+ cp main.pdf ../manuals/eva-manual.pdf
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index ffc7b2ce0a5815d7b34a636826b50ecc5349b42d..36de74a9f38df23c208828edc7d84fa141a14027 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -116,9 +116,16 @@ share/_frama-c: CEA_LGPL
share/analysis-scripts/frama-c.mk: CEA_LGPL
share/analysis-scripts/README.md: .ignore
share/analysis-scripts/cmd-dep.sh: .ignore
+share/analysis-scripts/concat-csv.sh: .ignore
+share/analysis-scripts/examples/example.c: .ignore
+share/analysis-scripts/examples/example.mk: .ignore
+share/analysis-scripts/examples/example-multi.mk: .ignore
+share/analysis-scripts/examples/example-slevel.mk: .ignore
+share/analysis-scripts/examples/Makefile: .ignore
share/analysis-scripts/flamegraph.pl: CDDL
share/analysis-scripts/list_files.py: .ignore
share/analysis-scripts/parse-coverage.sh: .ignore
+share/analysis-scripts/summary.sh: .ignore
share/analysis-scripts/template.mk: .ignore
share/autocomplete_frama-c: CEA_LGPL
share/Makefile.clean: CEA_LGPL
diff --git a/opam/opam b/opam/opam
index df7158ed6fb625a5804c020bf4ed21ce0b1e56f7..0a110bc90757aabb50e35f00d1a0763aad538878 100644
--- a/opam/opam
+++ b/opam/opam
@@ -44,7 +44,7 @@ authors: [
homepage: "http://frama-c.com/"
license: "GNU Lesser General Public License version 2.1"
dev-repo: "git+https://github.com/Frama-C/Frama-C-snapshot.git#latest"
-doc: "http://frama-c.com/download/user-manual-Chlorine-20180501.pdf"
+doc: "http://frama-c.com/download/user-manual-18.0-Argon.pdf"
bug-reports: "https://bts.frama-c.com/"
tags: [
"deductive"
diff --git a/src/kernel_internals/runtime/config.mli b/src/kernel_internals/runtime/config.mli
index 2d49810b265d24d7e86ea0f63a62cf3e40ec605c..70375d377faa650139f600ade9b5edc557acf1e3 100644
--- a/src/kernel_internals/runtime/config.mli
+++ b/src/kernel_internals/runtime/config.mli
@@ -28,11 +28,11 @@ val version: string
val codename: string
(** Frama-C version codename.
- @since Frama-C+dev *)
+ @since 18.0-Argon *)
val version_and_codename: string
(** Frama-C version and codename.
- @since Frama-C+dev *)
+ @since 18.0-Argon *)
val is_gui: bool ref
(** Is the Frama-C GUI running?
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index 38c85c983aa9b6220ae22506663dfa104b1a92f5..6aea5a03a1390e04aba9a8614cc008473c8c3c28 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -1671,7 +1671,7 @@ and acsl_extension_kind =
(** Where are we expected to find corresponding extension keyword.
@plugin development guide
- @since Frama-C+dev
+ @since 18.0-Argon
*)
and ext_category =
| Ext_contract
diff --git a/src/kernel_services/ast_data/globals.mli b/src/kernel_services/ast_data/globals.mli
index b5127dab9e63c7ee5102bdbbd9d00397d9ef37e1..d80e4af7670f923d25bd0e21f1caea1bc46b71fa 100644
--- a/src/kernel_services/ast_data/globals.mli
+++ b/src/kernel_services/ast_data/globals.mli
@@ -75,7 +75,7 @@ module Vars: sig
val remove: varinfo -> unit
(** Removes the given varinfo, which must have already been removed from the
AST. Warning: this is very dangerous.
- @since Frama-C+dev
+ @since 18.0-Argon
*)
val add_decl: varinfo -> unit
@@ -131,7 +131,7 @@ module Functions: sig
val remove: varinfo -> unit
(** Removes the given varinfo, which must have already been removed from the
AST. Warning: this is very dangerous.
- @since Frama-C+dev
+ @since 18.0-Argon
*)
val replace_by_declaration: funspec -> varinfo -> location -> unit
@@ -164,7 +164,7 @@ module FileIndex : sig
[@@deprecated "Use FileIndex.get_symbols instead."]
(** [find path] returns all global C symbols associated with [path],
plus [path] itself. The returned [global] list is reversed.
- @deprecated Frama-C+dev use [get_symbols] instead. *)
+ @deprecated 18.0-Argon use [get_symbols] instead. *)
val get_files: unit -> Datatype.Filepath.t list
(** Get the files list containing all [global] C symbols. *)
diff --git a/src/kernel_services/ast_data/kernel_function.mli b/src/kernel_services/ast_data/kernel_function.mli
index 501f1323be4686be7f89a9d0d83309aac65a421c..db00a8d5768d7120fb9a17069db38b4aa7f1be7d 100644
--- a/src/kernel_services/ast_data/kernel_function.mli
+++ b/src/kernel_services/ast_data/kernel_function.mli
@@ -161,7 +161,7 @@ val get_locals : t -> varinfo list
val get_statics : t -> varinfo list
(** Returns the list of static variables declared inside the function.
- @since Frama-C+dev *)
+ @since 18.0-Argon *)
exception No_Definition
val get_definition : t -> fundec
diff --git a/src/kernel_services/ast_data/property.mli b/src/kernel_services/ast_data/property.mli
index 9a852748600d19d00d7398fa09b4bfda310718dc..254ef04db0c75f395bc00644ebbbd356e9bc2910 100644
--- a/src/kernel_services/ast_data/property.mli
+++ b/src/kernel_services/ast_data/property.mli
@@ -164,15 +164,15 @@ val pretty_predicate_kind: Format.formatter -> predicate_kind -> unit
val pretty_debug: Format.formatter -> identified_property -> unit
(** Internal use only.
- @since Frama-C+dev *)
+ @since 18.0-Argon *)
(** create a Loc_contract or Loc_stmt depending on the kinstr.
- @since Frama-C+dev
+ @since 18.0-Argon
*)
val e_loc_of_stmt: kernel_function -> kinstr -> extended_loc
(** create a Loc_contract or Loc_stmt depending on the kinstr.
- @since Frama-C+dev
+ @since 18.0-Argon
*)
val o_loc_of_stmt: kernel_function -> kinstr -> other_loc
@@ -184,7 +184,7 @@ val o_loc_of_stmt: kernel_function -> kinstr -> other_loc
val ip_other: string -> other_loc -> identified_property
(** Create a non-standard property.
@since Nitrogen-20111001
- @modify Frama-C+dev Refine localisation argument
+ @modify 18.0-Argon Refine localisation argument
*)
val ip_reachable_stmt: kernel_function -> stmt -> identified_property
@@ -223,7 +223,7 @@ val ip_of_ensures:
(** Extended property.
@since Chlorine-20180501
- @modify Frama-C+dev refine localisation argument
+ @modify 18.0-Argon refine localisation argument
*)
val ip_of_extended: extended_loc -> acsl_extension -> identified_property
diff --git a/src/kernel_services/ast_printing/description.mli b/src/kernel_services/ast_printing/description.mli
index 9ec78a06ac1e9970b33e2dbb1b52c56d8d8b3f42..02b1ea479eef6d4c1174fd8e2bb51393d9284250 100644
--- a/src/kernel_services/ast_printing/description.mli
+++ b/src/kernel_services/ast_printing/description.mli
@@ -53,11 +53,11 @@ val pp_property : Format.formatter -> Property.t -> unit
val property_kind_and_node: Property.t -> (string * string) option
(** Returns separately the kind and the node of a property. Returns None for
unsupported property kinds. Used to output properties in csv files.
- @since Frama-C+dev *)
+ @since 18.0-Argon *)
val status_feedback: Property_status.Feedback.t -> string
(** User-friendly description of property statuses.
- @since Frama-C+dev *)
+ @since 18.0-Argon *)
type kf = [ `Always | `Never | `Context of kernel_function ]
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 2b7ca72f32c254d82e1eae2640897c25f2438e1a..ec5424a8b4737a8b5d4f2fa0542525ebfb922b8d 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -470,7 +470,7 @@ val isCompleteType: ?allowZeroSizeArrays:bool -> typ -> bool
array member. When in gcc mode, a zero-sized array is identified with a
FAM for this purpose.
- @since Frama-C+dev
+ @since 18.0-Argon
*)
val has_flexible_array_member: typ -> bool
@@ -542,27 +542,27 @@ val isIntegralOrPointerType: typ -> bool
(** True if the argument is an integral type (i.e. integer or enum), either
C or mathematical one.
- @modify Frama-C+dev expands the logic type definition if necessary. *)
+ @modify 18.0-Argon expands the logic type definition if necessary. *)
val isLogicIntegralType: logic_type -> bool
(** True if the argument is a boolean type, either integral C type or
mathematical boolean one.
- @modify Frama-C+dev expands the logic type definition if necessary. *)
+ @modify 18.0-Argon expands the logic type definition if necessary. *)
val isLogicBooleanType: logic_type -> bool
(** True if the argument is a floating point type. *)
val isFloatingType: typ -> bool
(** True if the argument is a floating point type.
- @modify Frama-C+dev expands the logic type definition if necessary. *)
+ @modify 18.0-Argon expands the logic type definition if necessary. *)
val isLogicFloatType: logic_type -> bool
(** True if the argument is a C floating point type or logic 'real' type.
- @modify Frama-C+dev expands the logic type definition if necessary. *)
+ @modify 18.0-Argon expands the logic type definition if necessary. *)
val isLogicRealOrFloatType: logic_type -> bool
(** True if the argument is the logic 'real' type.
- @modify Frama-C+dev expands the logic type definition if necessary. *)
+ @modify 18.0-Argon expands the logic type definition if necessary. *)
val isLogicRealType: logic_type -> bool
(** True if the argument is an arithmetic type (i.e. integer, enum or
@@ -575,7 +575,7 @@ val isArithmeticOrPointerType: typ -> bool
(** True if the argument is a logic arithmetic type (i.e. integer, enum or
floating point, either C or mathematical one.
- @modify Frama-C+dev expands the logic type definition if necessary. *)
+ @modify 18.0-Argon expands the logic type definition if necessary. *)
val isLogicArithmeticType: logic_type -> bool
(** True if the argument is a function type *)
@@ -583,23 +583,23 @@ val isFunctionType: typ -> bool
(** True if the argument is the logic function type.
Expands the logic type definition if necessary.
- @since Frama-C+dev *)
+ @since 18.0-Argon *)
val isLogicFunctionType: logic_type -> bool
(** True if the argument is a pointer type. *)
val isPointerType: typ -> bool
(** True if the argument is a function pointer type.
- @since Frama-C+dev *)
+ @since 18.0-Argon *)
val isFunPtrType: typ -> bool
(** True if the argument is the logic function pointer type.
Expands the logic type definition if necessary.
- @since Frama-C+dev *)
+ @since 18.0-Argon *)
val isLogicFunPtrType: logic_type -> bool
(** True if the argument is the type for reified C types.
- @modify Frama-C+dev expands the logic type definition if necessary. *)
+ @modify 18.0-Argon expands the logic type definition if necessary. *)
val isTypeTagType: logic_type -> bool
(** True if the argument denotes the type of ... in a variadic function.
@@ -1184,7 +1184,7 @@ val dropAttributes: string list -> attributes -> attributes
(** a field struct marked with this attribute is known to be mutable, i.e.
it can be modified even on a const object.
- @since Frama-C+dev
+ @since 18.0-Argon
*)
val frama_c_mutable: string
@@ -1192,7 +1192,7 @@ val frama_c_mutable: string
object being initialized by the current function, which can thus assign
any sub-object regardless of const status.
- @since Frama-C+dev
+ @since 18.0-Argon
*)
val frama_c_init_obj: string
diff --git a/src/kernel_services/ast_queries/logic_const.mli b/src/kernel_services/ast_queries/logic_const.mli
index a9353c9609de93781af178547bee2e7d9f68ee87..0a10bccaffa9298760d40a61d79bd93371ec2ff7 100644
--- a/src/kernel_services/ast_queries/logic_const.mli
+++ b/src/kernel_services/ast_queries/logic_const.mli
@@ -198,18 +198,18 @@ val pseparated: ?loc:location -> term list -> predicate
(* ************************************************************************** *)
(** instantiate type variables in a logic type.
- @since Frama-C+dev moved from Logic_utils *)
+ @since 18.0-Argon moved from Logic_utils *)
val instantiate :
(string * logic_type) list ->
logic_type -> logic_type
(** @return [true] if the logic type definition can be expanded.
- @since Frama-C+dev *)
+ @since 18.0-Argon *)
val is_unrollable_ltdef : logic_type_info -> bool
(** expands logic type definitions only.
To expands both logic part and C part, uses [Logic_utils.unroll_type].
- @since Frama-C+dev *)
+ @since 18.0-Argon *)
val unroll_ltdef : logic_type -> logic_type
(** [isLogicType test typ] is [false] for pure logic types and the result
@@ -218,7 +218,7 @@ val isLogicCType : (typ -> bool) -> logic_type -> bool
(** returns [true] if the type is a list<t>.
@since Aluminium-20160501
- @modify Frama-C+dev expands the logic type definition if necessary. *)
+ @modify 18.0-Argon expands the logic type definition if necessary. *)
val is_list_type: logic_type -> bool
(** [make_type_list_of t] returns the type list<[t]>.
@@ -228,52 +228,52 @@ val make_type_list_of: logic_type -> logic_type
(** returns the type of elements of a list type.
@raise Failure if the input type is not a list type.
@since Aluminium-20160501
- @modify Frama-C+dev expands the logic type definition if necessary. *)
+ @modify 18.0-Argon expands the logic type definition if necessary. *)
val type_of_list_elem: logic_type -> logic_type
(** returns [true] if the type is a set<t>.
@since Neon-20140301
- @modify Frama-C+dev expands the logic type definition if necessary. *)
+ @modify 18.0-Argon expands the logic type definition if necessary. *)
val is_set_type: logic_type -> bool
(** [set_conversion ty1 ty2] returns a set type as soon as [ty1] and/or [ty2]
is a set. Elements have type [ty1], or the type of the elements of [ty1] if
it is itself a set-type ({i.e.} we do not build set of sets that way).
- @modify Frama-C+dev expands the logic type definitions if necessary. *)
+ @modify 18.0-Argon expands the logic type definitions if necessary. *)
val set_conversion: logic_type -> logic_type -> logic_type
(** converts a type into the corresponding set type if needed. Does nothing
if the argument is already a set type.
- @modify Frama-C+dev expands the logic type definition if necessary. *)
+ @modify 18.0-Argon expands the logic type definition if necessary. *)
val make_set_type: logic_type -> logic_type
(** returns the type of elements of a set type.
@raise Failure if the input type is not a set type.
- @modify Frama-C+dev expands the logic type definition if necessary. *)
+ @modify 18.0-Argon expands the logic type definition if necessary. *)
val type_of_element: logic_type -> logic_type
(** [plain_or_set f t] applies [f] to [t] or to the type of elements of [t]
if it is a set type.
- @modify Frama-C+dev expands the logic type definition if necessary. *)
+ @modify 18.0-Argon expands the logic type definition if necessary. *)
val plain_or_set: (logic_type -> 'a) -> logic_type -> 'a
(** [transform_element f t] is the same as
[set_conversion (plain_or_set f t) t]
@since Nitrogen-20111001
- @modify Frama-C+dev expands the logic type definition if necessary.
+ @modify 18.0-Argon expands the logic type definition if necessary.
*)
val transform_element: (logic_type -> logic_type) -> logic_type -> logic_type
(** [true] if the argument is not a set type.
- @modify Frama-C+dev expands the logic type definition if necessary. *)
+ @modify 18.0-Argon expands the logic type definition if necessary. *)
val is_plain_type: logic_type -> bool
(** @return true if the argument is the boolean type.
- @modify Frama-C+dev expands the logic type definition if necessary. *)
+ @modify 18.0-Argon expands the logic type definition if necessary. *)
val is_boolean_type: logic_type -> bool
(** @since Sodium-20150201
- @modify Frama-C+dev expands the logic type definition if necessary. *)
+ @modify 18.0-Argon expands the logic type definition if necessary. *)
val boolean_type: logic_type
(* ************************************************************************** *)
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index d7eb312fc1d66a140a49c6547653a6db67f3efdb..e978b3e829ab0e7a77f27cc5dbcf961bcd189fec 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -177,7 +177,7 @@ val register_behavior_extension:
@plugin development guide
- @since Frama-C+dev
+ @since 18.0-Argon
*)
val register_global_extension:
string ->
@@ -189,7 +189,7 @@ val register_global_extension:
@plugin development guide
- @since Frama-C+dev
+ @since 18.0-Argon
*)
val register_code_annot_extension:
string ->
@@ -201,7 +201,7 @@ val register_code_annot_extension:
@plugin development guide
- @since Frama-C+dev
+ @since 18.0-Argon
*)
val register_code_annot_next_stmt_extension:
string ->
@@ -212,7 +212,7 @@ val register_code_annot_next_stmt_extension:
@plugin development guide
- @since Frama-C+dev
+ @since 18.0-Argon
*)
val register_code_annot_next_loop_extension:
string ->
@@ -224,7 +224,7 @@ val register_code_annot_next_loop_extension:
@plugin development guide
- @since Frama-C+dev
+ @since 18.0-Argon
*)
val register_code_annot_next_both_extension:
string ->
diff --git a/src/kernel_services/parsetree/logic_ptree.mli b/src/kernel_services/parsetree/logic_ptree.mli
index 8b5b418cda57ec1407e6583aaffd88ae0b5270c0..ea5a3d072be27850366bb39e8d82daefc4fa70da 100644
--- a/src/kernel_services/parsetree/logic_ptree.mli
+++ b/src/kernel_services/parsetree/logic_ptree.mli
@@ -369,7 +369,7 @@ type code_annot =
| AExtended of string list * bool * extension
(** extension in a code or loop (when boolean flag is true) annotation.
@since Silicon-20161101
- @modify Frama-C+dev
+ @modify 18.0-Argon
*)
(** custom trees *)
diff --git a/src/kernel_services/plugin_entry_points/log.mli b/src/kernel_services/plugin_entry_points/log.mli
index 1efef9b18217cbc189d356ce1be767f5b3887ba8..436820f29d8691c8bbdd16bcc1618f7306cca624 100644
--- a/src/kernel_services/plugin_entry_points/log.mli
+++ b/src/kernel_services/plugin_entry_points/log.mli
@@ -221,22 +221,22 @@ module type Messages = sig
val with_result : (event option -> 'b) -> ('a,'b) pretty_aborter
(** [with_result f fmt] calls [f] in the same condition as [logwith].
@since Beryllium-20090601-beta1
- @modified Frama-C+dev the argument of the continuation is optionnal *)
+ @modified 18.0-Argon the argument of the continuation is optionnal *)
val with_warning : (event option -> 'b) -> ('a,'b) pretty_aborter
(** [with_warning f fmt] calls [f] in the same condition as [logwith].
@since Beryllium-20090601-beta1
- @modified Frama-C+dev the argument of the continuation is optionnal *)
+ @modified 18.0-Argon the argument of the continuation is optionnal *)
val with_error : (event option -> 'b) -> ('a,'b) pretty_aborter
(** [with_error f fmt] calls [f] in the same condition as [logwith].
@since Beryllium-20090601-beta1
- @modified Frama-C+dev the argument of the continuation is optionnal *)
+ @modified 18.0-Argon the argument of the continuation is optionnal *)
val with_failure : (event option -> 'b) -> ('a,'b) pretty_aborter
(** [with_failure f fmt] calls [f] in the same condition as [logwith].
@since Beryllium-20090601-beta1
- @modified Frama-C+dev the argument of the continuation is optionnal *)
+ @modified 18.0-Argon the argument of the continuation is optionnal *)
val log : ?kind:kind -> ?verbose:int -> ?debug:int -> 'a pretty_printer
(** Generic log routine. The default kind is [Result]. Use cases (with
@@ -261,7 +261,7 @@ module type Messages = sig
In case the [wkey] is considered as a [Failure], the continution is not called.
This kind of message denotes a fatal error aborting Frama-C.
Notice that the [~emitwith] action is called iff a message is logged.
- @since Frama-C+dev *)
+ @since 18.0-Argon *)
val register : kind -> (event -> unit) -> unit
(** Local registry for listeners. *)
@@ -284,7 +284,7 @@ module type Messages = sig
val dkey_name: category -> string
(** returns the category name as a string.
- @since Frama-C+dev
+ @since 18.0-Argon
*)
val is_registered_category: string -> bool
@@ -346,7 +346,7 @@ module type Messages = sig
val wkey_name: warn_category -> string
(** returns the warning category name as a string.
- @since Frama-C+dev
+ @since 18.0-Argon
*)
val get_warn_category: string -> warn_category option
@@ -362,19 +362,19 @@ module type Messages = sig
end
(** Split an event category into its constituants.
- @since Frama-C+dev *)
+ @since 18.0-Argon *)
val evt_category : event -> string list
(** Split a category specification into its constituants.
["*"] is considered as empty, and [""] categories are skipped.
- @since Frama-C+dev *)
+ @since 18.0-Argon *)
val split_category : string -> string list
(** Sub-category checks.
[is_subcategory a b] checks whether [a] is a sub-category of [b].
Indeed, it checks whether [b] is a prefix of [a], that is,
that [a] equals [b] or refines [b] with (a list of) sub-category(ies).
- @since Frama-C+dev *)
+ @since 18.0-Argon *)
val is_subcategory : string list -> string list -> bool
(** Each plugin has its own channel to output messages.
@@ -446,7 +446,7 @@ val kernel_label_name: string
val source : file:Filepath.Normalized.t -> line:int -> Filepath.position
(** @since Chlorine-20180501
- @modify Frama-C+dev change type of [file]
+ @modify 18.0-Argon change type of [file]
*)
val get_current_source : unit -> Filepath.position
diff --git a/src/kernel_services/plugin_entry_points/plugin.mli b/src/kernel_services/plugin_entry_points/plugin.mli
index 09efba3f25bd058e05a8aa6ce8e4585ae67d16a2..cf9adbaa4e1277bc9b94a1199256dc12a729aa79 100644
--- a/src/kernel_services/plugin_entry_points/plugin.mli
+++ b/src/kernel_services/plugin_entry_points/plugin.mli
@@ -69,7 +69,7 @@ module type S_no_log = sig
-plugin-msg-key, and -plugin-warn-key.
[add_plugin_output_aliases [alias]] adds the aliases -alias-help,
-alias-verbose, etc.
- @since Frama-C+dev *)
+ @since 18.0-Argon *)
end
(** Provided plug-general services for plug-ins.
diff --git a/src/libraries/datatype/datatype.mli b/src/libraries/datatype/datatype.mli
index cb813ba6dc83014ed37c1ae721c94206cabd04cd..605282f8bf42b4535e71b736934c9adc36139508 100644
--- a/src/libraries/datatype/datatype.mli
+++ b/src/libraries/datatype/datatype.mli
@@ -345,7 +345,7 @@ val integer: Integer.t Type.t
(** Type-safe strings representing normalized filepaths.
See module {!Filepath.Normalized}.
- @since Frama-C+dev *)
+ @since 18.0-Argon *)
module Filepath: sig
include S_with_collections with type t = Filepath.Normalized.t
val of_string: ?base_name:string -> string -> t
diff --git a/src/libraries/stdlib/extlib.mli b/src/libraries/stdlib/extlib.mli
index d331629c8bc5b0ddaa916a976a62ccb46793d280..9c98ba0a4c5279adbef1699ea0768febaf901e80 100644
--- a/src/libraries/stdlib/extlib.mli
+++ b/src/libraries/stdlib/extlib.mli
@@ -141,7 +141,7 @@ val find_opt : ('a -> 'b option) -> 'a list -> 'b
is no such value the list l.
@since Nitrogen-20111001
- @deprecated Frama-C+dev use [Transitioning.List.find_opt] instead *)
+ @deprecated 18.0-Argon use [Transitioning.List.find_opt] instead *)
val iteri: (int -> 'a -> unit) -> 'a list -> unit
(** Same as iter, but the function to be applied take also as argument the
@@ -178,7 +178,7 @@ val list_slice: ?first:int -> ?last:int -> 'a list -> 'a list
Negative indices are allowed, and count from the end of the list.
[list_slice] never raises exceptions: out-of-bounds arguments are clipped,
and inverted ranges result in empty lists.
- @since Frama-C+dev *)
+ @since 18.0-Argon *)
(* ************************************************************************* *)
(** {2 Arrays} *)
@@ -307,7 +307,7 @@ val strip_underscore: string -> string
(** remove underscores at the beginning and end of a string. If a string
is composed solely of underscores, return the empty string
- @since Frama-C+dev
+ @since 18.0-Argon
*)
val html_escape: string -> string
diff --git a/src/libraries/utils/filepath.mli b/src/libraries/utils/filepath.mli
index 2c9267e77f4d876dcae466f45a7f7aec92185018..b5fe7d255f9e545fb317ebdb064611c5759f766d 100644
--- a/src/libraries/utils/filepath.mli
+++ b/src/libraries/utils/filepath.mli
@@ -63,7 +63,7 @@ val is_relative: ?base_name:string -> string -> bool
in the filesystem.
@since Neon-20140301
- @deprecated since Frama-C+dev
+ @deprecated since 18.0-Argon
*)
val pretty: string -> string
[@@deprecated "Use Filepath.Normalized.to_pretty_string instead."]
@@ -76,7 +76,7 @@ val add_symbolic_dir: string -> string -> unit
(** The [Normalized] module is simply a wrapper that ensures that paths are
always normalized. Used by [Datatype.Filepath].
- @since Frama-C+dev *)
+ @since 18.0-Argon *)
module Normalized: sig
(** The normalized (absolute) path. *)
@@ -123,7 +123,7 @@ module Normalized: sig
end
(** Describes a position in a source file.
- @since Frama-C+dev
+ @since 18.0-Argon
*)
type position =
{
@@ -134,7 +134,7 @@ type position =
}
(** Pretty-prints a position, in the format file:line.
- @since Frama-C+dev
+ @since 18.0-Argon
*)
val pp_pos : Format.formatter -> position -> unit
diff --git a/tests/misc/oracle/debug_category.16.res.oracle b/tests/misc/oracle/debug_category.16.res.oracle
index 75e2529443bacd2087a9202069d4eee278b6f201..708cc59e04fa55dc3bb39458bb840dd6f145359b 100644
--- a/tests/misc/oracle/debug_category.16.res.oracle
+++ b/tests/misc/oracle/debug_category.16.res.oracle
@@ -9,7 +9,7 @@
Plug-in test aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
- Your Frama-C version is 18.0+dev (Argon).
+ Your Frama-C version is 18.0 (Argon).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
diff --git a/tests/misc/oracle/log-file.1.res.oracle b/tests/misc/oracle/log-file.1.res.oracle
index a7ef0e3d8b8280aa5101209cf259ce5b9cc16375..f80564b48f8e005f479cfa2ebb10007902b71e17 100644
--- a/tests/misc/oracle/log-file.1.res.oracle
+++ b/tests/misc/oracle/log-file.1.res.oracle
@@ -14,7 +14,7 @@
Frama-C aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
- Your Frama-C version is 18.0+dev (Argon).
+ Your Frama-C version is 18.0 (Argon).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
diff --git a/tests/misc/oracle/plugin-log-all.txt b/tests/misc/oracle/plugin-log-all.txt
index 2483f6ebcc8f221037ad68a82185c2ff62960064..1a773b13cb6c253a07b1204bddef249e3ba04f0e 100644
--- a/tests/misc/oracle/plugin-log-all.txt
+++ b/tests/misc/oracle/plugin-log-all.txt
@@ -14,7 +14,7 @@ The full backtrace is:
Frama-C aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
-Your Frama-C version is 18.0+dev (Argon).
+Your Frama-C version is 18.0 (Argon).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines